--- a/src/HOL/MicroJava/BV/BVSpec.thy Mon Jul 17 13:59:10 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Mon Jul 17 14:00:53 2000 +0200
@@ -14,9 +14,10 @@
prog_type = "cname \\<Rightarrow> class_type"
consts
- wt_LS :: "[load_and_store,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
+wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count] \\<Rightarrow> bool"
+
primrec
-"wt_LS (Load idx) G phi max_pc pc =
+"wt_instr (Load idx) G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc \\<and>
@@ -24,7 +25,7 @@
(\\<exists>ts. (LT ! idx) = Some ts \\<and>
G \\<turnstile> (ts # ST , LT) <=s phi ! (pc+1)))"
-"wt_LS (Store idx) G phi max_pc pc =
+"wt_instr (Store idx) G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc \\<and>
@@ -32,22 +33,19 @@
(\\<exists>ts ST'. ST = ts # ST' \\<and>
G \\<turnstile> (ST' , LT[idx:=Some ts]) <=s phi ! (pc+1)))"
-"wt_LS (Bipush i) G phi max_pc pc =
+"wt_instr (Bipush i) G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc \\<and>
G \\<turnstile> ((PrimT Integer) # ST , LT) <=s phi ! (pc+1))"
-"wt_LS (Aconst_null) G phi max_pc pc =
+"wt_instr (Aconst_null) G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc \\<and>
G \\<turnstile> (NT # ST , LT) <=s phi ! (pc+1))"
-consts
- wt_MO :: "[manipulate_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
-primrec
-"wt_MO (Getfield F C) G phi max_pc pc =
+"wt_instr (Getfield F C) G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc \\<and>
@@ -57,7 +55,7 @@
G \\<turnstile> oT \\<preceq> (Class C) \\<and>
G \\<turnstile> (T # ST' , LT) <=s phi ! (pc+1)))"
-"wt_MO (Putfield F C) G phi max_pc pc =
+"wt_instr (Putfield F C) G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc \\<and>
@@ -69,21 +67,14 @@
G \\<turnstile> vT \\<preceq> T \\<and>
G \\<turnstile> (ST' , LT) <=s phi ! (pc+1)))"
-
-consts
- wt_CO :: "[create_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
-primrec
-"wt_CO (New C) G phi max_pc pc =
+"wt_instr (New C) G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc \\<and>
is_class G C \\<and>
G \\<turnstile> ((Class C) # ST , LT) <=s phi ! (pc+1))"
-consts
- wt_CH :: "[check_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
-primrec
-"wt_CH (Checkcast C) G phi max_pc pc =
+"wt_instr (Checkcast C) G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc \\<and>
@@ -91,56 +82,49 @@
(\\<exists>rt ST'. ST = RefT rt # ST' \\<and>
G \\<turnstile> (Class C # ST' , LT) <=s phi ! (pc+1)))"
-consts
- wt_OS :: "[op_stack,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
-primrec
-"wt_OS Pop G phi max_pc pc =
+"wt_instr Pop G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
\\<exists>ts ST'. pc+1 < max_pc \\<and>
ST = ts # ST' \\<and>
G \\<turnstile> (ST' , LT) <=s phi ! (pc+1))"
-"wt_OS Dup G phi max_pc pc =
+"wt_instr Dup G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc \\<and>
(\\<exists>ts ST'. ST = ts # ST' \\<and>
G \\<turnstile> (ts # ts # ST' , LT) <=s phi ! (pc+1)))"
-"wt_OS Dup_x1 G phi max_pc pc =
+"wt_instr Dup_x1 G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc \\<and>
(\\<exists>ts1 ts2 ST'. ST = ts1 # ts2 # ST' \\<and>
G \\<turnstile> (ts1 # ts2 # ts1 # ST' , LT) <=s phi ! (pc+1)))"
-"wt_OS Dup_x2 G phi max_pc pc =
+"wt_instr Dup_x2 G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc \\<and>
(\\<exists>ts1 ts2 ts3 ST'. ST = ts1 # ts2 # ts3 # ST' \\<and>
G \\<turnstile> (ts1 # ts2 # ts3 # ts1 # ST' , LT) <=s phi ! (pc+1)))"
-"wt_OS Swap G phi max_pc pc =
+"wt_instr Swap G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc \\<and>
(\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and>
G \\<turnstile> (ts # ts' # ST' , LT) <=s phi ! (pc+1)))"
-"wt_OS IAdd G phi max_pc pc =
+"wt_instr IAdd G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc \\<and>
(\\<exists>ST'. ST = (PrimT Integer) # (PrimT Integer) # ST' \\<and>
G \\<turnstile> ((PrimT Integer) # ST' , LT) <=s phi ! (pc+1)))"
-
-consts
- wt_BR :: "[branch,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
-primrec
-"wt_BR (Ifcmpeq branch) G phi max_pc pc =
+"wt_instr (Ifcmpeq branch) G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc \\<and> (nat(int pc+branch)) < max_pc \\<and>
@@ -150,16 +134,13 @@
G \\<turnstile> (ST' , LT) <=s phi ! (pc+1) \\<and>
G \\<turnstile> (ST' , LT) <=s phi ! (nat(int pc+branch))))"
-"wt_BR (Goto branch) G phi max_pc pc =
+"wt_instr (Goto branch) G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
(nat(int pc+branch)) < max_pc \\<and>
G \\<turnstile> (ST , LT) <=s phi ! (nat(int pc+branch)))"
-consts
- wt_MI :: "[meth_inv,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
-primrec
-"wt_MI (Invoke mn fpTs) G phi max_pc pc =
+"wt_instr (Invoke mn fpTs) G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
pc+1 < max_pc \\<and>
@@ -170,30 +151,13 @@
(\\<exists>D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
G \\<turnstile> (rT # ST' , LT) <=s phi ! (pc+1))))))"
-consts
- wt_MR :: "[meth_ret,jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool"
-primrec
- "wt_MR Return G rT phi pc =
+"wt_instr Return G rT phi max_pc pc =
(let (ST,LT) = phi ! pc
in
(\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT))"
constdefs
- wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count] \\<Rightarrow> bool"
- "wt_instr instr G rT phi max_pc pc \\<equiv>
- case instr of
- LS ins \\<Rightarrow> wt_LS ins G phi max_pc pc
- | CO ins \\<Rightarrow> wt_CO ins G phi max_pc pc
- | MO ins \\<Rightarrow> wt_MO ins G phi max_pc pc
- | CH ins \\<Rightarrow> wt_CH ins G phi max_pc pc
- | MI ins \\<Rightarrow> wt_MI ins G phi max_pc pc
- | MR ins \\<Rightarrow> wt_MR ins G rT phi pc
- | OS ins \\<Rightarrow> wt_OS ins G phi max_pc pc
- | BR ins \\<Rightarrow> wt_BR ins G phi max_pc pc"
-
-
-constdefs
wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \\<Rightarrow> bool"
"wt_start G C pTs mxl phi \\<equiv>
G \\<turnstile> ([],(Some(Class C))#((map Some pTs))@(replicate mxl None)) <=s phi!0"
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Mon Jul 17 13:59:10 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Mon Jul 17 14:00:53 2000 +0200
@@ -5,7 +5,7 @@
*)
val defs1 = exec.simps@[split_def,sup_state_def,correct_state_def,
- correct_frame_def,wt_instr_def];
+ correct_frame_def];
Goalw [correct_state_def,Let_def,correct_frame_def,split_def]
"\\<lbrakk> wt_jvm_prog G phi; \
@@ -25,7 +25,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = LS(Load idx); \
+\ ins!pc = Load idx; \
\ 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> \
@@ -38,7 +38,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = LS(Store idx); \
+\ ins!pc = Store idx; \
\ 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> \
@@ -55,7 +55,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = LS(Bipush i); \
+\ ins!pc = Bipush i; \
\ 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> \
@@ -79,7 +79,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = LS Aconst_null; \
+\ ins!pc = Aconst_null; \
\ 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> \
@@ -89,23 +89,6 @@
qed "Aconst_null_correct";
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = LS ls_com; \
-\ 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_prog_impl_wt_instr_cor] 1);
- ba 1;
- ba 1;
-by(rewtac wt_jvm_prog_def);
-by (case_tac "ls_com" 1);
-by (ALLGOALS (fast_tac (claset() addIs [Load_correct,Store_correct,Bipush_correct,Aconst_null_correct])));
-qed "LS_correct";
-
-
-(**** CH ****)
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> \
@@ -124,7 +107,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = CH (Checkcast D); \
+\ ins!pc = Checkcast D; \
\ 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> \
@@ -135,28 +118,11 @@
addss (simpset() addsimps [map_eq_Cons,approx_val_def])) 1);
qed "Checkcast_correct";
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = CH ch_com; \
-\ 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_prog_impl_wt_instr_cor] 1);
- ba 1;
- ba 1;
-by(rewtac wt_jvm_prog_def);
-by (case_tac "ch_com" 1);
-by (ALLGOALS (fast_tac (claset() addIs [Checkcast_correct])));
-qed "CH_correct";
-
-
-(******* MO *******)
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = MO (Getfield F D); \
+\ ins!pc = Getfield F D; \
\ 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> \
@@ -187,7 +153,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = MO (Putfield F D); \
+\ ins!pc = Putfield F D; \
\ 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> \
@@ -209,24 +175,6 @@
qed "Putfield_correct";
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = MO mo_com; \
-\ 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_prog_impl_wt_instr_cor] 1);
- ba 1;
- ba 1;
-by(rewtac wt_jvm_prog_def);
-by (case_tac "mo_com" 1);
-by (ALLGOALS (fast_tac (claset() addIs [Getfield_correct,Putfield_correct])));
-qed "MO_correct";
-
-
-(****** CO ******)
-
Goal "(\\<forall>x y. P(x,y)) = (\\<forall>z. P z)";
by(Fast_tac 1);
qed "collapse_paired_All";
@@ -234,7 +182,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = CO(New cl_idx); \
+\ ins!pc = New cl_idx; \
\ 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> \
@@ -249,28 +197,13 @@
addsplits [option.split])) 1);
qed "New_correct";
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = CO co_com; \
-\ 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_prog_impl_wt_instr_cor] 1);
- ba 1;
- ba 1;
-by(rewtac wt_jvm_prog_def);
-by (case_tac "co_com" 1);
-by (ALLGOALS (fast_tac (claset() addIs [New_correct])));
-qed "CO_correct";
-
-(****** MI ******)
+(****** Method Invocation ******)
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins ! pc = MI(Invoke mn pTs); \
+\ ins ! pc = Invoke 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> \
@@ -347,27 +280,12 @@
by (Asm_simp_tac 1);
qed "Invoke_correct";
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = MI mi_com; \
-\ 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_prog_impl_wt_instr_cor] 1);
- ba 1;
- ba 1;
-by (case_tac "mi_com" 1);
-by (ALLGOALS (fast_tac (claset() addIs [Invoke_correct])));
-qed "MI_correct";
-
-(****** MR ******)
Delsimps [map_append];
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins ! pc = MR Return; \
+\ ins ! pc = Return; \
\ 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> \
@@ -388,25 +306,11 @@
qed "Return_correct";
Addsimps [map_append];
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = MR mr; \
-\ 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_prog_impl_wt_instr_cor] 1);
- ba 1;
- ba 1;
-by (case_tac "mr" 1);
-by (ALLGOALS (fast_tac (claset() addIs [Return_correct])));
-qed "MR_correct";
-(****** BR ******)
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins ! pc = BR(Goto branch); \
+\ ins ! pc = Goto branch; \
\ 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> \
@@ -419,7 +323,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = BR(Ifcmpeq branch); \
+\ ins!pc = Ifcmpeq branch; \
\ 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> \
@@ -428,28 +332,10 @@
qed "Ifiacmpeq_correct";
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = BR br_com; \
-\ 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_prog_impl_wt_instr_cor] 1);
- ba 1;
- ba 1;
-by(rewtac wt_jvm_prog_def);
-by (case_tac "br_com" 1);
-by (ALLGOALS (fast_tac (claset() addIs [Goto_correct,Ifiacmpeq_correct])));
-qed "BR_correct";
-
-
-(****** OS ******)
-
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins ! pc = OS Pop; \
+\ ins ! pc = Pop; \
\ 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> \
@@ -461,7 +347,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins ! pc = OS Dup; \
+\ ins ! pc = Dup; \
\ 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> \
@@ -474,7 +360,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins ! pc = OS Dup_x1; \
+\ ins ! pc = Dup_x1; \
\ 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> \
@@ -486,7 +372,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins ! pc = OS Dup_x2; \
+\ ins ! pc = Dup_x2; \
\ 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> \
@@ -498,7 +384,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins ! pc = OS Swap; \
+\ ins ! pc = Swap; \
\ 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> \
@@ -511,7 +397,7 @@
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins ! pc = OS IAdd; \
+\ ins ! pc = IAdd; \
\ 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> \
@@ -521,20 +407,28 @@
qed "IAdd_correct";
+(** instr correct **)
+
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins!pc = OS os_com; \
\ 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_prog_impl_wt_instr_cor] 1);
ba 1;
ba 1;
+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 (case_tac "os_com" 1);
-by (ALLGOALS (fast_tac (claset() addIs [Pop_correct,Dup_correct,Dup_x1_correct,Dup_x2_correct,Swap_correct,IAdd_correct])));
-qed "OS_correct";
+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,
+ Dup_x1_correct,Dup_x2_correct,Swap_correct,IAdd_correct])));
+qed "instr_correct";
+
(** Main **)
@@ -556,8 +450,7 @@
by(split_all_tac 1);
by(hyp_subst_tac 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 [split_if_asm,instr.split,instr.split_asm] addsimps exec.simps@[split_def]) 1);
+ by (force_tac (claset() addIs [instr_correct], simpset() addsplits [split_if_asm] addsimps exec.simps@[split_def]) 1);
by (case_tac "frs" 1);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps exec.simps)));
qed_spec_mp "BV_correct_1";
@@ -565,8 +458,10 @@
(*******)
Goal
"\\<lbrakk> xp=None; frs\\<noteq>[] \\<rbrakk> \\<Longrightarrow> (\\<exists>state'. exec (G,xp,hp,frs) = Some state')";
-by (fast_tac (claset() addIs [BV_correct_1]
- addss (simpset() addsplits [instr.split] addsimps [neq_Nil_conv]@defs1)) 1);
+by (auto_tac (claset() addIs [BV_correct_1],
+ (simpset() addsplits [instr.split] addsimps [neq_Nil_conv]@defs1)));
+by (case_tac "(snd (snd (snd (the (method (G, ab) (ac, b)))))) ! ba" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps defs1)));
val lemma = result();
Goal
--- a/src/HOL/MicroJava/BV/Correct.thy Mon Jul 17 13:59:10 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy Mon Jul 17 14:00:53 2000 +0200
@@ -34,7 +34,7 @@
in
(\\<exists>rT maxl ins.
method (G,C) sig = Some(C,rT,(maxl,ins)) \\<and>
- (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = MI(Invoke mn pTs) \\<and>
+ (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = (Invoke mn pTs) \\<and>
(mn,pTs) = sig0 \\<and>
(\\<exists>apTs D ST'.
fst((phi C sig)!k) = (rev apTs) @ (Class D) # ST' \\<and>
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Mon Jul 17 13:59:10 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Mon Jul 17 14:00:53 2000 +0200
@@ -18,13 +18,13 @@
contains_dead :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
"contains_dead ins cert phi pc \\<equiv>
- (((\\<exists> branch. ins!pc = BR (Goto branch)) \\<or> ins!pc = MR Return) \\<or>
- (\\<exists>mi. ins!pc = MI mi)) \\<longrightarrow> Suc pc < length phi \\<longrightarrow>
+ (((\\<exists> branch. ins!pc = (Goto branch)) \\<or> ins!pc = Return) \\<or>
+ (\\<exists>m l. ins!pc = Invoke m l)) \\<longrightarrow> Suc pc < length phi \\<longrightarrow>
cert ! (Suc pc) = Some (phi ! Suc pc)"
contains_targets :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
"contains_targets ins cert phi pc \\<equiv>
- \\<forall> branch. (ins!pc = BR (Goto branch) \\<or> ins!pc = BR (Ifcmpeq branch)) \\<longrightarrow>
+ \\<forall> branch. (ins!pc = (Goto branch) \\<or> ins!pc = (Ifcmpeq branch)) \\<longrightarrow>
(let pc' = nat (int pc+branch) in pc' < length phi \\<longrightarrow> cert!pc' = Some (phi!pc'))"
fits :: "[instr list, certificate, method_type] \\<Rightarrow> bool"
@@ -36,14 +36,14 @@
is_target :: "[instr list, p_count] \\<Rightarrow> bool"
"is_target ins pc \\<equiv>
\\<exists> pc' branch. pc' < length ins \\<and>
- (ins ! pc' = (BR (Ifcmpeq branch)) \\<or> ins ! pc' = (BR (Goto branch))) \\<and>
+ (ins ! pc' = (Ifcmpeq branch) \\<or> ins ! pc' = (Goto branch)) \\<and>
pc = (nat(int pc'+branch))"
maybe_dead :: "[instr list, p_count] \\<Rightarrow> bool"
"maybe_dead ins pc \\<equiv>
- \\<exists> pc'. pc = pc'+1 \\<and> ((\\<exists> branch. ins!pc' = BR (Goto branch)) \\<or>
- ins!pc' = MR Return \\<or>
- (\\<exists>mi. ins!pc' = MI mi))"
+ \\<exists> pc'. pc = pc'+1 \\<and> ((\\<exists> branch. ins!pc' = (Goto branch)) \\<or>
+ ins!pc' = Return \\<or>
+ (\\<exists>m l. ins!pc' = Invoke m l))"
mdot :: "[instr list, p_count] \\<Rightarrow> bool"
@@ -70,10 +70,6 @@
let (sig,rT,maxl,b) = \\<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \\<in> set mdecls \\<and> sg = sig in
make_cert b (Phi C sig)";
-constdefs
- wfprg :: "jvm_prog \\<Rightarrow> bool"
- "wfprg G \\<equiv> \\<exists>wf_mb. wf_prog wf_mb G";
-
lemma length_ofn: "\\<forall>n. length (option_filter_n l P n) = length l";
by (induct l) auto;
@@ -163,7 +159,7 @@
proof (simp add: contains_targets_def, intro allI impI conjI);
fix branch;
- assume 1: "ins ! pc = BR (Goto branch)"
+ assume 1: "ins ! pc = Goto branch"
"nat (int pc + branch) < length phi"
"pc < length ins";
@@ -177,7 +173,7 @@
next;
fix branch;
- assume 2: "ins ! pc = BR (Ifcmpeq branch)"
+ assume 2: "ins ! pc = Ifcmpeq branch"
"nat (int pc + branch) < length phi"
"pc < length ins";
@@ -295,22 +291,20 @@
qed;
lemma method_inv_pseudo_mono:
-"\\<lbrakk>fits ins cert phi; i = ins!pc; i = MI meth_inv; pc < length ins;
+"\\<lbrakk>fits ins cert phi; i = ins!pc; i = Invoke mname list; pc < length ins;
wf_prog wf_mb G; G \\<turnstile> (x, y) <=s s1; wtl_inst (ins!pc) G rT s1 s1' cert mpc pc\\<rbrakk>
\\<Longrightarrow> \\<exists>s2'. wtl_inst i G rT (x, y) s2' cert mpc pc \\<and> \
((G \\<turnstile> s2' <=s s1') \\<or> (\\<exists> s. cert ! (Suc pc) = Some s \\<and> (G \\<turnstile> s2' <=s s)))";
-proof (cases meth_inv);
- case Invoke;
+proof -
assume fits: "fits ins cert phi" and
- i: "i = ins ! pc" "i = MI meth_inv" and
+ i: "i = ins ! pc" "i = Invoke mname list" and
pc: "pc < length ins" and
wfp: "wf_prog wf_mb G" and
"wtl_inst (ins!pc) G rT s1 s1' cert mpc pc" and
lt: "G \\<turnstile> (x, y) <=s s1";
- with Invoke;
- show ?thesis; (* (is "\\<exists>s2'. ?wtl s2' \\<and> (?lt s2' s1' \\<or> ?cert s2')" is "\\<exists>s2'. ?P s2'"); *)
- proof (clarsimp_tac simp del: split_paired_Ex);
+ thus ?thesis
+ proof (clarsimp_tac simp del: split_paired_Ex)
fix apTs X ST' y' s;
assume G: "G \\<turnstile> (x, y) <=s (rev apTs @ X # ST', y')";
@@ -353,7 +347,7 @@
hence x2: "G \\<turnstile> (a, y) <=s (apTs, y') \\<and> G \\<turnstile> b\\<preceq>X \\<and> G \\<turnstile> (c, y) <=s (ST', y')";
by (simp add: sup_state_rev_fst sup_state_Cons1);
- show ?thesis;
+ show ?thesis
proof (cases "X = NT");
case True;
with x2;
@@ -438,14 +432,14 @@
thus "\\<exists> apTs X ST'. ?A apTs X ST'"; by blast;
qed;
thus ?thesis; by blast;
- qed;
- qed;
- qed;
- qed;
- qed;
- qed;
- qed;
-qed;
+ qed
+ qed
+ qed
+ qed
+ qed
+ qed
+ qed
+qed
lemma sup_loc_some:
"\\<forall> y n. (G \\<turnstile> b <=l y) \\<longrightarrow> n < length y \\<longrightarrow> y!n = Some t \\<longrightarrow> (\\<exists>t. b!n = Some t \\<and> (G \\<turnstile> (b!n) <=o (y!n)))" (is "?P b");
@@ -500,7 +494,7 @@
show "xb = PrimT p \\<Longrightarrow> G \\<turnstile> xb \\<preceq> PrimT p"; by blast;
show "G\\<turnstile> xb \\<preceq> PrimT p \\<Longrightarrow> xb = PrimT p";
- proof (cases xb); print_cases;
+ proof (cases xb);
fix prim;
assume "xb = PrimT prim" "G\\<turnstile>xb\\<preceq>PrimT p";
thus ?thesis; by simp;
@@ -523,151 +517,103 @@
have 3: "\\<exists> a b. s2 = (a,b)"; by simp;
show ?thesis;
- proof (cases "ins ! pc");
+ proof (cases "ins ! pc", insert 1, insert 3);
- case LS;
- show ?thesis;
- proof (cases "load_and_store");
- case Load;
- with LS 1 3;
- show ?thesis; by (elim, clarsimp_tac) (rule mono_load [elimify], auto simp add: sup_state_length_snd);
- next;
- case Store;
- with LS 1 3;
- show ?thesis; by (elim, clarsimp_tac) (rule mono_store [elimify], auto simp add: sup_state_length_snd);
- next;
- case Bipush;
- with LS 1 3;
- show ?thesis; by (elim, clarsimp_tac simp add: sup_state_Cons1);
- next;
- case Aconst_null;
- with LS 1 3;
- show ?thesis; by (elim, clarsimp_tac simp add: sup_state_Cons1);
- qed;
-
- next;
- case CO;
- show ?thesis;
- proof (cases create_object);
- case New;
- with CO 1 3;
- show ?thesis; by (elim, clarsimp_tac simp add: sup_state_Cons1);
- qed;
-
- next;
- case MO;
+ case Load
+ with 1 3
+ show ?thesis; by (elim, clarsimp_tac) (rule mono_load [elimify], auto simp add: sup_state_length_snd);
+ next
+ case Store;
+ with 1 3;
+ show ?thesis; by (elim, clarsimp_tac) (rule mono_store [elimify], auto simp add: sup_state_length_snd);
+ next
+ case Getfield;
+ with 1 3;
show ?thesis;
- proof (cases manipulate_object);
- case Getfield;
- with MO 1 3;
- show ?thesis;
- proof (elim, clarsimp_tac simp add: sup_state_Cons2);
- fix oT x;
- assume "G \\<turnstile> x \\<preceq> oT" "G \\<turnstile> oT \\<preceq> Class cname";
- show "G \\<turnstile> x \\<preceq> Class cname"; by (rule widen_trans);
- qed;
- next;
- case Putfield;
- with MO 1 3;
- show ?thesis;
- proof (elim, clarsimp_tac simp add: sup_state_Cons2);
- fix x xa vT oT T;
- assume "G \\<turnstile> x \\<preceq> vT" "G \\<turnstile> vT \\<preceq> T";
- hence * : "G \\<turnstile> x \\<preceq> T"; by (rule widen_trans);
-
- assume "G \\<turnstile> xa \\<preceq> oT" "G \\<turnstile> oT \\<preceq> Class cname";
- hence "G \\<turnstile> xa \\<preceq> Class cname"; by (rule widen_trans);
-
- with *;
- show "(G \\<turnstile> xa \\<preceq> Class cname) \\<and> (G \\<turnstile> x \\<preceq> T)"; by blast;
- qed;
+ proof (elim, clarsimp_tac simp add: sup_state_Cons2);
+ fix oT x;
+ assume "G \\<turnstile> x \\<preceq> oT" "G \\<turnstile> oT \\<preceq> Class cname";
+ show "G \\<turnstile> x \\<preceq> Class cname"; by (rule widen_trans);
qed;
-
- next;
- case CH;
+ next
+ case Putfield;
+ with 1 3;
show ?thesis;
- proof (cases check_object);
- case Checkcast;
- with CH 1 3;
- show ?thesis; by (elim, clarsimp_tac simp add: sup_state_Cons2) (rule widen_RefT2);
- qed;
+ proof (elim, clarsimp_tac simp add: sup_state_Cons2);
+ fix x xa vT oT T;
+ assume "G \\<turnstile> x \\<preceq> vT" "G \\<turnstile> vT \\<preceq> T";
+ hence * : "G \\<turnstile> x \\<preceq> T"; by (rule widen_trans);
- next;
- case MI;
+ assume "G \\<turnstile> xa \\<preceq> oT" "G \\<turnstile> oT \\<preceq> Class cname";
+ hence "G \\<turnstile> xa \\<preceq> Class cname"; by (rule widen_trans);
+
+ with *
+ show "(G \\<turnstile> xa \\<preceq> Class cname) \\<and> (G \\<turnstile> x \\<preceq> T)"; by blast;
+ qed
+ next
+ case Checkcast;
+ with 1 3;
+ show ?thesis; by (elim, clarsimp_tac simp add: sup_state_Cons2) (rule widen_RefT2);
+ next
+ case Invoke;
with 1 2 3;
show ?thesis; by elim (rule method_inv_pseudo_mono [elimify], simp+);
-
- next;
- case MR;
- show ?thesis;
- proof (cases meth_ret);
- case Return;
- with MR 1 3;
- show ?thesis;
- proof (elim, clarsimp_tac simp add: sup_state_Cons2 simp del: split_paired_Ex);
- fix x T;
- assume "G\\<turnstile>x\\<preceq>T" "G\\<turnstile>T\\<preceq>rT";
- thus "G\\<turnstile>x\\<preceq>rT"; by (rule widen_trans);
- qed;
- qed;
-
- next;
- case OS;
+ next
+ case Return;
with 1 3;
show ?thesis;
- by - (cases op_stack, (elim, clarsimp_tac simp add: sup_state_Cons2 PrimT_PrimT)+);
-
- next;
- case BR;
+ proof (elim, clarsimp_tac simp add: sup_state_Cons2 simp del: split_paired_Ex);
+ fix x T;
+ assume "G\\<turnstile>x\\<preceq>T" "G\\<turnstile>T\\<preceq>rT";
+ thus "G\\<turnstile>x\\<preceq>rT"; by (rule widen_trans);
+ qed
+ next
+ case Goto;
+ with 1 3;
show ?thesis;
- proof (cases branch);
- case Goto;
- with BR 1 3;
- show ?thesis;
- proof (elim, clarsimp_tac simp del: split_paired_Ex);
- fix a b x y;
- assume "G \\<turnstile> (a, b) <=s s1" "G \\<turnstile> s1 <=s (x, y)";
- thus "G \\<turnstile> (a, b) <=s (x, y)"; by (rule sup_state_trans);
- qed;
+ proof (elim, clarsimp_tac simp del: split_paired_Ex);
+ fix a b x y;
+ assume "G \\<turnstile> (a, b) <=s s1" "G \\<turnstile> s1 <=s (x, y)";
+ thus "G \\<turnstile> (a, b) <=s (x, y)"; by (rule sup_state_trans);
+ qed
+ next
+ case Ifcmpeq;
+ with 1 3;
+ show ?thesis
+ proof (elim, clarsimp_tac simp add: sup_state_Cons2, intro conjI);
+ fix xt' b ST' y c d;
+ assume "G \\<turnstile> (xt', b) <=s (ST', y)" "G \\<turnstile> (ST', y) <=s (c, d)";
+ thus "G \\<turnstile> (xt', b) <=s (c, d)"; by (rule sup_state_trans);
next;
- case Ifcmpeq;
- with BR 1 3;
- show ?thesis;
- proof (elim, clarsimp_tac simp add: sup_state_Cons2, intro conjI);
- fix xt' b ST' y c d;
- assume "G \\<turnstile> (xt', b) <=s (ST', y)" "G \\<turnstile> (ST', y) <=s (c, d)";
- thus "G \\<turnstile> (xt', b) <=s (c, d)"; by (rule sup_state_trans);
+ fix ts ts' x xa;
+ assume * :
+ "(\\<exists>p. ts = PrimT p \\<and> ts' = PrimT p) \\<or> (\\<exists>r. ts = RefT r) \\<and> (\\<exists>r'. ts' = RefT r')";
+
+ assume x: "G\\<turnstile>x\\<preceq>ts" "G\\<turnstile>xa\\<preceq>ts'";
+
+ show "(\\<exists>p. x = PrimT p \\<and> xa = PrimT p) \\<or> (\\<exists>r. x = RefT r) \\<and> (\\<exists>r'. xa = RefT r')";
+ proof (cases x);
+ case PrimT;
+ with * x;
+ show ?thesis; by (auto simp add: PrimT_PrimT);
next;
- fix ts ts' x xa;
- assume * :
- "(\\<exists>p. ts = PrimT p \\<and> ts' = PrimT p) \\<or> (\\<exists>r. ts = RefT r) \\<and> (\\<exists>r'. ts' = RefT r')";
+ case RefT;
+ hence 1: "\\<exists>r. x = RefT r"; by blast;
+
+ have "\\<exists>r'. xa = RefT r'";
+ proof (cases xa);
+ case PrimT;
+ with RefT * x;
+ have "False"; by auto (rule widen_RefT [elimify], auto);
+ thus ?thesis; by blast;
+ qed blast;
- assume x: "G\\<turnstile>x\\<preceq>ts" "G\\<turnstile>xa\\<preceq>ts'";
-
- show "(\\<exists>p. x = PrimT p \\<and> xa = PrimT p) \\<or> (\\<exists>r. x = RefT r) \\<and> (\\<exists>r'. xa = RefT r')";
- proof (cases x);
- case PrimT;
- with * x;
- show ?thesis; by (auto simp add: PrimT_PrimT);
- next;
- case RefT;
- hence 1: "\\<exists>r. x = RefT r"; by blast;
-
- have "\\<exists>r'. xa = RefT r'";
- proof (cases xa);
- case PrimT;
- with RefT * x;
- have "False"; by auto (rule widen_RefT [elimify], auto);
- thus ?thesis; by blast;
- qed blast;
-
- with 1;
- show ?thesis; by blast;
- qed;
- qed;
- qed;
- qed;
-qed;
+ with 1
+ show ?thesis by blast
+ qed
+ qed
+ qed (elim, clarsimp_tac simp add: sup_state_Cons1 sup_state_Cons2 PrimT_PrimT)+
+qed
lemma wtl_inst_last_mono:
"\\<lbrakk>wtl_inst i G rT s1 s1' cert (Suc pc) pc; G \\<turnstile> s2 <=s s1\\<rbrakk> \\<Longrightarrow>
@@ -675,48 +621,20 @@
proof -;
assume * : "wtl_inst i G rT s1 s1' cert (Suc pc) pc" "G \\<turnstile> s2 <=s s1";
- show ?thesis;
- proof (cases i);
- case LS; with *;
- show ?thesis; by - (cases load_and_store, simp+);
- next;
- case CO; with *;
- show ?thesis; by - (cases create_object, simp);
- next;
- case MO; with *;
- show ?thesis; by - (cases manipulate_object, simp+);
- next;
- case CH; with *;
- show ?thesis; by - (cases check_object, simp);
- next;
- case MI; with *;
- show ?thesis; by - (cases meth_inv, simp);
- next;
- case OS; with *;
- show ?thesis; by - (cases op_stack, simp+);
- next;
- case MR;
- show ?thesis;
- proof (cases meth_ret);
- case Return; with MR *;
- show ?thesis;
- by (clarsimp_tac simp del: split_paired_Ex simp add: sup_state_Cons2)
- (rule widen_trans, blast+);
- qed;
- next;
- case BR;
- show ?thesis;
- proof (cases branch);
- case Ifcmpeq; with BR *;
- show ?thesis; by simp;
- next;
- case Goto; with BR *;
- show ?thesis;
+ show ?thesis
+ proof (cases i, insert *)
+ case Return with *
+ show ?thesis
+ by (clarsimp_tac simp del: split_paired_Ex simp add: sup_state_Cons2)
+ (rule widen_trans, blast+);
+ next
+ case Goto with *
+ show ?thesis
by (clarsimp_tac simp del: split_paired_Ex simp add: sup_state_Cons2)
(rule sup_state_trans, blast+);
- qed;
- qed;
-qed;
+ qed auto
+qed
+
lemma wtl_option_last_mono:
"\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; mpc = Suc pc; G \\<turnstile> s2 <=s s1\\<rbrakk> \\<Longrightarrow>
@@ -753,108 +671,82 @@
"\\<lbrakk>wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
pc < length ins; length ins = max_pc\\<rbrakk> \\<Longrightarrow>
\\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
-proof -;
+proof -
assume * : "wt_instr (ins!pc) G rT phi max_pc pc" "fits ins cert phi"
- "pc < length ins" "length ins = max_pc";
+ "pc < length ins" "length ins = max_pc"
+
+ have xy: "\\<exists> x y. phi!pc = (x,y)" by simp
- have xy: "\\<exists> x y. phi!pc = (x,y)"; by simp;
-
- show ?thesis;
- proof (cases "ins!pc");
- case LS; with * xy;
+ show ?thesis
+ proof (cases "ins!pc", insert *, insert xy);
+ case Return with * xy
+ show ?thesis
+ by (elim, clarsimp_tac simp add: fits_def contains_dead_def simp del: split_paired_Ex);
+ next
+ case Goto with * xy
+ show ?thesis;
+ by (clarsimp_tac simp add: fits_def contains_dead_def contains_targets_def simp del: split_paired_Ex);
+ next
+ case Ifcmpeq with * xy
show ?thesis;
- by - (cases load_and_store, (elim, force simp add: wt_instr_def)+);
- next;
- case CO; with * xy;
- show ?thesis;
- by - (cases create_object, (elim, force simp add: wt_instr_def)+);
- next;
- case MO; with * xy;
- show ?thesis;
- by - (cases manipulate_object, (elim, force simp add: wt_instr_def)+);
- next;
- case CH; with * xy;
- show ?thesis;
- by - (cases check_object, (elim, force simp add: wt_instr_def)+);
- next;
- case OS; with * xy;
- show ?thesis;
- by - (cases op_stack, (elim, force simp add: wt_instr_def)+);
- next;
- case MR; with * xy;
- show ?thesis;
- by - (cases meth_ret, elim,
- clarsimp_tac simp add: wt_instr_def fits_def contains_dead_def simp del: split_paired_Ex);
- next;
- case BR; with * xy;
- show ?thesis;
- by - (cases branch,
- (clarsimp_tac simp add: wt_instr_def fits_def contains_dead_def contains_targets_def
- simp del: split_paired_Ex)+);
- next;
- case MI;
- show ?thesis;
- proof (cases meth_inv);
- case Invoke;
- with MI * xy;
- show ?thesis;
- proof (elim, clarsimp_tac simp add: wt_instr_def simp del: split_paired_Ex);
- fix y apTs X ST';
- assume pc : "Suc pc < length ins";
- assume phi : "phi ! pc = (rev apTs @ X # ST', y)" "length apTs = length list";
- assume ** :
- "X = NT \\<or> (\\<exists>C. X = Class C \\<and>
- (\\<forall>x\\<in>set (zip apTs list). x \\<in> widen G) \\<and>
- (\\<exists>D rT. (\\<exists>b. method (G, C) (mname, list) = Some (D, rT, b)) \\<and> G \\<turnstile> (rT # ST', y) <=s phi ! Suc pc))"
- (is "?NT \\<or> ?CL");
+ by (clarsimp_tac simp add: fits_def contains_dead_def contains_targets_def simp del: split_paired_Ex);
+ next
+ case Invoke with * xy
+ show ?thesis
+ proof (elim, clarsimp_tac simp del: split_paired_Ex)
+ fix y apTs X ST';
+ assume pc : "Suc pc < length ins";
+ assume phi : "phi ! pc = (rev apTs @ X # ST', y)" "length apTs = length list";
+ assume ** :
+ "X = NT \\<or> (\\<exists>C. X = Class C \\<and>
+ (\\<forall>x\\<in>set (zip apTs list). x \\<in> widen G) \\<and>
+ (\\<exists>D rT. (\\<exists>b. method (G, C) (mname, list) = Some (D, rT, b)) \\<and> G \\<turnstile> (rT # ST', y) <=s phi ! Suc pc))"
+ (is "?NT \\<or> ?CL");
+
+ from Invoke pc *;
+ have cert: "cert ! Suc pc = Some (phi ! Suc pc)"; by (clarsimp_tac simp add: fits_def contains_dead_def);
-
- from MI Invoke pc *;
- have cert: "cert ! Suc pc = Some (phi ! Suc pc)"; by (clarsimp_tac simp add: fits_def contains_dead_def);
-
-
- show "\\<exists>s. (\\<exists>apTsa Xa ST'a.
- rev apTs @ X # ST' = rev apTsa @ Xa # ST'a \\<and>
- length apTsa = length list \\<and>
+ show "\\<exists>s. (\\<exists>apTsa Xa ST'a.
+ rev apTs @ X # ST' = rev apTsa @ Xa # ST'a \\<and>
+ length apTsa = length list \\<and>
(\\<exists>s''. cert ! Suc pc = Some s'' \\<and>
(s'' = s \\<and> Xa = NT \\<or>
G \\<turnstile> s <=s s'' \\<and>
(\\<exists>C. Xa = Class C \\<and>
(\\<forall>x\\<in>set (zip apTsa list). x \\<in> widen G) \\<and>
(\\<exists>D rT. (\\<exists>b. method (G, C) (mname, list) = Some (D, rT, b)) \\<and> (rT # ST'a, y) = s))))) \\<and>
- G \\<turnstile> s <=s phi ! Suc pc" (is "\\<exists>s. ?P s");
- proof (cases "X=NT");
- case True;
- with cert phi **;
- have "?P (phi ! Suc pc)"; by (force simp del: split_paired_Ex);
- thus ?thesis; by blast;
- next;
- case False;
- with **;
+ G \\<turnstile> s <=s phi ! Suc pc" (is "\\<exists>s. ?P s");
+ proof (cases "X=NT");
+ case True
+ with cert phi **
+ have "?P (phi ! Suc pc)" by (force simp del: split_paired_Ex)
+ thus ?thesis by blast
+ next
+ case False
+ with **
- have "?CL"; by simp;
+ have "?CL" by simp
- thus ?thesis;
- proof (elim exE conjE);
- fix C D rT b;
- assume "X = Class C" "\\<forall>x\\<in>set (zip apTs list). x \\<in> widen G"
- "G \\<turnstile> (rT # ST', y) <=s phi ! Suc pc"
- "method (G, C) (mname, list) = Some (D, rT, b)";
- with cert phi;
- have "?P (rT #ST', y)"; by (force simp del: split_paired_Ex);
- thus ?thesis; by blast;
- qed;
- qed;
- qed;
- qed;
- qed;
-qed;
+ thus ?thesis
+ proof (elim exE conjE);
+ fix C D rT b;
+ assume "X = Class C" "\\<forall>x\\<in>set (zip apTs list). x \\<in> widen G"
+ "G \\<turnstile> (rT # ST', y) <=s phi ! Suc pc"
+ "method (G, C) (mname, list) = Some (D, rT, b)";
+ with cert phi;
+ have "?P (rT #ST', y)" by (force simp del: split_paired_Ex)
+ thus ?thesis by blast
+ qed
+ qed
+ qed
+ qed (elim, force)+
+qed
lemma wt_instr_imp_wtl_option:
"\\<lbrakk>fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc; max_pc = length ins\\<rbrakk> \\<Longrightarrow>
\\<exists> s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
-proof -;
+proof -
assume fits : "fits ins cert phi" "pc < length ins"
and "wt_instr (ins!pc) G rT phi max_pc pc"
"max_pc = length ins";
@@ -881,6 +773,7 @@
qed;
qed;
+
lemma wtl_option_pseudo_mono:
"\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins;
wf_prog wf_mb G; G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow>
@@ -914,7 +807,7 @@
with Some G;
show ?thesis; by (simp add: wtl_inst_option_def);
- qed;
+ qed
qed;
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Mon Jul 17 13:59:10 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Mon Jul 17 14:00:53 2000 +0200
@@ -271,72 +271,18 @@
by (rule wtl_suc_pc [rulify]);
show ?thesis;
- proof (cases "i");
- case LS;
- with wo suc;
- show ?thesis;
- by - (cases "load_and_store",
- (cases "cert ! (length i1)",
- clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
- clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def)+);
- next;
- case CO;
- with wo suc;
- show ?thesis;
- by - (cases "create_object" ,
- cases "cert ! (length i1)",
- clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
- clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def);
- next;
- case MO;
- with wo suc;
- show ?thesis;
- by - (cases "manipulate_object" ,
- (cases "cert ! (length i1)",
- clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
- clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def)+);
- next;
- case CH;
- with wo suc;
- show ?thesis;
- by - (cases "check_object" , cases "cert ! (length i1)",
- clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
- clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def);
- next;
- case MI;
- with wo suc;
- show ?thesis;
- by - (cases "meth_inv", cases "cert ! (length i1)",
- clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
- intro exI conjI, rule refl, simp, force,
- clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def,
- intro exI conjI, rule refl, simp, force);
- next;
- case MR;
- with wo suc;
- show ?thesis;
- by - (cases "meth_ret" , cases "cert ! (length i1)",
- clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
- clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def);
- next;
- case OS;
- with wo suc;
- show ?thesis;
- by - (cases "op_stack" ,
- (cases "cert ! (length i1)",
- clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
- clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def)+);
- next;
- case BR;
- with wo suc;
- show ?thesis;
- by - (cases "branch",
- (cases "cert ! (length i1)",
- clarsimp_tac simp add: c2 c3 wt_instr_def wtl_inst_option_def split_beta,
- clarsimp_tac simp add: c1 c3 wt_instr_def wtl_inst_option_def)+);
- qed;
+ proof (cases i, insert suc, insert wo);
+ case Invoke with suc wo
+ show ?thesis
+ by - (cases "cert ! (length i1)",
+ clarsimp_tac simp add: c2 wtl_inst_option_def split_beta,
+ intro exI conjI, blast, simp, force,
+ clarsimp_tac simp add: c1 wtl_inst_option_def,
+ intro exI conjI, blast, simp, force)
+ qed (clarsimp_tac simp add: c1 c2 c3 wtl_inst_option_def split_beta split: option.split_asm)+
qed;
+
lemma wtl_fits_wt:
"\\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\\<rbrakk>
\\<Longrightarrow> \\<forall>pc. pc < length is \\<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc";
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Mon Jul 17 13:59:10 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Mon Jul 17 14:00:53 2000 +0200
@@ -14,10 +14,12 @@
class_certificate = "sig \\<Rightarrow> certificate"
prog_certificate = "cname \\<Rightarrow> class_certificate"
+
consts
- wtl_LS :: "[load_and_store,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
+wtl_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
+
primrec
-"wtl_LS (Load idx) s s' max_pc pc =
+"wtl_inst (Load idx) G rT s s' cert max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
@@ -25,7 +27,7 @@
(\\<exists>ts. (LT ! idx) = Some ts \\<and>
(ts # ST , LT) = s'))"
-"wtl_LS (Store idx) s s' max_pc pc =
+"wtl_inst (Store idx) G rT s s' cert max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
@@ -33,22 +35,19 @@
(\\<exists>ts ST'. ST = ts # ST' \\<and>
(ST' , LT[idx:=Some ts]) = s'))"
-"wtl_LS (Bipush i) s s' max_pc pc =
+"wtl_inst (Bipush i) G rT s s' cert max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
((PrimT Integer) # ST , LT) = s')"
-"wtl_LS (Aconst_null) s s' max_pc pc =
+"wtl_inst (Aconst_null) G rT s s' cert max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
(NT # ST , LT) = s')"
-consts
- wtl_MO :: "[manipulate_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
-primrec
-"wtl_MO (Getfield F C) G s s' max_pc pc =
+"wtl_inst (Getfield F C) G rT s s' cert max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
@@ -58,7 +57,7 @@
G \\<turnstile> oT \\<preceq> (Class C) \\<and>
(T # ST' , LT) = s'))"
-"wtl_MO (Putfield F C) G s s' max_pc pc =
+"wtl_inst (Putfield F C) G rT s s' cert max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
@@ -70,21 +69,14 @@
G \\<turnstile> vT \\<preceq> T \\<and>
(ST' , LT) = s'))"
-
-consts
- wtl_CO :: "[create_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
-primrec
-"wtl_CO (New C) G s s' max_pc pc =
+"wtl_inst (New C) G rT s s' cert max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
is_class G C \\<and>
((Class C) # ST , LT) = s')"
-consts
- wtl_CH :: "[check_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
-primrec
-"wtl_CH (Checkcast C) G s s' max_pc pc =
+"wtl_inst (Checkcast C) G rT s s' cert max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
@@ -92,54 +84,50 @@
(\\<exists>rt ST'. ST = RefT rt # ST' \\<and>
(Class C # ST' , LT) = s'))"
-consts
- wtl_OS :: "[op_stack,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
-primrec
-"wtl_OS Pop s s' max_pc pc =
+"wtl_inst Pop G rT s s' cert max_pc pc =
(let (ST,LT) = s
in
\\<exists>ts ST'. pc+1 < max_pc \\<and>
ST = ts # ST' \\<and>
(ST' , LT) = s')"
-"wtl_OS Dup s s' max_pc pc =
+"wtl_inst Dup G rT s s' cert max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
(\\<exists>ts ST'. ST = ts # ST' \\<and>
(ts # ts # ST' , LT) = s'))"
-"wtl_OS Dup_x1 s s' max_pc pc =
+"wtl_inst Dup_x1 G rT s s' cert max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
(\\<exists>ts1 ts2 ST'. ST = ts1 # ts2 # ST' \\<and>
(ts1 # ts2 # ts1 # ST' , LT) = s'))"
-"wtl_OS Dup_x2 s s' max_pc pc =
+"wtl_inst Dup_x2 G rT s s' cert max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
(\\<exists>ts1 ts2 ts3 ST'. ST = ts1 # ts2 # ts3 # ST' \\<and>
(ts1 # ts2 # ts3 # ts1 # ST' , LT) = s'))"
-"wtl_OS Swap s s' max_pc pc =
+"wtl_inst Swap G rT s s' cert max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
(\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and>
(ts # ts' # ST' , LT) = s'))"
-"wtl_OS IAdd s s' max_pc pc =
+"wtl_inst IAdd G rT s s' cert max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
(\\<exists>ST'. ST = (PrimT Integer) # (PrimT Integer) # ST' \\<and>
((PrimT Integer) # ST' , LT) = s'))"
-consts
- wtl_BR :: "[branch,jvm_prog,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
-primrec
-"wtl_BR (Ifcmpeq branch) G s s' cert max_pc pc =
+
+
+"wtl_inst (Ifcmpeq branch) G rT s s' cert max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and> (nat(int pc+branch)) < max_pc \\<and>
@@ -148,19 +136,16 @@
(\\<exists>r r'. ts = RefT r \\<and> ts' = RefT r')) \\<and>
((ST' , LT) = s') \\<and>
cert ! (nat(int pc+branch)) \\<noteq> None \\<and>
- G \\<turnstile> (ST' , LT) <=s the (cert ! (nat(int pc+branch)))))"
+ G \\<turnstile> (ST' , LT) <=s the (cert ! (nat(int pc+branch)))))"
-"wtl_BR (Goto branch) G s s' cert max_pc pc =
+"wtl_inst (Goto branch) G rT s s' cert max_pc pc =
((let (ST,LT) = s
in
(nat(int pc+branch)) < max_pc \\<and> cert ! (nat(int pc+branch)) \\<noteq> None \\<and>
G \\<turnstile> (ST , LT) <=s the (cert ! (nat(int pc+branch)))) \\<and>
(cert ! (pc+1) = Some s'))"
-
-consts
- wtl_MI :: "[meth_inv,jvm_prog,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
-primrec
-"wtl_MI (Invoke mn fpTs) G s s' cert max_pc pc =
+
+"wtl_inst (Invoke mn fpTs) G rT s s' cert max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
@@ -173,29 +158,13 @@
(\\<exists>D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
(rT # ST' , LT) = s')))))))"
-consts
- wtl_MR :: "[meth_ret,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
-primrec
- "wtl_MR Return G rT s s' cert max_pc pc =
+"wtl_inst Return G rT s s' cert max_pc pc =
((let (ST,LT) = s
in
(\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT)) \\<and>
(cert ! (pc+1) = Some s'))"
-consts
- wtl_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
- primrec
- "wtl_inst (LS ins) G rT s s' cert max_pc pc = wtl_LS ins s s' max_pc pc"
- "wtl_inst (CO ins) G rT s s' cert max_pc pc = wtl_CO ins G s s' max_pc pc"
- "wtl_inst (MO ins) G rT s s' cert max_pc pc = wtl_MO ins G s s' max_pc pc"
- "wtl_inst (CH ins) G rT s s' cert max_pc pc = wtl_CH ins G s s' max_pc pc"
- "wtl_inst (MI ins) G rT s s' cert max_pc pc = wtl_MI ins G s s' cert max_pc pc"
- "wtl_inst (MR ins) G rT s s' cert max_pc pc = wtl_MR ins G rT s s' cert max_pc pc"
- "wtl_inst (OS ins) G rT s s' cert max_pc pc = wtl_OS ins s s' max_pc pc"
- "wtl_inst (BR ins) G rT s s' cert max_pc pc = wtl_BR ins G s s' cert max_pc pc"
-
-
constdefs
wtl_inst_option :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
"wtl_inst_option i G rT s0 s1 cert max_pc pc \\<equiv>
@@ -237,32 +206,16 @@
"wtl_inst i G rT s0 s1 cert max_pc pc \\<longrightarrow>
wtl_inst i G rT s0 s1' cert max_pc pc \\<longrightarrow> s1 = s1'" (is "?P i")
proof (induct i)
-case LS
- show "?P (LS load_and_store)" by (induct load_and_store) auto
-case CO
- show "?P (CO create_object)" by (induct create_object) auto
-case MO
- show "?P (MO manipulate_object)" by (induct manipulate_object) auto
-case CH
- show "?P (CH check_object)" by (induct check_object) auto
-case MI
- show "?P (MI meth_inv)" proof (induct meth_inv)
- case Invoke
+case Invoke
have "\\<exists>x y. s0 = (x,y)" by (simp)
- thus "wtl_inst (MI (Invoke mname list)) G rT s0 s1 cert max_pc pc \\<longrightarrow>
- wtl_inst (MI (Invoke mname list)) G rT s0 s1' cert max_pc pc \\<longrightarrow>
+ thus "wtl_inst (Invoke mname list) G rT s0 s1 cert max_pc pc \\<longrightarrow>
+ wtl_inst (Invoke mname list) G rT s0 s1' cert max_pc pc \\<longrightarrow>
s1 = s1'"
proof elim
apply_end(clarsimp_tac, drule rev_eq, assumption+)
qed auto
- qed
-case MR
- show "?P (MR meth_ret)" by (induct meth_ret) auto
-case OS
- show "?P (OS op_stack)" by (induct op_stack) auto
-case BR
- show "?P (BR branch)" by (induct branch) auto
-qed
+qed auto
+
lemma wtl_inst_option_unique:
"\\<lbrakk>wtl_inst_option i G rT s0 s1 cert max_pc pc;
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Mon Jul 17 13:59:10 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Mon Jul 17 14:00:53 2000 +0200
@@ -6,62 +6,22 @@
Execution of the JVM
*)
-JVMExec = LoadAndStore + Object + Method + Opstack + Control +
-
-datatype
- instr = LS load_and_store
- | CO create_object
- | MO manipulate_object
- | CH check_object
- | MI meth_inv
- | MR meth_ret
- | OS op_stack
- | BR branch
-
-types
- bytecode = instr list
- jvm_prog = "(nat \\<times> bytecode)prog"
+JVMExec = JVMExecInstr +
consts
exec :: "jvm_prog \\<times> jvm_state \\<Rightarrow> jvm_state option"
-(** exec is not recursive. recdef is just used because for pattern matching **)
+(** exec is not recursive. recdef is just used for pattern matching **)
recdef exec "{}"
"exec (G, xp, hp, []) = None"
"exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
- Some (case snd(snd(snd(the(method (G,C) sig)))) ! pc of
- LS ins \\<Rightarrow> let (stk',loc',pc') = exec_las ins stk loc pc
- in
- (None,hp,(stk',loc',C,sig,pc')#frs)
-
- | CO ins \\<Rightarrow> let (xp',hp',stk',pc') = exec_co ins G hp stk pc
- in
- (xp',hp',(stk',loc,C,sig,pc')#frs)
-
- | MO ins \\<Rightarrow> let (xp',hp',stk',pc') = exec_mo ins hp stk pc
- in
- (xp',hp',(stk',loc,C,sig,pc')#frs)
+ (let
+ i = snd(snd(snd(the(method (G,C) sig)))) ! pc
+ in
+ Some (exec_instr i G hp stk loc C sig pc frs))"
- | CH ins \\<Rightarrow> let (xp',stk',pc') = exec_ch ins G hp stk pc
- in
- (xp',hp,(stk',loc,C,sig,pc')#frs)
-
- | MI ins \\<Rightarrow> let (xp',frs',stk',pc') = exec_mi ins G hp stk pc
- in
- (xp',hp,frs'@(stk',loc,C,sig,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
- in
- (None,hp,(stk',loc,C,sig,pc')#frs)
-
- | BR ins \\<Rightarrow> let (stk',pc') = exec_br ins stk pc
- in
- (None,hp,(stk',loc,C,sig,pc')#frs))"
-
- "exec (G, Some xp, hp, frs) = None"
+ "exec (G, Some xp, hp, frs) = None"
constdefs
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Mon Jul 17 14:00:53 2000 +0200
@@ -0,0 +1,112 @@
+(* Title: HOL/MicroJava/JVM/JVMExecInstr.thy
+ ID: $Id$
+ Author: Cornelia Pusch, Gerwin Klein
+ Copyright 1999 Technische Universitaet Muenchen
+
+Semantics of JVM instructions
+*)
+
+JVMExecInstr = JVMInstructions + JVMState +
+
+consts
+exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] \\<Rightarrow> jvm_state"
+primrec
+ "exec_instr (Load idx) G hp stk vars Cl sig pc frs =
+ (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)"
+
+ "exec_instr (Store idx) G hp stk vars Cl sig pc frs =
+ (None, hp, (tl stk, vars[idx:=hd stk], Cl, sig, pc+1)#frs)"
+
+ "exec_instr (Bipush ival) G hp stk vars Cl sig pc frs =
+ (None, hp, (Intg ival # stk, vars, Cl, sig, pc+1)#frs)"
+
+ "exec_instr Aconst_null G hp stk vars Cl sig pc frs =
+ (None, hp, (Null # stk, vars, Cl, sig, pc+1)#frs)"
+
+ "exec_instr (New C) G hp stk vars Cl sig pc frs =
+ (let xp' = raise_xcpt (\\<forall>x. hp x \\<noteq> None) OutOfMemory;
+ oref = newref hp;
+ fs = init_vars (fields(G,C));
+ 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', vars, Cl, sig, pc+1)#frs))"
+
+ "exec_instr (Getfield F C) G hp stk vars Cl sig pc frs =
+ (let oref = hd stk;
+ xp' = raise_xcpt (oref=Null) NullPointer;
+ (oc,fs) = the(hp(the_Addr oref));
+ stk' = if xp'=None then the(fs(F,C))#(tl stk) else tl stk
+ in
+ (xp', hp, (stk', vars, Cl, sig, pc+1)#frs))"
+
+ "exec_instr (Putfield F C) G hp stk vars Cl sig pc frs =
+ (let (fval,oref)= (hd stk, hd(tl stk));
+ xp' = raise_xcpt (oref=Null) NullPointer;
+ a = the_Addr oref;
+ (oc,fs) = the(hp a);
+ hp' = if xp'=None then hp(a \\<mapsto> (oc, fs((F,C) \\<mapsto> fval))) else hp
+ in
+ (xp', hp', (tl (tl stk), vars, Cl, sig, pc+1)#frs))"
+
+ "exec_instr (Checkcast C) G hp stk vars Cl sig pc frs =
+ (let oref = hd stk;
+ xp' = raise_xcpt (\\<not> cast_ok G C hp oref) ClassCast;
+ stk' = if xp'=None then stk else tl stk
+ in
+ (xp', hp, (stk', vars, Cl, sig, pc+1)#frs))"
+
+ "exec_instr (Invoke mn ps) G hp stk vars Cl sig pc frs =
+ (let n = length ps;
+ argsoref = take (n+1) stk;
+ oref = last argsoref;
+ xp' = raise_xcpt (oref=Null) NullPointer;
+ dynT = fst(the(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', hp, frs'@(drop (n+1) stk, vars, Cl, sig, pc+1)#frs))"
+
+ "exec_instr Return G hp stk0 vars Cl sig0 pc frs =
+ (if frs=[] then
+ (None, hp, [])
+ else
+ let val = hd stk0; (stk,loc,C,sig,pc) = hd frs
+ in
+ (None, hp, (val#stk,loc,C,sig,pc)#tl frs))"
+
+ "exec_instr Pop G hp stk vars Cl sig pc frs =
+ (None, hp, (tl stk, vars, Cl, sig, pc+1)#frs)"
+
+ "exec_instr Dup G hp stk vars Cl sig pc frs =
+ (None, hp, (hd stk # stk, vars, Cl, sig, pc+1)#frs)"
+
+ "exec_instr Dup_x1 G hp stk vars Cl sig pc frs =
+ (None, hp, (hd stk # hd (tl stk) # hd stk # (tl (tl stk)), vars, Cl, sig, pc+1)#frs)"
+
+ "exec_instr Dup_x2 G hp stk vars Cl sig pc frs =
+ (None, hp, (hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))),
+ vars, Cl, sig, pc+1)#frs)"
+
+ "exec_instr Swap G hp stk vars Cl sig pc frs =
+ (let (val1,val2) = (hd stk,hd (tl stk))
+ in
+ (None, hp, (val2#val1#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))"
+
+ "exec_instr IAdd G hp stk vars Cl sig pc frs =
+ (let (val1,val2) = (hd stk,hd (tl stk))
+ in
+ (None, hp, (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))"
+
+ "exec_instr (Ifcmpeq i) G hp stk vars Cl sig pc frs =
+ (let (val1,val2) = (hd stk, hd (tl stk));
+ pc' = if val1 = val2 then nat(int pc+i) else pc+1
+ in
+ (None, hp, (tl (tl stk), vars, Cl, sig, pc')#frs))"
+
+ "exec_instr (Goto i) G hp stk vars Cl sig pc frs =
+ (None, hp, (stk, vars, Cl, sig, nat(int pc+i))#frs)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Mon Jul 17 14:00:53 2000 +0200
@@ -0,0 +1,36 @@
+(* Title: HOL/MicroJava/JVM/JVMInstructions.thy
+ ID: $Id$
+ Author: Gerwin Klein
+ Copyright 2000 Technische Universitaet Muenchen
+
+Instructions of the JVM
+*)
+
+JVMInstructions = JVMState +
+
+datatype
+ instr = Load nat (* load from local variable *)
+ | Store nat (* store into local variable *)
+ | Bipush int (* push int *)
+ | Aconst_null (* push null *)
+ | New cname (* create object *)
+ | Getfield vname cname (* Fetch field from object *)
+ | Putfield vname cname (* Set field in object *)
+ | Checkcast cname (* Check whether object is of given type *)
+ | Invoke mname "(ty list)" (* inv. instance meth of an object *)
+ | Return
+ | Pop
+ | Dup
+ | Dup_x1
+ | Dup_x2
+ | Swap
+ | IAdd
+ | Goto int
+ | Ifcmpeq int (* Branch if int/ref comparison succeeds *)
+
+
+types
+ bytecode = "instr list"
+ jvm_prog = "(nat \\<times> bytecode) prog"
+
+end