--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sun Jan 14 18:17:37 2001 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sun Jan 14 18:19:18 2001 +0100
@@ -59,24 +59,20 @@
done
-lemma conf_Intg_Integer [iff]:
- "G,h \<turnstile> Intg i ::\<preceq> PrimT Integer"
-by (simp add: conf_def)
-
-
-lemma Bipush_correct:
+lemma LitPush_correct:
"[| wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins);
- ins!pc = Bipush i;
+ ins!pc = LitPush v;
wt_instr (ins!pc) G rT (phi C sig) maxs (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> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons)
-apply (blast intro: approx_stk_imp_approx_stk_sup
+apply (blast dest: conf_litval intro: conf_widen approx_stk_imp_approx_stk_sup
approx_loc_imp_approx_loc_sup)
done
+
lemma NT_subtype_conv:
"G \<turnstile> NT \<preceq> T = (T=NT \<or> (\<exists>C. T = Class C))"
proof -
@@ -92,21 +88,6 @@
by (force intro: null dest: l)
qed
-lemma Aconst_null_correct:
-"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
- ins!pc = Aconst_null;
- wt_instr (ins!pc) G rT (phi C sig) maxs (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> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 map_eq_Cons)
-apply (rule conjI)
- apply (force simp add: approx_val_Null NT_subtype_conv)
-apply (blast intro: approx_stk_imp_approx_stk_sup
- approx_loc_imp_approx_loc_sup)
-done
-
lemma Cast_conf2:
"[| wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v;
@@ -118,7 +99,7 @@
apply (simp add: null)
apply (clarsimp simp add: conf_def obj_ty_def)
apply (cases v)
-apply (auto intro: null rtrancl_trans)
+apply (auto intro: rtrancl_trans)
done
@@ -605,16 +586,15 @@
apply (frule wt_jvm_prog_impl_wt_instr_cor)
apply assumption+
apply (cases "ins!pc")
-prefer 9
+prefer 8
apply (rule Invoke_correct, assumption+)
-prefer 9
+prefer 8
apply (rule Return_correct, assumption+)
apply (unfold wt_jvm_prog_def)
apply (rule Load_correct, assumption+)
apply (rule Store_correct, assumption+)
-apply (rule Bipush_correct, assumption+)
-apply (rule Aconst_null_correct, assumption+)
+apply (rule LitPush_correct, assumption+)
apply (rule New_correct, assumption+)
apply (rule Getfield_correct, assumption+)
apply (rule Putfield_correct, assumption+)
--- a/src/HOL/MicroJava/BV/JVM.thy Sun Jan 14 18:17:37 2001 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy Sun Jan 14 18:19:18 2001 +0100
@@ -50,7 +50,6 @@
apply fastsimp
apply fastsimp
apply fastsimp
- apply fastsimp
apply clarsimp
defer
apply fastsimp
--- a/src/HOL/MicroJava/BV/Step.thy Sun Jan 14 18:17:37 2001 +0100
+++ b/src/HOL/MicroJava/BV/Step.thy Sun Jan 14 18:19:18 2001 +0100
@@ -17,8 +17,7 @@
recdef step' "{}"
"step' (Load idx, G, (ST, LT)) = (ok_val (LT ! idx) # ST, LT)"
"step' (Store idx, G, (ts#ST, LT)) = (ST, LT[idx:= OK ts])"
-"step' (Bipush i, G, (ST, LT)) = (PrimT Integer # ST, LT)"
-"step' (Aconst_null, G, (ST, LT)) = (NT#ST,LT)"
+"step' (LitPush v, G, (ST, LT)) = (the (typeof (\<lambda>v. None) v) # ST, LT)"
"step' (Getfield F C, G, (oT#ST, LT)) = (snd (the (field (G,C) F)) # ST, LT)"
"step' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)"
"step' (New C, G, (ST,LT)) = (Class C # ST, LT)"
@@ -52,9 +51,8 @@
(snd s) ! idx \<noteq> Err \<and>
maxs < length (fst s))"
"app' (Store idx, G, maxs, rT, (ts#ST, LT)) = (idx < length LT)"
-"app' (Bipush i, G, maxs, rT, s) = (maxs < length (fst s))"
-"app' (Aconst_null, G, maxs, rT, s) = (maxs < length (fst s))"
-"app' (Getfield F C, G, maxs, rT, (oT#ST, LT)) = (is_class G C \<and>
+"app' (LitPush v, G, maxs, rT, s) = (maxs < length (fst s) \<and> typeof (\<lambda>t. None) v \<noteq> None)"
+"app' (Getfield F C, G, maxs, rT, (oT#ST, LT)) = (is_class G C \<and>
field (G,C) F \<noteq> None \<and>
fst (the (field (G,C) F)) = C \<and>
G \<turnstile> oT \<preceq> (Class C))"
@@ -99,8 +97,7 @@
primrec
"succs (Load idx) pc = [pc+1]"
"succs (Store idx) pc = [pc+1]"
-"succs (Bipush i) pc = [pc+1]"
-"succs (Aconst_null) pc = [pc+1]"
+"succs (LitPush v) pc = [pc+1]"
"succs (Getfield F C) pc = [pc+1]"
"succs (Putfield F C) pc = [pc+1]"
"succs (New C) pc = [pc+1]"
@@ -157,13 +154,9 @@
"(app (Store idx) G maxs rT (Some s)) = (\<exists> ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
-lemma appBipush[simp]:
-"(app (Bipush i) G maxs rT (Some s)) = (maxs < length (fst s))"
- by (simp add: app_def)
-
-lemma appAconst[simp]:
-"(app Aconst_null G maxs rT (Some s)) = (maxs < length (fst s))"
- by (simp add: app_def)
+lemma appLitPush[simp]:
+"(app (LitPush v) G maxs rT (Some s)) = (maxs < length (fst s) \<and> typeof (\<lambda>v. None) v \<noteq> None)"
+ by (cases s, simp add: app_def)
lemma appGetField[simp]:
"(app (Getfield F C) G maxs rT (Some s)) =
@@ -283,10 +276,15 @@
hence "\<exists>apTs X ST. a = rev apTs @ X # ST \<and> length apTs = length fpTs"
by blast
with app
- show ?thesis by (auto simp add: app_def) blast
+ show ?thesis
+ by (unfold app_def, clarsimp) blast
qed
- with Pair have "?app s ==> ?P s" by simp
- thus ?thesis by (auto simp add: app_def)
+ with Pair
+ have "?app s ==> ?P s" by simp
+ moreover
+ have "?P s \<Longrightarrow> ?app s" by (unfold app_def) clarsimp
+ ultimately
+ show ?thesis by blast
qed
lemma step_Some:
--- a/src/HOL/MicroJava/BV/StepMono.thy Sun Jan 14 18:17:37 2001 +0100
+++ b/src/HOL/MicroJava/BV/StepMono.thy Sun Jan 14 18:19:18 2001 +0100
@@ -143,11 +143,7 @@
by - (cases s2, auto simp add: map_eq_Cons sup_loc_Cons2
sup_loc_length sup_state_conv)
next
- case Bipush
- with G app
- show ?thesis by simp
- next
- case Aconst_null
+ case LitPush
with G app
show ?thesis by simp
next
@@ -355,7 +351,7 @@
show ?thesis
by (clarsimp simp add: sup_state_conv sup_loc_update)
next
- case Bipush
+ case LitPush
with G s step app1 app2
show ?thesis
by (clarsimp simp add: sup_state_Cons1)
@@ -365,11 +361,6 @@
show ?thesis
by (clarsimp simp add: sup_state_Cons1)
next
- case Aconst_null
- with G s step app1 app2
- show ?thesis
- by (clarsimp simp add: sup_state_Cons1)
- next
case Getfield
with G s step app1 app2
show ?thesis
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Sun Jan 14 18:17:37 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Sun Jan 14 18:19:18 2001 +0100
@@ -21,16 +21,13 @@
"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 (LitPush v) G hp stk vars Cl sig pc frs =
+ (None, hp, (v # 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));
+ 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
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Sun Jan 14 18:17:37 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Sun Jan 14 18:19:18 2001 +0100
@@ -13,8 +13,7 @@
datatype
instr = Load nat (* load from local variable *)
| Store nat (* store into local variable *)
- | Bipush int (* push int *)
- | Aconst_null (* push null *)
+ | LitPush val (* push a literal (constant) *)
| New cname (* create object *)
| Getfield vname cname (* Fetch field from object *)
| Putfield vname cname (* Set field in object *)