# Theory JTypeSafe

Up to index of Isabelle/HOL/MicroJava

theory JTypeSafe
imports Eval Conform
begin

    (*  Title:      HOL/MicroJava/J/JTypeSafe.thy
        ID:         $Id: JTypeSafe.thy,v 1.13 2005/06/17 14:13:09 haftmann Exp $
        Author:     David von Oheimb
        Copyright   1999 Technische Universitaet Muenchen
    *)

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

    theory JTypeSafe imports Eval Conform begin

    declare split_beta [simp]

    lemma NewC_conforms:
    "[|h a = None; (x,(h, l))::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==>
      (x,(h(a\<mapsto>(C,(init_vars (fields (G,C))))), l))::\<preceq>(G, lT)"
    apply( erule conforms_upd_obj)
    apply(  unfold oconf_def)
    apply(  auto dest!: fields_is_type simp add: wf_prog_ws_prog)
    done

    lemma Cast_conf:
     "[| wf_prog wf_mb G; G,h\<turnstile>v::\<preceq>CC; G\<turnstile>CC \<preceq>? Class D; cast_ok G D h v|]
      ==> G,h\<turnstile>v::\<preceq>Class D"
    apply (case_tac "CC")
    apply simp
    apply (case_tac "ref_ty")
    apply (clarsimp simp add: conf_def)
    apply simp
    apply (ind_cases "G \<turnstile> Class cname \<preceq>? Class D", simp)
    apply (rule conf_widen, assumption+) apply (erule widen.subcls)

    apply (unfold cast_ok_def)
    apply( case_tac "v = Null")
    apply(  simp)
    apply(  clarify)
    apply( drule (1) non_npD)
    apply( auto intro!: conf_AddrI simp add: obj_ty_def)
    done

    lemma FAcc_type_sound:
    "[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (x,(h,l))::\<preceq>(G,lT);
      x' = None --> G,h\<turnstile>a'::\<preceq> Class C; np a' x' = None |] ==>
      G,h\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\<preceq>ft"
    apply( drule np_NoneD)
    apply( erule conjE)
    apply( erule (1) notE impE)
    apply( drule non_np_objD)
    apply   auto
    apply( drule conforms_heapD [THEN hconfD])
    apply(  assumption)
    apply (frule wf_prog_ws_prog)
    apply( drule (2) widen_cfs_fields)
    apply( drule (1) oconf_objD)
    apply auto
    done

    lemma FAss_type_sound:
     "[| wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a);
        (G, lT)\<turnstile>v::T'; G\<turnstile>T'\<preceq>ft;
        (G, lT)\<turnstile>aa::Class C;
        field (G,C) fn = Some (fd, ft); h''≤|h';
        x' = None --> G,h'\<turnstile>a'::\<preceq> Class C; h'≤|h;
        Norm (h, l)::\<preceq>(G, lT); G,h\<turnstile>x::\<preceq>T'; np a' x' = None|] ==>
      h''≤|h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))) ∧
      Norm(h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))), l)::\<preceq>(G, lT) ∧
      G,h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x))))\<turnstile>x::\<preceq>T'"
    apply( drule np_NoneD)
    apply( erule conjE)
    apply( simp)
    apply( drule non_np_objD)
    apply(  assumption)
    apply( clarify)
    apply( simp (no_asm_use))
    apply( frule (1) hext_objD)
    apply( erule exE)
    apply( simp)
    apply( clarify)
    apply( rule conjI)
    apply(  fast elim: hext_trans hext_upd_obj)
    apply( rule conjI)
    prefer 2
    apply(  fast elim: conf_upd_obj [THEN iffD2])

    apply( rule conforms_upd_obj)
    apply   auto
    apply(  rule_tac [2] hextI)
    prefer 2
    apply(  force)
    apply( rule oconf_hext)
    apply(  erule_tac [2] hext_upd_obj)
    apply (frule wf_prog_ws_prog)
    apply( drule (2) widen_cfs_fields)
    apply( rule oconf_obj [THEN iffD2])
    apply( simp (no_asm))
    apply( intro strip)
    apply( case_tac "(aaa, b) = (fn, fd)")
    apply(  simp)
    apply(  fast intro: conf_widen)
    apply( fast dest: conforms_heapD [THEN hconfD] oconf_objD)
    done

    lemma Call_lemma2: "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs;
       list_all2 (λT T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT;
      length pTs' = length pns; distinct pns;
      Ball (set lvars) (split (λvn. is_type G))
      |] ==> G,h\<turnstile>init_vars lvars(pns[\<mapsto>]pvs)[::\<preceq>]map_of lvars(pns[\<mapsto>]pTs')"
    apply (unfold wf_mhead_def)
    apply( clarsimp)
    apply( rule lconf_ext_list)
    apply(    rule Ball_set_table [THEN lconf_init_vars])
    apply(    force)
    apply(   assumption)
    apply(  assumption)
    apply( erule (2) conf_list_gext_widen)
    done

    lemma Call_type_sound:
     "[| wf_java_prog G; a' ≠ Null; Norm (h, l)::\<preceq>(G, lT); class G C = Some y;
         max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc≤|xh; xh≤|h;
         list_all2 (conf G h) pvs pTsa;
         (md, rT, pns, lvars, blk, res) =
                   the (method (G,fst (the (h (the_Addr a')))) (mn, pTs'));
      ∀lT. (np a' None, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) -->
      (G, lT)\<turnstile>blk\<surd> -->  h≤|xi ∧  (xcptb, xi, xl)::\<preceq>(G, lT);
      ∀lT. (xcptb,xi, xl)::\<preceq>(G, lT) --> (∀T. (G, lT)\<turnstile>res::T -->
              xi≤|h' ∧ (x',h', xj)::\<preceq>(G, lT) ∧ (x' = None --> G,h'\<turnstile>v::\<preceq>T));
      G,xh\<turnstile>a'::\<preceq> Class C
      |] ==>
      xc≤|h' ∧ (x',(h', l))::\<preceq>(G, lT) ∧  (x' = None --> G,h'\<turnstile>v::\<preceq>rTa)"
    apply( drule max_spec2mheads)
    apply( clarify)
    apply( drule (2) non_np_objD')
    apply( clarsimp)
    apply( frule (1) hext_objD)
    apply( clarsimp)
    apply( drule (3) Call_lemma)
    apply( clarsimp simp add: wf_java_mdecl_def)
    apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl)
    apply( drule spec, erule impE,  erule_tac [2] notE impE, tactic "assume_tac 2")
    apply(  rule conformsI)
    apply(   erule conforms_heapD)
    apply(  rule lconf_ext)
    apply(   force elim!: Call_lemma2)
    apply(  erule conf_hext, erule (1) conf_obj_AddrI)
    apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl)
    apply (simp add: conforms_def)

    apply( erule conjE)
    apply( drule spec, erule (1) impE)
    apply( drule spec, erule (1) impE)
    apply( erule_tac V = "?E\<turnstile>res::?rT" in thin_rl)
    apply( clarify)
    apply( rule conjI)
    apply(  fast intro: hext_trans)
    apply( rule conjI)
    apply(  rule_tac [2] impI)
    apply(  erule_tac [2] notE impE, tactic "assume_tac 2")
    apply(  frule_tac [2] conf_widen)
    apply(    tactic "assume_tac 4")
    apply(   tactic "assume_tac 2")
    prefer 2
    apply(  fast elim!: widen_trans)
    apply (rule conforms_xcpt_change)
    apply( rule conforms_hext) apply assumption
    apply(  erule (1) hext_trans)
    apply( erule conforms_heapD)
    apply (simp add: conforms_def)
    done

    declare split_if [split del]
    declare fun_upd_apply [simp del]
    declare fun_upd_same [simp]
    declare wf_prog_ws_prog [simp]

    ML{*
    val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
      (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
    *}
    ML{*
    Unify.search_bound := 40;
    Unify.trace_bound  := 40
    *}

    theorem eval_evals_exec_type_sound:
    "wf_java_prog G ==>
      (G\<turnstile>(x,(h,l)) -e  \<succ>v  -> (x', (h',l')) -->
          (∀lT.   (x,(h ,l ))::\<preceq>(G,lT) --> (∀T . (G,lT)\<turnstile>e  :: T -->
          h≤|h' ∧ (x',(h',l'))::\<preceq>(G,lT) ∧ (x'=None --> G,h'\<turnstile>v  ::\<preceq> T )))) ∧
      (G\<turnstile>(x,(h,l)) -es[\<succ>]vs-> (x', (h',l')) -->
          (∀lT.   (x,(h ,l ))::\<preceq>(G,lT) --> (∀Ts. (G,lT)\<turnstile>es[::]Ts -->
          h≤|h' ∧ (x',(h',l'))::\<preceq>(G,lT) ∧ (x'=None --> list_all2 (λv T. G,h'\<turnstile>v::\<preceq>T) vs Ts)))) ∧
      (G\<turnstile>(x,(h,l)) -c       -> (x', (h',l')) -->
          (∀lT.   (x,(h ,l ))::\<preceq>(G,lT) -->       (G,lT)\<turnstile>c  \<surd> -->
          h≤|h' ∧ (x',(h',l'))::\<preceq>(G,lT)))"
    apply( rule eval_evals_exec_induct)
    apply( unfold c_hupd_def)

    -- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
    apply( simp_all)
    apply( tactic "ALLGOALS strip_tac")
    apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims")
                     THEN_ALL_NEW Full_simp_tac) *})
    apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")

    -- "Level 7"
    -- "15 NewC"
    apply (drule sym)
    apply( drule new_AddrD)
    apply( erule disjE)
    prefer 2
    apply(  simp (no_asm_simp))
    apply (rule conforms_xcpt_change, assumption)
    apply (simp (no_asm_simp) add: xconf_def)
    apply( clarsimp)
    apply( rule conjI)
    apply(  force elim!: NewC_conforms)
    apply( rule conf_obj_AddrI)
    apply(  rule_tac [2] rtrancl_refl)
    apply( simp (no_asm))

    -- "for Cast"
    defer 1

    -- "14 Lit"
    apply( erule conf_litval)

    -- "13 BinOp"
    apply (tactic "forward_hyp_tac")
    apply (tactic "forward_hyp_tac")
    apply( rule conjI, erule (1) hext_trans)
    apply( erule conjI)
    apply( clarsimp)
    apply( drule eval_no_xcpt)
    apply( simp split add: binop.split)

    -- "12 LAcc"
    apply simp
    apply( fast elim: conforms_localD [THEN lconfD])

    -- "for FAss"
    apply( tactic {* EVERY'[eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims")
           THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*})

    -- "for if"
    apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8*})

    apply (tactic "forward_hyp_tac")

    -- "11+1 if"
    prefer 8
    apply(  fast intro: hext_trans)
    prefer 8
    apply(  fast intro: hext_trans)

    -- "10 Expr"
    prefer 7
    apply( fast)

    -- "9 ???"
    apply( simp_all)

    -- "8 Cast"
    prefer 8
    apply (rule conjI)
      apply (fast intro: conforms_xcpt_change xconf_raise_if)

      apply clarify
      apply (drule raise_if_NoneD)
      apply (clarsimp)
      apply (rule Cast_conf)
      apply assumption+

    -- "7 LAss"
    apply (fold fun_upd_def)
    apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims")
                     THEN_ALL_NEW Full_simp_tac) 1 *})
    apply (intro strip)
    apply (case_tac E)
    apply (simp)
    apply( blast intro: conforms_upd_local conf_widen)

    -- "6 FAcc"
    apply (rule conjI)
      apply (simp add: np_def)
      apply (fast intro: conforms_xcpt_change xconf_raise_if)
    apply( fast elim!: FAcc_type_sound)

    -- "5 While"
    prefer 5
    apply(erule_tac V = "?a --> ?b" in thin_rl)
    apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop)
    apply(force elim: hext_trans)

    apply (tactic "forward_hyp_tac")

    -- "4 Cond"
    prefer 4
    apply (case_tac "the_Bool v")
    apply simp
    apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
    apply simp
    apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)

    -- "3 ;;"
    prefer 3
    apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)

    -- "2 FAss"
    apply (subgoal_tac "(np a' x1, ab, ba) ::\<preceq> (G, lT)")
      prefer 2
      apply (simp add: np_def)
      apply (fast intro: conforms_xcpt_change xconf_raise_if)
    apply( case_tac "x2")
      -- "x2 = None"
      apply (simp)
      apply (tactic forward_hyp_tac, clarify)
      apply( drule eval_no_xcpt)
      apply( erule FAss_type_sound, rule HOL.refl, assumption+)
      -- "x2 = Some a"
      apply (  simp (no_asm_simp))
      apply(  fast intro: hext_trans)

    apply( tactic prune_params_tac)
    -- "Level 52"

    -- "1 Call"
    apply( case_tac "x")
    prefer 2
    apply(  clarsimp)
    apply(  drule exec_xcpt)
    apply(  simp)
    apply(  drule_tac eval_xcpt)
    apply(  simp)
    apply(  fast elim: hext_trans)
    apply( clarify)
    apply( drule evals_no_xcpt)
    apply( simp)
    apply( case_tac "a' = Null")
    apply(  simp)
    apply(  drule exec_xcpt)
    apply(  simp)
    apply(  drule eval_xcpt)
    apply(  simp)
    apply (rule conjI)
      apply(  fast elim: hext_trans)
      apply (rule conforms_xcpt_change, assumption)
      apply (simp (no_asm_simp) add: xconf_def)
    apply(clarsimp)

    apply( drule ty_expr_is_type, simp)
    apply(clarsimp)
    apply(unfold is_class_def)
    apply(clarsimp)

    apply(rule Call_type_sound);
    prefer 11
    apply blast
    apply (simp (no_asm_simp))+

    done
    ML{*
    Unify.search_bound := 20;
    Unify.trace_bound  := 20
    *}

    lemma eval_type_sound: "!!E s s'.
      [| wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T; G=prg E |]
      ==> (x',s')::\<preceq>E ∧ (x'=None --> G,heap s'\<turnstile>v::\<preceq>T) ∧ heap s ≤| heap s'"
    apply (simp (no_asm_simp) only: split_tupled_all)
    apply (drule eval_evals_exec_type_sound [THEN conjunct1, THEN mp, THEN spec, THEN mp])
    apply auto
    done

    lemma evals_type_sound: "!!E s s'.
      [| wf_java_prog G; G\<turnstile>(x,s) -es[\<succ>]vs -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>es[::]Ts; G=prg E |]
      ==> (x',s')::\<preceq>E ∧ (x'=None --> (list_all2 (λv T. G,heap s'\<turnstile>v::\<preceq>T) vs Ts)) ∧ heap s ≤| heap s'"
    apply (simp (no_asm_simp) only: split_tupled_all)
    apply (drule eval_evals_exec_type_sound [THEN conjunct2, THEN conjunct1, THEN mp, THEN spec, THEN mp])
    apply auto
    done

    lemma exec_type_sound: "!!E s s'.
      [| wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); (x,s)::\<preceq>E; E\<turnstile>s0\<surd>; G=prg E |]
      ==> (x',s')::\<preceq>E ∧ heap s ≤| heap s'"
    apply( simp (no_asm_simp) only: split_tupled_all)
    apply (drule eval_evals_exec_type_sound
                 [THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp])
    apply   auto
    done

    theorem all_methods_understood:
    "[|G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>a'-> Norm s'; a' ≠ Null;
              (x,s)::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig ≠ None|] ==>
      method (G,fst (the (heap s' (the_Addr a')))) sig ≠ None"
    apply (frule eval_type_sound, assumption+)
    apply(clarsimp)
    apply( frule widen_methd)
    apply assumption
    prefer 2
    apply(  fast)
    apply( drule non_npD)
    apply auto
    done

    declare split_beta [simp del]
    declare fun_upd_apply [simp]
    declare wf_prog_ws_prog [simp del]

    end

lemma NewC_conforms:

      [| h a = None; (x, h, l) ::<= (G, lT); wf_prog wf_mb G; is_class G C |]
      ==> (x, h(a |-> (C, init_vars (fields (G, C)))), l) ::<= (G, lT)

lemma Cast_conf:

      [| wf_prog wf_mb G; G,h |- v ::<= CC; G |- CC <=? Class D; cast_ok G D h v |]
      ==> G,h |- v ::<= Class D

lemma FAcc_type_sound:

      [| wf_prog wf_mb G; field (G, C) fn = Some (fd, ft); (x, h, l) ::<= (G, lT);
         x' = None --> G,h |- a' ::<= Class C; np a' x' = None |]
      ==> G,h |- the (snd (the (h (the_Addr a'))) (fn, fd)) ::<= ft

lemma FAss_type_sound:

      [| wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a); (G, lT) |- v :: T';
         G |- T' <= ft; (G, lT) |- aa :: Class C; field (G, C) fn = Some (fd, ft);
         h'' <=| h'; x' = None --> G,h' |- a' ::<= Class C; h' <=| h;
         Norm (h, l) ::<= (G, lT); G,h |- x ::<= T'; np a' x' = None |]
      ==> h'' <=| h(a |-> (c, fs((fn, fd) |-> x))) ∧
          Norm (h(a |-> (c, fs((fn, fd) |-> x))), l) ::<= (G, lT) ∧ G,h(a |->
          (c, fs((fn, fd) |-> x))) |- x ::<= T'

lemma Call_lemma2:

      [| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs;
         list_all2 (%T T'. G |- T <= T') pTs pTs'; wf_mhead G (mn, pTs') rT;
         length pTs' = length pns; distinct pns; ∀(vn, y)∈set lvars. is_type G y |]
      ==> G,h |- init_vars lvars(pns [|->] pvs) [::<=] map_of lvars(pns [|->] pTs')

lemma Call_type_sound:

      [| wf_java_prog G; a' ≠ Null; Norm (h, l) ::<= (G, lT); class G C = Some y;
         max_spec G C (mn, pTsa) = {((mda, rTa), pTs')}; xc <=| xh; xh <=| h;
         list_all2 (conf G h) pvs pTsa;
         (md, rT, pns, lvars, blk, res) = the (method (G, cname_of h a') (mn, pTs'));
         ∀lT. (np a' None, h, init_vars lvars(pns [|->] pvs, This |->
               a')) ::<= (G, lT) -->
              (G, lT) |- blk [ok] --> h <=| xi ∧ (xcptb, xi, xl) ::<= (G, lT);
         ∀lT. (xcptb, xi, xl) ::<= (G, lT) -->
              (∀T. (G, lT) |- res :: T -->
                   xi <=| h' ∧
                   (x', h', xj) ::<= (G, lT) ∧ (x' = None --> G,h' |- v ::<= T));
         G,xh |- a' ::<= Class C |]
      ==> xc <=| h' ∧ (x', h', l) ::<= (G, lT) ∧ (x' = None --> G,h' |- v ::<= rTa)

theorem eval_evals_exec_type_sound:

      wf_java_prog G
      ==> (((x, h, l), e, v, x', h', l') ∈ eval G -->
           (∀lT. (x, h, l) ::<= (G, lT) -->
                 (∀T. (G, lT) |- e :: T -->
                      h <=| h' ∧
                      (x', h', l') ::<= (G, lT) ∧
                      (x' = None --> G,h' |- v ::<= T)))) ∧
          (((x, h, l), es, vs, x', h', l') ∈ evals G -->
           (∀lT. (x, h, l) ::<= (G, lT) -->
                 (∀Ts. (G, lT) |- es [::] Ts -->
                       h <=| h' ∧
                       (x', h', l') ::<= (G, lT) ∧
                       (x' = None --> list_all2 (conf G h') vs Ts)))) ∧
          (((x, h, l), c, x', h', l') ∈ exec G -->
           (∀lT. (x, h, l) ::<= (G, lT) -->
                 (G, lT) |- c [ok] --> h <=| h' ∧ (x', h', l') ::<= (G, lT)))

lemma eval_type_sound:

      [| wf_java_prog G; G |- (x, s) -e>v-> (x', s'); (x, s) ::<= E; E |- e :: T;
         G = fst E |]
      ==> (x', s') ::<= E ∧ (x' = None --> G,fst s' |- v ::<= T) ∧ fst s <=| fst s'

lemma evals_type_sound:

      [| wf_java_prog G; G |- (x, s) -es[>]vs-> (x', s'); (x, s) ::<= E;
         E |- es [::] Ts; G = fst E |]
      ==> (x', s') ::<= E ∧
          (x' = None --> list_all2 (conf G (fst s')) vs Ts) ∧ fst s <=| fst s'

lemma exec_type_sound:

      [| wf_java_prog G; G |- (x, s) -s0.0-> (x', s'); (x, s) ::<= E; E |- s0.0 [ok];
         G = fst E |]
      ==> (x', s') ::<= E ∧ fst s <=| fst s'

theorem all_methods_understood:

      [| G = fst E; wf_java_prog G; G |- (x, s) -e>a'-> Norm s'; a' ≠ Null;
         (x, s) ::<= E; E |- e :: Class C; method (G, C) sig ≠ None |]
      ==> method (G, fst (the (fst s' (the_Addr a')))) sig ≠ None