# HG changeset patch # User nipkow # Date 943527688 -3600 # Node ID 1eaae1a2f8ff5c07712d1c393323e2733d0127ad # Parent 826c6222cca2fa475b9df4728ba7795ab9860947 Minor mods. diff -r 826c6222cca2 -r 1eaae1a2f8ff src/HOL/MicroJava/BV/BVSpec.ML --- a/src/HOL/MicroJava/BV/BVSpec.ML Wed Nov 24 13:36:14 1999 +0100 +++ b/src/HOL/MicroJava/BV/BVSpec.ML Thu Nov 25 12:01:28 1999 +0100 @@ -4,8 +4,6 @@ Copyright 1999 Technische Universitaet Muenchen *) -Addsimps [wt_MR_def]; - Goalw [wt_jvm_prog_def] "wt_jvm_prog G phi \\ (\\wt. wf_prog wt G)"; by(Blast_tac 1); qed "wt_jvm_progD"; diff -r 826c6222cca2 -r 1eaae1a2f8ff src/HOL/MicroJava/BV/BVSpec.thy --- a/src/HOL/MicroJava/BV/BVSpec.thy Wed Nov 24 13:36:14 1999 +0100 +++ b/src/HOL/MicroJava/BV/BVSpec.thy Thu Nov 25 12:01:28 1999 +0100 @@ -148,7 +148,7 @@ consts wt_MI :: "[meth_inv,jvm_prog,method_type,p_count,p_count] \\ bool" primrec -"wt_MI (Invokevirtual mn fpTs) G phi max_pc pc = +"wt_MI (Invoke mn fpTs) G phi max_pc pc = (let (ST,LT) = phi ! pc in pc+1 < max_pc \\ @@ -158,9 +158,10 @@ (\\D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\ G \\ (rT # ST' , LT) <=s phi ! (pc+1))))" -constdefs - wt_MR :: "[jvm_prog,ty,method_type,p_count] \\ bool" -"wt_MR G rT phi pc \\ +consts + wt_MR :: "[meth_ret,jvm_prog,ty,method_type,p_count] \\ bool" +primrec + "wt_MR Return G rT phi pc = (let (ST,LT) = phi ! pc in (\\T ST'. ST = T # ST' \\ G \\ T \\ rT))" @@ -175,7 +176,7 @@ | MO ins \\ wt_MO ins G phi max_pc pc | CH ins \\ wt_CH ins G phi max_pc pc | MI ins \\ wt_MI ins G phi max_pc pc - | MR \\ wt_MR G rT phi pc + | MR ins \\ wt_MR ins G rT phi pc | OS ins \\ wt_OS ins G phi max_pc pc | BR ins \\ wt_BR ins G phi max_pc pc" diff -r 826c6222cca2 -r 1eaae1a2f8ff src/HOL/MicroJava/BV/BVSpecTypeSafe.ML --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Wed Nov 24 13:36:14 1999 +0100 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Thu Nov 25 12:01:28 1999 +0100 @@ -10,7 +10,7 @@ Goalw [correct_state_def,Let_def,correct_frame_def,split_def] "\\ wt_jvm_prog G phi; \ \ cmethd (G,C) sig = Some (C,rT,maxl,ins); \ -\ correct_state G phi (None, hp, (stk,loc,C,sig,pc)#frs) \\ \ +\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ \\\ 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); @@ -28,8 +28,8 @@ \ ins!pc = LS(Load idx); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; 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 [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1); @@ -42,8 +42,8 @@ \ ins!pc = LS(Store idx); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by (fast_tac (claset() addDs [approx_stk_Cons_lemma] addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_subst RSN(2, approx_loc_imp_approx_loc_sup)] addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons]@defs1)) 1); @@ -60,8 +60,8 @@ \ ins!pc = LS(Bipush i); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; 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,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1); qed "Bipush_correct"; @@ -84,8 +84,8 @@ \ ins!pc = LS Aconst_null; \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; 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,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1); qed "Aconst_null_correct"; @@ -96,8 +96,8 @@ \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = LS ls_com; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); ba 1; ba 1; @@ -131,8 +131,8 @@ \ ins!pc = CH (Checkcast D); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by (asm_full_simp_tac (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons, xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1); by (fast_tac (claset() addDs [approx_stk_Cons_lemma] @@ -146,8 +146,8 @@ \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = CH ch_com; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); ba 1; ba 1; @@ -164,8 +164,8 @@ \ ins!pc = MO (Getfield F D); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1); by (Clarify_tac 1); by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1); @@ -203,8 +203,8 @@ \ ins!pc = MO (Putfield F D); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1); by (Clarify_tac 1); by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1); @@ -231,8 +231,8 @@ \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = MO mo_com; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); ba 1; ba 1; @@ -250,12 +250,12 @@ Goal "\\ wf_prog wt G; \ -\ cmethd (G,C) sig = Some (C,rT,maxl,ins); \ +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = CO(New cl_idx); \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ correct_state G phi (None, hp, (stk,loc,C,sig,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; 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), @@ -271,8 +271,8 @@ \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = CO co_com; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); ba 1; ba 1; @@ -287,11 +287,11 @@ Goal "\\ wt_jvm_prog G phi; \ \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ -\ ins ! pc = MI(Invokevirtual mn pTs); \ +\ ins ! pc = MI(Invoke mn pTs); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by(forward_tac [wt_jvm_progD] 1); by(etac exE 1); by (asm_full_simp_tac (simpset()addsimps[xcpt_update_def,raise_xcpt_def]@defs1 @@ -361,20 +361,20 @@ by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset()addsimps [map_eq_Cons,sup_loc_Cons])) 1); -qed "Invokevirtual_correct"; +qed "Invoke_correct"; Goal "\\ wt_jvm_prog G phi; \ \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = MI mi_com; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); ba 1; ba 1; by (exhaust_tac "mi_com" 1); -by (ALLGOALS (fast_tac (claset() addIs [Invokevirtual_correct]))); +by (ALLGOALS (fast_tac (claset() addIs [Invoke_correct]))); qed "MI_correct"; (****** MR ******) @@ -395,11 +395,11 @@ Goal "\\ wt_jvm_prog G phi; \ \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ -\ ins ! pc = MR; \ +\ ins ! pc = MR Return; \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by (asm_full_simp_tac (simpset() addsimps defs1) 1); by (Clarify_tac 1); by (asm_full_simp_tac (simpset() addsimps defs1) 1); @@ -424,13 +424,14 @@ Goal "\\ wt_jvm_prog G phi; \ \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ -\ ins!pc = MR; \ +\ ins!pc = MR mr; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); ba 1; ba 1; +by (exhaust_tac "mr" 1); by (ALLGOALS (fast_tac (claset() addIs [Return_correct]))); qed "MR_correct"; @@ -441,8 +442,8 @@ \ ins ! pc = BR(Goto branch); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup,approx_stk_imp_approx_stk_sup] addss (simpset() addsimps defs1)) 1); qed "Goto_correct"; @@ -454,8 +455,8 @@ \ ins!pc = BR(Ifcmpeq branch); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by (fast_tac (claset() addDs [approx_stk_Cons_lemma] addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1); qed "Ifiacmpeq_correct"; @@ -466,8 +467,8 @@ \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = BR br_com; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); ba 1; ba 1; @@ -485,8 +486,8 @@ \ ins ! pc = OS Pop; \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by (fast_tac (claset() addDs [approx_stk_Cons_lemma] addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1); qed "Pop_correct"; @@ -498,8 +499,8 @@ \ ins ! pc = OS Dup; \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by (fast_tac (claset() addDs [approx_stk_Cons_lemma] addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1); @@ -512,8 +513,8 @@ \ ins ! pc = OS Dup_x1; \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by (fast_tac (claset() addDs [approx_stk_Cons_lemma] addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1); @@ -525,8 +526,8 @@ \ ins ! pc = OS Dup_x2; \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by (fast_tac (claset() addDs [approx_stk_Cons_lemma] addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1); @@ -538,8 +539,8 @@ \ ins ! pc = OS Swap; \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by (fast_tac (claset() addDs [approx_stk_Cons_lemma] addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1); @@ -550,8 +551,8 @@ \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = OS os_com; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\ \ -\\\ correct_state G phi (xp',hp',frs')"; +\ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM (xp',hp',frs')\\"; by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); ba 1; ba 1; @@ -563,15 +564,15 @@ (** Main **) Goalw [correct_state_def,Let_def] - "correct_state G phi (None,hp,(stk,loc,C,sig,pc)#fs) \ -\ \\ \\meth. cmethd (G,C) sig = Some(C,meth)"; + "G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \ +\ \\ \\meth. cmethd (G,C) ml = Some(C,meth)"; by(Asm_full_simp_tac 1); by(Blast_tac 1); qed "correct_state_impl_Some_cmethd"; Goal -"\\state. \\ wt_jvm_prog G phi; correct_state G phi state\\ \ -\ \\ exec (G,state) = Some state' \\ correct_state G phi state'"; +"\\state. \\ wt_jvm_prog G phi; G,phi \\JVM state\\\\ \ +\ \\ exec (G,state) = Some state' \\ G,phi \\JVM state'\\"; by(split_all_tac 1); by(rename_tac "xp hp frs" 1); by (exhaust_tac "xp" 1); @@ -596,9 +597,8 @@ qed_spec_mp "exec_lemma"; Goal -"\\ wt_jvm_prog G phi; \ -\ correct_state G phi (xp,hp,frs); xp=None; frs\\[] \\ \ -\ \\ \\xp' hp' frs'. exec (G,xp,hp,frs) = Some (xp',hp',frs') \\ correct_state G phi (xp',hp',frs')"; +"\\ wt_jvm_prog G phi; G,phi \\JVM (xp,hp,frs)\\; xp=None; frs\\[] \\ \ +\ \\ \\xp' hp' frs'. exec(G,xp,hp,frs) = Some(xp',hp',frs') \\ G,phi \\JVM (xp',hp',frs')\\"; by (dres_inst_tac [("G","G"),("hp","hp")] exec_lemma 1); ba 1; by (fast_tac (claset() addIs [BV_correct_1]) 1); @@ -606,8 +606,7 @@ (*******) Goalw [exec_all_def] -"\\ wt_jvm_prog G phi; G \\ s -jvm\\ t \\ \ -\ \\ correct_state G phi s \\ correct_state G phi t"; +"\\ wt_jvm_prog G phi; G \\ s -jvm\\ t \\ \\ G,phi \\JVM s\\ \\ G,phi \\JVM t\\"; be rtrancl_induct 1; by (Simp_tac 1); by (fast_tac (claset() addIs [BV_correct_1] addss (simpset())) 1); @@ -615,7 +614,7 @@ Goal -"\\ wt_jvm_prog G phi; G \\ s0 -jvm\\ (None,hp,(stk,loc,cn,ml,pc)#frs); correct_state G phi s0 \\ \ +"\\ wt_jvm_prog G phi; G \\ s0 -jvm\\ (None,hp,(stk,loc,cn,ml,pc)#frs); G,phi \\JVM s0 \\\\ \ \ \\ approx_stk G hp stk (fst (((phi cn) ml) ! pc)) \\ approx_loc G hp loc (snd (((phi cn) ml) ! pc)) "; bd BV_correct 1; ba 1; diff -r 826c6222cca2 -r 1eaae1a2f8ff src/HOL/MicroJava/BV/Correct.ML --- a/src/HOL/MicroJava/BV/Correct.ML Wed Nov 24 13:36:14 1999 +0100 +++ b/src/HOL/MicroJava/BV/Correct.ML Thu Nov 25 12:01:28 1999 +0100 @@ -233,7 +233,7 @@ (** hconf **) -Goal "hp x = None \\ G,hp\\\\ \\ G,hp\\obj\\ \\ G,hp(newref hp\\obj)\\\\"; +Goal "hp x = None \\ G\\h hp\\ \\ G,hp\\obj\\ \\ G\\h hp(newref hp\\obj)\\"; by (asm_full_simp_tac (simpset() addsplits [split_split] addsimps [hconf_def]) 1); by (fast_tac (claset()addIs[oconf_imp_oconf_heap_newref] addss (simpset())) 1); @@ -241,7 +241,7 @@ Goal "map_of (fields (G, oT)) (F, D) = Some T \\ hp oloc = Some(oT,fs) \\ \ -\ G,hp\\v\\\\T \\ G,hp\\\\ \\ G,hp(oloc \\ (oT, fs((F,D)\\v)))\\\\"; +\ G,hp\\v\\\\T \\ G\\h hp\\ \\ G\\h hp(oloc \\ (oT, fs((F,D)\\v)))\\"; by (asm_full_simp_tac (simpset() addsimps [hconf_def]) 1); by (fast_tac (claset() addIs [oconf_imp_oconf_heap_update, oconf_imp_oconf_field_update] diff -r 826c6222cca2 -r 1eaae1a2f8ff src/HOL/MicroJava/BV/Correct.thy --- a/src/HOL/MicroJava/BV/Correct.thy Wed Nov 24 13:36:14 1999 +0100 +++ b/src/HOL/MicroJava/BV/Correct.thy Thu Nov 25 12:01:28 1999 +0100 @@ -35,7 +35,7 @@ in (\\rT maxl ins. cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\ - (\\mn pTs k. pc = k+1 \\ ins!k = MI(Invokevirtual mn pTs) \\ + (\\mn pTs k. pc = k+1 \\ ins!k = MI(Invoke mn pTs) \\ (mn,pTs) = ml0 \\ (\\apTs D ST'. fst((phi C ml)!k) = (rev apTs) @ (Class D) # ST' \\ @@ -49,6 +49,7 @@ constdefs correct_state :: "[jvm_prog,prog_type,jvm_state] \\ bool" + ("_,_\\JVM _\\" [51,51] 50) "correct_state G phi \\ \\(xp,hp,frs). case xp of None \\ (case frs of @@ -57,7 +58,7 @@ in \\rT maxl ins. cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\ - G,hp\\\\ \\ + G\\h hp\\ \\ correct_frame G hp ((phi C ml) ! pc) maxl ins f \\ correct_frames G hp phi rT C ml fs)) | Some x \\ True" diff -r 826c6222cca2 -r 1eaae1a2f8ff src/HOL/MicroJava/J/Conform.ML --- a/src/HOL/MicroJava/J/Conform.ML Wed Nov 24 13:36:14 1999 +0100 +++ b/src/HOL/MicroJava/J/Conform.ML Thu Nov 25 12:01:28 1999 +0100 @@ -210,11 +210,11 @@ section "hconf"; -Goalw [hconf_def] "\\G,h\\\\; h a = Some obj\\ \\ G,h\\obj\\"; +Goalw [hconf_def] "\\G\\h h\\; h a = Some obj\\ \\ G,h\\obj\\"; by (Fast_tac 1); qed "hconfD"; -Goalw [hconf_def] "\\a obj. h a=Some obj \\ G,h\\obj\\ \\ G,h\\\\"; +Goalw [hconf_def] "\\a obj. h a=Some obj \\ G,h\\obj\\ \\ G\\h h\\"; by (Fast_tac 1); qed "hconfI"; @@ -222,7 +222,7 @@ section "conforms"; val conforms_heapD = prove_goalw thy [conforms_def] - "(h, l)\\\\(G, lT) \\ G,h\\\\" + "(h, l)\\