# HG changeset patch
# User kleing
# Date 979492758 -3600
# Node ID 697fab84709e6d8614b7bf3b38d2fc2231deda71
# Parent  23386a5b63eb12022cbe6fe4027503ef989b48e3
removed instructions Aconst_null+Bipush, introduced LitPush

diff -r 23386a5b63eb -r 697fab84709e src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- 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+)
diff -r 23386a5b63eb -r 697fab84709e src/HOL/MicroJava/BV/JVM.thy
--- 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
diff -r 23386a5b63eb -r 697fab84709e src/HOL/MicroJava/BV/Step.thy
--- 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:
diff -r 23386a5b63eb -r 697fab84709e src/HOL/MicroJava/BV/StepMono.thy
--- 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
diff -r 23386a5b63eb -r 697fab84709e src/HOL/MicroJava/JVM/JVMExecInstr.thy
--- 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 
diff -r 23386a5b63eb -r 697fab84709e src/HOL/MicroJava/JVM/JVMInstructions.thy
--- 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     *)