--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Mon Aug 07 10:29:54 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Mon Aug 07 14:32:56 2000 +0200
@@ -5,7 +5,7 @@
*)
val defs1 = exec.simps@[split_def,sup_state_def,correct_state_def,
- correct_frame_def];
+ correct_frame_def, thm "wt_instr_def"];
Goalw [correct_state_def,Let_def,correct_frame_def,split_def]
"\\<lbrakk> wt_jvm_prog G phi; \
@@ -13,15 +13,16 @@
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
\\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
by (Asm_full_simp_tac 1);
-by(blast_tac (claset() addIs [wt_jvm_prog_impl_wt_instr]) 1);
+by(blast_tac (claset() addIs [thm "wt_jvm_prog_impl_wt_instr"]) 1);
qed "wt_jvm_prog_impl_wt_instr_cor";
-Delsimps [split_paired_All];
+Delsimps [split_paired_All];
(******* LS *******)
+
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
@@ -30,11 +31,13 @@
\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); \
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
+by (case_tac "phi C sig!pc" 1);
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_val_sup,
approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [map_eq_Cons]@defs1)) 1);
qed "Load_correct";
+
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
@@ -47,6 +50,7 @@
addss (simpset() addsimps [map_eq_Cons]@defs1)) 1);
qed "Store_correct";
+
Goalw [conf_def] "G,h \\<turnstile> Intg i \\<Colon>\\<preceq> PrimT Integer";
by(Simp_tac 1);
qed "conf_Intg_Integer";
@@ -60,6 +64,7 @@
\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
+by (case_tac "phi C sig ! pc" 1);
by (fast_tac (claset()addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_val_def,sup_PTS_eq,map_eq_Cons]@defs1)) 1);
qed "Bipush_correct";
@@ -84,12 +89,12 @@
\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
+by (case_tac "phi C sig ! pc" 1);
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_val_Null,NT_subtype_conv,map_eq_Cons]@defs1)) 1);
qed "Aconst_null_correct";
-
Goalw [cast_ok_def]
"\\<lbrakk> wf_prog ok G; G,h\\<turnstile>v\\<Colon>\\<preceq>RefT rt; cast_ok G C h v ; G\\<turnstile>Class C\\<preceq>T; is_class G C \\<rbrakk> \
\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T";
@@ -118,7 +123,6 @@
addss (simpset() addsimps [map_eq_Cons,approx_val_def])) 1);
qed "Checkcast_correct";
-
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
@@ -138,16 +142,16 @@
ba 1;
bd conf_RefTD 1;
by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (asm_full_simp_tac (simpset() addsimps []) 1);
br conjI 1;
bd widen_cfs_fields 1;
ba 1;
ba 1;
- by(fast_tac (claset() addIs [conf_widen] addss (simpset() addsimps [hconf_def,oconf_def,lconf_def])) 1);
+ by (fast_tac (claset() addIs [conf_widen] addss (simpset() addsimps [hconf_def,oconf_def,lconf_def])) 1);
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]) 1);
+qed "Getfield_correct";
-qed "Getfield_correct";
Goal
@@ -174,7 +178,6 @@
correct_frames_imp_correct_frames_field_update,conf_widen] addss (simpset())) 1);
qed "Putfield_correct";
-
Goal "(\\<forall>x y. P(x,y)) = (\\<forall>z. P z)";
by(Fast_tac 1);
qed "collapse_paired_All";
@@ -187,6 +190,7 @@
\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
+by (case_tac "phi C sig ! pc" 1);
by (fast_tac (claset() addSDs [collapse_paired_All RS iffD1]addIs [sup_heap_newref,
approx_stk_imp_approx_stk_sup_heap RSN(2,approx_stk_imp_approx_stk_sup),
approx_loc_imp_approx_loc_sup_heap RSN(2,approx_loc_imp_approx_loc_sup),
@@ -198,88 +202,105 @@
qed "New_correct";
+
+Delsimps (thms "app.simps");
+
(****** Method Invocation ******)
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins ! pc = Invoke mn pTs; \
+\ ins ! pc = Invoke C' mn pTs; \
\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by(forward_tac [wt_jvm_progD] 1);
+by(case_tac "phi C sig ! pc" 1);
+by(forward_tac [thm "wt_jvm_progD"] 1);
by(etac exE 1);
by(asm_full_simp_tac (simpset() addsimps defs1) 1);
by(Clarify_tac 1);
-by(case_tac "X\\<noteq>NT" 1);
- by (asm_full_simp_tac (simpset()addsimps[raise_xcpt_def]@defs1
- addsplits [option.split]) 1);
- by (Clarify_tac 1);
- by (asm_full_simp_tac (simpset() addsimps defs1) 1);
- bd approx_stk_append_lemma 1;
- by (Clarify_tac 1);
- by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
- bd conf_RefTD 1;
- by (Clarify_tac 1);
- by(rename_tac "oloc oT ofs T'" 1);
- by (asm_full_simp_tac (simpset() addsimps defs1) 1);
- bd subtype_widen_methd 1;
- ba 1;
+by(asm_full_simp_tac (simpset() addsimps [raise_xcpt_def] addsplits [option.split]) 1);
+by(Clarify_tac 1);
+bd approx_stk_append_lemma 1;
+by(clarsimp_tac (claset(), simpset() addsimps [approx_val_def]) 1);
+
+by (subgoal_tac "\\<exists> D'. X = Class D'" 1);
+ bd widen_RefT2 2;
+ by (Clarsimp_tac 2);
+ bd conf_RefTD 2;
+ by (Clarsimp_tac 2);
+ bd widen_Class 2;
+ by (Clarsimp_tac 2);
+
+by (Clarsimp_tac 1);
+bd conf_RefTD 1;
+by (Clarify_tac 1);
+by(rename_tac "oloc oT ofs T'" 1);
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
+by (subgoal_tac "G\\<turnstile>oT\\<preceq>C C'" 1);
+ bd widen.subcls 2;
+ bd widen.subcls 2;
+ by (((dtac widen_trans) THEN' atac THEN' Blast_tac) 2);
+bd subtype_widen_methd 1;
ba 1;
- be exE 1;
- by(rename_tac "oT'" 1);
- by (Clarify_tac 1);
- by(subgoal_tac "G \\<turnstile> oT \\<preceq>C oT'" 1);
- by(forw_inst_tac [("C","oT")](standard(rotate_prems 1 method_wf_mdecl)) 2);
- ba 2;
- by(Blast_tac 2);
- by (asm_full_simp_tac (simpset() addsimps defs1) 1);
- by(forward_tac [method_in_md] 1);
+ ba 1;
+by (Clarify_tac 1);
+bd subtype_widen_methd 1;
ba 1;
- back();
- back();
- by (Clarify_tac 1);
- by (asm_full_simp_tac (simpset() addsimps defs1) 1);
- by (forward_tac [wt_jvm_prog_impl_wt_start] 1);
- ba 1;
- back();
- by (asm_full_simp_tac (simpset() addsimps [wt_start_def,sup_state_def]) 1);
- by (Clarify_tac 1);
+ ba 1;
+be exE 1;
+by(rename_tac "oT'" 1);
+by (Clarify_tac 1);
+by(subgoal_tac "G \\<turnstile> oT \\<preceq>C oT'" 1);
+ by(forw_inst_tac [("C","oT")] method_wf_mdecl 2);
+ ba 2;
+ by (Blast_tac 2);
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
+by(forward_tac [method_in_md] 1);
+ ba 1;
+ back();
+ back();
+ back();
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
+by (forward_tac [thm "wt_jvm_prog_impl_wt_start"] 1);
+ ba 1;
+ back();
+by (asm_full_simp_tac (simpset() addsimps [thm "wt_start_def",sup_state_def]) 1);
+by (Clarify_tac 1);
(** approx_loc **)
+br conjI 1;
+ br approx_loc_imp_approx_loc_sup 1;
+ ba 1;
+ by (Fast_tac 2);
+ by (asm_full_simp_tac (simpset() addsimps [split_def,approx_val_def,approx_loc_append]) 1);
br conjI 1;
- br approx_loc_imp_approx_loc_sup 1;
+ br conf_widen 1;
ba 1;
by (Fast_tac 2);
- by (asm_full_simp_tac (simpset() addsimps [split_def,approx_val_def,approx_loc_append]) 1);
- br conjI 1;
- br conf_widen 1;
- ba 1;
- by (Fast_tac 2);
- by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1);
- br conjI 1;
- by (fast_tac (claset() addIs [approx_stk_rev RS iffD2 RSN(4,assConv_approx_stk_imp_approx_loc)]
- addss (simpset() addsimps [split_def,approx_val_def])) 1);
- by (asm_simp_tac (simpset() addsimps [list_all2_def,split_def,approx_loc_def,approx_val_None,set_replicate_conv_if]) 1);
-
+ by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1);
br conjI 1;
- by (asm_simp_tac (simpset() addsimps [min_def]) 1);
- br exI 1;
- br exI 1;
- br conjI 1;
- by(Blast_tac 1);
- by (fast_tac (claset()
- addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
- addss (simpset()addsimps [map_eq_Cons])) 1);
-by (Asm_full_simp_tac 1);
-bd approx_stk_append_lemma 1;
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [approx_val_def, raise_xcpt_def]) 1);
-bd conf_NullTD 1;
-by (Asm_simp_tac 1);
+ by (fast_tac (claset() addIs [approx_stk_rev RS iffD2 RSN(4,assConv_approx_stk_imp_approx_loc)]
+ addss (simpset() addsimps [split_def,approx_val_def])) 1);
+ by (asm_simp_tac (simpset() addsimps [list_all2_def,split_def,approx_loc_def,approx_val_None,set_replicate_conv_if]) 1);
+
+br conjI 1;
+ by (asm_simp_tac (simpset() addsimps [min_def]) 1);
+br exI 1;
+br exI 1;
+br conjI 1;
+ by(Blast_tac 1);
+by (Clarsimp_tac 1);
+
+by (fast_tac (claset()
+ addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
+ addss (simpset()addsimps [map_eq_Cons])) 1);
qed "Invoke_correct";
+Addsimps (thms "app.simps");
+
Delsimps [map_append];
Goal
@@ -295,9 +316,10 @@
by (asm_full_simp_tac (simpset() addsimps [map_eq_Cons]@defs1) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps defs1) 1);
-by (forward_tac [wt_jvm_prog_impl_wt_instr] 1);
+by (forward_tac [thm "wt_jvm_prog_impl_wt_instr"] 1);
by(EVERY1[atac, etac Suc_lessD]);
-by(rewtac wt_jvm_prog_def);
+by(rewtac (thm "wt_jvm_prog_def"));
+by (case_tac "phi ab (ac, b) ! k" 1);
by (fast_tac (claset()
addDs [subcls_widen_methd]
addEs [rotate_prems 1 widen_trans]
@@ -307,6 +329,7 @@
Addsimps [map_append];
+
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
@@ -329,7 +352,7 @@
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
-qed "Ifiacmpeq_correct";
+qed "Ifcmpeq_correct";
Goal
@@ -357,6 +380,7 @@
qed "Dup_correct";
+
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
@@ -407,6 +431,7 @@
qed "IAdd_correct";
+
(** instr correct **)
Goal
@@ -421,11 +446,11 @@
by(case_tac "ins!pc" 1);
by(fast_tac (claset() addIs [Invoke_correct]) 9);
by(fast_tac (claset() addIs [Return_correct]) 9);
-by(rewtac wt_jvm_prog_def);
+by(rewtac (thm "wt_jvm_prog_def"));
by (ALLGOALS (fast_tac (claset() addIs
[Load_correct,Store_correct,Bipush_correct,Aconst_null_correct,
Checkcast_correct,Getfield_correct,Putfield_correct,New_correct,
- Goto_correct,Ifiacmpeq_correct,Pop_correct,Dup_correct,
+ Goto_correct,Ifcmpeq_correct,Pop_correct,Dup_correct,
Dup_x1_correct,Dup_x2_correct,Swap_correct,IAdd_correct])));
qed "instr_correct";