Theory Sequent_Calculus_Verifier

(*
  Author: Jørgen Villadsen, DTU Compute, 2020
*)

section ‹Appendix: Completeness›

theory Sequent_Calculus_Verifier imports Sequent1 SeCaV begin

primrec from_tm and from_tm_list where
  ‹from_tm (Var n) = FOL_Fitting.Var n› |
  ‹from_tm (Fun a ts) = App a (from_tm_list ts)› |
  ‹from_tm_list [] = []› |
  ‹from_tm_list (t # ts) = from_tm t # from_tm_list ts›

primrec from_fm where
  ‹from_fm (Pre b ts) = Pred b (from_tm_list ts)› |
  ‹from_fm (Con p q) = And (from_fm p) (from_fm q)› |
  ‹from_fm (Dis p q) = Or (from_fm p) (from_fm q)› |
  ‹from_fm (Imp p q) = Impl (from_fm p) (from_fm q)› |
  ‹from_fm (Neg p) = FOL_Fitting.Neg (from_fm p)› |
  ‹from_fm (Uni p) = Forall (from_fm p)› |
  ‹from_fm (Exi p) = Exists (from_fm p)›

primrec to_tm and to_tm_list where
  ‹to_tm (FOL_Fitting.Var n) = Var n› |
  ‹to_tm (App a ts) = Fun a (to_tm_list ts)› |
  ‹to_tm_list [] = []› |
  ‹to_tm_list (t # ts) = to_tm t # to_tm_list ts›

primrec to_fm where
  ‹to_fm ⊥ = Neg (Imp (Pre 0 []) (Pre 0 []))› |
  ‹to_fm ⊤ = Imp (Pre 0 []) (Pre 0 [])› |
  ‹to_fm (Pred b ts) = Pre b (to_tm_list ts)› |
  ‹to_fm (And p q) = Con (to_fm p) (to_fm q)› |
  ‹to_fm (Or p q) = Dis (to_fm p) (to_fm q)› |
  ‹to_fm (Impl p q) = Imp (to_fm p) (to_fm q)› |
  ‹to_fm (FOL_Fitting.Neg p) = Neg (to_fm p)› |
  ‹to_fm (Forall p) = Uni (to_fm p)› |
  ‹to_fm (Exists p) = Exi (to_fm p)›

theorem to_from_tm [simp]: ‹to_tm (from_tm t) = t› ‹to_tm_list (from_tm_list ts) = ts›
  by (induct t and ts rule: from_tm.induct from_tm_list.induct) simp_all

theorem to_from_fm [simp]: ‹to_fm (from_fm p) = p›
  by (induct p) simp_all

lemma Truth [simp]: ‹⊩ Imp (Pre 0 []) (Pre 0 []) # z›
  using AlphaImp Basic Ext ext.simps member.simps(2) by metis

lemma paramst [simp]:
  ‹FOL_Fitting.new_term c t = new_term c (to_tm t)›
  ‹FOL_Fitting.new_list c l = new_list c (to_tm_list l)›
  by (induct t and l rule: FOL_Fitting.paramst.induct FOL_Fitting.paramsts.induct) simp_all

lemma params [iff]: ‹FOL_Fitting.new c p ⟷ new c (to_fm p)›
  by (induct p) simp_all

lemma list_params [iff]: ‹FOL_Fitting.news c z ⟷ news c (map to_fm z)›
  by (induct z) simp_all

lemma liftt [simp]:
  ‹to_tm (FOL_Fitting.liftt t) = inc_term (to_tm t)›
  ‹to_tm_list (FOL_Fitting.liftts l) = inc_list (to_tm_list l)›
  by (induct t and l rule: FOL_Fitting.liftt.induct FOL_Fitting.liftts.induct) simp_all

lemma substt [simp]:
  ‹to_tm (FOL_Fitting.substt t s v) = sub_term v (to_tm s) (to_tm t)›
  ‹to_tm_list (FOL_Fitting.substts l s v) = sub_list v (to_tm s) (to_tm_list l)›
  by (induct t and l rule: FOL_Fitting.substt.induct FOL_Fitting.substts.induct) simp_all

lemma subst [simp]: ‹to_fm (FOL_Fitting.subst A t s) = sub s (to_tm t) (to_fm A)›
  by (induct A arbitrary: t s) simp_all

lemma sim: ‹(⊢ x) ⟹ (⊩ (map to_fm x))›
  by (induct rule: SC.induct) (force intro: sequent_calculus.intros)+

lemma evalt [simp]:
  ‹semantics_term e f t = evalt e f (from_tm t)›
  ‹semantics_list e f ts = evalts e f (from_tm_list ts)›
  by (induct t and ts rule: from_tm.induct from_tm_list.induct) simp_all

lemma shift [simp]: ‹shift e 0 x = e⟨0:x⟩›
  unfolding shift_def FOL_Fitting.shift_def by simp

lemma semantics [iff]: ‹semantics e f g p ⟷ eval e f g (from_fm p)›
  by (induct p arbitrary: e) simp_all

abbreviation valid ("⪢ _" 0) where
  ‹(⪢ p) ≡ ∀(e :: _ ⇒ nat hterm) f g. semantics e f g p›

theorem complete_sound: ‹⪢ p ⟹ ⊩ [p]› ‹⊩ [q] ⟹ semantics e f g q›
  by (metis to_from_fm sim semantics list.map SC_completeness) (use sound in force)

corollary ‹(⪢ p) ⟷ (⊩ [p])›
  using complete_sound by fast

section ‹Reference›

text ‹Asta Halkjær From (2019): Sequent Calculus 🌐‹https://www.isa-afp.org/entries/FOL_Seq_Calc1.html››

end