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
   Last modified: 11 Aug, 2025
  *)

(*<*)
theory SyntaxAndSemantics
imports Main HOL.List
begin
(*>*)

datatype 'b formula = 
    FF                                      (‹⊥.›)
  | TT                                      (‹⊤.›)
  | atom 'b                
  | 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)


primrec t_v_evaluation :: "('b ⇒  bool) ⇒ 'b formula  ⇒ bool"
where
   "t_v_evaluation I ⊥. = False"
|  "t_v_evaluation I ⊤. = True"
|  "t_v_evaluation I (atom p) = I p"
|  "t_v_evaluation I (¬. F) = (¬ (t_v_evaluation I F))"
|  "t_v_evaluation I (F ∧. G) = ( (t_v_evaluation I F) ∧ (t_v_evaluation I G))"
|  "t_v_evaluation I (F ∨. G) = ( (t_v_evaluation I F) ∨ (t_v_evaluation I G))"
|  "t_v_evaluation I (F →. G) = ( (t_v_evaluation I F) ⟶ (t_v_evaluation I G))"  

lemma eval_false_implication:
  assumes "¬ t_v_evaluation I (F →.G)"
  shows "t_v_evaluation I F ∧ ¬ t_v_evaluation I G "
  by (meson assms t_v_evaluation.simps(7))

(*>*)

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

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"
  by (meson assms(1,2) model_def satisfiable_def subset_iff)
(*>*)

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

(*<*)

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" 
    by (auto simp add: model_def)
  hence "∀G∈S. t_v_evaluation I G" by blast
  moreover
   have 3: "t_v_evaluation I (¬. F)" using 2 by simp
   hence "¬t_v_evaluation I F" by auto 
  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)"  
      using hip by (simp add: consequence_def)
    obtain I where I: "I model S ∧ ¬(t_v_evaluation I F = True)" using 1 by auto
    hence  "I model S" by simp
    hence 2: "∀G∈S. t_v_evaluation I G" by (simp add: model_def) 
    have "¬t_v_evaluation I F" using I by simp
    hence 3: "t_v_evaluation I (¬. F)" by simp
    have  "∀G∈(S ∪ {¬. F}). t_v_evaluation I G" 
    proof (rule ballI) 
      fix G 
      assume hip2: "G∈(S ∪ {¬. F})"    
      show "t_v_evaluation I G"
      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)))"

lemma "tautology (F  →. (G →. F))"
  by (simp add: tautology_def)

lemma empty_model: "∀(I::'b ⇒ bool). I model {}"
proof - 
  fix I
  have "∀F∈ {}. t_v_evaluation (I::'b ⇒ bool) F" 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)" 
       using h1 by (unfold tautology_def, auto) 
    then obtain I where "¬ t_v_evaluation I (F →. G)" by auto 
    hence a: "¬ t_v_evaluation I (F →. G)"  by auto
    hence "t_v_evaluation I F  ∧ ¬t_v_evaluation I G" 
    proof -             
     { assume "¬ t_v_evaluation I F ∨ t_v_evaluation I G"
       hence "False"
       proof(rule disjE)
         assume "¬t_v_evaluation I F"
         hence " ¬t_v_evaluation I F" by auto
         hence "t_v_evaluation I (F →. G)" 
           by simp
         thus "False" using a by auto
       next
         assume "t_v_evaluation I G"
         hence "t_v_evaluation I G" by auto
         hence "t_v_evaluation I (F →. G)" by simp
         thus "False" using a by auto
       qed}  
     thus "t_v_evaluation I F ∧ ¬ t_v_evaluation I G" by auto
   qed
   hence "t_v_evaluation I F = True ∧ t_v_evaluation I (¬.G)" 
     by simp
   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 ∧ t_v_evaluation I (¬.G)" 
      by(simp add: model_def)
    then obtain I where I1: "t_v_evaluation I F" and I2: "t_v_evaluation I (¬.G)"
      by auto
    have "¬ t_v_evaluation I G" using I2  by auto   
    hence "¬t_v_evaluation I (F →. G)" using I1 
      by simp
    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 = ⊥."   
| "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)"
  shows "t_v_evaluation I (atom (i,a)) ∨ t_v_evaluation I (disjunction_atomic l i)"
  using assms by auto

lemma t_v_evaluation_atom:
  assumes "t_v_evaluation I (disjunction_atomic l i)"
  shows "∃x. x ∈ set l ∧ (t_v_evaluation I (atom (i,x)))"
proof-
  have "t_v_evaluation I (disjunction_atomic l i) ⟹
  ∃x. x ∈ set l ∧ (t_v_evaluation I (atom (i,x)))"
  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))"  
    proof-
      have
      "(t_v_evaluation I (atom (i,a))) ∨ t_v_evaluation I (disjunction_atomic l i)" 
        using Cons(2) t_v_evaluation_disjunctions1[of I] by auto      
      thus ?thesis
    proof(rule disjE)
      assume "t_v_evaluation I (atom (i,a))"
      thus ?thesis by auto
    next
      assume "t_v_evaluation I (disjunction_atomic l i)" 
      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  finiteness_set_to_list:
   "finite s ≡ (set (set_to_list s) = s)"
  unfolding set_to_list_def using List.finite_set finite_list tfl_some
  by (smt (verit, del_insts)) 

end