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