Various little changes like cmethd -> method and cfield -> field.
--- a/src/HOL/MicroJava/BV/BVSpec.ML Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.ML Fri Nov 26 08:46:59 1999 +0100
@@ -11,19 +11,19 @@
Goalw [wt_jvm_prog_def]
"\\<lbrakk> wt_jvm_prog G phi; \
-\ cmethd (G,C) sig = Some (C,rT,maxl,ins); \
+\ method (G,C) sig = Some (C,rT,maxl,ins); \
\ pc < length ins \\<rbrakk> \
\\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
-by(forward_tac [rotate_prems 2 cmethd_wf_mdecl] 1);
+by(forward_tac [rotate_prems 2 method_wf_mdecl] 1);
by (Asm_full_simp_tac 1);
by(asm_full_simp_tac (simpset() addsimps [wf_mdecl_def,wt_method_def]) 1);
qed "wt_jvm_prog_impl_wt_instr";
Goalw [wt_jvm_prog_def]
"\\<lbrakk> wt_jvm_prog G phi; \
-\ cmethd (G,C) sig = Some (C,rT,maxl,ins) \\<rbrakk> \\<Longrightarrow> \
+\ method (G,C) sig = Some (C,rT,maxl,ins) \\<rbrakk> \\<Longrightarrow> \
\ 0 < (length ins) \\<and> wt_start G C (snd sig) maxl (phi C sig)";
-by(forward_tac [rotate_prems 2 cmethd_wf_mdecl] 1);
+by(forward_tac [rotate_prems 2 method_wf_mdecl] 1);
by (Asm_full_simp_tac 1);
by(asm_full_simp_tac (simpset() addsimps [wf_mdecl_def,wt_method_def]) 1);
qed "wt_jvm_prog_impl_wt_start";
--- a/src/HOL/MicroJava/BV/BVSpec.thy Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Fri Nov 26 08:46:59 1999 +0100
@@ -52,7 +52,7 @@
in
pc+1 < max_pc \\<and>
is_class G C \\<and>
- (\\<exists>T oT ST'. cfield (G,C) F = Some(C,T) \\<and>
+ (\\<exists>T oT ST'. field (G,C) F = Some(C,T) \\<and>
ST = oT # ST' \\<and>
G \\<turnstile> oT \\<preceq> (Class C) \\<and>
G \\<turnstile> (T # ST' , LT) <=s phi ! (pc+1)))"
@@ -63,7 +63,7 @@
pc+1 < max_pc \\<and>
is_class G C \\<and>
(\\<exists>T vT oT ST'.
- cfield (G,C) F = Some(C,T) \\<and>
+ field (G,C) F = Some(C,T) \\<and>
ST = vT # oT # ST' \\<and>
G \\<turnstile> oT \\<preceq> (Class C) \\<and>
G \\<turnstile> vT \\<preceq> T \\<and>
@@ -155,7 +155,7 @@
(\\<exists>apTs C ST'. ST = (rev apTs) @ (Class C # ST') \\<and>
length apTs = length fpTs \\<and>
(\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
- (\\<exists>D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
+ (\\<exists>D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
G \\<turnstile> (rT # ST' , LT) <=s phi ! (pc+1))))"
consts
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Fri Nov 26 08:46:59 1999 +0100
@@ -9,7 +9,7 @@
Goalw [correct_state_def,Let_def,correct_frame_def,split_def]
"\\<lbrakk> wt_jvm_prog G phi; \
-\ cmethd (G,C) sig = Some (C,rT,maxl,ins); \
+\ method (G,C) sig = Some (C,rT,maxl,ins); \
\ 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);
@@ -24,7 +24,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ 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); \
@@ -38,7 +38,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ 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) ; \
@@ -56,7 +56,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ 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) ; \
@@ -80,7 +80,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ 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) ; \
@@ -93,7 +93,7 @@
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (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) ; \
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
@@ -127,14 +127,14 @@
Goal
"\\<lbrakk> wf_prog wt G; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ 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); \
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
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);
+ raise_xcpt_def]@defs1 addsplits [option.split]) 1);
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup,Cast_conf2]
addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons,approx_val_def])) 1);
@@ -143,7 +143,7 @@
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (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) ; \
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
@@ -160,13 +160,13 @@
(******* MO *******)
Goal
"\\<lbrakk> wf_prog wt G; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ 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); \
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
-by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 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 [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
by (Clarify_tac 1);
@@ -199,13 +199,13 @@
Goal
"\\<lbrakk> wf_prog wt G; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ 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); \
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
-by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 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 [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
by (Clarify_tac 1);
@@ -228,7 +228,7 @@
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (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) ; \
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
@@ -250,7 +250,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ ins!pc = CO(New cl_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) ; \
@@ -262,13 +262,13 @@
hconf_imp_hconf_newref,correct_frames_imp_correct_frames_newref,
rewrite_rule [split_def] correct_init_obj]
addss (simpset() addsimps [NT_subtype_conv,approx_stk_Cons,approx_val_def,conf_def,
- fun_upd_apply,sup_loc_Cons,map_eq_Cons,is_class_def,xcpt_update_def,raise_xcpt_def,init_vars_def]@defs1
+ fun_upd_apply,sup_loc_Cons,map_eq_Cons,is_class_def,raise_xcpt_def,init_vars_def]@defs1
addsplits [option.split])) 1);
qed "New_correct";
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (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) ; \
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
@@ -286,7 +286,7 @@
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ 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) ; \
@@ -294,7 +294,7 @@
\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
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
+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);
@@ -315,11 +315,11 @@
by(rename_tac "oT'" 1);
by (Clarify_tac 1);
by(subgoal_tac "G \\<turnstile> Class oT \\<preceq> Class oT'" 1);
- by(forw_inst_tac [("C","oT")](standard(rotate_prems 1 cmethd_wf_mdecl)) 2);
+ 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 [cmethd_in_md] 1);
+by(forward_tac [method_in_md] 1);
ba 1;
back();
back();
@@ -365,7 +365,7 @@
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (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) ; \
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
@@ -394,7 +394,7 @@
Delsimps [map_append];
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ 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) ; \
@@ -423,7 +423,7 @@
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ ins!pc = MR mr; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
@@ -438,7 +438,7 @@
(****** BR ******)
Goal
"\\<lbrakk> wf_prog wt G; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ 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) ; \
@@ -451,7 +451,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ 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) ; \
@@ -464,7 +464,7 @@
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (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) ; \
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
@@ -482,7 +482,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ 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); \
@@ -495,7 +495,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ 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); \
@@ -509,7 +509,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ 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); \
@@ -522,7 +522,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ 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); \
@@ -535,7 +535,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (G,C) ml = Some (C,rT,maxl,ins); \
\ 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); \
@@ -548,7 +548,7 @@
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
-\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
+\ method (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) ; \
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
@@ -565,10 +565,10 @@
Goalw [correct_state_def,Let_def]
"G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \
-\ \\<Longrightarrow> \\<exists>meth. cmethd (G,C) ml = Some(C,meth)";
+\ \\<Longrightarrow> \\<exists>meth. method (G,C) ml = Some(C,meth)";
by(Asm_full_simp_tac 1);
by(Blast_tac 1);
-qed "correct_state_impl_Some_cmethd";
+qed "correct_state_impl_Some_method";
Goal
"\\<And>state. \\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM state\\<surd>\\<rbrakk> \
@@ -580,7 +580,7 @@
by (asm_full_simp_tac (simpset() addsimps exec.rules) 1);
by(split_all_tac 1);
by(hyp_subst_tac 1);
- by(forward_tac [correct_state_impl_Some_cmethd] 1);
+ by(forward_tac [correct_state_impl_Some_method] 1);
by (force_tac (claset() addIs [LS_correct,CO_correct,MO_correct,CH_correct,MI_correct,MR_correct,OS_correct,
BR_correct], simpset() addsplits [instr.split,instr.split_asm] addsimps exec.rules@[split_def]) 1);
by (exhaust_tac "frs" 1);
--- a/src/HOL/MicroJava/BV/Correct.thy Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Fri Nov 26 08:46:59 1999 +0100
@@ -34,14 +34,14 @@
(ST,LT) = (phi C ml) ! pc
in
(\\<exists>rT maxl ins.
- cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
+ method (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
(\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = MI(Invoke mn pTs) \\<and>
(mn,pTs) = ml0 \\<and>
(\\<exists>apTs D ST'.
fst((phi C ml)!k) = (rev apTs) @ (Class D) # ST' \\<and>
length apTs = length pTs \\<and>
(\\<exists>D' rT' maxl' ins'.
- cmethd (G,D) (mn,pTs) = Some(D',rT',(maxl',ins')) \\<and>
+ method (G,D) (mn,pTs) = Some(D',rT',(maxl',ins')) \\<and>
G \\<turnstile> rT0 \\<preceq> rT') \\<and>
correct_frame G hp (tl ST, LT) maxl ins f \\<and>
correct_frames G hp phi rT C ml frs))))"
@@ -57,7 +57,7 @@
| (f#fs) \\<Rightarrow> (let (stk,loc,C,ml,pc) = f
in
\\<exists>rT maxl ins.
- cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
+ method (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
G\\<turnstile>h hp\\<surd> \\<and>
correct_frame G hp ((phi C ml) ! pc) maxl ins f \\<and>
correct_frames G hp phi rT C ml fs))
--- a/src/HOL/MicroJava/J/Eval.thy Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy Fri Nov 26 08:46:59 1999 +0100
@@ -72,7 +72,7 @@
(* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
Call "\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>a'\\<rightarrow> s1; a = the_Addr a';
G\\<turnstile>s1 -ps[\\<succ>]pvs\\<rightarrow> (x,(h,l)); dynT = fst (the (h a));
- (md,rT,pns,lvars,blk,res) = the (cmethd (G,dynT) (mn,pTs));
+ (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk\\<rightarrow> s3;
G\\<turnstile> s3 -res\\<succ>v \\<rightarrow> (x4,s4)\\<rbrakk> \\<Longrightarrow>
G\\<turnstile>Norm s0 -e..mn({pTs}ps)\\<succ>v\\<rightarrow> (x4,(heap s4,l))"
--- a/src/HOL/MicroJava/J/JTypeSafe.ML Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML Fri Nov 26 08:46:59 1999 +0100
@@ -44,7 +44,7 @@
by Auto_tac;
qed "Cast_conf";
-Goal "\\<lbrakk> wf_prog wtm G; cfield (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \
+Goal "\\<lbrakk> wf_prog wtm G; field (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \
\ x' = None \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>Class C; np a' x' = None \\<rbrakk> \\<Longrightarrow> \
\ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))\\<Colon>\\<preceq>ft";
by( dtac np_NoneD 1);
@@ -66,7 +66,7 @@
"\\<lbrakk> wf_prog wtm G; a = the_Addr a'; (c, fs) = the (h a); \
\ (G, lT)\\<turnstile>v\\<Colon>T'; G\\<turnstile>T'\\<preceq>ft; \
\ (G, lT)\\<turnstile>aa\\<Colon>Class C; \
-\ cfield (G,C) fn = Some (fd, ft); h''\\<le>|h'; \
+\ field (G,C) fn = Some (fd, ft); h''\\<le>|h'; \
\ x' = None \\<longrightarrow> G,h'\\<turnstile>a'\\<Colon>\\<preceq>Class C; h'\\<le>|h; \
\ (h, l)\\<Colon>\\<preceq>(G, lT); G,h\\<turnstile>x\\<Colon>\\<preceq>T'; np a' x' = None\\<rbrakk> \\<Longrightarrow> \
\ h''\\<le>|h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))) \\<and> \
@@ -126,7 +126,7 @@
\ max_spec G T (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 (cmethd (G,fst (the (h (the_Addr a')))) (mn, pTs'));\
+\ the (method (G,fst (the (h (the_Addr a')))) (mn, pTs'));\
\ \\<forall>lT. (h, init_vars lvars(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))\\<Colon>\\<preceq>(G, lT) \\<longrightarrow> \
\ (G, lT)\\<turnstile>blk\\<surd> \\<longrightarrow> h\\<le>|xi \\<and> (xi, xl)\\<Colon>\\<preceq>(G, lT); \
\ \\<forall>lT. (xi, xl)\\<Colon>\\<preceq>(G, lT) \\<longrightarrow> (\\<forall>T. (G, lT)\\<turnstile>res\\<Colon>T \\<longrightarrow> \
@@ -146,7 +146,7 @@
by( Clarsimp_tac 1);
by( EVERY'[dtac Call_lemma, atac, atac] 1);
by( clarsimp_tac (claset(),simpset() addsimps [wt_java_mdecl_def])1);
-by( thin_tac "cmethd ?sig ?x = ?y" 1);
+by( thin_tac "method ?sig ?x = ?y" 1);
by( EVERY'[dtac spec, etac impE] 1);
by( mp_tac 2);
by( rtac conformsI 1);
@@ -326,7 +326,7 @@
Goal "\\<lbrakk>G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>a'\\<rightarrow> Norm s'; a' \\<noteq> Null;\
\ s\\<Colon>\\<preceq>E; E\\<turnstile>e\\<Colon>RefT T; m_head G T sig \\<noteq> None\\<rbrakk> \\<Longrightarrow> \
-\ cmethd (G,fst (the (heap s' (the_Addr a')))) sig \\<noteq> None";
+\ method (G,fst (the (heap s' (the_Addr a')))) sig \\<noteq> None";
by( dtac eval_type_sound 1);
by( atac 1);
by( atac 1);
--- a/src/HOL/MicroJava/J/TypeRel.ML Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.ML Fri Nov 26 08:46:59 1999 +0100
@@ -76,8 +76,8 @@
by(Force_tac 1);
val wf_subcls1_rel = result();
-val cmethd_TC = prove_goalw_cterm [subcls1_rel_def]
- (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (cmethd.tcs)))))
+val method_TC = prove_goalw_cterm [subcls1_rel_def]
+ (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (method.tcs)))))
(K [auto_tac (claset() addIs [subcls1I], simpset())]);
val fields_TC = prove_goalw_cterm [subcls1_rel_def]
--- a/src/HOL/MicroJava/J/TypeRel.thy Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Fri Nov 26 08:46:59 1999 +0100
@@ -32,8 +32,8 @@
consts
- cmethd :: "'c prog \\<times> cname \\<Rightarrow> ( sig \\<leadsto> cname \\<times> ty \\<times> 'c)"
- cfield :: "'c prog \\<times> cname \\<Rightarrow> ( vname \\<leadsto> cname \\<times> ty)"
+ method :: "'c prog \\<times> cname \\<Rightarrow> ( sig \\<leadsto> cname \\<times> ty \\<times> 'c)"
+ field :: "'c prog \\<times> cname \\<Rightarrow> ( vname \\<leadsto> cname \\<times> ty)"
fields :: "'c prog \\<times> cname \\<Rightarrow> ((vname \\<times> cname) \\<times> ty) list"
constdefs (* auxiliary relations for recursive definitions below *)
@@ -42,10 +42,10 @@
"subcls1_rel \\<equiv> {((G,C),(G',C')). G = G' \\<and> wf ((subcls1 G)^-1) \\<and> G\\<turnstile>C'\\<prec>C1C}"
(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
-recdef cmethd "subcls1_rel"
- "cmethd (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> empty
+recdef method "subcls1_rel"
+ "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> empty
| Some (sc,fs,ms) \\<Rightarrow> (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow>
- if is_class G D then cmethd (G,D)
+ if is_class G D then method (G,D)
else arbitrary) \\<oplus>
map_of (map (\\<lambda>(s, m ).
(s,(C,m))) ms))
@@ -61,7 +61,7 @@
else arbitrary)"
defs
- cfield_def "cfield \\<equiv> map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
+ field_def "field \\<equiv> map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
i.e. sort of syntactic subtyping *)
--- a/src/HOL/MicroJava/J/WellForm.ML Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/J/WellForm.ML Fri Nov 26 08:46:59 1999 +0100
@@ -111,11 +111,11 @@
by( etac subcls1I 1);
qed "subcls1_induct";
-Goal "wf_prog wtm G \\<Longrightarrow> cmethd (G,C) = \
+Goal "wf_prog wtm G \\<Longrightarrow> method (G,C) = \
\ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
-\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> cmethd (G,D)) \\<oplus> \
+\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
-by( stac (cmethd_TC RS (wf_subcls1_rel RS (hd cmethd.rules))) 1);
+by( stac (method_TC RS (wf_subcls1_rel RS (hd method.rules))) 1);
by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def]
addsplits [option.split]) 1);
by( case_tac "C = Object" 1);
@@ -125,7 +125,7 @@
by( dtac wf_cdecl_supD 1);
by( atac 1);
by( Asm_full_simp_tac 1);
-val cmethd_rec = result();
+val method_rec = result();
Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wtm G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
@@ -144,14 +144,14 @@
by( Asm_full_simp_tac 1);
val fields_rec = result();
-val cmethd_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> cmethd (G,Object) = empty"
- (K [stac cmethd_rec 1,Auto_tac]);
+val method_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> method (G,Object) = empty"
+ (K [stac method_rec 1,Auto_tac]);
val fields_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> fields (G,Object) = []"(K [
stac fields_rec 1,Auto_tac]);
-Addsimps [cmethd_Object, fields_Object];
-val cfield_Object = prove_goalw thy [cfield_def]
- "\\<And>X. wf_prog wtm G \\<Longrightarrow> cfield (G,Object) = empty" (K [Asm_simp_tac 1]);
-Addsimps [cfield_Object];
+Addsimps [method_Object, fields_Object];
+val field_Object = prove_goalw thy [field_def]
+ "\\<And>X. wf_prog wtm G \\<Longrightarrow> field (G,Object) = empty" (K [Asm_simp_tac 1]);
+Addsimps [field_Object];
val subcls_C_Object = prove_goal thy
"\\<And>X. \\<lbrakk>is_class G C; wf_prog wtm G \\<rbrakk> \\<Longrightarrow> C \\<noteq> Object \\<longrightarrow> G\\<turnstile>C\\<prec>C Object" (K [
@@ -264,24 +264,24 @@
val widen_fields_mono = result();
-val cfs_fields_lemma = prove_goalw thy [cfield_def]
-"\\<And>X. cfield (G,C) fn = Some (fd, fT) \\<Longrightarrow> map_of(fields (G,C)) (fn, fd) = Some fT"
+val cfs_fields_lemma = prove_goalw thy [field_def]
+"\\<And>X. field (G,C) fn = Some (fd, fT) \\<Longrightarrow> map_of(fields (G,C)) (fn, fd) = Some fT"
(K [rtac table_map_Some 1, Asm_full_simp_tac 1]);
-val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>cfield (G,C) fn = Some (fd, fT);\
+val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>field (G,C) fn = Some (fd, fT);\
\ G\\<turnstile>Class C'\\<preceq>Class C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
-Goal "wf_prog wtm G \\<Longrightarrow> cmethd (G,C) sig = Some (md,mh,m)\
+Goal "wf_prog wtm G \\<Longrightarrow> method (G,C) sig = Some (md,mh,m)\
\ \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class md \\<and> wf_mdecl wtm G md (sig,(mh,m))";
by( case_tac "is_class G C" 1);
-by( forw_inst_tac [("C","C")] cmethd_rec 2);
+by( forw_inst_tac [("C","C")] method_rec 2);
by( asm_full_simp_tac (simpset() addsimps [is_class_def]
delsimps [not_None_eq]) 2);
by( etac subcls1_induct 1);
by( atac 1);
by( Force_tac 1);
-by( forw_inst_tac [("C","C")] cmethd_rec 1);
+by( forw_inst_tac [("C","C")] method_rec 1);
by( strip_tac1 1);
by( rotate_tac ~1 1);
by( Asm_full_simp_tac 1);
@@ -300,11 +300,11 @@
by( Asm_full_simp_tac 1);
by( rewtac wf_cdecl_def);
by( Asm_full_simp_tac 1);
-val cmethd_wf_mdecl = result() RS mp;
+val method_wf_mdecl = result() RS mp;
Goal "\\<lbrakk>G\\<turnstile>T\\<prec>C T'; wf_prog wt G\\<rbrakk> \\<Longrightarrow> \
-\ \\<forall>D rT b. cmethd (G,T') sig = Some (D,rT ,b) \\<longrightarrow>\
-\ (\\<exists>D' rT' b'. cmethd (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
+\ \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) \\<longrightarrow>\
+\ (\\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
by( etac trancl_trans_induct 1);
by( strip_tac1 2);
by( EVERY[dtac spec 2, dtac spec 2, dtac spec 2, mp_tac 2]);
@@ -312,7 +312,7 @@
by( strip_tac1 1);
by( dtac subcls1D 1);
by( strip_tac1 1);
-by( stac cmethd_rec 1);
+by( stac method_rec 1);
by( atac 1);
by( rewtac override_def);
by( asm_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
@@ -334,33 +334,33 @@
Goal
"\\<lbrakk> G\\<turnstile>Class C\\<preceq>Class D; wf_prog wt G; \
-\ cmethd (G,D) sig = Some (md, rT, b) \\<rbrakk> \
-\ \\<Longrightarrow> \\<exists>mD' rT' b'. cmethd (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
+\ method (G,D) sig = Some (md, rT, b) \\<rbrakk> \
+\ \\<Longrightarrow> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
by(auto_tac (claset() addSDs [widen_Class_Class]
- addDs [subcls_widen_methd,cmethd_wf_mdecl],
+ addDs [subcls_widen_methd,method_wf_mdecl],
simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def]));
qed "subtype_widen_methd";
-Goal "wf_prog wt G \\<Longrightarrow> \\<forall>D. cmethd (G,C) sig = Some(D,mh,code) \\<longrightarrow> is_class G D \\<and> cmethd (G,D) sig = Some(D,mh,code)";
+Goal "wf_prog wt G \\<Longrightarrow> \\<forall>D. method (G,C) sig = Some(D,mh,code) \\<longrightarrow> is_class G D \\<and> method (G,D) sig = Some(D,mh,code)";
by( case_tac "is_class G C" 1);
-by( forw_inst_tac [("C","C")] cmethd_rec 2);
+by( forw_inst_tac [("C","C")] method_rec 2);
by( asm_full_simp_tac (simpset() addsimps [is_class_def]
delsimps [not_None_eq]) 2);
by (etac subcls1_induct 1);
ba 1;
by (Asm_full_simp_tac 1);
-by (stac cmethd_rec 1);
+by (stac method_rec 1);
ba 1;
by (Clarify_tac 1);
by (eres_inst_tac [("x","Da")] allE 1);
by (Clarsimp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [map_of_map]) 1);
by (Clarify_tac 1);
- by (stac cmethd_rec 1);
+ by (stac method_rec 1);
ba 1;
by (asm_full_simp_tac (simpset() addsimps [override_def,map_of_map] addsplits [option.split]) 1);
-qed_spec_mp "cmethd_in_md";
+qed_spec_mp "method_in_md";
writeln"OK";
--- a/src/HOL/MicroJava/J/WellForm.thy Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Fri Nov 26 08:46:59 1999 +0100
@@ -38,7 +38,7 @@
| Some D \\<Rightarrow>
is_class G D \\<and> \\<not> G\\<turnstile>D\\<prec>C C \\<and>
(\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
- cmethd(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
+ method(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
wf_prog :: "'c wtm \\<Rightarrow> 'c prog \\<Rightarrow> bool"
"wf_prog wtm G \\<equiv>
--- a/src/HOL/MicroJava/J/WellType.ML Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/J/WellType.ML Fri Nov 26 08:46:59 1999 +0100
@@ -6,7 +6,7 @@
Goalw [m_head_def]
"\\<lbrakk> m_head G T sig = Some (md,rT); wf_prog wtm G; G\\<turnstile>Class T''\\<preceq>RefT T\\<rbrakk> \\<Longrightarrow> \
-\\\<exists>md' rT' b'. cmethd (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
+\\\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
by( forward_tac [widen_Class_RefT] 1);
by( etac exE 1);
by( hyp_subst_tac 1);
@@ -25,13 +25,13 @@
Goal
"\\<lbrakk>m_head G T sig = Some (md,rT); G\\<turnstile>Class T''\\<preceq>RefT T; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
-\ \\<exists>T' rT' b. cmethd (G,T'') sig = Some (T',rT',b) \\<and> \
+\ \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>Class T''\\<preceq>Class T' \\<and> wf_mhead G sig rT' \\<and> wtm G T' (sig,rT',b)";
by( dtac widen_methd 1);
by( atac 1);
by( atac 1);
by( Clarsimp_tac 1);
-by( dtac cmethd_wf_mdecl 1);
+by( dtac method_wf_mdecl 1);
by( atac 1);
by( rewtac wf_mdecl_def);
by Auto_tac;
--- a/src/HOL/MicroJava/J/WellType.thy Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy Fri Nov 26 08:46:59 1999 +0100
@@ -43,7 +43,7 @@
defs
m_head_def "m_head G t sig \\<equiv> case t of NullT \\<Rightarrow> None | ClassT C \\<Rightarrow>
- option_map (\\<lambda>(md,(rT,mb)). (Class md,rT)) (cmethd (G,C) sig)"
+ option_map (\\<lambda>(md,(rT,mb)). (Class md,rT)) (method (G,C) sig)"
more_spec_def "more_spec G \\<equiv> \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
@@ -118,7 +118,7 @@
(* cf. 15.10.1 *)
FAcc "\\<lbrakk>E\\<turnstile>a\\<Colon>Class C;
- cfield (prg E,C) fn = Some (fd,fT)\\<rbrakk> \\<Longrightarrow>
+ field (prg E,C) fn = Some (fd,fT)\\<rbrakk> \\<Longrightarrow>
E\\<turnstile>{fd}a..fn\\<Colon>fT"
(* cf. 15.25, 15.25.1 *)
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Fri Nov 26 08:46:59 1999 +0100
@@ -30,39 +30,38 @@
"exec (G, xp, hp, []) = None"
"exec (G, None, hp, (stk,loc,cn,ml,pc)#frs) =
- Some (case snd(snd(snd(the(cmethd (G,cn) ml)))) ! pc of
- LS ins \\<Rightarrow> (let (stk',loc',pc') = exec_las ins stk loc pc
- in
- (None,hp,(stk',loc',cn,ml,pc')#frs))
-
- | CO ins \\<Rightarrow> (let (xp',hp',stk',pc') = exec_co ins G hp stk pc
+ Some (case snd(snd(snd(the(method (G,cn) ml)))) ! pc of
+ LS ins \\<Rightarrow> let (stk',loc',pc') = exec_las ins stk loc pc
in
- (xp',hp',(stk',loc,cn,ml,pc')#frs))
+ (None,hp,(stk',loc',cn,ml,pc')#frs)
- | MO ins \\<Rightarrow> (let (xp',hp',stk',pc') = exec_mo ins hp stk pc
+ | CO ins \\<Rightarrow> let (xp',hp',stk',pc') = exec_co ins G hp stk pc
in
- (xp',hp',(stk',loc,cn,ml,pc')#frs))
+ (xp',hp',(stk',loc,cn,ml,pc')#frs)
- | CH ins \\<Rightarrow> (let (xp',stk',pc') = exec_ch ins G hp stk pc
+ | MO ins \\<Rightarrow> let (xp',hp',stk',pc') = exec_mo ins hp stk pc
in
- (xp',hp,(stk',loc,cn,ml,pc')#frs))
+ (xp',hp',(stk',loc,cn,ml,pc')#frs)
- | MI ins \\<Rightarrow> (let (xp',frs',stk',pc') = exec_mi ins G hp stk pc
+ | CH ins \\<Rightarrow> let (xp',stk',pc') = exec_ch ins G hp stk pc
in
- (xp',hp,frs'@(stk',loc,cn,ml,pc')#frs))
+ (xp',hp,(stk',loc,cn,ml,pc')#frs)
- | MR ins \\<Rightarrow> (let frs' = exec_mr ins stk frs in
- (None,hp,frs'))
+ | MI ins \\<Rightarrow> let (xp',frs',stk',pc') = exec_mi ins G hp stk pc
+ in
+ (xp',hp,frs'@(stk',loc,cn,ml,pc')#frs)
+
+ | MR ins \\<Rightarrow> let frs' = exec_mr ins stk frs in (None,hp,frs')
- | OS ins \\<Rightarrow> (let (stk',pc') = exec_os ins stk pc
+ | OS ins \\<Rightarrow> let (stk',pc') = exec_os ins stk pc
in
- (None,hp,(stk',loc,cn,ml,pc')#frs))
+ (None,hp,(stk',loc,cn,ml,pc')#frs)
- | BR ins \\<Rightarrow> (let (stk',pc') = exec_br ins stk pc
+ | BR ins \\<Rightarrow> let (stk',pc') = exec_br ins stk pc
in
- (None,hp,(stk',loc,cn,ml,pc')#frs)))"
+ (None,hp,(stk',loc,cn,ml,pc')#frs))"
- "exec (G, Some xp, hp, f#frs) = Some (Some xp, hp, [])"
+ "exec (G, Some xp, hp, f#frs) = None"
constdefs
--- a/src/HOL/MicroJava/JVM/JVMState.thy Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/JVM/JVMState.thy Fri Nov 26 08:46:59 1999 +0100
@@ -35,21 +35,10 @@
raise_xcpt :: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option"
"raise_xcpt c x \\<equiv> (if c then Some x else None)"
- heap_update :: "[xcpt option,aheap,aheap] \\<Rightarrow> aheap"
-"heap_update xp hp' hp \\<equiv> if xp=None then hp' else hp"
-
- stk_update :: "[xcpt option,opstack,opstack] \\<Rightarrow> opstack"
-"stk_update xp stk' stk \\<equiv> if xp=None then stk' else stk"
-
- xcpt_update :: "[xcpt option,'a,'a] \\<Rightarrow> 'a"
-"xcpt_update xp y' y \\<equiv> if xp=None then y' else y"
-
(** runtime state **)
types
- jvm_state = "xcpt option \\<times>
- aheap \\<times>
- frame list"
+ jvm_state = "xcpt option \\<times> aheap \\<times> frame list"
@@ -57,5 +46,5 @@
constdefs
dyn_class :: "'code prog \\<times> sig \\<times> cname \\<Rightarrow> cname"
-"dyn_class \\<equiv> \\<lambda>(G,sig,C). fst(the(cmethd(G,C) sig))"
+"dyn_class \\<equiv> \\<lambda>(G,sig,C). fst(the(method(G,C) sig))"
end
--- a/src/HOL/MicroJava/JVM/Method.thy Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/JVM/Method.thy Fri Nov 26 08:46:59 1999 +0100
@@ -23,9 +23,11 @@
argsoref = take (n+1) stk;
oref = last argsoref;
xp' = raise_xcpt (oref=Null) NullPointer;
- dynT = fst(hp \\<And> (the_Addr oref));
- (dc,mh,mxl,c)= the (cmethd (G,dynT) (mn,ps));
- frs' = xcpt_update xp' [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)] []
+ dynT = fst(hp !! (the_Addr oref));
+ (dc,mh,mxl,c)= the (method (G,dynT) (mn,ps));
+ frs' = if xp'=None
+ then [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
+ else []
in
(xp' , frs' , drop (n+1) stk , pc+1))"
--- a/src/HOL/MicroJava/JVM/Object.thy Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/JVM/Object.thy Fri Nov 26 08:46:59 1999 +0100
@@ -21,8 +21,8 @@
(let xp' = raise_xcpt (\\<forall>x. hp x \\<noteq> None) OutOfMemory;
oref = newref hp;
fs = init_vars (fields(G,C));
- hp' = xcpt_update xp' (hp(oref \\<mapsto> (C,fs))) hp;
- stk' = xcpt_update xp' ((Addr oref)#stk) stk
+ hp' = if xp'=None then hp(oref \\<mapsto> (C,fs)) else hp;
+ stk' = if xp'=None then (Addr oref)#stk else stk
in (xp' , hp' , stk' , pc+1))"
@@ -39,8 +39,8 @@
"exec_mo (Getfield F C) hp stk pc =
(let oref = hd stk;
xp' = raise_xcpt (oref=Null) NullPointer;
- (oc,fs) = hp \\<And> (the_Addr oref);
- stk' = xcpt_update xp' ((fs\\<And>(F,C))#(tl stk)) (tl stk)
+ (oc,fs) = hp !! (the_Addr oref);
+ stk' = if xp'=None then (fs!!(F,C))#(tl stk) else tl stk
in
(xp' , hp , stk' , pc+1))"
@@ -48,8 +48,8 @@
(let (fval,oref)= (hd stk, hd(tl stk));
xp' = raise_xcpt (oref=Null) NullPointer;
a = the_Addr oref;
- (oc,fs) = hp \\<And> a;
- hp' = xcpt_update xp' (hp(a \\<mapsto> (oc, fs((F,C) \\<mapsto> fval)))) hp
+ (oc,fs) = hp !! a;
+ hp' = if xp'=None then hp(a \\<mapsto> (oc, fs((F,C) \\<mapsto> fval))) else hp
in
(xp' , hp' , tl (tl stk), pc+1))"
@@ -66,7 +66,7 @@
"exec_ch (Checkcast C) G hp stk pc =
(let oref = hd stk;
xp' = raise_xcpt (\\<not> cast_ok G (Class C) hp oref) ClassCast;
- stk' = xcpt_update xp' stk (tl stk)
+ stk' = if xp'=None then stk else tl stk
in
(xp' , stk' , pc+1))"
--- a/src/HOL/MicroJava/JVM/Store.thy Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/JVM/Store.thy Fri Nov 26 08:46:59 1999 +0100
@@ -12,9 +12,9 @@
Store = Conform +
syntax
- value :: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b" ("_ \\<And> _")
+ map_apply :: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b" ("_ !! _")
translations
- "t \\<And> x" == "the (t x)"
+ "t !! x" == "the (t x)"
constdefs
newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a"