src/HOL/MicroJava/J/JTypeSafe.ML

unsymbolized

(*  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 [is_type_fields, map_of_SomeD], 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_tac1 "v = Null" 1);
by(  Asm_full_simp_tac 1);
by(  dtac widen_RefT 1);
by(  Clarify_tac 1);
by(  rtac widen.null 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( dtac widen_cfs_fields 1);
by(   atac 1);
by(  atac 1);
by( dtac oconf_objD 1);
by(  atac 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( strip_tac1 1);
by( Full_simp_tac 1);
by( EVERY [forward_tac [hext_objD] 1, atac 1]);
by( etac exE 1);
by( Asm_full_simp_tac 1);
by( strip_tac1 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_tac1 "(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); \
\    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 (insertI1 RSN (2,(equalityD2 RS subsetD))) 1);
by( dtac (max_spec2appl_meths RS appl_methsD) 1);
by( Clarify_tac 1);
by( datac non_np_objD' 2 1);
by(  strip_tac1 1);
by(  Asm_full_simp_tac 1);
by( Clarsimp_tac 1);
by( EVERY'[forward_tac [hext_objD], atac] 1);
by( Clarsimp_tac 1);
by( EVERY'[dtac Call_lemma, atac, atac] 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( strip_tac1 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];(*###*)
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 *)
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 *)

(* 14 NewC *)
by( dtac new_AddrD 1);
by( etac disjE 1);
by(  Asm_simp_tac 2);
by( etac conjE 1);
by( Asm_simp_tac 1);
by( rtac conjI 1);
by(  fast_tac (HOL_cs addSEs [NewC_conforms]) 1);
by( rtac conf_obj_AddrI 1);
by(  rtac rtrancl_refl 2);
by( Simp_tac 1);

(* for Cast *)
by( defer_tac 1);

(* 13 Lit *)
by( etac conf_litval 1);

(* 12 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);

(* 11 LAcc *)
by( fast_tac (claset() addEs [conforms_localD RS lconfD]) 1);

(* 10 Nil *)
by( Simp_tac 5);

(* 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_tac1 "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8);

by forward_hyp_tac;

(* 10+1 if *)
by(  fast_tac (HOL_cs addIs [hext_trans]) 8);
by( fast_tac (HOL_cs addIs [hext_trans]) 8);

(* 9 Expr *)
by( Fast_tac 6);

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( fast_tac (claset() addIs [ty_expr_ty_exprs_wt_stmt.Cond, ty_expr_ty_exprs_wt_stmt.Comp, ty_expr_ty_exprs_wt_stmt.Skip]
		       addEs [ty_expr_ty_exprs_wt_stmt.Loop]) 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_tac1 "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 51 *)

(* 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_tac1 "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( (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( not_None_tac 1);
by( split_all_tac 1);
by(rewtac wf_java_prog_def);
by( forward_tac [widen_methd] 1);
by(   atac 1);
by(  rtac (not_None_eq RS iffD1) 2);
by(  Fast_tac 2);
by( etac conjE 1);
by( dtac non_npD 1);
by Auto_tac;
qed "all_methods_understood";

Delsimps [split_beta];
Addsimps[fun_upd_apply];(*###*)