--- a/src/HOL/MicroJava/J/JTypeSafe.ML Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,330 +0,0 @@
-(* 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];
-