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"  

subsection "Set monad"

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)
syntax_consts "_set_bind" ⇌ set_bind
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)
syntax_consts "_errset_bind" ⇌ errset_bind
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