theory SystemF
imports Main
begin

section "Option Monad"

definition
  option_bind :: "['a option, 'a => 'b option] => 'b option" where
  "option_bind m f = (case m of None => None | Some r => f r)"
declare option_bind_def[simp]

syntax "_option_bind" :: "[pttrns,'a option,'b] => 'c" ("(_ := _;//_)" 0)
translations "P := E; F" == "CONST option_bind E (%P. F)"

definition return :: "'a \<Rightarrow> 'a option" where
  "return x \<equiv> Some x"
declare return_def[simp]
definition error :: "'a option" where
  "error \<equiv> None"
declare error_def[simp]

section "Syntax"

type_synonym name = nat

datatype ty
  = IntT
  | BoolT
  | ArrowT ty ty (infixr "\<rightarrow>" 200)
  | AllT ty
  | BVar nat
  | FVar name

datatype const
  = IntC int
  | BoolC bool

datatype opr
  = Succ
  | Prev
  | IsZero

datatype stmt
  = SLet name expr stmt
  | SRet expr
  | SCall name expr expr stmt
  | SInst name expr ty stmt

and expr 
  = Var name
  | Const const
  | PrimApp opr expr
  | Lam name stmt ty
  | TyAbs name stmt ty

datatype val
  = VConst const
  | Boxed const name
  | Closure nat stmt "(name \<times> val) list" "(name \<times> ty) list" ty ty
  | TAbs name stmt "(name \<times> val) list" "(name \<times> ty) list" ty ty

section "Operational Semantics"

type_synonym env = "(name \<times> val) list"
type_synonym tymap = "(name \<times> ty) list"
type_synonym stack = "(name \<times> ty \<times> ty \<times> stmt \<times> env \<times> tymap) list"
type_synonym state = "stmt \<times> env \<times> tymap \<times> stack"

fun lookup :: "'a \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b option" where
  "lookup x [] = None" |
  "lookup x ((y,v)#bs) = (if x = y then Some v else lookup x bs)"

fun delta :: "opr \<Rightarrow> val \<Rightarrow> val option" where
  "delta Succ (VConst (IntC n)) = Some (VConst (IntC (n + 1)))" |
  "delta Prev (VConst (IntC n)) = Some (VConst (IntC (n - 1)))" |
  "delta IsZero (VConst (IntC n)) = Some (VConst (BoolC (n = 0)))" |
  "delta f v = None"

fun cast :: "val \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> val" where
  castcf:"cast (VConst c) A (FVar \<alpha>) = Boxed c \<alpha>" |
  castc: "cast (VConst c) A B = VConst c" |
  castbf: "cast (Boxed c \<alpha>) A (FVar \<beta>) = Boxed c \<beta>" |
  castb: "cast (Boxed c \<alpha>) A B = VConst c" |
  castf: "cast (Closure x s \<rho> \<Sigma> A B) B' C = (Closure x s \<rho> \<Sigma> A C)" |
  casta: "cast (TAbs \<alpha> s \<rho> \<Sigma> A B) B' C = (TAbs \<alpha> s \<rho> \<Sigma> A C)"

fun eval :: "expr \<Rightarrow> env \<Rightarrow> tymap \<Rightarrow> val option" where
  evalv: "eval (Var x) \<rho> \<Sigma> = lookup x \<rho>" |
  evalc: "eval (Const c) \<rho> \<Sigma> = return (VConst c)" |
  evalp: "eval (PrimApp f e) \<rho> \<Sigma> = (v := eval e \<rho> \<Sigma>; delta f v)" |
  evall: "eval (Lam x s A) \<rho> \<Sigma> = return (Closure x s \<rho> \<Sigma> A A)" |
  evalt: "eval (TyAbs x s A) \<rho> \<Sigma> = return (TAbs x s \<rho> \<Sigma> A A)" 

primrec shift :: "nat \<Rightarrow> ty \<Rightarrow> ty" where
  "shift c IntT = IntT" |
  "shift c BoolT = BoolT" |
  "shift c (ArrowT T1 T2) = ArrowT (shift c T1) (shift c T2)" |
  "shift c (AllT T1) = AllT (shift (Suc c) T1)" |
  "shift c (BVar k) = (if k < c then BVar k else BVar (Suc k))" |
  "shift c (FVar x) = FVar x"

primrec bsub :: "nat \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty" where
  "bsub j S IntT = IntT" |
  "bsub j S BoolT = BoolT" |
  "bsub j S (ArrowT T1 T2) = ArrowT (bsub j S T1) (bsub j S T2)" |
  "bsub j S (AllT T1) = AllT (bsub (Suc j) (shift 0 S) T1)" |
  "bsub j S (BVar k) = (if k = j then S else BVar k)" |
  "bsub j S (FVar x) = FVar x"

abbreviation ty_bsub :: "ty \<Rightarrow> ty \<Rightarrow> ty" ("[_]_" [65,65] 64) where
  "[T1]T2 \<equiv> bsub 0 T1 T2"

text{* parallel type subsitution *}
primrec psub :: "tymap \<Rightarrow> ty \<Rightarrow> ty" where
  "psub \<Sigma> IntT = IntT" |
  "psub \<Sigma> BoolT = BoolT" |
  "psub \<Sigma> (ArrowT T1 T2) = ArrowT (psub \<Sigma> T1) (psub \<Sigma> T2)" |
  "psub \<Sigma> (AllT T) = AllT (psub \<Sigma> T)" |
  "psub \<Sigma> (BVar k) = BVar k" |
  "psub \<Sigma> (FVar x) = (case lookup x \<Sigma> of None \<Rightarrow> FVar x | Some T \<Rightarrow> T)"

fun step :: "state \<Rightarrow> state option" where
  "step (SLet x e s, \<rho>, \<Sigma>, k) =
    (v := eval e \<rho> \<Sigma>; 
     return (s, (x,v)#\<rho>, \<Sigma>, k))" |
  "step (SRet e, \<rho>, \<Sigma>, (x, S, T, s, \<rho>', \<Sigma>')#k) =
      (v := eval e \<rho> \<Sigma>;
       return (s, (x,cast v S T)#\<rho>', \<Sigma>', k))" |
  "step (SCall x e1 e2 s, \<rho>, \<Sigma>, k) =
     (v1 := eval e1 \<rho> \<Sigma>; v2 := eval e2 \<rho> \<Sigma>;
      case v1 of
        Closure y s' \<rho>' \<Sigma>' (S1\<rightarrow>S2) (T1\<rightarrow>T2) \<Rightarrow>
          return (s', (y,cast v2 T1 S1)#\<rho>', \<Sigma>', (x, S2, T2, s, \<rho>, \<Sigma>)#k)
      | _ \<Rightarrow> error)" |
  "step (SInst x e1 T s, \<rho>, \<Sigma>, k) =
     (v1 := eval e1 \<rho> \<Sigma>;
      case v1 of
        TAbs y s' \<rho>' \<Sigma>' (AllT S) (AllT T') \<Rightarrow>
          return (s', \<rho>', (y,psub \<Sigma> T)#\<Sigma>', (x, [FVar y]S, [T]T', s, \<rho>, \<Sigma>)#k)
      | _ \<Rightarrow> error)" |
  "step s = None"

datatype result = Fun | Poly | Con const | Error | TimeOut

primrec observe :: "val \<Rightarrow> result" where
  "observe (VConst c) = Con c" |
  "observe (Closure x s \<rho> \<Sigma> S T) = Fun" |
  "observe (TAbs x s \<rho> \<Sigma> S T) = Poly"

definition final :: "state \<Rightarrow> bool" where
  "final s \<equiv> (case s of (SRet e, \<rho>, \<Sigma>, []) \<Rightarrow> True | _ \<Rightarrow> False)"
declare final_def[simp]

fun steps :: "nat \<Rightarrow> state \<Rightarrow> result" where
  "steps 0 s = TimeOut" |
  "steps (Suc n) (SRet e, \<rho>, \<Sigma>, []) =
            (case eval e \<rho> \<Sigma> of
               None \<Rightarrow> Error
            | Some v \<Rightarrow> observe v)" |
  "steps (Suc n) s =
         (case step s of
           None \<Rightarrow> Error
         | Some s' \<Rightarrow> steps n s')"

definition run :: "stmt \<Rightarrow> result" where
  "run s \<equiv> steps 1000000 (s,[],[],[])"

section "Type System"

primrec close :: "name \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> ty" where
  "close x k IntT = IntT" |
  "close x k BoolT = BoolT" |
  "close x k (ArrowT T1 T2) = ArrowT (close x k T1) (close x k T2)" |
  "close x k (AllT T1) = AllT (close x (Suc k) T1)" |
  "close x k (BVar j) = BVar j" |
  "close x k (FVar y) = (if x = y then BVar k else FVar y)"

datatype bind = EVar ty | TVar
type_synonym ty_env = "(name \<times> bind) list"

primrec typeof :: "const \<Rightarrow> ty" where
  "typeof (IntC n) = IntT" |
  "typeof (BoolC b) = BoolT"

primrec typeof_opr :: "opr \<Rightarrow> ty" where
  "typeof_opr Succ = (IntT \<rightarrow> IntT)" |
  "typeof_opr Prev = (IntT \<rightarrow> IntT)" |
  "typeof_opr IsZero = (IntT \<rightarrow> BoolT)"

inductive wf_ty :: "ty_env \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> bool" ("_;_ \<turnstile> _ wf" [60,60,60] 59) where
  wfint[intro!]: "\<Gamma>;n \<turnstile> IntT wf" |
  wfbool[intro!]: "\<Gamma>;n \<turnstile> BoolT wf" |
  wffun[intro!]: "\<lbrakk> \<Gamma>;n \<turnstile> T1 wf; \<Gamma>;n \<turnstile> T2 wf \<rbrakk> \<Longrightarrow> \<Gamma>;n \<turnstile> (T1 \<rightarrow> T2) wf" |
  wfall[intro!]: "\<Gamma>;Suc n \<turnstile> T wf \<Longrightarrow> \<Gamma>;n \<turnstile> (AllT T) wf" |
  wfbvar[intro!]: "k < n \<Longrightarrow> \<Gamma>;n \<turnstile> (BVar k) wf" |
  wffvar1[intro!]: "lookup x \<Gamma> = Some TVar \<Longrightarrow> \<Gamma>;n \<turnstile> (FVar x) wf"

abbreviation wfty :: "ty_env \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _" [60,60] 59) where
   "\<Gamma> \<turnstile> T \<equiv> \<Gamma>;0 \<turnstile> T wf"

definition dom :: "('a \<times> 'b) list \<Rightarrow> 'a set" where
  "dom f \<equiv> set (map fst f)"
declare dom_def[simp]

inductive wf_env :: "ty_env \<Rightarrow> bool" where
  wf_nil[intro!]: "wf_env []" |
  wf_cons1[intro!]: "\<lbrakk> x \<notin> dom \<Gamma>; \<Gamma> \<turnstile> T; wf_env \<Gamma> \<rbrakk> \<Longrightarrow>
      wf_env ((x,EVar T)#\<Gamma>)" | 
  wf_cons2[intro!]: "\<lbrakk> x \<notin> dom \<Gamma>; wf_env \<Gamma> \<rbrakk> \<Longrightarrow>
      wf_env ((x,TVar)#\<Gamma>)"

inductive
  wt_expr :: "ty_env \<Rightarrow> expr \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile>\<^isub>e _ : _" [60,60,60] 59) 
  and wt_stmt :: "ty_env \<Rightarrow> stmt \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile>\<^isub>s _ : _" [60,60,60] 59) 
  where
  wtvar[intro!]: "lookup x \<Gamma> = Some (EVar A) \<Longrightarrow> \<Gamma> \<turnstile>\<^isub>e Var x : A" |
  wtconst[intro!]: "\<Gamma> \<turnstile>\<^isub>e Const c : typeof c" |
  wtpapp[intro!]: "\<lbrakk> typeof_opr f = A \<rightarrow> B; \<Gamma> \<turnstile>\<^isub>e e : A \<rbrakk> \<Longrightarrow>
     \<Gamma> \<turnstile>\<^isub>e PrimApp f e : B" |
  wtlam[intro!]: "\<lbrakk> (x,EVar A)#\<Gamma> \<turnstile>\<^isub>s s : B; x \<notin> dom \<Gamma>; \<Gamma> \<turnstile> A \<rbrakk> \<Longrightarrow>
     \<Gamma> \<turnstile>\<^isub>e Lam x s (A\<rightarrow>B) : (A \<rightarrow> B)" |
  wtpoly[intro!]: "\<lbrakk> (\<alpha>,TVar)#\<Gamma> \<turnstile>\<^isub>s s : A; \<alpha> \<notin> dom \<Gamma> \<rbrakk> \<Longrightarrow> 
     \<Gamma> \<turnstile>\<^isub>e TyAbs \<alpha> s (AllT (close \<alpha> 0 A)) : AllT (close \<alpha> 0 A)" |

  wtlet[intro!]: "\<lbrakk> \<Gamma> \<turnstile>\<^isub>e e : A; x \<notin> dom \<Gamma>; (x,EVar A)#\<Gamma> \<turnstile>\<^isub>s s : B \<rbrakk> \<Longrightarrow>
     \<Gamma> \<turnstile>\<^isub>s SLet x e s : B" |
  wtret[intro!]: "\<lbrakk> \<Gamma> \<turnstile>\<^isub>e e : A \<rbrakk> \<Longrightarrow>
     \<Gamma> \<turnstile>\<^isub>s SRet e : A" |
  wtcall[intro!]: "\<lbrakk> \<Gamma> \<turnstile>\<^isub>e e1 : A \<rightarrow> B; \<Gamma> \<turnstile>\<^isub>e e2 : A; x \<notin> dom \<Gamma>;
     (x, EVar B)#\<Gamma> \<turnstile>\<^isub>s s : C \<rbrakk> \<Longrightarrow>
     \<Gamma> \<turnstile>\<^isub>s SCall x e1 e2 s : C" |
  wtinst[intro!]: "\<lbrakk> \<Gamma> \<turnstile>\<^isub>e e : AllT A; \<Gamma> \<turnstile> B; x \<notin> dom \<Gamma>;
     (x,EVar ([B]A))#\<Gamma> \<turnstile>\<^isub>s s : C\<rbrakk> \<Longrightarrow>
     \<Gamma> \<turnstile>\<^isub>s SInst x e B s : C"

inductive wt_val :: "tymap \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile>\<^isub>v _ : _" [60,60,60] 59)
  and wt_env :: "ty_env \<Rightarrow> tymap \<Rightarrow> env \<Rightarrow> bool" ("_;_ \<turnstile> _" [60,60,60] 59) where
  wt_vc[intro!]: "typeof c = A \<Longrightarrow> \<Sigma>' \<turnstile>\<^isub>v (VConst c) : A" |
  wt_box[intro!]: "psub \<Sigma>' (FVar \<alpha>) = (typeof c) \<Longrightarrow>
      \<Sigma>' \<turnstile>\<^isub>v (Boxed c \<alpha>) : (FVar \<alpha>)" |
  wt_cl[intro!]: "\<lbrakk> wf_env \<Gamma>; \<Gamma>;\<Sigma> \<turnstile> (\<rho>::env); x \<notin> dom \<Gamma>; 
                    \<Gamma> \<turnstile> A\<^isub>1; psub \<Sigma> (A\<^isub>1\<rightarrow>A\<^isub>2) = psub \<Sigma>' B; 
                   (x,EVar A\<^isub>1)#\<Gamma> \<turnstile>\<^isub>s s : A\<^isub>2 \<rbrakk> \<Longrightarrow> 
     \<Sigma>' \<turnstile>\<^isub>v (Closure x s \<rho> \<Sigma> (A\<^isub>1\<rightarrow>A\<^isub>2) B) : B" |
  wt_tabs[intro!]: "\<lbrakk> wf_env \<Gamma>; \<Gamma>;\<Sigma> \<turnstile> \<rho>; \<alpha> \<notin> dom \<Gamma>; 
                      psub \<Sigma> (AllT (close \<alpha> 0 A)) = psub \<Sigma>' B;
                      (\<alpha>,TVar)#\<Gamma> \<turnstile>\<^isub>s s : A \<rbrakk> \<Longrightarrow>
     \<Sigma>' \<turnstile>\<^isub>v (TAbs \<alpha> s \<rho> \<Sigma> (AllT (close \<alpha> 0 A)) B) : B" |

  wt_nil[intro!]: "[];[] \<turnstile> []" |
  wt_cons[intro!]: "\<lbrakk> x \<notin> dom \<Gamma>; \<Sigma> \<turnstile>\<^isub>v v : A; \<Gamma> \<turnstile> A; \<Gamma>;\<Sigma> \<turnstile> (\<rho>::env) \<rbrakk> \<Longrightarrow> 
     ((x,EVar A)#\<Gamma>);\<Sigma> \<turnstile> ((x,v)#\<rho>)" |
  wt_cons2[intro!]: "\<lbrakk> \<alpha> \<notin> dom \<Gamma>; [] \<turnstile> T; \<Gamma>;\<Sigma> \<turnstile> (\<rho>::env) \<rbrakk> \<Longrightarrow> 
     ((\<alpha>,TVar)#\<Gamma>);((\<alpha>,T)#\<Sigma>) \<turnstile> \<rho>"

inductive wt_stack :: "tymap \<Rightarrow> stack \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _ \<Rightarrow> _") where
  nil_stack[intro!]: "\<Sigma> \<turnstile> [] : A \<Rightarrow> A" |
  cons_stack[intro!]: "\<lbrakk> wf_env \<Gamma>; \<Gamma>; \<Sigma> \<turnstile> \<rho>; psub \<Sigma>' A = psub \<Sigma> B; 
                         (x,EVar B)#\<Gamma> \<turnstile>\<^isub>s s : C; \<Gamma> \<turnstile> B;
                         x \<notin> dom \<Gamma>; \<Sigma> \<turnstile> k : C \<Rightarrow> D \<rbrakk> \<Longrightarrow>
     \<Sigma>' \<turnstile> (x, A, B, s, \<rho>, \<Sigma>)#k : A \<Rightarrow> D"

inductive wt_state :: "state \<Rightarrow> ty \<Rightarrow> bool" where
  wts[intro!]: "\<lbrakk> wf_env \<Gamma>; \<Gamma>;\<Sigma> \<turnstile> \<rho>; \<Gamma> \<turnstile>\<^isub>s s : A; 
                  \<Sigma> \<turnstile> k : A \<Rightarrow> B \<rbrakk> \<Longrightarrow>
    wt_state (s, \<rho>, \<Sigma>, k) B"

fun wt_result :: "result \<Rightarrow> ty \<Rightarrow> bool" where
  "wt_result Fun (A \<rightarrow> B) = True" |
  "wt_result Poly (AllT A) = True" |
  "wt_result (Con c) A = (typeof c = A)" |
  "wt_result Error A = False"

section "Type Safety"

inductive_cases
  bool_int[elim!]: "\<Sigma> \<turnstile>\<^isub>v (VConst (BoolC b)) : IntT" and
  int_any[elim!]: "\<Sigma> \<turnstile>\<^isub>v (VConst (IntC n)) : A" and
  intval_inv[elim!]: "\<Sigma> \<turnstile>\<^isub>v v : IntT" and
  boolval_inv[elim!]: "\<Sigma> \<turnstile>\<^isub>v v : BoolT" and
  bvarval_inv[elim!]: "\<Sigma> \<turnstile>\<^isub>v v : (BVar k)" and
  fvarval_inv[elim!]: "\<Sigma> \<turnstile>\<^isub>v v : (FVar x)" and
  const_any[elim!]: "\<Sigma> \<turnstile>\<^isub>v (VConst c) : A" and
  bool_any[elim!]: "\<Sigma> \<turnstile>\<^isub>v (VConst (BoolC b)) : A" and
  clos_any[elim!]: "\<Sigma> \<turnstile>\<^isub>v (Closure x s \<rho> \<Sigma>' S T) : A" and
  clos_int[elim!]: "\<Sigma> \<turnstile>\<^isub>v (Closure x s \<rho> \<Sigma>' S T) : IntT" and
  clos_bool[elim!]: "\<Sigma> \<turnstile>\<^isub>v (Closure x s \<rho> \<Sigma>' S T) : BoolT" and
  tabs_any[elim!]: "\<Sigma> \<turnstile>\<^isub>v (TAbs x e \<rho> \<Sigma>' S T) : A " and
  const_fun[elim!]: "\<Sigma> \<turnstile>\<^isub>v (VConst c) : (A \<rightarrow> B)" and
  clos_fun[elim!]: "\<Sigma> \<turnstile>\<^isub>v (Closure x s \<rho> \<Sigma>' S T) : (A \<rightarrow> B)" and
  funval_inv[elim!]: "\<Sigma> \<turnstile>\<^isub>v v : (A \<rightarrow> B)" and
  boxed_inv[elim!]: "\<Sigma> \<turnstile>\<^isub>v Boxed c n : T"

subsection "Lemmas Regarding Lookup"

(*
lemma lookup_dom_iff:
  shows "(\<exists> v. lookup x F = Some v) = (x \<in> dom F)"
  apply (induct F)
  apply simp
  apply force
  done
*)

lemma lookup_dom:
  assumes l: "lookup x F = Some v"
  shows "x \<in> dom F"
  using l apply (induct F)
  apply simp
  apply force
  done

(*
lemma dom_lookup:
  assumes x: "x \<in> dom F"
  shows "\<exists> v. lookup x F = Some v"
  using x apply (induct F)
  apply simp
  apply (case_tac a) 
  apply (case_tac "x = aa") apply simp
  apply simp
  done
*)

lemma not_dom_lookup:
  assumes x: "x \<notin> dom F"
  shows "lookup x F = None"
  using x apply (induct F)
  apply simp
  apply force
  done

(*
lemma lookup_none_dom:
  assumes x: "lookup x F = None"
  shows "x \<notin> dom F"
  using x apply (induct F arbitrary: x)
  apply simp
  apply simp
  apply (case_tac a) apply simp
  apply (case_tac "x = aa") apply auto
  done
*)

subsection "Lemmas Regarding Well-Formed Types"

lemma wf_ty_weaken_cons:
  fixes T::ty
  assumes wft: "\<Gamma>; n \<turnstile> T wf" and xg: "x \<notin> dom \<Gamma>"
  shows "(x,b)#\<Gamma>;n \<turnstile> T wf"
  using wft xg
  apply (induct T)
  apply force
  apply force
  apply force
  apply force
  apply force
  apply clarify
  using lookup_dom apply force
  done

lemma wf_ty_weaken_ty:
  fixes T::ty
  assumes wft: "\<Gamma>; n \<turnstile> T wf" and g: "\<Gamma> = []"
  shows "\<Gamma>';n \<turnstile> T wf"
  using wft g
  apply (induct T) apply auto done

lemma wf_ty_weaken_n:
  fixes T::ty
  assumes wft: "\<Gamma>; n \<turnstile> T wf" and nm: "n \<le> m"
  shows "\<Gamma>;m \<turnstile> T wf"
  using wft nm apply (induct T arbitrary: m)
  apply auto
  done

lemma wf_ty_weaken:
  fixes T::ty
  assumes wft: "[] \<turnstile> T"
  shows "\<Gamma>;n \<turnstile> T wf"
  using wft wf_ty_weaken_n wf_ty_weaken_ty apply fast done

lemma wf_env_strengthen:
  fixes B::ty
  assumes wfe: "\<Gamma>'; n \<turnstile> B wf" and g: "\<Gamma>' = (x,EVar A)#\<Gamma>"
  shows "\<Gamma>;n \<turnstile> B wf"
  using wfe g apply (induct arbitrary: x A rule: wf_ty.induct)
  apply force
  apply force
  apply force
  apply force
  apply force
  apply simp apply (case_tac "x = xa") apply auto
  done

lemma close_wf:
  fixes S::ty
  assumes wts: "\<Gamma>';n \<turnstile> S wf" and kn: "k < n" and g: "\<Gamma>'=(x,TVar)#\<Gamma>"
  shows "\<Gamma>;n \<turnstile> (close x k S) wf"
  using wts kn g
  apply (induct arbitrary: k rule: wf_ty.induct)
  apply auto
  done

inductive_cases
  wf_fun_inv[elim!]: "\<Gamma>; n \<turnstile> (A \<rightarrow> B) wf" and
  wf_all_inv[elim!]: "\<Gamma>; n \<turnstile> (AllT A) wf" and
  wf_bvar_inv[elim!]: "\<Gamma>; n \<turnstile> (BVar k) wf" and
  wf_fvar_inv[elim!]: "\<Gamma>; n \<turnstile> (FVar x) wf" 

lemma wf_shift:
  fixes n::nat
  assumes wf: "\<Gamma>;n \<turnstile> T wf"
  shows "\<Gamma>; Suc n \<turnstile> (shift c T) wf"
  using wf apply (induct arbitrary: c rule: wf_ty.induct)
  apply auto done

lemma wf_bsub:
  fixes \<Gamma>::ty_env and A::ty and n::nat
  assumes 1:"\<Gamma>;m \<turnstile> A wf" and 2: "\<Gamma>;n \<turnstile> T wf" and 3: "m = Suc n"
  shows "\<Gamma>;n \<turnstile> (bsub n T A) wf"
  using 1 2 3 apply (induct arbitrary: n T rule: wf_ty.induct)
  apply auto
  apply (frule_tac n=na and c=0 in wf_shift) apply simp
  done

lemma bsub_close_id:
  fixes n::nat and T::ty
  assumes wft: "\<Gamma>;n \<turnstile> T wf"
  shows "bsub n (FVar x) (close x n T) = T"
  using wft apply (induct rule: wf_ty.induct) by auto

subsection "Lemmas Regarding Well-Formed Environments"

inductive_cases wf_env_inv[elim!]: "wf_env ((a,b)#\<Gamma>)"

lemma lookup_wf[rule_format]:
  assumes wf: "wf_env \<Gamma>"
  shows "\<forall> x T. lookup x \<Gamma> = Some (EVar T) \<longrightarrow> \<Gamma> \<turnstile> T"
  using wf apply (induct rule: wf_env.induct)
  apply simp
  apply clarsimp apply (case_tac "xa = x") apply simp 
    using wf_ty_weaken_cons apply force
    apply clarsimp apply (erule_tac x=xa in allE)
    apply (erule_tac x=Ta in allE) apply simp
    using wf_ty_weaken_cons apply force
  apply clarsimp apply (case_tac "xa = x") apply simp 
    using wf_ty_weaken_cons apply force
  done

lemma wte_wts_wft:
  "(\<Gamma> \<turnstile>\<^isub>e e : T \<longrightarrow> wf_env \<Gamma> \<longrightarrow> \<Gamma> \<turnstile> T) 
   \<and> (\<Gamma> \<turnstile>\<^isub>s s : T \<longrightarrow> wf_env \<Gamma> \<longrightarrow> \<Gamma> \<turnstile> T)"
  apply (induct rule: wt_expr_wt_stmt.induct)
  using lookup_wf apply blast
  apply (case_tac c) apply force apply force
  apply (case_tac f) apply force apply force apply force
  apply clarsimp apply (erule impE) apply force 
    apply (rule_tac \<Gamma>=\<Gamma> and B=B and n=0 in wf_env_strengthen) 
    apply blast apply blast
  apply clarsimp apply (erule impE) apply force
    using close_wf wf_ty_weaken_n apply fast
  apply clarsimp apply (erule impE) apply force 
    using wf_env_strengthen apply fast
  apply force
  apply clarsimp apply (erule impE) apply (rule wf_cons1)
    apply simp apply blast apply simp
    using wf_env_strengthen apply fast
  apply clarsimp apply (erule impE) apply (rule wf_cons1)
    apply simp using wf_bsub apply force apply simp
    using wf_env_strengthen apply fast
  done

subsection "Lemmas Regarding Well-Typed Values and Environments"

lemma lookup_wft_aux:
  "(\<Sigma> \<turnstile>\<^isub>v v : T \<longrightarrow> True) \<and>
   (\<Gamma>;\<Sigma> \<turnstile> \<rho> \<longrightarrow> (\<forall> x T. lookup x \<Sigma> = Some T \<longrightarrow> [] \<turnstile> T))"
  apply (induct rule: wt_val_wt_env.induct) apply auto done

lemma wtenv_lookup_wft: "\<lbrakk> \<Gamma>;\<Sigma> \<turnstile> \<rho>; lookup x \<Sigma> = Some T \<rbrakk> \<Longrightarrow> [] \<turnstile> T"
  using lookup_wft_aux apply auto done

lemma wtenv_lookup_iff_aux:
  "(\<Sigma> \<turnstile>\<^isub>v v : T \<longrightarrow> True) \<and>
   (\<Gamma>;\<Sigma> \<turnstile> \<rho> \<longrightarrow> (\<forall> x. (lookup x \<Gamma> = Some TVar) = (\<exists> T. lookup x \<Sigma> = Some T)))"
  apply (induct rule: wt_val_wt_env.induct)
  apply force
  apply force
  apply force
  apply force
  apply simp
  apply clarify apply (erule_tac x=xa in allE)
  apply simp
  apply (case_tac "xa=x") apply simp
  using not_dom_lookup apply force
  apply simp
  apply clarify
  apply simp
  done

lemma wtenv_lookup_iff:
  "\<Gamma>;\<Sigma> \<turnstile> \<rho> \<Longrightarrow> (lookup x \<Gamma> = Some TVar) = (\<exists> T. lookup x \<Sigma> = Some T)"
  using wtenv_lookup_iff_aux apply auto done

lemma wft_swap_env:
  fixes \<rho>::env
  assumes 1: "\<Gamma>; \<Sigma> \<turnstile> \<rho>" and 2: "\<Gamma>'; \<Sigma> \<turnstile> \<rho>" and 3: "\<Gamma> \<turnstile> T"
  shows "\<Gamma>' \<turnstile> T"
  using 3 2 1 apply (induct arbitrary: \<Gamma>' \<Sigma> rule: wf_ty.induct)
  using wtenv_lookup_iff apply auto done

lemma wt_cast:
  assumes wtv: "\<Sigma> \<turnstile>\<^isub>v v : S" and st: "psub \<Sigma> S = psub \<Sigma>' T" and wft: "\<Gamma> \<turnstile> T"
  shows "\<Sigma>' \<turnstile>\<^isub>v (cast v S T) : T"
  using st wtv wft apply (cases v)
  (* v= VConst const *)
  apply simp apply (case_tac T)
    apply clarsimp apply (case_tac const) apply simp apply simp
    apply clarsimp apply (case_tac const) apply simp apply simp
    apply clarsimp apply (case_tac const) apply simp apply simp
    apply clarsimp apply (case_tac const) apply simp apply simp
    apply clarsimp 
    apply simp apply (rule wt_box) apply (case_tac "lookup nat \<Sigma>'")
      apply simp apply clarify
      apply (case_tac const) apply simp apply simp 
      apply simp apply clarify 
      apply (case_tac const) apply simp apply simp 
  (* v = Boxed const nat *)
  apply simp apply (case_tac T)
    apply clarsimp
    apply clarsimp 
    apply clarsimp apply (case_tac "lookup nat \<Sigma>") apply clarsimp
      apply clarsimp apply (case_tac const) apply simp apply simp
    apply clarsimp apply (case_tac "lookup nat \<Sigma>") apply clarsimp
      apply clarsimp apply (case_tac const) apply simp apply simp
    apply clarsimp 
    apply clarsimp 
  (* v = Closure ... *)
  apply simp apply (erule clos_any) apply clarsimp
    apply (rule wt_cl) apply simp apply simp apply simp apply simp
    using wte_wts_wft apply force apply simp 
  (* v = TAbs ... *) 
  apply simp apply (erule tabs_any) apply clarsimp
    apply (rule wt_tabs) apply auto 
  done

lemma psub_cons_weaken:
  fixes \<rho>::env
  assumes wft: "\<Gamma> \<turnstile> T" and gs: "\<Gamma>; \<Sigma> \<turnstile> \<rho>"
  and xg: "x \<notin> dom \<Gamma>"
  shows "psub \<Sigma> T = psub ((x,T')#\<Sigma>) T"
  using wft gs xg apply (induct rule: wf_ty.induct)
  apply force
  apply force
  apply force
  apply force
  apply force
  apply simp
  apply (case_tac "xa = x")
    apply simp
  apply (case_tac "lookup x \<Sigma>")
    using wtenv_lookup_iff apply force
    using not_dom_lookup apply force
  apply auto
  done

lemma weaken_env_val:
  "(\<Sigma> \<turnstile>\<^isub>v v : T' \<longrightarrow> (\<forall> T \<Gamma> \<rho> x. [] \<turnstile> T \<longrightarrow> \<Gamma> \<turnstile> T' \<longrightarrow> \<Gamma>; \<Sigma> \<turnstile> \<rho>
                \<longrightarrow> x \<notin> dom \<Gamma> \<longrightarrow> (x,T)#\<Sigma> \<turnstile>\<^isub>v v : T'))
   \<and> (\<Gamma>;\<Sigma> \<turnstile> \<rho> \<longrightarrow> (\<forall> T x. [] \<turnstile> T \<longrightarrow> x \<notin> dom \<Gamma>
      \<longrightarrow> (x, TVar) # \<Gamma>;(x, T) # \<Sigma> \<turnstile> \<rho>))" 
  (is "(\<Sigma> \<turnstile>\<^isub>v v : T' \<longrightarrow> ?P \<Sigma> v T') \<and> (\<Gamma>;\<Sigma> \<turnstile> \<rho> \<longrightarrow> ?Q \<Gamma> \<Sigma> \<rho>)")
proof (induct rule: wt_val_wt_env.induct)
  fix c A \<Sigma>'
  assume "typeof c = A"
  thus "?P \<Sigma>' (VConst c) A" apply force done
next
  fix \<Sigma>' x' c
  assume "psub \<Sigma>' (FVar x') = typeof c"
  thus "?P \<Sigma>' (Boxed c x') (FVar x')"
    apply auto
    apply (case_tac "lookup x' \<Sigma>'") apply auto
    apply (case_tac c) apply auto
    using not_dom_lookup apply force  
    done
next
  fix \<Gamma> and \<Sigma>::tymap and \<rho>::env and x A1 A2 \<Sigma>' B s
  assume wfg: "wf_env \<Gamma>" and wfE: "\<Gamma>;\<Sigma> \<turnstile> \<rho>" and IH: "?Q \<Gamma> \<Sigma> \<rho>"
    and xpg: "x \<notin> dom \<Gamma>" and wfs1: "\<Gamma> \<turnstile> A1"
    and ps12: "psub \<Sigma> (A1 \<rightarrow> A2) = psub \<Sigma>' B" 
    and wts: "(x,EVar A1)#\<Gamma> \<turnstile>\<^isub>s s : A2"
  show "?P \<Sigma>' (Closure x s \<rho> \<Sigma> (A1 \<rightarrow> A2) B) B"
    apply (rule allI)+ apply (rule impI)+
    apply (rule wt_cl)
    prefer 6 using wts apply assumption
    using wfg apply assumption
    using wfE apply simp
    using xpg apply simp 
    using wfs1 apply simp
  proof -
    fix T' \<Gamma>' and \<rho>'::env and x''
    assume wftp: "[] \<turnstile> T'" and gpt: "\<Gamma>' \<turnstile> B" and gps: "\<Gamma>' ; \<Sigma>' \<turnstile> \<rho>'"
      and xgp: "x'' \<notin> dom \<Gamma>'"
    from gpt gps xgp have "psub \<Sigma>' B = psub ((x'', T') # \<Sigma>') B"
      apply (rule psub_cons_weaken) done
    thus "psub \<Sigma> (A1 \<rightarrow> A2) = psub ((x'', T') # \<Sigma>') B"
      using ps12 apply simp done
  qed
next
  fix \<Gamma> and \<Sigma>::tymap and \<rho>::env and xa S \<Sigma>' T s
  assume wfg: "wf_env \<Gamma>" and wtr: "\<Gamma>;\<Sigma> \<turnstile> \<rho>"
    and IH: "?Q \<Gamma> \<Sigma> \<rho>"
    and xag: "xa \<notin> dom \<Gamma>"
    and psx: "psub \<Sigma> (AllT (close xa 0 S)) = psub \<Sigma>' T"
    and wts: "(xa, TVar) # \<Gamma> \<turnstile>\<^isub>s s : S"
  show "?P \<Sigma>' (TAbs xa s \<rho> \<Sigma> (AllT (close xa 0 S)) T) T"
    apply (rule allI)+ apply (rule impI)+
    apply (rule wt_tabs)
    prefer 5 using wts apply assumption
    using wfg apply assumption
    prefer 2 using xag apply assumption
    using wtr apply assumption
  proof -
    fix Ta \<Gamma>' and \<rho>'::env and x'
    assume wfta: "[] \<turnstile> Ta" and wft: "\<Gamma>' \<turnstile> T" and gsp: "\<Gamma>';\<Sigma>' \<turnstile> \<rho>'"
      and xgp: "x' \<notin> dom \<Gamma>'" 
    from wft gsp xgp
    have "psub \<Sigma>' T = psub ((x', Ta) # \<Sigma>') T" 
      apply (rule psub_cons_weaken) done
    with psx show " psub \<Sigma> (AllT (close xa 0 S)) = psub ((x', Ta) # \<Sigma>') T"
      by simp
  qed
next
  fix \<Sigma> show "?Q [] [] []" apply auto done
next
  fix x \<Gamma> \<Sigma> v A and E::env
  assume xg: "x \<notin> dom \<Gamma>" and wtv: "\<Sigma> \<turnstile>\<^isub>v v : A"
    and IH1: "?P \<Sigma> v A"
    and wfa: "\<Gamma> \<turnstile> A" and wtE: "\<Gamma>;\<Sigma> \<turnstile> E"
    and IH2: "?Q \<Gamma> \<Sigma> E"
  show "?Q ((x,EVar A)#\<Gamma>) \<Sigma> ((x,v)#E)"
    apply (rule allI)+ apply (rule impI)+
    apply (rule wt_cons2)
    apply simp apply simp
    apply (rule wt_cons)
    using xg apply assumption
    using wtv apply simp
    using wfa apply assumption
    using wtE apply assumption
    done
next
  fix x \<Gamma> T \<Sigma> and E::env
  assume xg: "x \<notin> dom \<Gamma>" and wft: "[] \<turnstile> T" and wtE: "\<Gamma>;\<Sigma> \<turnstile> E"
    and IH: "?Q \<Gamma> \<Sigma> E"
  show "?Q ((x,TVar)#\<Gamma>) ((x,T)#\<Sigma>) E"
    apply (rule allI)+ apply (rule impI)+
    apply (rule wt_cons2)
    apply simp
    using wft apply simp
    using IH apply simp
    apply (erule_tac x=T in allE)
    apply (erule impE) using wft apply assumption
    apply (erule_tac x=x in allE)
    apply (erule impE)
    using xg apply simp
    apply simp
    done
qed

lemma weaken_wtval:
  "\<lbrakk> \<Sigma> \<turnstile>\<^isub>v v : T'; [] \<turnstile> T; \<Gamma> \<turnstile> T'; \<Gamma>; \<Sigma> \<turnstile> \<rho>; x \<notin> dom \<Gamma> \<rbrakk> \<Longrightarrow> (x,T)#\<Sigma> \<turnstile>\<^isub>v v : T'"
  using weaken_env_val apply simp  apply blast done

lemma weaken_wtenv:
  fixes \<rho>::env
  assumes wtr: "\<Gamma>;\<Sigma> \<turnstile> \<rho>" and wft: "[] \<turnstile> T" and xg: "x \<notin> dom \<Gamma>"
  shows "(x, TVar) # \<Gamma>;(x, T) # \<Sigma> \<turnstile> \<rho>"
  using weaken_env_val wtr wft xg apply simp done

lemma lookup_safe: 
  fixes \<rho>::env
  assumes wtg: "\<Gamma>;\<Sigma> \<turnstile> \<rho>" and wfg: "wf_env \<Gamma>"
  and l: "lookup x \<Gamma> = Some (EVar A)"
  shows "\<exists> v. lookup x \<rho> = Some v \<and> \<Sigma> \<turnstile>\<^isub>v v : A \<and> \<Gamma> \<turnstile> A"
  using wtg wfg l 
  apply (induct \<rho>) 
  apply force
  apply force
  apply force
  apply force
  apply force
  apply (case_tac "x = xa") apply simp 
    apply (rule wf_ty_weaken_cons) apply simp
    apply (erule wf_env_inv) apply simp apply blast
    apply simp
    apply (erule wf_env_inv) apply simp apply (erule exE) apply simp
      apply (rule wf_ty_weaken_cons) apply simp apply simp
    apply simp 
  apply clarsimp apply (case_tac "x = \<alpha>") apply simp 
    apply simp
    apply (erule wf_env_inv) apply simp 
    apply simp
    apply (erule exE) apply simp
    apply (rule conjI)
    apply (rule weaken_wtval) apply simp apply simp apply force
    apply force apply force
    apply (rule wf_ty_weaken_cons) apply simp
    apply simp
  done

subsection "Lemmas Regarding the Dynamic Semantics"

lemma delta_safe: 
  fixes A::ty
  assumes wtop: "typeof_opr f = A \<rightarrow> B"
  and wtv: "\<Sigma> \<turnstile>\<^isub>v v : A"
  shows "\<exists> v'. delta f v = Some v' \<and> \<Sigma> \<turnstile>\<^isub>v v' : B"
  using wtop wtv
  apply (case_tac f)
  apply (case_tac v) apply auto apply (case_tac const) apply auto
  apply (case_tac v) apply auto apply (case_tac c) apply auto
  apply (case_tac c) apply auto apply (case_tac c) apply auto
  apply (case_tac c) apply auto
  apply (case_tac c) apply auto
  done

inductive_cases wtv[elim!]: "\<Gamma> \<turnstile>\<^isub>e Var x : A" and
  wtc[elim!]: "\<Gamma> \<turnstile>\<^isub>e Const c : A" and
  wti[elim!]: "\<Gamma> \<turnstile>\<^isub>e Const (IntC n) : A" and
  wtb[elim!]: "\<Gamma> \<turnstile>\<^isub>e Const (BoolC b) : A" and
  wtp[elim!]: "\<Gamma> \<turnstile>\<^isub>e PrimApp f e : A" and
  wtlam_inv[elim!]: "\<Gamma> \<turnstile>\<^isub>e Lam x s T : A" and
  wtabs[elim!]: "\<Gamma> \<turnstile>\<^isub>e TyAbs x s T : A" and
  wtlet_inv[elim!]: "\<Gamma> \<turnstile>\<^isub>s SLet x e s : A" and
  wtret_inv[elim!]: "\<Gamma> \<turnstile>\<^isub>s SRet e : A" and
  wtcall_inv[elim!]: "\<Gamma> \<turnstile>\<^isub>s SCall x e1 e2 s : A" and
  wtinst_inv[elim!]: "\<Gamma> \<turnstile>\<^isub>s SInst x e T s : A" 

lemma eval_safe:
  fixes \<Gamma>::"ty_env" and \<rho>::env
  assumes wte: "\<Gamma> \<turnstile>\<^isub>e e : A" and wfg: "wf_env \<Gamma>" and wtg: "\<Gamma>; \<Sigma> \<turnstile> \<rho>"
  shows "\<exists> v. eval e \<rho> \<Sigma> = Some v \<and> \<Sigma> \<turnstile>\<^isub>v v : A"
  using wte wfg wtg
proof (induct e \<rho> \<Sigma> arbitrary: A rule: eval.induct)
  fix x \<rho> \<Sigma> A
  assume wte: "\<Gamma> \<turnstile>\<^isub>e Var x : A" and wfg: "wf_env \<Gamma>" and wtr: "\<Gamma>;\<Sigma> \<turnstile> \<rho>"
  from wte have lx: "lookup x \<Gamma> = Some (EVar A)" by blast
  from wtr wfg lx obtain v where lv: "lookup x \<rho> = Some v"
    and wtv: "\<Sigma> \<turnstile>\<^isub>v v : A" using lookup_safe apply blast done
  from lv wtv show "\<exists>v. eval (Var x) \<rho> \<Sigma> = Some v \<and> \<Sigma> \<turnstile>\<^isub>v v : A" by simp
next
  fix c \<rho> \<Sigma> A
  assume wte: "\<Gamma> \<turnstile>\<^isub>e Const c : A" and wfg: "wf_env \<Gamma>" and wtr: "\<Gamma>;\<Sigma> \<turnstile> \<rho>"
  from wte have "typeof c = A" by blast
  hence "\<Sigma> \<turnstile>\<^isub>v VConst c : A" by blast
  thus "\<exists>v. eval (Const c) \<rho> \<Sigma> = Some v \<and> \<Sigma> \<turnstile>\<^isub>v v : A" by simp
next
  fix f e \<rho> \<Sigma> A
  assume IH: "\<And>A. \<lbrakk>\<Gamma> \<turnstile>\<^isub>e e : A; wf_env \<Gamma>; \<Gamma>;\<Sigma> \<turnstile> \<rho> \<rbrakk>
            \<Longrightarrow> \<exists>v. eval e \<rho> \<Sigma> = Some v \<and> \<Sigma> \<turnstile>\<^isub>v v : A"
    and wtp: "\<Gamma> \<turnstile>\<^isub>e PrimApp f e : A" and wfg: "wf_env \<Gamma>" and wtr: "\<Gamma>;\<Sigma> \<turnstile> \<rho>"
  from wtp obtain T where tf: "typeof_opr f = T \<rightarrow> A"
    and wte: "\<Gamma> \<turnstile>\<^isub>e e : T" apply blast done
  from wte wfg wtr IH obtain v where ev: "eval e \<rho> \<Sigma> = Some v"
    and wtv: "\<Sigma> \<turnstile>\<^isub>v v : T" apply blast done
  from tf wtv obtain v' where d: "delta f v = Some v'"
    and wtvp: "\<Sigma> \<turnstile>\<^isub>v v' : A" using delta_safe apply blast done
  from ev d wtvp show "\<exists>v. eval (PrimApp f e) \<rho> \<Sigma> = Some v \<and> \<Sigma> \<turnstile>\<^isub>v v : A" 
    by simp
next
  fix x s T \<rho> \<Sigma> A
  assume wtl: "\<Gamma> \<turnstile>\<^isub>e Lam x s T : A" and wfg: "wf_env \<Gamma>" and wtr: "\<Gamma>;\<Sigma> \<turnstile> \<rho>"
  let ?V = "Closure x s \<rho> \<Sigma> T T"
  from wtl obtain T1 T2 where a: "A=T1\<rightarrow>T2" 
    and wts: "(x,EVar T1)#\<Gamma> \<turnstile>\<^isub>s s : T2"
    and xg: "x \<notin> dom \<Gamma>" and wft1: "\<Gamma> \<turnstile> T1" and t: "T=T1\<rightarrow>T2" 
    apply auto done
  from wfg wft1 xg have wtg2: "wf_env ((x,EVar T1)#\<Gamma>)" by auto
  from wts wtg2 have "((x,EVar T1)#\<Gamma>) \<turnstile> T2" using wte_wts_wft by auto
  hence wft2: "\<Gamma> \<turnstile> T2" using wf_env_strengthen apply auto done
  from wfg wtr xg wts t a wft1 wft2
  have "\<Sigma> \<turnstile>\<^isub>v ?V : A" apply simp apply (rule wt_cl) apply auto done
  thus "\<exists>v. eval (Lam x s T) \<rho> \<Sigma> = Some v \<and> \<Sigma> \<turnstile>\<^isub>v v : A" apply simp done
next
  fix x s T \<rho> \<Sigma> A
  assume wtp: "\<Gamma> \<turnstile>\<^isub>e TyAbs x s T : A" and wfg: "wf_env \<Gamma>" and wtr: "\<Gamma>;\<Sigma> \<turnstile> \<rho>"
  from wtp obtain S where a: "A = AllT (close x 0 S)" 
    and wts: "(x,TVar)#\<Gamma> \<turnstile>\<^isub>s s : S" and xg: "x \<notin> dom \<Gamma>" 
    and t: "T = AllT (close x 0 S)"
    apply (rule wtabs) apply simp done
  let ?V = "TAbs x s \<rho> \<Sigma> T T"
  from wfg xg have wfg2: "wf_env ((x,TVar)#\<Gamma>)" apply auto done
  from wts wfg2 have "(x,TVar)#\<Gamma> \<turnstile> S"
    using wte_wts_wft apply auto done
  hence "(x,TVar)#\<Gamma>;Suc 0 \<turnstile> S wf" using wf_ty_weaken_n apply fast done
  hence "\<Gamma>;Suc 0 \<turnstile> (close x 0 S) wf" using close_wf apply fast done
  hence wfa: "\<Gamma> \<turnstile> AllT (close x 0 S)" apply blast done
  from wfg wtr xg wts a t wfa have "\<Sigma> \<turnstile>\<^isub>v ?V : A"
    apply simp apply (rule wt_tabs) apply simp+ done
  thus "\<exists>v. eval (TyAbs x s T) \<rho> \<Sigma> = Some v \<and> \<Sigma> \<turnstile>\<^isub>v v : A" by simp
qed

inductive_cases wts_inv[elim!]: "wt_state s A"
inductive_cases wtk_cons_inv[elim!]: "\<Sigma> \<turnstile> (x, T1, T2, s, \<rho>, \<Sigma>')#k : A \<Rightarrow> C"
inductive_cases polyval_inv[elim!]: "\<Sigma> \<turnstile>\<^isub>v v : AllT T"

lemma tymap_psub_wf:
  fixes n::nat and T::ty and \<rho>::env
  assumes wfpt: "[];n \<turnstile> (psub \<Sigma> T) wf" and gs: "\<Gamma>; \<Sigma> \<turnstile> \<rho>"
  shows "\<Gamma>;n \<turnstile> T wf"
  using wfpt gs apply (induct T arbitrary: n)
  apply auto
  apply (case_tac "lookup nat \<Sigma>") apply auto
  using wtenv_lookup_iff apply auto
  done

lemma psub_tymap_wf:
  fixes T::ty and \<rho>::env
  assumes wft: "\<Gamma> \<turnstile> T" and gs: "\<Gamma>; \<Sigma> \<turnstile> \<rho>"
  shows "[] \<turnstile> psub \<Sigma> T"
  using wft gs apply (induct rule: wf_ty.induct)
  apply force
  apply force
  apply force
  apply force
  apply force
  apply simp
  apply (case_tac "lookup x \<Sigma>")
    apply simp using wtenv_lookup_iff apply force
    apply simp
    apply (frule wtenv_lookup_wft) apply simp 
    apply (rule wf_ty_weaken_n) apply simp apply simp
  done

lemma psub_wf:
  fixes n::nat and S::ty and \<rho>::env and \<rho>'::env
  assumes wfa2: "\<Gamma>;n \<turnstile> S wf" and gs: "\<Gamma>; \<Sigma> \<turnstile> \<rho>" and gs2: "\<Gamma>'; \<Sigma>' \<turnstile> \<rho>'"
  and at: "psub \<Sigma> S = psub \<Sigma>' T" 
  shows "\<Gamma>';n \<turnstile> T wf"
  using wfa2 gs gs2 at
  apply (induct arbitrary: \<Sigma> T \<Gamma>' \<Sigma>' rule: wf_ty.induct)
  apply simp apply (case_tac T) apply simp apply blast apply simp apply simp
     apply simp apply simp apply simp apply (case_tac "lookup nat \<Sigma>'")
     apply simp apply simp apply clarify 
     using wtenv_lookup_iff apply simp
  apply simp apply (case_tac T) apply simp apply blast apply simp apply simp
     apply simp apply simp apply (case_tac "lookup nat \<Sigma>'") apply simp
     apply simp apply clarify using wtenv_lookup_iff apply simp
  apply simp apply (case_tac T) apply simp apply simp apply simp
     apply force apply simp apply simp apply simp
     apply (case_tac "lookup nat \<Sigma>'") apply simp
     apply simp apply clarify using wtenv_lookup_iff apply force
  apply simp apply (case_tac Ta) apply simp apply simp apply simp
     apply force apply simp apply simp 
     apply (case_tac "lookup nat \<Sigma>'") apply simp
     apply simp apply clarify using wtenv_lookup_iff apply force
  apply simp apply (case_tac T) apply simp apply simp apply simp
     apply simp apply simp apply blast apply simp 
     apply (case_tac "lookup nat \<Sigma>'") apply simp
     apply simp apply clarify using wtenv_lookup_iff apply force
  apply simp apply (case_tac "lookup x \<Sigma>") apply simp
     using wtenv_lookup_iff apply force
     apply simp
     apply (subgoal_tac "[] \<turnstile> psub \<Sigma>' T")
     prefer 2
     apply (frule wtenv_lookup_wft) apply simp  apply clarify
     apply (rule tymap_psub_wf) 
     apply (rule wf_ty_weaken_n) apply blast apply simp apply simp
  done

lemma shift_id:
  assumes wft: "\<Gamma>;k \<turnstile> T wf" and kn: "k \<le> n"
  shows "T = shift n T"
  using wft kn apply (induct T arbitrary: n) apply auto done

lemma bsub_id:
  assumes wft: "\<Gamma>;k \<turnstile> T wf" and kn: "k \<le> n"
  shows "T = bsub n S T"
  using wft kn apply (induct T arbitrary: n S)
  apply force
  apply force
  apply force
  apply force
  apply force
  apply force
  done

lemma psub_shift:
  fixes \<rho>::env and T::ty
  assumes wtr: "\<Gamma>;\<Sigma> \<turnstile> \<rho>" and wft: "\<Gamma>';k \<turnstile> T wf" 
  shows "psub \<Sigma> (shift n T) = shift n (psub \<Sigma> T)"
  using wtr wft apply (induct T arbitrary: n k)
  apply simp 
  apply simp
  apply force
  apply force
  apply simp
  apply simp
  apply (case_tac "lookup nat \<Sigma>") 
  apply auto
  apply (frule wtenv_lookup_wft) apply simp
  apply (rule shift_id) apply blast apply simp
  done

lemma psub_bsub:
  fixes \<rho>::env and n::nat
  assumes wtr: "\<Gamma>;\<Sigma> \<turnstile> \<rho>" and wft: "\<Gamma>'; n \<turnstile> T wf"
  shows "psub \<Sigma> (bsub n T B) = bsub n (psub \<Sigma> T) (psub \<Sigma> B)"
  using wtr wft apply (induct B arbitrary: n T)
  apply simp
  apply simp
  apply force
  prefer 2 apply simp
proof -
  fix B n T
  assume IH: "\<And>n T. \<lbrakk>\<Gamma>;\<Sigma> \<turnstile> \<rho>; \<Gamma>';n \<turnstile> T wf\<rbrakk>
              \<Longrightarrow> psub \<Sigma> (bsub n T B) = bsub n (psub \<Sigma> T) (psub \<Sigma> B)"
    and wtr: "\<Gamma>;\<Sigma> \<turnstile> \<rho>" and wft: "\<Gamma>';n \<turnstile> T wf"
  show "psub \<Sigma> (bsub n T (AllT B)) = bsub n (psub \<Sigma> T) (psub \<Sigma> (AllT B))"
  proof simp
    from wft have wfst: "\<Gamma>'; Suc n \<turnstile> (shift 0 T) wf" 
      using wf_shift[of \<Gamma>' n T] apply simp done
    from wtr wfst IH
    have "psub \<Sigma> (bsub (Suc n) (shift 0 T) B) =
          bsub (Suc n) (psub \<Sigma> (shift 0 T)) (psub \<Sigma> B)"
      apply simp done
    also from wtr wft
    have "... = bsub (Suc n) (shift 0 (psub \<Sigma> T)) (psub \<Sigma> B)"
      using psub_shift[of \<Gamma> \<Sigma> \<rho> \<Gamma>' n T 0] apply simp done
    finally show "psub \<Sigma> (bsub (Suc n) (shift 0 T) B) =
                  bsub (Suc n) (shift 0 (psub \<Sigma> T)) (psub \<Sigma> B)" by simp
  qed
next
  fix k n T
  assume wtr: "\<Gamma>;\<Sigma> \<turnstile> \<rho>" and wft: "\<Gamma>';n \<turnstile> T wf"
  show "psub \<Sigma> (bsub n T (FVar k)) =
        bsub n (psub \<Sigma> T) (psub \<Sigma> (FVar k))"
    apply simp
    apply (case_tac "lookup k \<Sigma>")
      apply simp
      apply simp
      using wtr apply (frule wtenv_lookup_wft)
      using wtr bsub_id apply simp
    done
qed

lemma close_id:
  assumes wft: "\<Gamma>;k \<turnstile> T wf" and xg: "x \<notin> dom \<Gamma>"
  shows "T = close x n T"
  using wft xg apply (induct arbitrary: n rule: wf_ty.induct)
  apply simp
  apply simp
  apply simp
  apply simp
  apply simp
  apply simp
  apply (subgoal_tac "x \<notin> dom \<Gamma>")
  apply (frule not_dom_lookup) 
  apply auto
  done
  
lemma psub_close:
  assumes xg: "x \<notin> dom \<Gamma>" and wtr: "\<Gamma>;\<Sigma> \<turnstile> \<rho>"
  shows "psub \<Sigma> (close x k T) = close x k (psub \<Sigma> T)"
  using xg wtr apply (induct T arbitrary: k)
  apply simp
  apply simp
  apply force
  apply simp 
  apply simp
  apply simp
   apply (case_tac "x = nat")
   apply simp
   apply (case_tac "lookup nat \<Sigma>") apply simp
   apply simp
   apply (subgoal_tac "nat \<notin> dom \<Gamma>")
   apply (frule not_dom_lookup)
   apply (frule wtenv_lookup_iff) apply simp apply force apply simp
 apply simp apply (case_tac "lookup nat \<Sigma>") apply simp
   apply simp
   apply (subgoal_tac "x \<notin> dom \<Gamma>")
   apply (frule not_dom_lookup)
   apply (frule wtenv_lookup_iff) apply simp 
   apply (rule close_id) 
   apply (rule wtenv_lookup_wft) apply assumption apply simp apply simp
   apply simp
   done

lemma bsub_close_psub:
  assumes wft: "\<Gamma>;n \<turnstile> T wf" and wfs: "[] \<turnstile> S" 
  shows "bsub n S (close x n T) = psub [(x,S)] T"
  using wft wfs apply (induct T arbitrary: S)
  apply simp
  apply simp
  apply simp
  apply simp
  apply (subgoal_tac "shift 0 S = S")
  apply simp
  using shift_id apply force
  apply simp
  apply simp 
  done

lemma wf_psub: 
  assumes wft: "\<Gamma>;n \<turnstile> T wf" and wtr: "\<Gamma>';\<Sigma> \<turnstile> \<rho>"
  shows "\<Gamma>;n \<turnstile> psub \<Sigma> T wf"
  using wft wtr apply (induct T)
  apply force
  apply force
  apply force
  apply force
  apply force
  apply simp
  apply (case_tac "lookup x \<Sigma>")
  apply simp apply clarify
  apply simp
  apply (frule wtenv_lookup_wft) apply simp
  apply (rule wf_ty_weaken_ty)
  apply (rule wf_ty_weaken_n) 
  apply simp
  apply simp
  apply simp
  done

lemma psub_id:
  assumes wft: "\<Gamma>;n \<turnstile> T wf" and g: "\<Gamma> = []"
  shows "psub \<Sigma> T = T"
  using wft g apply (induct T) apply auto done

lemma psub_cons:
  assumes yg: "y \<notin> dom \<Gamma>" and wtr: "\<Gamma>;\<Sigma> \<turnstile> \<rho>"
  shows "psub [(y, T)] (psub \<Sigma> S) = psub ((y, T) # \<Sigma>) S"
  using yg wtr apply (induct S)
  apply simp
  apply simp
  apply simp
  apply simp
  apply simp
  apply (frule not_dom_lookup)
  apply (frule_tac x=y in wtenv_lookup_iff) 
  apply simp
  apply (case_tac "nat = y")
  apply simp
  apply simp
  apply (case_tac "lookup nat \<Sigma>")
  apply simp
  apply simp
  apply (frule wtenv_lookup_wft) apply simp
  apply (rule psub_id) apply simp apply simp
  done

lemma psub_close_ext:
  fixes \<rho>'::env
  assumes 1: "psub \<Sigma>' (close y 0 S') = psub \<Sigma> B" 
  and 2: "(y,TVar)#\<Gamma>' \<turnstile> S'" and 3: "\<Gamma>;Suc 0 \<turnstile> B wf" and 4: "y \<notin> dom \<Gamma>'"
  and gr: "\<Gamma>; \<Sigma> \<turnstile> \<rho>" and gr2: "\<Gamma>'; \<Sigma>' \<turnstile> \<rho>'" and wft: "\<Gamma> \<turnstile> T"
  shows "psub ((y, psub \<Sigma> T) # \<Sigma>') S' = psub \<Sigma> ([T]B)" 
proof -
  from 2 gr2 have 5: "(y,TVar)#\<Gamma>' \<turnstile> psub \<Sigma>' S'" 
    apply (rule wf_psub) done
  from wft gr have 6: "[] \<turnstile> psub \<Sigma> T" apply (rule psub_tymap_wf) done
  from gr wft have "psub \<Sigma> ([T]B) = [psub \<Sigma> T]psub \<Sigma> B"
    using psub_bsub[of \<Gamma> \<Sigma> \<rho> \<Gamma> 0 T B] apply simp done
  also have "... = [psub \<Sigma> T]psub \<Sigma>' (close y 0 S')"
    using 1 apply simp done
  also from 4 gr2 have "... = [psub \<Sigma> T]close y 0 (psub \<Sigma>' S')"
    using psub_close apply simp done
  also from 5 6 have "... = psub [(y,psub \<Sigma> T)] (psub \<Sigma>' S')"
    using bsub_close_psub[of "(y,TVar)#\<Gamma>'" 0 "psub \<Sigma>' S'" "psub \<Sigma> T" y]
    apply simp done
  also from 4 gr2 have "... = psub ((y, psub \<Sigma> T) # \<Sigma>') S'"
    apply (rule psub_cons) done
  finally show ?thesis by simp
qed

lemma step_safe: 
  assumes wtsA: "wt_state s A"
  shows "final s \<or> (\<exists> s'. step s = Some s' \<and> wt_state s' A)"
  using wtsA 
proof (rule wts_inv)
  fix \<Gamma>::ty_env and \<Sigma> and \<rho>::env and st A' k
  assume st: "s = (st, \<rho>, \<Sigma>, k)" and wfg: "wf_env \<Gamma>" and gr: "\<Gamma>;\<Sigma> \<turnstile> \<rho>" 
    and wtst: "\<Gamma> \<turnstile>\<^isub>s st : A'" and wt_k: "\<Sigma> \<turnstile> k : A' \<Rightarrow> A"
  from wfg wtst have wfap: "\<Gamma> \<turnstile> A'" using wte_wts_wft apply auto done
  show ?thesis 
  proof (cases st)
    case (SLet x e s2)
    from wtst SLet obtain B where wte: "\<Gamma> \<turnstile>\<^isub>e e : B" and xg: "x \<notin> dom \<Gamma>"
      and wts2: "(x,EVar B)#\<Gamma> \<turnstile>\<^isub>s s2 : A'" by auto 
    from wte wfg gr obtain v where v: "eval e \<rho> \<Sigma> = Some v"
      and wtv: "\<Sigma> \<turnstile>\<^isub>v v : B" using eval_safe by blast
    from wte wfg have wfb: "\<Gamma> \<turnstile> B" using wte_wts_wft apply auto done
    from xg wtv wfb gr have gr2: "(x,EVar B)#\<Gamma>; \<Sigma> \<turnstile> (x,v)#\<rho>" 
      by (rule wt_cons)
    from v SLet xg st wfg gr2 wts2 wt_k wtv wfb show ?thesis
      apply clarsimp apply (rule wts) apply auto done
  next
    case (SRet e)
    show ?thesis
    proof (cases k)
      assume k: "k = []" from SRet st k have "final s" by simp
      thus ?thesis by blast
    next
      fix f k' assume k: "k = f#k'"
      from wtst SRet have wte: "\<Gamma> \<turnstile>\<^isub>e e : A'" by blast
      from wte wfg gr obtain v where v: "eval e \<rho> \<Sigma> = Some v"
        and wtv: "\<Sigma> \<turnstile>\<^isub>v v : A'" using eval_safe by blast
      obtain x S T s' \<rho>' \<Sigma>' where f: "f = (x,S,T,s',\<rho>',\<Sigma>')"
        apply (case_tac f) apply blast done
      from wt_k f k have wt_k2: "\<Sigma> \<turnstile> (x,S,T,s',\<rho>',\<Sigma>')#k' : A' \<Rightarrow> A" by simp 
      from wt_k2 show ?thesis
      proof
        fix \<Gamma>' C
        assume wfgp: "wf_env \<Gamma>'" and wtr: "\<Gamma>';\<Sigma>' \<turnstile> \<rho>'"
          and at: "psub \<Sigma> A' = psub \<Sigma>' T" 
          and wtsp: "(x,EVar T)#\<Gamma>' \<turnstile>\<^isub>s s' : C"
          and xg: "x \<notin> fst ` set \<Gamma>'" 
          and wtkp: "\<Sigma>' \<turnstile> k' : C \<Rightarrow> A" and s: "S = A'"
        from wfap gr wtr at have wft: "\<Gamma>' \<turnstile> T" by (rule psub_wf)
        from wft wfgp xg
        have 1: "wf_env ((x, EVar T) # \<Gamma>')" by auto
        have 2: "(x, EVar T) # \<Gamma>';\<Sigma>' \<turnstile> (x, cast v S T) # \<rho>'" 
        proof (rule wt_cons)
          show "\<Sigma>' \<turnstile>\<^isub>v cast v S T : T"
            apply (rule wt_cast)
            using wtv s apply simp
            using at s apply simp
            using wft apply simp done
        next
          from wft show "\<Gamma>' \<turnstile> T" .
        next
          from wtr show "\<Gamma>';\<Sigma>' \<turnstile> \<rho>'" .
        next
          from xg show "x \<notin> dom \<Gamma>'" by simp
        qed
        from st SRet k f v 1 2 show ?thesis
          apply simp apply (rule wts)
          prefer 4 using wtkp apply assumption
          prefer 3 using wtsp apply assumption
          apply assumption+ done
      qed
    qed
  next
    case (SCall x e1 e2 s2)
    from wtst SCall obtain B::ty and C where wte1: "\<Gamma> \<turnstile>\<^isub>e e1 : B \<rightarrow> C" 
      and wte2: "\<Gamma> \<turnstile>\<^isub>e e2 : B" and xg: "x \<notin> dom \<Gamma>"
      and wts2: "(x,EVar C)#\<Gamma> \<turnstile>\<^isub>s s2 : A'" by auto
    from wte1 wfg have wfbc: "\<Gamma> \<turnstile> B \<rightarrow> C" using wte_wts_wft apply auto done
    from wte1 wfg gr obtain v1 where v1: "eval e1 \<rho> \<Sigma> = Some v1"
      and wtv1: "\<Sigma> \<turnstile>\<^isub>v v1 : B \<rightarrow> C" 
      using eval_safe[of \<Gamma> e1 "B\<rightarrow>C" \<Sigma> \<rho>] apply simp apply (erule exE) 
      apply simp done
    from wte2 wfg gr obtain v2 where v2: "eval e2 \<rho> \<Sigma> = Some v2"
      and wtv2: "\<Sigma> \<turnstile>\<^isub>v v2 : B" using eval_safe by blast
    from wtv1 show ?thesis
    proof
      fix c assume "typeof c = B \<rightarrow> C"
      thus ?thesis apply (case_tac c) apply auto done
    next
      fix \<Gamma> \<Sigma>' \<rho> x S sa
      assume "AllT (psub \<Sigma>' (close x 0 S)) = psub \<Sigma> (B \<rightarrow> C)"
      thus ?thesis apply simp done
    next
      fix \<Gamma>'::ty_env and \<Sigma>'  and \<rho>'::env and y and A1::ty and A2::ty and s' 
      assume v1cl: "v1 = Closure y s' \<rho>' \<Sigma>' (A1 \<rightarrow> A2) (B \<rightarrow> C)"
        and wfg2: "wf_env \<Gamma>'" and gr2: "\<Gamma>';\<Sigma>' \<turnstile> \<rho>'" 
        and yg: "y \<notin> fst ` set \<Gamma>'" and wfs12: "\<Gamma>' \<turnstile> A1"
        and sbc: "psub \<Sigma>' A1 \<rightarrow> psub \<Sigma>' A2 = psub \<Sigma> (B \<rightarrow> C)" 
        and wtsp: "(y, EVar A1)#\<Gamma>' \<turnstile>\<^isub>s s' : A2"
      from st SCall v1 v2 v1cl show ?thesis
        apply simp apply (rule wts)
        prefer 3 using wtsp apply assumption
        apply (rule wf_cons1) using yg apply simp
          using wfs12 apply assumption
          using wfg2 apply assumption
      proof -
        show "\<Sigma>' \<turnstile> (x, A2, C, s2, \<rho>, \<Sigma>) # k : A2 \<Rightarrow> A"
          apply (rule cons_stack)
          using wfg apply assumption
          using gr apply assumption
          using sbc apply force
          using wts2 apply blast
          using wfbc apply blast
          using xg apply simp
          using wt_k apply simp
          done
      next
        show "(y, EVar A1) # \<Gamma>';\<Sigma>' \<turnstile> (y, cast v2 B A1) # \<rho>'"
        proof (rule wt_cons)
          from sbc have bs1: "psub \<Sigma> B = psub \<Sigma>' A1" by auto
          from wtv2 bs1 wfs12
          show "\<Sigma>' \<turnstile>\<^isub>v cast v2 B A1 : A1" by (rule wt_cast)
        next
          from wfs12 show "\<Gamma>' \<turnstile> A1" .
        next
          from gr2 show "\<Gamma>'; \<Sigma>' \<turnstile> \<rho>'" .
        next
          from yg show "y \<notin> dom \<Gamma>'" by simp
        qed
      qed
    qed
  next
    case (SInst x e T s1)
    from wtst SInst obtain B::ty
      where wte1: "\<Gamma> \<turnstile>\<^isub>e e : AllT B" and wft: "\<Gamma> \<turnstile> T" and xg: "x \<notin> dom \<Gamma>"
      and wts1: "(x,EVar ([T]B))#\<Gamma> \<turnstile>\<^isub>s s1 : A'" by auto
    from wte1 wfg gr obtain v1 where ev1: "eval e \<rho> \<Sigma> = Some v1"
      and wtv1: "\<Sigma> \<turnstile>\<^isub>v v1 : AllT B"
      using eval_safe[of \<Gamma> e "AllT B" \<Sigma> \<rho>] apply simp 
      apply (erule exE) apply auto done
    from wtv1 show ?thesis
    proof (rule polyval_inv)
      fix c assume "v1 = VConst c" and "typeof c = AllT B"
      thus ?thesis
        apply (case_tac c) apply force apply force done
    next
      fix \<Gamma> \<Sigma>' E x S1 S2 sa
      assume "v1 = Closure x sa E \<Sigma>' (S1 \<rightarrow> S2) (AllT B)"
        and "psub \<Sigma>' S1 \<rightarrow> psub \<Sigma>' S2 = psub \<Sigma> (AllT B)"
      thus ?thesis apply simp done
    next
      fix \<Gamma>' \<Sigma>' and \<rho>'::env and y S' s' 
      assume  v1: "v1 = TAbs y s' \<rho>' \<Sigma>' (AllT (close y 0 S')) (AllT B)" 
        and wfgp: "wf_env \<Gamma>'" and gr2: "\<Gamma>'; \<Sigma>' \<turnstile> \<rho>'" 
        and ygp: "y \<notin> fst ` set \<Gamma>'" 
        and allsb: "AllT (psub \<Sigma>' (close y 0 S')) = psub \<Sigma> (AllT B)"
        and wtsp: "(y,TVar)#\<Gamma>' \<turnstile>\<^isub>s s' : S'"
      let ?T = "psub \<Sigma> T"
      let ?S = "(y,?T)#\<Sigma>'" and ?G = "(y,TVar)#\<Gamma>'"
      from wfgp ygp have wfgp2: "wf_env ?G" apply auto done
      from wft gr have wft2: "[] \<turnstile> psub \<Sigma> T" using psub_tymap_wf by blast
      from st SInst ev1 v1 wtsp show ?thesis 
        apply simp apply (rule wts)
        prefer 3 apply assumption
        using wfgp2 apply assumption
      proof -
        from gr2 wft2 ygp show "?G; ?S \<turnstile> \<rho>'" 
          using weaken_wtenv apply auto done
      next
        from wtsp wfgp2 have wfsp: "?G \<turnstile> S'" using wte_wts_wft apply simp done
        from wfsp have csp: "[FVar y]close y 0 S' = S'"
          using bsub_close_id apply simp done
        from wte1 wfg have wfb: "\<Gamma> \<turnstile> AllT B" using wte_wts_wft apply auto done
        from allsb wfsp wfb ygp gr gr2 wft
        have 1: "psub ((y, psub \<Sigma> T) # \<Sigma>') S' = psub \<Sigma> ([T]B)" 
          apply simp apply (rule psub_close_ext) apply simp apply simp 
          apply clarify apply simp apply simp apply simp apply simp
          apply simp done
        from wfb wft have 2: "\<Gamma> \<turnstile> [T]B" using wf_bsub[of \<Gamma> "Suc 0" B 0 T]
          apply clarsimp done
        from csp wts1 wfg
        show "?S \<turnstile> (x,[FVar y]close y 0 S', ty_bsub T B, s1, \<rho>, \<Sigma>)#k : S' \<Rightarrow> A"
          apply simp apply (rule cons_stack) 
          prefer 4 apply assumption
          apply assumption
          using gr apply assumption
          using allsb apply simp
          using 1 apply assumption
          using 2 apply assumption
          using xg apply assumption
          using wt_k apply assumption
          done
      qed
    qed
  qed
qed

end