Theory Tseytin_Sema

theory Tseytin_Sema
imports Sema Tseytin
begin           

lemma biimp_simp[simp]: "𝒜 ⊨ F ❙↔ G ⟷ (𝒜 ⊨ F ⟷ 𝒜 ⊨ G)"
  unfolding biimp_def by auto
    
locale freshstuff_sema = freshstuff
begin
  
definition "tseytin_update 𝒜 F ≡ (let U = map (apsnd (formula_semantics 𝒜)) (tseytin_assmt F) in foldl pair_fun_upd 𝒜 U)"

lemma tseyting_update_keep_subformula_sema: "G ∈ set (subformulae F) ⟹ tseytin_update 𝒜 F ⊨ G ⟷ 𝒜 ⊨ G"
proof -
  assume "G ∈ set (subformulae F)"
  hence sub: "atoms G ⊆ atoms F" by(fact subformula_atoms)
  have natoms: "k ∈ atoms F ⟹ k ∉ fst ` set (tseytin_assmt F)" for k l 
    using tseytin_assmt_new_atoms by force
  have "k ∈ atoms F ⟹ tseytin_update 𝒜 F k = 𝒜 k" for k
    unfolding tseytin_update_def Let_def 
    by(force intro!: fold_pair_upd_triv dest!: natoms)
  thus ?thesis using relevant_atoms_same_semantics sub by (metis subsetCE)
qed   

lemma "(k,G) ∈ set (tseytin_assmt F) ⟹ tseytin_update 𝒜 F k ⟷ tseytin_update 𝒜 F ⊨ G"
proof(induction F arbitrary: G)
  case (Atom x)
  then show ?case by(simp add: tseytin_update_def tseytin_assmt_def Let_def pair_fun_upd_def)
next
  case Bot
  then show ?case by(simp add: tseytin_update_def tseytin_assmt_def Let_def pair_fun_upd_def)
next
  case (Not F)
  then show ?case
    oops
      
lemma tseytin_updates: "(k,G) ∈ set (tseytin_assmt F) ⟹ tseytin_update 𝒜 F k ⟷ tseytin_update 𝒜 F ⊨ G"
  apply(subst tseytin_update_def)
  apply(simp add: tseytin_assmt_def Let_def foldl_pair_fun_upd_map_of map_of_map_apsnd distinct_zipunzip[OF nfresh_distinct[OF atoms_finite]])
  apply(subst tseyting_update_keep_subformula_sema)
   apply(erule in_set_zipE; simp; fail)
  ..

lemma tseytin_tran1: "G ∈ set (subformulae F) ⟹ H ∈ set (tseytin_tran1 S G) ⟹ ∀J ∈ set (subformulae F). tseytin_update 𝒜 F ⊨ J ⟷ tseytin_update 𝒜 F ⊨ (S J) ⟹ tseytin_update 𝒜 F ⊨ H"
proof(induction G arbitrary: H)
  case Bot thus ?case by auto
next
  case (Atom k) thus ?case by fastforce
next
  case (Not G)
  consider "H = S (❙¬ G) ❙↔ ❙¬ (S G)" | " H ∈ set (tseytin_tran1 S G)" using Not.prems(2) by auto
  then show ?case proof cases
    case 1 then show ?thesis using Not.prems(3)
      by (metis Not.prems(1) biimp_simp formula_semantics.simps(3) set_subset_Cons subformulae.simps(3) subformulae_self subsetCE subsubformulae)
  next
    have D: "❙¬G ∈ set (subformulae F) ⟹ G ∈ set (subformulae F)"
      by(elim subsubformulae; simp)
    case 2 then show ?thesis using D Not.IH Not.prems(1,3) by blast
  qed
next
  case (And G1 G2)
  have el: "G1 ∈ set (subformulae F)" "G2 ∈ set (subformulae F)" using subsubformulae And.prems(1) by fastforce+
  with And.IH And.prems(3) have IH: "H ∈ set (tseytin_tran1 S G1) ⟹ tseytin_update 𝒜 F ⊨ H"
                                    "H ∈ set (tseytin_tran1 S G2) ⟹ tseytin_update 𝒜 F ⊨ H" for H
    by blast+
  show ?case using And.prems IH el by(simp; elim disjE; simp; insert And.prems(1) formula_semantics.simps(4), blast)
next
  case (Or G1 G2)
  have el: "G1 ∈ set (subformulae F)" "G2 ∈ set (subformulae F)" using subsubformulae Or.prems(1) by fastforce+
  with Or.IH Or.prems(3) have IH: "H ∈ set (tseytin_tran1 S G1) ⟹ tseytin_update 𝒜 F ⊨ H"
                                  "H ∈ set (tseytin_tran1 S G2) ⟹ tseytin_update 𝒜 F ⊨ H" for H
    by blast+
  show ?case using Or.prems(3,2) IH el by(simp; elim disjE; simp; metis Or.prems(1) formula_semantics.simps(5))
next
  case (Imp G1 G2)
  have el: "G1 ∈ set (subformulae F)" "G2 ∈ set (subformulae F)" using subsubformulae Imp.prems(1) by fastforce+
  with Imp.IH Imp.prems(3) have IH: "H ∈ set (tseytin_tran1 S G1) ⟹ tseytin_update 𝒜 F ⊨ H"
                                    "H ∈ set (tseytin_tran1 S G2) ⟹ tseytin_update 𝒜 F ⊨ H" for H
    by blast+
  show ?case using Imp.prems(3,2) IH el by(simp; elim disjE; simp; metis Imp.prems(1) formula_semantics.simps(6))
qed

lemma all_tran_formulas_validated: "∀J ∈ set (subformulae F). tseytin_update 𝒜 F ⊨ J ⟷ tseytin_update 𝒜 F ⊨ (tseytin_toatom F J)"
  apply(simp add: tseytin_toatom_def)
  apply(intro ballI)
  apply(subst tseytin_updates)
   apply(erule tseytin_assmt_backlookup)
  ..

lemma tseytin_tran_equisat: "𝒜 ⊨ F ⟷ tseytin_update 𝒜 F ⊨ (tseytin_tran F)"
  using all_tran_formulas_validated tseytin_tran1 all_tran_formulas_validated tseyting_update_keep_subformula_sema by(simp add: tseytin_tran_def Let_def) blast
(* unfortunately, that's not enough. *)
    
lemma tseytin_tran1_orig_connection: "G ∈ set (subformulae F) ⟹ (∀H∈set (tseytin_tran1 (tseytin_toatom F) G). 𝒜 ⊨ H) ⟹
  𝒜 ⊨ G ⟷ 𝒜 ⊨ tseytin_toatom F G"
  by(induction G; simp; drule subformulas_in_subformulas; simp)

lemma tseytin_untran: "𝒜 ⊨ (tseytin_tran F) ⟹ 𝒜 ⊨ F" 
proof -
  have 1: "⟦𝒜 ⊨ tseytin_toatom F F; 𝒜 ⊨ F⟧ ⟹ tseytin_update 𝒜 F ⊨ tseytin_toatom F F"
    using all_tran_formulas_validated tseyting_update_keep_subformula_sema by blast
  let ?C = "λ𝒜. (∀H ∈ set (tseytin_tran1 (tseytin_toatom F) F). 𝒜 ⊨ H)"
  have 2: "?C 𝒜 ⟹ ?C (tseytin_update 𝒜 F)"
    using all_tran_formulas_validated tseytin_tran1 by blast
  assume "𝒜 ⊨ tseytin_tran F"
  hence "tseytin_update 𝒜 F ⊨ tseytin_tran F" 
    unfolding tseytin_tran_def
    apply(simp add: Let_def)
    apply(intro conjI)
     apply(elim conjE)
     apply(drule tseytin_tran1_orig_connection[OF subformulae_self])
     apply(clarsimp simp add: tseytin_assmt_distinct foldl_pair_fun_upd_map_of 1 2)+
    done
  thus ?thesis using tseytin_tran_equisat by blast
qed
lemma tseytin_tran_equiunsatisfiable: "⊨ ❙¬F ⟷ ⊨ ❙¬ (tseytin_tran F)"  (is "?l ⟷ ?r")
proof(rule iffI; erule contrapos_pp)
  assume "¬?l"
  then obtain 𝒜 where "𝒜 ⊨ F" by auto
  hence "tseytin_update 𝒜 F ⊨ (tseytin_tran F)" using tseytin_tran_equisat by simp
  thus "¬?r" by simp blast
next
  assume "¬?r"
  then obtain 𝒜 where "𝒜 ⊨ tseytin_tran F" by auto
  thus "~?l" using tseytin_untran by simp blast 
qed
  
end
  
interpretation freshsemanats: freshstuff_sema freshnat
  by (simp add: freshnats.freshstuff_axioms freshstuff_sema_def)
print_theorems
(* Just showing that it is possible. There isn't really anything new that could be executed here. *)
  
end