(* Title: HOL/MicroJava/J/JTypeSafe.ML
ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
Type safety proof
*)
Addsimps [split_beta];
Goal "[|h a = None; (h, l)::\\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==> \
\ (h(a\\<mapsto>(C,(init_vars (fields (G,C))))), l)::\\<preceq>(G, lT)";
by( etac conforms_upd_obj 1);
by( rewtac oconf_def);
by( auto_tac (claset() addSDs [fields_is_type], simpset()));
qed "NewC_conforms";
Goalw [cast_ok_def]
"[| wf_prog wf_mb G; G,h\\<turnstile>v::\\<preceq>Class C; G\\<turnstile>C\\<preceq>? D; cast_ok G D h v|] \
\ ==> G,h\\<turnstile>v::\\<preceq>Class D";
by( case_tac "v = Null" 1);
by( Asm_full_simp_tac 1);
by( dtac widen_RefT 1);
by( Clarify_tac 1);
by( datac non_npD 1 1);
by( auto_tac (claset() addSIs [conf_AddrI], simpset() addsimps [obj_ty_def]));
qed "Cast_conf";
Goal "[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (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";
by( dtac np_NoneD 1);
by( etac conjE 1);
by( mp_tac 1);
by( dtac non_np_objD 1);
by Auto_tac;
by( dtac (conforms_heapD RS hconfD) 1);
by( atac 1);
by( datac widen_cfs_fields 2 1);
by( datac oconf_objD 1 1);
by Auto_tac;
qed "FAcc_type_sound";
Goal
"[| 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''\\<le>|h'; \
\ x' = None --> G,h'\\<turnstile>a'::\\<preceq> Class C; h'\\<le>|h; \
\ (h, l)::\\<preceq>(G, lT); G,h\\<turnstile>x::\\<preceq>T'; np a' x' = None|] ==> \
\ h''\\<le>|h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))) \\<and> \
\ (h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))), l)::\\<preceq>(G, lT) \\<and> \
\ G,h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x))))\\<turnstile>x::\\<preceq>T'";
by( dtac np_NoneD 1);
by( etac conjE 1);
by( Asm_full_simp_tac 1);
by( dtac non_np_objD 1);
by( atac 1);
by( SELECT_GOAL Auto_tac 1);
by( Clarify_tac 1);
by( Full_simp_tac 1);
by( EVERY [ftac hext_objD 1, atac 1]);
by( etac exE 1);
by( Asm_full_simp_tac 1);
by( Clarify_tac 1);
by( rtac conjI 1);
by( fast_tac (HOL_cs addEs [hext_trans, hext_upd_obj]) 1);
by( rtac conjI 1);
by( fast_tac (HOL_cs addEs [conf_upd_obj RS iffD2]) 2);
by( rtac conforms_upd_obj 1);
by Auto_tac;
by( rtac hextI 2);
by( Force_tac 2);
by( rtac oconf_hext 1);
by( etac hext_upd_obj 2);
by( dtac widen_cfs_fields 1);
by( atac 1);
by( atac 1);
by( rtac (oconf_obj RS iffD2) 1);
by( Simp_tac 1);
by( strip_tac 1);
by( case_tac "(aaa, b) = (fn, fd)" 1);
by( Asm_full_simp_tac 1);
by( fast_tac (HOL_cs addIs [conf_widen]) 1);
by( fast_tac (HOL_cs addDs [conforms_heapD RS hconfD, oconf_objD]) 1);
qed "FAss_type_sound";
Goalw [wf_mhead_def] "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs; \
\ list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT; \
\ length pTs' = length pns; nodups pns; \
\ Ball (set lvars) (split (\\<lambda>vn. is_type G)) \
\ |] ==> G,h\\<turnstile>init_vars lvars(pns[\\<mapsto>]pvs)[::\\<preceq>]map_of lvars(pns[\\<mapsto>]pTs')";
by( Clarsimp_tac 1);
by( rtac lconf_ext_list 1);
by( rtac (Ball_set_table RS lconf_init_vars) 1);
by( Force_tac 1);
by( atac 1);
by( atac 1);
by( (etac conf_list_gext_widen THEN_ALL_NEW atac) 1);
qed "Call_lemma2";
Goalw [wf_java_prog_def]
"[| wf_java_prog G; a' \\<noteq> Null; (h, l)::\\<preceq>(G, lT); class G C = Some y; \
\ max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\\<le>|xh; xh\\<le>|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'));\
\ \\<forall>lT. (h, init_vars lvars(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))::\\<preceq>(G, lT) --> \
\ (G, lT)\\<turnstile>blk\\<surd> --> h\\<le>|xi \\<and> (xi, xl)::\\<preceq>(G, lT); \
\ \\<forall>lT. (xi, xl)::\\<preceq>(G, lT) --> (\\<forall>T. (G, lT)\\<turnstile>res::T --> \
\ xi\\<le>|h' \\<and> (h', xj)::\\<preceq>(G, lT) \\<and> (x' = None --> G,h'\\<turnstile>v::\\<preceq>T)); \
\ G,xh\\<turnstile>a'::\\<preceq> Class C |] ==> \
\ xc\\<le>|h' \\<and> (h', l)::\\<preceq>(G, lT) \\<and> (x' = None --> G,h'\\<turnstile>v::\\<preceq>rTa)";
by( dtac max_spec2mheads 1);
by( Clarify_tac 1);
by( datac non_np_objD' 2 1);
by( Clarsimp_tac 1);
by( Clarsimp_tac 1);
by( EVERY'[ftac hext_objD, atac] 1);
by( Clarsimp_tac 1);
by( datac Call_lemma 3 1);
by( clarsimp_tac (claset(),simpset() addsimps [wf_java_mdecl_def])1);
by( thin_tac "method ?sig ?x = ?y" 1);
by( EVERY'[dtac spec, etac impE] 1);
by( mp_tac 2);
by( rtac conformsI 1);
by( etac conforms_heapD 1);
by( rtac lconf_ext 1);
by( force_tac (claset() addSEs [Call_lemma2],simpset()) 1);
by( EVERY'[etac conf_hext, etac conf_obj_AddrI, atac] 1);
by( thin_tac "?E\\<turnstile>?blk\\<surd>" 1);
by( etac conjE 1);
by( EVERY'[dtac spec, mp_tac] 1);
(*by( thin_tac "?E::\\<preceq>(G, pT')" 1);*)
by( EVERY'[dtac spec, mp_tac] 1);
by( thin_tac "?E\\<turnstile>res::?rT" 1);
by( Clarify_tac 1);
by( rtac conjI 1);
by( fast_tac (HOL_cs addIs [hext_trans]) 1);
by( rtac conjI 1);
by( rtac impI 2);
by( mp_tac 2);
by( forward_tac [conf_widen] 2);
by( atac 4);
by( atac 2);
by( fast_tac (HOL_cs addSEs [widen_trans]) 2);
by( etac conforms_hext 1);
by( etac hext_trans 1);
by( atac 1);
by( etac conforms_heapD 1);
qed "Call_type_sound";
Unify.search_bound := 40;
Unify.trace_bound := 40;
Delsplits[split_if];
Delsimps[fun_upd_apply];
Addsimps[fun_upd_same];
val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]));
Goal
"wf_java_prog G ==> \
\ (G\\<turnstile>(x,(h,l)) -e \\<succ>v -> (x', (h',l')) --> \
\ (\\<forall>lT. (h ,l )::\\<preceq>(G,lT) --> (\\<forall>T . (G,lT)\\<turnstile>e :: T --> \
\ h\\<le>|h' \\<and> (h',l')::\\<preceq>(G,lT) \\<and> (x'=None --> G,h'\\<turnstile>v ::\\<preceq> T )))) \\<and> \
\ (G\\<turnstile>(x,(h,l)) -es[\\<succ>]vs-> (x', (h',l')) --> \
\ (\\<forall>lT. (h ,l )::\\<preceq>(G,lT) --> (\\<forall>Ts. (G,lT)\\<turnstile>es[::]Ts --> \
\ h\\<le>|h' \\<and> (h',l')::\\<preceq>(G,lT) \\<and> (x'=None --> list_all2 (\\<lambda>v T. G,h'\\<turnstile>v::\\<preceq>T) vs Ts)))) \\<and> \
\ (G\\<turnstile>(x,(h,l)) -c -> (x', (h',l')) --> \
\ (\\<forall>lT. (h ,l )::\\<preceq>(G,lT) --> (G,lT)\\<turnstile>c \\<surd> --> \
\ h\\<le>|h' \\<and> (h',l')::\\<preceq>(G,lT)))";
by( rtac eval_evals_exec.induct 1);
by( rewtac c_hupd_def);
(* several simplifications, XcptE, XcptEs, XcptS, Skip, Nil?? *)
by( ALLGOALS Asm_full_simp_tac);
by( ALLGOALS strip_tac);
by( ALLGOALS (eresolve_tac ty_expr_ty_exprs_wt_stmt.elims
THEN_ALL_NEW Full_simp_tac));
by( ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac]));
by( rewtac wf_java_prog_def);
(* Level 7 *)
(* 15 NewC *)
by( dtac new_AddrD 1);
by( etac disjE 1);
by( Asm_simp_tac 2);
by( Clarsimp_tac 1);
by( rtac conjI 1);
by( force_tac (claset() addSEs [NewC_conforms],simpset()) 1);
by( rtac conf_obj_AddrI 1);
by( rtac rtrancl_refl 2);
by( Simp_tac 1);
(* for Cast *)
by( defer_tac 1);
(* 14 Lit *)
by( etac conf_litval 1);
(* 13 BinOp *)
by forward_hyp_tac;
by forward_hyp_tac;
by( EVERY'[rtac conjI, eatac hext_trans 1] 1);
by( etac conjI 1);
by( Clarsimp_tac 1);
by( dtac eval_no_xcpt 1);
by( asm_full_simp_tac (simpset() addsplits [binop.split]) 1);
(* 12 LAcc *)
by( fast_tac (claset() addEs [conforms_localD RS lconfD]) 1);
(* for FAss *)
by( EVERY'[eresolve_tac ty_expr_ty_exprs_wt_stmt.elims THEN_ALL_NEW Full_simp_tac,
REPEAT o (etac conjE), hyp_subst_tac] 3);
(* for if *)
by( (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8);
by forward_hyp_tac;
(* 11+1 if *)
by( fast_tac (HOL_cs addIs [hext_trans]) 8);
by( fast_tac (HOL_cs addIs [hext_trans]) 8);
(* 10 Expr *)
by( Fast_tac 6);
(* 9 ??? *)
by( ALLGOALS Asm_full_simp_tac);
(* 8 Cast *)
by( EVERY'[rtac impI, dtac raise_if_NoneD, Clarsimp_tac,
fast_tac (claset() addEs [Cast_conf])] 8);
(* 7 LAss *)
by( asm_simp_tac (simpset() addsplits [split_if]) 1);
by( EVERY'[eresolve_tac ty_expr_ty_exprs_wt_stmt.elims THEN_ALL_NEW Full_simp_tac] 1);
by( blast_tac (claset() addIs [conforms_upd_local, conf_widen]) 1);
(* 6 FAcc *)
by( fast_tac (claset() addSEs [FAcc_type_sound]) 1);
(* 5 While *)
by(thin_tac "?a \\<longrightarrow> ?b" 5);
by(datac ty_expr_ty_exprs_wt_stmt.Loop 1 5);
by(force_tac (claset() addEs [hext_trans], simpset()) 5);
by forward_hyp_tac;
(* 4 Cons *)
by( fast_tac (claset() addDs [evals_no_xcpt] addIs [conf_hext,hext_trans]) 3);
(* 3 ;; *)
by( fast_tac (claset() addIs [hext_trans]) 3);
(* 2 FAss *)
by( case_tac "x2 = None" 1);
by( Asm_simp_tac 2);
by( fast_tac (claset() addIs [hext_trans]) 2);
by( Asm_full_simp_tac 1);
by( dtac eval_no_xcpt 1);
by( SELECT_GOAL (etac FAss_type_sound 1 THEN rtac refl 1 THEN ALLGOALS atac) 1);
by prune_params_tac;
(* Level 52 *)
(* 1 Call *)
by( case_tac "x" 1);
by( Clarsimp_tac 2);
by( dtac exec_xcpt 2);
by( Asm_full_simp_tac 2);
by( dtac eval_xcpt 2);
by( Asm_full_simp_tac 2);
by( fast_tac (HOL_cs addEs [hext_trans]) 2);
by( Clarify_tac 1);
by( dtac evals_no_xcpt 1);
by( Asm_full_simp_tac 1);
by( case_tac "a' = Null" 1);
by( Asm_full_simp_tac 1);
by( dtac exec_xcpt 1);
by( Asm_full_simp_tac 1);
by( dtac eval_xcpt 1);
by( Asm_full_simp_tac 1);
by( fast_tac (HOL_cs addEs [hext_trans]) 1);
by( datac ty_expr_is_type 1 1);
by(Clarsimp_tac 1);
by(rewtac is_class_def);
by(Clarsimp_tac 1);
by( (rtac (rewrite_rule [wf_java_prog_def] Call_type_sound)
THEN_ALL_NEW Asm_simp_tac) 1);
qed "eval_evals_exec_type_sound";
Goal "!!E s s'. \
\ [| G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>v -> (x',s'); s::\\<preceq>E; E\\<turnstile>e::T |] \
\ ==> s'::\\<preceq>E \\<and> (x'=None --> G,heap s'\\<turnstile>v::\\<preceq>T)";
by( split_all_tac 1);
bd (eval_evals_exec_type_sound RS conjunct1 RS mp RS spec RS mp) 1;
by Auto_tac;
qed "eval_type_sound";
Goal "!!E s s'. \
\ [| G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -s0-> (x',s'); s::\\<preceq>E; E\\<turnstile>s0\\<surd> |] \
\ ==> s'::\\<preceq>E";
by( split_all_tac 1);
bd (eval_evals_exec_type_sound RS conjunct2 RS conjunct2 RS mp RS spec RS mp) 1;
by Auto_tac;
qed "exec_type_sound";
Goal "[|G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>a'-> Norm s'; a' \\<noteq> Null;\
\ s::\\<preceq>E; E\\<turnstile>e::Class C; method (G,C) sig \\<noteq> None|] ==> \
\ method (G,fst (the (heap s' (the_Addr a')))) sig \\<noteq> None";
by( datac eval_type_sound 4 1);
by(Clarsimp_tac 1);
by(rewtac wf_java_prog_def);
by( forward_tac [widen_methd] 1);
by( atac 1);
by( Fast_tac 2);
by( dtac non_npD 1);
by Auto_tac;
qed "all_methods_understood";
Delsimps [split_beta];
Addsimps[fun_upd_apply];