new ADD instruction

--- a/src/HOL/MicroJava/BV/BVSpec.thy	Thu Jul 06 11:24:09 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Thu Jul 06 12:15:05 2000 +0200
@@ -129,6 +129,14 @@
 	 (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and> 	 
 		       G \\<turnstile> (ts # ts' # ST' , LT) <=s phi ! (pc+1)))"
 
+"wt_OS ADD G 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

--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Thu Jul 06 11:24:09 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Thu Jul 06 12:15:05 2000 +0200
@@ -510,6 +510,20 @@
 	addss (simpset() addsimps [map_eq_Cons]@defs1)) 1);
 qed "Swap_correct";
 
+
+Goal 
+"\\<lbrakk> wf_prog wt G; \
+\  method (G,C) sig = Some (C,rT,maxl,ins); \
+\  ins ! pc = OS ADD; \
+\  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> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
+by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
+  addss (simpset() addsimps [map_eq_Cons, approx_val_def]@defs1)) 1);
+qed "ADD_correct";
+
+
 Goal
 "\\<lbrakk> wt_jvm_prog G phi; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
@@ -522,7 +536,7 @@
  ba 1;
 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])));
+by (ALLGOALS (fast_tac (claset() addIs [Pop_correct,Dup_correct,Dup_x1_correct,Dup_x2_correct,Swap_correct,ADD_correct])));
 qed "OS_correct";
 
 (** Main **)

--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Jul 06 11:24:09 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Jul 06 12:15:05 2000 +0200
@@ -615,7 +615,7 @@
     case OS;
     with 1 3;
     show ?thesis; 
-      by - (cases op_stack, (elim, clarsimp_tac simp add: sup_state_Cons2)+);
+      by - (cases op_stack, (elim, clarsimp_tac simp add: sup_state_Cons2 PrimT_PrimT)+);
 
   next;
     case BR;

--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Thu Jul 06 11:24:09 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Thu Jul 06 12:15:05 2000 +0200
@@ -138,9 +138,9 @@
   qed;  
   with all; 
   show ?thesis;  
-  proof elim; 
+  proof (elim exE allE impE conjE); 
     show "wtl_inst_list is G rT s0 s2 cert (0+length is) 0"; by simp; 
-  qed (auto simp add: fits_def); 
+  qed (auto simp add: fits_def);  
 qed; 
 
 

--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Jul 06 11:24:09 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Jul 06 12:15:05 2000 +0200
@@ -130,6 +130,12 @@
 	 (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and> 	 
 		       (ts # ts' # ST' , LT) = s'))"
 
+"wtl_OS ADD s s' 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

--- a/src/HOL/MicroJava/JVM/Opstack.thy	Thu Jul 06 11:24:09 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Opstack.thy	Thu Jul 06 12:15:05 2000 +0200
@@ -17,6 +17,7 @@
  | Dup_x1
  | Dup_x2
  | Swap
+ | ADD
 	  
 consts
  exec_os :: "[op_stack,opstack,p_count] \\<Rightarrow> (opstack \\<times> p_count)" 
@@ -35,4 +36,9 @@
 	 in
 	 (val2#val1#(tl (tl stk)) , pc+1))"
 
+  "exec_os ADD stk pc =
+  (let (val1,val2) = (hd stk,hd (tl stk))
+   in
+   (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), pc+1))"
+
 end