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