Theory Syntax

section ‹Syntax›

theory Syntax imports List_Syntax begin

subsection ‹Terms and Formulas›

datatype tm
  = Var nat (#)
  | Fun nat tm list ()

datatype fm
  = Falsity ()
  | Pre nat tm list ()
  | Imp fm fm (infixr  55)
  | Uni fm ()

type_synonym sequent = fm list × fm list

subsubsection ‹Substitution›

primrec add_env :: 'a  (nat  'a)  nat  'a (infix  0) where
  (t  s) 0 = t
| (t  s) (Suc n) = s n

primrec lift_tm :: tm  tm where
  lift_tm (#n) = #(n+1)
| lift_tm (f ts) = f (map lift_tm ts)

primrec sub_tm :: (nat  tm)  tm  tm where
  sub_tm s (#n) = s n
| sub_tm s (f ts) = f (map (sub_tm s) ts)

primrec sub_fm :: (nat  tm)  fm  fm where
  sub_fm _  = 
| sub_fm s (P ts) = P (map (sub_tm s) ts)
| sub_fm s (p  q) = sub_fm s p  sub_fm s q
| sub_fm s (p) = (sub_fm (#0  λn. lift_tm (s n)) p)

abbreviation inst_single :: tm  fm  fm (_) where
  t  sub_fm (t  #)

subsubsection ‹Variables›

primrec vars_tm :: tm  nat list where
  vars_tm (#n) = [n]
| vars_tm (_ ts) = concat (map vars_tm ts)

primrec vars_fm :: fm  nat list where
  vars_fm  = []
| vars_fm (_ ts) = concat (map vars_tm ts)
| vars_fm (p  q) = vars_fm p @ vars_fm q
| vars_fm (p) = vars_fm p

primrec max_list :: nat list  nat where
  max_list [] = 0
| max_list (x # xs) = max x (max_list xs)

lemma max_list_append: max_list (xs @ ys) = max (max_list xs) (max_list ys)
  by (induct xs) auto

lemma max_list_concat: xs [∈] xss  max_list xs  max_list (concat xss)
  by (induct xss) (auto simp: max_list_append)

lemma max_list_in: max_list xs < n  n [∉] xs
  by (induct xs) auto

definition vars_fms :: fm list  nat list where
  vars_fms A  concat (map vars_fm A)

lemma vars_fms_member: p [∈] A  vars_fm p [⊆] vars_fms A
  unfolding vars_fms_def by (induct A) auto

lemma max_list_mono: A [⊆] B  max_list A  max_list B
  by (induct A) (simp, metis linorder_not_le list.set_intros(1) max.absorb2 max.absorb3
      max_list.simps(2) max_list_in set_subset_Cons subset_code(1))

lemma max_list_vars_fms:
  assumes max_list (vars_fms A)  n p [∈] A
  shows max_list (vars_fm p)  n
  using assms max_list_mono vars_fms_member by (meson dual_order.trans)

definition fresh :: fm list  nat where
  fresh A  Suc (max_list (vars_fms A))

subsection ‹Rules›

datatype rule =
  Idle | Axiom nat tm list | FlsL | FlsR | ImpL fm fm | ImpR fm fm | UniL tm fm | UniR fm

end