(* https://kwarc.info/teaching/AI/assignments/a8.pdf *)
theory ded
imports Main
begin

typedecl v

definition entails :: "(v ⇒ bool) ⇒ v set ⇒ bool" (infix "⊧" 50) where
  "M ⊧ F ⟷ (∀p ∈ F. M p = True)"
declare entails_def[simp]

lemma satisfy_p:
  assumes "M p = True"
  shows "M ⊧ {p}"
  using assms by simp

lemma falsify_p:
  assumes "M p = False"
  shows "¬ M ⊧ {p}"
  using assms by simp

definition M' :: "v ⇒ bool"
  where "M' p = True"

lemma no_unsatisfiable:
  shows "¬ (∃ F. ∀ M. ¬ M ⊧ F)"
proof
  assume "∃ F. ∀ M. ¬ M ⊧ F"
  then obtain F where "∀ M. ¬ M ⊧ F" by auto
  hence H : "∀ M. ∀ p ∈ F. M p = False" by auto
  have "∀ p ∈ F. M' p = False" using H by auto
  moreover have "∀ p ∈ F. M' p = True" by (simp add: M'_def)
  ultimately show False by blast
qed

lemma valid_empty:
  shows "M ⊧ {}"
  by simp

end