# HG changeset patch # User kleing # Date 963835253 -7200 # Node ID c32c5696ec2a65767670412522def1439c336e2d # Parent cc0fd5226bb70ce0e54ae1ec672a633a41f167f3 flat instruction set diff -r cc0fd5226bb7 -r c32c5696ec2a src/HOL/MicroJava/BV/BVSpec.thy --- 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 \\ class_type" consts - wt_LS :: "[load_and_store,jvm_prog,method_type,p_count,p_count] \\ bool" +wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count] \\ 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 \\ @@ -24,7 +25,7 @@ (\\ts. (LT ! idx) = Some ts \\ G \\ (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 \\ @@ -32,22 +33,19 @@ (\\ts ST'. ST = ts # ST' \\ G \\ (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 \\ G \\ ((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 \\ G \\ (NT # ST , LT) <=s phi ! (pc+1))" -consts - wt_MO :: "[manipulate_object,jvm_prog,method_type,p_count,p_count] \\ 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 \\ @@ -57,7 +55,7 @@ G \\ oT \\ (Class C) \\ G \\ (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 \\ @@ -69,21 +67,14 @@ G \\ vT \\ T \\ G \\ (ST' , LT) <=s phi ! (pc+1)))" - -consts - wt_CO :: "[create_object,jvm_prog,method_type,p_count,p_count] \\ 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 \\ is_class G C \\ G \\ ((Class C) # ST , LT) <=s phi ! (pc+1))" -consts - wt_CH :: "[check_object,jvm_prog,method_type,p_count,p_count] \\ 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 \\ @@ -91,56 +82,49 @@ (\\rt ST'. ST = RefT rt # ST' \\ G \\ (Class C # ST' , LT) <=s phi ! (pc+1)))" -consts - wt_OS :: "[op_stack,jvm_prog,method_type,p_count,p_count] \\ 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 \\ts ST'. pc+1 < max_pc \\ ST = ts # ST' \\ G \\ (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 \\ (\\ts ST'. ST = ts # ST' \\ G \\ (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 \\ (\\ts1 ts2 ST'. ST = ts1 # ts2 # ST' \\ G \\ (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 \\ (\\ts1 ts2 ts3 ST'. ST = ts1 # ts2 # ts3 # ST' \\ G \\ (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 \\ (\\ts ts' ST'. ST = ts' # ts # ST' \\ G \\ (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 \\ (\\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 -"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 \\ (nat(int pc+branch)) < max_pc \\ @@ -150,16 +134,13 @@ G \\ (ST' , LT) <=s phi ! (pc+1) \\ G \\ (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 \\ G \\ (ST , LT) <=s phi ! (nat(int pc+branch)))" -consts - wt_MI :: "[meth_inv,jvm_prog,method_type,p_count,p_count] \\ 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 \\ @@ -170,30 +151,13 @@ (\\D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\ G \\ (rT # ST' , LT) <=s phi ! (pc+1))))))" -consts - wt_MR :: "[meth_ret,jvm_prog,ty,method_type,p_count] \\ bool" -primrec - "wt_MR Return G rT phi pc = +"wt_instr Return G rT phi max_pc pc = (let (ST,LT) = phi ! pc in (\\T ST'. ST = T # ST' \\ G \\ T \\ rT))" constdefs - wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count] \\ bool" - "wt_instr instr G rT phi max_pc pc \\ - case instr of - LS ins \\ wt_LS ins G phi max_pc pc - | CO ins \\ wt_CO ins G phi max_pc pc - | MO ins \\ wt_MO ins G phi max_pc pc - | CH ins \\ wt_CH ins G phi max_pc pc - | MI ins \\ wt_MI ins G phi max_pc pc - | MR ins \\ wt_MR ins G rT phi pc - | OS ins \\ wt_OS ins G phi max_pc pc - | BR ins \\ wt_BR ins G phi max_pc pc" - - -constdefs wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \\ bool" "wt_start G C pTs mxl phi \\ G \\ ([],(Some(Class C))#((map Some pTs))@(replicate mxl None)) <=s phi!0" diff -r cc0fd5226bb7 -r c32c5696ec2a src/HOL/MicroJava/BV/BVSpecTypeSafe.ML --- 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] "\\ wt_jvm_prog G phi; \ @@ -25,7 +25,7 @@ Goal "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -38,7 +38,7 @@ Goal "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -55,7 +55,7 @@ Goal "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -79,7 +79,7 @@ Goal "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -89,23 +89,6 @@ qed "Aconst_null_correct"; -Goal -"\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -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] "\\ wf_prog ok G; G,h\\v\\\\RefT rt; cast_ok G C h v ; G\\Class C\\T; is_class G C \\ \ @@ -124,7 +107,7 @@ Goal "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -135,28 +118,11 @@ addss (simpset() addsimps [map_eq_Cons,approx_val_def])) 1); qed "Checkcast_correct"; -Goal -"\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -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 "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -187,7 +153,7 @@ Goal "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -209,24 +175,6 @@ qed "Putfield_correct"; -Goal -"\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -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 "(\\x y. P(x,y)) = (\\z. P z)"; by(Fast_tac 1); qed "collapse_paired_All"; @@ -234,7 +182,7 @@ Goal "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -249,28 +197,13 @@ addsplits [option.split])) 1); qed "New_correct"; -Goal -"\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -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 "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -347,27 +280,12 @@ by (Asm_simp_tac 1); qed "Invoke_correct"; -Goal -"\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -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 "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -388,25 +306,11 @@ qed "Return_correct"; Addsimps [map_append]; -Goal -"\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -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 "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -419,7 +323,7 @@ Goal "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -428,28 +332,10 @@ qed "Ifiacmpeq_correct"; -Goal -"\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -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 "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -461,7 +347,7 @@ Goal "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -474,7 +360,7 @@ Goal "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -486,7 +372,7 @@ Goal "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -498,7 +384,7 @@ Goal "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -511,7 +397,7 @@ Goal "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ @@ -521,20 +407,28 @@ qed "IAdd_correct"; +(** instr correct **) + Goal "\\ 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 \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ \\\ G,phi \\JVM state'\\"; 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 "\\ xp=None; frs\\[] \\ \\ (\\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 diff -r cc0fd5226bb7 -r c32c5696ec2a src/HOL/MicroJava/BV/Correct.thy --- 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 (\\rT maxl ins. method (G,C) sig = Some(C,rT,(maxl,ins)) \\ - (\\mn pTs k. pc = k+1 \\ ins!k = MI(Invoke mn pTs) \\ + (\\mn pTs k. pc = k+1 \\ ins!k = (Invoke mn pTs) \\ (mn,pTs) = sig0 \\ (\\apTs D ST'. fst((phi C sig)!k) = (rev apTs) @ (Class D) # ST' \\ diff -r cc0fd5226bb7 -r c32c5696ec2a src/HOL/MicroJava/BV/LBVComplete.thy --- 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] \\ bool" "contains_dead ins cert phi pc \\ - (((\\ branch. ins!pc = BR (Goto branch)) \\ ins!pc = MR Return) \\ - (\\mi. ins!pc = MI mi)) \\ Suc pc < length phi \\ + (((\\ branch. ins!pc = (Goto branch)) \\ ins!pc = Return) \\ + (\\m l. ins!pc = Invoke m l)) \\ Suc pc < length phi \\ cert ! (Suc pc) = Some (phi ! Suc pc)" contains_targets :: "[instr list, certificate, method_type, p_count] \\ bool" "contains_targets ins cert phi pc \\ - \\ branch. (ins!pc = BR (Goto branch) \\ ins!pc = BR (Ifcmpeq branch)) \\ + \\ branch. (ins!pc = (Goto branch) \\ ins!pc = (Ifcmpeq branch)) \\ (let pc' = nat (int pc+branch) in pc' < length phi \\ cert!pc' = Some (phi!pc'))" fits :: "[instr list, certificate, method_type] \\ bool" @@ -36,14 +36,14 @@ is_target :: "[instr list, p_count] \\ bool" "is_target ins pc \\ \\ pc' branch. pc' < length ins \\ - (ins ! pc' = (BR (Ifcmpeq branch)) \\ ins ! pc' = (BR (Goto branch))) \\ + (ins ! pc' = (Ifcmpeq branch) \\ ins ! pc' = (Goto branch)) \\ pc = (nat(int pc'+branch))" maybe_dead :: "[instr list, p_count] \\ bool" "maybe_dead ins pc \\ - \\ pc'. pc = pc'+1 \\ ((\\ branch. ins!pc' = BR (Goto branch)) \\ - ins!pc' = MR Return \\ - (\\mi. ins!pc' = MI mi))" + \\ pc'. pc = pc'+1 \\ ((\\ branch. ins!pc' = (Goto branch)) \\ + ins!pc' = Return \\ + (\\m l. ins!pc' = Invoke m l))" mdot :: "[instr list, p_count] \\ bool" @@ -70,10 +70,6 @@ let (sig,rT,maxl,b) = \\ (sg,rT,maxl,b). (sg,rT,maxl,b) \\ set mdecls \\ sg = sig in make_cert b (Phi C sig)"; -constdefs - wfprg :: "jvm_prog \\ bool" - "wfprg G \\ \\wf_mb. wf_prog wf_mb G"; - lemma length_ofn: "\\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: -"\\fits ins cert phi; i = ins!pc; i = MI meth_inv; pc < length ins; +"\\fits ins cert phi; i = ins!pc; i = Invoke mname list; pc < length ins; wf_prog wf_mb G; G \\ (x, y) <=s s1; wtl_inst (ins!pc) G rT s1 s1' cert mpc pc\\ \\ \\s2'. wtl_inst i G rT (x, y) s2' cert mpc pc \\ \ ((G \\ s2' <=s s1') \\ (\\ s. cert ! (Suc pc) = Some s \\ (G \\ 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 \\ (x, y) <=s s1"; - with Invoke; - show ?thesis; (* (is "\\s2'. ?wtl s2' \\ (?lt s2' s1' \\ ?cert s2')" is "\\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 \\ (x, y) <=s (rev apTs @ X # ST', y')"; @@ -353,7 +347,7 @@ hence x2: "G \\ (a, y) <=s (apTs, y') \\ G \\ b\\X \\ G \\ (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 "\\ 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: "\\ y n. (G \\ b <=l y) \\ n < length y \\ y!n = Some t \\ (\\t. b!n = Some t \\ (G \\ (b!n) <=o (y!n)))" (is "?P b"); @@ -500,7 +494,7 @@ show "xb = PrimT p \\ G \\ xb \\ PrimT p"; by blast; show "G\\ xb \\ PrimT p \\ xb = PrimT p"; - proof (cases xb); print_cases; + proof (cases xb); fix prim; assume "xb = PrimT prim" "G\\xb\\PrimT p"; thus ?thesis; by simp; @@ -523,151 +517,103 @@ have 3: "\\ 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 \\ x \\ oT" "G \\ oT \\ Class cname"; - show "G \\ x \\ 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 \\ x \\ vT" "G \\ vT \\ T"; - hence * : "G \\ x \\ T"; by (rule widen_trans); - - assume "G \\ xa \\ oT" "G \\ oT \\ Class cname"; - hence "G \\ xa \\ Class cname"; by (rule widen_trans); - - with *; - show "(G \\ xa \\ Class cname) \\ (G \\ x \\ T)"; by blast; - qed; + proof (elim, clarsimp_tac simp add: sup_state_Cons2); + fix oT x; + assume "G \\ x \\ oT" "G \\ oT \\ Class cname"; + show "G \\ x \\ 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 \\ x \\ vT" "G \\ vT \\ T"; + hence * : "G \\ x \\ T"; by (rule widen_trans); - next; - case MI; + assume "G \\ xa \\ oT" "G \\ oT \\ Class cname"; + hence "G \\ xa \\ Class cname"; by (rule widen_trans); + + with * + show "(G \\ xa \\ Class cname) \\ (G \\ x \\ 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\\x\\T" "G\\T\\rT"; - thus "G\\x\\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\\x\\T" "G\\T\\rT"; + thus "G\\x\\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 \\ (a, b) <=s s1" "G \\