# Theory SystemF

```section "Semantics and type soundness for System F"

theory SystemF
imports Main "HOL-Library.FSet"
begin

subsection "Syntax and values"

type_synonym name = nat

datatype ty = TVar nat | TNat | Fun ty ty (infix "→" 60) | Forall ty

datatype exp = EVar name | ENat nat | ELam ty exp | EApp exp exp
| EAbs exp  | EInst exp ty | EFix ty exp

datatype val = VNat nat | Fun "(val × val) fset" | Abs "val option" | Wrong

fun val_le :: "val ⇒ val ⇒ bool" (infix "⊑" 52) where
"(VNat n) ⊑ (VNat n') = (n = n')" |
"(Fun f) ⊑ (Fun f') = (fset f ⊆ fset f')" |
"(Abs None) ⊑ (Abs None) = True" |
"Abs (Some v) ⊑ Abs (Some v') = v ⊑ v'" |
"Wrong ⊑ Wrong = True" |
"(v::val) ⊑ v' = False"

definition set_bind :: "'a set ⇒ ('a ⇒ 'b set) ⇒ 'b set" where
"set_bind m f ≡ { v. ∃ v'. v' ∈ m ∧ v ∈ f v' }"
declare set_bind_def[simp]

syntax "_set_bind" :: "[pttrns,'a set,'b] ⇒ 'c" ("(_ ← _;//_)" 0)
translations "P ← E; F" ⇌ "CONST set_bind E (λP. F)"

definition errset_bind :: "val set ⇒ (val ⇒ val set) ⇒ val set" where
"errset_bind m f ≡ { v. ∃ v'. v' ∈ m ∧ v' ≠ Wrong ∧ v ∈ f v' } ∪ {v. v = Wrong ∧ Wrong ∈ m }"
declare errset_bind_def[simp]

syntax "_errset_bind" :: "[pttrns,val set,val] ⇒ 'c" ("(_ := _;//_)" 0)
translations "P := E; F" ⇌ "CONST errset_bind E (λP. F)"

definition return :: "val ⇒ val set" where
"return v ≡ {v'. v' ⊑ v }"
declare return_def[simp]

subsection "Denotational semantics"

type_synonym tyenv = "(val set) list"
type_synonym env = "val list"

inductive iterate :: "(env ⇒ val set) ⇒ env ⇒ val ⇒ bool" where
iterate_none[intro!]: "iterate Ee ρ (Fun {||})" |
iterate_again[intro!]: "⟦ iterate Ee ρ f; f' ∈ Ee (f#ρ) ⟧ ⟹ iterate Ee ρ f'"

abbreviation apply_fun :: "val set ⇒ val set ⇒ val set" where
"apply_fun V1 V2 ≡ (v1 := V1; v2 := V2;
case v1 of Fun f ⇒
(v2',v3') ← fset f;
if v2' ⊑ v2 then return v3' else {}
| _ ⇒ return Wrong)"

fun E :: "exp ⇒ env ⇒ val set" where
Enat: "E (ENat n) ρ = return (VNat n)" |
Evar: "E (EVar n) ρ = return (ρ!n)" |
Elam: "E (ELam τ e) ρ = {v. ∃ f. v = Fun f ∧ (∀ v1 v2'. (v1,v2') ∈ fset f ⟶
(∃ v2. v2 ∈ E e (v1#ρ) ∧ v2' ⊑ v2)) }" |
Eapp: "E (EApp e1 e2) ρ = apply_fun (E e1 ρ) (E e2 ρ)" |
Efix: "E (EFix τ e) ρ = { v. iterate (E e) ρ v }" |
Eabs: "E (EAbs e) ρ = {v. (∃ v'. v = Abs (Some v') ∧ v' ∈ E e ρ)
∨ (v = Abs None ∧ E e ρ = {}) }" |
Einst: "E (EInst e τ) ρ =
(v := E e ρ;
case v of
Abs None ⇒ {}
| Abs (Some v') ⇒ return v'
| _ ⇒ return Wrong)"

subsection "Types: substitution and semantics"

fun shift :: "nat ⇒ nat ⇒ ty ⇒ ty" where
"shift k c TNat = TNat" |
"shift k c (TVar n) = (if c ≤ n then TVar (n + k) else TVar n)" |
"shift k c (σ → σ') = (shift k c σ) → (shift k c σ')" |
"shift k c (Forall σ) = Forall (shift k (Suc c) σ)"

fun subst :: "nat ⇒ ty ⇒ ty ⇒ ty" where
"subst k τ TNat = TNat" |
"subst k τ (TVar n) = (if k = n then τ
else if k < n then TVar (n - 1)
else TVar n)" |
"subst k τ (σ → σ') = (subst k τ σ) → (subst k τ σ')" |
"subst k τ (Forall σ) = Forall (subst (Suc k) (shift (Suc 0) 0 τ) σ)"

fun T :: "ty ⇒ tyenv ⇒ val set" where
Tnat: "T TNat ρ = {v. ∃ n. v = VNat n }" |
Tvar: "T (TVar n) ρ = (if n < length ρ then
{v. ∃ v'. v'∈ρ!n ∧ v ⊑ v' ∧ v ≠ Wrong}
else {})" |
Tfun: "T (σ → τ) ρ = {v. ∃ f. v = Fun f ∧
(∀ v1 v2'.(v1,v2')∈fset f ⟶
v1∈T σ ρ⟶(∃ v2. v2 ∈ T τ ρ ∧ v2' ⊑ v2))}" |
Tall: "T (Forall τ) ρ = {v. (∃v'. v = Abs (Some v') ∧ (∀ V. v' ∈ T τ (V#ρ)))
∨ v = Abs None }"

subsection "Type system"

type_synonym tyctx = "(ty × nat) list × nat"

definition wf_tyvar :: "tyctx ⇒ nat ⇒ bool" where
"wf_tyvar Γ n ≡ n < snd Γ"
definition push_ty :: "ty ⇒ tyctx ⇒ tyctx" where
"push_ty τ Γ ≡ ((τ,snd Γ) # fst Γ, snd Γ)"
definition push_tyvar :: "tyctx ⇒ tyctx" where
"push_tyvar Γ ≡ (fst Γ, Suc (snd Γ))"

definition good_ctx :: "tyctx ⇒ bool" where
"good_ctx Γ ≡ ∀ n. n < length (fst Γ) ⟶ snd ((fst Γ) ! n) ≤ snd Γ"

definition lookup :: "tyctx ⇒ nat ⇒ ty option" where
"lookup Γ n ≡ (if n < length (fst Γ) then
let k = snd Γ - snd ((fst Γ)!n) in
Some (shift k 0 (fst ((fst Γ)!n)))
else None)"

inductive well_typed :: "tyctx ⇒ exp ⇒ ty ⇒ bool" ("_ ⊢ _ : _" [55,55,55] 54) where
wtnat[intro!]: "Γ ⊢ ENat n : TNat" |
wtvar[intro!]: "⟦ lookup Γ n = Some τ ⟧ ⟹ Γ ⊢ EVar n : τ" |
wtapp[intro!]: "⟦ Γ ⊢ e : σ → τ; Γ ⊢ e' : σ ⟧ ⟹ Γ ⊢ EApp e e' : τ" |
wtlam[intro!]: "⟦ push_ty σ Γ ⊢ e : τ ⟧ ⟹ Γ ⊢ ELam σ e : σ → τ" |
wtfix[intro!]: "⟦ push_ty (σ→τ) Γ ⊢ e : σ→τ ⟧ ⟹ Γ ⊢ EFix (σ → τ) e : σ → τ" |
wtabs[intro!]: "⟦ push_tyvar Γ ⊢ e : τ ⟧ ⟹ Γ ⊢ EAbs e : Forall τ" |
wtinst[intro!]: "⟦ Γ ⊢ e : Forall τ ⟧ ⟹ Γ ⊢ EInst e σ : (subst 0 σ τ)"

inductive wfenv :: "env ⇒ tyenv ⇒ tyctx ⇒ bool" ("⊢ _,_ : _" [55,55,55] 54) where
wfnil[intro!]: "⊢ [],[] : ([],0)" |
wfvbind[intro!]: "⟦ ⊢ ρ,η : Γ; v ∈ T τ η ⟧ ⟹ ⊢  (v#ρ),η : push_ty τ Γ" |
wftbind[intro!]: "⟦ ⊢ ρ,η : Γ ⟧ ⟹ ⊢ ρ, (V#η) : push_tyvar Γ"

inductive_cases
wtnat_inv[elim!]: "Γ ⊢ ENat n : τ" and
wtvar_inv[elim!]: "Γ ⊢ EVar n : τ" and
wtapp_inv[elim!]: "Γ ⊢ EApp e e' : τ" and
wtlam_inv[elim!]: "Γ ⊢ ELam σ e : τ" and
wtfix_inv[elim!]: "Γ ⊢ EFix σ e : τ" and
wtabs_inv[elim!]: "Γ ⊢ EAbs e : τ" and
wtinst_inv[elim!]: "Γ ⊢ EInst e σ : τ"

lemma wfenv_good_ctx: "⊢ ρ,η : Γ ⟹ good_ctx Γ"
proof (induction rule: wfenv.induct)
case wfnil
then show ?case by (force simp: good_ctx_def)
next
case (wfvbind ρ η Γ v τ)
then show ?case
apply (simp add: good_ctx_def push_ty_def) apply (cases Γ) apply simp
apply clarify apply (rename_tac n) apply (case_tac n) apply force apply force done
next
case (wftbind ρ η Γ V)
then show ?case
apply (simp add: good_ctx_def push_tyvar_def) apply (cases Γ) apply simp
apply clarify apply (rename_tac n) apply (case_tac n) apply auto done
qed

subsection "Well-typed Programs don't go wrong"

lemma nth_append1[simp]: "n < length ρ1 ⟹ (ρ1@ρ2)!n = ρ1!n"
proof (induction ρ1 arbitrary: ρ2 n)
case Nil
then show ?case by auto
next
case (Cons a ρ1)
then show ?case by (cases n) auto
qed

lemma nth_append2[simp]: "n ≥ length ρ1 ⟹ (ρ1@ρ2)!n = ρ2!(n - length ρ1)"
proof (induction ρ1 arbitrary: ρ2 n)
case Nil
then show ?case by auto
next
case (Cons a ρ1)
then show ?case by (cases n) auto
qed

lemma shift_append_preserves_T_aux:
shows "T τ (ρ1@ρ3) = T (shift (length ρ2) (length ρ1) τ) (ρ1@ρ2@ρ3)"
proof (induction τ arbitrary: ρ1 ρ2 ρ3)
case (Forall τ)
then show ?case
apply simp
apply (rule equalityI) apply (rule subsetI) apply (simp only: mem_Collect_eq)
apply (erule disjE) apply (erule exE) apply (erule conjE) apply (rule disjI1)
apply (rename_tac x v')
apply (rule_tac x=v' in exI) apply simp apply clarify
apply (rename_tac V)
apply (erule_tac x=V in allE)
apply (subgoal_tac "T τ ((V#ρ1) @ ρ3) =
T (shift (length ρ2) (length (V#ρ1)) τ) ((V#ρ1) @ ρ2 @ ρ3)")
prefer 2 apply blast apply force
apply (rule disjI2) apply force
apply (rule subsetI) apply (simp only: mem_Collect_eq)
apply (erule disjE) apply (erule exE) apply (erule conjE) apply (rule disjI1)
apply (rename_tac x v')
apply (rule_tac x=v' in exI) apply simp apply clarify
apply (rename_tac V)
apply (erule_tac x=V in allE)
apply (subgoal_tac "T τ ((V#ρ1) @ ρ3) =
T (shift (length ρ2) (length (V#ρ1)) τ) ((V#ρ1) @ ρ2 @ ρ3)")
prefer 2 apply blast apply force
apply (rule disjI2) apply force done
qed force+

lemma shift_append_preserves_T: shows "T τ ρ3 = T (shift (length ρ2) 0 τ) (ρ2@ρ3)"
using shift_append_preserves_T_aux[of τ "[]" ρ3 ρ2] by auto

lemma drop_shift_preserves_T:
assumes k: "k ≤ length ρ" shows "T τ (drop k ρ) = T (shift k 0 τ) ρ"
proof -
let ?r2 = "take k ρ" and ?r3 = "drop k ρ"
have 1: "T τ (?r3) = T (shift (length ?r2) 0 τ) (?r2@?r3)"
using shift_append_preserves_T_aux[of τ "[]" ?r3 ?r2] by simp
have 2: "?r2@?r3 = ρ" by simp
from k have 3: "length ?r2 = k" by simp
from 1 2 3 show ?thesis by simp
qed

lemma shift_cons_preserves_T: shows "T τ ρ = T (shift (Suc 0) 0 τ) (b#ρ)"
using drop_shift_preserves_T[of "Suc 0" "b#ρ" τ] by simp

lemma compose_shift: shows "shift (j+k) c τ = shift j c (shift k c τ)"
by (induction τ arbitrary: j k c) auto

lemma shift_zero_id[simp]: "shift 0 c τ = τ"
by (induction τ arbitrary: c) auto

lemma lookup_wfenv: assumes r_g: "⊢ ρ,η : Γ" and ln: "lookup Γ n = Some τ"
shows "∃ v. ρ!n = v ∧ v ∈ T τ η"
using r_g ln
proof (induction ρ η Γ arbitrary: n τ rule: wfenv.induct)
case wfnil
then show ?case unfolding lookup_def by force
next
case (wfvbind ρ η Γ v τ')
from wfvbind(2) have vtp: "v ∈ T τ' η" .
show ?case
proof (cases n)
case 0
from 0 wfvbind(4) have t: "τ =  shift 0 0 τ'" unfolding lookup_def by (simp add: push_ty_def)
from 0 vtp t show ?thesis by simp
next
case (Suc n')
let ?G = "push_ty τ' Γ"
from wfvbind(4) Suc obtain σ k where gnp: "(fst Γ)!n' = (σ,k)" and t: "τ = shift (snd Γ - k) 0 σ"
and npg: "n' < length (fst Γ)"
unfolding lookup_def push_ty_def apply (cases "n' < length (fst Γ)") apply auto
apply (cases "fst Γ ! n'") apply auto done
from gnp Suc npg t have ln: "lookup Γ n' = Some τ" unfolding lookup_def by auto
from wfvbind(3) ln obtain v' where rnp: "ρ!n' = v'" and vt: "v' ∈ T τ η" by blast
from Suc rnp vt show ?thesis by simp
qed
next
case (wftbind ρ η Γ V)
let ?a = "fst Γ" and ?b = "snd Γ"
obtain σ k where s: "σ = fst (fst Γ ! n)" and k: "k = snd (fst Γ ! n)" by auto
from wftbind(3) s k have t: "τ = shift (Suc ?b - k) 0 σ" and nl: "n < length (fst Γ)"
unfolding push_tyvar_def lookup_def apply auto
apply (case_tac "n < length (fst Γ)", auto)+ done
let ?t = "shift (?b - k) 0 (fst (?a ! n))"
from wftbind(3) k have ln: "lookup Γ n = Some ?t"
unfolding push_tyvar_def lookup_def
apply (cases Γ) apply (rename_tac k' G) apply simp apply (case_tac "n < length k'") by auto
from wftbind(2) ln obtain v' where rn_vp: "ρ ! n = v'" and vp_t: "v' ∈ T ?t η" by blast
from vp_t have "v' ∈ T (shift (Suc 0) 0 ?t) (V # η)" using shift_cons_preserves_T by auto
hence vp_t2: "v' ∈ T (shift (Suc 0 + (?b - k)) 0 (fst (?a!n))) (V # η)"
using compose_shift[of "Suc 0" "?b - k" 0 "fst (?a!n)"] by simp
from wftbind(1) have "good_ctx Γ" using wfenv_good_ctx by blast
from this k nl have "?b ≥ k" unfolding good_ctx_def by auto
from this have "Suc 0 + (?b - k) = Suc ?b - k" by simp
from this vp_t2 have vp_t3: "v' ∈ T (shift (Suc ?b - k) 0 (fst (?a!n))) (V # η)" by simp
from rn_vp vp_t3 t s show ?case by auto
qed

lemma less_wrong[elim!]: "⟦ v ⊑ Wrong; v = Wrong ⟹ P ⟧ ⟹ P"
by (case_tac v) auto

lemma less_nat[elim!]: "⟦ v ⊑ VNat n; v = VNat n ⟹ P ⟧ ⟹ P"
by (case_tac v) auto

lemma less_fun[elim!]: "⟦ v ⊑ Fun f; ⋀ f'. ⟦ v = Fun f'; fset f' ⊆ fset f ⟧ ⟹ P ⟧ ⟹ P"
by (case_tac v) auto

lemma less_refl[simp]: "v ⊑ v"
proof (induction v)
case (Abs v')
then show ?case by (cases v') auto
qed force+

lemma less_trans: fixes v1::val and v2::val and v3::val
shows "⟦ v1 ⊑ v2; v2 ⊑ v3 ⟧ ⟹ v1 ⊑ v3"
proof (induction v2 arbitrary: v1 v3)
case (VNat n)
then show ?case by (cases v1) auto
next
case (Fun t)
then show ?case
apply (cases v1)
apply force
apply simp
apply (cases v3)
apply auto done
next
case (Abs v)
then show ?case
apply (cases v1) apply force apply force apply (case_tac v3) apply force apply force
apply (rename_tac v' v3') apply simp apply (cases v) apply (case_tac v')
apply force apply force
apply (case_tac v3') apply force apply simp apply (case_tac v')
apply force+ done
next
case Wrong
then show ?case by auto
qed

lemma T_down_closed: assumes vt: "v ∈ T τ η" and vp_v: "v' ⊑ v"
shows "v' ∈ T τ η"
using vt vp_v
proof (induction τ arbitrary: v v' η)
case (TVar x v v' η)
then show ?case
apply simp apply (case_tac "x < length η")
apply simp apply clarify
apply (rule_tac x=v' in exI)
apply simp apply (rule conjI)
apply (rule less_trans) apply blast apply blast
apply (case_tac v')
apply (case_tac v)
apply force+
apply (case_tac v)
apply force+ done
next
case TNat
then show ?case by auto
next
case (Fun τ1 τ2)
then show ?case apply simp apply clarify apply (rule_tac x=f' in exI) apply fastforce done
next
case (Forall τ v v' η)
then show ?case
apply simp apply (erule disjE) apply clarify apply (cases v') apply force apply force
apply simp apply (rename_tac v'') apply (case_tac v'') apply simp apply simp apply clarify
apply (erule_tac x=V in allE) apply blast
apply force
apply simp
apply (case_tac v') apply auto done
qed

lemma wrong_not_in_T: "Wrong ∉ T τ η"
by (induction τ) auto

lemma fun_app: assumes vmn: "V ⊆ T (m → n) η" and v2s: "V' ⊆ T m η"
shows "apply_fun V V' ⊆ T n η"
using vmn v2s apply simp apply (rule conjI)
prefer 2 apply force
apply clarify
apply (erule disjE)
prefer 2 using wrong_not_in_T apply blast
apply clarify apply (rename_tac v'') apply (case_tac v') apply auto
apply (rename_tac v1 v2) apply (case_tac "v1 ⊑ v''") apply auto
apply (subgoal_tac "∀v1 v2'.
(v1, v2') ∈ fset x2 ⟶ v1 ∈ T m η ⟶ (∃v2. v2 ∈ T n η ∧ v2' ⊑ v2)")
prefer 2 apply blast
apply (rename_tac v1 v2)
apply (erule_tac x=v1 in allE) apply (erule_tac x=v2 in allE) apply (erule impE) apply simp
apply (erule impE) using T_down_closed apply blast
apply clarify  using T_down_closed apply blast
done

lemma T_eta: "{v. ∃v'. v' ∈ T σ (η) ∧ v ⊑ v' ∧ v ≠ Wrong} = T σ η"
apply auto
using T_down_closed apply blast
apply (rename_tac v)
apply (rule_tac x=v in exI)
apply simp
using wrong_not_in_T apply blast done

lemma compositionality: "T τ (η1 @ (T σ (η1@η2)) # η2) = T (subst (length η1) σ τ) (η1@η2)"
proof (induction τ arbitrary: σ η1 η2)
case (TVar x)
then show ?case
apply (case_tac "length η1 = x") apply simp using T_eta apply blast
apply (case_tac "length η1 < x") apply (subgoal_tac "∃ x'. x = Suc x'") prefer 2
apply (cases x)
apply force+
done
next
case TNat
then show ?case by auto
next
case (Fun τ1 τ2)
then show ?case by auto
next
case (Forall τ)
show "T (Forall τ) (η1 @ T σ (η1 @ η2) # η2) =
T (subst (length η1) σ (Forall τ)) (η1 @ η2)"
apply simp
apply (rule equalityI) apply (rule subsetI) apply (simp only: mem_Collect_eq)
apply (erule disjE) prefer 2 apply force apply (erule exE) apply (erule conjE) apply (rule disjI1)
apply (rule_tac x=v' in exI) apply simp apply clarify
apply (erule_tac x="V" in allE)
prefer 2 apply (rule subsetI) apply (simp only: mem_Collect_eq)
apply (erule disjE) prefer 2 apply force apply (erule exE) apply (erule conjE) apply (rule disjI1)
apply (rule_tac x=v' in exI) apply simp apply clarify
apply (erule_tac x="V" in allE)
defer
proof -
fix x v' V
let ?L1 = "length η1" and ?R1 = "V#η1" and ?s = "shift (Suc 0) 0 σ"
assume 1: "v' ∈ T τ (V # (η1 @ T σ (η1 @ η2) # η2))"
from 1 have a: "v' ∈ T τ (?R1 @ T σ (η1@η2) # η2)" by simp

have b: "T σ (η1@η2) = T ?s (V#(η1@η2))" by (rule shift_cons_preserves_T)
from a b have c: "v' ∈ T τ (?R1 @ T ?s (?R1 @ η2) # η2)" by simp
from Forall[of ?R1 ?s η2] have 2: "T τ (?R1 @ T ?s (?R1 @ η2) # η2) =
T (subst (length ?R1) ?s τ) (?R1 @ η2)" by simp
from c 2 show "v' ∈ T (subst (Suc ?L1) ?s τ) (V # (η1 @ η2))" by simp
next
fix x v' V
let ?L1 = "length η1" and ?R1 = "V#η1" and ?s = "shift (Suc 0) 0 σ"
assume 1: "v' ∈ T (subst (Suc (length η1)) (shift (Suc 0) 0 σ) τ) (V # η1 @ η2)"
from Forall[of ?R1 ?s η2] have 2: "T τ (?R1 @ T ?s (?R1 @ η2) # η2) =
T (subst (length ?R1) ?s τ) (?R1 @ η2)" by simp
from 1 2 have 3: "v' ∈ T τ (?R1 @ T ?s (?R1 @ η2) # η2)" by simp
have b: "T σ (η1@η2) = T ?s (V#(η1@η2))" by (rule shift_cons_preserves_T)
from 3 b have a: "v' ∈ T τ (?R1 @ T σ (η1@η2) # η2)" by simp
from this show "v' ∈ T τ (V # η1 @ T σ (η1 @ η2) # η2)" by simp
qed
qed

lemma iterate_sound:
assumes it: "iterate Ee ρ v"
and IH: "∀ v. v ∈ T (σ→τ) η ⟶ Ee (v#ρ) ⊆ T (σ→τ) η"
shows "v ∈ T (σ→τ) η" using it IH
proof (induction rule: iterate.induct)
case (iterate_none Ee ρ)
then show ?case by auto
next
case (iterate_again Ee ρ f f')
from iterate_again have f_st: "f ∈ T (σ→τ) η" by blast
from iterate_again f_st have "Ee (f#ρ) ⊆ T (σ→τ) η" by blast
from this iterate_again show ?case by auto
qed

theorem welltyped_dont_go_wrong:
assumes wte: "Γ ⊢ e : τ" and wfr: "⊢ ρ,η : Γ"
shows "E e ρ ⊆ T τ η"
using wte wfr
proof (induction Γ e τ arbitrary: ρ η rule: well_typed.induct)
case (wtnat Γ n ρ η)
then show ?case by auto
next
case (wtvar Γ n τ ρ η)
from wtvar obtain v where lx: "ρ ! n = v" and vt: "v ∈ T τ η"using lookup_wfenv by blast
from lx vt show ?case apply auto using T_down_closed[of "ρ!n" τ "η"] by blast
next
case (wtapp Γ e σ τ e' ρ η)
from wtapp have Ee: "E e ρ ⊆ T (σ → τ) η" by blast
from wtapp have Eep: "E e' ρ ⊆ T σ η" by blast
from Ee Eep show ?case using fun_app by simp
next
case (wtlam σ Γ e τ ρ η)
show ?case
apply simp apply (rule subsetI) apply clarify apply (rule_tac x=f in exI) apply simp
apply clarify apply (erule_tac x=v1 in allE) apply (erule_tac x=v2' in allE) apply clarify
proof -
fix f v1 v2' v2
assume v1_T: "v1 ∈ T σ η" and v2_E: "v2 ∈ E e (v1#ρ)" and v2p_v2: "v2' ⊑ v2"
let ?r = "v1#ρ"
from wtlam(3) v1_T have 1: "⊢ v1#ρ,η : push_ty σ Γ" by blast
from wtlam(2) 1 have IH: "E e (v1#ρ) ⊆ T τ η" by blast
from IH v2_E have v2_T: "v2 ∈ T τ η" by blast
from v2_T have v2_Tb: "v2 ∈ T τ η" by simp
from v2_Tb v2p_v2 show "∃v2. v2 ∈ T τ η ∧ v2' ⊑ v2 " by blast
qed
next
case (wtfix σ τ Γ e ρ η)
have "∀ v. iterate (E e) ρ v ⟶ v ∈ T (σ → τ) η"
proof clarify
fix v assume it: "iterate (E e) ρ v"
have 1: " ∀v. v ∈ T (σ → τ) η ⟶ E e (v#ρ) ⊆ T (σ → τ) η"
proof clarify
fix v' v'' assume 2: "v' ∈ T (σ→τ) η" and 3: "v'' ∈ E e (v'#ρ)"
from wtfix(3) 2 have "⊢ (v'#ρ),η : push_ty (σ → τ) Γ" by blast
from wtfix(2) this have IH: "E e (v'#ρ) ⊆ T (σ→τ) η" by blast
from 3 IH have "v'' ∈ T (σ→τ)  η" by blast
from this show "v'' ∈ T (σ → τ) η" by simp
qed
from it 1 show "v ∈ T (σ → τ) η" using iterate_sound[of "E e" ρ v σ τ] by blast
qed
from this show ?case by auto
next
case (wtabs Γ e τ ρ η)
show ?case apply simp apply (rule subsetI) apply (simp only: mem_Collect_eq)
apply (erule disjE) apply (erule exE) apply (erule conjE) apply (rule disjI1)
apply (rule_tac x=v' in exI) apply simp apply clarify prefer 2 apply (rule disjI2)
apply force
proof -
fix x v' V assume 2: "v' ∈ E e ρ"
from wtabs(3) have 3: " ⊢ ρ,(V#η) : push_tyvar Γ" by blast
from wtabs(2) 3 have IH: "E e ρ ⊆ T τ (V#η)" by blast
from 2 IH show "v' ∈ T τ (V#η)" by (case_tac ρ) auto
qed
next
case (wtinst Γ e τ σ ρ η)
from wtinst(2) wtinst(3) have IH: "E e ρ ⊆ T (Forall τ) η" by blast
show ?case
apply simp apply (rule conjI)
apply (rule subsetI) apply (simp only: mem_Collect_eq) apply (erule exE)
apply (erule conjE)+
proof -
fix x v' assume vp_E: "v' ∈ E e ρ" and vp_w: "v' ≠ Wrong" and
x: "x ∈ (case v' of Abs None ⇒ {} | Abs (Some xa) ⇒ return xa
| _ ⇒ {v'. v' ⊑ Wrong})"
from IH vp_E have vp_T: "v' ∈ T (Forall τ) η" by blast
from vp_T have "(∃v''. v' = Abs (Some v'') ∧ (∀ V. v'' ∈ T τ (V#η)))
∨ v' = Abs None" by simp
from this show "x ∈ T (subst 0 σ τ) η"
proof
assume "∃v''. v' = Abs (Some v'') ∧ (∀ V. v'' ∈ T τ (V#η))"
from this obtain v'' where vp: "v' = Abs (Some v'')" and
vpp_T: "∀ V. v'' ∈ T τ (V#η)" by blast
from vp x have x_vpp: "x ⊑ v''" by auto
let ?V = "T σ η"
from vpp_T have "v'' ∈ T τ (?V#η)" by blast
from this have "v'' ∈ T (subst 0 σ τ) η" using compositionality[of τ "[]" σ] by simp
from this x_vpp show "x ∈ T (subst 0 σ τ) η" using T_down_closed by blast
next
assume vp: "v' = Abs None"
from vp x show "x ∈ T (subst 0 σ τ) η" by simp
qed
next
from IH show "{v. v = Wrong ∧ Wrong ∈ E e ρ} ⊆ T (subst 0 σ τ) η"
using wrong_not_in_T by auto
qed
qed

end

```