Theory SyntaxAndSemantics

(* Formalization adapted from: 
   Fabián Fernando Serrano Suárez, "Formalización en Isar de la
   Meta-Lógica de Primer Orden." PhD thesis, 
   Departamento de Ciencias de la Computación e Inteligencia Artificial,
   Universidad de Sevilla, Spain, 2012.
   https://idus.us.es/handle/11441/57780.  In Spanish  *)

(*<*)
theory SyntaxAndSemantics
imports Main  
begin
(*>*)

datatype 'b formula = 
    FF
  | TT
  | atom 'b                 (* ("P_" [1000]) *)
  | Negation "'b formula"                   ("¬.(_)" [110] 110)
  | Conjunction "'b formula" "'b formula"     (infixl "∧."  109)
  | Disjunction "'b formula" "'b formula"     (infixl "∨."  108)
  | Implication "'b formula" "'b formula"   (infixl "→." 100)


lemma "(¬.¬. Atom P →. Atom Q  →. Atom R) = 
       (((¬. (¬. Atom P)) →. Atom Q) →. Atom R)"
by simp


datatype v_truth = Ttrue | Ffalse 


definition v_negation :: "v_truth ⇒ v_truth" where
 "v_negation x ≡ (if x = Ttrue then Ffalse else Ttrue)"

definition v_conjunction ::  "v_truth ⇒ v_truth ⇒ v_truth" where
 "v_conjunction x y ≡ (if x = Ffalse then Ffalse else y)"

definition v_disjunction ::  "v_truth ⇒ v_truth ⇒ v_truth" where
 "v_disjunction x y ≡ (if x = Ttrue then Ttrue else y)"

definition v_implication :: "v_truth ⇒ v_truth ⇒ v_truth" where
 "v_implication x y ≡ (if x = Ffalse then Ttrue else y)"


primrec t_v_evaluation :: "('b ⇒  v_truth) ⇒ 'b formula  ⇒ v_truth"
where
   "t_v_evaluation I FF = Ffalse"
|  "t_v_evaluation I TT = Ttrue"
|  "t_v_evaluation I (atom p) = I p"
|  "t_v_evaluation I (¬. F) = (v_negation (t_v_evaluation I F))"
|  "t_v_evaluation I (F ∧. G) = (v_conjunction (t_v_evaluation I F) (t_v_evaluation I G))"
|  "t_v_evaluation I (F ∨. G) = (v_disjunction (t_v_evaluation I F) (t_v_evaluation I G))"
|  "t_v_evaluation I (F →. G) = (v_implication (t_v_evaluation I F) (t_v_evaluation I G))"  


lemma Bivaluation:
shows "t_v_evaluation I F = Ttrue ∨  t_v_evaluation I F = Ffalse"
(*<*)
proof(cases "t_v_evaluation I F")
  assume "t_v_evaluation I F = Ttrue" thus ?thesis by simp
  next  
  assume hip: "t_v_evaluation I F = Ffalse" thus ?thesis by simp
qed
(*>*)


lemma NegationValues1:
assumes "t_v_evaluation I (¬.F) = Ffalse"
shows "t_v_evaluation I F = Ttrue"
(*<*)
proof -
  { assume "t_v_evaluation I F ≠ Ttrue"
    hence "t_v_evaluation I F = Ffalse"  using Bivaluation by auto
    hence "t_v_evaluation I (¬.F) = Ttrue" by(simp add:v_negation_def)
    hence "False"
      using assms by auto}
  thus "t_v_evaluation I F = Ttrue" by auto
qed
(*>*)


lemma NegationValues2:
assumes "t_v_evaluation I (¬.F) = Ttrue"
shows "t_v_evaluation I F = Ffalse"
(*<*)
proof -
  { assume "t_v_evaluation I F ≠ Ffalse"
    hence "t_v_evaluation I F = Ttrue"  using Bivaluation by auto
    hence "t_v_evaluation I (¬.F) = Ffalse" by(simp add:v_negation_def)
    hence "False" using assms by auto}
  thus "t_v_evaluation I F = Ffalse" by auto
qed
(*>*)

lemma  non_Ttrue:
  assumes "t_v_evaluation I F ≠  Ttrue" shows "t_v_evaluation I F = Ffalse"
(*<*)
proof(rule ccontr)
  assume "t_v_evaluation I F ≠ Ffalse"
  thus False using assms Bivaluation by auto
qed
(*>*)


lemma ConjunctionValues: 
  assumes "t_v_evaluation I (F ∧. G) = Ttrue" 
  shows "t_v_evaluation I F = Ttrue ∧ t_v_evaluation I G = Ttrue"
(*<*)
proof - 
 { assume "¬(t_v_evaluation I  F = Ttrue ∧ t_v_evaluation I  G = Ttrue)" 
   hence "t_v_evaluation I  F ≠ Ttrue ∨ t_v_evaluation I G ≠ Ttrue" by simp
   hence "t_v_evaluation I  F = Ffalse ∨ t_v_evaluation I G = Ffalse" using Bivaluation by auto
   hence "t_v_evaluation I (F ∧. G) = Ffalse" by(auto simp add: v_conjunction_def)
   hence "False" using assms by simp}    
 thus "t_v_evaluation I F = Ttrue ∧ t_v_evaluation I G = Ttrue" by auto
qed
(*>*)


lemma DisjunctionValues:
  assumes "t_v_evaluation I (F ∨. G ) = Ttrue"
  shows "t_v_evaluation I  F = Ttrue ∨ t_v_evaluation I G = Ttrue" 
(*<*)
proof - 
 { assume "¬(t_v_evaluation I  F = Ttrue ∨ t_v_evaluation I G  = Ttrue)" 
   hence "t_v_evaluation I F  ≠ Ttrue ∧ t_v_evaluation I G ≠ Ttrue" by simp
   hence "t_v_evaluation I  F = Ffalse ∧ t_v_evaluation I G = Ffalse" using Bivaluation by auto
   hence "t_v_evaluation I (F ∨. G) = Ffalse" by(simp add: v_disjunction_def)
   hence "False" using assms by simp}    
 thus "t_v_evaluation I F = Ttrue ∨ t_v_evaluation I G = Ttrue" by auto
qed
(*>*)


lemma ImplicationValues:
  assumes "t_v_evaluation I (F →. G) = Ttrue"
  shows "t_v_evaluation I F = Ttrue ⟶ t_v_evaluation I G = Ttrue"
(*<*) 
proof - 
 { assume "¬(t_v_evaluation I F = Ttrue ⟶ t_v_evaluation I G = Ttrue)" 
   hence "t_v_evaluation I F =  Ttrue ∧ t_v_evaluation I G ≠ Ttrue" by simp
   hence "t_v_evaluation I F = Ttrue ∧ t_v_evaluation I G = Ffalse" using Bivaluation by auto
   hence "t_v_evaluation I (F →. G) = Ffalse" by(simp add: v_implication_def)
   hence "False" using assms by simp}    
 thus "t_v_evaluation I F = Ttrue ⟶ t_v_evaluation I G = Ttrue" by auto
qed

lemma eval_false_implication:
  assumes "t_v_evaluation I (F →.G) = Ffalse"
  shows "t_v_evaluation I F = Ttrue ∧ t_v_evaluation I G = Ffalse"
proof(rule ccontr) 
  assume "¬ (t_v_evaluation I F = Ttrue ∧ t_v_evaluation I G = Ffalse)"
  hence "t_v_evaluation I F = Ffalse ∨ t_v_evaluation I G = Ttrue"
    using Bivaluation by auto 
  hence "t_v_evaluation I (F →.G) = Ttrue"
    by(unfold t_v_evaluation_def, unfold v_implication_def, auto) 
  thus False using assms by auto
qed

(*>*)


definition model :: "('b ⇒ v_truth) ⇒ 'b formula set ⇒ bool" ("_ model _" [80,80] 80) where
 "I model S ≡ (∀F ∈ S. t_v_evaluation I F = Ttrue)"


definition satisfiable :: "'b formula set ⇒ bool" where
 "satisfiable S ≡ (∃v. v model S)"

(*<*)

lemma satisfiable_subset:
  assumes "satisfiable S" and "H⊆S"
  shows "satisfiable H"
proof(unfold satisfiable_def)
  show "∃v. v model H"
  proof-
    have "∃v. v model S" using assms(1) by(unfold satisfiable_def)
    then obtain v where v: "v model S" by auto
    have "v model H"
    proof(unfold model_def)
      show  "∀F∈H. t_v_evaluation v F = Ttrue"
      proof
        fix F
        assume "F∈H"
        thus "t_v_evaluation v F = Ttrue" using assms(2) v by(unfold model_def, auto)
      qed
    qed
    thus ?thesis by auto
  qed
qed

(*>*)

  
definition consequence :: "'b formula set ⇒ 'b formula ⇒ bool" ("_ ⊨ _" [80,80] 80) where
 "S ⊨ F ≡ (∀I. I model S ⟶ t_v_evaluation I F = Ttrue)"


(*<*)

lemma ConsSat:
  assumes "S ⊨ F"
  shows "¬ satisfiable (S ∪ {¬. F})"
proof(rule notI)
  assume "satisfiable (S ∪ {¬. F})"
  hence 1: "∃I. I model (S ∪ {¬. F})" by (auto simp add: satisfiable_def) 
  obtain I where I: "I model (S ∪ {¬. F})" using 1 by auto
  hence 2: "∀G∈(S ∪ {¬. F}). t_v_evaluation I G = Ttrue" 
    by (auto simp add: model_def)
  hence "∀G∈S. t_v_evaluation I G = Ttrue" by blast
  moreover
  have 3: "t_v_evaluation I (¬. F) = Ttrue" using 2 by simp
  hence "t_v_evaluation I F = Ffalse" 
    proof (cases "t_v_evaluation I F")
      assume "t_v_evaluation I F = Ttrue" 
      thus ?thesis using 3 by(simp add:v_negation_def)
      next
      assume "t_v_evaluation I F = Ffalse" 
      thus ?thesis by simp
    qed
  ultimately 
  show "False" using assms 
    by (simp add: consequence_def, simp add: model_def)
qed


lemma SatCons:
  assumes "¬ satisfiable (S ∪ {¬. F})"
  shows "S ⊨ F"
proof (rule contrapos_np)
  assume hip: "¬ S ⊨ F"
  show "satisfiable (S ∪ {¬. F})"
  proof -
    have 1: "∃I. I model S ∧ ¬(t_v_evaluation I F = Ttrue)"  
      using hip by (simp add: consequence_def)
    obtain I where I: "I model S ∧ ¬(t_v_evaluation I F = Ttrue)" using 1 by auto
    hence  "I model S" by simp
    hence 2: "∀G∈S. t_v_evaluation I G = Ttrue" by (simp add: model_def) 
    have "¬(t_v_evaluation I F = Ttrue)" using I by simp
    hence 3: "t_v_evaluation I (¬. F) = Ttrue" by (simp add:v_negation_def)
    have  "∀G∈(S ∪ {¬. F}). t_v_evaluation I G = Ttrue" 
    proof (rule ballI) 
      fix G 
      assume hip2: "G∈(S ∪ {¬. F})"    
      show "t_v_evaluation I G = Ttrue"
      proof (cases)
        assume "G∈S"
        thus ?thesis using 2 by simp
        next
        assume "¬G∈S"
        hence "G = (¬. F)"using hip2 by simp
        thus ?thesis using 3 by simp
      qed
    qed
    hence "I model (S ∪ {¬. F})" by (simp add: model_def)   
    thus ?thesis by (auto simp add: satisfiable_def)
  qed
  next
  show "¬ satisfiable (S ∪ {¬. F})" using assms by simp
qed 
(*>*)

 
theorem EquiConsSat: 
  shows  "S ⊨ F = (¬ satisfiable (S ∪ {¬. F}))"
(*<*)
using SatCons ConsSat by blast
(*>*)


definition tautology :: "'b formula ⇒ bool" where
  "tautology F ≡ (∀I. ((t_v_evaluation I F) = Ttrue))"

lemma "tautology (F  →. (G →. F))" 
proof - 
  have "∀I. t_v_evaluation I (F →. (G →. F)) = Ttrue"
  proof 
    fix I
    show "t_v_evaluation I (F →. (G →. F)) = Ttrue"
    proof (cases "t_v_evaluation I F")
      text‹ Caso 1: ›    
    { assume "t_v_evaluation I F = Ttrue"        
      thus ?thesis by (simp add: v_implication_def) }               
      next 
      text‹ Caso 2: › 
    { assume "t_v_evaluation I F = Ffalse"    
      thus ?thesis by(simp add: v_implication_def) }     
    qed 
  qed  
  thus ?thesis by (simp add: tautology_def)
qed



(*<*)


lemma empty_model: "∀(I::'b ⇒ v_truth). I model {}"
proof - 
  have "∀F∈ {}. t_v_evaluation (I::'b ⇒ v_truth) F = Ttrue" by simp
  thus "∀I. I model {}" by (simp add: model_def)
qed
(*>*)


theorem CNS_tautology: "tautology F = ({} ⊨ F)"
(*<*)
by(simp add: tautology_def consequence_def empty_model)
(*>*)



theorem TautSatis:
  shows "tautology (F →. G) = (¬ satisfiable{F, ¬.G})"
(*<*)
proof -
 { assume h1: "¬ tautology (F →. G)"
   have "satisfiable{F, ¬.G}"
   proof -
     have "∃ I. t_v_evaluation I (F →. G) ≠ Ttrue" 
       using h1 by (unfold tautology_def, auto) 
    then obtain I where "t_v_evaluation I (F →. G) ≠ Ttrue" by auto 
    hence a: "t_v_evaluation I (F →. G) = Ffalse" using Bivaluation by blast
    hence "t_v_evaluation I F = Ttrue ∧ t_v_evaluation I G = Ffalse" 
    proof -
     { assume "t_v_evaluation I F ≠ Ttrue ∨ t_v_evaluation I G ≠ Ffalse"
       hence "False"
       proof(rule disjE)
         assume "t_v_evaluation I F ≠ Ttrue"
         hence "t_v_evaluation I F = Ffalse" using Bivaluation by auto
         hence "t_v_evaluation I (F →. G) = Ttrue" 
           by (auto simp add: v_implication_def)
         thus "False" using a by auto
       next
         assume "t_v_evaluation I G ≠ Ffalse"
         hence "t_v_evaluation I G = Ttrue" using Bivaluation by auto
         hence "t_v_evaluation I (F →. G) = Ttrue" by( simp add: v_implication_def)
         thus "False" using a by auto
       qed}  
     thus "t_v_evaluation I F = Ttrue ∧ t_v_evaluation I G = Ffalse" by auto
   qed
   hence "t_v_evaluation I F = Ttrue ∧ t_v_evaluation I (¬.G) = Ttrue" 
     by (simp add:v_negation_def)
   hence "∃ I. I model {F, ¬.G}" by (auto simp add: model_def)  
   thus "satisfiable {F, ¬.G}" by(simp add: satisfiable_def)
 qed}
moreover
{ assume h2: "satisfiable {F, ¬.G}" 
  have "¬ tautology (F →. G)" 
  proof -  
    have "∃ I. I model {F, ¬.G}" using h2 by (simp add: satisfiable_def)  
    hence "∃ I. t_v_evaluation I F = Ttrue ∧ t_v_evaluation I (¬.G) = Ttrue" 
      by(simp add: model_def)
    then obtain I where I1: "t_v_evaluation I F = Ttrue" and I2: "t_v_evaluation I (¬.G) = Ttrue"
      by auto
    have "t_v_evaluation I G = Ffalse" using I2 NegationValues2 by auto   
    hence "t_v_evaluation I (F →. G) = Ffalse" using I1 
      by (simp add: v_implication_def)
    thus "¬ tautology (F →. G)" by (auto, unfold tautology_def, auto)
  qed}
  ultimately
  show ?thesis by auto
qed

  
definition equivalent:: "'b formula  ⇒ 'b formula ⇒ bool" where
  "equivalent F G ≡ (∀ I. (t_v_evaluation I F) = (t_v_evaluation I G))"

primrec disjunction_atomic :: "'b list ⇒'a ⇒ ('a × 'b)formula"  where
 "disjunction_atomic [] i = FF"   
| "disjunction_atomic (x#D) i = (atom (i, x)) ∨. (disjunction_atomic D i)"

lemma t_v_evaluation_disjunctions1:
  assumes "t_v_evaluation I (disjunction_atomic (a # l) i) = Ttrue"
  shows "t_v_evaluation I (atom (i,a)) = Ttrue ∨ t_v_evaluation I (disjunction_atomic l i) = Ttrue" 
proof-
  have
  "(disjunction_atomic (a # l) i) = (atom (i,a)) ∨. (disjunction_atomic l i)"
    by auto
  hence "t_v_evaluation I ((atom (i ,a)) ∨. (disjunction_atomic l i)) = Ttrue" 
    using assms by auto
  thus ?thesis using DisjunctionValues by blast
qed

lemma t_v_evaluation_atom:
  assumes "t_v_evaluation I (disjunction_atomic l i) = Ttrue"
  shows "∃x. x ∈ set l ∧ (t_v_evaluation I (atom (i,x)) = Ttrue)"
proof-
  have "t_v_evaluation I (disjunction_atomic l i) = Ttrue ⟹
  ∃x. x ∈ set l ∧ (t_v_evaluation I (atom (i,x)) = Ttrue)"
  proof(induct l)
    case Nil
    then show ?case by auto
  next   
    case (Cons a l)  
    show  "∃x. x ∈ set (a # l) ∧ t_v_evaluation I (atom (i,x)) = Ttrue"  
    proof-
      have
      "(t_v_evaluation I (atom (i,a)) = Ttrue) ∨ t_v_evaluation I (disjunction_atomic l i)=Ttrue" 
        using Cons(2) t_v_evaluation_disjunctions1[of I] by auto      
      thus ?thesis
    proof(rule disjE)
      assume "t_v_evaluation I (atom (i,a)) = Ttrue"
      thus ?thesis by auto
    next
      assume "t_v_evaluation I (disjunction_atomic l i) = Ttrue" 
      thus ?thesis using Cons by auto    
    qed
  qed
qed
  thus ?thesis using assms by auto
qed 

definition set_to_list :: "'a set ⇒ 'a list"
  where "set_to_list s =  (SOME l. set l = s)"

lemma  set_set_to_list:
   "finite s ⟹ set (set_to_list s) = s"
  unfolding set_to_list_def by (metis (mono_tags) finite_list some_eq_ex)


(*>*)
     
(*<*)
end
(*>*)