# HG changeset patch # User kleing # Date 962878505 -7200 # Node ID 678e718a5a8649f68f130279e88c9d7820deaec0 # Parent 103acc345f7509ed1c6f4120cbbc495ed13a3765 new ADD instruction diff -r 103acc345f75 -r 678e718a5a86 src/HOL/MicroJava/BV/BVSpec.thy --- 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 @@ (\\ts ts' ST'. ST = ts' # ts # ST' \\ G \\ (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 \\ + (\\ST'. ST = (PrimT Integer) # (PrimT Integer) # ST' \\ + G \\ ((PrimT Integer) # ST' , LT) <=s phi ! (pc+1)))" + + consts wt_BR :: "[branch,jvm_prog,method_type,p_count,p_count] \\ bool" primrec diff -r 103acc345f75 -r 678e718a5a86 src/HOL/MicroJava/BV/BVSpecTypeSafe.ML --- 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 +"\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ +\\\ G,phi \\JVM state'\\"; +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 "\\ 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 **) diff -r 103acc345f75 -r 678e718a5a86 src/HOL/MicroJava/BV/LBVComplete.thy --- 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; diff -r 103acc345f75 -r 678e718a5a86 src/HOL/MicroJava/BV/LBVCorrect.thy --- 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; diff -r 103acc345f75 -r 678e718a5a86 src/HOL/MicroJava/BV/LBVSpec.thy --- 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 @@ (\\ts ts' ST'. ST = ts' # ts # ST' \\ (ts # ts' # ST' , LT) = s'))" +"wtl_OS ADD s s' max_pc pc = + (let (ST,LT) = s + in + pc+1 < max_pc \\ + (\\ST'. ST = (PrimT Integer) # (PrimT Integer) # ST' \\ + ((PrimT Integer) # ST' , LT) = s'))" consts wtl_BR :: "[branch,jvm_prog,state_type,state_type,certificate,p_count,p_count] \\ bool" primrec diff -r 103acc345f75 -r 678e718a5a86 src/HOL/MicroJava/JVM/Opstack.thy --- 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] \\ (opstack \\ 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