Theory Smolka

theory Smolka
  imports Main
begin

section ‹Human-authored proof formalization›

text ‹
  Formalization of the correctness proof of the Smolka-Blanchette algorithm
  for minimal type annotation of terms.

  The algorithm takes a Church-typed term and removes type annotations while
  preserving unique type-reconstruction, achieving both completeness (unique
  well-typed completion) and local minimality (removing any further annotation
  breaks uniqueness).
›

subsection ‹Types›

text ‹
  Corresponds to Subsection 1.1 of the paper.
  We fix an infinite set of type variables and define types as:
    $\sigma ::= \alpha | \sigma \Rightarrow \tau | (\sigma_1, ..., \sigma_n) \kappa$
  We represent this as a datatype with \<^term>‹Arrow› as a distinguished binary constructor
  and \<^term>‹TyCon› for n-ary type constructors.
›

datatype ('tv, 'k) ty =
  TyVar 'tv
| Arrow "('tv, 'k) ty" "('tv, 'k) ty"
| TyCon 'k "('tv, 'k) ty list"

text ‹
  Maybe-types: \<^typ>‹('tv, 'k) ty option› where \<^term>‹None› represents $\bot$ (no type annotation)
  and \<^term>‹Some σ› represents an actual type.
›

type_synonym ('tv, 'k) mty = "('tv, 'k) ty option"

subsubsection ‹Type variables of a type›

text ‹
  \<^term>‹tvars_ty›: the set of type variables occurring in a type.
  Extended to maybe-types with \<^term>‹tvars_mty None = {}›.
›

fun tvars_ty :: "('tv, 'k) ty ⇒ 'tv set" where
  "tvars_ty (TyVar a) = {a}"
| "tvars_ty (Arrow σ τ) = tvars_ty σ ∪ tvars_ty τ"
| "tvars_ty (TyCon κ σs) = ⋃(tvars_ty ` set σs)"

definition tvars_mty :: "('tv, 'k) mty ⇒ 'tv set" where
  "tvars_mty ξ = (case ξ of None ⇒ {} | Some σ ⇒ tvars_ty σ)"

lemma tvars_mty_None[simp]: "tvars_mty None = {}"
  by (simp add: tvars_mty_def)

lemma tvars_mty_Some[simp]: "tvars_mty (Some σ) = tvars_ty σ"
  by (simp add: tvars_mty_def)

lemma tvars_ty_finite[simp, intro]: "finite (tvars_ty τ)"
  by (induction τ) auto

lemma tvars_mty_finite[simp, intro]: "finite (tvars_mty ξ)"
  by (cases ξ) auto

subsubsection ‹Type substitution›

text ‹
  A type substitution is a function from type variables to types.
  \<^term>‹subst_ty ρ σ› applies \<^term>‹ρ› to \<^term>‹σ›.
  Extended to maybe-types with \<^term>‹subst_mty ρ None = None›.
›

fun subst_ty :: "('tv ⇒ ('tv, 'k) ty) ⇒ ('tv, 'k) ty ⇒ ('tv, 'k) ty" where
  "subst_ty ρ (TyVar a) = ρ a"
| "subst_ty ρ (Arrow σ τ) = Arrow (subst_ty ρ σ) (subst_ty ρ τ)"
| "subst_ty ρ (TyCon κ σs) = TyCon κ (map (subst_ty ρ) σs)"

definition subst_mty :: "('tv ⇒ ('tv, 'k) ty) ⇒ ('tv, 'k) mty ⇒ ('tv, 'k) mty" where
  "subst_mty ρ ξ = map_option (subst_ty ρ) ξ"

lemma subst_mty_None[simp]: "subst_mty ρ None = None"
  by (simp add: subst_mty_def)

lemma subst_mty_Some[simp]: "subst_mty ρ (Some σ) = Some (subst_ty ρ σ)"
  by (simp add: subst_mty_def)

subsubsection ‹Substitution composition and single substitution›

definition comp_subst ::
  "('tv ⇒ ('tv,'k) ty) ⇒ ('tv ⇒ ('tv,'k) ty) ⇒ ('tv ⇒ ('tv,'k) ty)" (infixl "∘∘" 55) where
  "(ρ ∘∘ ρ') a = subst_ty ρ (ρ' a)"

text ‹
  Composition \<^term>‹ρ ∘∘ ρ'› is defined by \<^term>‹(ρ ∘∘ ρ') a = subst_ty ρ (ρ' a)›.
  Single substitution \<^term>‹single_subst τ α› maps \<^term>‹α› to \<^term>‹τ› and everything else to itself.
›

definition single_subst :: "('tv,'k) ty ⇒ 'tv ⇒ ('tv ⇒ ('tv,'k) ty)" where
  "single_subst τ α = (λa. if a = α then τ else TyVar a)"

lemma single_subst_same[simp]: "single_subst τ α α = τ"
  by (simp add: single_subst_def)

lemma single_subst_other[simp]: "a ≠ α ⟹ single_subst τ α a = TyVar a"
  by (simp add: single_subst_def)

subsubsection ‹Basic properties of substitution›

lemma subst_ty_comp:
  "subst_ty ρ (subst_ty ρ' τ) = subst_ty (ρ ∘∘ ρ') τ"
  by (induction τ) (auto simp: comp_subst_def)

lemma subst_ty_id[simp]: "subst_ty TyVar τ = τ"
  by (induction τ) (auto simp: map_idI)

lemma subst_mty_id[simp]: "subst_mty TyVar ξ = ξ"
  by (cases ξ) (auto simp: subst_mty_def)

lemma subst_mty_comp: "subst_mty ρ (subst_mty ρ' ξ) = subst_mty (ρ ∘∘ ρ') ξ"
  by (cases ξ) (auto simp: subst_mty_def subst_ty_comp comp_subst_def)

lemma subst_ty_agree:
  "subst_ty ρ τ = subst_ty ρ' τ ⟷ (∀α ∈ tvars_ty τ. ρ α = ρ' α)"
  by (induction τ) auto

lemma subst_ty_cong:
  "(⋀α. α ∈ tvars_ty τ ⟹ ρ α = ρ' α) ⟹ subst_ty ρ τ = subst_ty ρ' τ"
  using subst_ty_agree by blast

lemma subst_ty_swap:
  assumes "β ∉ tvars_ty τ"
  shows "subst_ty (single_subst (TyVar α) β) (subst_ty (single_subst (TyVar β) α) τ) = τ"
  using assms
  by (induction τ) (auto simp: map_idI single_subst_def)

text ‹Substitution distributes over \<^const>‹tvars_ty›.›
lemma tvars_ty_subst: "tvars_ty (subst_ty ρ τ) = ⋃(tvars_ty ` ρ ` tvars_ty τ)"
  by (induction τ) auto

lemma tvars_mty_subst:
  "tvars_mty (subst_mty ρ ξ) = ⋃(tvars_ty ` ρ ` tvars_mty ξ)"
  by (cases ξ) (auto simp: tvars_ty_subst)


subsection ‹Terms›

text ‹
  Partially-typed terms: $t ::= x_\xi | c_\xi | (t1~t2)_\xi | (\lambda x_\xi. t)_\zeta$
  We do not quotient by alpha-equivalence.
›

datatype ('tv, 'k, 'v, 'c) trm =
  Vr 'v "('tv,'k) mty"
| Ct 'c "('tv,'k) mty"
| App "('tv,'k,'v,'c) trm" "('tv,'k,'v,'c) trm" "('tv,'k) mty"
| Lam 'v "('tv,'k) mty" "('tv,'k,'v,'c) trm" "('tv,'k) mty"

subsubsection ‹Type variables of a term›

text ‹\<^term>‹tvars_trm›: set of type variables occurring in all annotations of a term.›

fun tvars_trm :: "('tv,'k,'v,'c) trm ⇒ 'tv set" where
  "tvars_trm (Vr x ξ) = tvars_mty ξ"
| "tvars_trm (Ct c ξ) = tvars_mty ξ"
| "tvars_trm (App t1 t2 ξ) = tvars_trm t1 ∪ tvars_trm t2 ∪ tvars_mty ξ"
| "tvars_trm (Lam x ξ t ζ) = tvars_mty ξ ∪ tvars_trm t ∪ tvars_mty ζ"

lemma tvars_trm_finite[simp, intro]: "finite (tvars_trm t)"
  by (induction t) auto

subsubsection ‹Substitution on terms›

text ‹\<^term>‹subst_trm ρ t›: apply type substitution \<^term>‹ρ› to all type annotations in \<^term>‹t›.›

fun subst_trm :: "('tv ⇒ ('tv,'k) ty) ⇒ ('tv,'k,'v,'c) trm ⇒ ('tv,'k,'v,'c) trm" where
  "subst_trm ρ (Vr x ξ) = Vr x (subst_mty ρ ξ)"
| "subst_trm ρ (Ct c ξ) = Ct c (subst_mty ρ ξ)"
| "subst_trm ρ (App t1 t2 ξ) = App (subst_trm ρ t1) (subst_trm ρ t2) (subst_mty ρ ξ)"
| "subst_trm ρ (Lam x ξ t ζ) = Lam x (subst_mty ρ ξ) (subst_trm ρ t) (subst_mty ρ ζ)"

lemma subst_trm_comp:
  "subst_trm ρ (subst_trm ρ' t) = subst_trm (ρ ∘∘ ρ') t"
  by (induction t) (auto simp: subst_mty_comp)

lemma subst_trm_id[simp]: "subst_trm TyVar t = t"
  by (induction t) auto

lemma subst_trm_cong:
  "(⋀α. α ∈ tvars_trm t ⟹ ρ α = ρ' α) ⟹ subst_trm ρ t = subst_trm ρ' t"
proof (induction t)
  case (Vr x ξ)
  then show ?case by (cases ξ) (auto intro: subst_ty_cong)
next
  case (Ct c ξ)
  then show ?case by (cases ξ) (auto intro: subst_ty_cong)
next
  case (App t1 t2 ξ)
  then show ?case by (cases ξ) (auto cong: subst_ty_cong)
next
  case (Lam x ξ t ζ)
  then show ?case by (cases ξ; cases ζ) (auto intro: subst_ty_cong)
qed

lemma subst_trm_agree:
  "subst_trm ρ t = subst_trm ρ' t ⟷ (∀α ∈ tvars_trm t. ρ α = ρ' α)"
proof (induction t)
  case (Vr x ξ)
  then show ?case by (cases ξ) (auto simp: subst_ty_agree)
next
  case (Ct c ξ)
  then show ?case by (cases ξ) (auto simp: subst_ty_agree)
next
  case (App t1 t2 ξ)
  then show ?case by (cases ξ) (auto simp: subst_ty_agree)
next
  case (Lam x ξ t ζ)
  then show ?case by (cases ξ; cases ζ) (auto simp: subst_ty_agree)
qed

text ‹If \<^term>‹subst_trm ρ v = v›, then \<^term>‹ρ› acts as identity on \<^term>‹tvars_trm v›.›
lemma subst_trm_id_on_tvars:
  assumes "subst_trm ρ v = v" "α ∈ tvars_trm v"
  shows "ρ α = TyVar α"
proof -
  from assms(1) have "subst_trm ρ v = subst_trm TyVar v" by simp
  then have "∀α ∈ tvars_trm v. ρ α = TyVar α" by (simp only: subst_trm_agree)
  with assms(2) show ?thesis by blast
qed

lemma subst_trm_swap:
  assumes "β ∉ tvars_trm t"
  shows "subst_trm (single_subst (TyVar α) β) (subst_trm (single_subst (TyVar β) α) t) = t"
  using assms
proof (induction t)
  case (Vr x ξ)
  then show ?case by (cases ξ) (auto simp: subst_ty_swap)
next
  case (Ct c ξ)
  then show ?case by (cases ξ) (auto simp: subst_ty_swap)
next
  case (App t1 t2 ξ)
  then show ?case by (cases ξ) (auto simp: subst_ty_swap)
next
  case (Lam x ξ t ζ)
  then show ?case by (cases ξ; cases ζ) (auto simp: subst_ty_swap)
qed

lemma tvars_trm_subst:
  "tvars_trm (subst_trm ρ t) = ⋃(tvars_ty ` ρ ` tvars_trm t)"
  by (induction t) (auto simp: tvars_mty_subst)

subsubsection ‹Term predicates: F-term, U-term, C-term›

text ‹
  F-term: all annotations are types \<^term>‹None›.
  U-term: all annotations are \<^term>‹None›.
  C-term: variable and constant annotations are types, application and abstraction
  outer annotations are \<^term>‹None›, and binding variable annotations are types.
›

fun fterm :: "('tv,'k,'v,'c) trm ⇒ bool" where
  "fterm (Vr x ξ) ⟷ ξ ≠ None"
| "fterm (Ct c ξ) ⟷ ξ ≠ None"
| "fterm (App t1 t2 ξ) ⟷ fterm t1 ∧ fterm t2 ∧ ξ ≠ None"
| "fterm (Lam x ξ t ζ) ⟷ ξ ≠ None ∧ fterm t ∧ ζ ≠ None"

fun uterm :: "('tv,'k,'v,'c) trm ⇒ bool" where
  "uterm (Vr x ξ) ⟷ ξ = None"
| "uterm (Ct c ξ) ⟷ ξ = None"
| "uterm (App t1 t2 ξ) ⟷ uterm t1 ∧ uterm t2 ∧ ξ = None"
| "uterm (Lam x ξ t ζ) ⟷ ξ = None ∧ uterm t ∧ ζ = None"

fun cterm :: "('tv,'k,'v,'c) trm ⇒ bool" where
  "cterm (Vr x ξ) ⟷ ξ ≠ None"
| "cterm (Ct c ξ) ⟷ ξ ≠ None"
| "cterm (App t1 t2 ξ) ⟷ cterm t1 ∧ cterm t2 ∧ ξ = None"
| "cterm (Lam x ξ t ζ) ⟷ ξ ≠ None ∧ cterm t ∧ ζ = None"

lemma fterm_subst[simp]: "fterm v ⟹ fterm (subst_trm ρ v)"
  by (induction v) auto

subsubsection ‹Unambiguity›

text ‹
  A term is unambiguous if no variable appears as a binding variable at two
  different positions. We define the set of binding variables and then unambiguity.
›

fun bvars :: "('tv,'k,'v,'c) trm ⇒ 'v set" where
  "bvars (Vr x ξ) = {}"
| "bvars (Ct c ξ) = {}"
| "bvars (App t1 t2 ξ) = bvars t1 ∪ bvars t2"
| "bvars (Lam x ξ t ζ) = {x} ∪ bvars t"
                                          
lemma subst_trm_bvars[simp]: "bvars (subst_trm ρ t) = bvars t"
  by (induction t) auto

fun unambiguous :: "('tv,'k,'v,'c) trm ⇒ bool" where
  "unambiguous (Vr x ξ) ⟷ True"
| "unambiguous (Ct c ξ) ⟷ True"
| "unambiguous (App t1 t2 ξ) ⟷
    unambiguous t1 ∧ unambiguous t2 ∧ bvars t1 ∩ bvars t2 = {}"
| "unambiguous (Lam x ξ t ζ) ⟷
    unambiguous t ∧ x ∉ bvars t"

lemma subst_trm_unambiguous[simp]: "unambiguous (subst_trm ρ t) = unambiguous t"
  by (induction t) auto

subsection ‹Positions›

text ‹
  Positions are lists of naturals in \<^term>‹{1,2}›.
  \<^term>‹poss t›: the set of positions of a term.
  \<^term>‹mtp_of t p›: the maybe-type at position \<^term>‹p› in \<^term>‹t›.
›

fun poss :: "('tv,'k,'v,'c) trm ⇒ nat list set" where
  "poss (Vr x ξ) = {[]}"
| "poss (Ct c ξ) = {[]}"
| "poss (App t1 t2 ξ) = {[]} ∪ ((λp. 1 # p) ` poss t1) ∪ ((λp. 2 # p) ` poss t2)"
| "poss (Lam x ξ t ζ) = {[]} ∪ {[1]} ∪ ((λp. 2 # p) ` poss t)"

lemma poss_finite[simp, intro]: "finite (poss t)"
  by (induction t) auto

lemma nil_in_poss[simp]: "[] ∈ poss t"
  by (cases t) auto

lemma subst_trm_poss[simp]: "poss (subst_trm ρ t) = poss t"
  by (induction t) auto

fun mtp_of :: "('tv,'k,'v,'c) trm ⇒ nat list ⇒ ('tv,'k) mty" where
  "mtp_of (Vr x ξ) p = ξ"
| "mtp_of (Ct c ξ) p = ξ"
| "mtp_of (App t1 t2 ξ) p = (case p of
    [] ⇒ ξ
  | (Suc 0 # p') ⇒ mtp_of t1 p'
  | (Suc (Suc 0) # p') ⇒ mtp_of t2 p'
  | _ ⇒ None)"
| "mtp_of (Lam x ξ t ζ) p = (case p of
    [] ⇒ ζ
  | [Suc 0] ⇒ ξ
  | (Suc (Suc 0) # p') ⇒ mtp_of t p'
  | _ ⇒ None)"

text ‹
    \<^term>‹mtpOf t› is the maybe-type of the root of \<^term>‹t›.
›

abbreviation mtp_of_root :: "('tv,'k,'v,'c) trm ⇒ ('tv,'k) mty" where
  "mtp_of_root t ≡ mtp_of t []"

lemma mtp_of_subst:
  assumes "p ∈ poss t"
  shows "mtp_of (subst_trm ρ t) p = subst_mty ρ (mtp_of t p)"
  using assms by (induction t arbitrary: p) (auto split: list.splits nat.splits)

lemma tvars_trm_eq_UN_mtp:
  "tvars_trm t = (⋃p ∈ poss t. tvars_mty (mtp_of t p))"
  by (induction t) (auto simp: image_iff)

lemma fterm_mtp_of_Some:
  assumes "fterm v" "p ∈ poss v"
  shows "∃σ. mtp_of v p = Some σ"
  using assms by (induction v arbitrary: p) (auto split: list.splits nat.splits)

subsubsection ‹Removing annotations›

fun remove_annot :: "('tv,'k,'v,'c) trm ⇒ nat list ⇒ ('tv,'k,'v,'c) trm" where
  "remove_annot (Vr x ξ) p = Vr x None"
| "remove_annot (Ct c ξ) p = Ct c None"
| "remove_annot (App t1 t2 ξ) p = (case p of
    [] ⇒ App t1 t2 None
  | Suc 0 # p' ⇒ App (remove_annot t1 p') t2 ξ
  | Suc (Suc 0) # p' ⇒ App t1 (remove_annot t2 p') ξ
  | _ ⇒ App t1 t2 None)"
| "remove_annot (Lam x ξ t ζ) p = (case p of
    [] ⇒ Lam x ξ t None
  | [Suc 0] ⇒ Lam x None t ζ
  | Suc (Suc 0) # p' ⇒ Lam x ξ (remove_annot t p') ζ
  | _ ⇒ Lam x ξ t None)"

lemma mtp_of_remove_self:
  assumes "p ∈ poss t"
  shows "mtp_of (remove_annot t p) p = None"
  using assms by (induction t arbitrary: p) auto

lemma mtp_of_remove_other:
  assumes "p ∈ poss t" "q ∈ poss t" "q ≠ p"
  shows "mtp_of (remove_annot t p) q = mtp_of t q"
  using assms
  by (induction t arbitrary: p q) fastforce+

lemma remove_annot_poss:
  assumes "p ∈ poss t"
  shows "poss (remove_annot t p) = poss t"
  using assms by (induction t arbitrary: p) auto

lemma remove_annot_bvars:
  assumes "p ∈ poss t"
  shows "bvars (remove_annot t p) = bvars t"
  using assms by (induction t arbitrary: p) auto

lemma remove_annot_unambiguous:
  assumes "p ∈ poss t" "unambiguous t"
  shows "unambiguous (remove_annot t p)"
  using assms by (induction t arbitrary: p) (auto simp: remove_annot_bvars)

text ‹Erase: remove all type annotations.›

fun erase :: "('tv,'k,'v,'c) trm ⇒ ('tv,'k,'v,'c) trm" where
  "erase (Vr x ξ) = Vr x None"
| "erase (Ct c ξ) = Ct c None"
| "erase (App t1 t2 ξ) = App (erase t1) (erase t2) None"
| "erase (Lam x ξ t ζ) = Lam x None (erase t) None"

lemma erase_uterm[simp]: "uterm (erase t)"
  by (induction t) auto

lemma erase_poss[simp]: "poss (erase t) = poss t"
  by (induction t) auto

lemma erase_bvars[simp]: "bvars (erase t) = bvars t"
  by (induction t) auto

lemma erase_unambiguous[simp]: "unambiguous (erase t) = unambiguous t"
  by (induction t) auto

subsection ‹Completion relations for types and terms›

definition mcompl :: "('tv,'k) mty ⇒ ('tv,'k) mty ⇒ bool" (infix "⊑⇩m" 50) where
  "ξ ⊑⇩m ζ ⟷ (ξ = None ∨ ξ = ζ)"

lemma mcompl_None[simp, intro]: "None ⊑⇩m ζ"
  by (simp add: mcompl_def)

lemma mcompl_refl[simp, intro]: "ξ ⊑⇩m ξ"
  by (simp add: mcompl_def)

lemma mcompl_Some_iff[simp]: "Some σ ⊑⇩m ζ ⟷ ζ = Some σ"
  by (auto simp: mcompl_def)

lemma mcompl_antisym: "⟦ ξ ⊑⇩m ζ; ζ ⊑⇩m ξ ⟧ ⟹ ξ = ζ"
  by (auto simp: mcompl_def)

lemma mcompl_trans: "⟦ ξ ⊑⇩m ζ; ζ ⊑⇩m χ ⟧ ⟹ ξ ⊑⇩m χ"
  by (auto simp: mcompl_def)

inductive compl :: "('tv,'k,'v,'c) trm ⇒ ('tv,'k,'v,'c) trm ⇒ bool" (infix "⊑" 50) where
  compl_Vr: "ξ ⊑⇩m ζ ⟹ Vr x ξ ⊑ Vr x ζ"
| compl_Ct: "ξ ⊑⇩m ζ ⟹ Ct c ξ ⊑ Ct c ζ"
| compl_App: "⟦ s1 ⊑ s1'; s2 ⊑ s2'; ξ ⊑⇩m ξ' ⟧ ⟹ App s1 s2 ξ ⊑ App s1' s2' ξ'"
| compl_Lam: "⟦ ζ ⊑⇩m ζ'; t ⊑ t'; ξ ⊑⇩m ξ' ⟧ ⟹ Lam x ζ t ξ ⊑ Lam x ζ' t' ξ'"

subsubsection ‹Inversion rules›
text ‹Inversion rules for \<^term>‹compl›. These follow from the cases rule.›

lemma compl_Vr_leftE:
  assumes "Vr x ξ ⊑ t"
  obtains ξ' where "ξ ⊑⇩m ξ'" "t = Vr x ξ'"
  using assms by (cases rule: compl.cases) auto

lemma compl_Ct_leftE:
  assumes "Ct c ξ ⊑ t"
  obtains ξ' where "ξ ⊑⇩m ξ'" "t = Ct c ξ'"
  using assms by (cases rule: compl.cases) auto

lemma compl_App_leftE:
  assumes "App s1 s2 ξ ⊑ t"
  obtains s1' s2' ξ' where "s1 ⊑ s1'" "s2 ⊑ s2'" "ξ ⊑⇩m ξ'" "t = App s1' s2' ξ'"
  using assms by (cases rule: compl.cases) auto

lemma compl_Lam_leftE:
  assumes "Lam x ζ s ξ ⊑ t"
  obtains s' ζ' ξ' where "s ⊑ s'" "ζ ⊑⇩m ζ'" "ξ ⊑⇩m ξ'" "t = Lam x ζ' s' ξ'"
  using assms by (cases rule: compl.cases) auto

lemma compl_Vr_rightE:
  assumes "t ⊑ Vr x ξ"
  obtains ξ' where "ξ' ⊑⇩m ξ" "t = Vr x ξ'"
  using assms by (cases rule: compl.cases) auto

lemma compl_Ct_rightE:
  assumes "t ⊑ Ct c ξ"
  obtains ξ' where "ξ' ⊑⇩m ξ" "t = Ct c ξ'"
  using assms by (cases rule: compl.cases) auto

lemma compl_App_rightE:
  assumes "t ⊑ App s1 s2 ξ"
  obtains s1' s2' ξ' where "s1' ⊑ s1" "s2' ⊑ s2" "ξ' ⊑⇩m ξ" "t = App s1' s2' ξ'"
  using assms by (cases rule: compl.cases) auto

lemma compl_Lam_rightE:
  assumes "t ⊑ Lam x ζ s ξ"
  obtains s' ζ' ξ' where "s' ⊑ s" "ζ' ⊑⇩m ζ" "ξ' ⊑⇩m ξ" "t = Lam x ζ' s' ξ'"
  using assms by (cases rule: compl.cases) auto

subsubsection ‹Basic properties›
lemma compl_refl[simp, intro]: "t ⊑ t"
  by (induction t) (auto intro: compl.intros)

lemma compl_poss_eq: "t ⊑ s ⟹ poss t = poss s"
  by (induction t s rule: compl.induct) auto

lemma compl_bvars_eq: "t ⊑ s ⟹ bvars t = bvars s"
  by (induction t s rule: compl.induct) auto

lemma compl_unambiguous: "t ⊑ s ⟹ unambiguous t = unambiguous s"
  by (induction t s rule: compl.induct) (auto simp: compl_bvars_eq)

lemma erase_compl[simp, intro]: "erase t ⊑ t"
  by (induction t) (auto intro: compl.intros)

lemma remove_annot_compl:
  assumes "p ∈ poss t"
  shows "remove_annot t p ⊑ t"
  using assms by (induction t arbitrary: p) (auto split: list.splits nat.splits intro: compl.intros)

lemma compl_trans: "⟦ s ⊑ t; t ⊑ u ⟧ ⟹ s ⊑ u"
  by (induction s t arbitrary: u rule: compl.induct)
    (auto elim!: compl_Vr_leftE compl_Ct_leftE compl_App_leftE compl_Lam_leftE 
      intro: compl.intros dest: mcompl_trans)

lemma compl_antisym: "⟦ s ⊑ t; t ⊑ s ⟧ ⟹ s = t"
  by (induction s t rule: compl.induct) (auto elim!: compl_Vr_rightE compl_Ct_rightE 
      compl_App_rightE compl_Lam_rightE dest: mcompl_antisym)

lemma compl_mtp_of_root: "t ⊑ s ⟹ mtp_of t [] ⊑⇩m mtp_of s []"
  by (erule compl.cases) auto

subsubsection ‹Positions and completions›

lemma compl_mtp_of:
  assumes "t ⊑ s"
  shows "mtp_of t p ⊑⇩m mtp_of s p"
  using assms
  by (induction t s arbitrary: p rule: compl.induct) (auto split: list.splits nat.splits)

text ‹\<^term>‹erase t ⊑ s› is preserved by \<^term>‹remove_annot› (erased term has \<^term>‹None› everywhere).›
lemma erase_compl_remove_annot:
  assumes "erase t ⊑ s"
  shows "erase t ⊑ remove_annot s p"
  using assms
proof (induction t arbitrary: s p)
  case (Vr x ξ)
  then show ?case by (auto elim!: compl_Vr_leftE intro: compl.intros)
next
  case (Ct c ξ)
  then show ?case by (auto elim!: compl_Ct_leftE intro: compl.intros)
next
  case (App t1 t2 ξ)
  from App.prems(1) obtain s1 s2 ξs where seq: "s = App s1 s2 ξs"
    "erase t1 ⊑ s1" "erase t2 ⊑ s2"
    by (auto elim!: compl_App_leftE)
  show ?case using App.prems seq
    by (cases p) (auto split: nat.splits intro: compl.intros App.IH)
next
  case (Lam x ξ t ζ)
  from Lam.prems(1) obtain s0 ζs ξs where seq: "s = Lam x ζs s0 ξs"
    "erase t ⊑ s0"
    by (auto elim!: compl_Lam_leftE)
  show ?case using Lam.prems seq
    by (cases p) (auto split: nat.splits list.splits intro: compl.intros Lam.IH)
qed

text ‹
  Same shape extensionality: If \<^term>‹t ⊑ u› and \<^term>‹t ⊑ u'›, and \<^term>‹u›, \<^term>‹u'› are F-terms 
  with the same type at every position, then \<^term>‹u = u'›.
›

lemma fterm_extensionality:
  assumes "t ⊑ u" "t ⊑ u'" "fterm u" "fterm u'" "⋀p. p ∈ poss t ⟹ mtp_of u p = mtp_of u' p"
  shows "u = u'"
  using assms
proof (induction t arbitrary: u u')
  case (Vr x ξ)
  from Vr.prems(1) obtain ξu where "u = Vr x ξu" by (auto elim!: compl_Vr_leftE)
  moreover from Vr.prems(2) obtain ξu' where "u' = Vr x ξu'" by (auto elim!: compl_Vr_leftE)
  ultimately show "u = u'" using Vr.prems(5)[of "[]"] by auto
next
  case (Ct c ξ)
  from Ct.prems(1) obtain ξu where "u = Ct c ξu" by (auto elim!: compl_Ct_leftE)
  moreover from Ct.prems(2) obtain ξu' where "u' = Ct c ξu'" by (auto elim!: compl_Ct_leftE)
  ultimately show "u = u'" using Ct.prems(5)[of "[]"] by auto
next
  case (App t1 t2 ξ)
  from App.prems(1) obtain u1 u2 ξu where ueq: "u = App u1 u2 ξu"
    "t1 ⊑ u1" "t2 ⊑ u2" by (auto elim!: compl_App_leftE)
  from App.prems(2) obtain u1' u2' ξu' where u'eq: "u' = App u1' u2' ξu'"
    "t1 ⊑ u1'" "t2 ⊑ u2'" by (auto elim!: compl_App_leftE)
  have fu: "fterm u1" "fterm u2" using App.prems(3) ueq(1) by auto
  have fu': "fterm u1'" "fterm u2'" using App.prems(4) u'eq(1) by auto
  have eq1: "⋀p. p ∈ poss t1 ⟹ mtp_of u1 p = mtp_of u1' p"
  proof -
    fix p assume "p ∈ poss t1"
    then have "Suc 0 # p ∈ poss (App t1 t2 ξ)" by auto
    from App.prems(5)[OF this] ueq(1) u'eq(1) show "mtp_of u1 p = mtp_of u1' p" by auto
  qed
  have eq2: "⋀p. p ∈ poss t2 ⟹ mtp_of u2 p = mtp_of u2' p"
  proof -
    fix p assume "p ∈ poss t2"
    then have "2 # p ∈ poss (App t1 t2 ξ)" by auto
    from App.prems(5)[OF this] ueq(1) u'eq(1) show "mtp_of u2 p = mtp_of u2' p" by auto
  qed
  have "u1 = u1'" using App.IH(1)[OF ueq(2) u'eq(2) fu(1) fu'(1) eq1] .
  moreover have "u2 = u2'" using App.IH(2)[OF ueq(3) u'eq(3) fu(2) fu'(2) eq2] .
  moreover have "ξu = ξu'" using App.prems(5)[of "[]"] ueq(1) u'eq(1) by auto
  ultimately show "u = u'" using ueq(1) u'eq(1) by auto
next
  case (Lam x ξ t ζ)
  from Lam.prems(1) obtain u0 ζu ξu where ueq: "u = Lam x ζu u0 ξu"
    "t ⊑ u0" by (auto elim!: compl_Lam_leftE)
  from Lam.prems(2) obtain u0' ζu' ξu' where u'eq: "u' = Lam x ζu' u0' ξu'"
    "t ⊑ u0'" by (auto elim!: compl_Lam_leftE)
  have fu: "fterm u0" using Lam.prems(3) ueq(1) by auto
  have fu': "fterm u0'" using Lam.prems(4) u'eq(1) by auto
  have eq0: "⋀p. p ∈ poss t ⟹ mtp_of u0 p = mtp_of u0' p"
  proof -
    fix p assume "p ∈ poss t"
    then have "2 # p ∈ poss (Lam x ξ t ζ)" by auto
    from Lam.prems(5)[OF this] ueq(1) u'eq(1) show "mtp_of u0 p = mtp_of u0' p" by auto
  qed
  have "u0 = u0'" using Lam.IH[OF ueq(2) u'eq(2) fu fu' eq0] .
  moreover have "ζu = ζu'" using Lam.prems(5)[of "[Suc 0]"] ueq(1) u'eq(1) by auto
  moreover have "ξu = ξu'" using Lam.prems(5)[of "[]"] ueq(1) u'eq(1) by auto
  ultimately show "u = u'" using ueq(1) u'eq(1) by auto
qed

text ‹
  The crucial fact for completeness:
  If \<^term>‹t ⊑ u› and \<^term>‹u› is an instance of \<^term>‹v› (\<^term>‹u ≤ v›), 
  and every type variable of \<^term>‹v› is "witnessed" at some
  non-bot position of t, then \<^term>‹u› is the unique F-term \<^term>‹u'› with \<^term>‹t ⊑ u'› and \<^term>‹u' ≤ v›.
›

theorem crucial_uniqueness:
  assumes compl_u: "t ⊑ u" and fu: "fterm u"
    and inst_u: "∃ρ. u = subst_trm ρ v" and fv: "fterm v"
    and cover: "∀α ∈ tvars_trm v. ∃p ∈ poss v. α ∈ tvars_mty (mtp_of v p) ∧ mtp_of t p ≠ None"
    and compl_u': "t ⊑ u'" and fu': "fterm u'"
    and inst_u': "∃ρ'. u' = subst_trm ρ' v"
  shows "u = u'"
proof -
  from inst_u obtain ρ where u_eq: "u = subst_trm ρ v" by auto
  from inst_u' obtain ρ' where u'_eq: "u' = subst_trm ρ' v" by auto
  text ‹By @{thm fterm_extensionality}, suffices to show \<^term>‹∀p ∈ poss t. mtp_of u p = mtp_of u' p›.›
  have poss_eq: "poss t = poss v"
    using compl_poss_eq[OF compl_u] u_eq by simp
  show "u = u'"
  proof (rule fterm_extensionality[OF compl_u compl_u' fu fu'])
    fix p assume p_in: "p ∈ poss t"
    then have pv: "p ∈ poss v" using poss_eq by auto
    have u_mtp: "mtp_of u p = subst_mty ρ (mtp_of v p)"
      using mtp_of_subst[OF pv] u_eq by auto
    have u'_mtp: "mtp_of u' p = subst_mty ρ' (mtp_of v p)"
      using mtp_of_subst[OF pv] u'_eq by auto
    text ‹Since v is an F-term, \<^term>‹∃σ. mtp_of v p = Some σ›.›
    have "∃σ. mtp_of v p = Some σ" using fterm_mtp_of_Some[OF fv pv] .
    then obtain σ where vsig: "mtp_of v p = Some σ" by auto
    text ‹Need to show \<^term>‹subst_ty ρ σ = subst_ty ρ' σ›.
      By @{thm subst_ty_agree}, suffices to show \<^term>‹∀α ∈ tvars_ty σ. ρ α = ρ' α›.›
    have "subst_ty ρ σ = subst_ty ρ' σ"
    proof (rule subst_ty_cong)
      fix α assume alpha_in: "α ∈ tvars_ty σ"
      then have "α ∈ tvars_trm v"
        using vsig pv tvars_trm_eq_UN_mtp by fastforce
      from cover[rule_format, OF this]
      obtain q where qv: "q ∈ poss v" and alpha_q: "α ∈ tvars_mty (mtp_of v q)"
        and t_q: "mtp_of t q ≠ None" by auto
      have qt: "q ∈ poss t" using poss_eq qv by auto
      text ‹Since \<^term>‹mtp_of t q› is not \<^term>‹None› and \<^term>‹t ⊑ u›, \<^term>‹u'›, 
        the annotation is preserved.›
      have "mtp_of t q ⊑⇩m mtp_of u q" using compl_mtp_of[OF compl_u] .
      moreover have "mtp_of t q ⊑⇩m mtp_of u' q" using compl_mtp_of[OF compl_u'] .
      ultimately have eq_at_q: "mtp_of u q = mtp_of t q ∧ mtp_of u' q = mtp_of t q"
        using t_q by (auto simp: mcompl_def)
      then have "mtp_of u q = mtp_of u' q" by simp
      text ‹Now use @{thm mtp_of_subst} to relate to substitutions.›
      have "subst_mty ρ (mtp_of v q) = subst_mty ρ' (mtp_of v q)"
        using ‹mtp_of u q = mtp_of u' q› mtp_of_subst[OF qv] u_eq u'_eq by auto
      then show "ρ α = ρ' α" using alpha_q
        by (cases "mtp_of v q") (auto simp: subst_ty_agree)
    qed
    then show "mtp_of u p = mtp_of u' p" using u_mtp u'_mtp vsig by simp
  qed
qed

text ‹Strict \<^term>‹(⊑)› witnesses a position difference.›
lemma compl_strict_witness:
  assumes "s' ⊑ s" "s' ≠ s"
  shows "∃p ∈ poss s. mtp_of s' p = None ∧ mtp_of s p ≠ None"
  using assms
proof (induction s' s rule: compl.induct)
  case (compl_App s1 s1' s2 s2' ξ ξ')
  show ?case
  proof (cases "s1 = s1'")
    case True
    then show ?thesis
    proof (cases "s2 = s2'")
      case True
      with ‹s1 = s1'› compl_App.prems compl_App.hyps
      show ?thesis by (auto simp: mcompl_def)
    next
      case False
      with compl_App.IH(2) obtain p where "p ∈ poss s2'" "mtp_of s2 p = None" "mtp_of s2' p ≠ None"
        by auto
      then show ?thesis by (intro bexI[of _ "2 # _"]) auto
    qed
  next
    case False
    with compl_App.IH(1) obtain p where "p ∈ poss s1'" "mtp_of s1 p = None" "mtp_of s1' p ≠ None"
      by auto
    then show ?thesis by (intro bexI[of _ "Suc 0 # p"]) auto
  qed
next
  case (compl_Lam ζ ζ' t t' ξ ξ' x)
  show ?case
  proof (cases "t = t'")
    case True
    then show ?thesis
    proof (cases "ζ = ζ'")
      case True
      with ‹t = t'› compl_Lam.prems compl_Lam.hyps
      show ?thesis by (auto simp: mcompl_def)
    next
      case False
      with compl_Lam.hyps show ?thesis
        by (auto simp: mcompl_def intro!: bexI[of _ "[Suc 0]"])
    qed
  next
    case False
    with compl_Lam.IH obtain p where "p ∈ poss t'" "mtp_of t p = None" "mtp_of t' p ≠ None"
      by auto
    then show ?thesis by auto
  qed
qed (auto simp: mcompl_def)

text ‹Multiple completions from agreeing substitutions.›
lemma multiple_compl:
  assumes "s ⊑ subst_trm ρ v"
    "⋀α p. ⟦ p ∈ poss v; α ∈ tvars_mty (mtp_of v p); mtp_of s p ≠ None ⟧ ⟹ ρ α = ρ' α"
  shows "s ⊑ subst_trm ρ' v"
  using assms
proof (induction v arbitrary: s)
  case (Vr x ξ)
  show ?case
  proof (cases ξ)
    case None then show ?thesis using Vr by (auto elim!: compl_Vr_rightE intro: compl.intros)
  next
    case (Some σ)
    from Vr.prems(1) Some obtain ξs where seq: "s = Vr x ξs" "ξs ⊑⇩m Some (subst_ty ρ σ)"
      by (auto elim!: compl_Vr_rightE)
    show ?thesis
    proof (cases "ξs")
      case None then show ?thesis using seq(1) Some by (auto intro: compl.intros)
    next
      case (Some τ)
      then have "τ = subst_ty ρ σ" using seq(2) by (auto simp: mcompl_def)
      moreover have "∀α∈tvars_ty σ. ρ α = ρ' α"
        using Vr.prems(2)[of "[]"] seq(1) Some ‹ξ = Some σ› by auto
      then have "subst_ty ρ σ = subst_ty ρ' σ" by (intro subst_ty_cong) auto
      ultimately have "τ = subst_ty ρ' σ" by simp
      then show ?thesis using seq(1) Some ‹ξ = Some σ› by (auto intro: compl.intros simp: mcompl_def)
    qed
  qed
next
  case (Ct c ξ)
  then show ?case
  proof (cases ξ)
    case None then show ?thesis using Ct by (auto elim!: compl_Ct_rightE intro: compl.intros)
  next
    case (Some σ)
    from Ct.prems(1) Some obtain ξs where seq: "s = Ct c ξs" "ξs ⊑⇩m Some (subst_ty ρ σ)"
      by (auto elim!: compl_Ct_rightE)
    show ?thesis
    proof (cases "ξs")
      case None then show ?thesis using seq(1) Some by (auto intro: compl.intros)
    next
      case (Some τ)
      then have "τ = subst_ty ρ σ" using seq(2) by (auto simp: mcompl_def)
      moreover have "∀α∈tvars_ty σ. ρ α = ρ' α"
        using Ct.prems(2)[of "[]"] seq(1) Some ‹ξ = Some σ› by auto
      then have "subst_ty ρ σ = subst_ty ρ' σ" by (intro subst_ty_cong) auto
      ultimately have "τ = subst_ty ρ' σ" by simp
      then show ?thesis using seq(1) Some ‹ξ = Some σ› by (auto intro: compl.intros simp: mcompl_def)
    qed
  qed
next
  case (App t1 t2 ξ)
  from App.prems(1) obtain s1 s2 ξs where seq: "s = App s1 s2 ξs"
    "s1 ⊑ subst_trm ρ t1" "s2 ⊑ subst_trm ρ t2" "ξs ⊑⇩m subst_mty ρ ξ"
    by (auto elim!: compl_App_rightE)
  have "s1 ⊑ subst_trm ρ' t1"
  proof (rule App.IH(1)[OF seq(2)])
    fix α p assume "p ∈ poss t1" "α ∈ tvars_mty (mtp_of t1 p)" "mtp_of s1 p ≠ None"
    then show "ρ α = ρ' α" using App.prems(2)[of "Suc 0 # p" α] seq(1) by auto
  qed
  moreover have "s2 ⊑ subst_trm ρ' t2"
  proof (rule App.IH(2)[OF seq(3)])
    fix α p assume "p ∈ poss t2" "α ∈ tvars_mty (mtp_of t2 p)" "mtp_of s2 p ≠ None"
    then show "ρ α = ρ' α" using App.prems(2)[of "2 # p" α] seq(1) by auto
  qed
  moreover have "ξs ⊑⇩m subst_mty ρ' ξ"
  proof (cases ξ)
    case None then show ?thesis using seq(4) by auto
  next
    case (Some σ)
    show ?thesis
    proof (cases ξs)
      case None then show ?thesis by auto
    next
      case (Some τ)
      then have "τ = subst_ty ρ σ" using seq(4) ‹ξ = Some σ› by (auto simp: mcompl_def)
      moreover have "∀α ∈ tvars_ty σ. ρ α = ρ' α"
        using App.prems(2)[of "[]"] seq(1) Some ‹ξ = Some σ› by auto
      then have "subst_ty ρ σ = subst_ty ρ' σ" by (intro subst_ty_cong) auto
      ultimately show ?thesis using Some ‹ξ = Some σ› by (auto simp: mcompl_def)
    qed
  qed
  ultimately show ?case using seq(1) by (auto intro: compl.intros)
next
  case (Lam x ξ t ζ)
  from Lam.prems(1) obtain s0 ζs ξs where
    seq: "s = Lam x ζs s0 ξs"
    "s0 ⊑ subst_trm ρ t" "ζs ⊑⇩m subst_mty ρ ξ" "ξs ⊑⇩m subst_mty ρ ζ"
    by (auto elim!: compl_Lam_rightE)
  have "s0 ⊑ subst_trm ρ' t"
  proof (rule Lam.IH[OF seq(2)])
    fix α p assume "p ∈ poss t" "α ∈ tvars_mty (mtp_of t p)" "mtp_of s0 p ≠ None"
    then show "ρ α = ρ' α" using Lam.prems(2)[of "2 # p" α] seq(1) by auto
  qed
  moreover have "ζs ⊑⇩m subst_mty ρ' ξ"
  proof (cases ξ)
    case None then show ?thesis using seq(3) by auto
  next
    case (Some σ)
    show ?thesis
    proof (cases "ζs")
      case None then show ?thesis by auto
    next
      case (Some τ)
      then have "τ = subst_ty ρ σ" using seq(3) ‹ξ = Some σ› by (auto simp: mcompl_def)
    have "∀α' ∈ tvars_ty σ. ρ α' = ρ' α'"
    proof (intro ballI)
      fix α' assume "α' ∈ tvars_ty σ"
      then show "ρ α' = ρ' α'"
        using Lam.prems(2)[of "[Suc 0]" α'] ‹ξ = Some σ› seq(1) Some by auto
    qed
    then have eq: "subst_ty ρ σ = subst_ty ρ' σ" by (intro subst_ty_cong) auto
    from ‹τ = subst_ty ρ σ› eq have "τ = subst_ty ρ' σ" by simp
    then show ?thesis using Some ‹ξ = Some σ› by (auto simp: mcompl_def)
    qed
  qed
  moreover have "ξs ⊑⇩m subst_mty ρ' ζ"
  proof (cases ζ)
    case None then show ?thesis using seq(4) by auto
  next
    case (Some σ)
    show ?thesis
    proof (cases "ξs")
      case None then show ?thesis by auto
    next
      case (Some τ)
      then have "τ = subst_ty ρ σ" using seq(4) ‹ζ = Some σ› by (auto simp: mcompl_def)
      moreover have "∀α ∈ tvars_ty σ. ρ α = ρ' α"
        using Lam.prems(2)[of "[]"] seq(1) Some ‹ζ = Some σ› by auto
      then have "subst_ty ρ σ = subst_ty ρ' σ" by (intro subst_ty_cong) auto
      ultimately show ?thesis using Some ‹ζ = Some σ› by (auto simp: mcompl_def)
    qed
  qed
  ultimately show ?case using seq(1) by (auto intro: compl.intros)
qed

subsubsection ‹Well-typedness and type inference›

text ‹
  Well-typedness predicate on F-terms.
  We work in a locale fixing the constant-typing function \<^term>‹ctpOf›.
  We also use the abbreviation \<^term>‹tpOf› for the type of an F-term.
›

abbreviation tpOf :: "('tv,'k,'v,'c) trm ⇒ nat list ⇒ ('tv,'k) ty" where
  "tpOf u p ≡ the (mtp_of u p)"

abbreviation tpOfR :: "('tv,'k,'v,'c) trm ⇒ ('tv,'k) ty" where
  "tpOfR u ≡ the (mtp_of u [])"

text ‹Free typed variables of a term: pairs \<^term>‹(x, σ)› where variable \<^term>‹x›
  occurs free with type annotation \<^term>‹Some σ›.›

fun fvars :: "('tv,'k,'v,'c) trm ⇒ ('v × ('tv,'k) ty) set" where
  "fvars (Vr x (Some σ)) = {(x, σ)}"
| "fvars (Vr x None) = {}"
| "fvars (Ct c ξ) = {}"
| "fvars (App t1 t2 ξ) = fvars t1 ∪ fvars t2"
| "fvars (Lam x ξ t ζ) = {(y, σ) ∈ fvars t. y ≠ x}"

lemma fvars_subst: "fvars (subst_trm ρ t) = (λ(x, σ). (x, subst_ty ρ σ)) ` fvars t"
proof (induction t)
  case (Vr x ξ) then show ?case by (cases ξ) auto
next
  case (Ct c ξ) then show ?case by auto
next
  case (App t1 t2 ξ) then show ?case by auto
next
  case (Lam x ξ t ζ) then show ?case by auto
qed

locale signature =
  fixes ctpOf :: "'c ⇒ ('tv,'k) ty"
begin

inductive wt :: "('tv,'k,'v,'c) trm ⇒ bool" ("⊢ _" [50] 50) where
  wt_Vr: "⊢ Vr x (Some σ)"
| wt_Ct: "∃ρ. σ = subst_ty ρ (ctpOf c) ⟹ ⊢ Ct c (Some σ)"
| wt_App: "⟦ ⊢ u; ⊢ v; tpOfR u = Arrow (tpOfR v) σ ⟧ ⟹ ⊢ App u v (Some σ)"
| wt_Lam: "⟦ ⊢ u; ∀τ. (x, τ) ∈ fvars u ⟶ τ = σ ⟧ ⟹ ⊢ Lam x (Some σ) u (Some (Arrow σ (tpOfR u)))"

text ‹Inversion rules for \<^const>‹wt›.›

lemma wt_Vr_inv: "⊢ Vr x ξ ⟹ ∃σ. ξ = Some σ"
  by (erule wt.cases) auto

lemma wt_Ct_inv: "⊢ Ct c (Some σ) ⟹ ∃ρ. σ = subst_ty ρ (ctpOf c)"
  by (erule wt.cases) auto

lemma wt_App_inv: "⊢ App t1 t2 (Some σ) ⟹ ⊢ t1 ∧ ⊢ t2 ∧ tpOfR t1 = Arrow (tpOfR t2) σ"
  by (erule wt.cases) auto

lemma wt_Lam_inv: "⊢ Lam x (Some σ) t (Some τ) ⟹ ⊢ t ∧ τ = Arrow σ (tpOfR t)"
  by (erule wt.cases) auto

lemma wt_App_invE:
  assumes "⊢ App u1 u2 ξ"
  obtains σ where "⊢ u1" "⊢ u2" "ξ = Some σ" "tpOfR u1 = Arrow (tpOfR u2) σ"
  using assms by (auto elim: wt.cases)

lemma wt_Lam_invE:
  assumes "⊢ Lam x ξ u ζ"
  obtains σ where "⊢ u" "ξ = Some σ" "ζ = Some (Arrow σ (tpOfR u))"
    "∀τ. (x, τ) ∈ fvars u ⟶ τ = σ"
  using assms by (auto elim: wt.cases)

lemma wt_fterm: "⊢ u ⟹ fterm u"
  by (induction u rule: wt.induct) auto


text ‹Substitution lemma for well-typedness.
  Since @{thm wt_Vr} has no conditions, any type substitution preserves \<^term>‹wt›.›
lemma subst_wt:
  assumes "⊢ v"
  shows "⊢ subst_trm ρ v"
  using assms
proof (induction v rule: wt.induct)
  case (wt_Vr x σ)
  show ?case by (simp, rule wt.wt_Vr)
next
  case (wt_Ct σ c)
  then obtain ρ0 where "σ = subst_ty ρ0 (ctpOf c)" by auto
  then have "subst_ty ρ σ = subst_ty (ρ ∘∘ ρ0) (ctpOf c)"
    by (simp add: subst_ty_comp)
  then show ?case by (simp, intro wt.wt_Ct, auto)
next
  case (wt_App u v σ)
  from wt_App have fu: "fterm u" "fterm v" by (auto dest: wt_fterm)
  then obtain τ1 τ2 where "mtp_of u [] = Some τ1" "mtp_of v [] = Some τ2"
    using fterm_mtp_of_Some by (metis nil_in_poss)
  with wt_App have tp: "tpOfR (subst_trm ρ u) = Arrow (tpOfR (subst_trm ρ v)) (subst_ty ρ σ)"
    by (simp add: mtp_of_subst[of "[]" u ρ, simplified] mtp_of_subst[of "[]" v ρ, simplified])
  from wt_App tp show ?case by (simp, intro wt.wt_App) auto
next
  case (wt_Lam u x σ)
  from wt_Lam have fu: "fterm u" by (auto dest: wt_fterm)
  then obtain τ where mt: "mtp_of u [] = Some τ"
    using fterm_mtp_of_Some by (metis nil_in_poss)
  from wt_Lam mt show ?case
  proof -
    have eq: "mtp_of (subst_trm ρ u) [] = Some (subst_ty ρ τ)"
      using mt by (simp add: mtp_of_subst[of "[]" u ρ, simplified])
    have tpR: "tpOfR (subst_trm ρ u) = subst_ty ρ τ" using eq by simp
    have tpU: "tpOfR u = τ" using mt by simp
    have fv_cond: "∀τ'. (x, τ') ∈ fvars (subst_trm ρ u) ⟶ τ' = subst_ty ρ σ"
      using wt_Lam(2) by (auto simp: fvars_subst)
    from wt_Lam have "⊢ Lam x (Some (subst_ty ρ σ)) (subst_trm ρ u)
      (Some (Arrow (subst_ty ρ σ) (tpOfR (subst_trm ρ u))))"
      by (intro wt.wt_Lam) (use fv_cond in auto)
    then show ?thesis using tpR tpU by simp
  qed
qed

text ‹
  If \<^term>‹t› is a typeable unambiguous C-term, then its well-typed completion
  is unique (there is exactly one F-term \<^term>‹u› such that \<^term>‹t ⊑ u› and \<^term>‹wt u›).
›

lemma cterm_unique_completion:
  assumes "cterm t" "unambiguous t"
    "t ⊑ u" "⊢ u" "t ⊑ v" "⊢ v"
  shows "u = v"
  using assms
proof (induction t arbitrary: u v)
  case (Vr x ξ)
  then show ?case by (auto elim!: compl_Vr_leftE simp: mcompl_def)
next
  case (Ct c ξ)
  then show ?case by (auto elim!: compl_Ct_leftE simp: mcompl_def)
next
  case (App t1 t2 ξ)
  from App.prems have ct1: "cterm t1" "cterm t2" "ξ = None" by auto
  from App.prems have ua1: "unambiguous t1" "unambiguous t2" by auto
  from App.prems(3) obtain u1 u2 ξu where ueq: "u = App u1 u2 ξu"
    "t1 ⊑ u1" "t2 ⊑ u2" "ξ ⊑⇩m ξu"
    by (auto elim!: compl_App_leftE)
  from App.prems(5) obtain v1 v2 ξv where veq: "v = App v1 v2 ξv"
    "t1 ⊑ v1" "t2 ⊑ v2" "ξ ⊑⇩m ξv"
    by (auto elim!: compl_App_leftE)
  from App.prems(4) ueq(1) obtain σu where
    wtu: "⊢ u1" "⊢ u2" and xiu: "ξu = Some σu" and
    tpu: "tpOfR u1 = Arrow (tpOfR u2) σu"
    by (auto elim!: wt_App_invE)
  from App.prems(6) veq(1) obtain σv where
    wtv: "⊢ v1" "⊢ v2" and xiv: "ξv = Some σv" and
    tpv: "tpOfR v1 = Arrow (tpOfR v2) σv"
    by (auto elim!: wt_App_invE)
  have "u1 = v1" using App.IH(1)[OF ct1(1) ua1(1) ueq(2) wtu(1) veq(2) wtv(1)] .
  moreover have "u2 = v2" using App.IH(2)[OF ct1(2) ua1(2) ueq(3) wtu(2) veq(3) wtv(2)] .
  ultimately have "σu = σv" using tpu tpv by simp
  with ueq(1) veq(1) ‹u1 = v1› ‹u2 = v2› xiu xiv show "u = v" by simp
next
  case (Lam x ξ t ζ)
  from Lam.prems have ct: "cterm t" "ξ ≠ None" "ζ = None" by auto
  from Lam.prems have ua: "unambiguous t" by auto
  obtain σ where sig: "ξ = Some σ" using ct(2) by (cases ξ) auto
  from Lam.prems(3) sig obtain u' ξu where ueq: "u = Lam x (Some σ) u' ξu"
    "t ⊑ u'"
    by (auto elim!: compl_Lam_leftE simp: mcompl_def)
  from Lam.prems(5) sig obtain v' ξv where veq: "v = Lam x (Some σ) v' ξv"
    "t ⊑ v'"
    by (auto elim!: compl_Lam_leftE simp: mcompl_def)
  from Lam.prems(4) ueq(1) obtain τu where
    wtu: "⊢ u'" and xiusig: "Some σ = Some σ" and xiu: "ξu = Some (Arrow σ (tpOfR u'))"
    by (auto elim!: wt_Lam_invE)
  from Lam.prems(6) veq(1) obtain τv where
    wtv: "⊢ v'" and xivsig: "Some σ = Some σ" and xiv: "ξv = Some (Arrow σ (tpOfR v'))"
    by (auto elim!: wt_Lam_invE)
  have "u' = v'" using Lam.IH[OF ct(1) ua ueq(2) wtu veq(2) wtv] .
  with ueq veq xiu xiv show "u = v" by simp
qed

subsubsection ‹Well-Typed Completions›
definition is_wt_completion :: "('tv,'k,'v,'c) trm ⇒ ('tv,'k,'v,'c) trm ⇒ bool" where
  "is_wt_completion t u ⟷ t ⊑ u ∧ fterm u ∧ ⊢ u"

definition is_mgen :: "('tv,'k,'v,'c) trm ⇒ ('tv,'k,'v,'c) trm ⇒ bool" where
  "is_mgen t v ⟷ is_wt_completion t v ∧
    (∀u. is_wt_completion t u ⟶ (∃ρ. u = subst_trm ρ v))"

definition typeable :: "('tv,'k,'v,'c) trm ⇒ bool" where
  "typeable t ⟷ (∃u. is_wt_completion t u)"

end

text ‹
  We work in an extended locale that assumes the existence of \<^term>‹is_mgen›: 
  For any typeable unambiguous term, there exists a most general well-typed completion.
›

locale signature_with_mgen = signature ctpOf
  for ctpOf :: "'c ⇒ ('tv,'k) ty" +
  assumes mgen_exists:
    "⟦ typeable (t::('tv,'k,'v,'c) trm); unambiguous t ⟧ ⟹ ∃v. is_mgen t v" and
    tyvars_inf: "infinite (UNIV :: 'tv set)"
begin

definition mgen :: "('tv,'k,'v,'c) trm ⇒ ('tv,'k,'v,'c) trm" where
  "mgen t = (SOME v. is_mgen t v)"

lemma mgen_is_mgen:
  assumes "typeable t" "unambiguous t"
  shows "is_mgen t (mgen t)"
proof -
  from assms have "∃v. is_mgen t v"
    by (intro mgen_exists)
  then show ?thesis unfolding mgen_def by (rule someI_ex)
qed

lemma mgen_compl:
  assumes "typeable t" "unambiguous t"
  shows "t ⊑ mgen t"
  using mgen_is_mgen[OF assms] by (auto simp: is_mgen_def is_wt_completion_def)

lemma mgen_fterm:
  assumes "typeable t" "unambiguous t"
  shows "fterm (mgen t)"
  using mgen_is_mgen[OF assms] by (auto simp: is_mgen_def is_wt_completion_def)

lemma mgen_wt:
  assumes "typeable t" "unambiguous t"
  shows "⊢ mgen t"
  using mgen_is_mgen[OF assms] by (auto simp: is_mgen_def is_wt_completion_def)

lemma mgen_most_general:
  assumes "typeable t" "unambiguous t" "is_wt_completion t u"
  shows "∃ρ. u = subst_trm ρ (mgen t)"
  using mgen_is_mgen[OF assms(1,2)] assms(3) by (auto simp: is_mgen_def)

subsection ‹Correct Printings›

text ‹A correct printing of a typable unambiguous C-term \<^term>‹t› is a term \<^term>‹s› such that 
  \<^term>‹mgen t› is the unique most general well-typed completion of \<^term>‹s›:›
definition ‹correct_printing t s ⟷ (∀t'. is_mgen s t' ⟷ t' = mgen t)›

definition ‹strong_correct_printing t s ⟷ (∀t'. is_wt_completion s t' ⟷ t' = mgen t)›


text ‹Extra tyvars yield distinct most general completions.›
lemma two_mgen:
  assumes ua: "unambiguous s" and mg: "is_mgen s v" and extra: "tvars_trm v - tvars_trm s ≠ {}"
  shows "∃v'. v' ≠ v ∧ is_mgen s v'"
proof -
  from mg have sv: "s ⊑ v" and fv: "fterm v" and wtv: "⊢ v"
    and mg_prop: "⋀u. is_wt_completion s u ⟹ ∃ρ. u = subst_trm ρ v"
    by (auto simp: is_mgen_def is_wt_completion_def)
  from extra obtain α where alpha_v: "α ∈ tvars_trm v" and alpha_ns: "α ∉ tvars_trm s" by auto
  text ‹Property (a): \<^term>‹α› only appears at \<^term>‹None› positions of \<^term>‹s›.›
  have prop_a: "mtp_of s p = None" if "p ∈ poss v" "α ∈ tvars_mty (mtp_of v p)" for p
  proof (rule ccontr)
    assume "mtp_of s p ≠ None"
    have "p ∈ poss s" using that(1) compl_poss_eq[OF sv] by simp
    have "mtp_of s p ⊑⇩m mtp_of v p" using compl_mtp_of[OF sv] .
    then have "mtp_of s p = mtp_of v p" using ‹mtp_of s p ≠ None› by (auto simp: mcompl_def)
    then have "α ∈ tvars_mty (mtp_of s p)" using that(2) by simp
    then have "α ∈ tvars_trm s" using tvars_trm_eq_UN_mtp ‹p ∈ poss s› by fastforce
    with alpha_ns show False by contradiction
  qed
  obtain β where beta_nv: "β ∉ tvars_trm v"
    using ex_new_if_finite[OF tyvars_inf tvars_trm_finite[of v]] by blast
  define v' where "v' = subst_trm (single_subst (TyVar β) α) v"
  text ‹v != v'.›
  have v_neq: "v ≠ v'"
  proof
    assume "v = v'"
    then have "subst_trm (single_subst (TyVar β) α) v = v" by (simp add: v'_def)
    then have "single_subst (TyVar β) α α = TyVar α"
      using subst_trm_id_on_tvars[of "single_subst (TyVar β) α" v α] alpha_v by simp
    then show False using beta_nv alpha_v by simp
  qed
  have wtv': "⊢ v'" unfolding v'_def using subst_wt[OF wtv] .
  have fv': "fterm v'" unfolding v'_def using fv by (induction v) auto
  text ‹\<^term>‹s ⊑ v'› using @{thm multiple_compl}.›
  have sv': "s ⊑ v'"
  proof -
    have "s ⊑ subst_trm TyVar v" using sv by simp
    then show "s ⊑ v'" unfolding v'_def
    proof (rule multiple_compl)
      fix α' p assume "p ∈ poss v" "α' ∈ tvars_mty (mtp_of v p)" "mtp_of s p ≠ None"
      then have "α ∉ tvars_mty (mtp_of v p)" using prop_a by auto
      then have "α' ≠ α" using ‹α' ∈ tvars_mty (mtp_of v p)› by auto
      then show "TyVar α' = single_subst (TyVar β) α α'" by (simp add: single_subst_def)
    qed
  qed
  text ‹\<^term>‹v'› is most general.›
  have "⋀u. is_wt_completion s u ⟹ ∃ρ. u = subst_trm ρ v'"
  proof -
    fix u assume "is_wt_completion s u"
    then obtain ρ where "u = subst_trm ρ v" using mg_prop by auto
    have "v = subst_trm (single_subst (TyVar α) β) v'"
      unfolding v'_def using subst_trm_swap[OF beta_nv] by simp
    then have "u = subst_trm (ρ ∘∘ single_subst (TyVar α) β) v'"
      using ‹u = subst_trm ρ v› subst_trm_comp by metis
    then show "∃ρ. u = subst_trm ρ v'" by blast
  qed
  then have "is_mgen s v'"
    using sv' fv' wtv' by (auto simp: is_mgen_def is_wt_completion_def)
  with v_neq show ?thesis by auto
qed

text ‹Lift distinct completions to distinct most general completions.›
lemma lift_to_most_general:
  fixes s :: ‹('tv,'k,'v,'c) trm›
  assumes "unambiguous s" "is_wt_completion s u" "is_wt_completion s u'" "u ≠ u'"
  obtains v v' where ‹v ≠ v'› ‹is_mgen s v› ‹is_mgen s v'›
proof -
  have ty_s: "typeable s" using assms(2) by (auto simp: typeable_def)
  have mg: "is_mgen s (mgen s)" using mgen_is_mgen[OF ty_s assms(1)] .
  obtain ρ where u_eq: "u = subst_trm ρ (mgen s)"
    using mgen_most_general[OF ty_s assms(1,2)] by auto
  obtain ρ' where u'_eq: "u' = subst_trm ρ' (mgen s)"
    using mgen_most_general[OF ty_s assms(1,3)] by auto
  from assms(4) u_eq u'_eq have "∃α ∈ tvars_trm (mgen s). ρ α ≠ ρ' α"
    by (auto simp: subst_trm_agree)
  then obtain α where alpha_v: "α ∈ tvars_trm (mgen s)" and rho_neq: "ρ α ≠ ρ' α" by auto
  have sv: "s ⊑ mgen s" using mgen_compl[OF ty_s assms(1)] .
  have "α ∉ tvars_trm s"
  proof
    assume "α ∈ tvars_trm s"
    then obtain p where ps: "p ∈ poss s" and alpha_s: "α ∈ tvars_mty (mtp_of s p)"
      using tvars_trm_eq_UN_mtp by fastforce
    then have snone: "mtp_of s p ≠ None" by (cases "mtp_of s p") auto
    have pv: "p ∈ poss (mgen s)" using ps compl_poss_eq[OF sv] by simp
    have "mtp_of s p = mtp_of (mgen s) p"
      using compl_mtp_of[OF sv, of p] snone by (auto simp: mcompl_def)
    then have alpha_vp: "α ∈ tvars_mty (mtp_of (mgen s) p)" using alpha_s by simp
    have u_at: "mtp_of u p = subst_mty ρ (mtp_of (mgen s) p)"
      using mtp_of_subst[OF pv] u_eq by auto
    have u'_at: "mtp_of u' p = subst_mty ρ' (mtp_of (mgen s) p)"
      using mtp_of_subst[OF pv] u'_eq by auto
    have "s ⊑ u" using assms(2) by (auto simp: is_wt_completion_def)
    then have "mtp_of u p = mtp_of s p"
      using compl_mtp_of[of _ _ p] snone by (fastforce simp: mcompl_def)
    moreover have "s ⊑ u'" using assms(3) by (auto simp: is_wt_completion_def)
    then have "mtp_of u' p = mtp_of s p"
      using compl_mtp_of[of _ _ p] snone by (fastforce simp: mcompl_def)
    ultimately have "subst_mty ρ (mtp_of (mgen s) p) = subst_mty ρ' (mtp_of (mgen s) p)"
      using u_at u'_at by simp
    then have "ρ α = ρ' α" using alpha_vp
      by (cases "mtp_of (mgen s) p") (auto simp: subst_ty_agree)
    with rho_neq show False by contradiction
  qed
  with alpha_v have "tvars_trm (mgen s) - tvars_trm s ≠ {}" by auto
  from two_mgen[OF assms(1) mg this]
  obtain v' where "v' ≠ mgen s" "is_mgen s v'" by auto
  with mg that show ?thesis
    by auto
qed

corollary strong_correct_printing_iff:
  assumes ‹unambiguous s›
  shows ‹strong_correct_printing t s ⟷ correct_printing t s›
  using assms
  unfolding strong_correct_printing_def correct_printing_def
  using is_mgen_def typeable_def mgen_is_mgen[of s] lift_to_most_general[of s ‹mgen t›]
  by metis

subsection ‹The Algorithm›

text ‹
  The \<^term>‹test› predicate, \<^term>‹decrease› function, and the algorithm \<^term>‹smobla›.
  We work in a locale that also fixes a position-picking function \<^term>‹pickPos›.
›

definition non_bot_poss :: "('tv,'k,'v,'c) trm ⇒ nat list set" where
  "non_bot_poss s = {p ∈ poss s. mtp_of s p ≠ None}"

definition test :: "('tv,'k,'v,'c) trm ⇒ ('tv,'k,'v,'c) trm ⇒ nat list ⇒ bool" where
  "test v s p ⟷
    p ∈ poss s ∩ poss v ∧ mtp_of s p ≠ None ∧
    (∀α ∈ tvars_mty (mtp_of v p).
      ∃q ∈ poss s - {p}. α ∈ tvars_mty (mtp_of v q) ∧ mtp_of s q ≠ None)"

end

locale algorithm = signature_with_mgen ctpOf
  for ctpOf :: "'c ⇒ ('tv,'k) ty" +
  fixes pickPos :: "('tv,'k,'v,'c) trm ⇒ ('tv,'k,'v,'c) trm ⇒ nat list"
  assumes compat: "test v s p ⟹ test v s (pickPos v s)"
begin

function decrease :: "('tv,'k,'v,'c) trm ⇒ ('tv,'k,'v,'c) trm ⇒ ('tv,'k,'v,'c) trm" where
  "decrease v s = (if ∃p. test v s p
    then decrease v (remove_annot s (pickPos v s))
    else s)"
  by auto

termination
proof (relation "measure (λ(v, s). card (non_bot_poss s))")
  show "wf (measure (λ(v, s). card (non_bot_poss s)))" by simp
next
  fix v s :: "('tv,'k,'v,'c) trm"
  assume "∃p. test v s p"
  then obtain p0 where t0: "test v s p0" by auto
  then have t: "test v s (pickPos v s)" using compat by auto
  then have pp: "pickPos v s ∈ poss s" and nb: "mtp_of s (pickPos v s) ≠ None"
    by (auto simp: test_def)
  have rm: "mtp_of (remove_annot s (pickPos v s)) (pickPos v s) = None"
    using mtp_of_remove_self pp by auto
  have ps: "poss (remove_annot s (pickPos v s)) = poss s"
    using remove_annot_poss pp by auto
  have sub: "non_bot_poss (remove_annot s (pickPos v s)) ⊂ non_bot_poss s"
  proof (intro psubsetI subsetI)
    fix q assume q_in: "q ∈ non_bot_poss (remove_annot s (pickPos v s))"
    then have qp: "q ∈ poss s" and qnb: "mtp_of (remove_annot s (pickPos v s)) q ≠ None"
      by (auto simp: non_bot_poss_def ps)
    have "q ≠ pickPos v s" using qnb rm by auto
    then have "mtp_of s q ≠ None" using mtp_of_remove_other[OF pp _ ‹q ≠ pickPos v s›] qp qnb
      by (auto simp: compl_poss_eq)
    then show "q ∈ non_bot_poss s" using qp by (auto simp: non_bot_poss_def)
  next
    show "non_bot_poss (remove_annot s (pickPos v s)) ≠ non_bot_poss s"
    proof
      assume eq: "non_bot_poss (remove_annot s (pickPos v s)) = non_bot_poss s"
      have "pickPos v s ∈ non_bot_poss s" using pp nb by (auto simp: non_bot_poss_def)
      then have "pickPos v s ∈ non_bot_poss (remove_annot s (pickPos v s))" using eq by simp
      then show False using rm by (auto simp: non_bot_poss_def)
    qed
  qed
  then show "((v, remove_annot s (pickPos v s)), v, s)
    ∈ measure (λ(v, s). card (non_bot_poss s))"
    using psubset_card_mono[OF finite_subset[OF _ poss_finite[of s]]] 
      by (auto simp: non_bot_poss_def)
qed

lemmas decrease.simps[simp del]

definition smobla :: "('tv,'k,'v,'c) trm ⇒ ('tv,'k,'v,'c) trm" where
  "smobla t = decrease (mgen (erase t)) (mgen t)"

subsection ‹Completeness›

text ‹Auxiliary: decrease only removes annotations, so \<^term>‹decrease v s ⊑ s›.›
lemma decrease_compl:
  "decrease v s ⊑ s"
proof (induction v s rule: decrease.induct)
  case (1 v s)
  show ?case
    using compat compl_trans[OF 1 remove_annot_compl]
    by (force simp: test_def decrease.simps[of v s])
qed

text ‹Auxiliary: \<^term>‹erase t ⊑ decrease v s› if \<^term>‹erase t ⊑ s›.›
lemma erase_compl_decrease:
  "erase t ⊑ s ⟹ erase t ⊑ decrease v s"
proof (induction v s rule: decrease.induct)
  case (1 v s)
  show ?case
    using compat erase_compl_remove_annot[OF  1(2)]
    by (auto simp: test_def decrease.simps[of v s] intro: 1)
qed

text ‹The decrease invariant: coverage is preserved by \<^term>‹decrease›.›
lemma decrease_coverage:
  assumes "fterm v" "s ⊑ subst_trm ρ v"
    "∀α ∈ tvars_trm v. ∃p ∈ poss v. α ∈ tvars_mty (mtp_of v p) ∧ mtp_of s p ≠ None"
  shows "∀α ∈ tvars_trm v. ∃p ∈ poss v. α ∈ tvars_mty (mtp_of v p) ∧
    mtp_of (decrease v s) p ≠ None"
  using assms(2,3)
proof (induction v s rule: decrease.induct)
  case (1 v s)
  show ?case
  proof (cases "∃p. test v s p")
    case False
    then have "decrease v s = s" by (metis decrease.simps)
    with 1(3) show ?thesis by simp
  next
    case True
    then have t: "test v s (pickPos v s)" using compat by auto
    then have pp: "pickPos v s ∈ poss v" by (auto simp: test_def)
    have rm_compl: "remove_annot s (pickPos v s) ⊑ subst_trm ρ v"
      using compl_trans[OF remove_annot_compl 1(2)] t by (auto simp: test_def)
    have rm_cov: "∀α ∈ tvars_trm v. ∃p ∈ poss v. α ∈ tvars_mty (mtp_of v p) ∧
      mtp_of (remove_annot s (pickPos v s)) p ≠ None"
    proof (intro ballI)
      fix α assume "α ∈ tvars_trm v"
      with 1(3) obtain q where qv: "q ∈ poss v" "α ∈ tvars_mty (mtp_of v q)"
        "mtp_of s q ≠ None" by auto
      have ps_eq: "poss s = poss v"
        using compl_poss_eq[OF 1(2)] by simp
      show "∃p ∈ poss v. α ∈ tvars_mty (mtp_of v p) ∧
        mtp_of (remove_annot s (pickPos v s)) p ≠ None"
      proof (cases "q = pickPos v s")
        case False
        then have "mtp_of (remove_annot s (pickPos v s)) q = mtp_of s q"
          using mtp_of_remove_other t qv(1) ps_eq by (auto simp: test_def)
        with qv show ?thesis by auto
      next
        case True
        text ‹\<^term>‹q = pickPos v s›, so \<^term>‹mtp_of s q› is removed. But by the test condition,
          \<^term>‹α› is covered by some other position.›
        from t True have "∃q' ∈ poss s - {q}. α ∈ tvars_mty (mtp_of v q') ∧ mtp_of s q' ≠ None"
          using qv(2) by (auto simp: test_def)
        then obtain q' where q'v: "q' ∈ poss v" "q' ≠ pickPos v s"
          "α ∈ tvars_mty (mtp_of v q')" "mtp_of s q' ≠ None"
          using ps_eq True by auto
        have "mtp_of (remove_annot s (pickPos v s)) q' = mtp_of s q'"
          using mtp_of_remove_other t q'v(1,2) ps_eq by (auto simp: test_def)
        with q'v show ?thesis by auto
      qed
    qed
    from 1(1)[OF True rm_compl rm_cov] True
    show ?thesis by (metis decrease.simps)
  qed
qed

theorem completeness:
  assumes ty: "typeable t" and ua: "unambiguous t" and ct: "cterm t"
  shows ‹correct_printing t (smobla t)›
proof -
  let ?v = "mgen (erase t)"
  let ?s = "smobla t"
  text ‹Basic setup: \<^term>‹erase t› is typeable and unambiguous.›
  have er_ty: "typeable (erase t)"
    using ty by (auto simp: typeable_def is_wt_completion_def
      intro: compl_trans[OF erase_compl])
  have er_ua: "unambiguous (erase t)" using ua by simp
  have t_ty_ua: "typeable t" "unambiguous t" using ty ua by auto
  text ‹Part 1: \<^term>‹erase t ⊑ ?s› and \<^term>‹?s ⊑ mgen t›.›
  have s_def: "?s = decrease ?v (mgen t)" by (simp add: smobla_def)
  have compl1: "erase t ⊑ mgen t" using erase_compl mgen_compl[OF ty ua] compl_trans by blast
  have s_compl_mgen: "?s ⊑ mgen t" using decrease_compl s_def by simp
  have er_compl_s: "erase t ⊑ ?s" using erase_compl_decrease[OF compl1] s_def by simp
  text ‹\<^term>‹mgen t› is a well-typed F-term completion of \<^term>‹?s›.›
  have wt_completion: "is_wt_completion ?s (mgen t)"
    unfolding is_wt_completion_def using s_compl_mgen mgen_fterm[OF ty ua] mgen_wt[OF ty ua] by auto
  text ‹Part 2: uniqueness. Any well-typed completion of \<^term>‹?s› must equal \<^term>‹mgen t›.›
  have unique: "u = mgen t" if u_wc: ‹is_wt_completion ?s u› for u
  proof -
    from u_wc have su: "?s ⊑ u" and fu: "fterm u" and wtu: "⊢ u"
      by (auto simp: is_wt_completion_def)
    text ‹\<^term>‹u› is a completion of \<^term>‹erase t›, hence \<^term>‹u› is an instance of \<^term>‹?v›.›
    have er_u: "erase t ⊑ u" using compl_trans[OF er_compl_s su] .
    have "is_wt_completion (erase t) u"
      unfolding is_wt_completion_def using er_u fu wtu by auto
    then obtain ρ' where u_inst: "u = subst_trm ρ' ?v"
      using mgen_most_general[OF er_ty er_ua] by auto
    text ‹Similarly, \<^term>‹mgen t› is a completion of \<^term>‹erase t›, hence \<^term>‹mgen t› is an 
      instance of \<^term>‹?v›.›
    have "is_wt_completion (erase t) (mgen t)"
      unfolding is_wt_completion_def using compl1 mgen_fterm[OF ty ua] mgen_wt[OF ty ua] by auto
    then obtain ρ where mgen_inst: "mgen t = subst_trm ρ ?v"
      using mgen_most_general[OF er_ty er_ua] by auto
    text ‹The coverage condition: every tyvar of \<^term>‹?v› is witnessed 
      at a non-bot position of \<^term>‹?s›.›
    have fv: "fterm ?v" using mgen_fterm[OF er_ty er_ua] .
    have cov: "∀α ∈ tvars_trm ?v. ∃p ∈ poss ?v. α ∈ tvars_mty (mtp_of ?v p) ∧
      mtp_of (mgen t) p ≠ None"
    proof (intro ballI)
      fix α assume "α ∈ tvars_trm ?v"
      then obtain p where "p ∈ poss ?v" "α ∈ tvars_mty (mtp_of ?v p)"
      using tvars_trm_eq_UN_mtp by fastforce
      moreover have "mtp_of (mgen t) p ≠ None"
      proof -
        have "p ∈ poss (mgen t)" using ‹p ∈ poss ?v› compl_poss_eq[OF compl1]
          compl_poss_eq[OF mgen_compl[OF er_ty er_ua]] by simp
        then show ?thesis using fterm_mtp_of_Some[OF mgen_fterm[OF ty ua]] by fastforce
      qed
      ultimately show "∃p ∈ poss ?v. α ∈ tvars_mty (mtp_of ?v p) ∧ mtp_of (mgen t) p ≠ None"
        by auto
    qed
    have s_compl_subst: "?s ⊑ subst_trm ρ ?v" using s_compl_mgen mgen_inst by simp
    have cov_mgen: "∀α ∈ tvars_trm ?v. ∃p ∈ poss ?v. α ∈ tvars_mty (mtp_of ?v p) ∧
      mtp_of (mgen t) p ≠ None" using cov .
    have cov_s: "∀α ∈ tvars_trm ?v. ∃p ∈ poss ?v. α ∈ tvars_mty (mtp_of ?v p) ∧
      mtp_of ?s p ≠ None"
    proof (intro ballI)
      fix α assume "α ∈ tvars_trm ?v"
      have dec_cov: "∀α ∈ tvars_trm ?v. ∃p ∈ poss ?v. α ∈ tvars_mty (mtp_of ?v p) ∧
        mtp_of (decrease ?v (mgen t)) p ≠ None"
      proof -
        have "mgen t ⊑ subst_trm ρ ?v" using mgen_inst by simp
        then show ?thesis using decrease_coverage[OF fv] cov_mgen by blast
      qed
      with ‹α ∈ tvars_trm ?v› obtain p where "p ∈ poss ?v"
        "α ∈ tvars_mty (mtp_of ?v p)" "mtp_of (decrease ?v (mgen t)) p ≠ None"
        by auto
      then show "∃p ∈ poss ?v. α ∈ tvars_mty (mtp_of ?v p) ∧ mtp_of ?s p ≠ None"
        unfolding s_def by blast
    qed
    text ‹Apply @{thm crucial_uniqueness}.›
    have "∃ρ. mgen t = subst_trm ρ ?v" using mgen_inst by auto
    moreover have "∃ρ'. u = subst_trm ρ' ?v" using u_inst by auto
    show "u = mgen t"
    proof -
      have "mgen t = u"
        by (rule crucial_uniqueness[OF s_compl_mgen mgen_fterm[OF ty ua]
          ‹∃ρ. mgen t = subst_trm ρ ?v› fv cov_s su fu ‹∃ρ'. u = subst_trm ρ' ?v›])
      then show ?thesis by simp
    qed
  qed

  show ?thesis
    using assms wt_completion unique mgen_is_mgen
    unfolding correct_printing_def is_mgen_def
    by fastforce+
qed

subsection ‹Minimality›

text ‹Supporting lemmas for minimality.›

text ‹After decrease, no position passes the test.›
lemma decrease_no_test:
  "¬test v (decrease v s) p"
proof (induction v s rule: decrease.induct)
  case (1 v s)
  show ?case
  proof (cases "∃p. test v s p")
    case False
    then show ?thesis by (metis decrease.simps)
  next
    case True
    then have "decrease v s = decrease v (remove_annot s (pickPos v s))"
      by (metis decrease.simps)
    with 1 True show ?thesis by simp
  qed
qed

text ‹Decrease preserves unambiguity.›
lemma decrease_unambiguous:
  "unambiguous s ⟹ unambiguous (decrease v s)"
proof (induction v s rule: decrease.induct)
  case (1 v s)
  show ?case
  proof (cases "∃p. test v s p")
    case False
    then show ?thesis using 1(2) by (metis decrease.simps)
  next
    case True
    then have pp: "pickPos v s ∈ poss s" using compat by (auto simp: test_def)
    have "unambiguous (remove_annot s (pickPos v s))"
      using remove_annot_unambiguous[OF pp] 1(2) by auto
    then have "unambiguous (decrease v (remove_annot s (pickPos v s)))"
      using 1(1)[OF True] by auto
    with True show ?thesis by (metis decrease.simps)
  qed
qed

text ‹Coverage minimality.›
theorem smobla_distinct_completions:
  assumes ty: "typeable t" and ua: "unambiguous t" and ct: "cterm t"
    and ua': "unambiguous s'" and s'_compl: "s' ⊑ smobla t" and s'_neq: "s' ≠ smobla t"
  obtains v v' where "v ≠ v'" "is_mgen s' v" "is_mgen s' v'"
proof -
  let ?s = "smobla t"
  let ?v = "mgen (erase t)"
  have s_ua: "unambiguous ?s"
    using decrease_unambiguous compl_unambiguous[OF mgen_compl[OF ty ua]] ua
    unfolding smobla_def by metis
  text ‹Get a position where \<^term>‹s'› has \<^term>‹None› but \<^term>‹?s› has non-\<^term>‹None›.›
  from compl_strict_witness[OF s'_compl s'_neq]
  obtain p where ps: "p ∈ poss ?s" and s'_none: "mtp_of s' p = None" and s_some: "mtp_of ?s p ≠ None"
    by auto
  text ‹Since not \<^term>‹test ?v ?s p›, there exists a tyvar uncovered by \<^term>‹?s›.›
  have no_test: "¬ test ?v ?s p" using decrease_no_test unfolding smobla_def by blast
  text ‹From completeness, \<^term>‹mgen t› is the unique well-typed completion of \<^term>‹?s›.
    \<^term>‹s' ⊑ ?s› and \<^term>‹?s ⊑ mgen t›, so \<^term>‹mgen t› is a completion of \<^term>‹s'›.
    Any other completion of \<^term>‹s'› gives two distinct completions.›

  have s_compl_mgen: "?s ⊑ mgen t"
    using decrease_compl smobla_def by metis
  have s'_compl_mgen: "is_wt_completion s' (mgen t)"
    using compl_trans[OF s'_compl s_compl_mgen] mgen_fterm[OF ty ua] mgen_wt[OF ty ua]
    by (auto simp: is_wt_completion_def)
  text ‹Construct a second distinct completion using the uncovered tyvar.›
  have er_ty: "typeable (erase t)"
    using ty by (auto simp: typeable_def is_wt_completion_def intro: compl_trans[OF erase_compl])
  have er_ua: "unambiguous (erase t)" using ua by simp
  obtain ρ where mgen_inst: "mgen t = subst_trm ρ ?v"
    using mgen_most_general[OF er_ty er_ua]
      compl_trans[OF erase_compl mgen_compl[OF ty ua]] mgen_fterm[OF ty ua] mgen_wt[OF ty ua]
    by (auto simp: is_wt_completion_def)
  have fv: "fterm ?v" using mgen_fterm[OF er_ty er_ua] .
  have wtv: "⊢ ?v" using mgen_wt[OF er_ty er_ua] .
  have poss_sv: "poss ?s = poss ?v"
    using compl_poss_eq[OF s_compl_mgen] mgen_inst by simp
  have pv: "p ∈ poss ?v" using ps poss_sv by simp
  text ‹Extract tyvar from the negated test.›
  from no_test ps pv s_some obtain α where alpha_vp: "α ∈ tvars_mty (mtp_of ?v p)"
    and uncov: "∀q ∈ poss ?s - {p}. α ∈ tvars_mty (mtp_of ?v q) ⟶ mtp_of ?s q = None"
    unfolding test_def by blast
  text ‹Property (c): \<^term>‹α› is uncovered in \<^term>‹s'›.›
  have poss_s': "poss s' = poss ?s" using compl_poss_eq[OF s'_compl] .
  have prop_c: ‹mtp_of s' q = None› if ‹q ∈ poss s'› and ‹α ∈ tvars_mty (mtp_of ?v q)› for q
    using compl_mtp_of[OF s'_compl, of q] that uncov
    by (auto simp: mcompl_def s'_none poss_s')
  have s'_compl_vrho: "s' ⊑ subst_trm ρ ?v"
    using compl_trans[OF s'_compl s_compl_mgen] mgen_inst by simp
  text ‹Construct type differing from \<^term>‹ρ› at \<^term>‹α›.
    Simplest: \<^term>‹TyVar› with a fresh variable, always well-typed.›
  obtain w :: "('tv,'k) ty" where w_neq: "w ≠ ρ α"
    using ty.distinct(1) by metis
  define ρ' where "ρ' = (λβ. if β = α then w else ρ β)"
  text ‹(2) \<^term>‹ρ› and \<^term>‹ρ'› agree on non-\<^term>‹None› positions of \<^term>‹s'›.›
  have agree: "ρ β = ρ' β" if "q ∈ poss ?v" "β ∈ tvars_mty (mtp_of ?v q)" "mtp_of s' q ≠ None" 
      for β q using that ρ'_def poss_s' poss_sv prop_c by auto
  have s'_compl_vrho': "s' ⊑ subst_trm ρ' ?v"
    using multiple_compl[OF s'_compl_vrho agree] .
  have wtvrho': "⊢ subst_trm ρ' ?v" using subst_wt[OF wtv] .
  have "α ∈ tvars_trm ?v" using alpha_vp tvars_trm_eq_UN_mtp pv by fastforce
  then have vrho_neq: "subst_trm ρ ?v ≠ subst_trm ρ' ?v"
    using w_neq by (auto simp: subst_trm_agree ρ'_def)
  text ‹Two distinct completions of \<^term>‹s'›.›
  have wc1: "is_wt_completion s' (subst_trm ρ ?v)"
    using s'_compl_vrho fv subst_wt[OF wtv] by (auto simp: is_wt_completion_def)
  have wc2: "is_wt_completion s' (subst_trm ρ' ?v)"
    using s'_compl_vrho' fv wtvrho' by (auto simp: is_wt_completion_def)
  from lift_to_most_general[OF ua' wc1 wc2 vrho_neq] show ?thesis using that by metis
qed

corollary minimality:
  assumes "typeable t" "unambiguous t" "cterm t" ‹s ⊑ smobla t› ‹correct_printing t s›
  shows ‹s = smobla t›
  using assms smobla_distinct_completions
  unfolding correct_printing_def
  by (metis mgen_compl decrease_unambiguous compl_unambiguous smobla_def)

end

end