Theory TypeSafe

(*  Title:      Jinja/J/SmallTypeSafe.thy
    ID:         $Id: TypeSafe.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

header {* \isaheader{Type Safety Proof} *}

theory TypeSafe = Progress + JWellForm:

subsection{*Basic preservation lemmas*}

text{* First two easy preservation lemmas. *}

theorem red_preserves_hconf:
  "P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩ ==> (!!T E. [| P,E,h \<turnstile> e : T; P \<turnstile> h \<surd> |] ==> P \<turnstile> h' \<surd>)"
and reds_preserves_hconf:
  "P \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',(h',l')⟩ ==> (!!Ts E. [| P,E,h \<turnstile> es [:] Ts; P \<turnstile> h \<surd> |] ==> P \<turnstile> h' \<surd>)"
(*<*)
proof (induct rule:red_reds_induct)
  case (RedNew C FDTs a h h' l)
  have new: "new_Addr h = Some a" and fields: "P \<turnstile> C has_fields FDTs"
   and h': "h' = h(a\<mapsto>(C, init_fields FDTs))"
   and hconf: "P \<turnstile> h \<surd>" and wt_New: "P,E,h \<turnstile> new C : T" .
  from new have None: "h a = None" by(rule new_Addr_SomeD)
  moreover have "P,h \<turnstile> (C,init_fields FDTs) \<surd>"
    using wt_New fields
    by(fastsimp intro!:fconf_init_fields simp:oconf_def)
  ultimately show "P \<turnstile> h' \<surd>" using h' by(fast intro: hconf_new[OF hconf])
next
  case (RedFAss C D F a fs h l v)
  let ?fs' = "fs((F,D)\<mapsto>v)"
  have hconf: "P \<turnstile> h \<surd>" and ha: "h a = Some(C,fs)"
   and wt: "P,E,h \<turnstile> addr a\<bullet>F{D}:=Val v : T" .
  from wt ha obtain FDTs TF Tv where typeofv: "typeofh v = Some Tv"
    and has: "P \<turnstile> C has F:TF in D"
    and sub: "P \<turnstile> Tv ≤ TF" by auto
  have "P,h \<turnstile> (C, ?fs') \<surd>"
  proof (rule oconf_fupd[OF has])
    show "P,h \<turnstile> (C, fs) \<surd>" using hconf ha by(simp add:hconf_def)
    show "P,h \<turnstile> v :≤ TF" using sub typeofv by(simp add:conf_def)
  qed
  with hconf ha show "P \<turnstile> h(a\<mapsto>(C, ?fs')) \<surd>"  by (rule hconf_upd_obj)
qed auto
(*>*)


theorem red_preserves_lconf:
  "P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩ ==>
  (!!T E. [| P,E,h \<turnstile> e:T; P,h \<turnstile> l (:≤)w E |] ==> P,h' \<turnstile> l' (:≤)w E)"
and reds_preserves_lconf:
  "P \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',(h',l')⟩ ==>
  (!!Ts E. [| P,E,h \<turnstile> es[:]Ts; P,h \<turnstile> l (:≤)w E |] ==> P,h' \<turnstile> l' (:≤)w E)"
(*<*)
proof(induct rule:red_reds_induct)
  case RedNew thus ?case
    by(fast intro:lconf_hext red_hext_incr[OF red_reds.RedNew])
next
  case RedLAss thus ?case by(fastsimp elim: lconf_upd simp:conf_def)
next
  case RedFAss thus ?case
    by(fast intro:lconf_hext red_hext_incr[OF red_reds.RedFAss])
next
  case (InitBlockRed T V e e' h h' l l' v v' T')
  have red: "P \<turnstile> ⟨e, (h, l(V\<mapsto>v))⟩ -> ⟨e',(h', l')⟩"
   and IH: "!!T E . [| P,E,h \<turnstile> e:T; P,h \<turnstile> l(V\<mapsto>v) (:≤)w E |]
                     ==> P,h' \<turnstile> l' (:≤)w E"
   and l'V: "l' V = Some v'" and lconf: "P,h \<turnstile> l (:≤)w E"
   and wt: "P,E,h \<turnstile> {V:T := Val v; e} : T'" .
  from lconf_hext[OF lconf red_hext_incr[OF red]]
  have "P,h' \<turnstile> l (:≤)w E" .
  moreover from IH lconf wt have "P,h' \<turnstile> l' (:≤)w E(V\<mapsto>T)"
    by(auto simp del: fun_upd_apply simp: fun_upd_same lconf_upd2 conf_def)
  ultimately show "P,h' \<turnstile> l'(V := l V) (:≤)w E"
    by (fastsimp simp:lconf_def split:split_if_asm)
next
  case (BlockRedNone T V e e' h h' l l' T')
  have red: "P \<turnstile> ⟨e,(h, l(V := None))⟩ -> ⟨e',(h', l')⟩"
   and IH: "!!E T. [| P,E,h \<turnstile> e : T; P,h \<turnstile> l(V:=None) (:≤)w E |]
                   ==> P,h' \<turnstile> l' (:≤)w E"
   and lconf: "P,h \<turnstile> l (:≤)w E" and wt: "P,E,h \<turnstile> {V:T; e} : T'" .
  from lconf_hext[OF lconf red_hext_incr[OF red]]
  have "P,h' \<turnstile> l (:≤)w E" .
  moreover have "P,h' \<turnstile> l' (:≤)w E(V\<mapsto>T)"
    by(rule IH, insert lconf wt, auto simp:lconf_def)
  ultimately show "P,h' \<turnstile> l'(V := l V) (:≤)w E"
    by (fastsimp simp:lconf_def split:split_if_asm)
next
  case (BlockRedSome T V e e' h h' l l' v T')
  have red: "P \<turnstile> ⟨e,(h, l(V := None))⟩ -> ⟨e',(h', l')⟩"
   and IH: "!!E T. [|P,E,h \<turnstile> e : T; P,h \<turnstile> l(V:=None) (:≤)w E|]
                   ==> P,h' \<turnstile> l' (:≤)w E"
   and lconf: "P,h \<turnstile> l (:≤)w E" and wt: "P,E,h \<turnstile> {V:T; e} : T'" .
  from lconf_hext[OF lconf red_hext_incr[OF red]]
  have "P,h' \<turnstile> l (:≤)w E" .
  moreover have "P,h' \<turnstile> l' (:≤)w E(V\<mapsto>T)"
    by(rule IH, insert lconf wt, auto simp:lconf_def)
  ultimately show "P,h' \<turnstile> l'(V := l V) (:≤)w E"
    by (fastsimp simp:lconf_def split:split_if_asm)
qed auto
(*>*)


text{* Preservation of definite assignment more complex and requires a
few lemmas first. *}

lemma [iff]: "!!A. [| length Vs = length Ts; length vs = length Ts|] ==>
 \<D> (blocks (Vs,Ts,vs,e)) A = \<D> e (A \<squnion> ⌊set Vs⌋)"
(*<*)
apply(induct Vs Ts vs e rule:blocks.induct)
apply(simp_all add:hyperset_defs)
done
(*>*)


lemma red_lA_incr: "P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩ ==> ⌊dom l⌋ \<squnion> \<A> e \<sqsubseteq>  ⌊dom l'⌋ \<squnion> \<A> e'"
and reds_lA_incr: "P \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',(h',l')⟩ ==> ⌊dom l⌋ \<squnion> \<A>s es \<sqsubseteq>  ⌊dom l'⌋ \<squnion> \<A>s es'"
(*<*)
apply(induct rule:red_reds_induct)
apply(simp_all del:fun_upd_apply add:hyperset_defs)
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply force
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply(blast dest:red_lcl_incr)
apply(blast dest:red_lcl_incr)
apply blast
apply blast
apply blast
done
(*>*)


text{* Now preservation of definite assignment. *}

lemma assumes wf: "wf_J_prog P"
shows red_preserves_defass:
  "P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩ ==> \<D> e ⌊dom l⌋ ==> \<D> e' ⌊dom l'⌋"
and "P \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',(h',l')⟩ ==> \<D>s es ⌊dom l⌋ ==> \<D>s es' ⌊dom l'⌋"
(*<*)
proof (induct rule:red_reds_induct)
  case BinOpRed1 thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case FAssRed1 thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case CallObj thus ?case by (auto elim!: Ds_mono[OF red_lA_incr])
next
  case RedCall thus ?case
    apply (auto dest!:sees_wf_mdecl[OF wf] simp:wf_mdecl_def elim!:D_mono')
    by(auto simp:hyperset_defs)
next
  case InitBlockRed thus ?case
    by(auto simp:hyperset_defs elim!:D_mono' simp del:fun_upd_apply)
next
  case BlockRedNone thus ?case
    by(auto simp:hyperset_defs elim!:D_mono' simp del:fun_upd_apply)
next
  case BlockRedSome thus ?case
    by(auto simp:hyperset_defs elim!:D_mono' simp del:fun_upd_apply)
next
  case SeqRed thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case CondRed thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case TryRed thus ?case
    by (fastsimp dest:red_lcl_incr intro:D_mono' simp:hyperset_defs)
next
  case ListRed1 thus ?case by (auto elim!: Ds_mono[OF red_lA_incr])
next
  case RedWhile thus ?case by(auto simp:hyperset_defs elim!:D_mono')
qed (auto simp:hyperset_defs)
(*>*)


text{* Combining conformance of heap and local variables: *}

constdefs
  sconf :: "J_prog => env => state => bool"   ("_,_ \<turnstile> _ \<surd>"   [51,51,51]50)
  "P,E \<turnstile> s \<surd>  ≡  let (h,l) = s in P \<turnstile> h \<surd> ∧ P,h \<turnstile> l (:≤)w E"

lemma red_preserves_sconf:
  "[| P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩; P,E,hp s \<turnstile> e : T; P,E \<turnstile> s \<surd> |] ==> P,E \<turnstile> s' \<surd>"
(*<*)
by(fastsimp intro:red_preserves_hconf red_preserves_lconf
            simp add:sconf_def)
(*>*)

lemma reds_preserves_sconf:
  "[| P \<turnstile> ⟨es,s⟩ [->] ⟨es',s'⟩; P,E,hp s \<turnstile> es [:] Ts; P,E \<turnstile> s \<surd> |] ==> P,E \<turnstile> s' \<surd>"
(*<*)
by(fastsimp intro:reds_preserves_hconf reds_preserves_lconf
            simp add:sconf_def)
(*>*)


subsection "Subject reduction"

lemma wt_blocks:
 "!!E. [| length Vs = length Ts; length vs = length Ts |] ==>
       (P,E,h \<turnstile> blocks(Vs,Ts,vs,e) : T) =
       (P,E(Vs[\<mapsto>]Ts),h \<turnstile> e:T ∧ (∃Ts'. map (typeofh) vs = map Some Ts' ∧ P \<turnstile> Ts' [≤] Ts))"
(*<*)
apply(induct Vs Ts vs e rule:blocks.induct)
prefer 5; apply (force simp add:rel_list_all2_Cons2)
apply simp_all
done
(*>*)


theorem assumes wf: "wf_J_prog P"
shows subject_reduction2: "P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩ ==>
  (!!E T. [| P,E \<turnstile> (h,l) \<surd>; P,E,h \<turnstile> e:T |]
           ==> ∃T'. P,E,h' \<turnstile> e':T' ∧ P \<turnstile> T' ≤ T)"
and subjects_reduction2: "P \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',(h',l')⟩ ==>
  (!!E Ts. [| P,E \<turnstile> (h,l) \<surd>; P,E,h \<turnstile> es [:] Ts |]
            ==> ∃Ts'. P,E,h' \<turnstile> es' [:] Ts' ∧ P \<turnstile> Ts' [≤] Ts)"
(*<*)
proof (induct rule:red_reds_induct)
  case (RedCall C D M T Ts a body fs pns h l vs E T')
  have hp: "hp(h,l) a = Some(C,fs)"
   and method: "P \<turnstile> C sees M: Ts->T = (pns,body) in D"
   and wt: "P,E,h \<turnstile> addr a\<bullet>M(map Val vs) : T'" .
  obtain Ts' where wtes: "P,E,h \<turnstile> map Val vs [:] Ts'"
    and subs: "P \<turnstile> Ts' [≤] Ts" and T'isT: "T' = T"
    using wt method hp by (auto dest:sees_method_fun)
  from wtes subs have length_vs: "length vs = length Ts"
    by(fastsimp simp:list_all2_def dest!:WTrts_same_length)
  from sees_wf_mdecl[OF wf method] obtain T''
    where wtabody: "P,[this#pns [\<mapsto>] Class D#Ts] \<turnstile> body :: T''"
    and T''subT: "P \<turnstile> T'' ≤ T" and length_pns: "length pns = length Ts"
    by(fastsimp simp:wf_mdecl_def simp del:map_upds_twist)
  from wtabody have "P,empty(this#pns [\<mapsto>] Class D#Ts),h \<turnstile> body : T''"
    by(rule WT_implies_WTrt)
  hence "P,E(this#pns [\<mapsto>] Class D#Ts),h \<turnstile> body : T''"
    by(rule WTrt_env_mono) simp
  hence "P,E,h \<turnstile> blocks(this#pns, Class D#Ts, Addr a#vs, body) : T''"
  using wtes subs hp sees_method_decl_above[OF method] length_vs length_pns
    by(fastsimp simp add:wt_blocks rel_list_all2_Cons2)
  with T''subT T'isT show ?case by blast
next
  case RedNewFail thus ?case
    by (unfold sconf_def hconf_def) (fastsimp elim!:typeof_OutOfMemory)
next
  case CastRed thus ?case
    by(clarsimp simp:is_refT_def)
      (blast intro: widens_trans dest!:widen_Class[THEN iffD1])
next
  case RedCastFail thus ?case
    by (unfold sconf_def hconf_def)  (fastsimp elim!:typeof_ClassCast)
next
  case (BinOpRed1 bop e1 e1' e2 h l h' l')
  have red: "P \<turnstile> ⟨e1,(h,l)⟩ -> ⟨e1',(h',l')⟩"
   and IH: "!!E T. [|P,E \<turnstile> (h,l) \<surd>; P,E,h \<turnstile> e1:T|]
                 ==> ∃U. P,E,h' \<turnstile> e1' : U ∧ P \<turnstile> U ≤ T"
   and conf: "P,E \<turnstile> (h,l) \<surd>" and wt: "P,E,h \<turnstile> e1 «bop» e2 : T" .
  have "P,E,h' \<turnstile> e1' «bop» e2 : T"
  proof (cases bop)
    assume [simp]: "bop = Eq"
    from wt obtain T1 T2 where [simp]: "T = Boolean"
      and wt1: "P,E,h \<turnstile> e1 : T1" and wt2: "P,E,h \<turnstile> e2 : T2" by auto
    show ?thesis
      using WTrt_hext_mono[OF wt2 red_hext_incr[OF red]] IH[OF conf wt1]
      by auto
  next
    assume  [simp]: "bop = Add"
    from wt have [simp]: "T = Integer"
      and wt1: "P,E,h \<turnstile> e1 : Integer" and wt2: "P,E,h \<turnstile> e2 : Integer"
      by auto
    show ?thesis
      using IH[OF conf wt1] WTrt_hext_mono[OF wt2 red_hext_incr[OF red]]
      by auto
  qed
  thus ?case by auto
next
  case (BinOpRed2 bop e2 e2' h l h' l' v1)
  have red: "P \<turnstile> ⟨e2,(h,l)⟩ -> ⟨e2',(h',l')⟩"
   and IH: "!!E T. [|P,E \<turnstile> (h,l) \<surd>; P,E,h \<turnstile> e2:T|]
                 ==> ∃U. P,E,h' \<turnstile> e2' : U ∧ P \<turnstile> U ≤ T"
   and conf: "P,E \<turnstile> (h,l) \<surd>" and wt: "P,E,h \<turnstile> (Val v1) «bop» e2 : T" .
  have "P,E,h' \<turnstile> (Val v1) «bop» e2' : T"
  proof (cases bop)
    assume [simp]: "bop = Eq"
    from wt obtain T1 T2 where [simp]: "T = Boolean"
      and wt1: "P,E,h \<turnstile> Val v1 : T1" and wt2: "P,E,h \<turnstile> e2:T2" by auto
    show ?thesis
      using IH[OF conf wt2] WTrt_hext_mono[OF wt1 red_hext_incr[OF red]]
      by auto
  next
    assume  [simp]: "bop = Add"
    from wt have [simp]: "T = Integer"
      and wt1: "P,E,h \<turnstile> Val v1 : Integer" and wt2: "P,E,h \<turnstile> e2 : Integer"
      by auto
    show ?thesis
      using IH[OF conf wt2] WTrt_hext_mono[OF wt1 red_hext_incr[OF red]]
      by auto
  qed
  thus ?case by auto
next
  case (RedBinOp bop) thus ?case
  proof (cases bop)
    case Eq thus ?thesis using RedBinOp by auto
  next
    case Add thus ?thesis using RedBinOp by auto
  qed
next
  case RedVar thus ?case by (fastsimp simp:sconf_def lconf_def conf_def)
next
  case LAssRed thus ?case by(blast intro:widen_trans)
next
  case (FAccRed D F e e' h l h' l')
  have IH: "!!E T. [|P,E \<turnstile> (h,l) \<surd>; P,E,h \<turnstile> e : T|]
                 ==> ∃U. P,E,h' \<turnstile> e' : U ∧ P \<turnstile> U ≤ T"
   and conf: "P,E \<turnstile> (h,l) \<surd>" and wt: "P,E,h \<turnstile> e\<bullet>F{D} : T" .
  -- "The goal: ?case = @{prop ?case}"
  -- "Now distinguish the two cases how wt can have arisen."
  { fix C assume wte: "P,E,h \<turnstile> e : Class C"
             and has: "P \<turnstile> C has F:T in D"
    from IH[OF conf wte]
    obtain U where wte': "P,E,h' \<turnstile> e' : U" and UsubC: "P \<turnstile> U ≤ Class C"
      by auto
    -- "Now distinguish what @{term U} can be."
    { assume "U = NT" hence ?case using wte'
        by(blast intro:WTrtFAccNT widen_refl) }
    moreover
    { fix C' assume U: "U = Class C'" and C'subC: "P \<turnstile> C' \<preceq>* C"
      from has_field_mono[OF has C'subC] wte' U
      have ?case by(blast intro:WTrtFAcc) }
    ultimately have ?case using UsubC by(simp add: widen_Class) blast }
  moreover
  { assume "P,E,h \<turnstile> e : NT"
    hence "P,E,h' \<turnstile> e' : NT" using IH[OF conf] by fastsimp
    hence ?case  by(fastsimp intro:WTrtFAccNT widen_refl) }
  ultimately show ?case using wt by blast
next
  case RedFAcc thus ?case
    by(fastsimp simp:sconf_def hconf_def oconf_def fconf_def conf_def has_field_def
                dest:has_fields_fun)
next
  case RedFAccNull thus ?case
    by(fastsimp intro: widen_refl WTThrow[OF WTVal] elim!: typeof_NullPointer
                simp: sconf_def hconf_def)
next
  case (FAssRed1 D F e e' e2 h l h' l')
  have red: "P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩"
   and IH: "!!E T. [|P,E \<turnstile> (h,l) \<surd>; P,E,h \<turnstile> e : T|]
                 ==> ∃U. P,E,h' \<turnstile> e' : U ∧ P \<turnstile> U ≤ T"
   and conf: "P,E \<turnstile> (h,l) \<surd>" and wt: "P,E,h \<turnstile> e\<bullet>F{D}:=e2 : T" .
  from wt have void: "T = Void" by blast
  -- "We distinguish if @{term e} has type @{term NT} or a Class type"
  -- "Remember ?case = @{term ?case}"
  { assume "P,E,h \<turnstile> e : NT"
    hence "P,E,h' \<turnstile> e' : NT" using IH[OF conf] by fastsimp
    moreover obtain T2 where "P,E,h \<turnstile> e2 : T2" using wt by auto
    from this red_hext_incr[OF red] have  "P,E,h' \<turnstile> e2 : T2"
      by(rule WTrt_hext_mono)
    ultimately have ?case using void by(blast intro!:WTrtFAssNT)
  }
  moreover
  { fix C TF T2 assume wt1: "P,E,h \<turnstile> e : Class C" and wt2: "P,E,h \<turnstile> e2 : T2"
    and has: "P \<turnstile> C has F:TF in D" and sub: "P \<turnstile> T2 ≤ TF"
    obtain U where wt1': "P,E,h' \<turnstile> e' : U" and UsubC: "P \<turnstile> U ≤ Class C"
      using IH[OF conf wt1] by blast
    have wt2': "P,E,h' \<turnstile> e2 : T2"
      by(rule WTrt_hext_mono[OF wt2 red_hext_incr[OF red]])
    -- "Is @{term U} the null type or a class type?"
    { assume "U = NT" with wt1' wt2' void have ?case
        by(blast intro!:WTrtFAssNT) }
    moreover
    { fix C' assume UClass: "U = Class C'" and subclass: "P \<turnstile> C' \<preceq>* C"
      have "P,E,h' \<turnstile> e' : Class C'" using wt1' UClass by auto
      moreover have "P \<turnstile> C' has F:TF in D"
        by(rule has_field_mono[OF has subclass])
      ultimately have ?case using wt2' sub void by(blast intro:WTrtFAss) }
    ultimately have ?case using UsubC by(auto simp add:widen_Class) }
  ultimately show ?case using wt by blast
next
  case (FAssRed2 D F e2 e2' h l h' l' v)
  have red: "P \<turnstile> ⟨e2,(h,l)⟩ -> ⟨e2',(h',l')⟩"
   and IH: "!!E T. [|P,E \<turnstile> (h,l) \<surd>; P,E,h \<turnstile> e2 : T|]
                 ==> ∃U. P,E,h' \<turnstile> e2' : U ∧ P \<turnstile> U ≤ T"
   and conf: "P,E \<turnstile> (h,l) \<surd>" and wt: "P,E,h \<turnstile> Val v\<bullet>F{D}:=e2 : T" .
  from wt have [simp]: "T = Void" by auto
  from wt show ?case
  proof (rule WTrt_elim_cases)
    fix C TF T2
    assume wt1: "P,E,h \<turnstile> Val v : Class C"
      and has: "P \<turnstile> C has F:TF in D"
      and wt2: "P,E,h \<turnstile> e2 : T2" and TsubTF: "P \<turnstile> T2 ≤ TF"
    have wt1': "P,E,h' \<turnstile> Val v : Class C"
      by(rule WTrt_hext_mono[OF wt1 red_hext_incr[OF red]])
    obtain T2' where wt2': "P,E,h' \<turnstile> e2' : T2'" and T'subT: "P \<turnstile> T2' ≤ T2"
      using IH[OF conf wt2] by blast
    have "P,E,h' \<turnstile> Val v\<bullet>F{D}:=e2' : Void"
      by(rule WTrtFAss[OF wt1' has wt2' widen_trans[OF T'subT TsubTF]])
    thus ?case by auto
  next
    fix T2 assume null: "P,E,h \<turnstile> Val v : NT" and wt2: "P,E,h \<turnstile> e2 : T2"
    from null have "v = Null" by simp
    moreover
    obtain T2' where "P,E,h' \<turnstile> e2' : T2' ∧ P \<turnstile> T2' ≤ T2"
      using IH[OF conf wt2] by blast
    ultimately show ?thesis by(fastsimp intro:WTrtFAssNT)
  qed
next
  case RedFAss thus ?case by(auto simp del:fun_upd_apply)
next
  case RedFAssNull thus ?case
    by(fastsimp intro: WTThrow[OF WTVal] elim!:typeof_NullPointer simp:sconf_def hconf_def)
next
  case (CallObj M e e' es h l h' l')
  have red: "P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩"
   and IH: "!!E T. [|P,E \<turnstile> (h,l) \<surd>; P,E,h \<turnstile> e : T|]
                 ==> ∃U. P,E,h' \<turnstile> e' : U ∧ P \<turnstile> U ≤ T"
   and conf: "P,E \<turnstile> (h,l) \<surd>" and wt: "P,E,h \<turnstile> e\<bullet>M(es) : T" .
  -- "We distinguish if @{term e} has type @{term NT} or a Class type"
  -- "Remember ?case = @{term ?case}"
  { assume "P,E,h \<turnstile> e:NT"
    hence "P,E,h' \<turnstile> e' : NT" using IH[OF conf] by fastsimp
    moreover
    fix Ts assume wtes: "P,E,h \<turnstile> es [:] Ts"
    have "P,E,h' \<turnstile> es [:] Ts"
      by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]])
    ultimately have ?case by(blast intro!:WTrtCallNT) }
  moreover
  { fix C D Ts Us pns body
    assume wte: "P,E,h \<turnstile> e : Class C"
      and method: "P \<turnstile> C sees M:Ts->T = (pns,body) in D"
      and wtes: "P,E,h \<turnstile> es [:] Us" and subs: "P \<turnstile> Us [≤] Ts"
    obtain U where wte': "P,E,h' \<turnstile> e' : U" and UsubC: "P \<turnstile> U ≤ Class C"
      using IH[OF conf wte] by blast
    -- "Is @{term U} the null type or a class type?"
    { assume "U = NT"
      moreover have "P,E,h' \<turnstile> es [:] Us"
        by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]])
      ultimately have ?case using wte' by(blast intro!:WTrtCallNT) }
    moreover
    { fix C' assume UClass: "U = Class C'" and subclass: "P \<turnstile> C' \<preceq>* C"
      have "P,E,h' \<turnstile> e' : Class C'" using wte' UClass by auto
      moreover obtain Ts' T' pns' body' D'
        where method': "P \<turnstile> C' sees M:Ts'->T' = (pns',body') in D'"
        and subs': "P \<turnstile> Ts [≤] Ts'" and sub': "P \<turnstile> T' ≤ T"
        using Call_lemma[OF method subclass wf] by fast
      moreover have "P \<turnstile> D' \<preceq>* D"
        by(rule sees_method_decl_mono[OF subclass method method'])
      moreover have "P,E,h' \<turnstile> es [:] Us"
        by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]])
      ultimately have ?case
        using subs by(blast intro:WTrtCall rtrancl_trans widens_trans) }
    ultimately have ?case using UsubC by(auto simp add:widen_Class) }
  ultimately show ?case using wt by auto
next
  case (CallParams M es es' h l h' l' v)
  have reds: "P \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',(h',l')⟩"
   and IH: "!!E Ts. [|P,E \<turnstile> (h,l) \<surd>; P,E,h \<turnstile> es [:] Ts|]
                 ==> ∃Us. P,E,h' \<turnstile> es' [:] Us ∧ P \<turnstile> Us [≤] Ts"
   and conf: "P,E \<turnstile> (h,l) \<surd>" and wt: "P,E,h \<turnstile> Val v\<bullet>M(es) : T" .
  from wt show ?case
  proof (rule WTrt_elim_cases)
    fix C D Ts Us pns body
    assume wte: "P,E,h \<turnstile> Val v : Class C"
      and "P \<turnstile> C sees M:Ts->T = (pns,body) in D"
      and wtes: "P,E,h \<turnstile> es [:] Us" and "P \<turnstile> Us [≤] Ts"
    moreover have "P,E,h' \<turnstile> Val v : Class C"
      by(rule WTrt_hext_mono[OF wte reds_hext_incr[OF reds]])
    moreover
    obtain Us' where "P,E,h' \<turnstile> es' [:] Us' ∧ P \<turnstile> Us' [≤] Us"
      using IH[OF conf wtes] by blast
    ultimately show ?thesis by(blast intro:WTrtCall widens_trans)
  next
    fix Us
    assume null: "P,E,h \<turnstile> Val v : NT" and wtes: "P,E,h \<turnstile> es [:] Us"
    from null have "v = Null" by simp
    moreover
    obtain Us' where "P,E,h' \<turnstile> es' [:] Us' ∧ P \<turnstile> Us' [≤] Us"
      using IH[OF conf wtes] by blast
    ultimately show ?thesis by(fastsimp intro:WTrtCallNT)
  qed
next
  case RedCallNull thus ?case
    by(fastsimp intro: WTThrow[OF WTVal] elim!:typeof_NullPointer simp: sconf_def hconf_def)
next
  case (InitBlockRed T V e e' h h' l l' v v' E T')
  have red: "P \<turnstile> ⟨e, (h,l(V\<mapsto>v))⟩ -> ⟨e',(h',l')⟩"
   and IH: "!!E T. [|P,E \<turnstile> (h,l(V\<mapsto>v)) \<surd>; P,E,h \<turnstile> e : T|]
                    ==> ∃U. P,E,h' \<turnstile> e' : U ∧ P \<turnstile> U ≤ T"
   and v': "l' V = Some v'" and conf: "P,E \<turnstile> (h,l) \<surd>"
   and wt: "P,E,h \<turnstile> {V:T := Val v; e} : T'" .
  from wt obtain T1 where wt1: "typeofh v = Some T1"
    and T1subT: "P \<turnstile> T1 ≤ T" and wt2: "P,E(V\<mapsto>T),h \<turnstile> e : T'" by auto
  have lconf2: "P,h \<turnstile> l(V\<mapsto>v) (:≤)w E(V\<mapsto>T)" using conf wt1 T1subT
    by(simp add:sconf_def lconf_upd2 conf_def)
  have "∃T1'. typeofh' v' = Some T1' ∧ P \<turnstile> T1' ≤ T"
    using v' red_preserves_lconf[OF red wt2 lconf2]
    by(fastsimp simp:lconf_def conf_def)
  with IH conf lconf2 wt2 show ?case by (fastsimp simp add:sconf_def)
next
  case BlockRedNone thus ?case
    by(auto simp del:fun_upd_apply)(fastsimp simp:sconf_def lconf_def)
next
  case (BlockRedSome T V e e' h h' l l' v E Te)
  have red: "P \<turnstile> ⟨e,(h,l(V:=None))⟩ -> ⟨e',(h',l')⟩"
   and IH: "!!E T. [|P,E \<turnstile> (h,l(V:=None)) \<surd>; P,E,h \<turnstile> e : T|]
                   ==> ∃T'. P,E,h' \<turnstile> e' : T' ∧ P \<turnstile> T' ≤ T"
   and Some: "l' V = Some v" and conf: "P,E \<turnstile> (h,l) \<surd>"
   and wt: "P,E,h \<turnstile> {V:T; e} : Te" .
  obtain Te' where IH': "P,E(V\<mapsto>T),h' \<turnstile> e' : Te' ∧ P \<turnstile> Te' ≤ Te"
    using IH conf wt by(fastsimp simp:sconf_def lconf_def)
  have "P,h' \<turnstile> l' (:≤)w E(V\<mapsto>T)" using conf wt
    by(fastsimp intro:red_preserves_lconf[OF red] simp:sconf_def lconf_def)
  hence "P,h' \<turnstile> v :≤ T" using Some by(fastsimp simp:lconf_def)
  with IH' show ?case
    by(fastsimp simp:sconf_def conf_def fun_upd_same simp del:fun_upd_apply)
next
  case SeqRed thus ?case
    by auto (blast dest:WTrt_hext_mono[OF _ red_hext_incr])
next
  case CondRed thus ?case
    by auto (blast intro:WTrt_hext_mono[OF _ red_hext_incr])+
next
  case ThrowRed thus ?case
    by(auto simp:is_refT_def)(blast dest:widen_Class[THEN iffD1])+
next
  case RedThrowNull thus ?case
    by(fastsimp intro: WTThrow[OF WTVal] elim!:typeof_NullPointer simp:sconf_def hconf_def)
next
  case TryRed thus ?case
    by auto (blast intro:widen_trans WTrt_hext_mono[OF _ red_hext_incr])
next
  case RedTryFail thus ?case
    by(fastsimp intro: WTrtThrow[OF WTrtVal] simp:sconf_def hconf_def)
next
  case ListRed1 thus ?case
    by(fastsimp dest: WTrts_hext_mono[OF _ red_hext_incr])
next
  case ListRed2 thus ?case
    by(fastsimp dest: hext_typeof_mono[OF reds_hext_incr])
qed fastsimp+ (* esp all Throw propagation rules are dealt with here *)
(*>*)


corollary subject_reduction:
  "[| wf_J_prog P; P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩; P,E \<turnstile> s \<surd>; P,E,hp s \<turnstile> e:T |]
  ==> ∃T'. P,E,hp s' \<turnstile> e':T' ∧ P \<turnstile> T' ≤ T"
(*<*)by(cases s, cases s', fastsimp dest:subject_reduction2)(*>*)

corollary subjects_reduction:
  "[| wf_J_prog P; P \<turnstile> ⟨es,s⟩ [->] ⟨es',s'⟩; P,E \<turnstile> s \<surd>; P,E,hp s \<turnstile> es[:]Ts |]
  ==> ∃Ts'. P,E,hp s' \<turnstile> es'[:]Ts' ∧ P \<turnstile> Ts' [≤] Ts"
(*<*)by(cases s, cases s', fastsimp dest:subjects_reduction2)(*>*)


subsection {* Lifting to @{text"->*"} *}

text{* Now all these preservation lemmas are first lifted to the transitive
closure \dots *}

lemma Red_preserves_sconf:
assumes wf: "wf_J_prog P" and Red: "P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩"
shows "!!T. [| P,E,hp s \<turnstile> e : T; P,E \<turnstile> s \<surd> |] ==> P,E \<turnstile> s' \<surd>"
(*<*)
using Red
proof (induct rule:converse_rtrancl_induct2)
  case refl show ?case .
next
  case step thus ?case
    by(blast intro:red_preserves_sconf dest: subject_reduction[OF wf])
qed
(*>*)


lemma Red_preserves_defass:
assumes wf: "wf_J_prog P" and reds: "P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩"
shows "\<D> e ⌊dom(lcl s)⌋ ==> \<D> e' ⌊dom(lcl s')⌋"
using reds
proof (induct rule:converse_rtrancl_induct2)
  case refl thus ?case .
next
  case (step e s e' s') thus ?case
    by(cases s,cases s')(auto dest:red_preserves_defass[OF wf])
qed


lemma Red_preserves_type:
assumes wf: "wf_J_prog P" and Red: "P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩"
shows "!!T. [| P,E \<turnstile> s\<surd>; P,E,hp s \<turnstile> e:T |]
    ==> ∃T'. P \<turnstile> T' ≤ T ∧ P,E,hp s' \<turnstile> e':T'"
(*<*)
using Red
proof (induct rule:converse_rtrancl_induct2)
  case refl thus ?case by blast
next
  case step thus ?case
    by(blast intro:widen_trans red_preserves_sconf
             dest:subject_reduction[OF wf])
qed
(*>*)


subsection {* Lifting to @{text"=>"} *}

text{* \dots and now to the big step semantics, just for fun. *}

lemma eval_preserves_sconf:
  "[| wf_J_prog P; P \<turnstile> ⟨e,s⟩ => ⟨e',s'⟩; P,E \<turnstile> e::T; P,E \<turnstile> s\<surd> |] ==> P,E \<turnstile> s'\<surd>"
(*<*)
by(blast intro:Red_preserves_sconf big_by_small WT_implies_WTrt wf_prog_wwf_prog)
(*>*)


lemma eval_preserves_type: assumes wf: "wf_J_prog P"
shows "[| P \<turnstile> ⟨e,s⟩ => ⟨e',s'⟩; P,E \<turnstile> s\<surd>; P,E \<turnstile> e::T |]
   ==> ∃T'. P \<turnstile> T' ≤ T ∧ P,E,hp s' \<turnstile> e':T'"
(*<*)
by(blast dest:big_by_small[OF wf_prog_wwf_prog[OF wf]]
              WT_implies_WTrt Red_preserves_type[OF wf])
(*>*)


subsection "The final polish"

text{* The above preservation lemmas are now combined and packed nicely. *}

constdefs
  wf_config :: "J_prog => env => state => expr => ty => bool"   ("_,_,_ \<turnstile> _ : _ \<surd>"   [51,0,0,0,0]50)
  "P,E,s \<turnstile> e:T \<surd>  ≡  P,E \<turnstile> s \<surd> ∧ P,E,hp s \<turnstile> e:T"

theorem Subject_reduction: assumes wf: "wf_J_prog P"
shows "P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==> P,E,s \<turnstile> e : T \<surd>
       ==> ∃T'. P,E,s' \<turnstile> e' : T' \<surd> ∧ P \<turnstile> T' ≤ T"
(*<*)
by(force simp add: wf_config_def
   elim:red_preserves_sconf dest:subject_reduction[OF wf])
(*>*)


theorem Subject_reductions:
assumes wf: "wf_J_prog P" and reds: "P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩"
shows "!!T. P,E,s \<turnstile> e:T \<surd> ==> ∃T'. P,E,s' \<turnstile> e':T' \<surd> ∧ P \<turnstile> T' ≤ T"
(*<*)
using reds
proof (induct rule:converse_rtrancl_induct2)
  case refl thus ?case by blast
next
  case step thus ?case
    by(blast dest:Subject_reduction[OF wf] intro:widen_trans)
qed
(*>*)


corollary Progress: assumes wf: "wf_J_prog P"
shows "[| P,E,s  \<turnstile> e : T \<surd>; \<D> e ⌊dom(lcl s)⌋; ¬ final e |] ==> ∃e' s'. P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩"
(*<*)
using progress[OF wf_prog_wwf_prog[OF wf]]
by(auto simp:wf_config_def sconf_def)
(*>*)


corollary TypeSafety:
  "[| wf_J_prog P; P,E \<turnstile> s \<surd>; P,E \<turnstile> e::T; \<D> e ⌊dom(lcl s)⌋;
     P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩; ¬(∃e'' s''. P \<turnstile> ⟨e',s'⟩ -> ⟨e'',s''⟩) |]
 ==> (∃v. e' = Val v ∧ P,hp s' \<turnstile> v :≤ T) ∨
      (∃a. e' = Throw a ∧ a ∈ dom(hp s'))"
(*<*)
apply(subgoal_tac " P,E,s \<turnstile> e:T \<surd>")
 prefer 2
 apply(fastsimp simp:wf_config_def dest:WT_implies_WTrt)
apply(frule (2) Subject_reductions)
apply(erule exE conjE)+
apply(frule (2) Red_preserves_defass)
apply(subgoal_tac "final e'")
 prefer 2
 apply(blast dest: Progress)
apply (fastsimp simp:wf_config_def final_def conf_def dest: Progress)
done
(*>*)


end