Theory Propositional_Proof_Systems.Sema

subsection‹Semantics›
theory Sema
imports Formulas
begin

type_synonym 'a valuation = "'a ⇒ bool"
text‹The implicit statement here is that an assignment or valuation is always defined on all atoms (because HOL is a total logic).
Thus, there are no unsuitable assignments.›

primrec formula_semantics :: "'a valuation ⇒ 'a formula ⇒ bool" (infix ‹⊨› 51) where
"𝒜 ⊨ Atom k = 𝒜 k" |
"_ ⊨ ⊥ = False" |
"𝒜 ⊨ Not F = (¬ 𝒜 ⊨ F)" |
"𝒜 ⊨ And F G = (𝒜 ⊨ F ∧ 𝒜 ⊨ G)" |
"𝒜 ⊨ Or F G = (𝒜 ⊨ F ∨ 𝒜 ⊨ G)" |
"𝒜 ⊨ Imp F G = (𝒜 ⊨ F ⟶ 𝒜 ⊨ G)"

abbreviation valid (‹⊨ _› 51) where
"⊨ F ≡ ∀A. A ⊨ F"

lemma irrelevant_atom[simp]: "A ∉ atoms F ⟹ (𝒜(A := V)) ⊨ F ⟷ 𝒜 ⊨ F"
  by (induction F; simp)
lemma relevant_atoms_same_semantics: "∀k ∈ atoms F. 𝒜⇩1 k = 𝒜⇩2 k ⟹ 𝒜⇩1 ⊨ F ⟷ 𝒜⇩2 ⊨ F"
  by(induction F; simp)

context begin
text‹Just a definition more similar to~\<^cite>‹‹p. 5› in "schoening1987logik"›.
Unfortunately, using this as the main definition would get in the way of automated reasoning all the time.›
private primrec formula_semantics_alt where
"formula_semantics_alt 𝒜 (Atom k) = 𝒜 k" |
"formula_semantics_alt 𝒜 (Bot) = False" |
"formula_semantics_alt 𝒜 (Not a) = (if formula_semantics_alt 𝒜 a then False else True)" |
"formula_semantics_alt 𝒜 (And a b) = (if formula_semantics_alt 𝒜 a then formula_semantics_alt 𝒜 b else False)" |
"formula_semantics_alt 𝒜 (Or a b) = (if formula_semantics_alt 𝒜 a then True else formula_semantics_alt 𝒜 b)" |
"formula_semantics_alt 𝒜 (Imp a b) = (if formula_semantics_alt 𝒜 a then formula_semantics_alt 𝒜 b else True)"
private lemma "formula_semantics_alt 𝒜 F ⟷ 𝒜 ⊨ F"
  by(induction F; simp)

text‹If you fancy a definition more similar to~\<^cite>‹‹p. 39› in "gallier2015logic"›,
this is probably the closest you can go without going incredibly ugly.›
private primrec formula_semantics_tt where
"formula_semantics_tt 𝒜 (Atom k) = 𝒜 k" |
"formula_semantics_tt 𝒜 (Bot) = False" |
"formula_semantics_tt 𝒜 (Not a) = (case formula_semantics_tt 𝒜 a of True ⇒ False | False ⇒ True)" |
"formula_semantics_tt 𝒜 (And a b) = (case (formula_semantics_tt 𝒜 a, formula_semantics_tt 𝒜 b) of
  (False, False) ⇒ False
| (False, True) ⇒ False
| (True, False) ⇒ False
| (True, True) ⇒ True)" |
"formula_semantics_tt 𝒜 (Or a b) = (case (formula_semantics_tt 𝒜 a, formula_semantics_tt 𝒜 b) of
  (False, False) ⇒ False
| (False, True) ⇒ True
| (True, False) ⇒ True
| (True, True) ⇒ True)" |
"formula_semantics_tt 𝒜 (Imp a b) = (case (formula_semantics_tt 𝒜 a, formula_semantics_tt 𝒜 b) of
  (False, False) ⇒ True
| (False, True) ⇒ True
| (True, False) ⇒ False
| (True, True) ⇒ True)"
private lemma "A ⊨ F ⟷ formula_semantics_tt A F"
  by(induction F; simp split: prod.splits bool.splits)
end

definition entailment :: "'a formula set ⇒ 'a formula ⇒ bool" (‹(_ ⊫/ _)› (* \TTurnstile *) [53,53] 53) where
"Γ ⊫ F ≡ (∀𝒜. ((∀G ∈ Γ. 𝒜 ⊨ G) ⟶ (𝒜 ⊨ F)))"
text‹We write entailment differently than semantics (‹⊨› vs. ‹⊫›).
For humans, it is usually pretty clear what is meant in a specific situation, 
but it often needs to be decided from context that Isabelle/HOL does not have.›
  
text‹Some helpers for the derived connectives›
lemma top_semantics[simp,intro!]: "A ⊨ ⊤" unfolding Top_def by simp
lemma BigAnd_semantics[simp]: "A ⊨ ❙⋀F ⟷ (∀f ∈ set F. A ⊨ f)" by(induction F; simp)
lemma BigOr_semantics[simp]: "A ⊨ ❙⋁F ⟷ (∃f ∈ set F. A ⊨ f)" by(induction F; simp)
    
text‹Definitions for sets of formulae, used for compactness and model existence.›

definition "sat S ≡ ∃𝒜. ∀F ∈ S. 𝒜 ⊨ F"
definition "fin_sat S ≡ (∀s ⊆ S. finite s ⟶ sat s)"
  
lemma entail_sat: "Γ ⊫ ⊥ ⟷ ¬ sat Γ" (* btw. *)
  unfolding sat_def entailment_def by simp

lemma pn_atoms_updates: "p ∉ snd (pn_atoms F) ⟹ n ∉ fst (pn_atoms F) ⟹
  ((M ⊨ F ⟶ (M(p := True) ⊨ F ∧ M(n := False) ⊨ F))) ∧ ((¬(M ⊨ F)) ⟶ ¬(M(n := True) ⊨ F) ∧ ¬(M(p := False) ⊨ F))"
proof(induction F arbitrary: n p)
  case (Imp F G)
  from Imp.prems have prems:
     "p ∉ fst (pn_atoms F)" "p ∉ snd (pn_atoms G)"
     "n ∉ snd (pn_atoms F)" "n ∉ fst (pn_atoms G)"
    by(simp_all add: prod_unions_def split: prod.splits)
  have IH1: "M ⊨ F ⟹ M(n := True) ⊨ F" " M ⊨ F ⟹ M(p := False) ⊨ F" "¬ M ⊨ F ⟹ ¬ M(p := True) ⊨ F" "¬ M ⊨ F ⟹ ¬ M(n := False) ⊨ F"
    using Imp.IH(1)[OF prems(3) prems(1)] by blast+
  have IH2: "M ⊨ G ⟹ M(p := True) ⊨ G" "M ⊨ G ⟹ M(n := False) ⊨ G" "¬ M ⊨ G ⟹ ¬ M(n := True) ⊨ G" "¬ M ⊨ G ⟹ ¬ M(p := False) ⊨ G" 
    using Imp.IH(2)[OF prems(2) prems(4)] by blast+
   show ?case proof(intro conjI; intro impI)
     assume "M ⊨ F ❙→ G"
     then consider "¬ M ⊨ F" | "M ⊨G" by auto
     thus "M(p := True) ⊨ F ❙→ G ∧ M(n := False) ⊨ F ❙→ G" using IH1(3,4) IH2(1,2) by cases simp_all
   next
     assume "¬(M ⊨ F ❙→ G)"
     hence "M ⊨ F" "¬M ⊨ G" by simp_all
     thus "¬ M(n := True) ⊨ F ❙→ G ∧ ¬ M(p := False) ⊨ F ❙→ G" using IH1(1,2) IH2(3,4) by simp
   qed
 next
  case (And F G)
  from And.prems have prems:
     "p ∉ snd (pn_atoms F)" "p ∉ snd (pn_atoms G)"
     "n ∉ fst (pn_atoms F)" "n ∉ fst (pn_atoms G)"
    by(simp_all add: prod_unions_def split: prod.splits)
  have IH1: "M ⊨ F ⟹ M(p := True) ⊨ F" " M ⊨ F ⟹ M(n := False) ⊨ F" "¬ M ⊨ F ⟹ ¬ M(n := True) ⊨ F" "¬ M ⊨ F ⟹ ¬ M(p := False) ⊨ F"
    using And.IH(1)[OF prems(1) prems(3)] by blast+
  have IH2: "M ⊨ G ⟹ M(p := True) ⊨ G" "M ⊨ G ⟹ M(n := False) ⊨ G" "¬ M ⊨ G ⟹ ¬ M(n := True) ⊨ G" "¬ M ⊨ G ⟹ ¬ M(p := False) ⊨ G" 
    using And.IH(2)[OF prems(2) prems(4)] by blast+
  show ?case proof(intro conjI; intro impI)
    assume "¬M ⊨ F ❙∧ G"
    then consider "¬ M ⊨ F" | "¬ M ⊨G" by auto
    thus "¬ M(n := True) ⊨ F ❙∧ G ∧ ¬ M(p := False) ⊨ F ❙∧ G" using IH1 IH2 by cases simp_all
  next
    assume "M ⊨ F ❙∧ G"
    hence "M ⊨ F" "M ⊨ G" by simp_all
    thus "M(p := True) ⊨ F ❙∧ G ∧ M(n := False) ⊨ F ❙∧ G " using IH1 IH2 by simp
  qed
next
  case (Or F G)
  from Or.prems have prems:
     "p ∉ snd (pn_atoms F)" "p ∉ snd (pn_atoms G)"
     "n ∉ fst (pn_atoms F)" "n ∉ fst (pn_atoms G)"
    by(simp_all add: prod_unions_def split: prod.splits)
  have IH1: "M ⊨ F ⟹ M(p := True) ⊨ F" " M ⊨ F ⟹ M(n := False) ⊨ F" "¬ M ⊨ F ⟹ ¬ M(n := True) ⊨ F" "¬ M ⊨ F ⟹ ¬ M(p := False) ⊨ F"
    using Or.IH(1)[OF prems(1) prems(3)] by blast+
  have IH2: "M ⊨ G ⟹ M(p := True) ⊨ G" "M ⊨ G ⟹ M(n := False) ⊨ G" "¬ M ⊨ G ⟹ ¬ M(n := True) ⊨ G" "¬ M ⊨ G ⟹ ¬ M(p := False) ⊨ G" 
    using Or.IH(2)[OF prems(2) prems(4)] by blast+
  show ?case proof(intro conjI; intro impI)
    assume "M ⊨ F ❙∨ G"
    then consider "M ⊨ F" | "M ⊨G" by auto
    thus "M(p := True) ⊨ F ❙∨ G ∧ M(n := False) ⊨ F ❙∨ G" using IH1 IH2 by cases simp_all
  next
    assume "¬M ⊨ F ❙∨ G"
    hence "¬M ⊨ F" "¬M ⊨ G" by simp_all
    thus "¬M(n := True) ⊨ F ❙∨ G ∧ ¬M(p := False) ⊨ F ❙∨ G " using IH1 IH2 by simp
  qed
qed simp_all
  
lemma const_simplifier_correct: "𝒜 ⊨ simplify_consts F ⟷ 𝒜 ⊨ F"
  by (induction F) (auto simp add: Let_def isstop_def Top_def split: formula.splits) 
 
end