Theory Syntax

theory Syntax
  imports Main "HOL-Library.Countable"
begin

section ‹Syntax: a deep embedding of HOL in HOL›

text ‹BKK's language of classical higher-order logic --- HOL, by which we mean
  Church's simple theory of types throughout (BKK Sections 2.1--2.2) --- in a @{emph ‹locally
  nameless›} representation: bound variables are de Bruijn indices, free variables
      and parameters carry their type.  BKK take alphabetic variants to be identical (BKK
  Section 2.1); locally nameless makes that literally true --- ‹α›-equivalent terms are
  @{emph ‹equal›}, so capture-avoiding substitution and the entire renaming theory disappear.
  As in BKK, non-logical constants are @{emph ‹parameters›} with names drawn from a type ‹'p›, and
  we include BKK's optional primitive equality ‹Eq σ› (BKK Section 2.1, Remark 7.9),
  alongside the always-expressible defined Leibniz equality (BKK Section 2.2).
  Beyond BKK's signature we deliberately carry a family of description operators ‹Iota σ› of
  type ‹(σ ❙⇒ 𝗈) ❙⇒ σ›, one for each type: BKK have no description operator (they decline to
  add one, BKK Section 2.3.1, pointing to Andrews 1972 for the semantic issues); we follow that
  reference instead and equip ‹Iota σ› with the description axiom for singletons --- the rule
  ‹NK(ι)› of the calculus and the corresponding model condition ‹gm_descB›.  Definitions
      and lemmas below that carry no BKK
  reference are locally-nameless infrastructure (opening, closing, freshness, renaming): they
  have no counterpart in the paper, where identification of alphabetic variants is handled
  informally (BKK Section 2.1).›

subsection ‹Types and terms›

datatype ty = Ind (‹ι›) | Bool (‹𝗈›) | Fun ty ty (infixr ‹❙⇒› 65)

datatype (pars: 'p) tm =
    Bnd nat  ― ‹bound variable (de Bruijn index)›
  | Fre nat ty  ― ‹free variable: a name and its type›
  | Par 'p ty                            ― ‹parameter (typed constant)›
  | Neg | Dis | Pi ty | Iota ty | Eq ty
      ― ‹logical constants ‹❙¬, ❙∨, ❙Π⇘_σ⇙, ❙ι⇘_σ⇙, ❙=⇘_σ⇙››
  | App "'p tm" "'p tm"  (infixl ‹❙⋅› 200)
  | Abs ty "'p tm"    ― ‹abstraction, domain type annotated (BKK's ‹λX⇘_σ⇙. A›; nameless, so no binder variable)›
  for map: prn ― ‹We call the map function for the parameter type @{term prn} for parameter renaming.›

text ‹BKK write disjunctions in infix and negations in prefix notation (BKK Section 2.2
  declares the convention of writing ‹((∨A)B)› as ‹A ∨ B›); we mirror this with
  input/output abbreviations for the applied connectives.›

text ‹Abstraction is written ‹❙Λ⇘_σ⇙ b› for BKK's ‹λX⇘_σ⇙. A› (bold ‹Λ›, since ‹λ›
  is reserved); being nameless, it displays the domain type but no binder variable.›

notation Abs (‹❙Λ⇘_⇙ _› [0, 200] 200)

text ‹Decorated atoms: a free variable ‹x› of type ‹σ› is written ‹x⇧^f⇘_σ⇙› (BKK's
  ‹X⇘_σ⇙›), a parameter ‹w› is written ‹w⇧^p⇘_σ⇙› (BKK's typed constants).›

notation Fre (‹_⇧^f⇘_⇙› [1000, 0] 1000)
notation Par (‹_⇧^p⇘_⇙› [1000, 0] 1000)

abbreviation NegA :: "'p tm ⇒ 'p tm"  (‹❙¬ _› [66] 66) where
  "❙¬ A ≡ Neg ❙⋅ A"
abbreviation DisA :: "'p tm ⇒ 'p tm ⇒ 'p tm"  (infixr ‹❙∨› 61) where
  "A ❙∨ B ≡ (Dis ❙⋅ A) ❙⋅ B"

text ‹Summary of the term notation and its BKK Section 2 counterparts: application
  ‹s ❙⋅ t› (BKK juxtaposition), abstraction ‹❙Λ⇘_σ⇙ b›, free variables ‹x⇧^f⇘_σ⇙› (BKK's
  ‹X⇘_σ⇙›), parameters ‹w⇧^p⇘_σ⇙› (typed constants), and the applied connectives ‹❙¬ A› and
  ‹A ❙∨ B›.  The defined layer adds ‹A ❙⊃ B›, ‹❙Π⇘_σ⇙ b›, Leibniz equality ‹A ❙≐⇘_α⇙ B› and applied
  primitive equality (below); opening is ‹b❙⟨u❙⟩› (below); on the semantic side, ‹⦇A⦈⇘_ξ⇙› is
  the denotation and ‹ξ(x⇘_σ⇙ := d)› the assignment update (Section 2).›

text ‹Types and terms (over a countable parameter type) are countable, so the language of
  sentences can be enumerated --- the basis for our countable rendering of BKK's
  transfinite extension construction (BKK Section 6, Lemma 6.32).›

instance ty :: countable by countable_datatype
instance tm :: (countable) countable by countable_datatype

subsection ‹Opening and free-variable substitution›

text ‹‹opn⇘_k⇙ u t› replaces the bound index ‹k› in ‹t› by ‹u›; ‹t❙⦇u❙⦈› opens the top binder.
  Because bound variables are indices, substituting for a free variable (‹fsub›) needs no
  renaming: it passes straight through ‹Abs›.›

primrec opn :: "nat ⇒ 'p tm ⇒ 'p tm ⇒ 'p tm" where
    "opn k u (Bnd i) = (if i = k then u else Bnd i)"
  | "opn k u (n⇧^f⇘σ⇙) = n⇧^f⇘σ⇙"
  | "opn k u (p⇧^p⇘σ⇙) = p⇧^p⇘σ⇙"
  | "opn k u Neg = Neg"
  | "opn k u Dis = Dis"
  | "opn k u (Pi σ) = Pi σ"
  | "opn k u (Iota τ) = Iota τ"
  | "opn k u (Eq τ) = Eq τ"
  | "opn k u (s ❙⋅ t) = (opn k u s) ❙⋅ (opn k u t)"
  | "opn k u (❙Λ⇘σ⇙ b) = ❙Λ⇘σ⇙ (opn (Suc k) u b)"

text ‹Opening the outermost binder is by far the most frequent operation, so it gets its
  own notation: ‹b❙⟨u❙⟩› is ‹b› with de Bruijn index ‹0› instantiated to ‹u› ---
  BKK's ‹[u/X]B› for the bound variable of the enclosing abstraction or quantifier.›

abbreviation opn0 (‹_❙⟨_❙⟩› [1000, 0] 1000) where "b❙⟨u❙⟩ ≡ opn 0 u b"

primrec fsub :: "nat ⇒ ty ⇒ 'p tm ⇒ 'p tm ⇒ 'p tm" where
    "fsub x σ u (Bnd i) = Bnd i"
  | "fsub x σ u (n⇧^f⇘τ⇙) = (if n = x ∧ τ = σ then u else n⇧^f⇘τ⇙)"
  | "fsub x σ u (p⇧^p⇘τ⇙) = p⇧^p⇘τ⇙"
  | "fsub x σ u Neg = Neg"
  | "fsub x σ u Dis = Dis"
  | "fsub x σ u (Pi τ) = Pi τ"
  | "fsub x σ u (Iota τ) = Iota τ"
  | "fsub x σ u (Eq τ) = Eq τ"
  | "fsub x σ u (s ❙⋅ t) = (fsub x σ u s) ❙⋅ (fsub x σ u t)"
  | "fsub x σ u (❙Λ⇘τ⇙ b) = ❙Λ⇘τ⇙ (fsub x σ u b)"

text ‹Substitution notation: ‹b❙[u❙/x⇘_σ⇙❙]› substitutes ‹u› for the free variable ‹x⇧^f⇘_σ⇙› in ‹b›.›

syntax "_fsub" :: "logic ⇒ logic ⇒ logic ⇒ logic ⇒ logic"  (‹_❙[_❙'/_⇘_⇙❙]› [1000, 0, 0, 0] 1000)
syntax_consts "_fsub" == "fsub"
translations "b❙[u❙/x⇘σ⇙❙]" ⇌ "CONST fsub x σ u b"

subsection ‹Free variables and parameters›

primrec fvs :: "'p tm ⇒ nat set" where
    "fvs (Bnd i) = {}"
  | "fvs (n⇧^f⇘σ⇙) = {n}"
  | "fvs (p⇧^p⇘σ⇙) = {}"
  | "fvs Neg = {}"  | "fvs Dis = {}"  | "fvs (Pi σ) = {}"
  | "fvs (Iota σ) = {}"  | "fvs (Eq σ) = {}"
  | "fvs (s ❙⋅ t) = fvs s ∪ fvs t"
  | "fvs (❙Λ⇘σ⇙ b) = fvs b"

lemma finite_fvs [simp]: "finite (fvs t)" by (induction t) auto
lemma finite_pars [simp]: "finite (pars t)" by (induction t) auto

text ‹Renaming parameters.  Eigen-parameters (BKK's ‹w⇘_α⇙›) must be chosen fresh; to weaken the
  context or extend a consistent set we move them out of the way with an injective renaming.›

lemma prn_opn: "prn ρ (opn k u t) = opn k (prn ρ u) (prn ρ t)" by (induction t arbitrary: k) auto
lemma pars_prn: "pars (prn ρ t) = ρ ` pars t" by (induction t) auto
lemma prn_prn: "prn f (prn g t) = prn (λp. f (g p)) t" by (induction t) auto
lemma prn_id [simp]: "prn (λp. p) t = t" by (induction t) auto
lemma prn_cong: "(⋀p. p ∈ pars t ⟹ ρ p = p) ⟹ prn ρ t = t" by (induction t) auto

text ‹The typed free occurrences --- the (name, type) pairs a term reads from an assignment.
  A name can occur at several types, so this is finer than @{const fvs}.›

primrec occ :: "'p tm ⇒ (nat × ty) set" where
    "occ (Bnd i) = {}"
  | "occ (n⇧^f⇘σ⇙) = {(n, σ)}"
  | "occ (p⇧^p⇘σ⇙) = {}"
  | "occ Neg = {}"  | "occ Dis = {}"  | "occ (Pi σ) = {}"
  | "occ (Iota σ) = {}"  | "occ (Eq σ) = {}"
  | "occ (s ❙⋅ t) = occ s ∪ occ t"
  | "occ (❙Λ⇘σ⇙ b) = occ b"

lemma fvs_eq_fst_occ: "fvs t = fst ` occ t" by (induction t) (auto simp: image_Un)
lemma occ_opn: "occ (opn k u t) ⊆ occ t ∪ occ u" by (induction t arbitrary: k) auto

subsection ‹A fresh free variable exists›

text ‹A deterministic fresh name for a finite set (used for the abstraction case of the
  denotation).›

definition fresh :: "nat set ⇒ nat" where "fresh S ≡ LEAST n. n ∉ S"

lemma fresh_notin: "finite S ⟹ fresh S ∉ S"
  by (metis LeastI ex_new_if_finite infinite_UNIV_nat fresh_def)

subsection ‹Basic laws of opening and substitution›

text ‹Free variables of a substitution.  (A name may occur at several types, so ‹x› is only
  removed under the safe over-approximation.)›

lemma fvs_fsub: "fvs (fsub x σ u t) ⊆ fvs t ∪ fvs u" by (induction t) auto
lemma fvs_opn: "fvs (opn k u t) ⊆ fvs t ∪ fvs u" by (induction t arbitrary: k) auto

text ‹Opening with a free variable preserves size --- the measure for the size-recursive
  denotation of an abstraction (its body is opened with a fresh variable of the same size).›

lemma size_opn_Fre [simp]: "size (opn k (x⇧^f⇘σ⇙) t) = size t" by (induction t arbitrary: k) auto

subsection ‹Local closure›

text ‹A term is @{emph ‹locally closed›} if every bound index is captured by an enclosing
  binder.  As is standard for the locally-nameless representation, the ‹Abs› rule uses a
  @{emph ‹cofinite›} quantifier: opening the body with a fresh free variable is locally closed.
  A locally closed term denotes exactly an ‹α›-equivalence class of BKK's named terms
  (BKK Section 2.1).›

inductive lc :: "'p tm ⇒ bool" where
    lc_Fre [intro]: "lc (n⇧^f⇘σ⇙)"
  | lc_Par [intro]: "lc (p⇧^p⇘σ⇙)"
  | lc_Neg [intro]: "lc Neg"
  | lc_Dis [intro]: "lc Dis"
  | lc_Pi  [intro]: "lc (Pi σ)"
  | lc_Iota [intro]: "lc (Iota σ)"
  | lc_Eq [intro]: "lc (Eq σ)"
  | lc_App [intro]: "lc s ⟹ lc t ⟹ lc (s ❙⋅ t)"
  | lc_Abs: "finite L ⟹ (⋀x. x ∉ L ⟹ lc (b❙⟨x⇧^f⇘σ⇙❙⟩)) ⟹ lc (❙Λ⇘σ⇙ b)"

text ‹If opening at ‹j› is already fixed by a later opening at ‹i ≠ j›, then opening
  at ‹i› alone was already the identity.›

lemma opn_core: "i ≠ j ⟹ opn j v t = opn i u (opn j v t) ⟹ opn i u t = t"
proof (induction t arbitrary: i j)
  case (Abs τ b)
  have "opn (Suc i) u b = b"
    by (metis Abs.IH opn.simps(10) Abs.prems(1) tm.inject(8) Abs.prems(2) old.nat.inject)
  thus ?case by simp
qed (auto split: if_splits)

text ‹A locally closed term ignores opening.›

lemma opn_lc [simp]: "lc t ⟹ opn k u t = t"
proof (induction arbitrary: k rule: lc.induct)
  case (lc_Abs L b σ)
  obtain x where x: "x ∉ L"
    using lc_Abs.hyps(1) by (meson ex_new_if_finite infinite_UNIV_nat)
  have IH: "opn (Suc k) u (b❙⟨x⇧^f⇘σ⇙❙⟩) = b❙⟨x⇧^f⇘σ⇙❙⟩" using lc_Abs.IH x by auto
  have "opn (Suc k) u b = b" by (metis opn_core IH nat.simps(3))
  thus ?case by simp
qed simp_all

text ‹‹fsub› commutes with opening when the substituted term is locally closed.›

lemma fsub_opn: "lc u ⟹ fsub x σ u (opn k v t) = opn k (fsub x σ u v) (fsub x σ u t)"
  by (induction t arbitrary: k) auto

text ‹Opening with ‹u› equals opening with a fresh free variable and then substituting ‹u› for it.›

lemma fsub_intro: "x ∉ fvs t ⟹ opn k u t = fsub x σ u (opn k (x⇧^f⇘σ⇙) t)"
  by (induction t arbitrary: k) auto

text ‹Openings at distinct indices commute (for locally closed fillers).›

lemma opn_opn_comm: "i ≠ j ⟹ lc u ⟹ lc v ⟹ opn i u (opn j v t) = opn j v (opn i u t)"
  by (induction t arbitrary: i j) auto

subsection ‹Typing: well-formed formulae›

text ‹‹wff⇘_σ⇙(t)› is BKK's ‹t ∈ wff⇘_σ⇙(Σ)› (BKK Section 2.1): ‹t› is a well-formed formula of
  type ‹σ›.  The ‹Abs› rule uses the cofinite quantifier, so a well-formed formula is in
  particular locally closed.›

inductive wff :: "ty ⇒ 'p tm ⇒ bool"  (‹wff⇘_⇙'(_')› [0,0] 1000) where
    wff_Fre: "wff⇘σ⇙(n⇧^f⇘σ⇙)"
  | wff_Par: "wff⇘σ⇙(p⇧^p⇘σ⇙)"
  | wff_Neg: "wff⇘𝗈❙⇒𝗈⇙(Neg)"
  | wff_Dis: "wff⇘𝗈❙⇒𝗈❙⇒𝗈⇙(Dis)"
  | wff_Pi:  "wff⇘(σ❙⇒𝗈)❙⇒𝗈⇙(Pi σ)"
  | wff_Iota: "wff⇘(σ❙⇒𝗈)❙⇒σ⇙(Iota σ)"
  | wff_Eq: "wff⇘σ❙⇒σ❙⇒𝗈⇙(Eq σ)"
  | wff_App: "wff⇘σ❙⇒τ⇙(s) ⟹ wff⇘σ⇙(t) ⟹ wff⇘τ⇙(s ❙⋅ t)"
  | wff_Abs: "finite L ⟹ (⋀x. x ∉ L ⟹ wff⇘τ⇙(b❙⟨x⇧^f⇘σ⇙❙⟩)) ⟹ wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ b)"

lemma wff_lc: "wff⇘σ⇙(t) ⟹ lc t" by (induction rule: wff.induct) (auto intro: lc_Abs)

inductive_cases wff_FreE [elim!]: "wff⇘τ⇙(n⇧^f⇘σ⇙)"
inductive_cases wff_ParE [elim!]: "wff⇘τ⇙(p⇧^p⇘σ⇙)"
inductive_cases wff_NegE [elim!]: "wff⇘τ⇙(Neg)"
inductive_cases wff_DisE [elim!]: "wff⇘τ⇙(Dis)"
inductive_cases wff_PiE  [elim!]: "wff⇘τ⇙(Pi σ)"
inductive_cases wff_IotaE [elim!]: "wff⇘τ⇙(Iota σ)"
inductive_cases wff_EqE [elim!]: "wff⇘τ⇙(Eq σ)"
inductive_cases wff_AppE [elim]: "wff⇘τ⇙(s ❙⋅ t)"
inductive_cases wff_AbsE [elim]: "wff⇘τ⇙(❙Λ⇘σ⇙ b)"

text ‹Types are unique.›

lemma wff_unique: "wff⇘σ⇙(t) ⟹ wff⇘τ⇙(t) ⟹ σ = τ"
proof (induction σ t arbitrary: τ rule: wff.induct)
  case (wff_Abs L ρ b σ)
  from wff_Abs.prems obtain L' ρ' where t: "τ = σ ❙⇒ ρ'"
      and fL': "finite L'" and hb: "⋀x. x ∉ L' ⟹ wff⇘ρ'⇙(b❙⟨x⇧^f⇘σ⇙❙⟩)" 
    by auto
  obtain x where x: "x ∉ L ∪ L'" using wff_Abs(1) fL'
    by (meson ex_new_if_finite finite_UnI infinite_UNIV_nat)
  have "ρ = ρ'" using wff_Abs.IH hb x by auto
  thus ?case using t by simp
qed (fast)+

text ‹Well-typedness is preserved when a free variable is replaced by a term of the same
  type (BKK Section 2.1: substitution respects the typing; the paper leaves this implicit).›

lemma wff_fsub: "wff⇘τ⇙(t) ⟹ wff⇘ρ⇙(u) ⟹ wff⇘τ⇙(fsub x ρ u t)"
proof (induction τ t rule: wff.induct)
  case (wff_Abs L τ b σ) 
  have lcu: "lc u" using wff_Abs.prems by (rule wff_lc)
  have "wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ (fsub x ρ u b))"
    by (metis finite_insert fsub.simps(2) fsub_opn insert_iff lcu wff.wff_Abs 
              wff_Abs.IH wff_Abs.hyps(1) wff_Abs.prems)
  thus ?case by simp
qed (auto intro: wff.intros simp: wff.wff_Fre)

text ‹Consequently an abstraction may be opened with @{emph ‹any›} fresh free variable and
  stays well-typed --- the locally-nameless counterpart of BKK's ‹α›-invariance (BKK Section 2.1).›

lemma wff_Abs_open: assumes w: "wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ b)" and x: "x ∉ fvs b"
  shows "wff⇘τ⇙(b❙⟨x⇧^f⇘σ⇙❙⟩)"
proof -
  from w obtain L τ' where Lτ': "finite L" "τ = τ'" "⋀y. y ∉ L ⟹ wff⇘τ'⇙(b❙⟨y⇧^f⇘σ⇙❙⟩)" by auto
  obtain y where y: "y ∉ L ∪ fvs b"
    using Lτ'(1) by (meson ex_new_if_finite finite_UnI finite_fvs infinite_UNIV_nat)
  have "b❙⟨x⇧^f⇘σ⇙❙⟩ = fsub y σ (x⇧^f⇘σ⇙) (b❙⟨y⇧^f⇘σ⇙❙⟩)" using y
    by (intro fsub_intro) auto
  moreover have "wff⇘τ'⇙(fsub y σ (x⇧^f⇘σ⇙) (b❙⟨y⇧^f⇘σ⇙❙⟩))" using Lτ'(3) y wff_Fre
    by (auto intro: wff_fsub)
  ultimately show ?thesis using Lτ'(2) by simp
qed

text ‹Opening a well-typed abstraction with a well-typed argument stays well-typed --- the
  typing counterpart of ‹β›-reduction (implicit in BKK Section 2.1; the semantic analogue is BKK
      Lemma 3.20).›

lemma wff_opn: "wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ b) ⟹ wff⇘σ⇙(a) ⟹ wff⇘τ⇙(b❙⟨a❙⟩)" 
  by (metis finite_fvs fresh_notin fsub_intro wff_Abs_open wff_fsub)

text ‹Parameter renaming leaves the typing unchanged (there is no BKK counterpart: parameter
  renaming is part of the locally-nameless infrastructure).›

lemma wff_prn[intro!]: "wff⇘σ⇙(t) ⟹ wff⇘σ⇙(prn ρ t)"
proof (induction σ t rule: wff.induct)
  case wff_Abs thus ?case by (metis (mono_tags, lifting) prn_opn tm.simps(120,128) wff.wff_Abs)
qed (auto intro: wff.intros)

subsection ‹Turning one parameter into a free variable›

text ‹‹pvar w σ x t› replaces every occurrence of the parameter ‹w› at type ‹σ› by the free
  variable ‹x›.  This realizes the evaluation variant of BKK's proof of Theorem 7.3 (case
  ‹NK(ΠI)›): from an evaluation ‹ℰ› ``one can define another evaluation function ‹ℰ'› such
  that ‹ℰ'(w) ≡ a› and ‹ℰ'(A) ≡ ℰ(A)› if ‹w› does not occur in ‹A›''.›

primrec pvar :: "'p ⇒ ty ⇒ nat ⇒ 'p tm ⇒ 'p tm" where
    "pvar w σ x (Bnd i) = Bnd i"
  | "pvar w σ x (n⇧^f⇘τ⇙) = n⇧^f⇘τ⇙"
  | "pvar w σ x (p⇧^p⇘τ⇙) = (if p = w ∧ τ = σ then x⇧^f⇘σ⇙ else p⇧^p⇘τ⇙)"
  | "pvar w σ x Neg = Neg"
  | "pvar w σ x Dis = Dis"
  | "pvar w σ x (Pi τ) = Pi τ"
  | "pvar w σ x (Iota τ) = Iota τ"
  | "pvar w σ x (Eq τ) = Eq τ"
  | "pvar w σ x (s ❙⋅ t) = (pvar w σ x s) ❙⋅ (pvar w σ x t)"
  | "pvar w σ x (❙Λ⇘τ⇙ b) = ❙Λ⇘τ⇙ (pvar w σ x b)"

lemma pvar_opn: "pvar w σ x (opn k u t) = opn k (pvar w σ x u) (pvar w σ x t)"
  by (induction t arbitrary: k) auto
lemma pvar_id [simp]: "w ∉ pars t ⟹ pvar w σ x t = t"
  by (induction t) auto
lemma wff_pvar: "wff⇘τ⇙(t) ⟹ wff⇘τ⇙(pvar w σ x t)"
proof (induction τ t rule: wff.induct)
  case wff_Abs thus ?case by (metis pvar.simps(10,2) pvar_opn wff.wff_Abs)
qed (auto intro: wff.intros)

subsection ‹‹β›-conversion (BKK Section 2)›

text ‹BKK's ‹β›-equality ‹≡⇩_β› (BKK Section 2.1): the congruence closure of the ‹β›-redex
  ‹(λx. b) a → b[a/x]›.  In the locally-nameless
  presentation the redex reduces to ‹b❙⟨a❙⟩›, and the rule under an abstraction is stated
  cofinitely, as for typing and local closure.›

text ‹The relation is @{emph ‹type-indexed›}: ‹s ≈⇘_ρ⇙ t› holds only for well-formed terms of type
  ‹ρ›.  Carrying the type keeps the symmetric/transitive rules type-preserving (a ‹β›-expansion
  does not otherwise determine the argument's type), which is exactly what the soundness proof of
  ‹NK(β)› needs.›

inductive beq :: "'p tm ⇒ ty ⇒ 'p tm ⇒ bool"  (‹_ ≈⇘_⇙ _› [51, 0, 51] 50) where
    beta:  "wff⇘σ❙⇒ρ⇙(❙Λ⇘σ⇙ b) ⟹ wff⇘σ⇙(a) ⟹ (❙Λ⇘σ⇙ b) ❙⋅ a ≈⇘ρ⇙ b❙⟨a❙⟩"
  | refl:  "wff⇘ρ⇙(t) ⟹ t ≈⇘ρ⇙ t"
  | sym:   "s ≈⇘ρ⇙ t ⟹ t ≈⇘ρ⇙ s"
  | trans: "r ≈⇘ρ⇙ s ⟹ s ≈⇘ρ⇙ t ⟹ r ≈⇘ρ⇙ t"
  | appL:  "s ≈⇘σ❙⇒ρ⇙ s' ⟹ wff⇘σ⇙(t) ⟹ s ❙⋅ t ≈⇘ρ⇙ s' ❙⋅ t"
  | appR:  "t ≈⇘σ⇙ t' ⟹ wff⇘σ❙⇒ρ⇙(s) ⟹ s ❙⋅ t ≈⇘ρ⇙ s ❙⋅ t'"
  | abs:   "finite L ⟹ (⋀x. x ∉ L ⟹ b❙⟨x⇧^f⇘σ⇙❙⟩ ≈⇘τ⇙ b'❙⟨x⇧^f⇘σ⇙❙⟩)
              ⟹ ❙Λ⇘σ⇙ b ≈⇘σ❙⇒τ⇙ ❙Λ⇘σ⇙ b'"

text ‹‹β›-conversion relates well-formed terms of the stated type.›

lemma beq_wff: "s ≈⇘ρ⇙ t ⟹ wff⇘ρ⇙(s) ∧ wff⇘ρ⇙(t)"
proof (induction rule: beq.induct)
  case beta thus ?case by (auto intro: wff_App wff_opn)
next
  case abs thus ?case by (metis wff_Abs)
qed (auto intro: wff_App)

lemma beq_wffL: "s ≈⇘ρ⇙ t ⟹ wff⇘ρ⇙(s)" and beq_wffR: "s ≈⇘ρ⇙ t ⟹ wff⇘ρ⇙(t)"
  using beq_wff by blast+

text ‹‹β›-conversion is stable under parameter renaming.›

lemma beq_rename[intro!]: "s ≈⇘τ⇙ t ⟹ prn π s ≈⇘τ⇙ prn π t"
proof (induction rule: beq.induct)
  case beta thus ?case by simp (metis beq.beta prn_opn tm.simps(128) wff_prn)
next case refl thus ?case using beq.refl wff_prn by blast
next case sym thus ?case using beq.sym by blast
next case trans thus ?case using beq.trans by blast
next case appL thus ?case using beq.appL by force
next case appR thus ?case using beq.appR by force
next case abs thus ?case by (metis (mono_tags, lifting) beq.abs prn_opn tm.simps(120,128))
qed


subsection ‹The defined logical layer (BKK Section 2.2)›

text ‹Following BKK (BKK Section 2.2), everything beyond the primitive constants of the
  signature --- ‹❙¬›, ‹❙∨›, ‹Pi⇘_σ⇙›, the primitive equality ‹Eq σ› and the description
  operators ‹Iota σ› (above) --- is defined.
  The universal quantifier is BKK's shorthand ‹❙∀X⇘_σ⇙. A ≡ ❙Π⇘_σ⇙(λX⇘_σ⇙. A)› and implication
  their ‹A ❙⊃ B ≡ (❙¬A) ❙∨ B›.  For falsity we deviate mildly from BKK, who use
  ‹F⇘_𝗈⇙ ≡ ❙¬❙∀P⇘_𝗈⇙. P ❙∨ ❙¬P› (BKK Lemma 3.43, footnote 11): our ‹❙⊥› is ‹❙∀X⇘_𝗈⇙. X› and ‹❙⊤ ≡ ❙¬❙⊥›.
  The two choices are interderivable in ‹NK⇩_β› (cf.\ BKK Remark 7.2) and both falsa are
  unsatisfied in every ‹Σ›-model, so every use below is invariant under the exchange.
  Leibniz equality --- always expressible, alongside the primitive ‹Eq α› of the signature ---
  is BKK's Leibniz combinator ‹Q⇘_α⇙ ≡ λX⇘_α⇙ Y⇘_α⇙. ❙∀P⇘_α❙⇒𝗈⇙. P X ❙⊃ P Y› (BKK Section 2.2,
  the Leibniz formula for equality).  Because bound variables are de Bruijn indices, ‹Leib α› is
  a genuinely @{emph ‹closed›} term: BKK's reserved bound names ‹X, Y, P› are simply the indices
  ‹2, 1, 0›.›


definition Forall :: "ty ⇒ 'p tm ⇒ 'p tm"  (‹❙Π⇘_⇙ _› [0, 200] 200) where 
  "❙Π⇘σ⇙ b = (Pi σ) ❙⋅ (❙Λ⇘σ⇙ b)"
definition FalseB :: "'p tm"  (‹❙⊥›) where "❙⊥ = ❙Π⇘𝗈⇙ (Bnd 0)"
definition TrueB :: "'p tm"  (‹❙⊤›) where "❙⊤ = ❙¬ ❙⊥"
definition ImpB :: "'p tm ⇒ 'p tm ⇒ 'p tm"  (infixr ‹❙⊃› 60) where
  "φ ❙⊃ ψ = (❙¬ φ) ❙∨ ψ"
definition Leib :: "ty ⇒ 'p tm" where
  "Leib α = ❙Λ⇘α⇙ (Abs α (❙Π⇘α❙⇒𝗈⇙ ((Bnd 0) ❙⋅ (Bnd 2) ❙⊃ (Bnd 0) ❙⋅ (Bnd 1))))"
abbreviation LeibA :: "'p tm ⇒ ty ⇒ 'p tm ⇒ 'p tm"  (‹_ ❙≐⇘_⇙ _› [66,0,66] 65) where
  "A ❙≐⇘α⇙ B ≡ ((Leib α) ❙⋅ A) ❙⋅ B"

text ‹Primitive equality applied (BKK's optional ‹=⇩_α ∈ Σ⇘_{α→α→𝗈}⇙›, BKK Remark 7.9).›

abbreviation PEqA :: "'p tm ⇒ ty ⇒ 'p tm ⇒ 'p tm"  (‹_ ❙=⇘_⇙ _› [66,0,66] 65) where
  "A ❙=⇘α⇙ B ≡ ((Eq α) ❙⋅ A) ❙⋅ B"
lemma wff_PEq [intro]: "wff⇘α⇙(A) ⟹ wff⇘α⇙(B) ⟹ wff⇘𝗈⇙(A ❙=⇘α⇙ B)"
  by (rule wff_App[OF wff_App[OF wff_Eq]])

subsection ‹Opening distributes over the defined layer›

lemma opn_Forall [simp]: "opn k u (❙Π⇘σ⇙ b) = ❙Π⇘σ⇙ (opn (Suc k) u b)"
  by (simp add: Forall_def)
lemma opn_ImpB [simp]: "opn k u (φ ❙⊃ ψ) = (opn k u φ) ❙⊃ (opn k u ψ)"
  by (simp add: ImpB_def)
lemma opn_FalseB [simp]: "opn k u (❙⊥ :: 'p tm) = ❙⊥"
  by (simp add: FalseB_def)
lemma opn_Leib [simp]: "opn k u (Leib α :: 'p tm) = Leib α"
  by (simp add: Leib_def)

subsection ‹A convenient abstraction-typing rule›

text ‹For the closed defined terms, opening the body with @{emph ‹any›} free variable is
  well-typed, so the cofinite side-condition collapses to a universal one.›

lemma wff_AbsI: "(⋀x. wff⇘τ⇙(b❙⟨x⇧^f⇘σ⇙❙⟩)) ⟹ wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ b)"
  by (rule wff_Abs[of "{}"]) auto

subsection ‹Typing of the defined layer›

lemma wff_Forall [intro]: "(⋀x. wff⇘𝗈⇙(b❙⟨x⇧^f⇘σ⇙❙⟩)) ⟹ wff⇘𝗈⇙(❙Π⇘σ⇙ b)"
  by (metis Forall_def wff_AbsI wff_App wff_Pi)
lemma wff_Not [intro]: "wff⇘𝗈⇙(φ) ⟹ wff⇘𝗈⇙(❙¬ φ)"
  by (rule wff_App[OF wff_Neg])
lemma wff_Or [intro]: "wff⇘𝗈⇙(φ) ⟹ wff⇘𝗈⇙(ψ) ⟹ wff⇘𝗈⇙(φ ❙∨ ψ)"
  by (rule wff_App[OF wff_App[OF wff_Dis]])
lemma wff_ImpB [intro]: "wff⇘𝗈⇙(φ) ⟹ wff⇘𝗈⇙(ψ) ⟹ wff⇘𝗈⇙(φ ❙⊃ ψ)"
  by (metis ImpB_def wff_Not wff_Or)
lemma wff_FalseB [intro, simp]: "wff⇘𝗈⇙(❙⊥)" unfolding FalseB_def
  by (rule wff_Forall) (simp add: wff_Fre)
lemma wff_TrueB [intro, simp]: "wff⇘𝗈⇙(❙⊤)" unfolding TrueB_def
  by (rule wff_Not[OF wff_FalseB])
lemma wff_App_FreFre [intro]: "wff⇘𝗈⇙((p⇧^f⇘σ ❙⇒ 𝗈⇙) ❙⋅ (x⇧^f⇘σ⇙))"
  by (rule wff_App[OF wff_Fre wff_Fre])
lemma wff_Leib [intro, simp]: "wff⇘α❙⇒α❙⇒𝗈⇙(Leib α)"
  by (auto simp: Leib_def del: wff_Forall wff_ImpB wff_App_FreFre
           intro!: wff_AbsI wff_Forall wff_ImpB wff_App_FreFre)
lemma wff_LeibE [intro]: "wff⇘α⇙(A) ⟹ wff⇘α⇙(B) ⟹ wff⇘𝗈⇙(A ❙≐⇘α⇙ B)"
  by (rule wff_App[OF wff_App[OF wff_Leib]])

subsection ‹Free variables and local closure of the defined layer›

lemma fvs_defs [simp]: "fvs (❙Π⇘σ⇙ b) = fvs b" "fvs (❙⊥ :: 'p tm) = {}" "fvs (❙⊤ :: 'p tm) = {}"
  "fvs (φ ❙⊃ ψ) = fvs φ ∪ fvs ψ" "fvs (Leib α :: 'p tm) = {}"
  by (simp_all add: Forall_def FalseB_def TrueB_def ImpB_def Leib_def)

lemma pars_defs [simp]: "pars (❙Π⇘σ⇙ b) = pars b" "pars (❙⊥ :: 'p tm) = {}"
  "pars (❙⊤ :: 'p tm) = {}" "pars (φ ❙⊃ ψ) = pars φ ∪ pars ψ" "pars (Leib α :: 'p tm) = {}"
  by (simp_all add: Forall_def FalseB_def TrueB_def ImpB_def Leib_def)

subsection ‹Parameter renaming distributes over the defined layer›

lemma prn_Forall [simp]: "prn ρ (❙Π⇘σ⇙ b) = ❙Π⇘σ⇙ (prn ρ b)"
  by (simp add: Forall_def)
lemma prn_ImpB [simp]: "prn ρ (φ ❙⊃ ψ) = (prn ρ φ) ❙⊃ (prn ρ ψ)"
  by (simp add: ImpB_def)
lemma prn_FalseB [simp]: "prn ρ (❙⊥ :: 'p tm) = ❙⊥"
  by (simp add: FalseB_def)
lemma prn_Leib [simp]: "prn ρ (Leib α :: 'p tm) = Leib α"
  by (simp add: Leib_def)

subsection ‹The defined existential quantifier›

abbreviation ExistsB :: "ty ⇒ 'p tm ⇒ 'p tm"  (‹❙∃⇘_⇙ _› [0, 200] 200) where
  "❙∃⇘σ⇙ b ≡ ❙¬ (❙Π⇘σ⇙ (❙¬ b))"

subsection ‹Named binders for the defined quantifiers›

text ‹Named-binder input syntax for the defined quantifiers: ‹clos k x σ t› abstracts the
  free variable ‹x⇧^f⇘_σ⇙› to the de Bruijn index ‹k› (the converse of ‹opn›), so that
  ‹❙∃x⇘_σ⇙. φ› and ‹❙Πx⇘_σ⇙. φ› bind an ordinary named variable; the locally-nameless
  representation is recovered by computation (the ‹_eq› lemmas below).›

primrec clos :: "nat ⇒ nat ⇒ ty ⇒ 'p tm ⇒ 'p tm" where
  "clos k x σ (Bnd i) = Bnd i"
| "clos k x σ (n⇧^f⇘τ⇙) = (if n = x ∧ τ = σ then Bnd k else n⇧^f⇘τ⇙)"
| "clos k x σ (p⇧^p⇘τ⇙) = p⇧^p⇘τ⇙"
| "clos k x σ Neg = Neg"
| "clos k x σ Dis = Dis"
| "clos k x σ (Pi τ) = Pi τ"
| "clos k x σ (Iota τ) = Iota τ"
| "clos k x σ (Eq τ) = Eq τ"
| "clos k x σ (s ❙⋅ t) = (clos k x σ s) ❙⋅ (clos k x σ t)"
| "clos k x σ (❙Λ⇘τ⇙ b) = ❙Λ⇘τ⇙ (clos (Suc k) x σ b)"

lemma clos_Forall [simp]: "clos k x σ (❙Π⇘τ⇙ b) = ❙Π⇘τ⇙ (clos (Suc k) x σ b)"
  by (simp add: Forall_def)
lemma clos_ImpB [simp]: "clos k x σ (φ ❙⊃ ψ) = (clos k x σ φ) ❙⊃ (clos k x σ ψ)"
  by (simp add: ImpB_def)
lemma clos_Leib [simp]: "clos k x σ (Leib α :: 'p tm) = Leib α"
  by (simp add: Leib_def)
definition ExN :: "nat ⇒ ty ⇒ 'p tm ⇒ 'p tm"  (‹❙∃_⇘_⇙. _› [1000, 0, 61] 61) where
  "❙∃x⇘σ⇙. b = ❙∃⇘σ⇙ (clos 0 x σ b)"
definition AllN :: "nat ⇒ ty ⇒ 'p tm ⇒ 'p tm"  (‹❙Π_⇘_⇙. _› [1000, 0, 61] 61) where
  "❙Πx⇘σ⇙. b = ❙Π⇘σ⇙ (clos 0 x σ b)"
definition LamN :: "nat ⇒ ty ⇒ 'p tm ⇒ 'p tm"  (‹❙Λ_⇘_⇙. _› [1000, 0, 61] 61) where
  "❙Λx⇘σ⇙. b = ❙Λ⇘σ⇙ (clos 0 x σ b)"

text ‹Fixed variable names for readable named-binder statements: the script letters
  ‹𝒢, ℱ, 𝒳, ℐ, ℋ› name the (numeric) free variables ‹0, …, 4›.›

definition 𝒢 :: nat where "𝒢 = 0"
definition ℱ :: nat where "ℱ = 1"
definition 𝒳 :: nat where "𝒳 = 2"
definition ℐ :: nat where "ℐ = 3"
definition ℋ :: nat where "ℋ = 4"

text‹Stronger size-based induction.›

lemma size_induct[case_names Bnd Fre Par Neg Dis Pi Iota Eq App Abs]:
  assumes ‹⋀x. P (Bnd x)›
      and ‹⋀x α. P x⇧^f⇘α⇙›
      and ‹⋀x α. P x⇧^p⇘α⇙›
      and ‹P Neg›
      and ‹P Dis›
      and ‹⋀α. P (Pi α)›
      and ‹⋀α. P (Iota α)›
      and ‹⋀α. P (Eq α)›
      and ‹⋀A B. (⋀C. size C ≤ size A ⟹ P C) ⟹ (⋀C. size C ≤ size B ⟹ P C) ⟹ P (A ❙⋅ B)›
      and ‹⋀α A. (⋀C. size C ≤ size A ⟹ P C) ⟹ P (❙Λ⇘α⇙ A)›
    shows ‹P x›
using assms proof (induct x rule: measure_induct_rule[where f = size])
  case (less x) thus ?case by (induct x; auto)
qed

end