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]: c p  new c (to_fm p)
  by (induct p) simp_all

lemma list_params [iff]: 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 = e0: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 SC_completeness) (use sound in force)

corollary ( p)  ( [p])
  using complete_sound by fast

section ‹Reference›

text ‹Asta Halkjær From (2019): Sequent Calculus 🌐‹›