# Theory Unary_PCF

theory Unary_PCF
imports FSet Countable_Set_Type Hereditary_Multiset List_Index
```(*  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 simp: fmember.rep_eq)
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ß'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
```