# HG changeset patch # User kleing # Date 967664859 -7200 # Node ID 1024a2d80ac016781aeb5d71d00b5b0914397a0e # Parent 3533e3e9267fb861ac6c9d5dfff2e2b6aae95f0b functional LBV style, dead code, type safety -> Isar diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/BVSpec.thy --- a/src/HOL/MicroJava/BV/BVSpec.thy Wed Aug 30 21:44:12 2000 +0200 +++ b/src/HOL/MicroJava/BV/BVSpec.thy Wed Aug 30 21:47:39 2000 +0200 @@ -3,61 +3,62 @@ Author: Cornelia Pusch Copyright 1999 Technische Universitaet Muenchen -Specification of bytecode verifier *) -theory BVSpec = Step : +header "The Bytecode Verifier" + +theory BVSpec = Step: types - method_type = "state_type list" - class_type = "sig \\ method_type" - prog_type = "cname \\ class_type" + method_type = "state_type option list" + class_type = "sig \ method_type" + prog_type = "cname \ class_type" constdefs -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_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' \ set (succs i pc). pc' < max_pc \ (G \ step i G (phi!pc) <=' 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_start :: "[jvm_prog,cname,ty list,nat,method_type] \ bool" +"wt_start G C pTs mxl phi \ + G \ Some ([],(Ok (Class C))#((map Ok pTs))@(replicate mxl Err)) <=' 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)" + 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 G phi \\ - wf_prog (\\G C (sig,rT,maxl,b). +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)" +"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"; +"\ 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)" +"\ 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)))" +(* for most instructions wt_instr collapses: *) +lemma +"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 \ step i G (phi!pc) <=' phi!(pc+1)))" by (simp add: wt_instr_def) end diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/BVSpecTypeSafe.ML --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Wed Aug 30 21:44:12 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,517 +0,0 @@ -(* Title: HOL/MicroJava/BV/BVSpecTypeSafe.ML - ID: $Id$ - Author: Cornelia Pusch - Copyright 1999 Technische Universitaet Muenchen -*) - -val defs1 = exec.simps@[split_def,thm "sup_state_def",correct_state_def, - correct_frame_def, thm "wt_instr_def"]; - -Goalw [correct_state_def,Let_def,correct_frame_def,split_def] -"\\ wt_jvm_prog G phi; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ 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 [thm "wt_jvm_prog_impl_wt_instr"]) 1); -qed "wt_jvm_prog_impl_wt_instr_cor"; - - -Delsimps [split_paired_All]; - - -(******* LS *******) - - -Goal -"\\ wf_prog wt G; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ ins!pc = Load idx; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ 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); \ -\ ins!pc = Store idx; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_subst RSN(2, approx_loc_imp_approx_loc_sup)] - 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"; -AddIffs [conf_Intg_Integer]; - -Goal -"\\ wf_prog wt G; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ ins!pc = Bipush i; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ 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,thm "sup_PTS_eq",map_eq_Cons]@defs1)) 1); -qed "Bipush_correct"; - -Goal "G \\ T' \\ T \\ T' = NT \\ (T=NT | (\\C. T = Class C))"; -be widen.induct 1; -by(Auto_tac); -by(rename_tac "R" 1); -by(case_tac "R" 1); -by(Auto_tac); -val lemma = result(); - -Goal "G \\ NT \\ T = (T=NT | (\\C. T = Class C))"; -by(force_tac (claset() addIs widen.intrs addDs [lemma],simpset()) 1); -qed "NT_subtype_conv"; - -Goal -"\\ wf_prog wt G; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ ins!pc = Aconst_null; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ 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"; -by (forward_tac [widen_Class] 1); -by (Clarify_tac 1); -be disjE 1; - by (asm_full_simp_tac (simpset() addsimps [widen.null]) 1); -by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [obj_ty_def]) 1); -by (case_tac "v" 1); -by (ALLGOALS (fast_tac (claset() addIs [rtrancl_trans] addss (simpset() addsimps [widen.null])))); -qed "Cast_conf2"; - -Goal -"\\ wf_prog wt G; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ ins!pc = Checkcast D; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -by (asm_full_simp_tac (simpset() addsimps [map_eq_Cons, - raise_xcpt_def]@defs1 addsplits [option.split]) 1); -by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup,Cast_conf2] - 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); \ -\ ins!pc = Getfield F D; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -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 [thm "sup_state_def",map_eq_Cons]) 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1); - -by (forward_tac [conf_widen] 1); - ba 1; - ba 1; -bd conf_RefTD 1; -by (Clarify_tac 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 [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]) 1); -qed "Getfield_correct"; - - - -Goal -"\\ wf_prog wt G; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ ins!pc = Putfield F D; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -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 [thm "sup_state_def",map_eq_Cons]) 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1); - -by (forward_tac [conf_widen] 1); - ba 2; - ba 1; -by (fast_tac (claset() addDs [conf_RefTD,widen_cfs_fields] - addIs [sup_heap_update_value,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), - hconf_imp_hconf_field_update, - 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"; - -Goal -"\\ wf_prog wt G; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ ins!pc = New cl_idx; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ 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), - hconf_imp_hconf_newref,correct_frames_imp_correct_frames_newref, - rewrite_rule [split_def] correct_init_obj] - addss (simpset() addsimps [NT_subtype_conv,approx_val_def,conf_def, - fun_upd_apply,map_eq_Cons,is_class_def,raise_xcpt_def,init_vars_def]@defs1 - addsplits [option.split])) 1); -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 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(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(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; - ba 1; -by (Clarify_tac 1); -bd subtype_widen_methd 1; - ba 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",thm "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 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); - -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 -"\\ wt_jvm_prog G phi; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ ins ! pc = Return; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -by (asm_full_simp_tac (simpset() addsimps (neq_Nil_conv::defs1) addsplits [split_if_asm]) 1); -by (Clarify_tac 1); -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 [thm "wt_jvm_prog_impl_wt_instr"] 1); - by(EVERY1[atac, etac Suc_lessD]); -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] - addIs [conf_widen] - addss (simpset() addsimps [approx_val_def,append_eq_conv_conj,map_eq_Cons]@defs1)) 1); -qed "Return_correct"; -Addsimps [map_append]; - - - -Goal -"\\ wf_prog wt G; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ ins ! pc = Goto branch; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup,approx_stk_imp_approx_stk_sup] - addss (simpset() addsimps defs1)) 1); -qed "Goto_correct"; - - -Goal -"\\ wf_prog wt G; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ ins!pc = Ifcmpeq branch; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ 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 "Ifcmpeq_correct"; - - -Goal -"\\ wf_prog wt G; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ ins ! pc = Pop; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ 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 "Pop_correct"; - - -Goal -"\\ wf_prog wt G; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ ins ! pc = Dup; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] - addss (simpset() addsimps [map_eq_Cons]@defs1)) 1); -qed "Dup_correct"; - - - -Goal -"\\ wf_prog wt G; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ ins ! pc = Dup_x1; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] - addss (simpset() addsimps [map_eq_Cons]@defs1)) 1); -qed "Dup_x1_correct"; - -Goal -"\\ wf_prog wt G; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ ins ! pc = Dup_x2; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] - addss (simpset() addsimps [map_eq_Cons]@defs1)) 1); -qed "Dup_x2_correct"; - -Goal -"\\ wf_prog wt G; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ ins ! pc = Swap; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] - addss (simpset() addsimps [map_eq_Cons]@defs1)) 1); -qed "Swap_correct"; - - -Goal -"\\ wf_prog wt G; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ ins ! pc = IAdd; \ -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] - addss (simpset() addsimps [map_eq_Cons, approx_val_def]@defs1)) 1); -qed "IAdd_correct"; - - - -(** instr correct **) - -Goal -"\\ wt_jvm_prog G phi; \ -\ method (G,C) sig = Some (C,rT,maxl,ins); \ -\ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ -\ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ -\\\ G,phi \\JVM state'\\"; -by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); - ba 1; - ba 1; -by(case_tac "ins!pc" 1); -by(fast_tac (claset() addIs [Invoke_correct]) 9); -by(fast_tac (claset() addIs [Return_correct]) 9); -by(rewtac (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,Ifcmpeq_correct,Pop_correct,Dup_correct, - Dup_x1_correct,Dup_x2_correct,Swap_correct,IAdd_correct]))); -qed "instr_correct"; - - -(** Main **) - -Goalw [correct_state_def,Let_def] - "G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \ -\ \\ \\meth. method (G,C) sig = Some(C,meth)"; -by(Asm_full_simp_tac 1); -by(Blast_tac 1); -qed "correct_state_impl_Some_method"; - -Goal -"\\state. \\ wt_jvm_prog G phi; G,phi \\JVM state\\\\ \ -\ \\ exec (G,state) = Some state' \\ G,phi \\JVM state'\\"; -by(split_all_tac 1); -by(rename_tac "xp hp frs" 1); -by (case_tac "xp" 1); - by (case_tac "frs" 1); - by (asm_full_simp_tac (simpset() addsimps exec.simps) 1); - by(split_all_tac 1); - by(hyp_subst_tac 1); - by(forward_tac [correct_state_impl_Some_method] 1); - by (force_tac (claset() addIs [instr_correct], simpset() addsplits [split_if_asm] addsimps exec.simps@[split_def]) 1); -by (case_tac "frs" 1); - by (ALLGOALS(asm_full_simp_tac (simpset() addsimps exec.simps))); -qed_spec_mp "BV_correct_1"; - -(*******) -Goal -"\\ xp=None; frs\\[] \\ \\ (\\state'. exec (G,xp,hp,frs) = Some state')"; -by (auto_tac (claset() addIs [BV_correct_1], - (simpset() addsplits [instr.split] addsimps [neq_Nil_conv]@defs1))); -by (case_tac "(snd (snd (snd (the (method (G, ab) (ac, b)))))) ! ba" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps defs1))); -val lemma = result(); - -Goal -"\\ wt_jvm_prog G phi; G,phi \\JVM (xp,hp,frs)\\; xp=None; frs\\[] \\ \ -\ \\ \\state'. exec(G,xp,hp,frs) = Some state' \\ G,phi \\JVM state'\\"; -by (dres_inst_tac [("G","G"),("hp","hp")] lemma 1); -ba 1; -by (fast_tac (claset() addIs [BV_correct_1]) 1); -qed "L1"; -(*******) - -Goalw [exec_all_def] -"\\ wt_jvm_prog G phi; G \\ s -jvm\\ t \\ \\ G,phi \\JVM s\\ \\ G,phi \\JVM t\\"; -be rtrancl_induct 1; - by (Simp_tac 1); -by (fast_tac (claset() addIs [BV_correct_1] addss (simpset())) 1); -qed_spec_mp "BV_correct"; - - -Goal -"\\ wt_jvm_prog G phi; G \\ s0 -jvm\\ (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \\JVM s0 \\\\ \ -\ \\ approx_stk G hp stk (fst (((phi C) sig) ! pc)) \\ approx_loc G hp loc (snd (((phi C) sig) ! pc)) "; -bd BV_correct 1; -ba 1; -ba 1; -by (asm_full_simp_tac (simpset() addsimps [correct_state_def,correct_frame_def,split_def] - addsplits [option.split_asm]) 1); -qed_spec_mp "BV_correct_initial"; diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Wed Aug 30 21:44:12 2000 +0200 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Wed Aug 30 21:47:39 2000 +0200 @@ -7,4 +7,630 @@ programs. *) -BVSpecTypeSafe = Correct +header "Type Safety Proof" + +theory BVSpecTypeSafe = Correct: + +lemmas defs1 = sup_state_def correct_state_def correct_frame_def wt_instr_def step_def +lemmas [simp del] = split_paired_All + +lemma wt_jvm_prog_impl_wt_instr_cor: + "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] + ==> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc" +apply (unfold correct_state_def Let_def correct_frame_def) +apply simp +apply (blast intro: wt_jvm_prog_impl_wt_instr) +. + +lemma Load_correct: +"\ wf_prog wt G; + method (G,C) sig = Some (C,rT,maxl,ins); + ins!pc = Load idx; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\" +apply (clarsimp simp add: defs1 map_eq_Cons) +apply (rule conjI) + apply (rule approx_loc_imp_approx_val_sup) + apply simp+ +apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup) +. + +lemma Store_correct: +"\ wf_prog wt G; + method (G,C) sig = Some (C,rT,maxl,ins); + ins!pc = Store idx; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\" +apply (clarsimp simp add: defs1 map_eq_Cons) +apply (rule conjI) + apply (blast intro: approx_stk_imp_approx_stk_sup) +apply (blast intro: approx_loc_imp_approx_loc_subst approx_loc_imp_approx_loc_sup) +. + + +lemma conf_Intg_Integer [iff]: + "G,h \ Intg i \\ PrimT Integer" +by (simp add: conf_def) + + +lemma Bipush_correct: +"\ wf_prog wt G; + method (G,C) sig = Some (C,rT,maxl,ins); + ins!pc = Bipush i; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\"; +apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons) +apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup) +. + +lemma NT_subtype_conv: + "G \ NT \ T = (T=NT \ (\C. T = Class C))" +proof - + have "\T T'. G \ T' \ T \ T' = NT \ (T=NT | (\C. T = Class C))" + apply (erule widen.induct) + apply auto + apply (case_tac R) + apply auto + . + note l = this + + show ?thesis + by (force intro: null dest: l) +qed + +lemma Aconst_null_correct: +"\ wf_prog wt G; + method (G,C) sig = Some (C,rT,maxl,ins); + ins!pc = Aconst_null; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\"; +apply (clarsimp simp add: defs1 map_eq_Cons) +apply (rule conjI) + apply (force simp add: approx_val_Null NT_subtype_conv) +apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup) +. + + +lemma Cast_conf2: + "\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" +apply (unfold cast_ok_def) +apply (frule widen_Class) +apply (elim exE disjE) + apply (simp add: null) +apply (clarsimp simp add: conf_def obj_ty_def) +apply (cases v) +apply (auto intro: null rtrancl_trans) +. + + +lemma Checkcast_correct: +"\ wf_prog wt G; + method (G,C) sig = Some (C,rT,maxl,ins); + ins!pc = Checkcast D; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\" +apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def) +apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup Cast_conf2) +. + + +lemma Getfield_correct: +"\ wf_prog wt G; + method (G,C) sig = Some (C,rT,maxl,ins); + ins!pc = Getfield F D; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\"; +apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def split: option.split) +apply (frule conf_widen) +apply assumption+ +apply (drule conf_RefTD) +apply (clarsimp simp add: defs1 approx_val_def) +apply (rule conjI) + apply (drule widen_cfs_fields) + apply assumption+ + apply (force intro: conf_widen simp add: hconf_def oconf_def lconf_def) +apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup) +. + +lemma Putfield_correct: +"\ wf_prog wt G; + method (G,C) sig = Some (C,rT,maxl,ins); + ins!pc = Putfield F D; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\"; +apply (clarsimp simp add: defs1 raise_xcpt_def split: option.split List.split) +apply (clarsimp simp add: approx_val_def) +apply (frule conf_widen) +prefer 2 +apply assumption +apply assumption +apply (drule conf_RefTD) +apply clarsimp +apply (blast intro: sup_heap_update_value approx_stk_imp_approx_stk_sup_heap approx_stk_imp_approx_stk_sup + approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup + hconf_imp_hconf_field_update + correct_frames_imp_correct_frames_field_update conf_widen dest: widen_cfs_fields) +. + +lemma collapse_paired_All: + "(\x y. P(x,y)) = (\z. P z)" + by fast + +lemma New_correct: +"\ wf_prog wt G; + method (G,C) sig = Some (C,rT,maxl,ins); + ins!pc = New cl_idx; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\" +apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def + fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 + split: option.split) +apply (force dest!: iffD1 [OF collapse_paired_All] + intro: sup_heap_newref approx_stk_imp_approx_stk_sup_heap approx_stk_imp_approx_stk_sup + approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup + hconf_imp_hconf_newref correct_frames_imp_correct_frames_newref + correct_init_obj simp add: NT_subtype_conv approx_val_def conf_def + fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 + split: option.split) +. + + +(****** Method Invocation ******) + +lemmas [simp del] = split_paired_Ex + +lemma Invoke_correct: +"\ wt_jvm_prog G phi; + method (G,C) sig = Some (C,rT,maxl,ins); + 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'\" +proof - + assume wtprog: "wt_jvm_prog G phi" + assume method: "method (G,C) sig = Some (C,rT,maxl,ins)" + assume ins: "ins ! pc = Invoke C' mn pTs" + assume wti: "wt_instr (ins!pc) G rT (phi C sig) (length ins) pc" + assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)" + assume approx: "G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\" + + from wtprog + obtain wfmb where + wfprog: "wf_prog wfmb G" + by (simp add: wt_jvm_prog_def) + + from ins method approx + obtain s where + heap_ok: "G\h hp\" and + phi_pc: "phi C sig!pc = Some s" and + frame: "correct_frame G hp s maxl ins (stk, loc, C, sig, pc)" and + frames: "correct_frames G hp phi rT sig frs" + by (clarsimp simp add: correct_state_def) + + from ins wti phi_pc + obtain apTs X ST LT D' rT body where + s: "s = (rev apTs @ X # ST, LT)" and + l: "length apTs = length pTs" and + X: "G\ X \ Class C'" and + w: "\x\set (zip apTs pTs). x \ widen G" and + mC': "method (G, C') (mn, pTs) = Some (D', rT, body)" and + pc: "Suc pc < length ins" and + step: "G \ step (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc" + by (simp add: wt_instr_def) (elim exE conjE, rule that) + + from step + obtain ST' LT' where + s': "phi C sig ! Suc pc = Some (ST', LT')" + by (simp add: step_def split_paired_Ex) (elim, rule that) + + from X + obtain T where + X_Ref: "X = RefT T" + by - (drule widen_RefT2, erule exE, rule that) + + from s ins frame + obtain + a_stk: "approx_stk G hp stk (rev apTs @ X # ST)" and + a_loc: "approx_loc G hp loc LT" and + suc_l: "length loc = Suc (length (snd sig) + maxl)" + by (simp add: correct_frame_def) + + from a_stk + obtain opTs stk' oX where + opTs: "approx_stk G hp opTs (rev apTs)" and + oX: "approx_val G hp oX (Ok X)" and + a_stk': "approx_stk G hp stk' ST" and + stk': "stk = opTs @ oX # stk'" and + l_o: "length opTs = length apTs" + "length stk' = length ST" + by - (drule approx_stk_append_lemma, simp, elim, simp) + + from oX + have "\T'. typeof (option_map obj_ty \ hp) oX = Some T' \ G \ T' \ X" + by (clarsimp simp add: approx_val_def conf_def) + + with X_Ref + obtain T' where + oX_Ref: "typeof (option_map obj_ty \ hp) oX = Some (RefT T')" + "G \ RefT T' \ X" + apply (elim, simp) + apply (frule widen_RefT2) + by (elim, simp) + + from stk' l_o l + have oX_pos: "last (take (Suc (length pTs)) stk) = oX" + by simp + + with state' method ins + have Null_ok: "oX = Null \ ?thesis" + by (simp add: correct_state_def raise_xcpt_def) + + { fix ref + assume oX_Addr: "oX = Addr ref" + + with oX_Ref + obtain obj where + loc: "hp ref = Some obj" "obj_ty obj = RefT T'" + by clarsimp + + then + obtain D where + obj_ty: "obj_ty obj = Class D" + by (auto simp add: obj_ty_def) + + with X_Ref oX_Ref loc + obtain D: "G \ Class D \ X" + by simp + + with X_Ref + obtain X' where + X': "X = Class X'" + by - (drule widen_Class, elim, rule that) + + with X + have "G \ X' \C C'" + by simp + + with mC' wfprog + obtain D0 rT0 maxl0 ins0 where + mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxl0, ins0)" "G\rT0\rT" + by (auto dest: subtype_widen_methd) + + from X' D + have "G \ D \C X'" + by simp + + with wfprog mX + obtain D'' rT' mxl' ins' where + mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxl', ins')" + "G \ rT' \ rT0" + by (auto dest: subtype_widen_methd) + + from mX mD + have rT': "G \ rT' \ rT" + by - (rule widen_trans) + + from mD wfprog + obtain mD'': + "method (G, D'') (mn, pTs) = Some (D'', rT', mxl', ins')" + "is_class G D''" + by (auto dest: method_in_md) + + from loc obj_ty + have "fst (the (hp ref)) = D" + by (simp add: obj_ty_def) + + with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD + have state'_val: + "state' = + Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' arbitrary, + D'', (mn, pTs), 0) # (stk', loc, C, sig, Suc pc) # frs)" + (is "state' = Norm (hp, ?f # ?f' # frs)") + by (simp add: raise_xcpt_def) + + from wtprog mD'' + have start: "wt_start G D'' pTs mxl' (phi D'' (mn, pTs)) \ ins' \ []" + by (auto dest: wt_jvm_prog_impl_wt_start) + + then + obtain LT0 where + LT0: "phi D'' (mn, pTs) ! 0 = Some ([], LT0)" + by (clarsimp simp add: wt_start_def sup_state_def) + + have c_f: "correct_frame G hp ([], LT0) mxl' ins' ?f" + proof - + from start LT0 + have sup_loc: + "G \ (Ok (Class D'') # map Ok pTs @ replicate mxl' Err) <=l LT0" + (is "G \ ?LT <=l LT0") + by (simp add: wt_start_def sup_state_def) + + have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)" + by (simp add: approx_loc_def approx_val_Err list_all2_def set_replicate_conv_if) + + from wfprog mD + have "G \ Class D \ Class D''" + by (auto dest: method_wf_mdecl) + with obj_ty loc + have a: "approx_val G hp (Addr ref) (Ok (Class D''))" + by (simp add: approx_val_def conf_def) + + from w l + have "\x\set (zip (rev apTs) (rev pTs)). x \ widen G" + by (auto simp add: zip_rev) + with wfprog l l_o opTs + have "approx_loc G hp opTs (map Ok (rev pTs))" + by (auto intro: assConv_approx_stk_imp_approx_loc) + hence "approx_stk G hp opTs (rev pTs)" + by (simp add: approx_stk_def) + hence "approx_stk G hp (rev opTs) pTs" + by (simp add: approx_stk_rev) + + with r a l_o l + have "approx_loc G hp (Addr ref # rev opTs @ replicate mxl' arbitrary) ?LT" + (is "approx_loc G hp ?lt ?LT") + by (auto simp add: approx_loc_append approx_stk_def) + + from wfprog this sup_loc + have "approx_loc G hp ?lt LT0" + by (rule approx_loc_imp_approx_loc_sup) + + with start l_o l + show ?thesis + by (simp add: correct_frame_def) + qed + + have c_f': "correct_frame G hp (tl ST', LT') maxl ins ?f'" + proof - + from s s' mC' step l + have "G \ LT <=l LT'" + by (simp add: step_def sup_state_def) + with wfprog a_loc + have a: "approx_loc G hp loc LT'" + by (rule approx_loc_imp_approx_loc_sup) + moreover + from s s' mC' step l + have "G \ map Ok ST <=l map Ok (tl ST')" + by (auto simp add: step_def sup_state_def map_eq_Cons) + with wfprog a_stk' + have "approx_stk G hp stk' (tl ST')" + by (rule approx_stk_imp_approx_stk_sup) + ultimately + show ?thesis + by (simp add: correct_frame_def suc_l pc) + qed + + with state'_val heap_ok mD'' ins method phi_pc s X' l + frames s' LT0 c_f c_f' + have ?thesis + by (simp add: correct_state_def) (intro exI conjI, force+) + } + + with Null_ok oX_Ref + show "G,phi \JVM state'\" + by - (cases oX, auto) +qed + +lemmas [simp del] = map_append + +lemma Return_correct: +"\ wt_jvm_prog G phi; + method (G,C) sig = Some (C,rT,maxl,ins); + ins ! pc = Return; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\" +apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm) +apply (frule wt_jvm_prog_impl_wt_instr) +apply (tactic "EVERY1[atac, etac Suc_lessD]") +apply (unfold wt_jvm_prog_def) +apply (tactic {* fast_tac (claset() + addDs [thm "subcls_widen_methd"] + addEs [rotate_prems 1 widen_trans] + addIs [conf_widen] + addss (simpset() addsimps [thm "approx_val_def",thm "append_eq_conv_conj", map_eq_Cons]@thms "defs1")) 1 *}) +. + +lemmas [simp] = map_append + +lemma Goto_correct: +"\ wf_prog wt G; + method (G,C) sig = Some (C,rT,maxl,ins); + ins ! pc = Goto branch; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\" +apply (clarsimp simp add: defs1) +apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup) +. + + +lemma Ifcmpeq_correct: +"\ wf_prog wt G; + method (G,C) sig = Some (C,rT,maxl,ins); + ins ! pc = Ifcmpeq branch; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\" +apply (clarsimp simp add: defs1) +apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup) +. + +lemma Pop_correct: +"\ wf_prog wt G; + method (G,C) sig = Some (C,rT,maxl,ins); + ins ! pc = Pop; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\" +apply (clarsimp simp add: defs1) +apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup) +. + +lemma Dup_correct: +"\ wf_prog wt G; + method (G,C) sig = Some (C,rT,maxl,ins); + ins ! pc = Dup; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\" +apply (clarsimp simp add: defs1 map_eq_Cons) +apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup + simp add: defs1 map_eq_Cons) +. + +lemma Dup_x1_correct: +"\ wf_prog wt G; + method (G,C) sig = Some (C,rT,maxl,ins); + ins ! pc = Dup_x1; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\" +apply (clarsimp simp add: defs1 map_eq_Cons) +apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup + simp add: defs1 map_eq_Cons) +. + +lemma Dup_x2_correct: +"\ wf_prog wt G; + method (G,C) sig = Some (C,rT,maxl,ins); + ins ! pc = Dup_x2; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\" +apply (clarsimp simp add: defs1 map_eq_Cons) +apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup + simp add: defs1 map_eq_Cons) +. + +lemma Swap_correct: +"\ wf_prog wt G; + method (G,C) sig = Some (C,rT,maxl,ins); + ins ! pc = Swap; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\" +apply (clarsimp simp add: defs1 map_eq_Cons) +apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup + simp add: defs1 map_eq_Cons) +. + +lemma IAdd_correct: +"\ wf_prog wt G; + method (G,C) sig = Some (C,rT,maxl,ins); + ins ! pc = IAdd; + wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ +\ G,phi \JVM state'\" +apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def) +apply (blast intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup) +. + + +(** instr correct **) + +lemma instr_correct: +"\ wt_jvm_prog G phi; + method (G,C) sig = Some (C,rT,maxl,ins); + 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'\" +apply (frule wt_jvm_prog_impl_wt_instr_cor) +apply assumption+ +apply (cases "ins!pc") +prefer 9 +apply (blast intro: Invoke_correct) +prefer 9 +apply (blast intro: Return_correct) +apply (unfold wt_jvm_prog_def) +apply (fast intro: Load_correct Store_correct Bipush_correct Aconst_null_correct + Checkcast_correct Getfield_correct Putfield_correct New_correct + Goto_correct Ifcmpeq_correct Pop_correct Dup_correct + Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+ +. + + +(** Main **) + +lemma correct_state_impl_Some_method: + "G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ + \ \meth. method (G,C) sig = Some(C,meth)" +by (auto simp add: correct_state_def Let_def) + + +lemma BV_correct_1 [rulify]: +"\state. \ wt_jvm_prog G phi; G,phi \JVM state\\ + \ exec (G,state) = Some state' \ G,phi \JVM state'\"; +apply (tactic "split_all_tac 1") +apply (rename_tac xp hp frs) +apply (case_tac xp) + apply (case_tac frs) + apply simp + apply (tactic "split_all_tac 1") + apply (tactic "hyp_subst_tac 1") + apply (frule correct_state_impl_Some_method) + apply (force intro: instr_correct) +apply (case_tac frs) +apply simp+ +. + + +lemma L0: + "\ xp=None; frs\[] \ \ (\state'. exec (G,xp,hp,frs) = Some state')" +by (clarsimp simp add: neq_Nil_conv simp del: split_paired_Ex) + +lemma L1: + "\wt_jvm_prog G phi; G,phi \JVM (xp,hp,frs)\; xp=None; frs\[]\ + \ \state'. exec(G,xp,hp,frs) = Some state' \ G,phi \JVM state'\" +apply (drule L0) +apply assumption +apply (fast intro: BV_correct_1) +. + + +theorem BV_correct [rulify]: +"\ wt_jvm_prog G phi; G \ s -jvm\ t \ \ G,phi \JVM s\ \ G,phi \JVM t\" +apply (unfold exec_all_def) +apply (erule rtrancl_induct) + apply simp +apply (auto intro: BV_correct_1) +. + + +theorem BV_correct_initial: +"\ wt_jvm_prog G phi; G \ s0 -jvm\ (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \JVM s0 \\ + \ approx_stk G hp stk (fst (the (((phi C) sig) ! pc))) \ approx_loc G hp loc (snd (the (((phi C) sig) ! pc)))" +apply (drule BV_correct) +apply assumption+ +apply (simp add: correct_state_def correct_frame_def split_def split: option.splits) +. + +end diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/Convert.thy --- a/src/HOL/MicroJava/BV/Convert.thy Wed Aug 30 21:44:12 2000 +0200 +++ b/src/HOL/MicroJava/BV/Convert.thy Wed Aug 30 21:47:39 2000 +0200 @@ -1,63 +1,106 @@ (* Title: HOL/MicroJava/BV/Convert.thy ID: $Id$ - Author: Cornelia Pusch + Author: Cornelia Pusch and Gerwin Klein Copyright 1999 Technische Universitaet Muenchen +*) -The supertype relation lifted to type options, type lists and state types. -*) +header "Lifted Type Relations" theory Convert = JVMExec: +text "The supertype relation lifted to type err, type lists and state types." + +datatype 'a err = Err | Ok 'a + types - locvars_type = "ty option list" + locvars_type = "ty err list" opstack_type = "ty list" state_type = "opstack_type \ locvars_type" -constdefs + +consts + strict :: "('a \ 'b err) \ ('a err \ 'b err)" +primrec + "strict f Err = Err" + "strict f (Ok x) = f x" + +consts + opt_map :: "('a \ 'b) \ ('a option \ 'b option)" +primrec + "opt_map f None = None" + "opt_map f (Some x) = Some (f x)" + +consts + val :: "'a err \ 'a" +primrec + "val (Ok s) = s" - (* lifts a relation to option with None as top element *) - lift_top :: "('a \ 'a \ bool) \ ('a option \ 'a option \ bool)" + +constdefs + (* lifts a relation to err with Err as top element *) + lift_top :: "('a \ 'b \ bool) \ ('a err \ 'b err \ bool)" "lift_top P a' a \ case a of - None \ True - | Some t \ (case a' of None \ False | Some t' \ P t' t)" + Err \ True + | Ok t \ (case a' of Err \ False | Ok t' \ P t' t)" + + (* lifts a relation to option with None as bottom element *) + lift_bottom :: "('a \ 'b \ bool) \ ('a option \ 'b option \ bool)" + "lift_bottom P a' a \ case a' of + None \ True + | Some t' \ (case a of None \ False | Some t \ P t' t)" + + sup_ty_opt :: "['code prog,ty err,ty err] \ bool" ("_ \_ <=o _") + "sup_ty_opt G \ lift_top (\t t'. G \ t \ t')" + + sup_loc :: "['code prog,locvars_type,locvars_type] \ bool" + ("_ \ _ <=l _" [71,71] 70) + "G \ LT <=l LT' \ list_all2 (\t t'. (G \ t <=o t')) LT LT'" + + sup_state :: "['code prog,state_type,state_type] \ bool" + ("_ \ _ <=s _" [71,71] 70) + "G \ s <=s s' \ (G \ map Ok (fst s) <=l map Ok (fst s')) \ G \ snd s <=l snd s'" + + sup_state_opt :: "['code prog,state_type option,state_type option] \ bool" + ("_ \ _ <=' _" [71,71] 70) + "sup_state_opt G \ lift_bottom (\t t'. G \ t <=s t')" - sup_ty_opt :: "['code prog,ty option,ty option] \ bool" ("_ \_ <=o _") - "sup_ty_opt G \ lift_top (\t t'. G \ t \ t')" +lemma not_Err_eq [iff]: + "(x \ Err) = (\a. x = Ok a)" + by (cases x) auto - sup_loc :: "['code prog,locvars_type,locvars_type] \ bool" ("_ \ _ <=l _" [71,71] 70) - "G \ LT <=l LT' \ list_all2 (\t t'. (G \ t <=o t')) LT LT'" - - sup_state :: "['code prog,state_type,state_type] \ bool" ("_ \ _ <=s _" [71,71] 70) - "G \ s <=s s' \ (G \ map Some (fst s) <=l map Some (fst s')) \ G \ snd s <=l snd s'" +lemma not_Some_eq [iff]: + "(\y. x \ Ok y) = (x = Err)" + by (cases x) auto lemma lift_top_refl [simp]: "[| !!x. P x x |] ==> lift_top P x x" - by (simp add: lift_top_def split: option.splits) + by (simp add: lift_top_def split: err.splits) lemma lift_top_trans [trans]: - "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |] ==> lift_top P x z" + "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |] + ==> lift_top P x z" proof - assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z" assume a: "lift_top P x y" assume b: "lift_top P y z" - { assume "z = None" + { assume "z = Err" hence ?thesis by (simp add: lift_top_def) } note z_none = this - { assume "x = None" + { assume "x = Err" with a b have ?thesis - by (simp add: lift_top_def split: option.splits) + by (simp add: lift_top_def split: err.splits) } note x_none = this { fix r t - assume x: "x = Some r" and z: "z = Some t" + assume x: "x = Ok r" and z: "z = Ok t" with a b - obtain s where y: "y = Some s" - by (simp add: lift_top_def split: option.splits) + obtain s where y: "y = Ok s" + by (simp add: lift_top_def split: err.splits) from a x y have "P r s" by (simp add: lift_top_def) @@ -75,21 +118,82 @@ show ?thesis by blast qed -lemma lift_top_None_any [simp]: - "lift_top P None any = (any = None)" - by (simp add: lift_top_def split: option.splits) +lemma lift_top_Err_any [simp]: + "lift_top P Err any = (any = Err)" + by (simp add: lift_top_def split: err.splits) + +lemma lift_top_Ok_Ok [simp]: + "lift_top P (Ok a) (Ok b) = P a b" + by (simp add: lift_top_def split: err.splits) + +lemma lift_top_any_Ok [simp]: + "lift_top P any (Ok b) = (\a. any = Ok a \ P a b)" + by (simp add: lift_top_def split: err.splits) + +lemma lift_top_Ok_any: + "lift_top P (Ok a) any = (any = Err \ (\b. any = Ok b \ P a b))" + by (simp add: lift_top_def split: err.splits) -lemma lift_top_Some_Some [simp]: - "lift_top P (Some a) (Some b) = P a b" - by (simp add: lift_top_def split: option.splits) + +lemma lift_bottom_refl [simp]: + "[| !!x. P x x |] ==> lift_bottom P x x" + by (simp add: lift_bottom_def split: option.splits) + +lemma lift_bottom_trans [trans]: + "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_bottom P x y; lift_bottom P y z |] + ==> lift_bottom P x z" +proof - + assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z" + assume a: "lift_bottom P x y" + assume b: "lift_bottom P y z" + + { assume "x = None" + hence ?thesis by (simp add: lift_bottom_def) + } note z_none = this -lemma lift_top_any_Some [simp]: - "lift_top P any (Some b) = (\a. any = Some a \ P a b)" - by (simp add: lift_top_def split: option.splits) + { assume "z = None" + with a b + have ?thesis + by (simp add: lift_bottom_def split: option.splits) + } note x_none = this + + { fix r t + assume x: "x = Some r" and z: "z = Some t" + with a b + obtain s where y: "y = Some s" + by (simp add: lift_bottom_def split: option.splits) + + from a x y + have "P r s" by (simp add: lift_bottom_def) + also + from b y z + have "P s t" by (simp add: lift_bottom_def) + finally + have "P r t" . -lemma lift_top_Some_any: - "lift_top P (Some a) any = (any = None \ (\b. any = Some b \ P a b))" - by (simp add: lift_top_def split: option.splits) + with x z + have ?thesis by (simp add: lift_bottom_def) + } + + with x_none z_none + show ?thesis by blast +qed + +lemma lift_bottom_any_None [simp]: + "lift_bottom P any None = (any = None)" + by (simp add: lift_bottom_def split: option.splits) + +lemma lift_bottom_Some_Some [simp]: + "lift_bottom P (Some a) (Some b) = P a b" + by (simp add: lift_bottom_def split: option.splits) + +lemma lift_bottom_any_Some [simp]: + "lift_bottom P (Some a) any = (\b. any = Some b \ P a b)" + by (simp add: lift_bottom_def split: option.splits) + +lemma lift_bottom_Some_any: + "lift_bottom P any (Some b) = (any = None \ (\a. any = Some a \ P a b))" + by (simp add: lift_bottom_def split: option.splits) @@ -105,18 +209,21 @@ "G \ s <=s s" by (simp add: sup_state_def) +theorem sup_state_opt_refl [simp]: + "G \ s <=' s" + by (simp add: sup_state_opt_def) -theorem anyConvNone [simp]: - "(G \ None <=o any) = (any = None)" +theorem anyConvErr [simp]: + "(G \ Err <=o any) = (any = Err)" by (simp add: sup_ty_opt_def) -theorem SomeanyConvSome [simp]: - "(G \ (Some ty') <=o (Some ty)) = (G \ ty' \ ty)" +theorem OkanyConvOk [simp]: + "(G \ (Ok ty') <=o (Ok ty)) = (G \ ty' \ ty)" by (simp add: sup_ty_opt_def) -theorem sup_ty_opt_Some: - "G \ a <=o (Some b) \ \ x. a = Some x" +theorem sup_ty_opt_Ok: + "G \ a <=o (Ok b) \ \ x. a = Ok x" by (clarsimp simp add: sup_ty_opt_def) lemma widen_PrimT_conv1 [simp]: @@ -124,8 +231,8 @@ by (auto elim: widen.elims) theorem sup_PTS_eq: - "(G \ Some (PrimT p) <=o X) = (X=None \ X = Some (PrimT p))" - by (auto simp add: sup_ty_opt_def lift_top_Some_any) + "(G \ Ok (PrimT p) <=o X) = (X=Err \ X = Ok (PrimT p))" + by (auto simp add: sup_ty_opt_def lift_top_Ok_any) @@ -138,7 +245,7 @@ by (simp add: sup_loc_def list_all2_Cons1) theorem sup_loc_Cons2: - "(G \ YT <=l (X#XT)) = (\Y YT'. YT=Y#YT' \ (G \ Y <=o X) \ (G \ YT' <=l XT))"; + "(G \ YT <=l (X#XT)) = (\Y YT'. YT=Y#YT' \ (G \ Y <=o X) \ (G \ YT' <=l XT))" by (simp add: sup_loc_def list_all2_Cons2) @@ -178,8 +285,8 @@ theorem all_nth_sup_loc: - "\b. length a = length b \ (\ n. n < length a \ (G \ (a!n) <=o (b!n))) \ (G \ a <=l b)" - (is "?P a") + "\b. length a = length b \ (\ n. n < length a \ (G \ (a!n) <=o (b!n))) \ + (G \ a <=l b)" (is "?P a") proof (induct a) show "?P []" by simp @@ -206,12 +313,13 @@ theorem sup_loc_append: - "[| length a = length b |] ==> (G \ (a@x) <=l (b@y)) = ((G \ a <=l b) \ (G \ x <=l y))" + "length a = length b ==> + (G \ (a@x) <=l (b@y)) = ((G \ a <=l b) \ (G \ x <=l y))" proof - assume l: "length a = length b" - have "\b. length a = length b \ (G \ (a@x) <=l (b@y)) = ((G \ a <=l b) \ (G \ x <=l y))" - (is "?P a") + have "\b. length a = length b \ (G \ (a@x) <=l (b@y)) = ((G \ a <=l b) \ + (G \ x <=l y))" (is "?P a") proof (induct a) show "?P []" by simp @@ -219,7 +327,7 @@ show "?P (l#ls)" proof (intro strip) fix b - assume "length (l#ls) = length (b::ty option list)" + assume "length (l#ls) = length (b::ty err list)" with IH show "(G \ ((l#ls)@x) <=l (b@y)) = ((G \ (l#ls) <=l b) \ (G \ x <=l y))" by - (cases b, auto) @@ -276,8 +384,8 @@ theorem sup_loc_update [rulify]: - "\ n y. (G \ a <=o b) \ n < length y \ (G \ x <=l y) \ (G \ x[n := a] <=l y[n := b])" - (is "?P x") + "\ n y. (G \ a <=o b) \ n < length y \ (G \ x <=l y) \ + (G \ x[n := a] <=l y[n := b])" (is "?P x") proof (induct x) show "?P []" by simp @@ -294,23 +402,28 @@ theorem sup_state_length [simp]: - "G \ s2 <=s s1 \ length (fst s2) = length (fst s1) \ length (snd s2) = length (snd s1)" + "G \ s2 <=s s1 ==> + length (fst s2) = length (fst s1) \ length (snd s2) = length (snd s1)" by (auto dest: sup_loc_length simp add: sup_state_def); theorem sup_state_append_snd: - "length a = length b \ (G \ (i,a@x) <=s (j,b@y)) = ((G \ (i,a) <=s (j,b)) \ (G \ (i,x) <=s (j,y)))" + "length a = length b ==> + (G \ (i,a@x) <=s (j,b@y)) = ((G \ (i,a) <=s (j,b)) \ (G \ (i,x) <=s (j,y)))" by (auto simp add: sup_state_def sup_loc_append) theorem sup_state_append_fst: - "length a = length b \ (G \ (a@x,i) <=s (b@y,j)) = ((G \ (a,i) <=s (b,j)) \ (G \ (x,i) <=s (y,j)))" + "length a = length b ==> + (G \ (a@x,i) <=s (b@y,j)) = ((G \ (a,i) <=s (b,j)) \ (G \ (x,i) <=s (y,j)))" by (auto simp add: sup_state_def sup_loc_append) theorem sup_state_Cons1: - "(G \ (x#xt, a) <=s (yt, b)) = (\y yt'. yt=y#yt' \ (G \ x \ y) \ (G \ (xt,a) <=s (yt',b)))" + "(G \ (x#xt, a) <=s (yt, b)) = + (\y yt'. yt=y#yt' \ (G \ x \ y) \ (G \ (xt,a) <=s (yt',b)))" by (auto simp add: sup_state_def map_eq_Cons) theorem sup_state_Cons2: - "(G \ (xt, a) <=s (y#yt, b)) = (\x xt'. xt=x#xt' \ (G \ x \ y) \ (G \ (xt',a) <=s (yt,b)))" + "(G \ (xt, a) <=s (y#yt, b)) = + (\x xt'. xt=x#xt' \ (G \ x \ y) \ (G \ (xt',a) <=s (yt,b)))" by (auto simp add: sup_state_def map_eq_Cons sup_loc_Cons2) theorem sup_state_ignore_fst: @@ -324,11 +437,32 @@ show ?thesis by (simp add: m sup_state_def) qed + +lemma sup_state_opt_None_any [iff]: + "(G \ None <=' any) = True" + by (simp add: sup_state_opt_def lift_bottom_def) + +lemma sup_state_opt_any_None [iff]: + "(G \ any <=' None) = (any = None)" + by (simp add: sup_state_opt_def) + +lemma sup_state_opt_Some_Some [iff]: + "(G \ (Some a) <=' (Some b)) = (G \ a <=s b)" + by (simp add: sup_state_opt_def del: split_paired_Ex) + +lemma sup_state_opt_any_Some [iff]: + "(G \ (Some a) <=' any) = (\b. any = Some b \ G \ a <=s b)" + by (simp add: sup_state_opt_def) + +lemma sup_state_opt_Some_any: + "(G \ any <=' (Some b)) = (any = None \ (\a. any = Some a \ G \ a <=s b))" + by (simp add: sup_state_opt_def lift_bottom_Some_any) + + theorem sup_ty_opt_trans [trans]: "\G \ a <=o b; G \ b <=o c\ \ G \ a <=o c" by (auto intro: lift_top_trans widen_trans simp add: sup_ty_opt_def) - theorem sup_loc_trans [trans]: "\G \ a <=l b; G \ b <=l c\ \ G \ a <=l c" proof - @@ -359,4 +493,9 @@ "\G \ a <=s b; G \ b <=s c\ \ G \ a <=s c" by (auto intro: sup_loc_trans simp add: sup_state_def) +theorem sup_state_opt_trans [trans]: + "\G \ a <=' b; G \ b <=' c\ \ G \ a <=' c" + by (auto intro: lift_bottom_trans sup_state_trans simp add: sup_state_opt_def) + + end diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/Correct.ML --- a/src/HOL/MicroJava/BV/Correct.ML Wed Aug 30 21:44:12 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,263 +0,0 @@ -(* Title: HOL/MicroJava/BV/Correct.ML - ID: $Id$ - Author: Cornelia Pusch - Copyright 1999 Technische Universitaet Muenchen -*) - -(** sup_heap **) - -Goalw [hext_def] - "hp x = None \\ hp \\| (hp((newref hp) \\ obj))"; -by (asm_full_simp_tac (simpset() addsimps []) 1); -by (Clarify_tac 1); -bd newref_None 1; -back(); -by (asm_full_simp_tac (simpset() addsimps []) 1); -qed_spec_mp "sup_heap_newref"; - - -Goalw [hext_def] -"hp a = Some (C,od') \\ hp \\| (hp(a \\ (C,od)))"; -by (asm_full_simp_tac (simpset() addsimps []) 1); -qed_spec_mp "sup_heap_update_value"; - - -(** approx_val **) - -Goalw [approx_val_def] -"approx_val G hp x None"; -by (Asm_full_simp_tac 1); -qed_spec_mp "approx_val_None"; - - -Goalw [approx_val_def] -"approx_val G hp Null (Some(RefT x))"; -by(Simp_tac 1); -by (fast_tac (claset() addIs widen.intrs) 1); -qed_spec_mp "approx_val_Null"; - - -Goal -"\\ wf_prog wt G \\ \ -\\\ approx_val G hp v (Some T) \\ G\\ T\\T' \\ approx_val G hp v (Some T')"; -by (case_tac "T" 1); - by (fast_tac (claset() addIs [conf_widen] addss (simpset()addsimps[approx_val_def])) 1); -by (fast_tac (claset() addIs [conf_widen] addss (simpset()addsimps[approx_val_def])) 1); -qed_spec_mp "approx_val_imp_approx_val_assConvertible"; - - -Goal -"approx_val G hp val at \\ hp \\| hp' \\ approx_val G hp' val at"; -by (asm_full_simp_tac (simpset() setloop (split_tac [option.split]) - addsimps [approx_val_def]) 1); -by(blast_tac (claset() addIs [conf_hext]) 1); -qed_spec_mp "approx_val_imp_approx_val_sup_heap"; - -Goal -"\\ hp a = Some obj' ; G,hp\\ v\\\\T ; obj_ty obj = obj_ty obj' \\ \ -\\\G,(hp(a\\obj))\\ v\\\\T"; -by (case_tac "v" 1); -by (auto_tac (claset() , simpset() addsimps [obj_ty_def,conf_def] addsplits [option.split])); -qed_spec_mp "approx_val_imp_approx_val_heap_update"; - - -Goal -"wf_prog wt G \\ approx_val G h val us \\ G \\ us <=o us' \\ approx_val G h val us'"; -by (asm_simp_tac (simpset() addsimps [thm "sup_PTS_eq",approx_val_def] addsplits [option.split,val_.split,ty.split]) 1); -by(blast_tac (claset() addIs [conf_widen]) 1); -qed_spec_mp "approx_val_imp_approx_val_sup"; - - -Goalw [approx_loc_def,list_all2_def] -"\\ wf_prog wt G; approx_loc G hp loc LT; idx < length LT ; val = loc ! idx ; G \\ LT ! idx <=o at\\ \ -\\\ approx_val G hp val at"; -by (fast_tac (claset() addIs [approx_val_imp_approx_val_sup] addss (simpset() addsimps - [split_def,all_set_conv_all_nth])) 1); -qed "approx_loc_imp_approx_val_sup"; - - -(** approx_loc **) - -Goalw [approx_loc_def] -"approx_loc G hp (s#xs) (l#ls) = \ -\ (approx_val G hp s l \\ approx_loc G hp xs ls)"; -by (Simp_tac 1); -qed "approx_loc_Cons"; -AddIffs [approx_loc_Cons]; - - -Goalw [approx_stk_def,approx_loc_def,list_all2_def] -"\\ wf_prog wt G \\ \ -\\\ (\\tt'\\set (zip tys_n ts). tt' \\ widen G) \\ \ -\ length tys_n = length ts \\ approx_stk G hp s tys_n \\ approx_loc G hp s (map Some ts)"; -by (force_tac (claset() addIs [approx_val_imp_approx_val_assConvertible], simpset() - addsimps [all_set_conv_all_nth,split_def]) 1); -qed_spec_mp "assConv_approx_stk_imp_approx_loc"; - - -Goalw [approx_loc_def,list_all2_def] -"\\ lvars. approx_loc G hp lvars lt \\ hp \\| hp' \\ approx_loc G hp' lvars lt"; -by (case_tac "lt" 1); - by (Asm_simp_tac 1); -by (force_tac (claset() addIs [approx_val_imp_approx_val_sup_heap], - simpset() addsimps [neq_Nil_conv]) 1); -qed_spec_mp "approx_loc_imp_approx_loc_sup_heap"; - - -Goalw [thm "sup_loc_def",approx_loc_def,list_all2_def] -"wf_prog wt G \\ approx_loc G hp lvars lt \\ G \\ lt <=l lt' \\ approx_loc G hp lvars lt'"; -by (auto_tac (claset() , simpset() addsimps [all_set_conv_all_nth,split_def])); -by (auto_tac (claset() addEs [approx_val_imp_approx_val_sup] , simpset())); -qed_spec_mp "approx_loc_imp_approx_loc_sup"; - - -Goalw [approx_loc_def,list_all2_def] -"\\loc idx x X. (approx_loc G hp loc LT) \\ (approx_val G hp x X) \ -\ \\ (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"; -by (fast_tac (claset() addDs [set_update_subset_insert RS subsetD] - addss (simpset() addsimps [zip_update])) 1); -qed_spec_mp "approx_loc_imp_approx_loc_subst"; - - -Goalw [approx_loc_def,list_all2_def] -"\\L1 l2 L2. length l1=length L1 \ -\ \\ approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \\ approx_loc G hp l2 L2)"; -by(simp_tac (simpset() addcongs [conj_cong] addsimps [zip_append]) 1); -by(Blast_tac 1); -qed_spec_mp "approx_loc_append"; - - -(** approx_stk **) - -Goalw [approx_stk_def,approx_loc_def,list_all2_def] -"approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"; -by (fast_tac (claset() addss (simpset() addsimps [zip_rev,rev_map RS sym])) 1); -qed_spec_mp "approx_stk_rev_lem"; - -Goal -"approx_stk G hp (rev s) t = approx_stk G hp s (rev t)"; -by (fast_tac (claset() addIs [approx_stk_rev_lem RS subst] addss (simpset())) 1); -qed_spec_mp "approx_stk_rev"; - -Goalw [approx_stk_def] -"\\ lvars. approx_stk G hp lvars lt \\ hp \\| hp' \\ approx_stk G hp' lvars lt"; -by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup_heap]) 1); -qed_spec_mp "approx_stk_imp_approx_stk_sup_heap"; - - -Goalw [approx_stk_def] -"wf_prog wt G \\ approx_stk G hp lvars st \\ G \\ (map Some st) <=l (map Some st') \\ approx_stk G hp lvars st'"; -by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup]) 1); -qed_spec_mp "approx_stk_imp_approx_stk_sup"; - -Goalw [approx_stk_def,approx_loc_def] -"approx_stk G hp [] []"; -by (Simp_tac 1); -qed "approx_stk_Nil"; -AddIffs [approx_stk_Nil]; - -Goalw [approx_stk_def,approx_loc_def] -"approx_stk G hp (x # stk) (S#ST) = (approx_val G hp x (Some S) \\ approx_stk G hp stk ST)"; -by (Simp_tac 1); -qed "approx_stk_Cons"; -AddIffs [approx_stk_Cons]; - -Goalw [approx_stk_def,approx_loc_def] -"approx_stk G hp stk (S#ST') = \ -\ (\\s stk'. stk = s#stk' \\ approx_val G hp s (Some S) \\ approx_stk G hp stk' ST')"; -by (asm_full_simp_tac (simpset() addsimps [list_all2_Cons2]) 1); -qed "approx_stk_Cons_lemma"; -AddIffs [approx_stk_Cons_lemma]; - - -Goalw [approx_stk_def,approx_loc_def] -"approx_stk G hp stk (S@ST') \ -\ \\ (\\s stk'. stk = s@stk' \\ length s = length S \\ length stk' = length ST' \\ \ -\ approx_stk G hp s S \\ approx_stk G hp stk' ST')"; -by(asm_full_simp_tac (simpset() addsimps [list_all2_append2]) 1); -qed_spec_mp "approx_stk_append_lemma"; - - -(** oconf **) - -Goalw [oconf_def,lconf_def] -"\\ is_class G C; wf_prog wt G \\ \\ \ -\G,h\\ (C, map_of (map (\\(f,fT).(f,default_val fT)) (fields(G,C))))\\"; -by (asm_full_simp_tac (simpset() addsimps [map_of_map]) 1); -by (force_tac (claset() addIs [defval_conf] - addDs [map_of_SomeD,is_type_fields],simpset()) 1); -qed "correct_init_obj"; - - -Goalw [oconf_def,lconf_def] -"\\ map_of (fields (G, oT)) FD = Some T ; G,hp\\v\\\\T ; \ -\ G,hp\\(oT,fs)\\ \\ \ -\\\ G,hp\\(oT, fs(FD\\v))\\"; -by (asm_full_simp_tac (simpset() addsplits [ty.split]) 1); -qed_spec_mp "oconf_imp_oconf_field_update"; - - -Goalw [oconf_def,lconf_def] -"hp x = None \\ G,hp\\obj\\ \\ G,hp\\obj'\\ \ -\ \\ G,(hp(newref hp\\obj'))\\obj\\"; -by (Asm_full_simp_tac 1); -by (fast_tac (claset() addIs [conf_hext,sup_heap_newref]) 1); -qed_spec_mp "oconf_imp_oconf_heap_newref"; - -Goalw [oconf_def,lconf_def] -"hp a = Some obj' \\ obj_ty obj' = obj_ty obj'' \\ G,hp\\obj\\ \ -\ \\ G,hp(a\\obj'')\\obj\\"; -by (Asm_full_simp_tac 1); -by (fast_tac (claset() addIs [approx_val_imp_approx_val_heap_update] addss (simpset())) 1); -qed_spec_mp "oconf_imp_oconf_heap_update"; - - -(** hconf **) - - -Goal "hp x = None \\ G\\h hp\\ \\ G,hp\\obj\\ \\ G\\h hp(newref hp\\obj)\\"; -by (asm_full_simp_tac (simpset() addsplits [split_split] - addsimps [hconf_def]) 1); - by (fast_tac (claset()addIs[oconf_imp_oconf_heap_newref] addss (simpset())) 1); -qed_spec_mp "hconf_imp_hconf_newref"; - - -Goal "map_of (fields (G, oT)) (F, D) = Some T \\ hp oloc = Some(oT,fs) \\ \ -\ G,hp\\v\\\\T \\ G\\h hp\\ \\ G\\h hp(oloc \\ (oT, fs((F,D)\\v)))\\"; -by (asm_full_simp_tac (simpset() addsimps [hconf_def]) 1); -by (fast_tac (claset() addIs - [oconf_imp_oconf_heap_update, oconf_imp_oconf_field_update] - addss (simpset() addsimps [obj_ty_def])) 1); -qed_spec_mp "hconf_imp_hconf_field_update"; - - -(** correct_frames **) - -Delsimps [fun_upd_apply]; -Goal -"\\rT C sig. correct_frames G hp phi rT sig frs \\ \ -\ hp a = Some (C,od) \\ map_of (fields (G, C)) fl = Some fd \\ \ -\ G,hp\\v\\\\fd \ -\ \\ correct_frames G (hp(a \\ (C, od(fl\\v)))) phi rT sig frs"; -by (induct_tac "frs" 1); - by (Asm_full_simp_tac 1); -by (asm_full_simp_tac (simpset() addsimps [split_def,correct_frame_def]) 1); -by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup_heap, - approx_loc_imp_approx_loc_sup_heap, - sup_heap_update_value] addss (simpset())) 1); -qed_spec_mp "correct_frames_imp_correct_frames_field_update"; - - -Goal -"\\rT C sig. hp x = None \\ correct_frames G hp phi rT sig frs \\ \ -\ oconf G hp obj \ -\ \\ correct_frames G (hp(newref hp \\ obj)) phi rT sig frs"; -by (induct_tac "frs" 1); -by (asm_full_simp_tac (simpset() addsimps []) 1); -by (asm_full_simp_tac (simpset() addsimps [split_def,correct_frame_def]) 1); -by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup_heap, - approx_loc_imp_approx_loc_sup_heap, - hconf_imp_hconf_newref, - sup_heap_newref] addss (simpset())) 1); -qed_spec_mp "correct_frames_imp_correct_frames_newref"; - diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/Correct.thy --- a/src/HOL/MicroJava/BV/Correct.thy Wed Aug 30 21:44:12 2000 +0200 +++ b/src/HOL/MicroJava/BV/Correct.thy Wed Aug 30 21:47:39 2000 +0200 @@ -6,60 +6,319 @@ The invariant for the type safety proof. *) -Correct = BVSpec + +header "Type Safety Invariant" + +theory Correct = BVSpec: constdefs - approx_val :: "[jvm_prog,aheap,val,ty option] \\ bool" -"approx_val G h v any \\ case any of None \\ True | Some T \\ G,h\\v\\\\T" + approx_val :: "[jvm_prog,aheap,val,ty err] \ bool" +"approx_val G h v any \ case any of Err \ True | Ok T \ G,h\v\\T" - approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \\ bool" -"approx_loc G hp loc LT \\ list_all2 (approx_val G hp) loc LT" + approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \ bool" +"approx_loc G hp loc LT \ list_all2 (approx_val G hp) loc LT" + + approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \ bool" +"approx_stk G hp stk ST \ approx_loc G hp stk (map Ok ST)" - approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \\ bool" -"approx_stk G hp stk ST \\ approx_loc G hp stk (map Some ST)" + correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] \ frame \ bool" +"correct_frame G hp \ \(ST,LT) maxl ins (stk,loc,C,sig,pc). + approx_stk G hp stk ST \ approx_loc G hp loc LT \ + pc < length ins \ length loc=length(snd sig)+maxl+1" - correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] \\ frame \\ bool" -"correct_frame G hp \\ \\(ST,LT) maxl ins (stk,loc,C,sig,pc). - approx_stk G hp stk ST \\ approx_loc G hp loc LT \\ - pc < length ins \\ length loc=length(snd sig)+maxl+1" + correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] \ frame \ bool" +"correct_frame_opt G hp s \ case s of None \ \maxl ins f. False | Some t \ correct_frame G hp t" + consts - correct_frames :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \\ bool" + correct_frames :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \ bool" primrec "correct_frames G hp phi rT0 sig0 [] = True" "correct_frames G hp phi rT0 sig0 (f#frs) = - (let (stk,loc,C,sig,pc) = f; - (ST,LT) = (phi C sig) ! pc - in - (\\rT maxl ins. - method (G,C) sig = Some(C,rT,(maxl,ins)) \\ - (\\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' \\ - length apTs = length pTs \\ - (\\D' rT' maxl' ins'. - method (G,D) sig0 = Some(D',rT',(maxl',ins')) \\ - G \\ rT0 \\ rT') \\ - correct_frame G hp (tl ST, LT) maxl ins f \\ + (let (stk,loc,C,sig,pc) = f in + (\ST LT rT maxl ins. + phi C sig ! pc = Some (ST,LT) \ + method (G,C) sig = Some(C,rT,(maxl,ins)) \ + (\C' mn pTs k. pc = k+1 \ ins!k = (Invoke C' mn pTs) \ + (mn,pTs) = sig0 \ + (\apTs D ST' LT'. + (phi C sig)!k = Some ((rev apTs) @ (Class D) # ST', LT') \ + length apTs = length pTs \ + (\D' rT' maxl' ins'. + method (G,D) sig0 = Some(D',rT',(maxl',ins')) \ + G \ rT0 \ rT') \ + correct_frame G hp (tl ST, LT) maxl ins f \ correct_frames G hp phi rT sig frs))))" constdefs - correct_state :: "[jvm_prog,prog_type,jvm_state] \\ bool" - ("_,_\\JVM _\\" [51,51] 50) -"correct_state G phi \\ \\(xp,hp,frs). + correct_state :: "[jvm_prog,prog_type,jvm_state] \ bool" + ("_,_\JVM _\" [51,51] 50) +"correct_state G phi \ \(xp,hp,frs). case xp of - None \\ (case frs of - [] \\ True - | (f#fs) \\ G\\h hp\\ \\ + None \ (case frs of + [] \ True + | (f#fs) \ G\h hp\ \ (let (stk,loc,C,sig,pc) = f in - \\rT maxl ins. - method (G,C) sig = Some(C,rT,(maxl,ins)) \\ - correct_frame G hp ((phi C sig) ! pc) maxl ins f \\ + \rT maxl ins s. + method (G,C) sig = Some(C,rT,(maxl,ins)) \ + phi C sig ! pc = Some s \ + correct_frame G hp s maxl ins f \ correct_frames G hp phi rT sig fs)) - | Some x \\ True" + | Some x \ True" + + +lemma sup_heap_newref: + "hp x = None \ hp \| hp(newref hp \ obj)" +apply (unfold hext_def) +apply clarsimp +apply (drule newref_None 1) back +apply simp +. + +lemma sup_heap_update_value: + "hp a = Some (C,od') \ hp \| hp (a \ (C,od))" +by (simp add: hext_def) + + +(** approx_val **) + +lemma approx_val_Err: + "approx_val G hp x Err" +by (simp add: approx_val_def) + +lemma approx_val_Null: + "approx_val G hp Null (Ok (RefT x))" +by (auto intro: null simp add: approx_val_def) + +lemma approx_val_imp_approx_val_assConvertible [rulify]: + "wf_prog wt G \ approx_val G hp v (Ok T) \ G\ T\T' \ approx_val G hp v (Ok T')" +by (cases T) (auto intro: conf_widen simp add: approx_val_def) + +lemma approx_val_imp_approx_val_sup_heap [rulify]: + "approx_val G hp v at \ hp \| hp' \ approx_val G hp' v at" +apply (simp add: approx_val_def split: err.split) +apply (blast intro: conf_hext) +. + +lemma approx_val_imp_approx_val_heap_update: + "\hp a = Some obj'; G,hp\ v\\T; obj_ty obj = obj_ty obj'\ + \ G,hp(a\obj)\ v\\T" +by (cases v, auto simp add: obj_ty_def conf_def) + +lemma approx_val_imp_approx_val_sup [rulify]: + "wf_prog wt G \ (approx_val G h v us) \ (G \ us <=o us') \ (approx_val G h v us')" +apply (simp add: sup_PTS_eq approx_val_def split: err.split) +apply (blast intro: conf_widen) +. + +lemma approx_loc_imp_approx_val_sup: + "\wf_prog wt G; approx_loc G hp loc LT; idx < length LT; v = loc!idx; G \ LT!idx <=o at\ + \ approx_val G hp v at" +apply (unfold approx_loc_def) +apply (unfold list_all2_def) +apply (auto intro: approx_val_imp_approx_val_sup simp add: split_def all_set_conv_all_nth) +. + + +(** approx_loc **) + +lemma approx_loc_Cons [iff]: + "approx_loc G hp (s#xs) (l#ls) = (approx_val G hp s l \ approx_loc G hp xs ls)" +by (simp add: approx_loc_def) + +lemma assConv_approx_stk_imp_approx_loc [rulify]: + "wf_prog wt G \ (\tt'\set (zip tys_n ts). tt' \ widen G) + \ length tys_n = length ts \ approx_stk G hp s tys_n \ + approx_loc G hp s (map Ok ts)" +apply (unfold approx_stk_def approx_loc_def list_all2_def) +apply (clarsimp simp add: all_set_conv_all_nth) +apply (rule approx_val_imp_approx_val_assConvertible) +apply auto +. + + +lemma approx_loc_imp_approx_loc_sup_heap [rulify]: + "\lvars. approx_loc G hp lvars lt \ hp \| hp' \ approx_loc G hp' lvars lt" +apply (unfold approx_loc_def list_all2_def) +apply (cases lt) + apply simp +apply clarsimp +apply (rule approx_val_imp_approx_val_sup_heap) +apply auto +. + +lemma approx_loc_imp_approx_loc_sup [rulify]: + "wf_prog wt G \ approx_loc G hp lvars lt \ G \ lt <=l lt' \ approx_loc G hp lvars lt'" +apply (unfold sup_loc_def approx_loc_def list_all2_def) +apply (auto simp add: all_set_conv_all_nth) +apply (auto elim: approx_val_imp_approx_val_sup) +. + + +lemma approx_loc_imp_approx_loc_subst [rulify]: + "\loc idx x X. (approx_loc G hp loc LT) \ (approx_val G hp x X) + \ (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))" +apply (unfold approx_loc_def list_all2_def) +apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update) +. + + +lemmas [cong] = conj_cong + +lemma approx_loc_append [rulify]: + "\L1 l2 L2. length l1=length L1 \ + approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \ approx_loc G hp l2 L2)" +apply (unfold approx_loc_def list_all2_def) +apply simp +apply blast +. + +lemmas [cong del] = conj_cong + + +(** approx_stk **) + +lemma approx_stk_rev_lem: + "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t" +apply (unfold approx_stk_def approx_loc_def list_all2_def) +apply (auto simp add: zip_rev sym [OF rev_map]) +. + +lemma approx_stk_rev: + "approx_stk G hp (rev s) t = approx_stk G hp s (rev t)" +by (auto intro: subst [OF approx_stk_rev_lem]) + + +lemma approx_stk_imp_approx_stk_sup_heap [rulify]: + "\lvars. approx_stk G hp lvars lt \ hp \| hp' \ approx_stk G hp' lvars lt" +by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def) + +lemma approx_stk_imp_approx_stk_sup [rulify]: + "wf_prog wt G \ approx_stk G hp lvars st \ (G \ map Ok st <=l (map Ok st')) + \ approx_stk G hp lvars st'" +by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def) + +lemma approx_stk_Nil [iff]: + "approx_stk G hp [] []" +by (simp add: approx_stk_def approx_loc_def) + +lemma approx_stk_Cons [iff]: + "approx_stk G hp (x # stk) (S#ST) = + (approx_val G hp x (Ok S) \ approx_stk G hp stk ST)" +by (simp add: approx_stk_def approx_loc_def) + +lemma approx_stk_Cons_lemma [iff]: + "approx_stk G hp stk (S#ST') = + (\s stk'. stk = s#stk' \ approx_val G hp s (Ok S) \ approx_stk G hp stk' ST')" +by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def) + +lemma approx_stk_append_lemma: + "approx_stk G hp stk (S@ST') \ + (\s stk'. stk = s@stk' \ length s = length S \ length stk' = length ST' \ + approx_stk G hp s S \ approx_stk G hp stk' ST')" +by (simp add: list_all2_append2 approx_stk_def approx_loc_def) + + +(** oconf **) + +lemma correct_init_obj: + "\is_class G C; wf_prog wt G\ \ + G,h \ (C, map_of (map (\(f,fT).(f,default_val fT)) (fields(G,C)))) \" +apply (unfold oconf_def lconf_def) +apply (simp add: map_of_map) +apply (force intro: defval_conf dest: map_of_SomeD is_type_fields) +. + + +lemma oconf_imp_oconf_field_update [rulify]: + "\map_of (fields (G, oT)) FD = Some T; G,hp\v\\T; G,hp\(oT,fs)\ \ + \ G,hp\(oT, fs(FD\v))\" +by (simp add: oconf_def lconf_def) + + +lemma oconf_imp_oconf_heap_newref [rulify]: +"hp x = None \ G,hp\obj\ \ G,hp\obj'\ \ G,(hp(newref hp\obj'))\obj\" +apply (unfold oconf_def lconf_def) +apply simp +apply (fast intro: conf_hext sup_heap_newref) +. + + +lemma oconf_imp_oconf_heap_update [rulify]: + "hp a = Some obj' \ obj_ty obj' = obj_ty obj'' \ G,hp\obj\ + \ G,hp(a\obj'')\obj\" +apply (unfold oconf_def lconf_def) +apply simp +apply (force intro: approx_val_imp_approx_val_heap_update) +. + + +(** hconf **) + + +lemma hconf_imp_hconf_newref [rulify]: + "hp x = None \ G\h hp\ \ G,hp\obj\ \ G\h hp(newref hp\obj)\" +apply (simp add: hconf_def) +apply (fast intro: oconf_imp_oconf_heap_newref) +. + +lemma hconf_imp_hconf_field_update [rulify]: + "map_of (fields (G, oT)) (F, D) = Some T \ hp oloc = Some(oT,fs) \ + G,hp\v\\T \ G\h hp\ \ G\h hp(oloc \ (oT, fs((F,D)\v)))\" +apply (simp add: hconf_def) +apply (force intro: oconf_imp_oconf_heap_update oconf_imp_oconf_field_update + simp add: obj_ty_def) +. + +(** correct_frames **) + +lemmas [simp del] = fun_upd_apply + +lemma correct_frames_imp_correct_frames_field_update [rulify]: + "\rT C sig. correct_frames G hp phi rT sig frs \ + hp a = Some (C,od) \ map_of (fields (G, C)) fl = Some fd \ + G,hp\v\\fd + \ correct_frames G (hp(a \ (C, od(fl\v)))) phi rT sig frs"; +apply (induct frs) + apply simp +apply (clarsimp simp add: correct_frame_def) (*takes long*) +apply (intro exI conjI) + apply simp + apply simp + apply force + apply simp + apply (rule approx_stk_imp_approx_stk_sup_heap) + apply simp + apply (rule sup_heap_update_value) + apply simp +apply (rule approx_loc_imp_approx_loc_sup_heap) + apply simp +apply (rule sup_heap_update_value) +apply simp +. + +lemma correct_frames_imp_correct_frames_newref [rulify]: + "\rT C sig. hp x = None \ correct_frames G hp phi rT sig frs \ oconf G hp obj + \ correct_frames G (hp(newref hp \ obj)) phi rT sig frs" +apply (induct frs) + apply simp +apply (clarsimp simp add: correct_frame_def) +apply (intro exI conjI) + apply simp + apply simp + apply force + apply simp + apply (rule approx_stk_imp_approx_stk_sup_heap) + apply simp + apply (rule sup_heap_newref) + apply simp +apply (rule approx_loc_imp_approx_loc_sup_heap) + apply simp +apply (rule sup_heap_newref) +apply simp +. end + diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/LBVComplete.thy --- a/src/HOL/MicroJava/BV/LBVComplete.thy Wed Aug 30 21:44:12 2000 +0200 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy Wed Aug 30 21:47:39 2000 +0200 @@ -8,244 +8,119 @@ theory LBVComplete = BVSpec + LBVSpec + StepMono: - constdefs - is_approx :: "['a option list, 'a list] \ bool" - "is_approx a b \ length a = length b \ (\ n. n < length a \ - (a!n = None \ a!n = Some (b!n)))" - - contains_dead :: "[instr list, certificate, method_type, p_count] \ bool" - "contains_dead ins cert phi 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 \ ( - \ pc' \ succs (ins!pc) pc. pc' \ Suc pc \ pc' < length phi \ - cert!pc' = Some (phi!pc'))" - + "contains_targets ins cert phi pc \ + \pc' \ set (succs (ins!pc) pc). + pc' \ pc+1 \ pc' < length ins \ cert!pc' = phi!pc'" fits :: "[instr list, certificate, method_type] \ bool" - "fits ins cert phi \ is_approx cert phi \ length ins < length phi \ - (\ pc. pc < length ins \ - contains_dead ins cert phi pc \ - contains_targets ins cert phi pc)" + "fits ins cert phi \ \pc. pc < length ins \ + contains_targets ins cert phi pc \ + (cert!pc = None \ cert!pc = phi!pc)" is_target :: "[instr list, p_count] \ bool" - "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 \ pc \ succs (ins!pc') pc'" - - mdot :: "[instr list, p_count] \ bool" - "mdot ins pc \ maybe_dead ins pc \ is_target ins pc" + "is_target ins pc \ + \pc'. pc \ pc'+1 \ pc' < length ins \ pc \ set (succs (ins!pc') pc')" -consts - 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))" - constdefs - option_filter :: "['a list, nat \ bool] \ 'a option list" - "option_filter l P \ option_filter_n l P 0" - make_cert :: "[instr list, method_type] \ certificate" - "make_cert ins phi \ option_filter phi (mdot ins)" - + "make_cert ins phi \ + map (\pc. if is_target ins pc then phi!pc else None) [0..length ins(]" + make_Cert :: "[jvm_prog, prog_type] \ prog_certificate" "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)" + let (C,x,y,mdecls) = \ (Cl,x,y,mdecls). (Cl,x,y,mdecls) \ set G \ Cl = C; + (sig,rT,maxl,b) = \ (sg,rT,maxl,b). (sg,rT,maxl,b) \ set mdecls \ sg = sig + in make_cert b (Phi C sig)" lemmas [simp del] = split_paired_Ex -lemma length_ofn [rulify]: "\n. length (option_filter_n l P n) = length l" - by (induct l) auto - +lemma make_cert_target: + "[| pc < length ins; is_target ins pc |] ==> make_cert ins phi ! pc = phi!pc" + by (simp add: make_cert_def) -lemma is_approx_option_filter: "is_approx (option_filter l P) l" -proof - - { - fix a n - have "\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" - - 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 - - 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) - - 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 - } - - thus ?thesis - by (auto simp add: option_filter_def) -qed +lemma make_cert_approx: + "[| pc < length ins; make_cert ins phi ! pc \ phi ! pc |] ==> + make_cert ins phi ! pc = None" + by (auto simp add: make_cert_def) -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 (unfold contains_targets_def, clarsimp) +lemma make_cert_contains_targets: + "pc < length ins ==> contains_targets ins (make_cert ins phi) phi pc" +proof (unfold contains_targets_def, intro strip, elim conjE) fix pc' assume "pc < length ins" - "pc' \ succs (ins ! pc) pc" - "pc' \ Suc pc" and - pc': "pc' < length phi" + "pc' \ set (succs (ins ! pc) pc)" + "pc' \ pc+1" and + pc': "pc' < length ins" - hence "is_target ins pc'" by (auto simp add: is_target_def) + 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) + show "make_cert ins phi ! pc' = phi ! pc'" + by (auto intro: make_cert_target) 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" . +theorem fits_make_cert: + "fits ins (make_cert ins phi) phi" + by (auto dest: make_cert_approx simp add: fits_def make_cert_contains_targets) - 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) + "[| fits ins cert phi; pc' \ set (succs (ins!pc) pc); + pc' \ Suc pc; pc < length ins; pc' < length ins |] + ==> cert!pc' = phi!pc'" + by (clarsimp simp add: fits_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) - + "[| fits ins cert phi; pc < length ins; cert!pc = Some s |] + ==> cert!pc = phi!pc" + by (auto simp add: fits_def) + lemma wtl_inst_mono: -"\wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins; - G \ s2 <=s s1; i = ins!pc\ \ - \ s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \ (G \ s2' <=s s1')" + "[| wtl_inst i G rT s1 cert mpc pc = Ok s1'; fits ins cert phi; + pc < length ins; G \ s2 <=' s1; i = ins!pc |] ==> + \ s2'. wtl_inst (ins!pc) G rT s2 cert mpc pc = Ok s2' \ (G \ s2' <=' s1')" proof - assume pc: "pc < length ins" "i = ins!pc" - assume wtl: "wtl_inst i G rT s1 s1' cert mpc pc" + assume wtl: "wtl_inst i G rT s1 cert mpc pc = Ok s1'" assume fits: "fits ins cert phi" - assume G: "G \ s2 <=s s1" + assume G: "G \ s2 <=' s1" - let "?step s" = "step (i, G, s)" + let "?step s" = "step i G s" from wtl G - have app: "app (i, G, rT, s2)" by (auto simp add: wtl_inst_def app_mono) + have app: "app i G rT s2" by (auto simp add: wtl_inst_Ok 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) + have step: "succs i pc \ [] ==> G \ ?step s2 <=' ?step s1" + by - (drule step_mono, auto simp add: wtl_inst_Ok) { 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) + assume 0: "pc' \ set (succs i pc)" "pc' \ pc+1" + hence "succs i pc \ []" by auto + hence "G \ ?step s2 <=' ?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) + have "G \ ?step s1 <=' cert!pc'" + by (auto simp add: wtl_inst_Ok) finally - have "G\ the (?step s2) <=s the (cert!pc')" . + have "G\ ?step s2 <=' 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") + have "\s2'. wtl_inst i G rT s2 cert mpc pc = Ok s2' \ G \ s2' <=' s1'" + proof (cases "pc+1 \ set (succs i pc)") case True with wtl - have s1': "s1' = the (?step s1)" by (simp add: wtl_inst_def) + have s1': "s1' = ?step s1" by (simp add: wtl_inst_Ok) - have "wtl_inst i G rT s2 (the (?step s2)) cert mpc pc \ G \ (the (?step s2)) <=s s1'" + have "wtl_inst i G rT s2 cert mpc pc = Ok (?step s2) \ G \ ?step s2 <=' s1'" (is "?wtl \ ?G") proof from True s1' @@ -253,145 +128,193 @@ from True app wtl show ?wtl - by (clarsimp intro!: cert simp add: wtl_inst_def) + by (clarsimp intro!: cert simp add: wtl_inst_Ok) qed thus ?thesis by blast next case False with wtl - have "s1' = the (cert ! Suc pc)" by (simp add: wtl_inst_def) + have "s1' = cert ! Suc pc" by (simp add: wtl_inst_Ok) 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) + have "wtl_inst i G rT s2 cert mpc pc = Ok s1' \ G \ s1' <=' s1'" + by (clarsimp intro!: cert simp add: wtl_inst_Ok) thus ?thesis by blast qed with pc show ?thesis by simp qed - + -lemma wtl_option_mono: -"\wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi; - pc < length ins; G \ s2 <=s s1; i = ins!pc\ \ - \ s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \ (G \ s2' <=s s1')" +lemma wtl_cert_mono: + "[| wtl_cert i G rT s1 cert mpc pc = Ok s1'; fits ins cert phi; + pc < length ins; G \ s2 <=' s1; i = ins!pc |] ==> + \ s2'. wtl_cert (ins!pc) G rT s2 cert mpc pc = Ok s2' \ (G \ s2' <=' s1')" proof - - assume wtl: "wtl_inst_option i G rT s1 s1' cert mpc pc" and + assume wtl: "wtl_cert i G rT s1 cert mpc pc = Ok s1'" and fits: "fits ins cert phi" "pc < length ins" - "G \ s2 <=s s1" "i = ins!pc" + "G \ s2 <=' s1" "i = ins!pc" show ?thesis proof (cases (open) "cert!pc") case None with wtl fits show ?thesis - by - (rule wtl_inst_mono [elimify], (simp add: wtl_inst_option_def)+) + by - (rule wtl_inst_mono [elimify], (simp add: wtl_cert_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 <=' (Some a)" + by - (rule sup_state_opt_trans, auto simp add: wtl_cert_def split: if_splits) from Some wtl - have "wtl_inst i G rT a s1' cert mpc pc" by (simp add: wtl_inst_option_def) + have "wtl_inst i G rT (Some a) cert mpc pc = Ok s1'" + by (simp add: wtl_cert_def split: if_splits) 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)+) + have "\ s2'. wtl_inst (ins!pc) G rT (Some a) cert mpc pc = Ok s2' \ + (G \ s2' <=' s1')" + by - (rule wtl_inst_mono, (simp add: wtl_cert_def)+) with Some G - show ?thesis by (simp add: wtl_inst_option_def) + show ?thesis by (simp add: wtl_cert_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 - + "[| wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi; + pc < length ins; length ins = max_pc |] ==> + wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc \ Err" + proof - 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) + 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" + have pc': "\pc'. pc' \ set (succs (ins!pc) pc) ==> pc' < length ins" by (simp add: wt_instr_def) - 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) + let ?s' = "step (ins!pc) G (phi!pc)" 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) - - show ?thesis - 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) + have cert: "!!pc'. \pc' \ set (succs (ins!pc) pc); pc' < max_pc; pc' \ pc+1\ + \ G \ ?s' <=' cert!pc'" + by (auto dest: fitsD simp add: wt_instr_def) - from True fits app pc cert pc' - show "?wtl" - by (auto simp add: wtl_inst_def) - qed - - thus ?thesis by blast - - next - let ?s'' = "the (cert ! Suc pc)" - - 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 by blast - qed + from app pc cert pc' + show ?thesis + by (auto simp add: wtl_inst_Ok) qed - -lemma wt_instr_imp_wtl_option: -"\fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc; max_pc = length ins\ \ - \ s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \ G \ s <=s phi ! Suc pc" +lemma wt_less_wtl: + "[| wt_instr (ins!pc) G rT phi max_pc pc; + wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s; + fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==> + G \ s <=' phi ! Suc pc" proof - - assume fits : "fits ins cert phi" "pc < length ins" - and "wt_instr (ins!pc) G rT phi max_pc pc" - "max_pc = length ins" + assume wt: "wt_instr (ins!pc) G rT phi max_pc pc" + assume wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s" + assume fits: "fits ins cert phi" + assume pc: "Suc pc < length ins" "length ins = max_pc" + + { assume suc: "Suc pc \ set (succs (ins ! pc) pc)" + with wtl have "s = step (ins!pc) G (phi!pc)" + by (simp add: wtl_inst_Ok) + also from suc wt have "G \ ... <=' phi!Suc pc" + by (simp add: wt_instr_def) + finally have ?thesis . + } - hence * : "\ s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \ G \ s <=s phi ! Suc pc" - by - (rule wt_instr_imp_wtl_inst, simp+) + moreover + { assume "Suc pc \ set (succs (ins ! pc) pc)" + + with wtl + have "s = cert!Suc pc" + by (simp add: wtl_inst_Ok) + with fits pc + have ?thesis + by - (cases "cert!Suc pc", simp, drule fitsD2, assumption+, simp) + } + + ultimately + show ?thesis by blast +qed + + +lemma wt_instr_imp_wtl_cert: + "[| wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi; + pc < length ins; length ins = max_pc |] ==> + wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc \ Err" +proof - + assume "wt_instr (ins!pc) G rT phi max_pc pc" and + fits: "fits ins cert phi" and + pc: "pc < length ins" and + "length ins = max_pc" - show ?thesis - proof (cases "cert ! pc") - case None - with * - show ?thesis by (simp add: wtl_inst_option_def) + hence wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc \ Err" + by (rule wt_instr_imp_wtl_inst) + + hence "cert!pc = None ==> ?thesis" + by (simp add: wtl_cert_def) - next - case Some + moreover + { fix s + assume c: "cert!pc = Some s" + with fits pc + have "cert!pc = phi!pc" + by (rule fitsD2) + from this c wtl + have ?thesis + by (clarsimp simp add: wtl_cert_def) + } + + ultimately + show ?thesis by blast +qed + - from fits - 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 +lemma wt_less_wtl_cert: + "[| wt_instr (ins!pc) G rT phi max_pc pc; + wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s; + fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==> + G \ s <=' phi ! Suc pc" +proof - + assume wtl: "wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s" + + assume wti: "wt_instr (ins!pc) G rT phi max_pc pc" + "fits ins cert phi" + "Suc pc < length ins" "length ins = max_pc" + + { assume "cert!pc = None" + with wtl + have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s" + by (simp add: wtl_cert_def) + with wti + have ?thesis + by - (rule wt_less_wtl) + } + moreover + { fix t + assume c: "cert!pc = Some t" + with wti + have "cert!pc = phi!pc" + by - (rule fitsD2, simp+) + with c wtl + have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s" + by (simp add: wtl_cert_def) + with wti + have ?thesis + by - (rule wt_less_wtl) + } + + ultimately + show ?thesis by blast qed @@ -401,13 +324,15 @@ *} theorem wt_imp_wtl_inst_list: -"\ pc. (\pc'. pc' < length all_ins \ wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \ +"\ pc. (\pc'. pc' < length all_ins \ + wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \ fits all_ins cert phi \ (\l. pc = length l \ all_ins = l@ins) \ pc < length all_ins \ - (\ s. (G \ s <=s (phi!pc)) \ - (\s'. wtl_inst_list ins G rT s s' cert (length all_ins) pc))" -(is "\pc. ?wt \ ?fits \ ?l pc ins \ ?len pc \ ?wtl pc ins" is "\pc. ?C pc ins" is "?P ins") + (\ s. (G \ s <=' (phi!pc)) \ + wtl_inst_list ins G rT cert (length all_ins) pc s \ Err)" +(is "\pc. ?wt \ ?fits \ ?l pc ins \ ?len pc \ ?wtl pc ins" + is "\pc. ?C pc ins" is "?P ins") proof (induct "?P" "ins") case Nil show "?P []" by simp @@ -421,53 +346,56 @@ assume wt : "\pc'. pc' < length all_ins \ wt_instr (all_ins ! pc') G rT phi (length all_ins) pc'" assume fits: "fits all_ins cert phi" - assume G : "G \ s <=s phi ! pc" assume l : "pc < length all_ins" - + assume G : "G \ s <=' phi ! pc" assume pc : "all_ins = l@i#ins'" "pc = length l" hence i : "all_ins ! pc = i" by (simp add: nth_append) from l wt - have "wt_instr (all_ins!pc) G rT phi (length all_ins) pc" by blast + have wti: "wt_instr (all_ins!pc) G rT phi (length all_ins) pc" by blast with fits l - obtain s1 where - "wtl_inst_option (all_ins!pc) G rT (phi!pc) s1 cert (length all_ins) pc" and - s1: "G \ s1 <=s phi ! (Suc pc)" - by - (drule wt_instr_imp_wtl_option, assumption+, simp, elim exE conjE, simp) + have c: "wtl_cert (all_ins!pc) G rT (phi!pc) cert (length all_ins) pc \ Err" + by - (drule wt_instr_imp_wtl_cert, auto) - with fits l - obtain s2 where - o: "wtl_inst_option (all_ins!pc) G rT s s2 cert (length all_ins) pc" - and "G \ s2 <=s s1" - by - (drule wtl_option_mono, assumption+, simp, elim exE conjE, rule that) - - with s1 - have G': "G \ s2 <=s phi ! (Suc pc)" - by - (rule sup_state_trans, auto) - from Cons have "?C (Suc pc) ins'" by blast with wt fits pc have IH: "?len (Suc pc) \ ?wtl (Suc pc) ins'" by auto - show "\s'. wtl_inst_list (i#ins') G rT s s' cert (length all_ins) pc" + show "wtl_inst_list (i#ins') G rT cert (length all_ins) pc s \ Err" proof (cases "?len (Suc pc)") case False with pc have "ins' = []" by simp - with i o - show ?thesis by auto + with G i c fits l + show ?thesis by (auto dest: wtl_cert_mono) next case True with IH - have "?wtl (Suc pc) ins'" by blast - with G' + have wtl: "?wtl (Suc pc) ins'" by blast + + from c wti fits l True + obtain s'' where + "wtl_cert (all_ins!pc) G rT (phi!pc) cert (length all_ins) pc = Ok s''" + "G \ s'' <=' phi ! Suc pc" + by clarsimp (drule wt_less_wtl_cert, auto) + moreover + from calculation fits G l obtain s' where - "wtl_inst_list ins' G rT s2 s' cert (length all_ins) (Suc pc)" - by - (elim allE impE, auto) - with i o + c': "wtl_cert (all_ins!pc) G rT s cert (length all_ins) pc = Ok s'" and + "G \ s' <=' s''" + by - (drule wtl_cert_mono, auto) + ultimately + have G': "G \ s' <=' phi ! Suc pc" + by - (rule sup_state_opt_trans) + + with wtl + have "wtl_inst_list ins' G rT cert (length all_ins) (Suc pc) s' \ Err" + by auto + + with i c' show ?thesis by auto qed qed @@ -475,38 +403,42 @@ lemma fits_imp_wtl_method_complete: -"\wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\ - \ wtl_method G C pTs rT mxl ins cert" + "[| wt_method G C pTs rT mxl ins phi; fits ins cert phi |] ==> + wtl_method G C pTs rT mxl ins cert" by (simp add: wt_method_def wtl_method_def) (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def) lemma wtl_method_complete: -"\wt_method G C pTs rT mxl ins phi; wf_prog wf_mb G\ - \ wtl_method G C pTs rT mxl ins (make_cert ins phi)" + "wt_method G C pTs rT mxl ins phi ==> + wtl_method G C pTs rT mxl ins (make_cert ins phi)" proof - - assume * : "wt_method G C pTs rT mxl ins phi" "wf_prog wf_mb G" - - hence "fits ins (make_cert ins phi) phi" - by - (rule fits_make_cert, simp add: wt_method_def) - - with * - show ?thesis by - (rule fits_imp_wtl_method_complete) + assume "wt_method G C pTs rT mxl ins phi" + moreover + have "fits ins (make_cert ins phi) phi" + by (rule fits_make_cert) + ultimately + show ?thesis + by (rule fits_imp_wtl_method_complete) 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'" +"(a,b,c,d)\set l \ unique l \ (a',b',c',d') \ set l \ + a = a' \ b=b' \ c=c' \ d=d'" by (induct "l") auto lemma unique_epsilon: -"(a,b,c,d)\set l \ unique l \ (\ (a',b',c',d'). (a',b',c',d') \ set l \ a'=a) = (a,b,c,d)" + "(a,b,c,d)\set l \ unique l \ + (\ (a',b',c',d'). (a',b',c',d') \ set l \ a'=a) = (a,b,c,d)" by (auto simp add: unique_set) -theorem wtl_complete: "\wt_jvm_prog G Phi\ \ wtl_jvm_prog G (make_Cert G Phi)" +theorem wtl_complete: + "wt_jvm_prog G Phi ==> wtl_jvm_prog G (make_Cert G Phi)" proof (simp only: wt_jvm_prog_def) - assume wfprog: "wf_prog (\G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G" + assume wfprog: + "wf_prog (\G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G" thus ?thesis proof (simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def wf_mdecl_def, auto) @@ -514,13 +446,15 @@ assume 1 : "\(C,sc,fs,ms)\set G. Ball (set fs) (wf_fdecl G) \ unique fs \ - (\(sig,rT,mb)\set ms. wf_mhead G sig rT \ (\(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \ + (\(sig,rT,mb)\set ms. wf_mhead G sig rT \ + (\(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \ unique ms \ (case sc of None \ C = Object | Some D \ is_class G D \ (D, C) \ (subcls1 G)^* \ - (\(sig,rT,b)\set ms. \D' rT' b'. method (G, D) sig = Some (D', rT', b') \ G\rT\rT'))" + (\(sig,rT,b)\set ms. + \D' rT' b'. method (G, D) sig = Some (D', rT', b') \ G\rT\rT'))" "(a, aa, ab, b) \ set G" assume uG : "unique G" @@ -530,14 +464,16 @@ show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))" 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" + 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) assume "wt_method G a ba ad ae bb (Phi a (ac, ba))" with wfprog uG ub b 1 show ?thesis - by - (rule wtl_method_complete [elimify], assumption+, simp add: make_Cert_def unique_epsilon) + by - (rule wtl_method_complete [elimify], assumption+, + simp add: make_Cert_def unique_epsilon) qed qed qed diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/LBVCorrect.thy --- a/src/HOL/MicroJava/BV/LBVCorrect.thy Wed Aug 30 21:44:12 2000 +0200 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Wed Aug 30 21:47:39 2000 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/MicroJava/BV/BVLcorrect.thy +(* Title: HOL/MicroJava/BV/BVLCorrect.thy ID: $Id$ Author: Gerwin Klein Copyright 1999 Technische Universitaet Muenchen @@ -8,407 +8,285 @@ theory LBVCorrect = BVSpec + LBVSpec: +lemmas [simp del] = split_paired_Ex split_paired_All + constdefs -fits_partial :: "[method_type,nat,instr list,jvm_prog,ty,state_type,state_type,certificate] \ bool" -"fits_partial phi pc is G rT s0 s2 cert \ (\ a b i s1. (a@(i#b) = is) \ - wtl_inst_list a G rT s0 s1 cert (pc+length is) pc \ - wtl_inst_list (i#b) G rT s1 s2 cert (pc+length is) (pc+length a) \ - ((cert!(pc+length a) = None \ phi!(pc+length a) = s1) \ - (\ 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 :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] \ bool" +"fits phi is G rT s0 cert \ + (\pc s1. pc < length is \ + (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1 \ + (case cert!pc of None \ phi!pc = s1 + | Some t \ phi!pc = Some t)))" + +constdefs +make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] \ method_type" +"make_phi is G rT s0 cert \ + map (\pc. case cert!pc of + None \ val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0) + | Some t \ Some t) [0..length is(]" + -lemma fitsD: -"fits phi is G rT s0 s2 cert \ - (a@(i#b) = is) \ - 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 +lemma fitsD_None: + "\fits phi is G rT s0 cert; pc < length is; + wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; + cert ! pc = None\ \ phi!pc = s1" + by (auto simp add: fits_def) -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 fitsD_Some: + "\fits phi is G rT s0 cert; pc < length is; + wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; + cert ! pc = Some t\ \ phi!pc = Some t" + by (auto simp add: fits_def) + +lemma make_phi_Some: + "[| pc < length is; cert!pc = Some t |] ==> + make_phi is G rT s0 cert ! pc = Some t" + by (simp add: make_phi_def) + +lemma make_phi_None: + "[| pc < length is; cert!pc = None |] ==> + make_phi is G rT s0 cert ! pc = + val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)" + by (simp add: make_phi_def) 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" - 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 (open) ?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)" + "\phi. fits phi is G rT s0 cert" +proof - + have "fits (make_phi is G rT s0 cert) is G rT s0 cert" + by (auto simp add: fits_def make_phi_Some make_phi_None + split: option.splits) - 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 - - + thus ?thesis + by blast +qed + lemma fits_lemma1: -"\wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\ \ - \ pc t. pc < length is \ (cert ! pc) = Some t \ (phi ! pc) = t" -proof intro - fix pc t - assume wtl: "wtl_inst_list is G rT s0 s3 cert (length is) 0" - assume fits: "fits phi is G rT s0 s3 cert" - assume pc: "pc < length is" - assume cert: "cert ! pc = Some t" - from pc - have "is \ []" by auto - hence cons: "\i y. is = i#y" by (simp add: neq_Nil_conv) - from wtl pc - have "\a b s1. a@b = is \ length a = pc \ - wtl_inst_list a G rT s0 s1 cert (length is) 0 \ - wtl_inst_list b G rT s1 s3 cert (length is) (0+length a)" - (is "\a b s1. ?A a b \ ?L a \ ?W1 a s1 \ ?W2 a b s1") - by (rule wtl_partial [rulify]) - with cons - show "phi ! pc = t" - proof (elim exE conjE) - fix a b s1 i y - assume * :"?A a b" "?L a" "?W1 a s1" "?W2 a b s1" "is = i#y" - with pc - have "b \ []" by auto - hence "\b' bs. b = b'#bs" by (simp add: neq_Nil_conv) - thus ?thesis - proof (elim exE) - fix b' bs assume Cons: "b=b'#bs" - with * fits cert - show ?thesis - proof (unfold fits_def fits_partial_def, elim allE impE) - from * Cons show "a@b'#bs=is" by simp - qed simp+ - qed - qed + "[| wtl_inst_list is G rT cert (length is) 0 s = Ok s'; fits phi is G rT s cert |] + ==> \pc t. pc < length is \ cert!pc = Some t \ phi!pc = Some t" +proof (intro strip) + fix pc t + assume "wtl_inst_list is G rT cert (length is) 0 s = Ok s'" + then + obtain s'' where + "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s''" + by (blast dest: wtl_take) + moreover + assume "fits phi is G rT s cert" + "pc < length is" + "cert ! pc = Some t" + ultimately + show "phi!pc = Some t" by (auto dest: fitsD_Some) qed -lemma fits_lemma2: -"\wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; - wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a); - fits phi (a@i#b) G rT s0 s3 cert; cert!(length a) = None; - wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\ - \ phi!(length a) = s1" -proof (unfold fits_def fits_partial_def, elim allE impE) -qed (auto simp del: split_paired_Ex) - - lemma wtl_suc_pc: -"\wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; - wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a); - wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a)); - fits phi (a@i#b) G rT s0 s3 cert \ \ - b \ [] \ G \ s2 <=s (phi ! (Suc (length a)))" -proof - assume f: "fits phi (a@i#b) G rT s0 s3 cert" - assume "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0" - "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 \ []" + "[| wtl_inst_list is G rT cert (length is) 0 s \ Err; + wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'; + wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''; + fits phi is G rT s cert; Suc pc < length is |] ==> + G \ s'' <=' phi ! Suc pc" +proof - + + assume all: "wtl_inst_list is G rT cert (length is) 0 s \ Err" + assume fits: "fits phi is G rT s cert" + + assume wtl: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" and + wtc: "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''" and + pc: "Suc pc < length is" + + hence wts: "wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = Ok s''" + by (rule wtl_Suc) + + from all + have app: + "wtl_inst_list (take (Suc pc) is@drop (Suc pc) is) G rT cert (length is) 0 s \ Err" + by simp - 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 + from pc + have "0 < length (drop (Suc pc) is)" + by simp + then + obtain l ls where + "drop (Suc pc) is = l#ls" + by (auto simp add: neq_Nil_conv simp del: length_drop) + with app wts pc + obtain x where + "wtl_cert l G rT s'' cert (length is) (Suc pc) = Ok x" + by (auto simp add: wtl_append min_def simp del: append_take_drop_id) -lemma wtl_lemma: -"\wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0; - 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)); - fits phi (i1@i#i2) G rT s0 s3 cert\ \ - wt_instr i G rT phi (length (i1@i#i2)) (length i1)" (concl is "?P i") -proof - - assume w1: "wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0" (is ?w1) - assume wo: "wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1)" - assume w2: "wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1))" - assume f: "fits phi (i1@i#i2) G rT s0 s3 cert" - - from w1 wo w2 - have wtl: "wtl_inst_list (i1@i#i2) G rT s0 s3 cert (length (i1@i#i2)) 0" - by (rule wtl_cons_appendl) + hence c1: "\t. cert!Suc pc = Some t ==> G \ s'' <=' cert!Suc pc" + by (simp add: wtl_cert_def split: if_splits) + moreover + from fits pc wts + have c2: "\t. cert!Suc pc = Some t ==> phi!Suc pc = cert!Suc pc" + by - (drule fitsD_Some, auto) + moreover + from fits pc wts + have c3: "cert!Suc pc = None ==> phi!Suc pc = s''" + by (rule fitsD_None) + ultimately - with f - have c1: "\t. cert ! (length i1) = Some t \ phi ! (length i1) = t" - by intro (rule fits_lemma1 [rulify], auto) - - from w1 wo w2 f - have c2: "cert ! (length i1) = None \ phi ! (length i1) = s1" - by - (rule fits_lemma2) - - from wtl f - have c3: "\pc t. pc < length(i1@i#i2) \ cert ! pc = Some t \ phi ! pc = t" - by (rule fits_lemma1) - - from w1 wo w2 f - have suc: "i2 \ [] \ G \ s2 <=s phi ! Suc (length i1)" - by (rule wtl_suc_pc [rulify]) - - with wo - show ?thesis - by (auto simp add: c1 c2 c3 wt_instr_def wtl_inst_def wtl_inst_option_def split: option.split_asm) + show ?thesis + by - (cases "cert ! Suc pc", auto) qed lemma wtl_fits_wt: -"\wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\ - \ \pc. pc < length is \ wt_instr (is ! pc) G rT phi (length is) pc" -proof intro - assume fits: "fits phi is G rT s0 s3 cert" + "[| wtl_inst_list is G rT cert (length is) 0 s \ Err; + fits phi is G rT s cert; pc < length is |] ==> + wt_instr (is!pc) G rT phi (length is) pc" +proof - + + assume fits: "fits phi is G rT s cert" - fix pc - assume wtl: "wtl_inst_list is G rT s0 s3 cert (length is) 0" - and pc: "pc < length is" + assume pc: "pc < length is" and + wtl: "wtl_inst_list is G rT cert (length is) 0 s \ Err" + + then + obtain s' s'' where + w: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" and + c: "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''" + by - (drule wtl_all, auto) + + from fits wtl pc + have cert_Some: + "\t pc. [| pc < length is; cert!pc = Some t |] ==> phi!pc = Some t" + by (auto dest: fits_lemma1) - 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) + from fits wtl pc + have cert_None: "cert!pc = None ==> phi!pc = s'" + by - (drule fitsD_None) + + from pc c cert_None cert_Some + have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert (length is) pc = Ok s''" + by (auto simp add: wtl_cert_def split: if_splits option.splits) + + { fix pc' + assume pc': "pc' \ set (succs (is!pc) pc)" - from l pc - have "i2' \ []" by auto + with wti + have less: "pc' < length is" + by (simp add: wtl_inst_Ok) - from this - obtain i i2 where c: "i2' = i#i2" - by (simp add: neq_Nil_conv) (elim, rule that) + have "G \ step (is!pc) G (phi!pc) <=' phi ! pc'" + proof (cases "pc' = Suc pc") + case False + with wti pc' + have G: "G \ step (is ! pc) G (phi ! pc) <=' cert ! pc'" + by (simp add: wtl_inst_Ok) - 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 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) + hence "cert!pc' = None ==> step (is ! pc) G (phi ! pc) = None" + by simp + hence "cert!pc' = None ==> ?thesis" + by simp + + moreover + { fix t + assume "cert!pc' = Some t" + with less + have "phi!pc' = cert!pc'" + by (simp add: cert_Some) + with G + have ?thesis + by simp + } - with l c - show "wt_instr (is ! pc) G rT phi (length is) pc" - by (auto simp add: nth_append) + ultimately + show ?thesis by blast + next + case True + with pc' wti + have "step (is ! pc) G (phi ! pc) = s''" + by (simp add: wtl_inst_Ok) + also + from w c fits pc wtl + have "Suc pc < length is ==> G \ s'' <=' phi ! Suc pc" + by - (drule wtl_suc_pc) + with True less + have "G \ s'' <=' phi ! Suc pc" + by blast + finally + show ?thesis + by (simp add: True) + qed + } + + with wti + show ?thesis + by (auto simp add: wtl_inst_Ok wt_instr_def) 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" - 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; - fits phi is G rT s0 s2 cert\ \ G \ s0 <=s phi ! 0" + "[| 0 < length is; wtl_inst_list is G rT cert (length is) 0 s \ Err; + fits phi is G rT s cert |] ==> + G \ s <=' phi ! 0" 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 \ []" + assume wtl: "wtl_inst_list is G rT cert (length is) 0 s \ Err" + assume fits: "fits phi is G rT s cert" + assume pc: "0 < length is" + + from wtl + have wt0: "wtl_inst_list (take 0 is) G rT cert (length is) 0 s = Ok s" + by simp - from this - obtain y ys where cons: "is = y#ys" + with fits pc + have "cert!0 = None ==> phi!0 = s" + by (rule fitsD_None) + moreover + from fits pc wt0 + have "\t. cert!0 = Some t ==> phi!0 = cert!0" + by - (drule fitsD_Some, auto) + moreover + from pc + obtain x xs where "is = x#xs" by (simp add: neq_Nil_conv) (elim, rule that) + with wtl + obtain s' where + "wtl_cert x G rT s cert (length is) 0 = Ok s'" + by simp (elim, rule that, simp) + hence + "\t. cert!0 = Some t ==> G \ s <=' cert!0" + by (simp add: wtl_cert_def split: if_splits) - from fits + ultimately 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 cert: - "(cert ! (0 + length []) = None \ phi ! (0 + length []) = s0) \ - (\t. cert ! (0 + length []) = Some t \ phi ! (0 + length []) = t)" + by - (cases "cert!0", auto) +qed - 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" +"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 only: Let_def, elim conjE) + let "?s0" = "Some ([], Ok (Class C) # map Ok pTs @ replicate mxl Err)" + assume pc: "0 < length ins" + assume wtl: "wtl_inst_list ins G rT cert (length ins) 0 ?s0 \ Err" - from this - obtain phi where fits: "fits phi ins G rT ?s0 s2 cert \ length ins < length phi" + obtain phi where fits: "fits phi ins G rT ?s0 cert" 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]) + by (blast intro: wtl_fits_wt) - from neqNil wtl fits + from pc wtl fits have "wt_start G C pTs mxl phi" - by (elim conjE, unfold wt_start_def) (rule fits_first) + by (unfold wt_start_def) (rule fits_first) - with neqNil allpc fits + with pc allpc 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'" + "(a,b,c,d)\set l \ unique l \ (a',b',c',d') \ set l \ + a = a' \ b=b' \ c=c' \ d=d'" by (induct "l") auto lemma unique_epsilon: -"(a,b,c,d)\set l \ unique l \ (\ (a',b',c',d'). (a',b',c',d') \ set l \ a'=a) = (a,b,c,d)" + "(a,b,c,d)\set l \ unique l \ + (\ (a',b',c',d'). (a',b',c',d') \ set l \ a'=a) = (a,b,c,d)" by (auto simp add: unique_set) theorem wtl_correct: @@ -421,21 +299,24 @@ from wtl_prog show uniqueG: "unique G" by (simp add: wtl_jvm_prog_def wf_prog_def) - show "\Phi. Ball (set G) (wf_cdecl (\G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G)" + show "\Phi. Ball (set G) (wf_cdecl (\G C (sig,rT,maxl,b). + wt_method G C (snd sig) rT maxl b (Phi C sig)) G)" (is "\Phi. ?Q Phi") proof (intro exI) - let "?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\ - \ phi. wt_method G C (snd sig) rT maxl b phi" + let "?Phi" = "\ C sig. + let (C,x,y,mdecls) = \ (Cl,x,y,mdecls). (Cl,x,y,mdecls) \ set G \ Cl = C; + (sig,rT,maxl,b) = \ (sg,rT,maxl,b). (sg,rT,maxl,b) \ set mdecls \ sg = sig + in \ phi. wt_method G C (snd sig) rT maxl b phi" from wtl_prog show "?Q ?Phi" proof (unfold wf_cdecl_def, intro) fix x a b aa ba ab bb m assume 1: "x \ set G" "x = (a, b)" "b = (aa, ba)" "ba = (ab, bb)" "m \ set bb" with wtl_prog - show "wf_mdecl (\G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (?Phi C sig)) G a m" - proof (simp add: wf_mdecl_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def, elim conjE) + show "wf_mdecl (\G C (sig,rT,maxl,b). + wt_method G C (snd sig) rT maxl b (?Phi C sig)) G a m" + proof (simp add: wf_mdecl_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def, + elim conjE) apply_end (drule bspec, assumption, simp, elim conjE) assume "\(sig,rT,mb)\set bb. wf_mhead G sig rT \ (\(maxl,b). wtl_method G a (snd sig) rT maxl b (cert a sig)) mb" @@ -451,7 +332,7 @@ (\(Cl,x,y,mdecls). (Cl, x, y, mdecls) \ set G \ Cl = a))) mb) m" by - (drule bspec, assumption, clarsimp dest!: wtl_method_correct, - clarsimp intro!: selectI simp add: unique_epsilon) + 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 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/LBVSpec.thy --- a/src/HOL/MicroJava/BV/LBVSpec.thy Wed Aug 30 21:44:12 2000 +0200 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy Wed Aug 30 21:47:39 2000 +0200 @@ -1,10 +1,10 @@ -(* Title: HOL/MicroJava/BV/BVLightSpec.thy +(* Title: HOL/MicroJava/BV/LBVSpec.thy ID: $Id$ Author: Gerwin Klein Copyright 1999 Technische Universitaet Muenchen *) -header {* Specification of the LBV *} +header {* The Lightweight Bytecode Verifier *} theory LBVSpec = Step : @@ -14,256 +14,181 @@ class_certificate = "sig \ certificate" prog_certificate = "cname \ class_certificate" + constdefs -wtl_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \ bool" + check_cert :: "[instr, jvm_prog, state_type option, certificate, p_count, p_count] + \ bool" + "check_cert i G s cert pc max_pc \ \pc' \ set (succs i pc). pc' < max_pc \ + (pc' \ pc+1 \ G \ step i G s <=' cert!pc')" -"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 :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count] + \ state_type option err" + "wtl_inst i G rT s cert max_pc pc \ + if app i G rT s \ check_cert i G s cert pc max_pc then + if pc+1 mem (succs i pc) then Ok (step i G s) else Ok (cert!(pc+1)) + else Err"; -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) - -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) +lemma wtl_inst_Ok: +"(wtl_inst i G rT s cert max_pc pc = Ok s') = + (app i G rT s \ (\pc' \ set (succs i pc). + pc' < max_pc \ (pc' \ pc+1 \ G \ step i G s <=' cert!pc')) \ + (if pc+1 \ set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))" + by (auto simp add: wtl_inst_def check_cert_def set_mem_eq); constdefs -wtl_inst_option :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \ bool" -"wtl_inst_option i G rT s0 s1 cert max_pc pc \ - (case cert!pc of - None \ wtl_inst i G rT s0 s1 cert max_pc pc - | Some s0' \ (G \ s0 <=s s0') \ - wtl_inst i G rT s0' s1 cert max_pc pc)" - -consts - wtl_inst_list :: "[instr list,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \ bool" + wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count] + \ state_type option err" + "wtl_cert i G rT s cert max_pc pc \ + case cert!pc of + None \ wtl_inst i G rT s cert max_pc pc + | Some s' \ if G \ s <=' (Some s') then + wtl_inst i G rT (Some s') cert max_pc pc + else Err" + +consts + wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,p_count,p_count, + state_type option] \ state_type option err" primrec - "wtl_inst_list [] G rT s0 s2 cert max_pc pc = (s0 = s2)" - - "wtl_inst_list (instr#is) G rT s0 s2 cert max_pc pc = - (\s1. wtl_inst_option instr G rT s0 s1 cert max_pc pc \ - wtl_inst_list is G rT s1 s2 cert max_pc (pc+1))" + "wtl_inst_list [] G rT cert max_pc pc s = Ok s" + "wtl_inst_list (i#is) G rT cert max_pc pc s = + (let s' = wtl_cert i G rT s cert max_pc pc in + strict (wtl_inst_list is G rT cert max_pc (pc+1)) s')"; + constdefs - wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \ bool" - "wtl_method G C pTs rT mxl ins cert \ - let max_pc = length ins - in - 0 < max_pc \ - (\s2. wtl_inst_list ins G rT - ([],(Some(Class C))#((map Some pTs))@(replicate mxl None)) - s2 cert max_pc 0)" + wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \ bool" + "wtl_method G C pTs rT mxl ins cert \ + let max_pc = length ins + in + 0 < max_pc \ + wtl_inst_list ins G rT cert max_pc 0 + (Some ([],(Ok (Class C))#((map Ok pTs))@(replicate mxl Err))) \ Err" - wtl_jvm_prog :: "[jvm_prog,prog_certificate] \ bool" - "wtl_jvm_prog G cert \ - wf_prog (\G C (sig,rT,maxl,b). - wtl_method G C (snd sig) rT maxl b (cert C sig)) G" - -text {* \medskip *} - -lemma rev_eq: "\length a = n; length x = n; rev a @ b # c = rev x @ y # z\ \ a = x \ b = y \ c = z" -by auto - -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") -by (unfold wtl_inst_def, auto) + wtl_jvm_prog :: "[jvm_prog,prog_certificate] \ bool" + "wtl_jvm_prog G cert \ + wf_prog (\G C (sig,rT,maxl,b). wtl_method G C (snd sig) rT maxl b (cert C sig)) G" -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) +text {* \medskip *} -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") -proof (induct (open) ?P "is") - case Nil - show "?P []" by simp +lemma strict_Some [simp]: +"(strict f x = Ok y) = (\ z. x = Ok z \ f z = Ok y)" + by (cases x, auto) - case Cons - show "?P (a # list)" - proof intro - fix s0 fix pc - let "?o s0 s1" = "wtl_inst_option a G rT s0 s1 cert max_pc pc" - let "?l l s1 s2 pc" = "wtl_inst_list l G rT s1 s2 cert max_pc pc" - assume a: "?l (a#list) s0 s1 pc" - assume b: "?l (a#list) s0 s1' pc" - with a - 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 +lemma wtl_Cons: + "wtl_inst_list (i#is) G rT cert max_pc pc s \ Err = + (\s'. wtl_cert i G rT s cert max_pc pc = Ok s' \ + wtl_inst_list is G rT cert max_pc (pc+1) s' \ Err)" +by (auto simp del: split_paired_Ex) - have "s=s'" by(rule wtl_inst_option_unique) - with l l' Cons - show "s1 = s1'" by blast - qed -qed - -lemma wtl_partial: -"\ pc' pc s. - wtl_inst_list is G rT s s' cert mpc pc \ \ - pc' < length is \ \ - (\ a b s1. a @ b = is \ length a = pc' \ \ - wtl_inst_list a G rT s s1 cert mpc pc \ \ - wtl_inst_list b G rT s1 s' cert mpc (pc+length a))" (is "?P is") -proof (induct (open) ?P "is") - case Nil - show "?P []" by auto +lemma wtl_append: +"\ s pc. (wtl_inst_list (a@b) G rT cert mpc pc s = Ok s') = + (\s''. wtl_inst_list a G rT cert mpc pc s = Ok s'' \ + wtl_inst_list b G rT cert mpc (pc+length a) s'' = Ok s')" + (is "\ s pc. ?C s pc a" is "?P a") +proof (induct ?P a) + + show "?P []" by simp - case Cons - show "?P (a#list)" - proof (intro allI impI) - fix pc' pc s - assume length: "pc' < length (a # list)" - assume wtl: "wtl_inst_list (a # list) G rT s s' cert mpc pc" - show "\ a' b s1. - a' @ b = a#list \ length a' = pc' \ \ - wtl_inst_list a' G rT s s1 cert mpc pc \ \ - wtl_inst_list b G rT s1 s' cert mpc (pc+length a')" - (is "\ a b s1. ?E a b s1") - proof (cases (open) pc') - case 0 - with wtl - have "?E [] (a#list) s" by simp - thus ?thesis by blast + fix x xs + assume IH: "?P xs" + + show "?P (x#xs)" + proof (intro allI) + fix s pc + + show "?C s pc (x#xs)" + proof (cases "wtl_cert x G rT s cert mpc pc") + case Err thus ?thesis by simp next - case Suc - 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 + fix s0 + assume Ok: "wtl_cert x G rT s cert mpc pc = Ok s0" + + with IH + have "?C s0 (Suc pc) xs" by blast + + with Ok + show ?thesis by simp qed qed qed -lemma "wtl_append1": -"\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)\ \ - wtl_inst_list (x@y) G rT s0 s2 cert (length (x@y)) 0" +lemma wtl_take: + "wtl_inst_list is G rT cert mpc pc s = Ok s'' ==> + \s'. wtl_inst_list (take pc' is) G rT cert mpc pc s = Ok s'" proof - - assume w: - "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)" + assume "wtl_inst_list is G rT cert mpc pc s = Ok s''" + + hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mpc pc s = Ok s''" + by simp + + thus ?thesis + by (auto simp add: wtl_append simp del: append_take_drop_id) +qed - 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 (open) ?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 - 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 "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 +lemma take_Suc: + "\n. n < length l \ take (Suc n) l = (take n l)@[l!n]" (is "?P l") +proof (induct l) + show "?P []" by simp + + fix x xs + assume IH: "?P xs" + + show "?P (x#xs)" + proof (intro strip) + fix n + assume "n < length (x#xs)" + with IH + show "take (Suc n) (x # xs) = take n (x # xs) @ [(x # xs) ! n]" + by - (cases n, auto) qed - - with w - show ?thesis - proof (elim allE impE) - from w show "wtl_inst_list x G rT s0 s1 cert (0+length (x @ y)) 0" by simp - qed simp+ qed -lemma wtl_cons_appendl: -"\wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; - wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a); - wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\ \ - wtl_inst_list (a@i#b) G rT s0 s3 cert (length (a@i#b)) 0" +lemma wtl_Suc: + "[| wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'; + wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''; + Suc pc < length is |] ==> + wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = Ok s''" proof - - assume a: "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0" + assume wtt: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" + assume wtc: "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''" + assume pc: "Suc pc < length is" - assume "wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)" - "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))" + hence "take (Suc pc) is = (take pc is)@[is!pc]" + by (simp add: take_Suc) - hence "wtl_inst_list (i#b) G rT s1 s3 cert (length (a@i#b)) (length a)" - by (auto simp del: split_paired_Ex) - - with a - show ?thesis by (rule wtl_append1) + with wtt wtc pc + show ?thesis + by (simp add: wtl_append min_def) qed -lemma "wtl_append": -"\wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; - wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a); - wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\ \ - wtl_inst_list (a@[i]) G rT s0 s2 cert (length (a@i#b)) 0" +lemma wtl_all: + "[| wtl_inst_list is G rT cert (length is) 0 s \ Err; + pc < length is |] ==> + \s' s''. wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s' \ + wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''" proof - - assume a: "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0" - assume i: "wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)" - assume b: "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))" + assume all: "wtl_inst_list is G rT cert (length is) 0 s \ Err" - have "\ s0 pc. wtl_inst_list a G rT s0 s1 cert (pc+length (a@i#b)) pc \ - wtl_inst_option i G rT s1 s2 cert (pc+length (a@i#b)) (pc + length a) \ - wtl_inst_list b G rT s2 s3 cert (pc+length (a@i#b)) (Suc pc + length a) \ - wtl_inst_list (a@[i]) G rT s0 s2 cert (pc+length (a@i#b)) pc" (is "?P a") - proof (induct (open) ?P a) - case Nil - show "?P []" by (simp del: split_paired_Ex) - case Cons - show "?P (a#list)" (is "\s0 pc. ?x s0 pc \ ?y s0 pc \ ?z s0 pc \ ?p s0 pc") - proof intro - fix s0 pc - assume y: "?y s0 pc" - assume z: "?z s0 pc" - assume "?x s0 pc" - 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 - show ?thesis - proof (elim allE impE) - from a show "wtl_inst_list a G rT s0 s1 cert (0+length (a@i#b)) 0" by simp - qed auto + assume pc: "pc < length is" + hence "0 < length (drop pc is)" by simp + then + obtain i r where + Cons: "drop pc is = i#r" + by (auto simp add: neq_Nil_conv simp del: length_drop) + hence "i#r = drop pc is" .. + with all + have take: "wtl_inst_list (take pc is@i#r) G rT cert (length is) 0 s \ Err" + by simp + + from pc + have "is!pc = drop pc is ! 0" by simp + with Cons + have "is!pc = i" by simp + + with take pc + show ?thesis + by (auto simp add: wtl_append min_def) qed end diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/Step.thy --- a/src/HOL/MicroJava/BV/Step.thy Wed Aug 30 21:44:12 2000 +0200 +++ b/src/HOL/MicroJava/BV/Step.thy Wed Aug 30 21:47:39 2000 +0200 @@ -7,107 +7,114 @@ header {* Effect of instructions on the state type *} -theory Step = Convert : +theory Step = Convert: text "Effect of instruction on the state type:" consts -step :: "instr \ jvm_prog \ state_type \ state_type option" +step' :: "instr \ jvm_prog \ state_type \ state_type" -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))" +recdef step' "{}" +"step' (Load idx, G, (ST, LT)) = (val (LT ! idx) # ST, LT)" +"step' (Store idx, G, (ts#ST, LT)) = (ST, LT[idx:= Ok ts])" +"step' (Bipush i, G, (ST, LT)) = (PrimT Integer # ST, LT)" +"step' (Aconst_null, G, (ST, LT)) = (NT#ST,LT)" +"step' (Getfield F C, G, (oT#ST, LT)) = (snd (the (field (G,C) F)) # ST, LT)" +"step' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)" +"step' (New C, G, (ST,LT)) = (Class C # ST, LT)" +"step' (Checkcast C, G, (RefT rt#ST,LT)) = (Class C # ST,LT)" +"step' (Pop, G, (ts#ST,LT)) = (ST,LT)" +"step' (Dup, G, (ts#ST,LT)) = (ts#ts#ST,LT)" +"step' (Dup_x1, G, (ts1#ts2#ST,LT)) = (ts1#ts2#ts1#ST,LT)" +"step' (Dup_x2, G, (ts1#ts2#ts3#ST,LT)) = (ts1#ts2#ts3#ts1#ST,LT)" +"step' (Swap, G, (ts1#ts2#ST,LT)) = (ts2#ts1#ST,LT)" +"step' (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT)) + = (PrimT Integer#ST,LT)" +"step' (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = (ST,LT)" +"step' (Goto b, G, s) = s" + (* Return has no successor instruction in the same method: *) +(* "step' (Return, G, (T#ST,LT)) = None" *) +"step' (Invoke C mn fpTs, G, (ST,LT)) = (let ST' = drop (length fpTs) ST + in (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))" -"step (i,G,s) = None" +(* "step' (i,G,s) = None" *) + +constdefs + step :: "instr \ jvm_prog \ state_type option \ state_type option" + "step i G \ opt_map (\s. step' (i,G,s))" text "Conditions under which step is applicable:" consts -app :: "instr \ jvm_prog \ ty \ state_type \ bool" +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 \ +recdef app' "{}" +"app' (Load idx, G, rT, s) = (idx < length (snd s) \ + (snd s) ! idx \ Err)" +"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 \ +"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' (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, (ts#ts'#ST,LT)) = ((\p. ts = PrimT p \ ts' = PrimT p) \ + (\r r'. ts = RefT r \ ts' = RefT r'))" +"app' (Goto b, G, rT, s) = True" +"app' (Return, G, rT, (T#ST,LT)) = (G \ T \ rT)" +"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 \ method (G,C) (mn,fpTs) \ None \ + (\(aT,fT)\set(zip apTs fpTs). G \ aT \ fT)))" -"app (i,G,rT,s) = False" +"app' (i,G,rT,s) = False" + +constdefs + app :: "instr \ jvm_prog \ ty \ state_type option \ bool" + "app i G rT s \ case s of None \ True | Some t \ app' (i,G,rT,t)" text {* program counter of successor instructions: *} consts -succs :: "instr \ p_count \ p_count set" +succs :: "instr \ p_count \ p_count list" 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}" +"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)" @@ -120,7 +127,8 @@ 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) + hence * : "length a = 0 \ length a = 1 \ length a = 2" + by (auto simp add: less_Suc_eq) { fix x @@ -134,59 +142,79 @@ text {* \medskip -simp rules for \isa{app} without patterns, better suited for proofs: +simp rules for @{term app} *} -lemma appStore[simp]: -"app (Store idx, G, rT, s) = (\ ts ST LT. s = (ts#ST,LT) \ idx < length LT)" -by (cases s, cases "2 < length (fst s)", auto dest: 1 2) +lemma appNone[simp]: +"app i G rT None = True" + by (simp add: app_def) + +lemma appLoad[simp]: +"(app (Load idx) G rT (Some s)) = (idx < length (snd s) \ (snd s) ! idx \ Err)" + by (simp add: app_def) + +lemma appStore[simp]: +"(app (Store idx) G rT (Some s)) = (\ ts ST LT. s = (ts#ST,LT) \ idx < length LT)" + by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def) + +lemma appBipush[simp]: +"(app (Bipush i) G rT (Some s)) = True" + by (simp add: app_def) + +lemma appAconst[simp]: +"(app Aconst_null G rT (Some s)) = True" + by (simp add: app_def) + 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))" -by (cases s, cases "2 < length (fst s)", auto dest: 1 2) - +"(app (Getfield F C) G rT (Some s)) = + (\ oT vT ST LT. s = (oT#ST, LT) \ is_class G C \ + field (G,C) F = Some (C,vT) \ G \ oT \ (Class C))" + by (cases s, cases "2 < length (fst s)", auto dest!: 1 2 simp add: app_def) 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))))" -by (cases s, cases "2 < length (fst s)", auto dest: 1 2) +"(app (Putfield F C) G rT (Some s)) = + (\ vT vT' oT ST LT. s = (vT#oT#ST, LT) \ is_class G C \ + field (G,C) F = Some (C, vT') \ G \ oT \ (Class C) \ G \ vT \ vT')" + by (cases s, cases "2 < length (fst s)", auto dest!: 1 2 simp add: app_def) +lemma appNew[simp]: +"(app (New C) G rT (Some s)) = is_class G C" + by (simp add: app_def) lemma appCheckcast[simp]: -"app (Checkcast C, G, rT, s) = (\rT ST LT. s = (RefT rT#ST,LT) \ is_class G C)" -by (cases s, cases "fst s", simp, cases "hd (fst s)", auto) +"(app (Checkcast C) G rT (Some s)) = (\rT ST LT. s = (RefT rT#ST,LT) \ is_class G C)" + by (cases s, cases "fst s", simp add: app_def) + (cases "hd (fst s)", auto simp add: app_def) lemma appPop[simp]: -"app (Pop, G, rT, s) = (\ts ST LT. s = (ts#ST,LT))" -by (cases s, cases "2 < length (fst s)", auto dest: 1 2) +"(app Pop G rT (Some s)) = (\ts ST LT. s = (ts#ST,LT))" + by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def) lemma appDup[simp]: -"app (Dup, G, rT, s) = (\ts ST LT. s = (ts#ST,LT))" -by (cases s, cases "2 < length (fst s)", auto dest: 1 2) +"(app Dup G rT (Some s)) = (\ts ST LT. s = (ts#ST,LT))" + by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def) lemma appDup_x1[simp]: -"app (Dup_x1, G, rT, s) = (\ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" -by (cases s, cases "2 < length (fst s)", auto dest: 1 2) +"(app Dup_x1 G rT (Some s)) = (\ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" + by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def) lemma appDup_x2[simp]: -"app (Dup_x2, G, rT, s) = (\ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))" -by (cases s, cases "2 < length (fst s)", auto dest: 1 2) +"(app Dup_x2 G rT (Some s)) = (\ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))" + by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def) lemma appSwap[simp]: -"app (Swap, G, rT, s) = (\ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" -by (cases s, cases "2 < length (fst s)", auto dest: 1 2) +"app Swap G rT (Some s) = (\ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" + by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def) lemma appIAdd[simp]: -"app (IAdd, G, rT, s) = (\ ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))" (is "?app s = ?P s") +"app IAdd G rT (Some s) = (\ ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))" + (is "?app s = ?P s") proof (cases (open) s) case Pair have "?app (a,b) = ?P (a,b)" @@ -205,60 +233,69 @@ 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 + show ?thesis by - (cases p', auto simp add: app_def) + qed (auto simp add: a p ip t' app_def) + qed (auto simp add: a p ip app_def) + qed (auto simp add: a p app_def) + qed (auto simp add: a app_def) + qed (auto simp add: app_def) 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) +"app (Ifcmpeq b) G rT (Some s) = (\ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \ + ((\ p. ts1 = PrimT p \ ts2 = PrimT p) \ (\r r'. ts1 = RefT r \ ts2 = RefT r')))" + by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def) 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) +"app Return G rT (Some s) = (\T ST LT. s = (T#ST,LT) \ (G \ T \ rT))" + by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def) +lemma appGoto[simp]: +"app (Goto branch) G rT (Some s) = True" + by (simp add: app_def) 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") +"app (Invoke C mn fpTs) G rT (Some s) = (\apTs X ST LT mD' rT' b'. + 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) = Some (mD', rT', b'))" (is "?app s = ?P s") proof (cases (open) 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 + hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \ + length fpTs < length a" (is "?a \ ?l") + by (auto simp add: app_def) + 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 + show ?thesis by (auto simp add: app_def) blast qed with Pair have "?app s \ ?P s" by simp - thus ?thesis by auto + thus ?thesis by (auto simp add: app_def) qed -lemmas [simp del] = app_invoke - +lemma step_Some: + "step i G (Some s) \ None" + by (simp add: step_def) -lemma app_step_some: - "\app (i,G,rT,s); succs i pc \ {}\ \ step (i,G,s) \ None"; - by (cases s, cases i, auto) +lemma step_None [simp]: + "step i G None = None" + by (simp add: step_def) end diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/StepMono.thy --- a/src/HOL/MicroJava/BV/StepMono.thy Wed Aug 30 21:44:12 2000 +0200 +++ b/src/HOL/MicroJava/BV/StepMono.thy Wed Aug 30 21:47:39 2000 +0200 @@ -14,7 +14,8 @@ 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") +"\ y n. (G \ b <=l y) \ n < length y \ y!n = Ok t \ + (\t. b!n = Ok t \ (G \ (b!n) <=o (y!n)))" (is "?P b") proof (induct (open) ?P b) show "?P []" by simp @@ -24,12 +25,12 @@ 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" + "n < Suc (length zs)" "(z # zs) ! n = Ok t" - show "(\t. (a # list) ! n = Some t) \ G \(a # list) ! n <=o Some t" + show "(\t. (a # list) ! n = Ok t) \ G \(a # list) ! n <=o Ok t" proof (cases n) case 0 - with * show ?thesis by (simp add: sup_ty_opt_Some) + with * show ?thesis by (simp add: sup_ty_opt_Ok) next case Suc with Cons * @@ -40,7 +41,8 @@ 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))" +"\b. length a = length b \ + (\x\set (zip a b). x \ widen G) = (G \ (map Ok a) <=l (map Ok b))" (is "\b. length a = length b \ ?Q a b" is "?P a") proof (induct "a") show "?P []" by simp @@ -116,196 +118,211 @@ lemma app_mono: -"\G \ s2 <=s s1; app (i, G, rT, s1)\ \ app (i, G, rT, s2)"; +"\G \ s <=' s'; app i G rT s'\ \ app i G rT s"; proof - - assume G: "G \ s2 <=s s1" - assume app: "app (i, G, rT, s1)" - - show ?thesis - proof (cases (open) 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 simp add: map_eq_Cons 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 + { fix s1 s2 + assume G: "G \ s2 <=s s1" + assume app: "app i G rT (Some s1)" - 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, auto 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 + have "app i G rT (Some s2)" + proof (cases (open) 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 simp add: map_eq_Cons 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, 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, auto 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 mD' rT' b' 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) = Some (mD', rT', b')" + by (simp, elim exE conjE) (rule that) - 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 - 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 l l' + have "length (rev apTs') = length (rev apTs)" by simp - from this s1 s2 G - obtain - G': "G \ (apTs',LT') <=s (apTs,LT)" and - X : "G \ X' \ X" and "G \ (ST',LT') <=s (ST,LT)" - by (simp add: sup_state_rev_fst sup_state_append_fst sup_state_Cons1); + from this s1 s2 G + obtain + G': "G \ (apTs',LT') <=s (apTs,LT)" and + X : "G \ X' \ X" and "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) + 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" . + from G' + have "G \ map Ok apTs' <=l map Ok apTs" + by (simp add: sup_state_def) + also + from l w + have "G \ map Ok apTs <=l map Ok list" + by (simp add: all_widen_is_sup_loc) + finally + have "G \ map Ok apTs' <=l map Ok list" . - with l' - have w': "\x \ set (zip apTs' list). x \ widen G" - by (simp add: all_widen_is_sup_loc) + 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 + from Invoke s2 l' w' C' m + show ?thesis + by simp blast + qed + } note mono_Some = this + + assume "G \ s <=' s'" "app i G rT s'" + + thus ?thesis + by - (cases s, cases s', auto simp add: mono_Some) qed +lemmas [simp del] = split_paired_Ex +lemmas [simp] = step_def -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))" +lemma step_mono_Some: +"[| succs i pc \ []; app i G rT (Some s2); G \ s1 <=s s2 |] ==> + G \ the (step i G (Some s1)) <=s the (step i G (Some 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 succs: "succs i pc \ []" + assume app2: "app i G rT (Some 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 + hence "G \ Some s1 <=' Some s2" + by simp + from this app2 + have app1: "app i G rT (Some s1)" by (rule app_mono) + + have "step i G (Some s1) \ None \ step i G (Some s2) \ None" + by simp + then 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); + where step: "step i G (Some s1) = Some (a1',b1')" + "step i G (Some s2) = Some (a2',b2')" + by (auto simp del: step_def simp add: s) have "G \ (a1',b1') <=s (a2',b2')" proof (cases (open) i) @@ -313,11 +330,11 @@ with s app1 obtain y where - y: "nat < length b1" "b1 ! nat = Some y" by clarsimp + y: "nat < length b1" "b1 ! nat = Ok y" by clarsimp from Load s app2 obtain y' where - y': "nat < length b2" "b2 ! nat = Some y'" by clarsimp + y': "nat < length b2" "b2 ! nat = Ok y'" by clarsimp from G s have "G \ b1 <=l b2" by (simp add: sup_state_def) @@ -446,6 +463,12 @@ show ?thesis by auto qed +lemma step_mono: + "[| succs i pc \ []; app i G rT s2; G \ s1 <=' s2 |] ==> + G \ step i G s1 <=' step i G s2" + by (cases s1, cases s2, auto dest: step_mono_Some) +lemmas [simp del] = step_def end +