# HG changeset patch # User kleing # Date 965651576 -7200 # Node ID 40d64cb4f4e63b471f478703be47107cc1c71589 # Parent 15bee2731e43aba5a46948998dab4b4826e7257a BV and LBV specified in terms of app and step functions diff -r 15bee2731e43 -r 40d64cb4f4e6 src/HOL/MicroJava/BV/BVSpec.ML --- a/src/HOL/MicroJava/BV/BVSpec.ML Mon Aug 07 10:29:54 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ -(* Title: HOL/MicroJava/BV/BVSpec.ML - ID: $Id$ - Author: Cornelia Pusch - Copyright 1999 Technische Universitaet Muenchen -*) - -Goalw [wt_jvm_prog_def] "wt_jvm_prog G phi \\ (\\wt. wf_prog wt G)"; -by(Blast_tac 1); -qed "wt_jvm_progD"; - - -Goalw [wt_jvm_prog_def] -"\\ wt_jvm_prog G phi; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ pc < length ins \\ \ -\\\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"; -by(forward_tac [rotate_prems 2 method_wf_mdecl] 1); - by (Asm_full_simp_tac 1); -by(asm_full_simp_tac (simpset() addsimps [wf_mdecl_def,wt_method_def]) 1); -qed "wt_jvm_prog_impl_wt_instr"; - -Goalw [wt_jvm_prog_def] -"\\ wt_jvm_prog G phi; \ -\ method (G,C) sig = Some (C,rT,maxl,ins) \\ \\ \ -\ 0 < (length ins) \\ wt_start G C (snd sig) maxl (phi C sig)"; -by(forward_tac [rotate_prems 2 method_wf_mdecl] 1); - by (Asm_full_simp_tac 1); -by(asm_full_simp_tac (simpset() addsimps [wf_mdecl_def,wt_method_def]) 1); -qed "wt_jvm_prog_impl_wt_start"; diff -r 15bee2731e43 -r 40d64cb4f4e6 src/HOL/MicroJava/BV/BVSpec.thy --- a/src/HOL/MicroJava/BV/BVSpec.thy Mon Aug 07 10:29:54 2000 +0200 +++ b/src/HOL/MicroJava/BV/BVSpec.thy Mon Aug 07 14:32:56 2000 +0200 @@ -6,173 +6,58 @@ Specification of bytecode verifier *) -BVSpec = Convert + +theory BVSpec = Step : types - method_type = "state_type list" - class_type = "sig \\ method_type" - prog_type = "cname \\ class_type" - -consts -wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count] \\ bool" - -primrec -"wt_instr (Load idx) G rT phi max_pc pc = - (let (ST,LT) = phi ! pc - in - pc+1 < max_pc \\ - idx < length LT \\ - (\\ts. (LT ! idx) = Some ts \\ - G \\ (ts # ST , LT) <=s phi ! (pc+1)))" - -"wt_instr (Store idx) G rT phi max_pc pc = - (let (ST,LT) = phi ! pc - in - pc+1 < max_pc \\ - idx < length LT \\ - (\\ts ST'. ST = ts # ST' \\ - G \\ (ST' , LT[idx:=Some ts]) <=s phi ! (pc+1)))" - -"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_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))" - -"wt_instr (Getfield F C) G rT phi max_pc pc = - (let (ST,LT) = phi ! pc - in - pc+1 < max_pc \\ - is_class G C \\ - (\\T oT ST'. field (G,C) F = Some(C,T) \\ - ST = oT # ST' \\ - G \\ oT \\ (Class C) \\ - G \\ (T # ST' , LT) <=s phi ! (pc+1)))" - -"wt_instr (Putfield F C) G rT phi max_pc pc = - (let (ST,LT) = phi ! pc - in - pc+1 < max_pc \\ - is_class G C \\ - (\\T vT oT ST'. - field (G,C) F = Some(C,T) \\ - ST = vT # oT # ST' \\ - G \\ oT \\ (Class C) \\ - G \\ vT \\ T \\ - G \\ (ST' , LT) <=s phi ! (pc+1)))" - -"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))" - -"wt_instr (Checkcast C) G rT phi max_pc pc = - (let (ST,LT) = phi ! pc - in - pc+1 < max_pc \\ - is_class G C \\ - (\\rt ST'. ST = RefT rt # ST' \\ - G \\ (Class C # ST' , LT) <=s phi ! (pc+1)))" - -"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_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_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_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_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_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)))" - -"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 \\ - (\\ts ts' ST'. ST = ts # ts' # ST' \\ - ((\\p. ts = PrimT p \\ ts' = PrimT p) \\ - (\\r r'. ts = RefT r \\ ts' = RefT r')) \\ - G \\ (ST' , LT) <=s phi ! (pc+1) \\ - G \\ (ST' , LT) <=s phi ! (nat(int pc+branch))))" - -"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)))" - -"wt_instr (Invoke mn fpTs) G rT phi max_pc pc = - (let (ST,LT) = phi ! pc - in - pc+1 < max_pc \\ - (\\apTs X ST'. ST = (rev apTs) @ (X # ST') \\ - length apTs = length fpTs \\ - (X = NT \\ (\\C. X = Class C \\ - (\\(aT,fT)\\set(zip apTs fpTs). G \\ aT \\ fT) \\ - (\\D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\ - G \\ (rT # ST' , LT) <=s phi ! (pc+1))))))" - -"wt_instr Return G rT phi max_pc pc = - (let (ST,LT) = phi ! pc - in - (\\T ST'. ST = T # ST' \\ G \\ T \\ rT))" - + method_type = "state_type list" + class_type = "sig \\ method_type" + prog_type = "cname \\ class_type" constdefs - wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \\ bool" - "wt_start G C pTs mxl phi \\ +wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] \\ bool" +"wt_instr i G rT phi max_pc pc \\ + app (i, G, rT, phi!pc) \\ + (\\ pc' \\ (succs i pc). pc' < max_pc \\ (G \\ the (step (i, G, phi!pc)) <=s phi!pc'))" + +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" - wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\ bool" - "wt_method G C pTs rT mxl ins phi \\ +wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\ bool" +"wt_method G C pTs rT mxl ins phi \\ let max_pc = length ins in length ins < length phi \\ 0 < max_pc \\ wt_start G C pTs mxl phi \\ (\\pc. pc wt_instr (ins ! pc) G rT phi max_pc pc)" - wt_jvm_prog :: "[jvm_prog,prog_type] \\ bool" +wt_jvm_prog :: "[jvm_prog,prog_type] \\ bool" "wt_jvm_prog G phi \\ wf_prog (\\G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (phi C sig)) G" +lemma wt_jvm_progD: +"wt_jvm_prog G phi \\ (\\wt. wf_prog wt G)" +by (unfold wt_jvm_prog_def, blast) + +lemma wt_jvm_prog_impl_wt_instr: +"\\ wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins \\ + \\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"; +by (unfold wt_jvm_prog_def, drule method_wf_mdecl, + simp, simp add: wf_mdecl_def wt_method_def) + +lemma wt_jvm_prog_impl_wt_start: +"\\ wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins) \\ \\ + 0 < (length ins) \\ wt_start G C (snd sig) maxl (phi C sig)" +by (unfold wt_jvm_prog_def, drule method_wf_mdecl, + simp, simp add: wf_mdecl_def wt_method_def) + +lemma [simp]: +"succs i pc = {pc+1} \\ wt_instr i G rT phi max_pc pc = + (app (i, G, rT, phi!pc) \\ pc+1 < max_pc \\ + (G \\ the (step (i, G, phi!pc)) <=s phi!(pc+1)))" +by (simp add: wt_instr_def) + end + + diff -r 15bee2731e43 -r 40d64cb4f4e6 src/HOL/MicroJava/BV/BVSpecTypeSafe.ML --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Mon Aug 07 10:29:54 2000 +0200 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Mon Aug 07 14:32:56 2000 +0200 @@ -5,7 +5,7 @@ *) val defs1 = exec.simps@[split_def,sup_state_def,correct_state_def, - correct_frame_def]; + correct_frame_def, thm "wt_instr_def"]; Goalw [correct_state_def,Let_def,correct_frame_def,split_def] "\\ wt_jvm_prog G phi; \ @@ -13,15 +13,16 @@ \ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ \\\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"; by (Asm_full_simp_tac 1); -by(blast_tac (claset() addIs [wt_jvm_prog_impl_wt_instr]) 1); +by(blast_tac (claset() addIs [thm "wt_jvm_prog_impl_wt_instr"]) 1); qed "wt_jvm_prog_impl_wt_instr_cor"; -Delsimps [split_paired_All]; +Delsimps [split_paired_All]; (******* LS *******) + Goal "\\ wf_prog wt G; \ \ method (G,C) sig = Some (C,rT,maxl,ins); \ @@ -30,11 +31,13 @@ \ 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 (case_tac "phi C sig!pc" 1); by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_val_sup, approx_loc_imp_approx_loc_sup] addss (simpset() addsimps [map_eq_Cons]@defs1)) 1); qed "Load_correct"; + Goal "\\ wf_prog wt G; \ \ method (G,C) sig = Some (C,rT,maxl,ins); \ @@ -47,6 +50,7 @@ addss (simpset() addsimps [map_eq_Cons]@defs1)) 1); qed "Store_correct"; + Goalw [conf_def] "G,h \\ Intg i \\\\ PrimT Integer"; by(Simp_tac 1); qed "conf_Intg_Integer"; @@ -60,6 +64,7 @@ \ 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 (case_tac "phi C sig ! pc" 1); by (fast_tac (claset()addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps [approx_val_def,sup_PTS_eq,map_eq_Cons]@defs1)) 1); qed "Bipush_correct"; @@ -84,12 +89,12 @@ \ 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 (case_tac "phi C sig ! pc" 1); by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps [approx_val_Null,NT_subtype_conv,map_eq_Cons]@defs1)) 1); qed "Aconst_null_correct"; - 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 \\ \ \ \\ G,h\\v\\\\T"; @@ -118,7 +123,6 @@ addss (simpset() addsimps [map_eq_Cons,approx_val_def])) 1); qed "Checkcast_correct"; - Goal "\\ wf_prog wt G; \ \ method (G,C) sig = Some (C,rT,maxl,ins); \ @@ -138,16 +142,16 @@ ba 1; bd conf_RefTD 1; by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps []) 1); +by (asm_full_simp_tac (simpset() addsimps []) 1); br conjI 1; bd widen_cfs_fields 1; ba 1; ba 1; - by(fast_tac (claset() addIs [conf_widen] addss (simpset() addsimps [hconf_def,oconf_def,lconf_def])) 1); + by (fast_tac (claset() addIs [conf_widen] addss (simpset() addsimps [hconf_def,oconf_def,lconf_def])) 1); by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]) 1); +qed "Getfield_correct"; -qed "Getfield_correct"; Goal @@ -174,7 +178,6 @@ correct_frames_imp_correct_frames_field_update,conf_widen] addss (simpset())) 1); qed "Putfield_correct"; - Goal "(\\x y. P(x,y)) = (\\z. P z)"; by(Fast_tac 1); qed "collapse_paired_All"; @@ -187,6 +190,7 @@ \ 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 (case_tac "phi C sig ! pc" 1); by (fast_tac (claset() addSDs [collapse_paired_All RS iffD1]addIs [sup_heap_newref, approx_stk_imp_approx_stk_sup_heap RSN(2,approx_stk_imp_approx_stk_sup), approx_loc_imp_approx_loc_sup_heap RSN(2,approx_loc_imp_approx_loc_sup), @@ -198,88 +202,105 @@ qed "New_correct"; + +Delsimps (thms "app.simps"); + (****** Method Invocation ******) Goal "\\ wt_jvm_prog G phi; \ \ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ ins ! pc = Invoke mn pTs; \ +\ ins ! pc = Invoke C' 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)\\ \\ \ \\\ G,phi \\JVM state'\\"; -by(forward_tac [wt_jvm_progD] 1); +by(case_tac "phi C sig ! pc" 1); +by(forward_tac [thm "wt_jvm_progD"] 1); by(etac exE 1); by(asm_full_simp_tac (simpset() addsimps defs1) 1); by(Clarify_tac 1); -by(case_tac "X\\NT" 1); - by (asm_full_simp_tac (simpset()addsimps[raise_xcpt_def]@defs1 - addsplits [option.split]) 1); - by (Clarify_tac 1); - by (asm_full_simp_tac (simpset() addsimps defs1) 1); - bd approx_stk_append_lemma 1; - by (Clarify_tac 1); - by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1); - bd conf_RefTD 1; - by (Clarify_tac 1); - by(rename_tac "oloc oT ofs T'" 1); - by (asm_full_simp_tac (simpset() addsimps defs1) 1); - bd subtype_widen_methd 1; - ba 1; +by(asm_full_simp_tac (simpset() addsimps [raise_xcpt_def] addsplits [option.split]) 1); +by(Clarify_tac 1); +bd approx_stk_append_lemma 1; +by(clarsimp_tac (claset(), simpset() addsimps [approx_val_def]) 1); + +by (subgoal_tac "\\ D'. X = Class D'" 1); + bd widen_RefT2 2; + by (Clarsimp_tac 2); + bd conf_RefTD 2; + by (Clarsimp_tac 2); + bd widen_Class 2; + by (Clarsimp_tac 2); + +by (Clarsimp_tac 1); +bd conf_RefTD 1; +by (Clarify_tac 1); +by(rename_tac "oloc oT ofs T'" 1); +by (asm_full_simp_tac (simpset() addsimps defs1) 1); +by (subgoal_tac "G\\oT\\C C'" 1); + bd widen.subcls 2; + bd widen.subcls 2; + by (((dtac widen_trans) THEN' atac THEN' Blast_tac) 2); +bd subtype_widen_methd 1; ba 1; - be exE 1; - by(rename_tac "oT'" 1); - by (Clarify_tac 1); - by(subgoal_tac "G \\ oT \\C oT'" 1); - by(forw_inst_tac [("C","oT")](standard(rotate_prems 1 method_wf_mdecl)) 2); - ba 2; - by(Blast_tac 2); - by (asm_full_simp_tac (simpset() addsimps defs1) 1); - by(forward_tac [method_in_md] 1); + ba 1; +by (Clarify_tac 1); +bd subtype_widen_methd 1; ba 1; - back(); - back(); - by (Clarify_tac 1); - by (asm_full_simp_tac (simpset() addsimps defs1) 1); - by (forward_tac [wt_jvm_prog_impl_wt_start] 1); - ba 1; - back(); - by (asm_full_simp_tac (simpset() addsimps [wt_start_def,sup_state_def]) 1); - by (Clarify_tac 1); + ba 1; +be exE 1; +by(rename_tac "oT'" 1); +by (Clarify_tac 1); +by(subgoal_tac "G \\ oT \\C oT'" 1); + by(forw_inst_tac [("C","oT")] method_wf_mdecl 2); + ba 2; + by (Blast_tac 2); +by (asm_full_simp_tac (simpset() addsimps defs1) 1); +by(forward_tac [method_in_md] 1); + ba 1; + back(); + back(); + back(); +by (Clarify_tac 1); +by (asm_full_simp_tac (simpset() addsimps defs1) 1); +by (forward_tac [thm "wt_jvm_prog_impl_wt_start"] 1); + ba 1; + back(); +by (asm_full_simp_tac (simpset() addsimps [thm "wt_start_def",sup_state_def]) 1); +by (Clarify_tac 1); (** approx_loc **) +br conjI 1; + br approx_loc_imp_approx_loc_sup 1; + ba 1; + by (Fast_tac 2); + by (asm_full_simp_tac (simpset() addsimps [split_def,approx_val_def,approx_loc_append]) 1); br conjI 1; - br approx_loc_imp_approx_loc_sup 1; + br conf_widen 1; ba 1; by (Fast_tac 2); - by (asm_full_simp_tac (simpset() addsimps [split_def,approx_val_def,approx_loc_append]) 1); - br conjI 1; - br conf_widen 1; - ba 1; - by (Fast_tac 2); - by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1); - br conjI 1; - by (fast_tac (claset() addIs [approx_stk_rev RS iffD2 RSN(4,assConv_approx_stk_imp_approx_loc)] - addss (simpset() addsimps [split_def,approx_val_def])) 1); - by (asm_simp_tac (simpset() addsimps [list_all2_def,split_def,approx_loc_def,approx_val_None,set_replicate_conv_if]) 1); - + by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1); br conjI 1; - by (asm_simp_tac (simpset() addsimps [min_def]) 1); - br exI 1; - br exI 1; - br conjI 1; - by(Blast_tac 1); - by (fast_tac (claset() - addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] - addss (simpset()addsimps [map_eq_Cons])) 1); -by (Asm_full_simp_tac 1); -bd approx_stk_append_lemma 1; -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [approx_val_def, raise_xcpt_def]) 1); -bd conf_NullTD 1; -by (Asm_simp_tac 1); + by (fast_tac (claset() addIs [approx_stk_rev RS iffD2 RSN(4,assConv_approx_stk_imp_approx_loc)] + addss (simpset() addsimps [split_def,approx_val_def])) 1); + by (asm_simp_tac (simpset() addsimps [list_all2_def,split_def,approx_loc_def,approx_val_None,set_replicate_conv_if]) 1); + +br conjI 1; + by (asm_simp_tac (simpset() addsimps [min_def]) 1); +br exI 1; +br exI 1; +br conjI 1; + by(Blast_tac 1); +by (Clarsimp_tac 1); + +by (fast_tac (claset() + addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] + addss (simpset()addsimps [map_eq_Cons])) 1); qed "Invoke_correct"; +Addsimps (thms "app.simps"); + Delsimps [map_append]; Goal @@ -295,9 +316,10 @@ by (asm_full_simp_tac (simpset() addsimps [map_eq_Cons]@defs1) 1); by (Clarify_tac 1); by (asm_full_simp_tac (simpset() addsimps defs1) 1); -by (forward_tac [wt_jvm_prog_impl_wt_instr] 1); +by (forward_tac [thm "wt_jvm_prog_impl_wt_instr"] 1); by(EVERY1[atac, etac Suc_lessD]); -by(rewtac wt_jvm_prog_def); +by(rewtac (thm "wt_jvm_prog_def")); +by (case_tac "phi ab (ac, b) ! k" 1); by (fast_tac (claset() addDs [subcls_widen_methd] addEs [rotate_prems 1 widen_trans] @@ -307,6 +329,7 @@ Addsimps [map_append]; + Goal "\\ wf_prog wt G; \ \ method (G,C) sig = Some (C,rT,maxl,ins); \ @@ -329,7 +352,7 @@ \ 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_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1); -qed "Ifiacmpeq_correct"; +qed "Ifcmpeq_correct"; Goal @@ -357,6 +380,7 @@ qed "Dup_correct"; + Goal "\\ wf_prog wt G; \ \ method (G,C) sig = Some (C,rT,maxl,ins); \ @@ -407,6 +431,7 @@ qed "IAdd_correct"; + (** instr correct **) Goal @@ -421,11 +446,11 @@ 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(rewtac (thm "wt_jvm_prog_def")); 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, + Goto_correct,Ifcmpeq_correct,Pop_correct,Dup_correct, Dup_x1_correct,Dup_x2_correct,Swap_correct,IAdd_correct]))); qed "instr_correct"; diff -r 15bee2731e43 -r 40d64cb4f4e6 src/HOL/MicroJava/BV/Correct.thy --- a/src/HOL/MicroJava/BV/Correct.thy Mon Aug 07 10:29:54 2000 +0200 +++ b/src/HOL/MicroJava/BV/Correct.thy Mon Aug 07 14:32:56 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 = (Invoke mn pTs) \\ + (\\C' mn pTs k. pc = k+1 \\ ins!k = (Invoke C' mn pTs) \\ (mn,pTs) = sig0 \\ (\\apTs D ST'. fst((phi C sig)!k) = (rev apTs) @ (Class D) # ST' \\ diff -r 15bee2731e43 -r 40d64cb4f4e6 src/HOL/MicroJava/BV/LBVComplete.thy --- a/src/HOL/MicroJava/BV/LBVComplete.thy Mon Aug 07 10:29:54 2000 +0200 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy Mon Aug 07 14:32:56 2000 +0200 @@ -6,10 +6,12 @@ header {* Completeness of the LBV *} -theory LBVComplete = LBVSpec:; +theory LBVComplete = BVSpec + LBVSpec: + -ML_setup {* bind_thm ("widen_RefT", widen_RefT) *}; -ML_setup {* bind_thm ("widen_RefT2", widen_RefT2) *}; +ML_setup {* bind_thm ("widen_RefT", widen_RefT) *} +ML_setup {* bind_thm ("widen_RefT2", widen_RefT2) *} + constdefs is_approx :: "['a option list, 'a list] \\ bool" @@ -18,14 +20,14 @@ contains_dead :: "[instr list, certificate, method_type, p_count] \\ bool" "contains_dead ins cert phi pc \\ - (((\\ 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)" + Suc pc \\ succs (ins!pc) pc \\ 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 = (Goto branch) \\ ins!pc = (Ifcmpeq branch)) \\ - (let pc' = nat (int pc+branch) in pc' < length phi \\ cert!pc' = Some (phi!pc'))" + "contains_targets ins cert phi pc \\ ( + \\ pc' \\ succs (ins!pc) pc. pc' \\ Suc pc \\ pc' < length phi \\ + cert!pc' = Some (phi!pc'))" + fits :: "[instr list, certificate, method_type] \\ bool" "fits ins cert phi \\ is_approx cert phi \\ length ins < length phi \\ @@ -34,28 +36,21 @@ contains_targets ins cert phi pc)" is_target :: "[instr list, p_count] \\ bool" - "is_target ins pc \\ - \\ pc' branch. pc' < length ins \\ - (ins ! pc' = (Ifcmpeq branch) \\ ins ! pc' = (Goto branch)) \\ - pc = (nat(int pc'+branch))" - + "is_target ins pc \\ \\ pc'. pc' < length ins \\ pc \\ succs (ins!pc') pc'" + maybe_dead :: "[instr list, p_count] \\ bool" - "maybe_dead ins pc \\ - \\ pc'. pc = pc'+1 \\ ((\\ branch. ins!pc' = (Goto branch)) \\ - ins!pc' = Return \\ - (\\m l. ins!pc' = Invoke m l))" - + "maybe_dead ins pc \\ \\ pc'. pc = pc'+1 \\ pc \\ succs (ins!pc') pc'" mdot :: "[instr list, p_count] \\ bool" - "mdot ins pc \\ maybe_dead ins pc \\ is_target ins pc"; + "mdot ins pc \\ maybe_dead ins pc \\ is_target ins pc" consts - option_filter_n :: "['a list, nat \\ bool, nat] \\ 'a option list"; + option_filter_n :: "['a list, nat \\ bool, nat] \\ 'a option list" primrec "option_filter_n [] P n = []" "option_filter_n (h#t) P n = (if (P n) then Some h # option_filter_n t P (n+1) - else None # option_filter_n t P (n+1))"; + else None # option_filter_n t P (n+1))" constdefs option_filter :: "['a list, nat \\ bool] \\ 'a option list" @@ -68,678 +63,267 @@ "make_Cert G Phi \\ \\ C sig. let (C,x,y,mdecls) = \\ (Cl,x,y,mdecls). (Cl,x,y,mdecls) \\ set G \\ Cl = C in let (sig,rT,maxl,b) = \\ (sg,rT,maxl,b). (sg,rT,maxl,b) \\ set mdecls \\ sg = sig in - make_cert b (Phi C sig)"; + make_cert b (Phi C sig)" -lemma length_ofn: "\\n. length (option_filter_n l P n) = length l"; - by (induct l) auto; +lemma length_ofn: "\\n. length (option_filter_n l P n) = length l" + by (induct l) auto lemma is_approx_option_filter_n: -"\\n. is_approx (option_filter_n a P n) a" (is "?P a"); -proof (induct a); - show "?P []"; by (auto simp add: is_approx_def); +"\\n. is_approx (option_filter_n a P n) a" (is "?P a") +proof (induct a) + show "?P []" by (auto simp add: is_approx_def) - fix l ls; - assume Cons: "?P ls"; + fix l ls + assume Cons: "?P ls" - show "?P (l#ls)"; - proof (unfold is_approx_def, intro allI conjI impI); - fix n; - show "length (option_filter_n (l # ls) P n) = length (l # ls)"; - by (simp only: length_ofn); + show "?P (l#ls)" + proof (unfold is_approx_def, intro allI conjI impI) + fix n + show "length (option_filter_n (l # ls) P n) = length (l # ls)" + by (simp only: length_ofn) - fix m; - assume "m < length (option_filter_n (l # ls) P n)"; - hence m: "m < Suc (length ls)"; by (simp only: length_ofn) simp; + fix m + assume "m < length (option_filter_n (l # ls) P n)" + hence m: "m < Suc (length ls)" by (simp only: length_ofn) simp show "option_filter_n (l # ls) P n ! m = None \\ - option_filter_n (l # ls) P n ! m = Some ((l # ls) ! m)"; - proof (cases "m"); - assume "m = 0"; - with m; show ?thesis; by simp; - next; - fix m'; assume Suc: "m = Suc m'"; - from Cons; - show ?thesis; - proof (unfold is_approx_def, elim allE impE conjE); - from m Suc; - show "m' < length (option_filter_n ls P (Suc n))"; by (simp add: length_ofn); + option_filter_n (l # ls) P n ! m = Some ((l # ls) ! m)" + proof (cases "m") + assume "m = 0" + with m show ?thesis by simp + next + fix m' assume Suc: "m = Suc m'" + from Cons + show ?thesis + proof (unfold is_approx_def, elim allE impE conjE) + from m Suc + show "m' < length (option_filter_n ls P (Suc n))" by (simp add: length_ofn) assume "option_filter_n ls P (Suc n) ! m' = None \\ - option_filter_n ls P (Suc n) ! m' = Some (ls ! m')"; - with m Suc; - show ?thesis; by auto; - qed; - qed; - qed; -qed; - -lemma is_approx_option_filter: "is_approx (option_filter l P) l"; - by (simp add: option_filter_def is_approx_option_filter_n); - -lemma option_filter_Some: -"\\n < length l; P n\\ \\ option_filter l P ! n = Some (l!n)"; -proof -; - - assume 1: "n < length l" "P n"; - - have "\\n n'. n < length l \\ P (n+n') \\ option_filter_n l P n' ! n = Some (l!n)" - (is "?P l"); - proof (induct l); - show "?P []"; by simp; - - fix l ls; assume Cons: "?P ls"; - show "?P (l#ls)"; - proof (intro); - fix n n'; - assume l: "n < length (l # ls)"; - assume P: "P (n + n')"; - show "option_filter_n (l # ls) P n' ! n = Some ((l # ls) ! n)"; - proof (cases "n"); - assume "n=0"; - with P; show ?thesis; by simp; - next; - fix m; assume "n = Suc m"; - with l P Cons; - show ?thesis; by simp; - qed; - qed; - qed; - - with 1; - show ?thesis; by (auto simp add: option_filter_def); -qed; - -lemma option_filter_contains_dead: -"contains_dead ins (option_filter phi (mdot ins)) phi pc"; - by (auto intro: option_filter_Some simp add: contains_dead_def mdot_def maybe_dead_def); - -lemma option_filter_contains_targets: -"pc < length ins \\ contains_targets ins (option_filter phi (mdot ins)) phi pc"; -proof (simp add: contains_targets_def, intro allI impI conjI); - - fix branch; - assume 1: "ins ! pc = Goto branch" - "nat (int pc + branch) < length phi" - "pc < length ins"; - - show "option_filter phi (mdot ins) ! nat (int pc + branch) = Some (phi ! nat (int pc + branch))"; - proof (rule option_filter_Some); - from 1; show "nat (int pc + branch) < length phi"; by simp; - from 1; - have "is_target ins (nat (int pc + branch))"; by (auto simp add: is_target_def); - thus "mdot ins (nat (int pc + branch))"; by (simp add: mdot_def); - qed; - -next; - fix branch; - assume 2: "ins ! pc = Ifcmpeq branch" - "nat (int pc + branch) < length phi" - "pc < length ins"; - - show "option_filter phi (mdot ins) ! nat (int pc + branch) = Some (phi ! nat (int pc + branch))"; - proof (rule option_filter_Some); - from 2; show "nat (int pc + branch) < length phi"; by simp; - from 2; - have "is_target ins (nat (int pc + branch))"; by (auto simp add: is_target_def); - thus "mdot ins (nat (int pc + branch))"; by (simp add: mdot_def); - qed; - -qed; - - -lemma fits_make_cert: - "length ins < length phi \\ fits ins (make_cert ins phi) phi"; -proof -; - assume l: "length ins < length phi"; - - thus "fits ins (make_cert ins phi) phi"; - proof (unfold fits_def make_cert_def, intro conjI allI impI); - show "is_approx (option_filter phi (mdot ins)) phi"; by (rule is_approx_option_filter); - show "length ins < length phi"; .; - - fix pc; - show "contains_dead ins (option_filter phi (mdot ins)) phi pc"; by (rule option_filter_contains_dead); - - assume "pc < length ins"; - thus "contains_targets ins (option_filter phi (mdot ins)) phi pc"; by (rule option_filter_contains_targets); - qed; -qed; - - - -lemma append_length_n: "\\n. n \\ length x \\ (\\a b. x = a@b \\ length a = n)" (is "?P x"); -proof (induct "?P" "x"); - show "?P []"; by simp; - - fix l ls; assume Cons: "?P ls"; - - show "?P (l#ls)"; - proof (intro allI impI); - fix n; - assume l: "n \\ length (l # ls)"; - - show "\\a b. l # ls = a @ b \\ length a = n"; - proof (cases n); - assume "n=0"; thus ?thesis; by simp; - next; - fix "n'"; assume s: "n = Suc n'"; - with l; - have "n' \\ length ls"; by simp; - hence "\\a b. ls = a @ b \\ length a = n'"; by (rule Cons [rulify]); - thus ?thesis; - proof elim; - fix a b; - assume "ls = a @ b" "length a = n'"; - with s; - have "l # ls = (l#a) @ b \\ length (l#a) = n"; by simp; - thus ?thesis; by blast; - qed; - qed; - qed; -qed; - - - -lemma rev_append_cons: -"\\n < length x\\ \\ \\a b c. x = (rev a) @ b # c \\ length a = n"; -proof -; - assume n: "n < length x"; - hence "n \\ length x"; by simp; - hence "\\a b. x = a @ b \\ length a = n"; by (rule append_length_n [rulify]); - thus ?thesis; - proof elim; - fix r d; assume x: "x = r@d" "length r = n"; - with n; - have "\\b c. d = b#c"; by (simp add: neq_Nil_conv); - - thus ?thesis; - proof elim; - fix b c; - assume "d = b#c"; - with x; - have "x = (rev (rev r)) @ b # c \\ length (rev r) = n"; by simp; - thus ?thesis; by blast; - qed; - qed; -qed; - -lemma widen_NT: "G \\ b \\ NT \\ b = NT"; -proof (cases b); - case RefT; - thus "G\\b\\NT \\ b = NT"; by - (cases ref_ty, auto); -qed auto; - -lemma widen_Class: "G \\ b \\ Class C \\ \\r. b = RefT r"; -by (cases b) auto; - -lemma all_widen_is_sup_loc: -"\\b. length a = length b \\ (\\x\\set (zip a b). x \\ widen G) = (G \\ (map Some a) <=l (map Some b))" - (is "\\b. length a = length b \\ ?Q a b" is "?P a"); -proof (induct "a"); - show "?P []"; by simp; - - fix l ls; assume Cons: "?P ls"; - - show "?P (l#ls)"; - proof (intro allI impI); - fix b; - assume "length (l # ls) = length (b::ty list)"; - with Cons; - show "?Q (l # ls) b"; by - (cases b, auto); - qed; -qed; - -lemma method_inv_pseudo_mono: -"\\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 - - assume fits: "fits ins cert phi" 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"; - - 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')"; - assume lapTs: "length apTs = length list"; - assume "cert ! Suc pc = Some s"; - assume wtl: "s = s1' \\ X = NT \\ - G \\ s1' <=s s \\ - (\\C. X = Class C \\ - (\\x\\set (zip apTs list). x \\ widen G) \\ - (\\D rT. (\\b. method (G, C) (mname, list) = Some (D, rT, b)) \\ - (rT # ST', y') = s1'))" (is "?NT \\ ?ClassC"); - - from G; - have "\\a b c. x = rev a @ b # c \\ length a = length apTs"; - by - (rule rev_append_cons, simp add: sup_state_length_fst); - - thus "\\s2'. (\\apTs X ST'. - x = rev apTs @ X # ST' \\ - length apTs = length list \\ - (s = s2' \\ X = NT \\ - G \\ s2' <=s s \\ - (\\C. X = Class C \\ - (\\x\\set (zip apTs list). x \\ widen G) \\ - (\\D rT. (\\b. method (G, C) (mname, list) = Some (D, rT, b)) \\ - (rT # ST', y) = s2')))) \\ - (G \\ s2' <=s s1' \\ G \\ s2' <=s s)" (is "\\s2'. ?P s2'"); - proof elim; - fix a b c; - assume rac: "x = rev a @ b # c"; - with G; - have x: "G \\ (rev a @ b # c, y) <=s (rev apTs @ X # ST', y')"; by simp; - - assume l: "length a = length apTs"; - hence "length (rev a) = length (rev apTs)"; by simp; - - with x; - have "G \\ (rev a, y) <=s (rev apTs, y') \\ G \\ (b # c, y) <=s (X # ST', y')"; - by - (rule sup_state_append_fst [elimify], blast+); - - 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 - proof (cases "X = NT"); - case True; - with x2; - have "b = NT"; by (clarsimp_tac simp add: widen_NT); - - with rac l lapTs; - have "?P s"; by auto; - thus ?thesis; by blast; - - next; - case False; - - with wtl; - have "\\C. X = Class C"; by clarsimp_tac; - with x2; - have "\\r. b = RefT r"; by (auto simp add: widen_Class); - - thus ?thesis; - proof elim; - fix r; - assume b: "b = RefT r"; - show ?thesis; - proof (cases r); - case NullT; - with b rac x2 l lapTs wtl False; - have "?P s"; by auto; - thus ?thesis; by blast; - next; - case ClassT; - - from False wtl; - have wtlC: "?ClassC"; by simp; - - with b ClassT; - show ?thesis; - proof (elim exE conjE); - fix C D rT body; - assume ClassC: "X = Class C"; - assume zip: "\\x\\set (zip apTs list). x \\ widen G"; - assume s1': "(rT # ST', y') = s1'"; - assume s: "G \\ s1' <=s s"; - assume method: "method (G, C) (mname, list) = Some (D, rT, body)"; - - from ClassC b ClassT x2; - have "G \\ cname \\C C"; by simp; - with method wfp; - have "\\D' rT' b'. method (G, cname) (mname, list) = Some (D', rT', b') \\ G \\ rT'\\rT"; - by - (rule subcls_widen_methd, blast); - - thus ?thesis; - proof elim; - fix D' rT' body'; - assume method': "method (G, cname) (mname, list) = Some (D', rT', body')" "G\\rT'\\rT"; - - have "?P (rT'#c,y)" (is "(\\ apTs X ST'. ?A apTs X ST') \\ ?B"); - proof (intro conjI); - from s1' method' x2; - show "?B"; by (auto simp add: sup_state_Cons1); - - from b ClassT rac l lapTs method'; - have "?A a (Class cname) c"; - proof (simp, intro conjI); - - from method' x2; - have s': "G \\ (rT' # c, y) <=s (rT # ST', y')"; - by (auto simp add: sup_state_Cons1); - from s s1'; - have "G \\ (rT # ST', y') <=s s"; by simp; - with s'; - show "G \\ (rT' # c, y) <=s s"; by (rule sup_state_trans); - - from x2; - have 1: "G \\ map Some a <=l map Some apTs"; by (simp add: sup_state_def); - from lapTs zip; - have "G \\ map Some apTs <=l map Some list"; by (simp add: all_widen_is_sup_loc); - with 1; - have "G \\ map Some a <=l map Some list"; by (rule sup_loc_trans); - with l lapTs; - show "\\x\\set (zip a list). x \\ widen G"; by (simp add: all_widen_is_sup_loc); - - qed; - thus "\\ apTs X ST'. ?A apTs X ST'"; by blast; - qed; - thus ?thesis; by blast; - qed - qed - qed - qed + option_filter_n ls P (Suc n) ! m' = Some (ls ! m')" + with m Suc + show ?thesis by auto 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"); -proof (induct "?P" b); - show "?P []"; by simp; +lemma is_approx_option_filter: "is_approx (option_filter l P) l" + by (simp add: option_filter_def is_approx_option_filter_n) + +lemma option_filter_Some: +"\\n < length l; P n\\ \\ option_filter l P ! n = Some (l!n)" +proof - + + assume 1: "n < length l" "P n" + + have "\\n n'. n < length l \\ P (n+n') \\ option_filter_n l P n' ! n = Some (l!n)" + (is "?P l") + proof (induct l) + show "?P []" by simp - case Cons; - show "?P (a#list)"; - proof (clarsimp_tac simp add: list_all2_Cons1 sup_loc_def); - fix z zs n; - assume * : - "G \\ a <=o z" "list_all2 (sup_ty_opt G) list zs" - "n < Suc (length zs)" "(z # zs) ! n = Some t"; + fix l ls assume Cons: "?P ls" + show "?P (l#ls)" + proof (intro) + fix n n' + assume l: "n < length (l # ls)" + assume P: "P (n + n')" + show "option_filter_n (l # ls) P n' ! n = Some ((l # ls) ! n)" + proof (cases "n") + assume "n=0" + with P show ?thesis by simp + next + fix m assume "n = Suc m" + with l P Cons + show ?thesis by simp + qed + qed + qed + + with 1 + show ?thesis by (auto simp add: option_filter_def) +qed + +lemma option_filter_contains_dead: +"contains_dead ins (option_filter phi (mdot ins)) phi pc" + by (auto intro: option_filter_Some simp add: contains_dead_def mdot_def maybe_dead_def) - show "(\\t. (a # list) ! n = Some t) \\ G \\(a # list) ! n <=o Some t"; - proof (cases n); - case 0; - with *; show ?thesis; by (simp add: sup_ty_opt_some); - next; - case Suc; - with Cons *; - show ?thesis; by (simp add: sup_loc_def); - qed; - qed; -qed; +lemma option_filter_contains_targets: +"pc < length ins \\ contains_targets ins (option_filter phi (mdot ins)) phi pc" +proof (unfold contains_targets_def, clarsimp) + + fix pc' + assume "pc < length ins" + "pc' \\ succs (ins ! pc) pc" + "pc' \\ Suc pc" and + pc': "pc' < length phi" + + hence "is_target ins pc'" by (auto simp add: is_target_def) + + with pc' + show "option_filter phi (mdot ins) ! pc' = Some (phi ! pc')" + by (auto intro: option_filter_Some simp add: mdot_def) +qed + + +lemma fits_make_cert: + "length ins < length phi \\ fits ins (make_cert ins phi) phi" +proof - + assume l: "length ins < length phi" -lemma mono_load: -"\\G \\ (a, b) <=s (x, y); n < length y; y!n = Some t\\ \\ \\ts. b!n = Some ts \\ G \\ (ts#a, b) <=s (t#x, y)"; -proof (clarsimp_tac simp add: sup_state_def); - assume "G \\ b <=l y" "n < length y" "y!n = Some t"; - thus "\\ts. b ! n = Some ts \\ G\\ts\\t"; - by (rule sup_loc_some [rulify, elimify], clarsimp_tac); -qed; - -lemma mono_store: -"\\G \\ (a, b) <=s (ts # ST', y); n < length y\\ \\ - \\ t a'. a = t#a' \\ G \\ (a', b[n := Some t]) <=s (ST', y[n := Some ts])"; -proof (clarsimp_tac simp add: sup_state_def sup_loc_Cons2); - fix Y YT'; - assume * : "n < length y" "G \\ b <=l y" "G \\Y <=o Some ts" "G \\ YT' <=l map Some ST'"; - assume "map Some a = Y # YT'"; - hence "map Some (tl a) = YT' \\ Some (hd a) = Y \\ (\\y yt. a = y # yt)"; - by (rule map_hd_tl); - with *; - show "\\t a'. a = t # a' \\ G \\ map Some a' <=l map Some ST' \\ G \\ b[n := Some t] <=l y[n := Some ts]"; - by (clarsimp_tac simp add: sup_loc_update); -qed; + thus "fits ins (make_cert ins phi) phi" + proof (unfold fits_def make_cert_def, intro conjI allI impI) + show "is_approx (option_filter phi (mdot ins)) phi" + by (rule is_approx_option_filter) + + show "length ins < length phi" . + + fix pc + show "contains_dead ins (option_filter phi (mdot ins)) phi pc" + by (rule option_filter_contains_dead) + + assume "pc < length ins" + thus "contains_targets ins (option_filter phi (mdot ins)) phi pc" + by (rule option_filter_contains_targets) + qed +qed + +lemma fitsD: +"\\fits ins cert phi; pc' \\ succs (ins!pc) pc; pc' \\ Suc pc; pc < length ins; pc' < length ins\\ + \\ cert!pc' = Some (phi!pc')" +by (clarsimp simp add: fits_def contains_dead_def contains_targets_def) + +lemma fitsD2: +"\\fits ins cert phi; Suc pc \\ succs (ins!pc) pc; pc < length ins\\ + \\ cert ! Suc pc = Some (phi ! Suc pc)" +by (clarsimp simp add: fits_def contains_dead_def contains_targets_def) -lemma PrimT_PrimT: "(G \\ xb \\ PrimT p) = (xb = PrimT p)"; -proof; - show "xb = PrimT p \\ G \\ xb \\ PrimT p"; by blast; - show "G\\ xb \\ PrimT p \\ xb = PrimT p"; - proof (cases xb); - fix prim; - assume "xb = PrimT prim" "G\\xb\\PrimT p"; - thus ?thesis; by simp; - next; - fix ref; - assume "G\\xb\\PrimT p" "xb = RefT ref"; - thus ?thesis; by simp (rule widen_RefT [elimify], auto); - qed; -qed; +lemmas [trans] = sup_state_trans - -lemma wtl_inst_pseudo_mono: +lemma wtl_inst_mono: "\\wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins; wf_prog wf_mb G; G \\ s2 <=s s1; i = ins!pc\\ \\ - \\ s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \\ (G \\ s2' <=s s1' \\ (\\s. cert!(Suc pc) = Some s \\ G \\ s2' <=s s))"; -proof (simp only:); - assume 1 : "wtl_inst (ins ! pc) G rT s1 s1' cert mpc pc" "G \\ s2 <=s s1" "pc < length ins"; - assume 2 : "fits ins cert phi" "wf_prog wf_mb G" "i = ins!pc"; + \\ s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \\ (G \\ s2' <=s s1')"; +proof - + assume pc: "pc < length ins" "i = ins!pc" + assume wtl: "wtl_inst i G rT s1 s1' cert mpc pc" + assume fits: "fits ins cert phi" + assume G: "G \\ s2 <=s s1" + + let "?step s" = "step (i, G, s)" - have 3: "\\ a b. s2 = (a,b)"; by simp; - - show ?thesis; - proof (cases "ins ! pc", insert 1, insert 3); + from wtl G + have app: "app (i, G, rT, s2)" by (auto simp add: wtl_inst_def app_mono) + + from wtl G + have step: "succs i pc \\ {} \\ G \\ the (?step s2) <=s the (?step s1)" + by - (drule step_mono, auto simp add: wtl_inst_def) + + with app + have some: "succs i pc \\ {} \\ ?step s2 \\ None" by (simp add: app_step_some) - 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 (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 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); + { + fix pc' + assume 0: "pc' \\ succs i pc" "pc' \\ pc+1" + hence "succs i pc \\ {}" by auto + hence "G \\ the (?step s2) <=s the (?step s1)" by (rule step) + also + from wtl 0 + have "G \\ the (?step s1) <=s the (cert!pc')" + by (auto simp add: wtl_inst_def) + finally + have "G\\ the (?step s2) <=s the (cert!pc')" . + } note cert = this + + have "\\s2'. wtl_inst i G rT s2 s2' cert mpc pc \\ G \\ s2' <=s s1'" + proof (cases "pc+1 \\ succs i pc") + case True + with wtl + have s1': "s1' = the (?step s1)" by (simp add: wtl_inst_def) - 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; + have "wtl_inst i G rT s2 (the (?step s2)) cert mpc pc \\ G \\ (the (?step s2)) <=s s1'" + (is "?wtl \\ ?G") + proof + from True s1' + show ?G by (auto intro: step) + + from True app wtl + show ?wtl + by (clarsimp intro: cert simp add: wtl_inst_def) 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 Return; - with 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 - next - case Goto; - with 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 \\ s1 <=s (x, y)"; - thus "G \\ (a, b) <=s (x, y)"; by (rule sup_state_trans); - qed + thus ?thesis by blast next - case Ifcmpeq; - with 1 3; - show ?thesis - proof (elim, clarsimp_tac simp add: sup_state_Cons2, intro conjI); - fix xt' b ST' y c d; - assume "G \\ (xt', b) <=s (ST', y)" "G \\ (ST', y) <=s (c, d)"; - thus "G \\ (xt', b) <=s (c, d)"; by (rule sup_state_trans); - next; - fix ts ts' x xa; - assume * : - "(\\p. ts = PrimT p \\ ts' = PrimT p) \\ (\\r. ts = RefT r) \\ (\\r'. ts' = RefT r')"; - - assume x: "G\\x\\ts" "G\\xa\\ts'"; - - show "(\\p. x = PrimT p \\ xa = PrimT p) \\ (\\r. x = RefT r) \\ (\\r'. xa = RefT r')"; - proof (cases x); - case PrimT; - with * x; - show ?thesis; by (auto simp add: PrimT_PrimT); - next; - case RefT; - hence 1: "\\r. x = RefT r"; by blast; - - have "\\r'. xa = RefT r'"; - proof (cases xa); - case PrimT; - with RefT * x; - have "False"; by auto (rule widen_RefT [elimify], auto); - thus ?thesis; by blast; - qed blast; + case False + with wtl + have "s1' = the (cert ! Suc pc)" by (simp add: wtl_inst_def) - with 1 - show ?thesis by blast - qed - qed - qed (elim, clarsimp_tac simp add: sup_state_Cons1 sup_state_Cons2 PrimT_PrimT)+ -qed - -lemma wtl_inst_last_mono: -"\\wtl_inst i G rT s1 s1' cert (Suc pc) pc; G \\ s2 <=s s1\\ \\ - \\s2'. wtl_inst i G rT s2 s2' cert (Suc pc) pc \\ (G \\ s2' <=s s1')"; -proof -; - assume * : "wtl_inst i G rT s1 s1' cert (Suc pc) pc" "G \\ s2 <=s s1"; + with False app wtl + have "wtl_inst i G rT s2 s1' cert mpc pc \\ G \\ s1' <=s s1'" + by (clarsimp intro: cert simp add: wtl_inst_def) + + thus ?thesis by blast + qed - show ?thesis - proof (cases i, insert *) - case Return with * - show ?thesis - by (clarsimp_tac simp del: split_paired_Ex simp add: sup_state_Cons2) - (rule widen_trans, blast+); - next - case Goto with * - show ?thesis - by (clarsimp_tac simp del: split_paired_Ex simp add: sup_state_Cons2) - (rule sup_state_trans, blast+); - qed auto + with pc show ?thesis by simp qed - - -lemma wtl_option_last_mono: -"\\wtl_inst_option i G rT s1 s1' cert mpc pc; mpc = Suc pc; G \\ s2 <=s s1\\ \\ - \\s2'. wtl_inst_option i G rT s2 s2' cert mpc pc \\ (G \\ s2' <=s s1')"; -proof (simp only: ); - assume G: "G \\ s2 <=s s1"; - assume w: "wtl_inst_option i G rT s1 s1' cert (Suc pc) pc"; - - show "\\s2'. wtl_inst_option i G rT s2 s2' cert (Suc pc) pc \\ (G \\ s2' <=s s1')"; - proof (cases "cert!pc"); - case None; - with G w; - show ?thesis; by (simp add: wtl_inst_option_def wtl_inst_last_mono del: split_paired_Ex); - next; - case Some; - with G w; - have o: "G \\ s1 <=s a \\ wtl_inst i G rT a s1' cert (Suc pc) pc"; - by (simp add: wtl_inst_option_def); - hence w' : "wtl_inst i G rT a s1' cert (Suc pc) pc"; ..; - - from o G; - have G' : "G \\ s2 <=s a"; by - (rule sup_state_trans, blast+); - - from o; - have "\\s2'. wtl_inst i G rT a s2' cert (Suc pc) pc \\ G \\ s2' <=s s1'"; - by elim (rule wtl_inst_last_mono, auto); - - with Some w G'; - show ?thesis; by (auto simp add: wtl_inst_option_def); - qed; -qed; - + + lemma wt_instr_imp_wtl_inst: "\\wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi; pc < length ins; length ins = max_pc\\ \\ \\ s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\ G \\ s <=s phi ! Suc pc"; proof - - assume * : "wt_instr (ins!pc) G rT phi max_pc pc" "fits ins cert phi" - "pc < length ins" "length ins = max_pc" + assume wt: "wt_instr (ins!pc) G rT phi max_pc pc" + assume fits: "fits ins cert phi" + assume pc: "pc < length ins" "length ins = max_pc" + + from wt + have app: "app (ins!pc, G, rT, phi!pc)" by (simp add: wt_instr_def); + + from wt pc + have pc': "!!pc'. pc' \\ succs (ins!pc) pc \\ pc' < length ins" + by (simp add: wt_instr_def) - have xy: "\\ x y. phi!pc = (x,y)" by simp + let ?s' = "the (step (ins!pc,G, phi!pc))" + + from wt + have G: "!!pc'. pc' \\ succs (ins!pc) pc \\ G \\ ?s' <=s phi ! pc'" + by (simp add: wt_instr_def) + + from wt fits pc + have cert: "!!pc'. \\pc' \\ succs (ins!pc) pc; pc' < max_pc; pc' \\ pc+1\\ + \\ cert!pc' \\ None \\ G \\ ?s' <=s the (cert!pc')" + by (auto dest: fitsD simp add: wt_instr_def simp del: split_paired_Ex) show ?thesis - proof (cases "ins!pc", insert *, insert xy); - case Return with * xy - show ?thesis - by (elim, clarsimp_tac simp add: fits_def contains_dead_def simp del: split_paired_Ex); - next - case Goto with * xy - show ?thesis; - by (clarsimp_tac simp add: fits_def contains_dead_def contains_targets_def simp del: split_paired_Ex); - next - case Ifcmpeq with * xy - show ?thesis; - by (clarsimp_tac simp add: fits_def contains_dead_def contains_targets_def simp del: split_paired_Ex); - next - case Invoke with * xy - show ?thesis - proof (elim, clarsimp_tac simp del: split_paired_Ex) - fix y apTs X ST'; - assume pc : "Suc pc < length ins"; - assume phi : "phi ! pc = (rev apTs @ X # ST', y)" "length apTs = length list"; - assume ** : - "X = NT \\ (\\C. X = Class C \\ - (\\x\\set (zip apTs list). x \\ widen G) \\ - (\\D rT. (\\b. method (G, C) (mname, list) = Some (D, rT, b)) \\ G \\ (rT # ST', y) <=s phi ! Suc pc))" - (is "?NT \\ ?CL"); - - from Invoke pc *; - have cert: "cert ! Suc pc = Some (phi ! Suc pc)"; by (clarsimp_tac simp add: fits_def contains_dead_def); + proof (cases "pc+1 \\ succs (ins!pc) pc") + case True + + have "wtl_inst (ins!pc) G rT (phi!pc) ?s' cert max_pc pc \\ G \\ ?s' <=s phi ! Suc pc" (is "?wtl \\ ?G") + proof + from True + show "G \\ ?s' <=s phi ! Suc pc" by (simp add: G) + + from True fits app pc cert pc' + show "?wtl" + by (auto simp add: wtl_inst_def) + qed - show "\\s. (\\apTsa Xa ST'a. - rev apTs @ X # ST' = rev apTsa @ Xa # ST'a \\ - length apTsa = length list \\ - (\\s''. cert ! Suc pc = Some s'' \\ - (s'' = s \\ Xa = NT \\ - G \\ s <=s s'' \\ - (\\C. Xa = Class C \\ - (\\x\\set (zip apTsa list). x \\ widen G) \\ - (\\D rT. (\\b. method (G, C) (mname, list) = Some (D, rT, b)) \\ (rT # ST'a, y) = s))))) \\ - G \\ s <=s phi ! Suc pc" (is "\\s. ?P s"); - proof (cases "X=NT"); - case True - with cert phi ** - have "?P (phi ! Suc pc)" by (force simp del: split_paired_Ex) - thus ?thesis by blast - next - case False - with ** + thus ?thesis by blast + + next + let ?s'' = "the (cert ! Suc pc)" - have "?CL" by simp + case False + with fits app pc cert pc' + have "wtl_inst (ins ! pc) G rT (phi ! pc) ?s'' cert max_pc pc \\ G \\ ?s'' <=s phi ! Suc pc" + by (auto dest: fitsD2 simp add: wtl_inst_def) - thus ?thesis - proof (elim exE conjE); - fix C D rT b; - assume "X = Class C" "\\x\\set (zip apTs list). x \\ widen G" - "G \\ (rT # ST', y) <=s phi ! Suc pc" - "method (G, C) (mname, list) = Some (D, rT, b)"; - with cert phi; - have "?P (rT #ST', y)" by (force simp del: split_paired_Ex) - thus ?thesis by blast - qed - qed - qed - qed (elim, force)+ + thus ?thesis by blast + qed qed @@ -764,51 +348,49 @@ case Some; from fits; - have "pc < length phi"; by (clarsimp_tac simp add: fits_def); + have "pc < length phi"; by (clarsimp simp add: fits_def); with fits Some; have "cert ! pc = Some (phi!pc)"; by (auto simp add: fits_def is_approx_def); with *; show ?thesis; by (simp add: wtl_inst_option_def); - qed; -qed; + qed +qed -lemma wtl_option_pseudo_mono: +lemma wtl_option_mono: "\\wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins; wf_prog wf_mb G; G \\ s2 <=s s1; i = ins!pc\\ \\ - \\ s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\ - (G \\ s2' <=s s1' \\ (\\s. cert!(Suc pc) = Some s \\ G \\ s2' <=s s))"; -proof -; + \\ s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\ (G \\ s2' <=s s1')" +proof - assume wtl: "wtl_inst_option i G rT s1 s1' cert mpc pc" and fits: "fits ins cert phi" "pc < length ins" - "wf_prog wf_mb G" "G \\ s2 <=s s1" "i = ins!pc"; + "wf_prog wf_mb G" "G \\ s2 <=s s1" "i = ins!pc" - show ?thesis; - proof (cases "cert!pc"); - case None; + show ?thesis + proof (cases "cert!pc") + case None with wtl fits; show ?thesis; - by - (rule wtl_inst_pseudo_mono [elimify], (simp add: wtl_inst_option_def)+); - next; - case Some; + by - (rule wtl_inst_mono [elimify], (simp add: wtl_inst_option_def)+); + next + case Some with wtl fits; - have G: "G \\ s2 <=s a"; - by - (rule sup_state_trans, (simp add: wtl_inst_option_def)+); + have G: "G \\ s2 <=s a" + by - (rule sup_state_trans, (simp add: wtl_inst_option_def)+) - from Some wtl; - have "wtl_inst i G rT a s1' cert mpc pc"; by (simp add: wtl_inst_option_def); + from Some wtl + have "wtl_inst i G rT a s1' cert mpc pc"; by (simp add: wtl_inst_option_def) - with G fits; - have "\\ s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \\ - (G \\ s2' <=s s1' \\ (\\s. cert!(Suc pc) = Some s \\ G \\ s2' <=s s))"; - by - (rule wtl_inst_pseudo_mono, (simp add: wtl_inst_option_def)+); + with G fits + have "\\ s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \\ (G \\ s2' <=s s1')" + by - (rule wtl_inst_mono, (simp add: wtl_inst_option_def)+); with Some G; show ?thesis; by (simp add: wtl_inst_option_def); qed -qed; +qed (* main induction over instruction list *) @@ -854,7 +436,7 @@ with Nil 1 2 5; have "\\s'. wtl_inst_option a G rT s s' cert (Suc (length l)) pc"; - by elim (rule wtl_option_pseudo_mono [elimify], force+); + by elim (rule wtl_option_mono [elimify], force+); with Nil 2; show ?thesis; by auto; @@ -875,15 +457,15 @@ by - (rule wt_instr_imp_wtl_option [elimify], assumption+, simp+); hence "\\s1. wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc \\ - (G \\ s1 <=s (phi ! (Suc pc)) \\ (\\s. cert ! Suc pc = Some s \\ G \\ s1 <=s s))"; + (G \\ s1 <=s (phi ! (Suc pc)))" (* \\ (\\s. cert ! Suc pc = Some s \\ G \\ s1 <=s s))"; *) proof elim; fix s1'; assume "wtl_inst_option a G rT (phi!pc) s1' cert (Suc (pc + length list)) pc" and a :"G \\ s1' <=s phi ! Suc pc"; with 1 2 5; have "\\s1. wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc \\ - ((G \\ s1 <=s s1') \\ (\\s. cert ! Suc pc = Some s \\ G \\ s1 <=s s))"; - by - (rule wtl_option_pseudo_mono [elimify], simp+); + ((G \\ s1 <=s s1'))" (* \\ (\\s. cert ! Suc pc = Some s \\ G \\ s1 <=s s))"; *) + by - (rule wtl_option_mono [elimify], simp+); with a; show ?thesis; @@ -892,51 +474,23 @@ assume "G \\ s1 <=s s1'" "G \\ s1' <=s phi ! Suc pc"; show "G \\ s1 <=s phi ! Suc pc"; by (rule sup_state_trans); qed auto; - qed; + qed - thus ?thesis; + thus ?thesis proof (elim exE conjE); fix s1; assume wto: "wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc"; - assume Gs1: "G \\ s1 <=s phi ! Suc pc \\ (\\s. cert ! Suc pc = Some s \\ G \\ s1 <=s s)"; + assume Gs1: "G \\ s1 <=s phi ! Suc pc" (* \\ (\\s. cert ! Suc pc = Some s \\ G \\ s1 <=s s)"; *) - have "\\s'. wtl_inst_list list G rT s1 s' cert ((Suc pc)+length list) (Suc pc)"; - proof (cases "G \\ s1 <=s phi ! Suc pc"); - case True; - with Gs1; - have "G \\ s1 <=s phi ! Suc pc"; by simp; - with *; - show ?thesis; by blast; - next; - case False; - with Gs1; - have "\\c. cert ! Suc pc = Some c \\ G \\ s1 <=s c"; by simp; - thus ?thesis; - proof elim; - from 1 2 Cons Cons2; - have "Suc pc < length phi"; by (clarsimp_tac simp add: fits_def is_approx_def); + with * + have "\\s'. wtl_inst_list list G rT s1 s' cert ((Suc pc)+length list) (Suc pc)"; by blast - with 1; - have cert: "cert ! (Suc pc) = None \\ cert ! (Suc pc) = Some (phi ! Suc pc)"; - by (clarsimp_tac simp add: fits_def is_approx_def); - - fix c; - assume "cert ! Suc pc = Some c"; - with cert; - have c: "c = phi ! Suc pc"; by simp; - assume "G \\ s1 <=s c"; - with c; - have "G \\ s1 <=s phi ! Suc pc"; by simp; - with *; - show ?thesis; by blast; - qed; - qed; with wto; show ?thesis; by (auto simp del: split_paired_Ex); - qed; - qed; - qed; -qed; + qed + qed + qed +qed lemma fits_imp_wtl_method_complete: @@ -991,12 +545,12 @@ from 1; show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))"; - proof (rule bspec [elimify], clarsimp_tac); + proof (rule bspec [elimify], clarsimp); assume ub : "unique b"; assume m: "\\(sig,rT,mb)\\set b. wf_mhead G sig rT \\ (\\(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb"; from m b; show ?thesis; - proof (rule bspec [elimify], clarsimp_tac); + proof (rule bspec [elimify], clarsimp); assume "wt_method G a ba ad ae bb (Phi a (ac, ba))"; with wfprog uG ub b 1; show ?thesis; @@ -1004,6 +558,7 @@ qed; qed; qed; -qed; +qed -end; + +end diff -r 15bee2731e43 -r 40d64cb4f4e6 src/HOL/MicroJava/BV/LBVCorrect.thy --- a/src/HOL/MicroJava/BV/LBVCorrect.thy Mon Aug 07 10:29:54 2000 +0200 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Mon Aug 07 14:32:56 2000 +0200 @@ -6,7 +6,7 @@ header {* Correctness of the LBV *} -theory LBVCorrect = LBVSpec:; +theory LBVCorrect = BVSpec + LBVSpec: constdefs fits_partial :: "[method_type,nat,instr list,jvm_prog,ty,state_type,state_type,certificate] \\ bool" @@ -17,7 +17,7 @@ (\\ t. cert!(pc+length a) = Some t \\ phi!(pc+length a) = t)))" fits :: "[method_type,instr list,jvm_prog,ty,state_type,state_type,certificate] \\ bool" -"fits phi is G rT s0 s2 cert \\ fits_partial phi 0 is G rT s0 s2 cert"; +"fits phi is G rT s0 s2 cert \\ fits_partial phi 0 is G rT s0 s2 cert" lemma fitsD: "fits phi is G rT s0 s2 cert \\ @@ -25,123 +25,126 @@ wtl_inst_list a G rT s0 s1 cert (0+length is) 0 \\ wtl_inst_list (i#b) G rT s1 s2 cert (0+length is) (0+length a) \\ ((cert!(0+length a) = None \\ phi!(0+length a) = s1) \\ - (\\ t. cert!(0+length a) = Some t \\ phi!(0+length a) = t))"; -by (unfold fits_def fits_partial_def) blast; + (\\ t. cert!(0+length a) = Some t \\ phi!(0+length a) = t))" +by (unfold fits_def fits_partial_def) blast -lemma exists_list: "\\l. n < length l" (is "?Q n"); -proof (induct "n"); - fix n; assume "?Q n"; - thus "?Q (Suc n)"; - proof elim; - fix l; assume "n < length (l::'a list)"; - hence "Suc n < length (a#l)"; by simp; - thus ?thesis; ..; - qed; -qed auto; +lemma exists_list: "\\l. n < length l" (is "?Q n") +proof (induct "n") + fix n; assume "?Q n" + thus "?Q (Suc n)" + proof elim + fix l assume "n < length (l::'a list)" + hence "Suc n < length (a#l)" by simp + thus ?thesis .. + qed +qed auto lemma exists_phi: "wtl_inst_list is G rT s0 s2 cert (length is) 0 \\ - \\ phi. fits phi is G rT s0 s2 cert \\ length is < length phi"; -proof -; - assume all: "wtl_inst_list is G rT s0 s2 cert (length is) 0"; + \\ phi. fits phi is G rT s0 s2 cert \\ length is < length phi" +proof - + assume all: "wtl_inst_list is G rT s0 s2 cert (length is) 0" have "\\ s0 pc. wtl_inst_list is G rT s0 s2 cert (pc+length is) pc \\ (\\ phi. pc + length is < length phi \\ fits_partial phi pc is G rT s0 s2 cert)" - (is "?P is"); - proof (induct "?P" "is"); - case Nil; - show "?P []"; by (simp add: fits_partial_def exists_list); - case Cons; - show "?P (a#list)"; - proof (intro allI impI); - fix s0 pc; - assume wtl: "wtl_inst_list (a # list) G rT s0 s2 cert (pc + length (a # list)) pc"; - thus "\\phi. pc + length (a # list) < length phi \\ - fits_partial phi pc (a # list) G rT s0 s2 cert"; - obtain s1 where - opt: "wtl_inst_option a G rT s0 s1 cert (Suc pc + length list) pc" and - wtlSuc: "wtl_inst_list list G rT s1 s2 cert (Suc pc + length list) (Suc pc)"; - by auto; - with Cons; - show ?thesis; - obtain phi where fits: "fits_partial phi (Suc pc) list G rT s1 s2 cert" - and length: "(Suc pc) + length list < length phi"; by blast; - let "?A phi pc x s1'" = - "(cert ! (pc + length (x::instr list)) = None \\ phi ! (pc + length x) = s1') \\ - (\\t. cert ! (pc + length x) = Some t \\ phi ! (pc + length x) = t)"; - show ?thesis; - proof (cases "cert!pc"); - case None; - have "fits_partial (phi[pc:= s0]) pc (a # list) G rT s0 s2 cert"; - proof (unfold fits_partial_def, intro allI impI); - fix x i y s1'; - assume * : - "x @ i # y = a # list" - "wtl_inst_list x G rT s0 s1' cert (pc + length (a # list)) pc" - "wtl_inst_list (i # y) G rT s1' s2 cert (pc + length (a # list)) (pc + length x)"; - show "?A (phi[pc:= s0]) pc x s1'"; - proof (cases "x"); - assume "x = []"; - with * length None; - show ?thesis; by simp; - next; - fix b l; assume Cons: "x = b#l"; - with fits *; - have "?A (phi[pc:= s0]) (Suc pc) l s1'"; - proof (unfold fits_partial_def, elim allE impE); - from * Cons; - show "l @ i # y = list"; by simp; - from Cons opt *; - show "wtl_inst_list l G rT s1 s1' cert (Suc pc + length list) (Suc pc)"; - by (simp, elim) (drule wtl_inst_option_unique, assumption, simp); - qed simp+; - with Cons length; - show ?thesis; by auto; - qed; - qed; - with length; - show ?thesis; by intro auto; - next; - fix c; assume Some: "cert!pc = Some c"; - have "fits_partial (phi[pc:= c]) pc (a # list) G rT s0 s2 cert"; - proof (unfold fits_partial_def, intro allI impI); - fix x i y s1'; - assume * : - "x @ i # y = a # list" - "wtl_inst_list x G rT s0 s1' cert (pc + length (a # list)) pc" - "wtl_inst_list (i # y) G rT s1' s2 cert (pc + length (a # list)) (pc + length x)"; - show "?A (phi[pc:= c]) pc x s1'"; - proof (cases "x"); - assume "x = []"; - with length Some; - show ?thesis; by simp; - next; - fix b l; assume Cons: "x = b#l"; - with fits *; - have "?A (phi[pc:= c]) (Suc pc) l s1'"; - proof (unfold fits_partial_def, elim allE impE); - from * Cons; - show "l @ i # y = list"; by simp; - from Cons opt *; - show "wtl_inst_list l G rT s1 s1' cert (Suc pc + length list) (Suc pc)"; - by (simp, elim) (drule wtl_inst_option_unique, assumption, simp); - qed simp+; - with Cons length; - show ?thesis; by auto; - qed; - qed; - with length; - show ?thesis; by intro auto; - qed; - qed; - qed; - qed; - qed; - with all; - show ?thesis; - 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; + (is "?P is") + proof (induct "?P" "is") + case Nil + show "?P []" by (simp add: fits_partial_def exists_list) + case Cons + show "?P (a#list)" + proof (intro allI impI) + fix s0 pc + assume wtl: "wtl_inst_list (a # list) G rT s0 s2 cert (pc + length (a # list)) pc" + + from this + obtain s1 where + opt: "wtl_inst_option a G rT s0 s1 cert (Suc pc + length list) pc" and + wtlSuc: "wtl_inst_list list G rT s1 s2 cert (Suc pc + length list) (Suc pc)" + by auto + + with Cons + obtain phi where + fits: "fits_partial phi (Suc pc) list G rT s1 s2 cert" and + length: "(Suc pc) + length list < length phi" + by blast + + let "?A phi pc x s1'" = + "(cert ! (pc + length (x::instr list)) = None \\ phi ! (pc + length x) = s1') \\ + (\\t. cert ! (pc + length x) = Some t \\ phi ! (pc + length x) = t)" + + show "\\phi. pc + length (a # list) < length phi \\ + fits_partial phi pc (a # list) G rT s0 s2 cert" + proof (cases "cert!pc") + case None + have "fits_partial (phi[pc:= s0]) pc (a # list) G rT s0 s2 cert" + proof (unfold fits_partial_def, intro allI impI) + fix x i y s1' + assume * : + "x @ i # y = a # list" + "wtl_inst_list x G rT s0 s1' cert (pc + length (a # list)) pc" + "wtl_inst_list (i # y) G rT s1' s2 cert (pc + length (a # list)) (pc + length x)" + show "?A (phi[pc:= s0]) pc x s1'" + proof (cases "x") + assume "x = []" + with * length None + show ?thesis by simp + next + fix b l assume Cons: "x = b#l" + with fits * + have "?A (phi[pc:= s0]) (Suc pc) l s1'" + proof (unfold fits_partial_def, elim allE impE) + from * Cons + show "l @ i # y = list" by simp + from Cons opt * + show "wtl_inst_list l G rT s1 s1' cert (Suc pc + length list) (Suc pc)" + by (simp, elim) (drule wtl_inst_option_unique, assumption, simp) + qed simp+ + with Cons length + show ?thesis by auto + qed + qed + with length + show ?thesis by intro auto + next + fix c assume Some: "cert!pc = Some c" + have "fits_partial (phi[pc:= c]) pc (a # list) G rT s0 s2 cert" + proof (unfold fits_partial_def, intro allI impI) + fix x i y s1' + assume * : + "x @ i # y = a # list" + "wtl_inst_list x G rT s0 s1' cert (pc + length (a # list)) pc" + "wtl_inst_list (i # y) G rT s1' s2 cert (pc + length (a # list)) (pc + length x)" + show "?A (phi[pc:= c]) pc x s1'" + proof (cases "x") + assume "x = []" + with length Some + show ?thesis by simp + next + fix b l assume Cons: "x = b#l" + with fits * + have "?A (phi[pc:= c]) (Suc pc) l s1'" + proof (unfold fits_partial_def, elim allE impE) + from * Cons + show "l @ i # y = list" by simp + from Cons opt * + show "wtl_inst_list l G rT s1 s1' cert (Suc pc + length list) (Suc pc)" + by (simp, elim) (drule wtl_inst_option_unique, assumption, simp) + qed simp+ + with Cons length + show ?thesis by auto + qed + qed + with length + show ?thesis by intro auto + qed + qed + qed + with all + show ?thesis + 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 lemma fits_lemma1: @@ -205,38 +208,38 @@ "wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)" and w: "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))"; hence a: "wtl_inst_list (a@[i]) G rT s0 s2 cert (length (a@i#b)) 0"; by (rule wtl_append); - assume "b \\ []"; - thus "G \\ s2 <=s phi ! Suc (length a)"; - obtain b' bs where Cons: "b = b' # bs"; by (simp add: neq_Nil_conv) (elim exE, rule that); - hence "(a@[i]) @ b' # bs = a @ i # b"; by simp; - with f; - show ?thesis; - proof (rule fitsD [elimify]); - from Cons w; - show "wtl_inst_list (b' # bs) G rT s2 s3 cert (0 + length (a @ i # b)) (0 + length (a @ [i]))"; - by simp; - from a; - show "wtl_inst_list (a @ [i]) G rT s0 s2 cert (0 + length (a @ i # b)) 0"; by simp; + assume "b \\ []" - assume cert: - "(cert ! (0 + length (a @ [i])) = None \\ phi ! (0 + length (a @ [i])) = s2) \\ - (\\t. cert ! (0 + length (a @ [i])) = Some t \\ phi ! (0 + length (a @ [i])) = t)"; - show ?thesis; - proof (cases "cert ! Suc (length a)"); - assume "cert ! Suc (length a) = None"; - with cert; - have "s2 = phi ! Suc (length a)"; by simp; - thus ?thesis; by simp; - next; - fix t; assume "cert ! Suc (length a) = Some t"; - with cert; - have "phi ! Suc (length a) = t"; by (simp del: split_paired_All); - with cert Cons w; - show ?thesis; by (auto simp add: wtl_inst_option_def); - qed; - qed; - qed; -qed; + from this + obtain b' bs where Cons: "b = b' # bs"; by (simp add: neq_Nil_conv) (elim exE, rule that); + hence "(a@[i]) @ b' # bs = a @ i # b"; by simp; + with f + show "G \\ s2 <=s phi ! Suc (length a)"; + proof (rule fitsD [elimify]); + from Cons w; + show "wtl_inst_list (b' # bs) G rT s2 s3 cert (0 + length (a @ i # b)) (0 + length (a @ [i]))"; + by simp; + from a; + show "wtl_inst_list (a @ [i]) G rT s0 s2 cert (0 + length (a @ i # b)) 0"; by simp; + + assume cert: + "(cert ! (0 + length (a @ [i])) = None \\ phi ! (0 + length (a @ [i])) = s2) \\ + (\\t. cert ! (0 + length (a @ [i])) = Some t \\ phi ! (0 + length (a @ [i])) = t)"; + show ?thesis; + proof (cases "cert ! Suc (length a)"); + assume "cert ! Suc (length a) = None"; + with cert; + have "s2 = phi ! Suc (length a)"; by simp; + thus ?thesis; by simp; + next; + fix t; assume "cert ! Suc (length a) = Some t"; + with cert; + have "phi ! Suc (length a) = t"; by (simp del: split_paired_All); + with cert Cons w; + show ?thesis; by (auto simp add: wtl_inst_option_def) + qed + qed +qed lemma wtl_lemma: "\\wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0; @@ -270,17 +273,10 @@ have suc: "i2 \\ [] \\ G \\ s2 <=s phi ! Suc (length i1)"; by (rule wtl_suc_pc [rulify]); + with wo show ?thesis; - proof (cases i, insert suc, insert wo); - case Invoke with suc wo - show ?thesis - by - (cases "cert ! (length i1)", - clarsimp_tac simp add: c2 wtl_inst_option_def split_beta, - intro exI conjI, blast, simp, force, - clarsimp_tac simp add: c1 wtl_inst_option_def, - intro exI conjI, blast, simp, force) - qed (clarsimp_tac simp add: c1 c2 c3 wtl_inst_option_def split_beta split: option.split_asm)+ -qed; + by (auto simp add: c1 c2 c3 wt_instr_def wtl_inst_def wtl_inst_option_def split: option.split_asm) +qed lemma wtl_fits_wt: @@ -292,49 +288,55 @@ fix pc; assume wtl: "wtl_inst_list is G rT s0 s3 cert (length is) 0" and pc: "pc < length is"; + + from this + obtain i1 i2' s1 where + l: "i1 @ i2' = is" "length i1 = pc" and + w1: "wtl_inst_list i1 G rT s0 s1 cert (length is) 0" and + w2: "wtl_inst_list i2' G rT s1 s3 cert (length is) (0 + length i1)"; + by (rule wtl_partial [rulify, elimify]) (elim, rule that); - thus "wt_instr (is ! pc) G rT phi (length is) pc"; - obtain i1 i2' s1 where l: "i1 @ i2' = is" "length i1 = pc" and - w1: "wtl_inst_list i1 G rT s0 s1 cert (length is) 0" and - w2: "wtl_inst_list i2' G rT s1 s3 cert (length is) (0 + length i1)"; - by (rule wtl_partial [rulify, elimify]) (elim, rule that); - from l pc; - have "i2' \\ []"; by auto; - thus ?thesis; - obtain i i2 where c: "i2' = i#i2"; by (simp add: neq_Nil_conv) (elim, rule that); - with w2 l; - show ?thesis; - obtain s2 where w3: - "wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1)" - "wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1))"; by auto; + from l pc; + have "i2' \\ []"; by auto; + + from this + obtain i i2 where c: "i2' = i#i2" + by (simp add: neq_Nil_conv) (elim, rule that) + + with w2 l + obtain s2 + where w3: + "wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1)" + "wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1))" + by auto - from w1 l c; - have w4: "wtl_inst_list i1 G rT s0 s1 cert (length (i1 @ i # i2)) 0"; by simp; + from w1 l c + have w4: "wtl_inst_list i1 G rT s0 s1 cert (length (i1 @ i # i2)) 0" by simp + + from l c fits + have "fits phi (i1@i#i2) G rT s0 s3 cert" by simp + with w4 w3 + have "wt_instr i G rT phi (length (i1@i#i2)) (length i1)" by (rule wtl_lemma) - from l c fits; - have "fits phi (i1@i#i2) G rT s0 s3 cert"; by simp; - with w4 w3; - have "wt_instr i G rT phi (length (i1@i#i2)) (length i1)"; by (rule wtl_lemma); - with l c; - show ?thesis; by (auto simp add: nth_append); - qed; - qed; - qed; -qed; + with l c + show "wt_instr (is ! pc) G rT phi (length is) pc" + by (auto simp add: nth_append) +qed lemma wtl_inst_list_correct: "wtl_inst_list is G rT s0 s2 cert (length is) 0 \\ \\ phi. \\pc. pc < length is \\ wt_instr (is ! pc) G rT phi (length is) pc"; proof -; assume wtl: "wtl_inst_list is G rT s0 s2 cert (length is) 0"; - thus ?thesis; - obtain phi where "fits phi is G rT s0 s2 cert"; - by (rule exists_phi [elimify]) blast; - with wtl; - show ?thesis; - by (rule wtl_fits_wt [elimify]) blast; - qed; -qed; + + from this + obtain phi where "fits phi is G rT s0 s2 cert"; + by (rule exists_phi [elimify]) blast + + with wtl + show ?thesis + by (rule wtl_fits_wt [elimify]) blast; +qed lemma fits_first: "\\is \\ [];wtl_inst_list is G rT s0 s2 cert (length is) 0; @@ -342,58 +344,64 @@ proof -; assume wtl: "wtl_inst_list is G rT s0 s2 cert (length is) 0"; assume fits: "fits phi is G rT s0 s2 cert"; - assume "is \\ []"; - thus ?thesis; - obtain y ys where cons: "is = y#ys"; by (simp add: neq_Nil_conv) (elim, rule that); - from fits; - show ?thesis; - proof (rule fitsD [elimify]); - from cons; show "[]@y#ys = is"; by simp; - from cons wtl; - show "wtl_inst_list (y#ys) G rT s0 s2 cert (0 + length is) (0 + length [])"; - by simp; + assume "is \\ []" + + from this + obtain y ys where cons: "is = y#ys" + by (simp add: neq_Nil_conv) (elim, rule that) - assume cert: - "(cert ! (0 + length []) = None \\ phi ! (0 + length []) = s0) \\ - (\\t. cert ! (0 + length []) = Some t \\ phi ! (0 + length []) = t)"; + from fits + show ?thesis + proof (rule fitsD [elimify]) + from cons show "[]@y#ys = is" by simp + + from cons wtl + show "wtl_inst_list (y#ys) G rT s0 s2 cert (0 + length is) (0 + length [])" + by simp - show ?thesis; - proof (cases "cert!0"); - assume "cert!0 = None"; - with cert; - show ?thesis; by simp; - next; - fix t; assume "cert!0 = Some t"; - with cert; - have "phi!0 = t"; by (simp del: split_paired_All); - with cert cons wtl; - show ?thesis; by (auto simp add: wtl_inst_option_def); - qed; - qed simp; - qed; -qed; + assume cert: + "(cert ! (0 + length []) = None \\ phi ! (0 + length []) = s0) \\ + (\\t. cert ! (0 + length []) = Some t \\ phi ! (0 + length []) = t)" + + show ?thesis + proof (cases "cert!0") + assume "cert!0 = None" + with cert + show ?thesis by simp + next + fix t; assume "cert!0 = Some t" + with cert + have "phi!0 = t"; by (simp del: split_paired_All); + with cert cons wtl; + show ?thesis; by (auto simp add: wtl_inst_option_def); + qed + qed simp +qed lemma wtl_method_correct: -"wtl_method G C pTs rT mxl ins cert \\ \\ phi. wt_method G C pTs rT mxl ins phi"; -proof (unfold wtl_method_def, simp del: split_paired_Ex, elim exE conjE); - let "?s0" = "([], Some (Class C) # map Some pTs @ replicate mxl None)"; - fix s2; - assume neqNil: "ins \\ []"; - assume wtl: "wtl_inst_list ins G rT ?s0 s2 cert (length ins) 0"; - thus ?thesis; - obtain phi where fits: "fits phi ins G rT ?s0 s2 cert \\ length ins < length phi"; - by (rule exists_phi [elimify]) blast; - with wtl; - have allpc: - "\\pc. pc < length ins \\ wt_instr (ins ! pc) G rT phi (length ins) pc"; - by elim (rule wtl_fits_wt [elimify]); - from neqNil wtl fits; - have "wt_start G C pTs mxl phi"; - by (elim conjE, unfold wt_start_def) (rule fits_first); - with neqNil allpc fits; - show ?thesis; by (auto simp add: wt_method_def); - qed; -qed; +"wtl_method G C pTs rT mxl ins cert \\ \\ phi. wt_method G C pTs rT mxl ins phi" +proof (unfold wtl_method_def, simp del: split_paired_Ex, elim exE conjE) + let "?s0" = "([], Some (Class C) # map Some pTs @ replicate mxl None)" + fix s2 + assume neqNil: "ins \\ []" + assume wtl: "wtl_inst_list ins G rT ?s0 s2 cert (length ins) 0" + + from this + obtain phi where fits: "fits phi ins G rT ?s0 s2 cert \\ length ins < length phi" + by (rule exists_phi [elimify]) blast; + + with wtl + have allpc: + "\\pc. pc < length ins \\ wt_instr (ins ! pc) G rT phi (length ins) pc" + by elim (rule wtl_fits_wt [elimify]) + + from neqNil wtl fits + have "wt_start G C pTs mxl phi" + by (elim conjE, unfold wt_start_def) (rule fits_first) + + with neqNil allpc fits + show ?thesis by (auto simp add: wt_method_def) +qed lemma unique_set: "(a,b,c,d)\\set l \\ unique l \\ (a',b',c',d') \\ set l \\ a = a' \\ b=b' \\ c=c' \\ d=d'"; @@ -405,7 +413,7 @@ theorem wtl_correct: "wtl_jvm_prog G cert ==> \\ Phi. wt_jvm_prog G Phi"; -proof (clarsimp_tac simp add: wt_jvm_prog_def wf_prog_def, intro conjI); +proof (clarsimp simp add: wt_jvm_prog_def wf_prog_def, intro conjI); assume wtl_prog: "wtl_jvm_prog G cert"; thus "ObjectC \\ set G"; by (simp add: wtl_jvm_prog_def wf_prog_def); @@ -442,8 +450,8 @@ (\\(sg,rT,maxl,b). (sg, rT, maxl, b) \\ set mdecls \\ sg = sig)) (\\(Cl,x,y,mdecls). (Cl, x, y, mdecls) \\ set G \\ Cl = a))) mb) m"; by - (drule bspec, assumption, - clarsimp_tac elim: wtl_method_correct [elimify], - clarsimp_tac intro: selectI simp add: unique_epsilon); + clarsimp elim: wtl_method_correct [elimify], + clarsimp intro: selectI simp add: unique_epsilon); qed; qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def); qed; diff -r 15bee2731e43 -r 40d64cb4f4e6 src/HOL/MicroJava/BV/LBVSpec.thy --- a/src/HOL/MicroJava/BV/LBVSpec.thy Mon Aug 07 10:29:54 2000 +0200 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy Mon Aug 07 14:32:56 2000 +0200 @@ -7,162 +7,33 @@ header {* Specification of the LBV *} -theory LBVSpec = BVSpec: +theory LBVSpec = Step : types certificate = "state_type option list" class_certificate = "sig \\ certificate" prog_certificate = "cname \\ class_certificate" - -consts +constdefs wtl_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\ bool" -primrec -"wtl_inst (Load idx) G rT s s' cert max_pc pc = - (let (ST,LT) = s - in - pc+1 < max_pc \\ - idx < length LT \\ - (\\ts. (LT ! idx) = Some ts \\ - (ts # ST , LT) = s'))" - -"wtl_inst (Store idx) G rT s s' cert max_pc pc = - (let (ST,LT) = s - in - pc+1 < max_pc \\ - idx < length LT \\ - (\\ts ST'. ST = ts # ST' \\ - (ST' , LT[idx:=Some ts]) = s'))" - -"wtl_inst (Bipush i) G rT s s' cert max_pc pc = - (let (ST,LT) = s - in - pc+1 < max_pc \\ - ((PrimT Integer) # ST , LT) = s')" - -"wtl_inst (Aconst_null) G rT s s' cert max_pc pc = - (let (ST,LT) = s - in - pc+1 < max_pc \\ - (NT # ST , LT) = s')" - -"wtl_inst (Getfield F C) G rT s s' cert max_pc pc = - (let (ST,LT) = s - in - pc+1 < max_pc \\ - is_class G C \\ - (\\T oT ST'. field (G,C) F = Some(C,T) \\ - ST = oT # ST' \\ - G \\ oT \\ (Class C) \\ - (T # ST' , LT) = s'))" - -"wtl_inst (Putfield F C) G rT s s' cert max_pc pc = - (let (ST,LT) = s - in - pc+1 < max_pc \\ - is_class G C \\ - (\\T vT oT ST'. - field (G,C) F = Some(C,T) \\ - ST = vT # oT # ST' \\ - G \\ oT \\ (Class C) \\ - G \\ vT \\ T \\ - (ST' , LT) = s'))" - -"wtl_inst (New C) G rT s s' cert max_pc pc = - (let (ST,LT) = s - in - pc+1 < max_pc \\ - is_class G C \\ - ((Class C) # ST , LT) = s')" - -"wtl_inst (Checkcast C) G rT s s' cert max_pc pc = - (let (ST,LT) = s - in - pc+1 < max_pc \\ - is_class G C \\ - (\\rt ST'. ST = RefT rt # ST' \\ - (Class C # ST' , LT) = s'))" - -"wtl_inst Pop G rT s s' cert max_pc pc = - (let (ST,LT) = s - in - \\ts ST'. pc+1 < max_pc \\ - ST = ts # ST' \\ - (ST' , LT) = s')" +"wtl_inst i G rT s s' cert max_pc pc \\ app (i,G,rT,s) \\ + (let s'' = the (step (i,G,s)) in + (\\ pc' \\ (succs i pc). pc' < max_pc \\ + ((pc' \\ pc+1) \\ cert!pc' \\ None \\ G \\ s'' <=s the (cert!pc'))) \\ + (if (pc+1) \\ (succs i pc) then + s' = s'' + else + cert ! (pc+1) = Some s'))" -"wtl_inst Dup G rT s s' cert max_pc pc = - (let (ST,LT) = s - in - pc+1 < max_pc \\ - (\\ts ST'. ST = ts # ST' \\ - (ts # ts # ST' , LT) = s'))" - -"wtl_inst Dup_x1 G rT s s' cert max_pc pc = - (let (ST,LT) = s - in - pc+1 < max_pc \\ - (\\ts1 ts2 ST'. ST = ts1 # ts2 # ST' \\ - (ts1 # ts2 # ts1 # ST' , LT) = s'))" - -"wtl_inst Dup_x2 G rT s s' cert max_pc pc = - (let (ST,LT) = s - in - pc+1 < max_pc \\ - (\\ts1 ts2 ts3 ST'. ST = ts1 # ts2 # ts3 # ST' \\ - (ts1 # ts2 # ts3 # ts1 # ST' , LT) = s'))" - -"wtl_inst Swap G rT s s' cert max_pc pc = - (let (ST,LT) = s - in - pc+1 < max_pc \\ - (\\ts ts' ST'. ST = ts' # ts # ST' \\ - (ts # ts' # ST' , LT) = s'))" - -"wtl_inst IAdd G rT s s' cert max_pc pc = - (let (ST,LT) = s - in - pc+1 < max_pc \\ - (\\ST'. ST = (PrimT Integer) # (PrimT Integer) # ST' \\ - ((PrimT Integer) # ST' , LT) = s'))" - +lemma [simp]: +"succs i pc = {pc+1} \\ + wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \\ pc+1 < max_pc \\ (s' = the (step (i,G,s))))" +by (unfold wtl_inst_def, auto) -"wtl_inst (Ifcmpeq branch) G rT s s' cert max_pc pc = - (let (ST,LT) = s - in - pc+1 < max_pc \\ (nat(int pc+branch)) < max_pc \\ - (\\ts ts' ST'. ST = ts # ts' # ST' \\ - ((\\p. ts = PrimT p \\ ts' = PrimT p) \\ - (\\r r'. ts = RefT r \\ ts' = RefT r')) \\ - ((ST' , LT) = s') \\ - cert ! (nat(int pc+branch)) \\ None \\ - G \\ (ST' , LT) <=s the (cert ! (nat(int pc+branch)))))" - -"wtl_inst (Goto branch) G rT s s' cert max_pc pc = - ((let (ST,LT) = s - in - (nat(int pc+branch)) < max_pc \\ cert ! (nat(int pc+branch)) \\ None \\ - G \\ (ST , LT) <=s the (cert ! (nat(int pc+branch)))) \\ - (cert ! (pc+1) = Some s'))" - -"wtl_inst (Invoke mn fpTs) G rT s s' cert max_pc pc = - (let (ST,LT) = s - in - pc+1 < max_pc \\ - (\\apTs X ST'. ST = (rev apTs) @ (X # ST') \\ - length apTs = length fpTs \\ - (\\s''. cert ! (pc+1) = Some s'' \\ - ((s'' = s' \\ X = NT) \\ - ((G \\ s' <=s s'') \\ (\\C. X = Class C \\ - (\\(aT,fT)\\set(zip apTs fpTs). G \\ aT \\ fT) \\ - (\\D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\ - (rT # ST' , LT) = s')))))))" - -"wtl_inst Return G rT s s' cert max_pc pc = - ((let (ST,LT) = s - in - (\\T ST'. ST = T # ST' \\ G \\ T \\ rT)) \\ - (cert ! (pc+1) = Some s'))" +lemma [simp]: +"succs i pc = {} \\ wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \\ cert!(pc+1) = Some s')" +by (unfold wtl_inst_def, auto) constdefs @@ -205,24 +76,13 @@ lemma wtl_inst_unique: "wtl_inst i G rT s0 s1 cert max_pc pc \\ wtl_inst i G rT s0 s1' cert max_pc pc \\ s1 = s1'" (is "?P i") -proof (induct i) -case Invoke - have "\\x y. s0 = (x,y)" by (simp) - thus "wtl_inst (Invoke mname list) G rT s0 s1 cert max_pc pc \\ - wtl_inst (Invoke mname list) G rT s0 s1' cert max_pc pc \\ - s1 = s1'" - proof elim - apply_end(clarsimp_tac, drule rev_eq, assumption+) - qed auto -qed auto - +by (unfold wtl_inst_def, auto) lemma wtl_inst_option_unique: "\\wtl_inst_option i G rT s0 s1 cert max_pc pc; wtl_inst_option i G rT s0 s1' cert max_pc pc\\ \\ s1 = s1'" by (cases "cert!pc") (auto simp add: wtl_inst_unique wtl_inst_option_def) - lemma wtl_inst_list_unique: "\\ s0 pc. wtl_inst_list is G rT s0 s1 cert max_pc pc \\ wtl_inst_list is G rT s0 s1' cert max_pc pc \\ s1=s1'" (is "?P is") @@ -239,14 +99,13 @@ assume a: "?l (a#list) s0 s1 pc" assume b: "?l (a#list) s0 s1' pc" with a - show "s1 = s1'" - obtain s s' where "?o s0 s" "?o s0 s'" - and l: "?l list s s1 (Suc pc)" - and l': "?l list s' s1' (Suc pc)" by auto - have "s=s'" by(rule wtl_inst_option_unique) - with l l' Cons - show ?thesis by blast - qed + obtain s s' where "?o s0 s" "?o s0 s'" + and l: "?l list s s1 (Suc pc)" + and l': "?l list s' s1' (Suc pc)" by auto + + have "s=s'" by(rule wtl_inst_option_unique) + with l l' Cons + show "s1 = s1'" by blast qed qed @@ -279,25 +138,21 @@ thus ?thesis by blast next case Suc - with wtl - show ?thesis - obtain s0 where wtlSuc: "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)" - and wtlOpt: "wtl_inst_option a G rT s s0 cert mpc pc" by auto - from Cons - show ?thesis - obtain a' b s1' - where "a' @ b = list" "length a' = nat" - and w:"wtl_inst_list a' G rT s0 s1' cert mpc (Suc pc)" - and "wtl_inst_list b G rT s1' s' cert mpc (Suc pc + length a')" - proof (elim allE impE) - from length Suc show "nat < length list" by simp - from wtlSuc show "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)" . - qed (elim exE conjE, auto) - with Suc wtlOpt - have "?E (a#a') b s1'" by (auto simp del: split_paired_Ex) - thus ?thesis by blast - qed - qed + with wtl + obtain s0 where wtlSuc: "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)" + and wtlOpt: "wtl_inst_option a G rT s s0 cert mpc pc" by auto + from Cons + obtain a' b s1' + where "a' @ b = list" "length a' = nat" + and w:"wtl_inst_list a' G rT s0 s1' cert mpc (Suc pc)" + and "wtl_inst_list b G rT s1' s' cert mpc (Suc pc + length a')" + proof (elim allE impE) + from length Suc show "nat < length list" by simp + from wtlSuc show "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)" . + qed (elim exE conjE, auto) + with Suc wtlOpt + have "?E (a#a') b s1'" by (auto simp del: split_paired_Ex) + thus ?thesis by blast qed qed qed @@ -311,36 +166,36 @@ "wtl_inst_list x G rT s0 s1 cert (length (x@y)) 0" "wtl_inst_list y G rT s1 s2 cert (length (x@y)) (length x)" -have -"\\ pc s0. - wtl_inst_list x G rT s0 s1 cert (pc+length (x@y)) pc \\ - wtl_inst_list y G rT s1 s2 cert (pc+length (x@y)) (pc+length x) \\ - wtl_inst_list (x@y) G rT s0 s2 cert (pc+length (x@y)) pc" (is "?P x") -proof (induct "?P" "x") - case Nil - show "?P []" by simp -next - case Cons - show "?P (a#list)" - proof intro - fix pc s0 - assume y: - "wtl_inst_list y G rT s1 s2 cert (pc + length ((a # list) @ y)) (pc + length (a # list))" - assume al: - "wtl_inst_list (a # list) G rT s0 s1 cert (pc + length ((a # list) @ y)) pc" - thus "wtl_inst_list ((a # list) @ y) G rT s0 s2 cert (pc + length ((a # list) @ y)) pc" + have + "\\ pc s0. + wtl_inst_list x G rT s0 s1 cert (pc+length (x@y)) pc \\ + wtl_inst_list y G rT s1 s2 cert (pc+length (x@y)) (pc+length x) \\ + wtl_inst_list (x@y) G rT s0 s2 cert (pc+length (x@y)) pc" (is "?P x") + proof (induct "?P" "x") + case Nil + show "?P []" by simp + next + case Cons + show "?P (a#list)" + proof intro + fix pc s0 + assume y: + "wtl_inst_list y G rT s1 s2 cert (pc + length ((a # list) @ y)) (pc + length (a # list))" + assume al: + "wtl_inst_list (a # list) G rT s0 s1 cert (pc + length ((a # list) @ y)) pc" + from this obtain s' where - a: "wtl_inst_option a G rT s0 s' cert (Suc pc + length (list@y)) pc" and - l: "wtl_inst_list list G rT s' s1 cert (Suc pc + length (list@y)) (Suc pc)" by auto + a: "wtl_inst_option a G rT s0 s' cert (Suc pc + length (list@y)) pc" and + l: "wtl_inst_list list G rT s' s1 cert (Suc pc + length (list@y)) (Suc pc)" by auto with y Cons have "wtl_inst_list (list @ y) G rT s' s2 cert (Suc pc + length (list @ y)) (Suc pc)" by (elim allE impE) (assumption, simp+) with a - show ?thesis by (auto simp del: split_paired_Ex) + show "wtl_inst_list ((a # list) @ y) G rT s0 s2 cert (pc + length ((a # list) @ y)) pc" + by (auto simp del: split_paired_Ex) qed qed -qed - + with w show ?thesis proof (elim allE impE) @@ -390,18 +245,18 @@ assume y: "?y s0 pc" assume z: "?z s0 pc" assume "?x s0 pc" - thus "?p s0 pc" - obtain s0' where opt: "wtl_inst_option a G rT s0 s0' cert (pc + length ((a # list) @ i # b)) pc" - and list: "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)" - by (auto simp del: split_paired_Ex) - with y z Cons - have "wtl_inst_list (list @ [i]) G rT s0' s2 cert (Suc pc + length (list @ i # b)) (Suc pc)" - proof (elim allE impE) - from list show "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)" . - qed auto - with opt - show ?thesis by (auto simp del: split_paired_Ex) - qed + from this + obtain s0' where opt: "wtl_inst_option a G rT s0 s0' cert (pc + length ((a # list) @ i # b)) pc" + and list: "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)" + by (auto simp del: split_paired_Ex) + with y z Cons + have "wtl_inst_list (list @ [i]) G rT s0' s2 cert (Suc pc + length (list @ i # b)) (Suc pc)" + proof (elim allE impE) + from list show "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)" . + qed auto + with opt + show "?p s0 pc" + by (auto simp del: split_paired_Ex) qed qed with a i b diff -r 15bee2731e43 -r 40d64cb4f4e6 src/HOL/MicroJava/BV/Step.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/MicroJava/BV/Step.thy Mon Aug 07 14:32:56 2000 +0200 @@ -0,0 +1,718 @@ +(* Title: HOL/MicroJava/BV/Step.thy + ID: $Id$ + Author: Gerwin Klein + Copyright 2000 Technische Universitaet Muenchen +*) + +header {* Effect of instructions on the state type *} + + +theory Step = Convert : + + +(* effect of instruction on the state type *) +consts +step :: "instr \\ jvm_prog \\ state_type \\ state_type option" + +recdef step "{}" +"step (Load idx, G, (ST, LT)) = Some (the (LT ! idx) # ST, LT)" +"step (Store idx, G, (ts#ST, LT)) = Some (ST, LT[idx:= Some ts])" +"step (Bipush i, G, (ST, LT)) = Some (PrimT Integer # ST, LT)" +"step (Aconst_null, G, (ST, LT)) = Some (NT#ST,LT)" +"step (Getfield F C, G, (oT#ST, LT)) = Some (snd (the (field (G,C) F)) # ST, LT)" +"step (Putfield F C, G, (vT#oT#ST, LT)) = Some (ST,LT)" +"step (New C, G, (ST,LT)) = Some (Class C # ST, LT)" +"step (Checkcast C, G, (RefT rt#ST,LT)) = Some (Class C # ST,LT)" +"step (Pop, G, (ts#ST,LT)) = Some (ST,LT)" +"step (Dup, G, (ts#ST,LT)) = Some (ts#ts#ST,LT)" +"step (Dup_x1, G, (ts1#ts2#ST,LT)) = Some (ts1#ts2#ts1#ST,LT)" +"step (Dup_x2, G, (ts1#ts2#ts3#ST,LT)) = Some (ts1#ts2#ts3#ts1#ST,LT)" +"step (Swap, G, (ts1#ts2#ST,LT)) = Some (ts2#ts1#ST,LT)" +"step (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT)) + = Some (PrimT Integer#ST,LT)" +"step (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = Some (ST,LT)" +"step (Goto b, G, s) = Some s" +"step (Return, G, (T#ST,LT)) = None" (* Return has no successor instruction in the same method *) +"step (Invoke C mn fpTs, G, (ST,LT)) = (let ST' = drop (length fpTs) ST in + Some (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))" + +"step (i,G,s) = None" + + +(* conditions under which step is applicable *) +consts +app :: "instr \\ jvm_prog \\ ty \\ state_type \\ bool" + +recdef app "{}" +"app (Load idx, G, rT, s) = (idx < length (snd s) \\ (snd s) ! idx \\ None)" +"app (Store idx, G, rT, (ts#ST, LT)) = (idx < length LT)" +"app (Bipush i, G, rT, s) = True" +"app (Aconst_null, G, rT, s) = True" +"app (Getfield F C, G, rT, (oT#ST, LT)) = (is_class G C \\ + field (G,C) F \\ None \\ + fst (the (field (G,C) F)) = C \\ + G \\ oT \\ (Class C))" +"app (Putfield F C, G, rT, (vT#oT#ST, LT)) = (is_class G C \\ + field (G,C) F \\ None \\ + fst (the (field (G,C) F)) = C \\ + G \\ oT \\ (Class C) \\ + G \\ vT \\ (snd (the (field (G,C) F))))" +"app (New C, G, rT, s) = (is_class G C)" +"app (Checkcast C, G, rT, (RefT rt#ST,LT)) = (is_class G C)" +"app (Pop, G, rT, (ts#ST,LT)) = True" +"app (Dup, G, rT, (ts#ST,LT)) = True" +"app (Dup_x1, G, rT, (ts1#ts2#ST,LT)) = True" +"app (Dup_x2, G, rT, (ts1#ts2#ts3#ST,LT)) = True" +"app (Swap, G, rT, (ts1#ts2#ST,LT)) = True" +"app (IAdd, G, rT, (PrimT Integer#PrimT Integer#ST,LT)) + = True" +"app (Ifcmpeq b, G, rT, (ts1#ts2#ST,LT)) = ((\\ p. ts1 = PrimT p \\ ts1 = PrimT p) \\ + (\\r r'. ts1 = RefT r \\ ts2 = RefT r'))" +"app (Goto b, G, rT, s) = True" +"app (Return, G, rT, (T#ST,LT)) = (G \\ T \\ rT)" +app_invoke: +"app (Invoke C mn fpTs, G, rT, s) = (length fpTs < length (fst s) \\ + (let + apTs = rev (take (length fpTs) (fst s)); + X = hd (drop (length fpTs) (fst s)) + in + G \\ X \\ Class C \\ + (\\(aT,fT)\\set(zip apTs fpTs). G \\ aT \\ fT) \\ + method (G,C) (mn,fpTs) \\ None + ))" + +"app (i,G,rT,s) = False" + + +(* p_count of successor instructions *) +consts +succs :: "instr \\ p_count \\ p_count set" + +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 (Getfield F C) pc = {pc+1}" +"succs (Putfield F C) pc = {pc+1}" +"succs (New C) pc = {pc+1}" +"succs (Checkcast C) pc = {pc+1}" +"succs Pop pc = {pc+1}" +"succs Dup pc = {pc+1}" +"succs Dup_x1 pc = {pc+1}" +"succs Dup_x2 pc = {pc+1}" +"succs Swap pc = {pc+1}" +"succs IAdd pc = {pc+1}" +"succs (Ifcmpeq b) pc = {pc+1, nat (int pc + b)}" +"succs (Goto b) pc = {nat (int pc + b)}" +"succs Return pc = {}" +"succs (Invoke C mn fpTs) pc = {pc+1}" + + +lemma 1: "2 < length a \\ (\\l l' l'' ls. a = l#l'#l''#ls)" +proof (cases a) + fix x xs assume "a = x#xs" "2 < length a" + thus ?thesis by - (cases xs, simp, cases "tl xs", auto) +qed auto + +lemma 2: "\\(2 < length a) \\ a = [] \\ (\\ l. a = [l]) \\ (\\ l l'. a = [l,l'])" +proof -; + assume "\\(2 < length a)" + hence "length a < (Suc 2)" by simp + hence * : "length a = 0 \\ length a = 1 \\ length a = 2" by (auto simp add: less_Suc_eq) + + { + fix x + assume "length x = 1" + hence "\\ l. x = [l]" by - (cases x, auto) + } note 0 = this + + have "length a = 2 \\ \\l l'. a = [l,l']" by (cases a, auto dest: 0) + with * show ?thesis by (auto dest: 0) +qed + +lemma appStore[simp]: +"app (Store idx, G, rT, s) = (\\ ts ST LT. s = (ts#ST,LT) \\ idx < length LT)" (is "?app s = ?P s") +by (cases s, cases "2 < length (fst s)", auto dest: 1 2) + + +lemma appGetField[simp]: +"app (Getfield F C, G, rT, s) = (\\ oT ST LT. s = (oT#ST, LT) \\ is_class G C \\ + fst (the (field (G,C) F)) = C \\ + field (G,C) F \\ None \\ G \\ oT \\ (Class C))" (is "?app s = ?P s") +by (cases s, cases "2 < length (fst s)", auto dest: 1 2) + + +lemma appPutField[simp]: +"app (Putfield F C, G, rT, s) = (\\ vT oT ST LT. s = (vT#oT#ST, LT) \\ is_class G C \\ + field (G,C) F \\ None \\ fst (the (field (G,C) F)) = C \\ + G \\ oT \\ (Class C) \\ + G \\ vT \\ (snd (the (field (G,C) F))))" (is "?app s = ?P s") +by (cases s, cases "2 < length (fst s)", auto dest: 1 2) + + +lemma appCheckcast[simp]: +"app (Checkcast C, G, rT, s) = (\\rT ST LT. s = (RefT rT#ST,LT) \\ is_class G C)" (is "?app s = ?P s") +by (cases s, cases "fst s", simp, cases "hd (fst s)", auto) + +lemma appPop[simp]: +"app (Pop, G, rT, s) = (\\ts ST LT. s = (ts#ST,LT))" (is "?app s = ?P s") +by (cases s, cases "2 < length (fst s)", auto dest: 1 2) + + +lemma appDup[simp]: +"app (Dup, G, rT, s) = (\\ts ST LT. s = (ts#ST,LT))" (is "?app s = ?P s") +by (cases s, cases "2 < length (fst s)", auto dest: 1 2) + + +lemma appDup_x1[simp]: +"app (Dup_x1, G, rT, s) = (\\ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" (is "?app s = ?P s") +by (cases s, cases "2 < length (fst s)", auto dest: 1 2) + + +lemma appDup_x2[simp]: +"app (Dup_x2, G, rT, s) = (\\ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))"(is "?app s = ?P s") +by (cases s, cases "2 < length (fst s)", auto dest: 1 2) + + +lemma appSwap[simp]: +"app (Swap, G, rT, s) = (\\ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" (is "?app s = ?P s") +by (cases s, cases "2 < length (fst s)", auto dest: 1 2) + + +lemma appIAdd[simp]: +"app (IAdd, G, rT, s) = (\\ ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))" (is "?app s = ?P s") +proof (cases s) + case Pair + have "?app (a,b) = ?P (a,b)" + proof (cases "a") + fix t ts assume a: "a = t#ts" + show ?thesis + proof (cases t) + fix p assume p: "t = PrimT p" + show ?thesis + proof (cases p) + assume ip: "p = Integer" + show ?thesis + proof (cases ts) + fix t' ts' assume t': "ts = t' # ts'" + show ?thesis + proof (cases t') + fix p' assume "t' = PrimT p'" + with t' ip p a + show ?thesis by - (cases p', auto) + qed (auto simp add: a p ip t') + qed (auto simp add: a p ip) + qed (auto simp add: a p) + qed (auto simp add: a) + qed auto + with Pair show ?thesis by simp +qed + + +lemma appIfcmpeq[simp]: +"app (Ifcmpeq b, G, rT, s) = (\\ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \\ + ((\\ p. ts1 = PrimT p \\ ts1 = PrimT p) \\ + (\\r r'. ts1 = RefT r \\ ts2 = RefT r')))" +by (cases s, cases "2 < length (fst s)", auto dest: 1 2) + + +lemma appReturn[simp]: +"app (Return, G, rT, s) = (\\T ST LT. s = (T#ST,LT) \\ (G \\ T \\ rT))" +by (cases s, cases "2 < length (fst s)", auto dest: 1 2) + + +lemma appInvoke[simp]: +"app (Invoke C mn fpTs, G, rT, s) = (\\apTs X ST LT. + s = ((rev apTs) @ (X # ST), LT) \\ + length apTs = length fpTs \\ + G \\ X \\ Class C \\ + (\\(aT,fT)\\set(zip apTs fpTs). G \\ aT \\ fT) \\ + method (G,C) (mn,fpTs) \\ None)" (is "?app s = ?P s") +proof (cases s) + case Pair + have "?app (a,b) \\ ?P (a,b)" + proof - + assume app: "?app (a,b)" + hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \\ length fpTs < length a" + (is "?a \\ ?l") by auto + hence "?a \\ 0 < length (drop (length fpTs) a)" (is "?a \\ ?l") by auto + hence "?a \\ ?l \\ length (rev (take (length fpTs) a)) = length fpTs" by (auto simp add: min_def) + hence "\\apTs ST. a = rev apTs @ ST \\ length apTs = length fpTs \\ 0 < length ST" by blast + hence "\\apTs ST. a = rev apTs @ ST \\ length apTs = length fpTs \\ ST \\ []" by blast + hence "\\apTs ST. a = rev apTs @ ST \\ length apTs = length fpTs \\ (\\X ST'. ST = X#ST')" by (simp add: neq_Nil_conv) + hence "\\apTs X ST. a = rev apTs @ X # ST \\ length apTs = length fpTs" by blast + with app + show ?thesis by auto blast + qed + with Pair have "?app s \\ ?P s" by simp + thus ?thesis by auto +qed + +lemmas [simp del] = app_invoke +lemmas [trans] = sup_loc_trans + +ML_setup {* bind_thm ("widen_RefT", widen_RefT) *} +ML_setup {* bind_thm ("widen_RefT2", widen_RefT2) *} + + + +lemma app_step_some: +"\\app (i,G,rT,s); succs i pc \\ {} \\ \\ step (i,G,s) \\ None"; +by (cases s, cases i, auto) + +lemma sup_state_length: +"G \\ s2 <=s s1 \\ length (fst s2) = length (fst s1) \\ length (snd s2) = length (snd s1)" + by (cases s1, cases s2, simp add: sup_state_length_fst sup_state_length_snd) + +lemma PrimT_PrimT: "(G \\ xb \\ PrimT p) = (xb = PrimT p)" +proof + show "xb = PrimT p \\ G \\ xb \\ PrimT p" by blast + + show "G\\ xb \\ PrimT p \\ xb = PrimT p" + proof (cases xb) + fix prim + assume "xb = PrimT prim" "G\\xb\\PrimT p" + thus ?thesis by simp + next + fix ref + assume "G\\xb\\PrimT p" "xb = RefT ref" + thus ?thesis by simp (rule widen_RefT [elimify], auto) + qed +qed + +lemma sup_loc_some [rulify]: +"\\ 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") +proof (induct "?P" b) + show "?P []" by simp + + case Cons + show "?P (a#list)" + proof (clarsimp simp add: list_all2_Cons1 sup_loc_def) + fix z zs n + assume * : + "G \\ a <=o z" "list_all2 (sup_ty_opt G) list zs" + "n < Suc (length zs)" "(z # zs) ! n = Some t" + + show "(\\t. (a # list) ! n = Some t) \\ G \\(a # list) ! n <=o Some t" + proof (cases n) + case 0 + with * show ?thesis by (simp add: sup_ty_opt_some) + next + case Suc + with Cons * + show ?thesis by (simp add: sup_loc_def) + qed + qed +qed + + +lemma all_widen_is_sup_loc: +"\\b. length a = length b \\ (\\x\\set (zip a b). x \\ widen G) = (G \\ (map Some a) <=l (map Some b))" + (is "\\b. length a = length b \\ ?Q a b" is "?P a") +proof (induct "a") + show "?P []" by simp + + fix l ls assume Cons: "?P ls" + + show "?P (l#ls)" + proof (intro allI impI) + fix b + assume "length (l # ls) = length (b::ty list)" + with Cons + show "?Q (l # ls) b" by - (cases b, auto) + qed +qed + + +lemma append_length_n: "\\n. n \\ length x \\ (\\a b. x = a@b \\ length a = n)" (is "?P x") +proof (induct "?P" "x") + show "?P []" by simp + + fix l ls assume Cons: "?P ls" + + show "?P (l#ls)" + proof (intro allI impI) + fix n + assume l: "n \\ length (l # ls)" + + show "\\a b. l # ls = a @ b \\ length a = n" + proof (cases n) + assume "n=0" thus ?thesis by simp + next + fix "n'" assume s: "n = Suc n'" + with l + have "n' \\ length ls" by simp + hence "\\a b. ls = a @ b \\ length a = n'" by (rule Cons [rulify]) + thus ?thesis + proof elim + fix a b + assume "ls = a @ b" "length a = n'" + with s + have "l # ls = (l#a) @ b \\ length (l#a) = n" by simp + thus ?thesis by blast + qed + qed + qed +qed + + + +lemma rev_append_cons: +"\\n < length x\\ \\ \\a b c. x = (rev a) @ b # c \\ length a = n" +proof - + assume n: "n < length x" + hence "n \\ length x" by simp + hence "\\a b. x = a @ b \\ length a = n" by (rule append_length_n [rulify]) + thus ?thesis + proof elim + fix r d assume x: "x = r@d" "length r = n" + with n + have "\\b c. d = b#c" by (simp add: neq_Nil_conv) + + thus ?thesis + proof elim + fix b c + assume "d = b#c" + with x + have "x = (rev (rev r)) @ b # c \\ length (rev r) = n" by simp + thus ?thesis by blast + qed + qed +qed + + +lemma app_mono: +"\\G \\ s2 <=s s1; app (i, G, rT, s1)\\ \\ app (i, G, rT, s2)"; +proof - + assume G: "G \\ s2 <=s s1" + assume app: "app (i, G, rT, s1)" + + show ?thesis + proof (cases i) + case Load + + from G + have l: "length (snd s1) = length (snd s2)" by (simp add: sup_state_length) + + from G Load app + have "G \\ snd s2 <=l snd s1" by (auto simp add: sup_state_def) + + with G Load app l + show ?thesis by clarsimp (drule sup_loc_some, simp+) + next + case Store + with G app + show ?thesis + by - (cases s2, + auto dest: map_hd_tl simp add: sup_loc_Cons2 sup_loc_length sup_state_def) + next + case Bipush + thus ?thesis by simp + next + case Aconst_null + thus ?thesis by simp + next + case New + with app + show ?thesis by simp + next + case Getfield + with app G + show ?thesis + by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans) + next + case Putfield + + with app + obtain vT oT ST LT b + where s1: "s1 = (vT # oT # ST, LT)" and + "field (G, cname) vname = Some (cname, b)" + "is_class G cname" and + oT: "G\\ oT\\ (Class cname)" and + vT: "G\\ vT\\ b" + by simp (elim exE conjE, simp, rule that) + moreover + from s1 G + obtain vT' oT' ST' LT' + where s2: "s2 = (vT' # oT' # ST', LT')" and + oT': "G\\ oT' \\ oT" and + vT': "G\\ vT' \\ vT" + by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that) + moreover + from vT' vT + have "G \\ vT' \\ b" by (rule widen_trans) + moreover + from oT' oT + have "G\\ oT' \\ (Class cname)" by (rule widen_trans) + ultimately + show ?thesis + by (auto simp add: Putfield) + next + case Checkcast + with app G + show ?thesis + by - (cases s2, auto intro: widen_RefT2 simp add: sup_state_Cons2) + next + case Return + with app G + show ?thesis + by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans) + next + case Pop + with app G + show ?thesis + by - (cases s2, clarsimp simp add: sup_state_Cons2) + next + case Dup + with app G + show ?thesis + by - (cases s2, clarsimp simp add: sup_state_Cons2) + next + case Dup_x1 + with app G + show ?thesis + by - (cases s2, clarsimp simp add: sup_state_Cons2) + next + case Dup_x2 + with app G + show ?thesis + by - (cases s2, clarsimp simp add: sup_state_Cons2) + next + case Swap + with app G + show ?thesis + by - (cases s2, clarsimp simp add: sup_state_Cons2) + next + case IAdd + with app G + show ?thesis + by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT) + next + case Goto + with app + show ?thesis by simp + next + case Ifcmpeq + with app G + show ?thesis + by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT widen_RefT2) + next + case Invoke + + with app + obtain apTs X ST LT where + s1: "s1 = (rev apTs @ X # ST, LT)" and + l: "length apTs = length list" and + C: "G \\ X \\ Class cname" and + w: "\\x \\ set (zip apTs list). x \\ widen G" and + m: "method (G, cname) (mname, list) \\ None" + by (simp del: not_None_eq, elim exE conjE) (rule that) + + obtain apTs' X' ST' LT' where + s2: "s2 = (rev apTs' @ X' # ST', LT')" and + l': "length apTs' = length list" + proof - + from l s1 G + have "length list < length (fst s2)" + by (simp add: sup_state_length) + hence "\\a b c. (fst s2) = rev a @ b # c \\ length a = length list" + by (rule rev_append_cons [rulify]) + thus ?thesis + by - (cases s2, elim exE conjE, simp, rule that) + qed + + from l l' + have "length (rev apTs') = length (rev apTs)" by simp + + from this s1 s2 G + obtain + G': "G \\ (apTs',LT') <=s (apTs,LT)" + "G \\ X' \\ X" "G \\ (ST',LT') <=s (ST,LT)" + by (simp add: sup_state_rev_fst sup_state_append_fst sup_state_Cons1); + + with C + have C': "G \\ X' \\ Class cname" + by - (rule widen_trans, auto) + + from G' + have "G \\ map Some apTs' <=l map Some apTs" + by (simp add: sup_state_def) + also + from l w + have "G \\ map Some apTs <=l map Some list" + by (simp add: all_widen_is_sup_loc) + finally + have "G \\ map Some apTs' <=l map Some list" . + + with l' + have w': "\\x \\ set (zip apTs' list). x \\ widen G" + by (simp add: all_widen_is_sup_loc) + + from Invoke s2 l' w' C' m + show ?thesis + by simp blast + qed +qed + + +lemma step_mono: +"\\succs i pc \\ {}; app (i,G,rT,s2); G \\ s1 <=s s2\\ \\ + G \\ the (step (i,G,s1)) <=s the (step (i,G,s2))" +proof (cases s1, cases s2) + fix a1 b1 a2 b2 + assume s: "s1 = (a1,b1)" "s2 = (a2,b2)" + assume succs: "succs i pc \\ {}" + assume app2: "app (i,G,rT,s2)" + assume G: "G \\ s1 <=s s2" + + from G app2 + have app1: "app (i,G,rT,s1)" by (rule app_mono) + + from app1 app2 succs + obtain a1' b1' a2' b2' + where step: "step (i,G,s1) = Some (a1',b1')" "step (i,G,s2) = Some (a2',b2')"; + by (auto dest: app_step_some); + + have "G \\ (a1',b1') <=s (a2',b2')" + proof (cases i) + case Load + + with s app1 + obtain y where + y: "nat < length b1" "b1 ! nat = Some y" by clarsimp + + from Load s app2 + obtain y' where + y': "nat < length b2" "b2 ! nat = Some y'" by clarsimp + + from G s + have "G \\ b1 <=l b2" by (simp add: sup_state_def) + + with y y' + have "G \\ y \\ y'" + by - (drule sup_loc_some, simp+) + + with Load G y y' s step app1 app2 + show ?thesis by (clarsimp simp add: sup_state_def) + next + case Store + with G s step app1 app2 + show ?thesis + by (clarsimp simp add: sup_state_def sup_loc_update) + next + case Bipush + with G s step app1 app2 + show ?thesis + by (clarsimp simp add: sup_state_Cons1) + next + case New + with G s step app1 app2 + 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 + by (clarsimp simp add: sup_state_Cons1) + next + case Putfield + with G s step app1 app2 + show ?thesis + by (clarsimp simp add: sup_state_Cons1) + next + case Checkcast + with G s step app1 app2 + show ?thesis + by (clarsimp simp add: sup_state_Cons1) + next + case Invoke + + with s app1 + obtain a X ST where + s1: "s1 = (a @ X # ST, b1)" and + l: "length a = length list" + by (simp, elim exE conjE, simp) + + from Invoke s app2 + obtain a' X' ST' where + s2: "s2 = (a' @ X' # ST', b2)" and + l': "length a' = length list" + by (simp, elim exE conjE, simp) + + from l l' + have lr: "length a = length a'" by simp + + from lr G s s1 s2 + have "G \\ (ST, b1) <=s (ST', b2)" + by (simp add: sup_state_append_fst sup_state_Cons1) + + moreover + + from Invoke G s step app1 app2 + have "b1 = b1' \\ b2 = b2'" by simp + + ultimately + + have "G \\ (ST, b1') <=s (ST', b2')" by simp + + with Invoke G s step app1 app2 s1 s2 l l' + show ?thesis + by (clarsimp simp add: sup_state_def) + next + case Return + with succs have "False" by simp + thus ?thesis by blast + next + case Pop + with G s step app1 app2 + show ?thesis + by (clarsimp simp add: sup_state_Cons1) + next + case Dup + with G s step app1 app2 + show ?thesis + by (clarsimp simp add: sup_state_Cons1) + next + case Dup_x1 + with G s step app1 app2 + show ?thesis + by (clarsimp simp add: sup_state_Cons1) + next + case Dup_x2 + with G s step app1 app2 + show ?thesis + by (clarsimp simp add: sup_state_Cons1) + next + case Swap + with G s step app1 app2 + show ?thesis + by (clarsimp simp add: sup_state_Cons1) + next + case IAdd + with G s step app1 app2 + show ?thesis + by (clarsimp simp add: sup_state_Cons1) + next + case Goto + with G s step app1 app2 + show ?thesis by simp + next + case Ifcmpeq + with G s step app1 app2 + show ?thesis + by (clarsimp simp add: sup_state_Cons1) + qed + + with step + show ?thesis by auto +qed + + + +end