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