Theory Unary_PCF

(*  Title:       Towards Decidability of Behavioral Equivalence for Unary PCF
    Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2017
    Maintainer:  Dmitriy Traytel <traytel at inf.ethz.ch>
*)

section ‹Towards Decidability of Behavioral Equivalence for Unary PCF›

theory Unary_PCF
  imports
    "HOL-Library.FSet"
    "HOL-Library.Countable_Set_Type"
    "HOL-Library.Nat_Bijection"
    Hereditary_Multiset
    "List-Index.List_Index"
begin

subsection ‹Preliminaries›

lemma prod_UNIV: "UNIV = UNIV × UNIV"
  by auto

lemma infinite_cartesian_productI1: "infinite A ⟹ B ≠ {} ⟹ infinite (A × B)"
  by (auto dest!: finite_cartesian_productD1)


subsection ‹Types›

datatype type = ℬ (‹ℬ›) | Fun type type (infixr ‹→› 65)

definition mk_fun  (infixr ‹→→› 65) where
  "Ts →→ T = fold (→) (rev Ts) T"

primrec dest_fun where
  "dest_fun ℬ = []"
| "dest_fun (T → U) = T # dest_fun U"

definition arity where
  "arity T = length (dest_fun T)"

lemma mk_fun_dest_fun[simp]: "dest_fun T →→ ℬ = T"
  by (induct T) (auto simp: mk_fun_def)

lemma dest_fun_mk_fun[simp]: "dest_fun (Ts →→ T) = Ts @ dest_fun T"
  by (induct Ts) (auto simp: mk_fun_def)

primrec δ where
  "δ ℬ = HMSet {#}"
| "δ (T → U) = HMSet (add_mset (δ T) (hmsetmset (δ U)))"

lemma δ_mk_fun: "δ (Ts →→ T) = HMSet (hmsetmset (δ T) + mset (map δ Ts))"
  by (induct Ts) (auto simp: mk_fun_def)

lemma type_induct [case_names Fun]:
  assumes
   "(⋀T. (⋀T1 T2. T = T1 → T2 ⟹ P T1) ⟹
    (⋀T1 T2. T = T1 → T2 ⟹ P T2) ⟹ P T)"
  shows "P T"
proof (induct T)
  case ℬ
  show ?case by (rule assms) simp_all
next
  case Fun
  show ?case by (rule assms) (insert Fun, simp_all)
qed


subsection ‹Terms›

type_synonym name = string
type_synonym idx = nat
datatype expr =
    Var "name * type" (‹⟨_⟩›) | Bound idx | B bool
  | Seq expr expr  (infixr ‹?› 75) | App expr expr (infixl ‹⋅› 75)
  | Abs type expr (‹Λ⟨_⟩ _› [100, 100] 800)

declare [[coercion_enabled]]
declare [[coercion B]]
declare [[coercion Bound]]

notation (output) B (‹_›)
notation (output) Bound (‹_›)

primrec "open" :: "idx ⇒ expr ⇒ expr ⇒ expr" where
  "open i t (j :: idx) = (if i = j then t else j)"
| "open i t ⟨yU⟩ = ⟨yU⟩"
| "open i t (b :: bool) = b"
| "open i t (e1 ? e2) = open i t e1 ? open i t e2"
| "open i t (e1 ⋅ e2) = open i t e1 ⋅ open i t e2"
| "open i t (Λ⟨U⟩ e) = Λ⟨U⟩ (open (i + 1) t e)"

abbreviation "open0 ≡ open 0"
abbreviation "open_Var i xT ≡ open i ⟨xT⟩"
abbreviation "open0_Var xT ≡ open 0 ⟨xT⟩"

primrec "close_Var" :: "idx ⇒ name × type ⇒ expr ⇒ expr" where
  "close_Var i xT (j :: idx) = j"
| "close_Var i xT ⟨yU⟩ = (if xT = yU then i else ⟨yU⟩)"
| "close_Var i xT (b :: bool) = b"
| "close_Var i xT (e1 ? e2) = close_Var i xT e1 ? close_Var i xT e2"
| "close_Var i xT (e1 ⋅ e2) = close_Var i xT e1 ⋅ close_Var i xT e2"
| "close_Var i xT (Λ⟨U⟩ e) = Λ⟨U⟩ (close_Var (i + 1) xT e)"

abbreviation "close0_Var ≡ close_Var 0"

primrec "fv" :: "expr ⇒ (name × type) fset" where
  "fv (j :: idx) = {||}"
| "fv ⟨yU⟩ = {|yU|}"
| "fv (b :: bool) = {||}"
| "fv (e1 ? e2) = fv e1 |∪| fv e2"
| "fv (e1 ⋅ e2) = fv e1 |∪| fv e2"
| "fv (Λ⟨U⟩ e) = fv e"

abbreviation "fresh x e ≡ x |∉| fv e"

lemma ex_fresh: "∃x. (x :: char list, T) |∉| A"
proof (rule ccontr, unfold not_ex not_not)
  assume "∀x. (x, T) |∈| A"
  then have "infinite {x. (x, T) |∈| A}" (is "infinite ?P")
    by (auto simp add: infinite_UNIV_listI)
  moreover
  have "?P ⊆ fst ` fset A"
    by force
  from finite_surj[OF _ this] have "finite ?P"
    by simp
  ultimately show False by blast
qed

inductive lc where
  lc_Var[simp]: "lc ⟨xT⟩"
| lc_B[simp]: "lc (b :: bool)"
| lc_Seq: "lc e1 ⟹ lc e2 ⟹ lc (e1 ? e2)"
| lc_App: "lc e1 ⟹ lc e2 ⟹ lc (e1 ⋅ e2)"
| lc_Abs: "(∀x. (x, T) |∉| X ⟶ lc (open0_Var (x, T) e)) ⟹ lc (Λ⟨T⟩ e)"

declare lc.intros[intro]

definition "body T t ≡ (∃X. ∀x. (x, T) |∉| X ⟶ lc (open0_Var (x, T) t))"

lemma lc_Abs_iff_body: "lc (Λ⟨T⟩ t) ⟷ body T t"
  unfolding body_def by (subst lc.simps) simp

lemma fv_open_Var: "fresh xT t ⟹ fv (open_Var i xT t) |⊆| finsert xT (fv t)"
  by (induct t arbitrary: i) auto

lemma fv_close_Var[simp]: "fv (close_Var i xT t) = fv t |-| {|xT|}"
  by (induct t arbitrary: i) auto

lemma close_Var_open_Var[simp]: "fresh xT t ⟹ close_Var i xT (open_Var i xT t) = t"
  by (induct t arbitrary: i) auto

lemma open_Var_inj: "fresh xT t ⟹ fresh xT u ⟹ open_Var i xT t = open_Var i xT u ⟹ t = u"
  by (metis close_Var_open_Var)

context begin

private lemma open_Var_open_Var_close_Var: "i ≠ j ⟹ xT ≠ yU ⟹ fresh yU t ⟹
  open_Var i yU (open_Var j zV (close_Var j xT t)) = open_Var j zV (close_Var j xT (open_Var i yU t))"
  by (induct t arbitrary: i j) auto

lemma open_Var_close_Var[simp]: "lc t ⟹ open_Var i xT (close_Var i xT t) = t"
proof (induction t arbitrary: i rule: lc.induct)
  case (lc_Abs T X e i)
  obtain x where x: "fresh (x, T) e" "(x, T) ≠ xT" "(x, T) |∉| X"
    using ex_fresh[of _ "fv e |∪| finsert xT X"] by blast
  with lc_Abs.IH have "lc (open0_Var (x, T) e)"
    "open_Var (i + 1) xT (close_Var (i + 1) xT (open0_Var (x, T) e)) = open0_Var (x, T) e"
    by auto
  with x show ?case
    by (auto simp: open_Var_open_Var_close_Var
      dest: fset_mp[OF fv_open_Var, rotated]
      intro!: open_Var_inj[of "(x, T)" _ e 0])
qed auto

end

lemma close_Var_inj: "lc t ⟹ lc u ⟹ close_Var i xT t = close_Var i xT u ⟹ t = u"
  by (metis open_Var_close_Var)

primrec Apps (infixl ‹∙› 75) where
  "f ∙ [] = f"
| "f ∙ (x # xs) = f ⋅ x ∙ xs"

lemma Apps_snoc: "f ∙ (xs @ [x]) = f ∙ xs ⋅ x"
  by (induct xs arbitrary: f) auto

lemma Apps_append: "f ∙ (xs @ ys) = f ∙  xs ∙  ys"
  by (induct xs arbitrary: f) auto

lemma Apps_inj[simp]: "f ∙ ts = g ∙ ts ⟷ f = g"
  by (induct ts arbitrary: f g) auto

lemma eq_Apps_conv[simp]:
  fixes i :: idx and b :: bool and f :: expr and ts :: "expr list"
  shows
    "(⟨m⟩ = f ∙ ts) = (⟨m⟩ = f ∧ ts = [])"
    "(f  ∙ ts = ⟨m⟩) = (⟨m⟩ = f ∧ ts = [])"
    "(i = f ∙ ts) = (i = f ∧ ts = [])"
    "(f ∙ ts = i) = (i = f ∧ ts = [])"
    "(b = f ∙ ts) = (b = f ∧ ts = [])"
    "(f ∙ ts = b) = (b = f ∧ ts = [])"
    "(e1 ? e2 = f ∙ ts) = (e1 ? e2 = f ∧ ts = [])"
    "(f ∙ ts = e1 ? e2) = (e1 ? e2 = f ∧ ts = [])"
    "(Λ⟨T⟩ t = f ∙ ts) = (Λ⟨T⟩ t = f ∧ ts = [])"
    "(f ∙ ts = Λ⟨T⟩ t) = (Λ⟨T⟩ t = f ∧ ts = [])"
  by (induct ts arbitrary: f) auto

lemma Apps_Var_eq[simp]: "⟨xT⟩ ∙ ss = ⟨yU⟩ ∙ ts ⟷ xT = yU ∧ ss = ts"
proof (induct ss arbitrary: ts rule: rev_induct)
  case snoc
  then show ?case by (induct ts rule: rev_induct) (auto simp: Apps_snoc)
qed auto

lemma Apps_Abs_neq_Apps[simp, symmetric, simp]:
  "Λ⟨T⟩ r ⋅ t ≠ ⟨xT⟩ ∙ ss"
  "Λ⟨T⟩ r ⋅ t ≠ (i :: idx) ∙ ss"
  "Λ⟨T⟩ r ⋅ t ≠ (b :: bool) ∙ ss"
  "Λ⟨T⟩ r ⋅ t ≠ (e1 ? e2) ∙ ss"
  by (induct ss rule: rev_induct) (auto simp: Apps_snoc)

lemma App_Abs_eq_Apps_Abs[simp]: "Λ⟨T⟩ r ⋅ t = Λ⟨T'⟩ r' ∙ ss ⟷ T = T' ∧ r = r' ∧ ss = [t]"
  by (induct ss rule: rev_induct) (auto simp: Apps_snoc)

lemma Apps_Var_neq_Apps_Abs[simp, symmetric, simp]: "⟨xT⟩ ∙ ss ≠ Λ⟨T⟩ r ∙ ts"
proof (induct ss arbitrary: ts rule: rev_induct)
  case (snoc a ss)
  then show ?case by (induct ts rule: rev_induct) (auto simp: Apps_snoc)
qed simp

lemma Apps_Var_neq_Apps_beta[simp, THEN not_sym, simp]:
  "⟨xT⟩ ∙ ss ≠ Λ⟨T⟩ r ⋅ s ∙ ts"
  by (metis Apps_Var_neq_Apps_Abs Apps_append Apps_snoc eq_Apps_conv(9))

lemma [simp]:
  "(Λ⟨T⟩ r ∙ ts = Λ⟨T'⟩ r' ⋅ s' ∙ ts') = (T = T' ∧ r = r' ∧ ts = s' # ts')"
proof (induct ts arbitrary: ts' rule: rev_induct)
  case Nil
  then show ?case by (induct ts' rule: rev_induct) (auto simp: Apps_snoc)
next
  case snoc
  then show ?case by (induct ts' rule: rev_induct) (auto simp: Apps_snoc)
qed

lemma fold_eq_Bool_iff[simp]:
  "fold (→) (rev Ts) T = ℬ ⟷ Ts = [] ∧ T = ℬ"
  "ℬ = fold (→) (rev Ts) T ⟷ Ts = [] ∧ T = ℬ"
  by (induct Ts) auto

lemma fold_eq_Fun_iff[simp]:
  "fold (→) (rev Ts) T = U → V ⟷
   (Ts = [] ∧ T = U → V ∨ (∃Us. Ts = U # Us ∧ fold (→) (rev Us) T = V))"
  by (induct Ts) auto


subsection ‹Substitution›

primrec subst where
  "subst xT t ⟨yU⟩ = (if xT = yU then t else ⟨yU⟩)"
| "subst xT t (i :: idx) = i"
| "subst xT t (b :: bool) = b"
| "subst xT t (e1 ? e2) = subst xT t e1 ? subst xT t e2"
| "subst xT t (e1 ⋅ e2) = subst xT t e1 ⋅ subst xT t e2"
| "subst xT t (Λ⟨T⟩ e) = Λ⟨T⟩ (subst xT t e)"

lemma fv_subst:
  "fv (subst xT t u) = fv u |-| {|xT|} |∪| (if xT |∈| fv u then fv t else {||})"
  by (induct u) auto

lemma subst_fresh: "fresh xT u ⟹ subst xT t u = u"
  by (induct u) auto

context begin

private lemma open_open_id: "i ≠ j ⟹ open i t (open j t' u) = open j t' u ⟹ open i t u = u"
  by (induct u arbitrary: i j) (auto 6 0)

lemma lc_open_id: "lc u ⟹ open k t u = u"
proof (induct u arbitrary: k rule: lc.induct)
  case (lc_Abs T X e)
  obtain x where x: "fresh (x, T) e" "(x, T) |∉| X"
    using ex_fresh[of _ "fv e |∪| X"] by blast
  with lc_Abs show ?case
    by (auto intro: open_open_id dest: spec[of _ x] spec[of _ "Suc k"])
qed auto

lemma subst_open: "lc u ⟹ subst xT u (open i t v) = open i (subst xT u t) (subst xT u v)"
  by (induction v arbitrary: i) (auto intro: lc_open_id[symmetric])

lemma subst_open_Var:
  "xT ≠ yU ⟹ lc u ⟹ subst xT u (open_Var i yU v) = open_Var i yU (subst xT u v)"
  by (auto simp: subst_open)

lemma subst_Apps[simp]:
  "subst xT u (f ∙ xs) = subst xT u f ∙ map (subst xT u) xs"
  by (induct xs arbitrary: f) auto

end

context begin

private lemma fresh_close_Var_id: "fresh xT t ⟹ close_Var k xT t = t"
  by (induct t arbitrary: k) auto

lemma subst_close_Var:
  "xT ≠ yU ⟹ fresh yU u ⟹ subst xT u (close_Var i yU t) = close_Var i yU (subst xT u t)"
  by (induct t arbitrary: i) (auto simp: fresh_close_Var_id)

end

lemma subst_intro: "fresh xT t ⟹ lc u ⟹ open0 u t = subst xT u (open0_Var xT t)"
  by (auto simp: subst_fresh subst_open)

lemma lc_subst[simp]: "lc u ⟹ lc t ⟹ lc (subst xT t u)"
proof (induct u rule: lc.induct)
  case (lc_Abs T X e)
  then show ?case
    by (auto simp: subst_open_Var intro!: lc.lc_Abs[of _ "fv e |∪| X |∪| {|xT|}"])
qed auto

lemma body_subst[simp]: "body U u ⟹ lc t ⟹ body U (subst xT t u)"
proof (subst (asm) body_def, elim conjE exE)
  fix X
  assume [simp]: "lc t" "∀x. (x, U) |∉| X ⟶ lc (open0_Var (x, U) u)"
  show "body U (subst xT t u)"
  proof (unfold body_def, intro exI[of _ "finsert xT X"] conjI allI impI)
    fix x
    assume "(x, U) |∉| finsert xT X"
    then show "lc (open0_Var (x, U) (subst xT t u))"
      by (auto simp: subst_open_Var[symmetric])
  qed
qed

lemma lc_open_Var: "lc u ⟹ lc (open_Var i xT u)"
  by (simp add: lc_open_id)

lemma lc_open[simp]: "body U u ⟹ lc t ⟹ lc (open0 t u)"
proof (unfold body_def, elim conjE exE)
  fix X
  assume [simp]: "lc t" "∀x. (x, U) |∉| X ⟶ lc (open0_Var (x, U) u)"
  with ex_fresh[of _ "fv u |∪| X"] obtain x where [simp]: "fresh (x, U) u" "(x, U) |∉| X" by blast
  show ?thesis by (subst subst_intro[of "(x, U)"]) auto
qed


subsection ‹Typing›

inductive welltyped :: "expr ⇒ type ⇒ bool" (infix ‹:::› 60) where
  welltyped_Var[intro!]: "⟨(x, T)⟩ ::: T"
| welltyped_B[intro!]: "(b :: bool) ::: ℬ"
| welltyped_Seq[intro!]: "e1 ::: ℬ ⟹ e2 ::: ℬ ⟹ e1 ? e2 ::: ℬ"
| welltyped_App[intro]: "e1 ::: T → U ⟹ e2 ::: T ⟹ e1 ⋅ e2 ::: U"
| welltyped_Abs[intro]: "(∀x. (x, T) |∉| X ⟶ open0_Var (x, T) e ::: U) ⟹ Λ⟨T⟩ e ::: T → U"

inductive_cases welltypedE[elim!]:
   "⟨x⟩ ::: T"
   "(i :: idx) ::: T"
   "(b :: bool) ::: T"
   "e1 ? e2 ::: T"
   "e1 ⋅ e2 ::: T"
   "Λ⟨T⟩ e ::: U"

lemma welltyped_unique: "t ::: T ⟹ t ::: U ⟹ T = U"
proof (induction t T arbitrary: U rule: welltyped.induct)
  case (welltyped_Abs T X t U T')
  from welltyped_Abs.prems show ?case
  proof (elim welltypedE)
    fix Y U'
    obtain x where [simp]: "(x, T) |∉| X" "(x, T) |∉| Y"
      using ex_fresh[of _ "X |∪| Y"] by blast
    assume [simp]: "T' = T → U'" "∀x. (x, T) |∉| Y ⟶ open0_Var (x, T) t ::: U'"
    show "T → U = T'"
      by (auto intro: conjunct2[OF welltyped_Abs.IH[rule_format], rule_format, of x])
  qed
qed blast+

lemma welltyped_lc[simp]: "t ::: T ⟹ lc t"
  by (induction t T rule: welltyped.induct) auto

lemma welltyped_subst[intro]:
  "u ::: U ⟹ t ::: snd xT ⟹ subst xT t u ::: U"
proof (induction u U rule: welltyped.induct)
  case (welltyped_Abs T' X u U)
  then show ?case unfolding subst.simps
    by (intro welltyped.welltyped_Abs[of _ "finsert xT X"]) (auto simp: subst_open_Var[symmetric])
qed auto

lemma rename_welltyped: "u ::: U ⟹ subst (x, T) ⟨(y, T)⟩ u ::: U"
  by (rule welltyped_subst) auto

lemma welltyped_Abs_fresh:
  assumes "fresh (x, T) u" "open0_Var (x, T) u ::: U"
  shows "Λ⟨T⟩ u ::: T → U"
proof (intro welltyped_Abs[of _ "fv u"] allI impI)
  fix y
  assume "fresh (y, T) u"
  with assms(2) have "subst (x, T) ⟨(y, T)⟩ (open0_Var (x, T) u) ::: U" (is "?t ::: _")
    by (auto intro: rename_welltyped)
  also have "?t = open0_Var (y, T) u"
    by (subst subst_intro[symmetric]) (auto simp: assms(1))
  finally show "open0_Var (y, T) u ::: U" .
qed

lemma Apps_alt: "f ∙ ts ::: T ⟷
  (∃Ts. f ::: fold (→) (rev Ts) T ∧ list_all2 (:::) ts Ts)"
proof (induct ts arbitrary: f)
  case (Cons t ts)
  from Cons(1)[of "f ⋅ t"] show ?case
    by (force simp: list_all2_Cons1)
qed simp


subsection ‹Definition 10 and Lemma 11 from Schmidt-Schau{\ss}'s paper›

abbreviation "closed t ≡ fv t = {||}"

primrec constant0 where
  "constant0 ℬ = Var (''bool'', ℬ)"
| "constant0 (T → U) = Λ⟨T⟩ (constant0 U)"

definition "constant T = Λ⟨ℬ⟩ (close0_Var (''bool'', ℬ) (constant0 T))"

lemma fv_constant0[simp]: "fv (constant0 T) = {|(''bool'', ℬ)|}"
  by (induct T) auto

lemma closed_constant[simp]: "closed (constant T)"
  unfolding constant_def by auto

lemma welltyped_constant0[simp]: "constant0 T ::: T"
  by (induct T) (auto simp: lc_open_id)

lemma lc_constant0[simp]: "lc (constant0 T)"
  using welltyped_constant0 welltyped_lc by blast

lemma welltyped_constant[simp]: "constant T ::: ℬ → T"
  unfolding constant_def by (auto intro: welltyped_Abs_fresh[of "''bool''"])

definition nth_drop where
  "nth_drop i xs ≡ take i xs @ drop (Suc i) xs"

definition nth_arg (infixl ‹!-› 100) where
  "nth_arg T i ≡ nth (dest_fun T) i"

abbreviation ar where
  "ar T ≡ length (dest_fun T)"

lemma size_nth_arg[simp]: "i < ar T ⟹ size (T !- i) < size T"
  by (induct T arbitrary: i) (force simp: nth_Cons' nth_arg_def gr0_conv_Suc)+

fun π :: "type ⇒ nat ⇒ nat ⇒ type" where
  "π T i 0 = (if i < ar T then nth_drop i (dest_fun T) →→ ℬ else ℬ)"
| "π T i (Suc j) = (if i < ar T ∧ j < ar (T!-i)
    then π (T!-i) j 0 →
      map (π (T!-i) j o Suc) [0 ..< ar (T!-i!-j)] →→ π T i 0 else ℬ)"

theorem π_induct[rotated -2, consumes 2, case_names 0 Suc]:
  assumes "⋀T i. i < ar T ⟹ P T i 0"
    and "⋀T i j. i < ar T ⟹ j < ar (T !- i) ⟹ P (T !- i) j 0 ⟹
       (∀x < ar (T !- i !- j). P (T !- i) j (x + 1)) ⟹ P T i (j + 1)"
  shows "i < ar T ⟹ j ≤ ar (T !- i) ⟹ P T i j"
  by (induct T i j rule: π.induct) (auto intro: assms[simplified])

definition ε :: "type ⇒ nat ⇒ type" where
  "ε T i = π T i 0 → map (π T i o Suc) [0 ..< ar (T!-i)] →→ T"

definition Abss (‹Λ[_] _› [100, 100] 800) where
  "Λ[xTs] b = fold (λxT t. Λ⟨snd xT⟩ close0_Var xT t) (rev xTs) b"

definition Seqs (infixr ‹??› 75) where
  "ts ?? t = fold (λu t. u ? t) (rev ts) t"

definition "variant k base = base @ replicate k CHR ''*''"

lemma variant_inj: "variant i base = variant j base ⟹ i = j"
  unfolding variant_def by auto

lemma variant_inj2:
  "CHR ''*'' ∉ set b1 ⟹ CHR ''*'' ∉ set b2 ⟹ variant i b1 = variant j b2 ⟹ b1 = b2"
  unfolding variant_def
  by (auto simp: append_eq_append_conv2)
    (metis Nil_is_append_conv hd_append2 hd_in_set hd_rev last_ConsR
     last_snoc replicate_append_same rev_replicate)+

fun E :: "type ⇒ nat ⇒ expr" and P :: "type ⇒ nat ⇒ nat ⇒ expr" where
  "E T i = (if i < ar T then (let
       Ti = T!-i;
       x = λk. (variant k ''x'', T!-k);
       xs = map x [0 ..< ar T];
       xx_var = ⟨nth xs i⟩;
       x_vars = map (λx. ⟨x⟩) (nth_drop i xs);
       yy = (''z'', π T i 0);
       yy_var = ⟨yy⟩;
       y = λj. (variant j ''y'', π T i (j + 1));
       ys = map y [0 ..< ar Ti];
       e = λj. ⟨y j⟩ ∙ (P Ti j 0 ⋅ xx_var # map (λk. P Ti j (k + 1) ⋅ xx_var) [0 ..< ar (Ti!-j)]);
       guards = map (λi. xx_var ∙
           map (λj. constant (Ti!-j) ⋅ (if i = j then e i ∙ x_vars else True)) [0 ..< ar Ti])
         [0 ..< ar Ti]
     in Λ[(yy # ys @ xs)] (guards ?? (yy_var ∙ x_vars))) else constant (ε T i) ⋅ False)"
| "P T i 0 =
     (if i < ar T then (let
       f = (''f'', T);
       f_var = ⟨f⟩;
       x = λk. (variant k ''x'', T!-k);
       xs = nth_drop i (map x [0 ..< ar T]);
       x_vars = insert_nth i (constant (T!-i) ⋅ True) (map (λx. ⟨x⟩) xs)
     in Λ[(f # xs)] (f_var ∙ x_vars)) else constant (T → π T i 0) ⋅ False)"
| "P T i (Suc j) = (if i < ar T ∧ j < ar (T!-i) then (let
       Ti = T!-i;
       Tij = Ti!-j;
       f = (''f'', T);
       f_var = ⟨f⟩;
       x = λk. (variant k ''x'', T!-k);
       xs = nth_drop i (map x [0 ..< ar T]);
       yy = (''z'', π Ti j 0);
       yy_var = ⟨yy⟩;
       y = λk. (variant k ''y'', π Ti j (k + 1));
       ys = map y [0 ..< ar Tij];
       y_vars = yy_var # map (λx. ⟨x⟩) ys;
       x_vars = insert_nth i (E Ti j ∙ y_vars) (map (λx. ⟨x⟩) xs)
     in Λ[(f # yy # ys @ xs)] (f_var ∙ x_vars)) else constant (T → π T i (j + 1)) ⋅ False)"

lemma Abss_Nil[simp]: "Λ[[]] b = b"
  unfolding Abss_def by simp

lemma Abss_Cons[simp]: "Λ[(x#xs)] b = Λ⟨snd x⟩ (close0_Var x (Λ[xs] b))"
  unfolding Abss_def by simp

lemma welltyped_Abss: "b ::: U ⟹ T = map snd xTs →→ U ⟹ Λ[xTs] b ::: T"
  by (hypsubst_thin, induct xTs) (auto simp: mk_fun_def intro!: welltyped_Abs_fresh)

lemma welltyped_Apps: "list_all2 (:::) ts Ts ⟹ f ::: Ts →→ U ⟹ f ∙ ts ::: U"
  by (induct ts Ts arbitrary: f rule: list.rel_induct) (auto simp: mk_fun_def)

lemma welltyped_open_Var_close_Var[intro!]:
  "t ::: T ⟹ open0_Var xT (close0_Var xT t) ::: T"
  by auto

lemma welltyped_Var_iff[simp]:
  "⟨(x, T)⟩ ::: U ⟷ T = U"
  by auto

lemma welltyped_bool_iff[simp]: "(b :: bool) ::: T ⟷ T = ℬ"
  by auto

lemma welltyped_constant0_iff[simp]: "constant0 T ::: U ⟷ (U = T)"
  by (induct T arbitrary: U) (auto simp: ex_fresh lc_open_id)

lemma welltyped_constant_iff[simp]: "constant T ::: U ⟷ (U = ℬ → T)"
  unfolding constant_def
proof (intro iffI, elim welltypedE, hypsubst_thin, unfold type.inject simp_thms)
  fix X U
  assume "∀x. (x, ℬ) |∉| X ⟶ open0_Var (x, ℬ) (close0_Var (''bool'', ℬ) (constant0 T)) ::: U"
  moreover obtain x where "(x, ℬ) |∉| X" using ex_fresh[of ℬ X] by blast
  ultimately have "open0_Var (x, ℬ) (close0_Var (''bool'', ℬ) (constant0 T)) ::: U" by simp
  then have "open0_Var (''bool'', ℬ) (close0_Var (''bool'', ℬ) (constant0 T)) ::: U"
    using rename_welltyped[of ‹open0_Var (x, ℬ) (close0_Var (''bool'', ℬ) (constant0 T))›
       U x ℬ "''bool''"]
    by (auto simp: subst_open subst_fresh)
  then show "U = T" by auto
qed (auto intro!: welltyped_Abs_fresh)

lemma welltyped_Seq_iff[simp]: "e1 ? e2 ::: T ⟷ (T = ℬ ∧ e1 ::: ℬ ∧ e2 ::: ℬ)"
  by auto

lemma welltyped_Seqs_iff[simp]: "es ?? e ::: T ⟷
  ((es ≠ [] ⟶ T = ℬ) ∧ (∀e ∈ set es. e ::: ℬ) ∧ e ::: T)"
  by (induct es arbitrary: e) (auto simp: Seqs_def)

lemma welltyped_App_iff[simp]: "f ⋅ t ::: U ⟷ (∃T. f ::: T → U ∧ t ::: T)"
  by auto

lemma welltyped_Apps_iff[simp]: "f ∙ ts ::: U ⟷ (∃Ts. f ::: Ts →→ U ∧ list_all2 (:::) ts Ts)"
  by (induct ts arbitrary: f) (auto 0 3 simp: mk_fun_def list_all2_Cons1 intro: exI[of _ "_ # _"])

lemma eq_mk_fun_iff[simp]: "T = Ts →→ ℬ ⟷ Ts = dest_fun T"
  by auto

lemma map_nth_eq_drop_take[simp]: "j ≤ length xs ⟹ map (nth xs) [i ..< j] = drop i (take j xs)"
  by (induct j) (auto simp: take_Suc_conv_app_nth)

lemma dest_fun_π_0: "i < ar T ⟹ dest_fun (π T i 0) = nth_drop i (dest_fun T)"
  by auto

lemma welltyped_E: "E T i ::: ε T i" and welltyped_P: "P T i j ::: T → π T i j"
proof (induct T i and T i j rule: E_P.induct)
  case (1 T i)
  note P.simps[simp del] π.simps[simp del] ε_def[simp] nth_drop_def[simp] nth_arg_def[simp]
  from 1(1)[OF _ refl refl refl refl refl refl refl refl refl]
       1(2)[OF _ refl refl refl refl refl refl refl refl refl]
  show ?case
    by (auto 0 4 simp: Let_def o_def take_map[symmetric] drop_map[symmetric]
      list_all2_conv_all_nth nth_append min_def dest_fun_π_0 π.simps[of T i]
      intro!: welltyped_Abs_fresh welltyped_Abss[of _ ℬ])
next
  case (2 T i)
  show ?case
    by (auto simp: Let_def take_map drop_map o_def list_all2_conv_all_nth nth_append nth_Cons'
       nth_drop_def nth_arg_def
      intro!: welltyped_constant welltyped_Abs_fresh welltyped_Abss[of _ ℬ])
next
  case (3 T i j)
  note E.simps[simp del] π.simps[simp del] Abss_Cons[simp del] ε_def[simp]
    nth_drop_def[simp] nth_arg_def[simp]
  from 3(1)[OF _ refl refl refl refl refl refl refl refl refl refl refl]
  show ?case
    by (auto 0 3 simp: Let_def o_def take_map[symmetric] drop_map[symmetric]
      list_all2_conv_all_nth nth_append nth_Cons' min_def π.simps[of T i]
      intro!: welltyped_Abs_fresh welltyped_Abss[of _ ℬ])
qed

lemma δ_gt_0[simp]: "T ≠ ℬ ⟹ HMSet {#} < δ T"
  by (cases T) auto

lemma mset_nth_drop_less: "i < length xs ⟹ mset (nth_drop i xs) < mset xs"
  by (induct xs arbitrary: i) (auto simp: take_Cons' nth_drop_def gr0_conv_Suc)

lemma map_nth_drop: "i < length xs ⟹ map f (nth_drop i xs) = nth_drop i (map f xs)"
  by (induct xs arbitrary: i) (auto simp: take_Cons' nth_drop_def gr0_conv_Suc)

lemma empty_less_mset: "{#} < mset xs ⟷ xs ≠ []"
  by auto

lemma dest_fun_alt: "dest_fun T = map (λi. T !- i) [0..<ar T]"
  unfolding list_eq_iff_nth_eq nth_arg_def by auto

context notes π.simps[simp del] notes One_nat_def[simp del] begin

lemma δ_π:
  assumes "i < ar T" "j ≤ ar (T !- i)"
  shows "δ (π T i j) < δ T"
using assms proof (induct T i j rule: π_induct)
  fix T i
  assume "i < ar T"
  then show "δ (π T i 0) < δ T"
    by (subst (2) mk_fun_dest_fun[symmetric, of T], unfold δ_mk_fun)
      (auto simp: δ_mk_fun mset_map[symmetric] take_map[symmetric] drop_map[symmetric] π.simps
        mset_nth_drop_less map_nth_drop simp del: mset_map)
next
  fix T i j
  let ?Ti = "T !- i"
  assume [rule_format, simp]: "i < ar T" "j < ar ?Ti" "δ (π ?Ti j 0) < δ ?Ti"
    "∀k < ar (?Ti !- j). δ (π ?Ti j (k + 1)) < δ ?Ti"
  define X and Y and M where
    [simp]: "X = {#δ ?Ti#}" and
    [simp]: "Y = {#δ (π ?Ti j 0)#} + {#δ (π ?Ti j (k + 1)). k ∈# mset [0 ..< ar (?Ti !- j)]#}" and
    [simp]: "M ≡ {# δ z. z ∈# mset (nth_drop i (dest_fun T))#}"
  have "δ (π T i (j + 1)) = HMSet (Y + M)"
    by (auto simp: One_nat_def π.simps δ_mk_fun)
  also have "Y + M < X + M"
    unfolding less_multiset⇩D⇩M by (rule exI[of _ "X"], rule exI[of _ "Y"]) auto
  also have "HMSet (X + M) = δ T"
    unfolding M_def
    by (subst (2) mk_fun_dest_fun[symmetric, of T], subst (2) id_take_nth_drop[of i "dest_fun T"])
      (auto simp: δ_mk_fun nth_arg_def nth_drop_def)
  finally show "δ (π T i (j + 1)) < δ T" by simp
qed

end

end