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›}.  Binders bind indices and substitution replaces only free names, so
  capture cannot arise for locally closed substituends, the only ones used: explicit
  ‹α›-conversion and bound-variable renaming disappear, while substitution itself
  (opening, ‹fsub›, ‹msub›) of course remains.
  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 also carry a description operator ‹Iota σ› of type
  ‹(σ ⇒ 𝗈) ⇒ σ›, one for each type ‹σ›.  BKK themselves have no description operator:
  they decline to add one (BKK Section 2.3.1) and point to Andrews 1972 for the semantic
  issues.  We follow that reference.  ‹Iota σ› comes with the description axiom for
  singletons: the rule ‹NK(ι)› of the calculus and the model condition ‹gm_descB›, both
  schematic in the type ‹σ›.  (The ‹ι› in the rule's name is Andrews' symbol for
  description, not the type ‹ι› of individuals.)  Definitions and lemmas below that carry
  no BKK reference are infrastructure of the formalisation: opening, closing, freshness,
  parameter renaming, countability.  They have no counterpart in the paper, where the
  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.›

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 ‹Abstraction is written ‹Λσ b›; it corresponds to BKK's ‹λXσ. A›.  The symbol is a
  bold ‹Λ› because ‹λ› already denotes Isabelle's own abstraction.  The notation is
  nameless: it shows the domain type ‹σ› but no binder variable --- the body ‹b› refers to
  the abstracted position by the de Bruijn index ‹Bnd 0›.›

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

text ‹Decorated atoms: a free variable ‹x› of type ‹σ› is written ‹xfσ› (BKK's
  ‹Xσ›), a parameter ‹w› is written ‹wpσ› (BKK's typed constants).›

notation Fre (‹_f⇘_⇙› [1000, 0] 1000)
notation Par (‹_p⇘_⇙› [1000, 0] 1000)

text ‹The term notation and its BKK Section 2 counterparts: free variables ‹xfσ› are BKK's
  ‹Xσ›, application ‹s ⋅ t› is juxtaposition, and parameters ‹wpσ› are typed constants.
  The defined layer below adds ‹A ⊃ B›, ‹Πσ b›, Leibniz equality ‹A ≐α B› and applied
  primitive equality; opening is ‹b⟨u⟩›; on the semantic side ‹⦇A⦈ξ› is the denotation
  and ‹ξ(xσ := d)› the assignment update.›

text ‹Types and terms (over a countable parameter type) are countable.  These instances feed
  the countable-signature corollaries of the completeness development --- countable term-model
  domains, and the collapse of parameter-richness to purity; the extension construction itself
  (BKK Section 6, Lemma 6.32) walks a well-order of the term type and needs no countability.›

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

subsection ‹Opening and free-variable substitution›

text ‹‹opnk u t› replaces the bound index ‹k› in ‹t› by ‹u›.›

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 (nf⇘σ⇙) = nf⇘σ⇙"
  | "opn k u (pp⇘σ⇙) = pp⇘σ⇙"
  | "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"

text ‹Because bound variables are indices, substituting for a free variable (‹fsub›) needs no
  renaming: it passes straight through ‹Abs›.›

primrec fsub :: "nat ⇒ ty ⇒ 'p tm ⇒ 'p tm ⇒ 'p tm" where
    "fsub x σ u (Bnd i) = Bnd i"
  | "fsub x σ u (nf⇘τ⇙) = (if n = x ∧ τ = σ then u else nf⇘τ⇙)"
  | "fsub x σ u (pp⇘τ⇙) = pp⇘τ⇙"
  | "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)"

subsection ‹Free variables and parameters›

primrec fvs :: "'p tm ⇒ nat set" where
    "fvs (Bnd i) = {}"
  | "fvs (nf⇘σ⇙) = {n}"
  | "fvs (pp⇘σ⇙) = {}"
  | "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. We
  use the map function introduced by the datatype, term‹prn›, for the renaming and prove some
  lemmas about it.›

lemma prn_opn: "prn ρ (opn k u t) = opn k (prn ρ u) (prn ρ t)"
  by (induction t arbitrary: k) auto
text ‹The next lemma, ‹pars_prn›, keeps its statement from the initial release of this
  entry (August 2026) (compatibility export).›

lemma pars_prn: "pars (prn ρ t) = ρ ` pars t" by (simp add: tm.set_map)
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 (nf⇘σ⇙) = {(n, σ)}"
  | "occ (pp⇘σ⇙) = {}"
  | "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
lemma prn_occ [simp]: "occ (prn f t) = occ t" by (induction t) auto

subsection ‹A fresh free variable exists›

text ‹A deterministic fresh name for a finite set, used wherever a concrete fresh name is
  needed: in the abstraction case of the denotation and in several proofs.›

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: an over-approximation, since the name ‹x› may still
  occur at another type.›

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 term‹size›.›

lemma size_opn_Fre [simp]: "size (opn k (xf⇘σ⇙) 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 corresponds to an ‹α›-equivalence class of raw named terms
  (BKK Section 2.1); well-formedness is imposed separately below.›

inductive lc :: "'p tm ⇒ bool" where
    lc_Fre [intro]: "lc (nf⇘σ⇙)"
  | lc_Par [intro]: "lc (pp⇘σ⇙)"
  | 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⟨xf⇘σ⇙⟩)) ⟹ lc (Λ⇘σ⇙ b)"

text ‹The abstraction case of the next lemma: if the body opened at ‹j› is left unchanged
  by opening at ‹i ≠ j›, then the body itself is left unchanged by opening at ‹i›.›

lemma opn_core: "i ≠ j ⟹ opn j v t = opn i u (opn j v t) ⟹ opn i u t = t"
  by (induct t arbitrary: i j; auto split: if_splits) (metis nat.inject)

text ‹A locally closed term ignores opening.›

lemma opn_lc [simp]: "lc t ⟹ opn k u t = t"
  by (induct arbitrary: k rule: lc.induct; simp)
     (metis opn_core fresh_notin nat.distinct(1))

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 (xf⇘σ⇙) 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⇘σ⇙(nf⇘σ⇙)"
  | wff_Par: "wff⇘σ⇙(pp⇘σ⇙)"
  | 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⟨xf⇘σ⇙⟩)) ⟹ wff⇘σ⇒τ⇙(Λ⇘σ⇙ b)"

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

inductive_cases wff_FreE [elim!]: "wff⇘τ⇙(nf⇘σ⇙)"
inductive_cases wff_ParE [elim!]: "wff⇘τ⇙(pp⇘σ⇙)"
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 σ)
  then obtain L' ρ' where t: "τ = σ ⇒ ρ'"
      and fL': "finite L'" and hb: "⋀x. x ∉ L' ⟹ wff⇘ρ'⇙(b⟨xf⇘σ⇙⟩)" 
    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⟨xf⇘σ⇙⟩)"
proof -
  from w obtain L τ' where Lτ': "finite L" "τ = τ'" "⋀y. y ∉ L ⟹ wff⇘τ'⇙(b⟨yf⇘σ⇙⟩)" 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⟨xf⇘σ⇙⟩ = fsub y σ (xf⇘σ⇙) (b⟨yf⇘σ⇙⟩)" using y
    by (intro fsub_intro) auto
  moreover have "wff⇘τ'⇙(fsub y σ (xf⇘σ⇙) (b⟨yf⇘σ⇙⟩))" 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 (no BKK counterpart: renaming serves the
  eigen-parameter bookkeeping of the calculus).›

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 realises 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 (nf⇘τ⇙) = nf⇘τ⇙"
  | "pvar w σ x (pp⇘τ⇙) = (if p = w ∧ τ = σ then xf⇘σ⇙ else pp⇘τ⇙)"
  | "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)
lemma occ_pvar: "occ (pvar w σw x t) ⊆ occ t ∪ {(x, σw)}"
  by (induction t) auto
lemma pars_pvar: "pars (pvar w σ x t) ⊆ pars t"
  by (induction t) auto
lemma pvar_image_id: "∀D ∈ Φ. w ∉ pars D ⟹ pvar w σ x ` Φ = Φ"
  by (auto simp: image_iff)

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⟨xf⇘σ⇙⟩ ≈⇘τ⇙ b'⟨xf⇘σ⇙⟩)
              ⟹ Λ⇘σ⇙ b ≈⇘σ⇒τ⇙ Λ⇘σ⇙ b'"

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

lemma beq_wff: assumes "s ≈⇘ρ⇙ t" shows beq_wffL: "wff⇘ρ⇙(s)" and beq_wffR: "wff⇘ρ⇙(t)"
  by (atomize (full))
     (induction rule: beq.induct[OF assms]; auto simp: wff_Abs intro: wff_App wff_opn)

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 abs thus ?case by (metis (mono_tags, lifting) beq.abs prn_opn tm.simps(120,128))
qed(auto intro: beq.intros)

text ‹And likewise under parameter-to-variable substitution.›

lemma beq_pvar: "s ≈⇘ρ⇙ t ⟹ pvar w σw x s ≈⇘ρ⇙ pvar w σw x t"
proof (induction rule: beq.induct)
  case beta thus ?case by (smt (verit, best) beq.simps pvar.simps(10,9) pvar_opn wff_pvar)
qed(auto simp: wff_pvar beq.abs pvar_opn intro: beq.intros)


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; we use our form throughout.
  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 @{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"
definition AndB :: "'p tm ⇒ 'p tm ⇒ 'p tm"  (infixr ‹∧› 62) where
  "A ∧ B ≡ ¬ (¬ 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 ‹Free-variable substitution distributes over the defined layer›

lemma fsub_Forall [simp]: "fsub x σ u (Π⇘τ⇙ b) = Π⇘τ⇙ (fsub x σ u b)"
  by (simp add: Forall_def)
lemma fsub_ImpB [simp]: "fsub x σ u (φ ⊃ ψ) = (fsub x σ u φ) ⊃ (fsub x σ u ψ)"
  by (simp add: ImpB_def)
lemma fsub_FalseB [simp]: "fsub x σ u (⊥ :: 'p tm) = ⊥"
  by (simp add: FalseB_def)
lemma fsub_TrueB [simp]: "fsub x σ u (⊤ :: 'p tm) = ⊤"
  by (simp add: TrueB_def)
lemma fsub_AndB [simp]: "fsub x σ u (A ∧ B) = (fsub x σ u A) ∧ (fsub x σ u B)"
  by (simp add: AndB_def)

text ‹Substituting for a variable that does not occur is the identity.›

lemma fsub_notin: "x ∉ fvs t ⟹ fsub x σ u t = t"
  by (induction t) auto

subsection ‹A convenient abstraction-typing rule›

text ‹If opening the body with @{emph ‹every›} free variable is well-typed, the cofinite
  side-condition of ‹wff_Abs› is met.  This is the form used for the closed defined
  terms below.›

lemma wff_AbsI: "(⋀x. wff⇘τ⇙(b⟨xf⇘σ⇙⟩)) ⟹ wff⇘σ⇒τ⇙(Λ⇘σ⇙ b)"
  by (auto intro: wff_Abs)

subsection ‹Typing of the defined layer›

lemma wff_Forall [intro]: "(⋀x. wff⇘𝗈⇙(b⟨xf⇘σ⇙⟩)) ⟹ 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⇘𝗈⇙((pf⇘σ ⇒ 𝗈⇙) ⋅ (xf⇘σ⇙))"
  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]])
lemma wff_AndB [intro]: "wff⇘𝗈⇙(A) ⟹ wff⇘𝗈⇙(B) ⟹ wff⇘𝗈⇙(A ∧ B)"
  by (auto simp: AndB_def)

subsection ‹Free variables and parameters 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)

text ‹And likewise the parameter-to-variable substitution ‹pvar›.›

lemma pvar_Forall [simp]: "pvar w σ x (Π⇘α⇙ b) = Π⇘α⇙ (pvar w σ x b)"
  by (simp add: Forall_def)
lemma pvar_Leib [simp]: "pvar w σ x (Leib α) = Leib α"
  by (simp add: Leib_def Forall_def ImpB_def)

text ‹Leibniz equality ‹β›-reduces to its ‹∀›-form.›

lemma Leib_beq: assumes wA: "wff⇘α⇙(A)" and wB: "wff⇘α⇙(B)"
  shows "(A ≐⇘α⇙ B) ≈⇘𝗈⇙ Π⇘α⇒𝗈⇙ ((Bnd 0 ⋅ A) ⊃ (Bnd 0 ⋅ B))"
proof -
  have lcA: "lc A" and lcB: "lc B" using wA wB by (auto intro: wff_lc)
  let ?inner = "Λ⇘α⇙ (Π⇘α⇒𝗈⇙ ((Bnd 0 ⋅ A) ⊃ (Bnd 0 ⋅ Bnd 1)))"
  have "(Leib α ⋅ A) ≈⇘α⇒𝗈⇙ ?inner"
    using beq.beta[OF wff_Leib[unfolded Leib_def] wA]
    unfolding Leib_def by (simp add: opn_lc[OF lcA])
  moreover {
    have "wff⇘α⇒𝗈⇙(?inner)" using beq_wffR calculation by blast
    with beq.beta[OF this wB]
    have "(?inner ⋅ B) ≈⇘𝗈⇙ Π⇘α⇒𝗈⇙ ((Bnd 0 ⋅ A) ⊃ (Bnd 0 ⋅ B))"
      using opn_lc[OF lcA] opn_lc[OF lcB] by simp
  }
  ultimately show ?thesis using beq.trans beq.appL wB by blast
qed

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 ‹xfσ› to the de Bruijn index ‹k›, so that
  ‹∃xσ. φ› and ‹Πxσ. φ› bind an ordinary named variable.  We call this operation
  @{emph ‹closing›} the variable ‹x›; it is the converse of opening (‹opn›) and is not to be
  confused with a @{emph ‹closed›} term, one without free variables.›

primrec clos :: "nat ⇒ nat ⇒ ty ⇒ 'p tm ⇒ 'p tm" where
  "clos k x σ (Bnd i) = Bnd i"
| "clos k x σ (nf⇘τ⇙) = (if n = x ∧ τ = σ then Bnd k else nf⇘τ⇙)"
| "clos k x σ (pp⇘τ⇙) = pp⇘τ⇙"
| "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)"

text ‹How closing interacts with opening, substitution and the occurrence sets.›

lemma opn_clos_sub: "opn k v t = t ⟹ opn k v (clos k x σ t) = fsub x σ v t"
  by (induction t arbitrary: k) auto

lemma fsub_id: "fsub x σ (xf⇘σ⇙) t = t"
  by (induction t) auto

lemma occ_clos: "(x, σ) ∉ occ (clos k x σ t)"
  by (induction t arbitrary: k) auto

lemma pars_clos [simp]: "pars (clos k x σ t) = pars t"
  by (induction t arbitrary: k) auto

lemma finite_occ: "finite (occ t)"
  by (induction t) auto

lemma occ_fsub_closed: "occ u = {} ⟹ occ (fsub x σ u t) = occ t - {(x, σ)}"
  by (induction t) auto

text ‹Closing (‹clos›) a variable that does not occur in the term is the identity.  Closing a
  variable ‹y› commutes with the substitution ‹fsub› of a term ‹u› for a different variable
  ‹x›, provided ‹y› does not occur in ‹u›; hence ‹fsub› passes through the named binders.›

lemma clos_notin: "x ∉ fvs t ⟹ clos k x σ t = t"
  by (induction t arbitrary: k) auto

lemma fsub_clos:
  "(x, σ) ≠ (y, τ) ⟹ y ∉ fvs u ⟹ fsub x σ u (clos k y τ b) = clos k y τ (fsub x σ u b)"
  by (induction b arbitrary: k) (auto simp: clos_notin)

lemma fsub_AllN:
  "(x, σ) ≠ (y, τ) ⟹ y ∉ fvs u ⟹ fsub x σ u (Πy⇘τ⇙. b) = Πy⇘τ⇙. (fsub x σ u b)"
  by (simp add: AllN_def fsub_clos)

lemma fsub_ExN:
  "(x, σ) ≠ (y, τ) ⟹ y ∉ fvs u ⟹ fsub x σ u (∃y⇘τ⇙. b) = ∃y⇘τ⇙. (fsub x σ u b)"
  by (simp add: ExN_def fsub_clos)

lemma wff_LamN_clos:
  assumes "wff⇘𝗈⇙(b)"
  shows "wff⇘σ ⇒ 𝗈⇙(Λ⇘σ⇙ (clos 0 v σ b))"
  by (metis assms opn_clos_sub opn_lc wff_AbsI wff_Fre wff_fsub wff_lc)

lemma wff_AllN: assumes "wff⇘𝗈⇙(b)" shows "wff⇘𝗈⇙(Πv⇘σ⇙. b)"
  by (metis AllN_def Forall_def assms wff_App wff_LamN_clos wff_Pi)

lemma wff_ExN: assumes w: "wff⇘𝗈⇙(b)" shows "wff⇘𝗈⇙(∃v⇘σ⇙. b)"
  by (metis AllN_def ExN_def clos.simps(4,9) w wff_AllN wff_App wff_Neg)

subsection ‹Closed well-formed terms›

text ‹A @{emph ‹closed›} well-formed term, BKK's ‹cwffσ› (BKK Section 2.2; BKK reserve
  @{emph ‹sentence›} for closed formulae of type ‹𝗈› --- parameters are allowed,
  they play the role of BKK's constants).  These are the carriers of the term model.›

definition cwff :: "ty ⇒ 'p tm ⇒ bool" where "cwff σ A ≡ wff⇘σ⇙(A) ∧ fvs A = {}"
lemma cwffI: "wff⇘σ⇙(A) ⟹ fvs A = {} ⟹ cwff σ A" by (simp add: cwff_def)
lemma cwff_wff: "cwff σ A ⟹ wff⇘σ⇙(A)" by (simp add: cwff_def)
lemma cwff_closed: "cwff σ A ⟹ fvs A = {}" by (simp add: cwff_def)
lemma cwff_lc: "cwff σ A ⟹ lc A" by (metis cwff_def wff_lc)
lemma cwff_Neg: "cwff (𝗈⇒𝗈) Neg"
  and cwff_Dis: "cwff (𝗈⇒𝗈⇒𝗈) Dis"
  and cwff_Pi: "cwff ((σ⇒𝗈)⇒𝗈) (Pi σ)"
  and cwff_Iota: "cwff ((σ⇒𝗈)⇒σ) (Iota σ)"
  and cwff_TrueB: "cwff 𝗈 ⊤"
  and cwff_FalseB: "cwff 𝗈 ⊥"
  by (auto simp: cwff_def wff_Neg wff_Dis wff_Pi wff_Iota)
lemma cwff_Eq: "cwff (σ⇒σ⇒𝗈) (Eq σ)" by (simp add: cwff_def wff_Eq)
lemma cwff_Leib: "cwff (σ⇒σ⇒𝗈) (Leib σ)" by (simp add: cwff_def)
lemma cwff_Par: "cwff σ (pp⇘σ⇙)" by (simp add: cwff_def wff_Par)
lemma cwff_App: "cwff (σ⇒τ) s ⟹ cwff σ t ⟹ cwff τ (s ⋅ t)"
  by (auto simp: cwff_def intro: wff.wff_App)
lemma cwff_LeibE: "cwff α A ⟹ cwff α B ⟹ cwff 𝗈 (A ≐⇘α⇙ B)"
  by (meson cwff_App cwff_Leib)
lemma cwff_opn: "cwff (σ⇒τ) (Λ⇘σ⇙ b) ⟹ cwff σ a ⟹ cwff τ (b⟨a⟩)"
  by (metis (no_types, opaque_lifting) cwff_def fvs.simps(10) fvs_opn
      subset_empty sup.idem wff_opn)
lemma cwff_unique: "cwff σ A ⟹ cwff τ A ⟹ σ = τ"
  by (auto simp: cwff_def dest: wff_unique)

text ‹Converse of @{thm wff_Abs_open}: a body that is well-typed when opened with @{emph ‹one›}
  fresh variable yields a well-typed abstraction (all fresh openings are ‹α›-variants).›

lemma wff_Abs_open_rev: "wff⇘τ⇙(b⟨xf⇘σ⇙⟩) ⟹ x ∉ fvs b ⟹ wff⇘σ⇒τ⇙(Λ⇘σ⇙ b)"
  by (metis fsub_intro wff_AbsI wff_Fre wff_fsub)

subsection ‹Simultaneous substitution›

text ‹Simultaneous substitution of a term for every free variable --- the general form of
  which ‹fsub› is the single-variable and ‹vpar› (below) the variable-to-parameter instance,
  and the analogue of the closing substitution ‹σ› in BKK's term evaluation (BKK Definition
  3.35).  For locally closed replacements it commutes with opening --- the locally-nameless analogue
  of BKK's parallel substitution, with no binder renaming.›

primrec msub :: "(nat ⇒ ty ⇒ 'p tm) ⇒ 'p tm ⇒ 'p tm" where
    "msub ρ (Bnd i) = Bnd i"
  | "msub ρ (nf⇘τ⇙) = ρ n τ"
  | "msub ρ (pp⇘τ⇙) = pp⇘τ⇙"
  | "msub ρ Neg = Neg"
  | "msub ρ Dis = Dis"
  | "msub ρ (Pi τ) = Pi τ"
  | "msub ρ (Iota τ) = Iota τ"
  | "msub ρ (Eq τ) = Eq τ"
  | "msub ρ (s ⋅ t) = (msub ρ s) ⋅ (msub ρ t)"
  | "msub ρ (Λ⇘τ⇙ b) = Λ⇘τ⇙ (msub ρ b)"

lemma msub_opn: "(⋀n τ. lc (ρ n τ)) ⟹ msub ρ (opn k u t) = opn k (msub ρ u) (msub ρ t)"
  by (induction t arbitrary: k) auto
lemma msub_cong: "(⋀n τ. (n, τ) ∈ occ t ⟹ ρ n τ = ρ' n τ) ⟹ msub ρ t = msub ρ' t"
  by (induction t) auto
lemma msub_id: "msub (λn τ. nf⇘τ⇙) t = t"
  by (induction t) auto
lemma fvs_msub: "(⋀n τ. fvs (ρ n τ) = {}) ⟹ fvs (msub ρ t) = {}"
  by (induction t) auto
lemma wff_msub:
  "wff⇘σ⇙(t) ⟹ (⋀n τ. wff⇘τ⇙(ρ n τ)) ⟹ wff⇘σ⇙(msub ρ t)"
proof (induction σ t arbitrary: ρ rule: wff.induct)
  case (wff_Abs L τ b σ)
  have lcr: "lc (ρ n τ')" for n τ' using wff_Abs.prems
    by (rule wff_lc)
  have "wff⇘σ⇒τ⇙(Λ⇘σ⇙ (msub ρ b))"
  proof (rule wff.wff_Abs[of "L ∪ fvs b"])
    fix y assume y: "y ∉ L ∪ fvs b"
    let ?ρ = "ρ(y := (ρ y)(σ := yf⇘σ⇙))"
    have e: "msub ?ρ (b⟨yf⇘σ⇙⟩) = (msub ρ b)⟨yf⇘σ⇙⟩"
      by (smt (verit, ccfv_SIG) Un_iff fun_upd_other fun_upd_same
              fvs_eq_fst_occ image_eqI lc_Fre lcr msub.simps(2)
              msub_cong msub_opn prod.sel(1) y)
    have "wff⇘τ⇙(msub ?ρ (b⟨yf⇘σ⇙⟩))"
      using wff_Abs wff.wff_Fre y by (metis Un_iff fun_upd_other fun_upd_same)
    thus "wff⇘τ⇙((msub ρ b)⟨yf⇘σ⇙⟩)" using e by simp
  qed (simp add: wff_Abs)
  thus ?case by simp
qed(auto intro: wff.intros)

text ‹A well-formed term becomes a @{emph ‹closed›} well-formed term under a closed simultaneous
  substitution --- the instance used to build the term model.›

lemma cwff_msub: "wff⇘σ⇙(t) ⟹ (⋀n τ. cwff τ (ρ n τ)) ⟹ cwff σ (msub ρ t)"
  by (metis cwff_def wff_msub fvs_msub)

text ‹A closed term is untouched by simultaneous substitution.›

lemma msub_closed: "fvs t = {} ⟹ msub ρ t = t" by (induction t) auto

text ‹Substituting one closed replacement first: for a variable whose replacement is closed,
  the simultaneous substitution factors through the single substitution ‹fsub›.›

lemma msub_step:
  assumes cl: "fvs (ρ x σ) = {}"
  shows "msub ρ t = msub (λn τ. if n = x ∧ τ = σ then nf⇘τ⇙ else ρ n τ) (fsub x σ (ρ x σ) t)"
  by (induction t) (auto simp: msub_closed[OF cl])

text ‹‹vshift› renames every free variable ‹n› to ‹n + 1›, freeing the name ‹0› at every
  type; ‹β›-equality and typing are stable under it.›

definition vshift :: "'p tm ⇒ 'p tm" where "vshift = msub (λn τ. (Suc n)f⇘τ⇙)"
lemma occ_vshift: "occ (vshift t) = (λ(n, τ). (Suc n, τ)) ` occ t"
  unfolding vshift_def by (induction t) (auto simp: image_Un)
lemma pars_vshift: "pars (vshift t) = pars t"
  unfolding vshift_def by (induction t) auto
lemma wff_vshift: "wff⇘τ⇙(t) ⟹ wff⇘τ⇙(vshift t)"
  by (auto elim: wff_msub intro: wff_Fre simp: vshift_def)
lemma vshift_opn: "vshift (t⟨xf⇘σ⇙⟩) = (vshift t)⟨(Suc x)f⇘σ⇙⟩"
  unfolding vshift_def by (subst msub_opn) auto
lemma beq_vshift: "s ≈⇘ρ⇙ t ⟹ vshift s ≈⇘ρ⇙ vshift t"
proof (induction rule: beq.induct)
  case (beta σ ρ b a)
  moreover have "vshift ((Λ⇘σ⇙ b) ⋅ a) = (Λ⇘σ⇙ (vshift b)) ⋅ (vshift a)"
    by (simp add: vshift_def)
  moreover have "vshift (b⟨a⟩) = (vshift b)⟨vshift a⟩"
    unfolding vshift_def by (subst msub_opn) auto
  moreover have "wff⇘σ⇒ρ⇙(Λ⇘σ⇙ (vshift b))"
    using wff_vshift beta unfolding vshift_def by force
  ultimately show ?case using beq.beta wff_vshift by metis
next case appL thus ?case by (metis beq.appL msub.simps(9) vshift_def wff_vshift)
next case appR thus ?case by (metis beq.appR msub.simps(9) vshift_def wff_vshift)
next case (abs L b σ τ b')
  have "Λ⇘σ⇙ (vshift b) ≈⇘σ⇒τ⇙ Λ⇘σ⇙ (vshift b')"
  proof (rule beq.abs[of "{0} ∪ Suc ` L"])
    show "finite ({0} ∪ Suc ` L)" using abs.hyps(1) by simp
    fix y assume y: "y ∉ {0} ∪ Suc ` L"
    then obtain x where x: "y = Suc x" "x ∉ L" by (cases y) auto
    show "(vshift b)⟨yf⇘σ⇙⟩ ≈⇘τ⇙ (vshift b')⟨yf⇘σ⇙⟩" using abs.IH[OF x(2)]
      by (simp add: x(1) vshift_opn[symmetric])
  qed
  thus ?case by (simp add: vshift_def)
qed(auto simp: wff_vshift intro: beq.intros)

text ‹Replacing every free variable of a stock ‹S› at once by a parameter --- the converse of
  @{const pvar}, as the parameter-valued instance of @{const msub}.›

definition vpar :: "(nat × ty) set ⇒ (nat ⇒ ty ⇒ 'p) ⇒ 'p tm ⇒ 'p tm" where
  "vpar S π ≡ msub (λn τ. if (n, τ) ∈ S then (π n τ)p⇘τ⇙ else nf⇘τ⇙)"

lemma vpar_id: "S ∩ occ t = {} ⟹ vpar S π t = t"
  unfolding vpar_def by (subst msub_cong[where ρ' = "λn τ. nf⇘τ⇙"]) (auto simp: msub_id)

lemma vpar_cong: "occ t ⊆ S ⟹ vpar S π t = vpar UNIV π t"
  unfolding vpar_def by (rule msub_cong) auto

lemma pars_vpar: "q ∈ pars (vpar S π t) ⟹ q ∈ pars t ∨ (∃n σ. q = π n σ)"
  unfolding vpar_def by (induction t) (auto split: if_splits)

lemma cwff_vpar: "wff⇘τ⇙(t) ⟹ cwff τ (vpar UNIV π t)"
  unfolding vpar_def by (rule cwff_msub) (auto intro: cwffI wff_Par)

text ‹And @{const pvar} inverts it, one parameter at a time --- injectivity of ‹π› protects
  the not-yet-inverted parameters, freshness the original ones.›

lemma pvar_vpar:
  assumes inj: "⋀n τ. π n τ = π x σ ⟹ n = x ∧ τ = σ"
  shows "π x σ ∉ pars t ⟹ pvar (π x σ) σ x (vpar S π t) = vpar (S - {(x, σ)}) π t"
  unfolding vpar_def by (induction t) (auto dest: inj)

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 ‹Closing removes free occurrences of the closed name.›

lemma fvs_clos: "fvs (clos k v σ b) ⊆ fvs b"
  by (induction b arbitrary: k) auto

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 xf⇘α⇙›
      and ‹⋀x α. P xp⇘α⇙›
      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