--- 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 \\<Rightarrow> method_type"
- prog_type = "cname \\<Rightarrow> class_type"
+ method_type = "state_type option list"
+ class_type = "sig \<Rightarrow> method_type"
+ prog_type = "cname \<Rightarrow> class_type"
constdefs
-wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] \\<Rightarrow> bool"
-"wt_instr i G rT phi max_pc pc \\<equiv>
- app (i, G, rT, phi!pc) \\<and>
- (\\<forall> pc' \\<in> (succs i pc). pc' < max_pc \\<and> (G \\<turnstile> the (step (i, G, phi!pc)) <=s phi!pc'))"
+wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] \<Rightarrow> bool"
+"wt_instr i G rT phi max_pc pc \<equiv>
+ app i G rT (phi!pc) \<and>
+ (\<forall> pc' \<in> set (succs i pc). pc' < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!pc'))"
-wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \\<Rightarrow> bool"
-"wt_start G C pTs mxl phi \\<equiv>
- G \\<turnstile> ([],(Some(Class C))#((map Some pTs))@(replicate mxl None)) <=s phi!0"
+wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool"
+"wt_start G C pTs mxl phi \<equiv>
+ G \<turnstile> 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] \\<Rightarrow> bool"
-"wt_method G C pTs rT mxl ins phi \\<equiv>
+wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \<Rightarrow> bool"
+"wt_method G C pTs rT mxl ins phi \<equiv>
let max_pc = length ins
in
- length ins < length phi \\<and> 0 < max_pc \\<and> wt_start G C pTs mxl phi \\<and>
- (\\<forall>pc. pc<max_pc \\<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)"
+ 0 < max_pc \<and> wt_start G C pTs mxl phi \<and>
+ (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)"
-wt_jvm_prog :: "[jvm_prog,prog_type] \\<Rightarrow> bool"
-"wt_jvm_prog G phi \\<equiv>
- wf_prog (\\<lambda>G C (sig,rT,maxl,b).
+wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool"
+"wt_jvm_prog G phi \<equiv>
+ wf_prog (\<lambda>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 \\<Longrightarrow> (\\<exists>wt. wf_prog wt G)"
+"wt_jvm_prog G phi \<Longrightarrow> (\<exists>wt. wf_prog wt G)"
by (unfold wt_jvm_prog_def, blast)
lemma wt_jvm_prog_impl_wt_instr:
-"\\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins \\<rbrakk>
- \\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
+"\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins \<rbrakk>
+ \<Longrightarrow> 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:
-"\\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins) \\<rbrakk> \\<Longrightarrow>
- 0 < (length ins) \\<and> wt_start G C (snd sig) maxl (phi C sig)"
+"\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins) \<rbrakk> \<Longrightarrow>
+ 0 < (length ins) \<and> 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} \\<Longrightarrow> wt_instr i G rT phi max_pc pc =
- (app (i, G, rT, phi!pc) \\<and> pc+1 < max_pc \\<and>
- (G \\<turnstile> the (step (i, G, phi!pc)) <=s phi!(pc+1)))"
+(* for most instructions wt_instr collapses: *)
+lemma
+"succs i pc = [pc+1] \<Longrightarrow> wt_instr i G rT phi max_pc pc =
+ (app i G rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))"
by (simp add: wt_instr_def)
end
--- 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]
-"\\<lbrakk> wt_jvm_prog G phi; \
-\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> 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
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-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
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_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 \\<turnstile> Intg i \\<Colon>\\<preceq> PrimT Integer";
-by(Simp_tac 1);
-qed "conf_Intg_Integer";
-AddIffs [conf_Intg_Integer];
-
-Goal
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-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 \\<turnstile> T' \\<preceq> T \\<Longrightarrow> T' = NT \\<longrightarrow> (T=NT | (\\<exists>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 \\<turnstile> NT \\<preceq> T = (T=NT | (\\<exists>C. T = Class C))";
-by(force_tac (claset() addIs widen.intrs addDs [lemma],simpset()) 1);
-qed "NT_subtype_conv";
-
-Goal
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-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]
- "\\<lbrakk> wf_prog ok G; G,h\\<turnstile>v\\<Colon>\\<preceq>RefT rt; cast_ok G C h v ; G\\<turnstile>Class C\\<preceq>T; is_class G C \\<rbrakk> \
-\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>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
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-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
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-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
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-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 "(\\<forall>x y. P(x,y)) = (\\<forall>z. P z)";
-by(Fast_tac 1);
-qed "collapse_paired_All";
-
-Goal
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-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
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-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 "\\<exists> 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\\<turnstile>oT\\<preceq>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 \\<turnstile> oT \\<preceq>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
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-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
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup,approx_stk_imp_approx_stk_sup]
- addss (simpset() addsimps defs1)) 1);
-qed "Goto_correct";
-
-
-Goal
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
-qed "Ifcmpeq_correct";
-
-
-Goal
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
-qed "Pop_correct";
-
-
-Goal
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
- addss (simpset() addsimps [map_eq_Cons]@defs1)) 1);
-qed "Dup_correct";
-
-
-
-Goal
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
- addss (simpset() addsimps [map_eq_Cons]@defs1)) 1);
-qed "Dup_x1_correct";
-
-Goal
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
- addss (simpset() addsimps [map_eq_Cons]@defs1)) 1);
-qed "Dup_x2_correct";
-
-Goal
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
- addss (simpset() addsimps [map_eq_Cons]@defs1)) 1);
-qed "Swap_correct";
-
-
-Goal
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
- addss (simpset() addsimps [map_eq_Cons, approx_val_def]@defs1)) 1);
-qed "IAdd_correct";
-
-
-
-(** instr correct **)
-
-Goal
-"\\<lbrakk> 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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-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 \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \
-\ \\<Longrightarrow> \\<exists>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
-"\\<And>state. \\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM state\\<surd>\\<rbrakk> \
-\ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-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
-"\\<lbrakk> xp=None; frs\\<noteq>[] \\<rbrakk> \\<Longrightarrow> (\\<exists>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
-"\\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM (xp,hp,frs)\\<surd>; xp=None; frs\\<noteq>[] \\<rbrakk> \
-\ \\<Longrightarrow> \\<exists>state'. exec(G,xp,hp,frs) = Some state' \\<and> G,phi \\<turnstile>JVM state'\\<surd>";
-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]
-"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s -jvm\\<rightarrow> t \\<rbrakk> \\<Longrightarrow> G,phi \\<turnstile>JVM s\\<surd> \\<longrightarrow> G,phi \\<turnstile>JVM t\\<surd>";
-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
-"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s0 -jvm\\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \\<turnstile>JVM s0 \\<surd>\\<rbrakk> \
-\ \\<Longrightarrow> approx_stk G hp stk (fst (((phi C) sig) ! pc)) \\<and> 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";
--- 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+ ==> 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:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+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:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+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 \<turnstile> Intg i \<Colon>\<preceq> PrimT Integer"
+by (simp add: conf_def)
+
+
+lemma Bipush_correct:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>";
+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 \<turnstile> NT \<preceq> T = (T=NT \<or> (\<exists>C. T = Class C))"
+proof -
+ have "\<And>T T'. G \<turnstile> T' \<preceq> T \<Longrightarrow> T' = NT \<longrightarrow> (T=NT | (\<exists>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:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>";
+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:
+ "\<lbrakk>wf_prog ok G; G,h\<turnstile>v\<Colon>\<preceq>RefT rt; cast_ok G C h v; G\<turnstile>Class C\<preceq>T; is_class G C\<rbrakk>
+ \<Longrightarrow> G,h\<turnstile>v\<Colon>\<preceq>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:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+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:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>";
+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:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>";
+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:
+ "(\<forall>x y. P(x,y)) = (\<forall>z. P z)"
+ by fast
+
+lemma New_correct:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+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:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
+
+ 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\<turnstile>h hp\<surd>" 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\<turnstile> X \<preceq> Class C'" and
+ w: "\<forall>x\<in>set (zip apTs pTs). x \<in> widen G" and
+ mC': "method (G, C') (mn, pTs) = Some (D', rT, body)" and
+ pc: "Suc pc < length ins" and
+ step: "G \<turnstile> 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 "\<exists>T'. typeof (option_map obj_ty \<circ> hp) oX = Some T' \<and> G \<turnstile> T' \<preceq> X"
+ by (clarsimp simp add: approx_val_def conf_def)
+
+ with X_Ref
+ obtain T' where
+ oX_Ref: "typeof (option_map obj_ty \<circ> hp) oX = Some (RefT T')"
+ "G \<turnstile> RefT T' \<preceq> 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 \<Longrightarrow> ?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 \<turnstile> Class D \<preceq> X"
+ by simp
+
+ with X_Ref
+ obtain X' where
+ X': "X = Class X'"
+ by - (drule widen_Class, elim, rule that)
+
+ with X
+ have "G \<turnstile> X' \<preceq>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\<turnstile>rT0\<preceq>rT"
+ by (auto dest: subtype_widen_methd)
+
+ from X' D
+ have "G \<turnstile> D \<preceq>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 \<turnstile> rT' \<preceq> rT0"
+ by (auto dest: subtype_widen_methd)
+
+ from mX mD
+ have rT': "G \<turnstile> rT' \<preceq> 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)) \<and> ins' \<noteq> []"
+ 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 \<turnstile> (Ok (Class D'') # map Ok pTs @ replicate mxl' Err) <=l LT0"
+ (is "G \<turnstile> ?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 \<turnstile> Class D \<preceq> 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 "\<forall>x\<in>set (zip (rev apTs) (rev pTs)). x \<in> 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 \<turnstile> 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 \<turnstile> 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 \<turnstile>JVM state'\<surd>"
+ by - (cases oX, auto)
+qed
+
+lemmas [simp del] = map_append
+
+lemma Return_correct:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+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:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: defs1)
+apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
+.
+
+
+lemma Ifcmpeq_correct:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: defs1)
+apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
+.
+
+lemma Pop_correct:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: defs1)
+apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
+.
+
+lemma Dup_correct:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+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:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+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:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+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:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+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:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+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:
+"\<lbrakk> 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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+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 \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>
+ \<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)"
+by (auto simp add: correct_state_def Let_def)
+
+
+lemma BV_correct_1 [rulify]:
+"\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk>
+ \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>";
+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:
+ "\<lbrakk> xp=None; frs\<noteq>[] \<rbrakk> \<Longrightarrow> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
+by (clarsimp simp add: neq_Nil_conv simp del: split_paired_Ex)
+
+lemma L1:
+ "\<lbrakk>wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]\<rbrakk>
+ \<Longrightarrow> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>"
+apply (drule L0)
+apply assumption
+apply (fast intro: BV_correct_1)
+.
+
+
+theorem BV_correct [rulify]:
+"\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s -jvm\<rightarrow> t \<rbrakk> \<Longrightarrow> G,phi \<turnstile>JVM s\<surd> \<longrightarrow> G,phi \<turnstile>JVM t\<surd>"
+apply (unfold exec_all_def)
+apply (erule rtrancl_induct)
+ apply simp
+apply (auto intro: BV_correct_1)
+.
+
+
+theorem BV_correct_initial:
+"\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s0 -jvm\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk>
+ \<Longrightarrow> approx_stk G hp stk (fst (the (((phi C) sig) ! pc))) \<and> 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
--- 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 \<times> locvars_type"
-constdefs
+
+consts
+ strict :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
+primrec
+ "strict f Err = Err"
+ "strict f (Ok x) = f x"
+
+consts
+ opt_map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a option \<Rightarrow> 'b option)"
+primrec
+ "opt_map f None = None"
+ "opt_map f (Some x) = Some (f x)"
+
+consts
+ val :: "'a err \<Rightarrow> 'a"
+primrec
+ "val (Ok s) = s"
- (* lifts a relation to option with None as top element *)
- lift_top :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a option \<Rightarrow> 'a option \<Rightarrow> bool)"
+
+constdefs
+ (* lifts a relation to err with Err as top element *)
+ lift_top :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a err \<Rightarrow> 'b err \<Rightarrow> bool)"
"lift_top P a' a \<equiv> case a of
- None \<Rightarrow> True
- | Some t \<Rightarrow> (case a' of None \<Rightarrow> False | Some t' \<Rightarrow> P t' t)"
+ Err \<Rightarrow> True
+ | Ok t \<Rightarrow> (case a' of Err \<Rightarrow> False | Ok t' \<Rightarrow> P t' t)"
+
+ (* lifts a relation to option with None as bottom element *)
+ lift_bottom :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a option \<Rightarrow> 'b option \<Rightarrow> bool)"
+ "lift_bottom P a' a \<equiv> case a' of
+ None \<Rightarrow> True
+ | Some t' \<Rightarrow> (case a of None \<Rightarrow> False | Some t \<Rightarrow> P t' t)"
+
+ sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool" ("_ \<turnstile>_ <=o _")
+ "sup_ty_opt G \<equiv> lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
+
+ sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool"
+ ("_ \<turnstile> _ <=l _" [71,71] 70)
+ "G \<turnstile> LT <=l LT' \<equiv> list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'"
+
+ sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"
+ ("_ \<turnstile> _ <=s _" [71,71] 70)
+ "G \<turnstile> s <=s s' \<equiv> (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
+
+ sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool"
+ ("_ \<turnstile> _ <=' _" [71,71] 70)
+ "sup_state_opt G \<equiv> lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')"
- sup_ty_opt :: "['code prog,ty option,ty option] \<Rightarrow> bool" ("_ \<turnstile>_ <=o _")
- "sup_ty_opt G \<equiv> lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
+lemma not_Err_eq [iff]:
+ "(x \<noteq> Err) = (\<exists>a. x = Ok a)"
+ by (cases x) auto
- sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool" ("_ \<turnstile> _ <=l _" [71,71] 70)
- "G \<turnstile> LT <=l LT' \<equiv> list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'"
-
- sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool" ("_ \<turnstile> _ <=s _" [71,71] 70)
- "G \<turnstile> s <=s s' \<equiv> (G \<turnstile> map Some (fst s) <=l map Some (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
+lemma not_Some_eq [iff]:
+ "(\<forall>y. x \<noteq> 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) = (\<exists>a. any = Ok a \<and> 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 \<or> (\<exists>b. any = Ok b \<and> 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) = (\<exists>a. any = Some a \<and> 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 \<or> (\<exists>b. any = Some b \<and> 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 = (\<exists>b. any = Some b \<and> 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 \<or> (\<exists>a. any = Some a \<and> P a b))"
+ by (simp add: lift_bottom_def split: option.splits)
@@ -105,18 +209,21 @@
"G \<turnstile> s <=s s"
by (simp add: sup_state_def)
+theorem sup_state_opt_refl [simp]:
+ "G \<turnstile> s <=' s"
+ by (simp add: sup_state_opt_def)
-theorem anyConvNone [simp]:
- "(G \<turnstile> None <=o any) = (any = None)"
+theorem anyConvErr [simp]:
+ "(G \<turnstile> Err <=o any) = (any = Err)"
by (simp add: sup_ty_opt_def)
-theorem SomeanyConvSome [simp]:
- "(G \<turnstile> (Some ty') <=o (Some ty)) = (G \<turnstile> ty' \<preceq> ty)"
+theorem OkanyConvOk [simp]:
+ "(G \<turnstile> (Ok ty') <=o (Ok ty)) = (G \<turnstile> ty' \<preceq> ty)"
by (simp add: sup_ty_opt_def)
-theorem sup_ty_opt_Some:
- "G \<turnstile> a <=o (Some b) \<Longrightarrow> \<exists> x. a = Some x"
+theorem sup_ty_opt_Ok:
+ "G \<turnstile> a <=o (Ok b) \<Longrightarrow> \<exists> 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 \<turnstile> Some (PrimT p) <=o X) = (X=None \<or> X = Some (PrimT p))"
- by (auto simp add: sup_ty_opt_def lift_top_Some_any)
+ "(G \<turnstile> Ok (PrimT p) <=o X) = (X=Err \<or> 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 \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))";
+ "(G \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))"
by (simp add: sup_loc_def list_all2_Cons2)
@@ -178,8 +285,8 @@
theorem all_nth_sup_loc:
- "\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))) \<longrightarrow> (G \<turnstile> a <=l b)"
- (is "?P a")
+ "\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))) \<longrightarrow>
+ (G \<turnstile> 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 \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
+ "length a = length b ==>
+ (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
proof -
assume l: "length a = length b"
- have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
- (is "?P a")
+ have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and>
+ (G \<turnstile> 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 \<turnstile> ((l#ls)@x) <=l (b@y)) = ((G \<turnstile> (l#ls) <=l b) \<and> (G \<turnstile> x <=l y))"
by - (cases b, auto)
@@ -276,8 +384,8 @@
theorem sup_loc_update [rulify]:
- "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> (G \<turnstile> x[n := a] <=l y[n := b])"
- (is "?P x")
+ "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow>
+ (G \<turnstile> 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 \<turnstile> s2 <=s s1 \<Longrightarrow> length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
+ "G \<turnstile> s2 <=s s1 ==>
+ length (fst s2) = length (fst s1) \<and> 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 \<Longrightarrow> (G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))"
+ "length a = length b ==>
+ (G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))"
by (auto simp add: sup_state_def sup_loc_append)
theorem sup_state_append_fst:
- "length a = length b \<Longrightarrow> (G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))"
+ "length a = length b ==>
+ (G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))"
by (auto simp add: sup_state_def sup_loc_append)
theorem sup_state_Cons1:
- "(G \<turnstile> (x#xt, a) <=s (yt, b)) = (\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))"
+ "(G \<turnstile> (x#xt, a) <=s (yt, b)) =
+ (\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))"
by (auto simp add: sup_state_def map_eq_Cons)
theorem sup_state_Cons2:
- "(G \<turnstile> (xt, a) <=s (y#yt, b)) = (\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt',a) <=s (yt,b)))"
+ "(G \<turnstile> (xt, a) <=s (y#yt, b)) =
+ (\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (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 \<turnstile> None <=' any) = True"
+ by (simp add: sup_state_opt_def lift_bottom_def)
+
+lemma sup_state_opt_any_None [iff]:
+ "(G \<turnstile> any <=' None) = (any = None)"
+ by (simp add: sup_state_opt_def)
+
+lemma sup_state_opt_Some_Some [iff]:
+ "(G \<turnstile> (Some a) <=' (Some b)) = (G \<turnstile> a <=s b)"
+ by (simp add: sup_state_opt_def del: split_paired_Ex)
+
+lemma sup_state_opt_any_Some [iff]:
+ "(G \<turnstile> (Some a) <=' any) = (\<exists>b. any = Some b \<and> G \<turnstile> a <=s b)"
+ by (simp add: sup_state_opt_def)
+
+lemma sup_state_opt_Some_any:
+ "(G \<turnstile> any <=' (Some b)) = (any = None \<or> (\<exists>a. any = Some a \<and> G \<turnstile> a <=s b))"
+ by (simp add: sup_state_opt_def lift_bottom_Some_any)
+
+
theorem sup_ty_opt_trans [trans]:
"\<lbrakk>G \<turnstile> a <=o b; G \<turnstile> b <=o c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=o c"
by (auto intro: lift_top_trans widen_trans simp add: sup_ty_opt_def)
-
theorem sup_loc_trans [trans]:
"\<lbrakk>G \<turnstile> a <=l b; G \<turnstile> b <=l c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=l c"
proof -
@@ -359,4 +493,9 @@
"\<lbrakk>G \<turnstile> a <=s b; G \<turnstile> b <=s c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=s c"
by (auto intro: sup_loc_trans simp add: sup_state_def)
+theorem sup_state_opt_trans [trans]:
+ "\<lbrakk>G \<turnstile> a <=' b; G \<turnstile> b <=' c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=' c"
+ by (auto intro: lift_bottom_trans sup_state_trans simp add: sup_state_opt_def)
+
+
end
--- 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 \\<longrightarrow> hp \\<le>| (hp((newref hp) \\<mapsto> 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') \\<longrightarrow> hp \\<le>| (hp(a \\<mapsto> (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
-"\\<lbrakk> wf_prog wt G \\<rbrakk> \
-\\\<Longrightarrow> approx_val G hp v (Some T) \\<longrightarrow> G\\<turnstile> T\\<preceq>T' \\<longrightarrow> 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 \\<longrightarrow> hp \\<le>| hp' \\<longrightarrow> 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
-"\\<lbrakk> hp a = Some obj' ; G,hp\\<turnstile> v\\<Colon>\\<preceq>T ; obj_ty obj = obj_ty obj' \\<rbrakk> \
-\\\<Longrightarrow>G,(hp(a\\<mapsto>obj))\\<turnstile> v\\<Colon>\\<preceq>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 \\<Longrightarrow> approx_val G h val us \\<longrightarrow> G \\<turnstile> us <=o us' \\<longrightarrow> 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]
-"\\<lbrakk> wf_prog wt G; approx_loc G hp loc LT; idx < length LT ; val = loc ! idx ; G \\<turnstile> LT ! idx <=o at\\<rbrakk> \
-\\\<Longrightarrow> 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 \\<and> 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]
-"\\<lbrakk> wf_prog wt G \\<rbrakk> \
-\\\<Longrightarrow> (\\<forall>tt'\\<in>set (zip tys_n ts). tt' \\<in> widen G) \\<longrightarrow> \
-\ length tys_n = length ts \\<longrightarrow> approx_stk G hp s tys_n \\<longrightarrow> 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]
-"\\<forall> lvars. approx_loc G hp lvars lt \\<longrightarrow> hp \\<le>| hp' \\<longrightarrow> 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 \\<Longrightarrow> approx_loc G hp lvars lt \\<longrightarrow> G \\<turnstile> lt <=l lt' \\<longrightarrow> 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]
-"\\<forall>loc idx x X. (approx_loc G hp loc LT) \\<longrightarrow> (approx_val G hp x X) \
-\ \\<longrightarrow> (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]
-"\\<forall>L1 l2 L2. length l1=length L1 \
-\ \\<longrightarrow> approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \\<and> 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]
-"\\<forall> lvars. approx_stk G hp lvars lt \\<longrightarrow> hp \\<le>| hp' \\<longrightarrow> 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 \\<Longrightarrow> approx_stk G hp lvars st \\<longrightarrow> G \\<turnstile> (map Some st) <=l (map Some st') \\<longrightarrow> 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) \\<and> 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') = \
-\ (\\<exists>s stk'. stk = s#stk' \\<and> approx_val G hp s (Some S) \\<and> 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') \
-\ \\<Longrightarrow> (\\<exists>s stk'. stk = s@stk' \\<and> length s = length S \\<and> length stk' = length ST' \\<and> \
-\ approx_stk G hp s S \\<and> 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]
-"\\<lbrakk> is_class G C; wf_prog wt G \\<rbrakk> \\<Longrightarrow> \
-\G,h\\<turnstile> (C, map_of (map (\\<lambda>(f,fT).(f,default_val fT)) (fields(G,C))))\\<surd>";
-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]
-"\\<lbrakk> map_of (fields (G, oT)) FD = Some T ; G,hp\\<turnstile>v\\<Colon>\\<preceq>T ; \
-\ G,hp\\<turnstile>(oT,fs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,hp\\<turnstile>(oT, fs(FD\\<mapsto>v))\\<surd>";
-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 \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \\<longrightarrow> G,hp\\<turnstile>obj'\\<surd> \
-\ \\<longrightarrow> G,(hp(newref hp\\<mapsto>obj'))\\<turnstile>obj\\<surd>";
-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' \\<longrightarrow> obj_ty obj' = obj_ty obj'' \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \
-\ \\<longrightarrow> G,hp(a\\<mapsto>obj'')\\<turnstile>obj\\<surd>";
-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 \\<longrightarrow> G\\<turnstile>h hp\\<surd> \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \\<longrightarrow> G\\<turnstile>h hp(newref hp\\<mapsto>obj)\\<surd>";
-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 \\<and> hp oloc = Some(oT,fs) \\<and> \
-\ G,hp\\<turnstile>v\\<Colon>\\<preceq>T \\<and> G\\<turnstile>h hp\\<surd> \\<longrightarrow> G\\<turnstile>h hp(oloc \\<mapsto> (oT, fs((F,D)\\<mapsto>v)))\\<surd>";
-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
-"\\<forall>rT C sig. correct_frames G hp phi rT sig frs \\<longrightarrow> \
-\ hp a = Some (C,od) \\<longrightarrow> map_of (fields (G, C)) fl = Some fd \\<longrightarrow> \
-\ G,hp\\<turnstile>v\\<Colon>\\<preceq>fd \
-\ \\<longrightarrow> correct_frames G (hp(a \\<mapsto> (C, od(fl\\<mapsto>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
-"\\<forall>rT C sig. hp x = None \\<longrightarrow> correct_frames G hp phi rT sig frs \\<and> \
-\ oconf G hp obj \
-\ \\<longrightarrow> correct_frames G (hp(newref hp \\<mapsto> 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";
-
--- 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] \\<Rightarrow> bool"
-"approx_val G h v any \\<equiv> case any of None \\<Rightarrow> True | Some T \\<Rightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T"
+ approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool"
+"approx_val G h v any \<equiv> case any of Err \<Rightarrow> True | Ok T \<Rightarrow> G,h\<turnstile>v\<Colon>\<preceq>T"
- approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \\<Rightarrow> bool"
-"approx_loc G hp loc LT \\<equiv> list_all2 (approx_val G hp) loc LT"
+ approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \<Rightarrow> bool"
+"approx_loc G hp loc LT \<equiv> list_all2 (approx_val G hp) loc LT"
+
+ approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \<Rightarrow> bool"
+"approx_stk G hp stk ST \<equiv> approx_loc G hp stk (map Ok ST)"
- approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \\<Rightarrow> bool"
-"approx_stk G hp stk ST \\<equiv> approx_loc G hp stk (map Some ST)"
+ correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
+"correct_frame G hp \<equiv> \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
+ approx_stk G hp stk ST \<and> approx_loc G hp loc LT \<and>
+ pc < length ins \<and> length loc=length(snd sig)+maxl+1"
- correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] \\<Rightarrow> frame \\<Rightarrow> bool"
-"correct_frame G hp \\<equiv> \\<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
- approx_stk G hp stk ST \\<and> approx_loc G hp loc LT \\<and>
- pc < length ins \\<and> length loc=length(snd sig)+maxl+1"
+ correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
+"correct_frame_opt G hp s \<equiv> case s of None \<Rightarrow> \<lambda>maxl ins f. False | Some t \<Rightarrow> correct_frame G hp t"
+
consts
- correct_frames :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \\<Rightarrow> bool"
+ correct_frames :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \<Rightarrow> 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
- (\\<exists>rT maxl ins.
- method (G,C) sig = Some(C,rT,(maxl,ins)) \\<and>
- (\\<exists>C' mn pTs k. pc = k+1 \\<and> ins!k = (Invoke C' mn pTs) \\<and>
- (mn,pTs) = sig0 \\<and>
- (\\<exists>apTs D ST'.
- fst((phi C sig)!k) = (rev apTs) @ (Class D) # ST' \\<and>
- length apTs = length pTs \\<and>
- (\\<exists>D' rT' maxl' ins'.
- method (G,D) sig0 = Some(D',rT',(maxl',ins')) \\<and>
- G \\<turnstile> rT0 \\<preceq> rT') \\<and>
- correct_frame G hp (tl ST, LT) maxl ins f \\<and>
+ (let (stk,loc,C,sig,pc) = f in
+ (\<exists>ST LT rT maxl ins.
+ phi C sig ! pc = Some (ST,LT) \<and>
+ method (G,C) sig = Some(C,rT,(maxl,ins)) \<and>
+ (\<exists>C' mn pTs k. pc = k+1 \<and> ins!k = (Invoke C' mn pTs) \<and>
+ (mn,pTs) = sig0 \<and>
+ (\<exists>apTs D ST' LT'.
+ (phi C sig)!k = Some ((rev apTs) @ (Class D) # ST', LT') \<and>
+ length apTs = length pTs \<and>
+ (\<exists>D' rT' maxl' ins'.
+ method (G,D) sig0 = Some(D',rT',(maxl',ins')) \<and>
+ G \<turnstile> rT0 \<preceq> rT') \<and>
+ correct_frame G hp (tl ST, LT) maxl ins f \<and>
correct_frames G hp phi rT sig frs))))"
constdefs
- correct_state :: "[jvm_prog,prog_type,jvm_state] \\<Rightarrow> bool"
- ("_,_\\<turnstile>JVM _\\<surd>" [51,51] 50)
-"correct_state G phi \\<equiv> \\<lambda>(xp,hp,frs).
+ correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
+ ("_,_\<turnstile>JVM _\<surd>" [51,51] 50)
+"correct_state G phi \<equiv> \<lambda>(xp,hp,frs).
case xp of
- None \\<Rightarrow> (case frs of
- [] \\<Rightarrow> True
- | (f#fs) \\<Rightarrow> G\\<turnstile>h hp\\<surd> \\<and>
+ None \<Rightarrow> (case frs of
+ [] \<Rightarrow> True
+ | (f#fs) \<Rightarrow> G\<turnstile>h hp\<surd> \<and>
(let (stk,loc,C,sig,pc) = f
in
- \\<exists>rT maxl ins.
- method (G,C) sig = Some(C,rT,(maxl,ins)) \\<and>
- correct_frame G hp ((phi C sig) ! pc) maxl ins f \\<and>
+ \<exists>rT maxl ins s.
+ method (G,C) sig = Some(C,rT,(maxl,ins)) \<and>
+ phi C sig ! pc = Some s \<and>
+ correct_frame G hp s maxl ins f \<and>
correct_frames G hp phi rT sig fs))
- | Some x \\<Rightarrow> True"
+ | Some x \<Rightarrow> True"
+
+
+lemma sup_heap_newref:
+ "hp x = None \<Longrightarrow> hp \<le>| hp(newref hp \<mapsto> 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') \<Longrightarrow> hp \<le>| hp (a \<mapsto> (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 \<Longrightarrow> approx_val G hp v (Ok T) \<longrightarrow> G\<turnstile> T\<preceq>T' \<longrightarrow> 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 \<longrightarrow> hp \<le>| hp' \<longrightarrow> 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:
+ "\<lbrakk>hp a = Some obj'; G,hp\<turnstile> v\<Colon>\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk>
+ \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v\<Colon>\<preceq>T"
+by (cases v, auto simp add: obj_ty_def conf_def)
+
+lemma approx_val_imp_approx_val_sup [rulify]:
+ "wf_prog wt G \<Longrightarrow> (approx_val G h v us) \<longrightarrow> (G \<turnstile> us <=o us') \<longrightarrow> (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:
+ "\<lbrakk>wf_prog wt G; approx_loc G hp loc LT; idx < length LT; v = loc!idx; G \<turnstile> LT!idx <=o at\<rbrakk>
+ \<Longrightarrow> 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 \<and> approx_loc G hp xs ls)"
+by (simp add: approx_loc_def)
+
+lemma assConv_approx_stk_imp_approx_loc [rulify]:
+ "wf_prog wt G \<Longrightarrow> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G)
+ \<longrightarrow> length tys_n = length ts \<longrightarrow> approx_stk G hp s tys_n \<longrightarrow>
+ 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]:
+ "\<forall>lvars. approx_loc G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> 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 \<Longrightarrow> approx_loc G hp lvars lt \<longrightarrow> G \<turnstile> lt <=l lt' \<longrightarrow> 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]:
+ "\<forall>loc idx x X. (approx_loc G hp loc LT) \<longrightarrow> (approx_val G hp x X)
+ \<longrightarrow> (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]:
+ "\<forall>L1 l2 L2. length l1=length L1 \<longrightarrow>
+ approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> 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]:
+ "\<forall>lvars. approx_stk G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> 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 \<Longrightarrow> approx_stk G hp lvars st \<longrightarrow> (G \<turnstile> map Ok st <=l (map Ok st'))
+ \<longrightarrow> 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) \<and> 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') =
+ (\<exists>s stk'. stk = s#stk' \<and> approx_val G hp s (Ok S) \<and> 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') \<Longrightarrow>
+ (\<exists>s stk'. stk = s@stk' \<and> length s = length S \<and> length stk' = length ST' \<and>
+ approx_stk G hp s S \<and> approx_stk G hp stk' ST')"
+by (simp add: list_all2_append2 approx_stk_def approx_loc_def)
+
+
+(** oconf **)
+
+lemma correct_init_obj:
+ "\<lbrakk>is_class G C; wf_prog wt G\<rbrakk> \<Longrightarrow>
+ G,h \<turnstile> (C, map_of (map (\<lambda>(f,fT).(f,default_val fT)) (fields(G,C)))) \<surd>"
+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]:
+ "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v\<Colon>\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
+ \<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
+by (simp add: oconf_def lconf_def)
+
+
+lemma oconf_imp_oconf_heap_newref [rulify]:
+"hp x = None \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G,hp\<turnstile>obj'\<surd> \<longrightarrow> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>"
+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' \<longrightarrow> obj_ty obj' = obj_ty obj'' \<longrightarrow> G,hp\<turnstile>obj\<surd>
+ \<longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
+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 \<longrightarrow> G\<turnstile>h hp\<surd> \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>"
+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 \<and> hp oloc = Some(oT,fs) \<and>
+ G,hp\<turnstile>v\<Colon>\<preceq>T \<and> G\<turnstile>h hp\<surd> \<longrightarrow> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>"
+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]:
+ "\<forall>rT C sig. correct_frames G hp phi rT sig frs \<longrightarrow>
+ hp a = Some (C,od) \<longrightarrow> map_of (fields (G, C)) fl = Some fd \<longrightarrow>
+ G,hp\<turnstile>v\<Colon>\<preceq>fd
+ \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, od(fl\<mapsto>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]:
+ "\<forall>rT C sig. hp x = None \<longrightarrow> correct_frames G hp phi rT sig frs \<and> oconf G hp obj
+ \<longrightarrow> correct_frames G (hp(newref hp \<mapsto> 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
+
--- 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] \<Rightarrow> bool"
- "is_approx a b \<equiv> length a = length b \<and> (\<forall> n. n < length a \<longrightarrow>
- (a!n = None \<or> a!n = Some (b!n)))"
-
- contains_dead :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
- "contains_dead ins cert phi pc \<equiv>
- Suc pc \<notin> succs (ins!pc) pc \<and> Suc pc < length phi \<longrightarrow>
- cert ! (Suc pc) = Some (phi ! Suc pc)"
-
contains_targets :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
- "contains_targets ins cert phi pc \<equiv> (
- \<forall> pc' \<in> succs (ins!pc) pc. pc' \<noteq> Suc pc \<and> pc' < length phi \<longrightarrow>
- cert!pc' = Some (phi!pc'))"
-
+ "contains_targets ins cert phi pc \<equiv>
+ \<forall>pc' \<in> set (succs (ins!pc) pc).
+ pc' \<noteq> pc+1 \<and> pc' < length ins \<longrightarrow> cert!pc' = phi!pc'"
fits :: "[instr list, certificate, method_type] \<Rightarrow> bool"
- "fits ins cert phi \<equiv> is_approx cert phi \<and> length ins < length phi \<and>
- (\<forall> pc. pc < length ins \<longrightarrow>
- contains_dead ins cert phi pc \<and>
- contains_targets ins cert phi pc)"
+ "fits ins cert phi \<equiv> \<forall>pc. pc < length ins \<longrightarrow>
+ contains_targets ins cert phi pc \<and>
+ (cert!pc = None \<or> cert!pc = phi!pc)"
is_target :: "[instr list, p_count] \<Rightarrow> bool"
- "is_target ins pc \<equiv> \<exists> pc'. pc' < length ins \<and> pc \<in> succs (ins!pc') pc'"
-
- maybe_dead :: "[instr list, p_count] \<Rightarrow> bool"
- "maybe_dead ins pc \<equiv> \<exists> pc'. pc = pc'+1 \<and> pc \<notin> succs (ins!pc') pc'"
-
- mdot :: "[instr list, p_count] \<Rightarrow> bool"
- "mdot ins pc \<equiv> maybe_dead ins pc \<or> is_target ins pc"
+ "is_target ins pc \<equiv>
+ \<exists>pc'. pc \<noteq> pc'+1 \<and> pc' < length ins \<and> pc \<in> set (succs (ins!pc') pc')"
-consts
- option_filter_n :: "['a list, nat \<Rightarrow> bool, nat] \<Rightarrow> '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 \<Rightarrow> bool] \<Rightarrow> 'a option list"
- "option_filter l P \<equiv> option_filter_n l P 0"
-
make_cert :: "[instr list, method_type] \<Rightarrow> certificate"
- "make_cert ins phi \<equiv> option_filter phi (mdot ins)"
-
+ "make_cert ins phi \<equiv>
+ map (\<lambda>pc. if is_target ins pc then phi!pc else None) [0..length ins(]"
+
make_Cert :: "[jvm_prog, prog_type] \<Rightarrow> prog_certificate"
"make_Cert G Phi \<equiv> \<lambda> C sig.
- let (C,x,y,mdecls) = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C in
- let (sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig in
- make_cert b (Phi C sig)"
+ let (C,x,y,mdecls) = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
+ (sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
+ in make_cert b (Phi C sig)"
lemmas [simp del] = split_paired_Ex
-lemma length_ofn [rulify]: "\<forall>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 "\<forall>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 \<or>
- 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 \<or>
- 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 \<noteq> phi ! pc |] ==>
+ make_cert ins phi ! pc = None"
+ by (auto simp add: make_cert_def)
-lemma option_filter_Some:
-"\<lbrakk>n < length l; P n\<rbrakk> \<Longrightarrow> option_filter l P ! n = Some (l!n)"
-proof -
-
- assume 1: "n < length l" "P n"
-
- have "\<forall>n n'. n < length l \<longrightarrow> P (n+n') \<longrightarrow> 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 \<Longrightarrow> 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' \<in> succs (ins ! pc) pc"
- "pc' \<noteq> Suc pc" and
- pc': "pc' < length phi"
+ "pc' \<in> set (succs (ins ! pc) pc)"
+ "pc' \<noteq> 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 \<Longrightarrow> 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:
-"\<lbrakk>fits ins cert phi; pc' \<in> succs (ins!pc) pc; pc' \<noteq> Suc pc; pc < length ins; pc' < length ins\<rbrakk>
- \<Longrightarrow> cert!pc' = Some (phi!pc')"
-by (clarsimp simp add: fits_def contains_dead_def contains_targets_def)
+ "[| fits ins cert phi; pc' \<in> set (succs (ins!pc) pc);
+ pc' \<noteq> Suc pc; pc < length ins; pc' < length ins |]
+ ==> cert!pc' = phi!pc'"
+ by (clarsimp simp add: fits_def contains_targets_def)
lemma fitsD2:
-"\<lbrakk>fits ins cert phi; Suc pc \<notin> succs (ins!pc) pc; pc < length ins\<rbrakk>
- \<Longrightarrow> 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:
-"\<lbrakk>wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins;
- G \<turnstile> s2 <=s s1; i = ins!pc\<rbrakk> \<Longrightarrow>
- \<exists> s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \<and> (G \<turnstile> s2' <=s s1')"
+ "[| wtl_inst i G rT s1 cert mpc pc = Ok s1'; fits ins cert phi;
+ pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
+ \<exists> s2'. wtl_inst (ins!pc) G rT s2 cert mpc pc = Ok s2' \<and> (G \<turnstile> 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 \<turnstile> s2 <=s s1"
+ assume G: "G \<turnstile> 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 \<noteq> {} \<Longrightarrow> G \<turnstile> the (?step s2) <=s the (?step s1)"
- by - (drule step_mono, auto simp add: wtl_inst_def)
-
- with app
- have some: "succs i pc \<noteq> {} \<Longrightarrow> ?step s2 \<noteq> None" by (simp add: app_step_some)
+ have step: "succs i pc \<noteq> [] ==> G \<turnstile> ?step s2 <=' ?step s1"
+ by - (drule step_mono, auto simp add: wtl_inst_Ok)
{
fix pc'
- assume 0: "pc' \<in> succs i pc" "pc' \<noteq> pc+1"
- hence "succs i pc \<noteq> {}" by auto
- hence "G \<turnstile> the (?step s2) <=s the (?step s1)" by (rule step)
+ assume 0: "pc' \<in> set (succs i pc)" "pc' \<noteq> pc+1"
+ hence "succs i pc \<noteq> []" by auto
+ hence "G \<turnstile> ?step s2 <=' ?step s1" by (rule step)
also
from wtl 0
- have "G \<turnstile> the (?step s1) <=s the (cert!pc')"
- by (auto simp add: wtl_inst_def)
+ have "G \<turnstile> ?step s1 <=' cert!pc'"
+ by (auto simp add: wtl_inst_Ok)
finally
- have "G\<turnstile> the (?step s2) <=s the (cert!pc')" .
+ have "G\<turnstile> ?step s2 <=' cert!pc'" .
} note cert = this
- have "\<exists>s2'. wtl_inst i G rT s2 s2' cert mpc pc \<and> G \<turnstile> s2' <=s s1'"
- proof (cases "pc+1 \<in> succs i pc")
+ have "\<exists>s2'. wtl_inst i G rT s2 cert mpc pc = Ok s2' \<and> G \<turnstile> s2' <=' s1'"
+ proof (cases "pc+1 \<in> 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 \<and> G \<turnstile> (the (?step s2)) <=s s1'"
+ have "wtl_inst i G rT s2 cert mpc pc = Ok (?step s2) \<and> G \<turnstile> ?step s2 <=' s1'"
(is "?wtl \<and> ?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 \<and> G \<turnstile> s1' <=s s1'"
- by (clarsimp intro!: cert simp add: wtl_inst_def)
+ have "wtl_inst i G rT s2 cert mpc pc = Ok s1' \<and> G \<turnstile> 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:
-"\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi;
- pc < length ins; G \<turnstile> s2 <=s s1; i = ins!pc\<rbrakk> \<Longrightarrow>
- \<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \<and> (G \<turnstile> 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 \<turnstile> s2 <=' s1; i = ins!pc |] ==>
+ \<exists> s2'. wtl_cert (ins!pc) G rT s2 cert mpc pc = Ok s2' \<and> (G \<turnstile> 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 \<turnstile> s2 <=s s1" "i = ins!pc"
+ "G \<turnstile> 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 \<turnstile> s2 <=s a"
- by - (rule sup_state_trans, (simp add: wtl_inst_option_def)+)
+ have G: "G \<turnstile> 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 "\<exists> s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \<and> (G \<turnstile> s2' <=s s1')"
- by - (rule wtl_inst_mono, (simp add: wtl_inst_option_def)+)
+ have "\<exists> s2'. wtl_inst (ins!pc) G rT (Some a) cert mpc pc = Ok s2' \<and>
+ (G \<turnstile> 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:
-"\<lbrakk>wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
- pc < length ins; length ins = max_pc\<rbrakk> \<Longrightarrow>
- \<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \<and> G \<turnstile> 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 \<noteq> 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' \<in> succs (ins!pc) pc \<Longrightarrow> pc' < length ins"
+ have pc': "\<And>pc'. pc' \<in> 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' \<in> succs (ins!pc) pc \<Longrightarrow> G \<turnstile> ?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'. \<lbrakk>pc' \<in> succs (ins!pc) pc; pc' < max_pc; pc' \<noteq> pc+1\<rbrakk>
- \<Longrightarrow> cert!pc' \<noteq> None \<and> G \<turnstile> ?s' <=s the (cert!pc')"
- by (auto dest: fitsD simp add: wt_instr_def)
-
- show ?thesis
- proof (cases "pc+1 \<in> succs (ins!pc) pc")
- case True
-
- have "wtl_inst (ins!pc) G rT (phi!pc) ?s' cert max_pc pc \<and> G \<turnstile> ?s' <=s phi ! Suc pc" (is "?wtl \<and> ?G")
- proof
- from True
- show "G \<turnstile> ?s' <=s phi ! Suc pc" by (simp add: G)
+ have cert: "!!pc'. \<lbrakk>pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1\<rbrakk>
+ \<Longrightarrow> G \<turnstile> ?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 \<and> G \<turnstile> ?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:
-"\<lbrakk>fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc; max_pc = length ins\<rbrakk> \<Longrightarrow>
- \<exists> s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \<and> G \<turnstile> 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 \<turnstile> 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 \<in> 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 \<turnstile> ... <=' phi!Suc pc"
+ by (simp add: wt_instr_def)
+ finally have ?thesis .
+ }
- hence * : "\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \<and> G \<turnstile> s <=s phi ! Suc pc"
- by - (rule wt_instr_imp_wtl_inst, simp+)
+ moreover
+ { assume "Suc pc \<notin> 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 \<noteq> 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 \<noteq> 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 \<turnstile> 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:
-"\<forall> pc. (\<forall>pc'. pc' < length all_ins \<longrightarrow> wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \<longrightarrow>
+"\<forall> pc. (\<forall>pc'. pc' < length all_ins \<longrightarrow>
+ wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \<longrightarrow>
fits all_ins cert phi \<longrightarrow>
(\<exists>l. pc = length l \<and> all_ins = l@ins) \<longrightarrow>
pc < length all_ins \<longrightarrow>
- (\<forall> s. (G \<turnstile> s <=s (phi!pc)) \<longrightarrow>
- (\<exists>s'. wtl_inst_list ins G rT s s' cert (length all_ins) pc))"
-(is "\<forall>pc. ?wt \<longrightarrow> ?fits \<longrightarrow> ?l pc ins \<longrightarrow> ?len pc \<longrightarrow> ?wtl pc ins" is "\<forall>pc. ?C pc ins" is "?P ins")
+ (\<forall> s. (G \<turnstile> s <=' (phi!pc)) \<longrightarrow>
+ wtl_inst_list ins G rT cert (length all_ins) pc s \<noteq> Err)"
+(is "\<forall>pc. ?wt \<longrightarrow> ?fits \<longrightarrow> ?l pc ins \<longrightarrow> ?len pc \<longrightarrow> ?wtl pc ins"
+ is "\<forall>pc. ?C pc ins" is "?P ins")
proof (induct "?P" "ins")
case Nil
show "?P []" by simp
@@ -421,53 +346,56 @@
assume wt : "\<forall>pc'. pc' < length all_ins \<longrightarrow>
wt_instr (all_ins ! pc') G rT phi (length all_ins) pc'"
assume fits: "fits all_ins cert phi"
- assume G : "G \<turnstile> s <=s phi ! pc"
assume l : "pc < length all_ins"
-
+ assume G : "G \<turnstile> 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 \<turnstile> 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 \<noteq> 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 \<turnstile> s2 <=s s1"
- by - (drule wtl_option_mono, assumption+, simp, elim exE conjE, rule that)
-
- with s1
- have G': "G \<turnstile> 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) \<longrightarrow> ?wtl (Suc pc) ins'" by auto
- show "\<exists>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 \<noteq> 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 \<turnstile> 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 \<turnstile> s' <=' s''"
+ by - (drule wtl_cert_mono, auto)
+ ultimately
+ have G': "G \<turnstile> 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' \<noteq> Err"
+ by auto
+
+ with i c'
show ?thesis by auto
qed
qed
@@ -475,38 +403,42 @@
lemma fits_imp_wtl_method_complete:
-"\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\<rbrakk>
- \<Longrightarrow> 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:
-"\<lbrakk>wt_method G C pTs rT mxl ins phi; wf_prog wf_mb G\<rbrakk>
- \<Longrightarrow> 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)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow> a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'"
+"(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow>
+ a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'"
by (induct "l") auto
lemma unique_epsilon:
-"(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
+ "(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow>
+ (\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
by (auto simp add: unique_set)
-theorem wtl_complete: "\<lbrakk>wt_jvm_prog G Phi\<rbrakk> \<Longrightarrow> 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 (\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G"
+ assume wfprog:
+ "wf_prog (\<lambda>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 : "\<forall>(C,sc,fs,ms)\<in>set G.
Ball (set fs) (wf_fdecl G) \<and>
unique fs \<and>
- (\<forall>(sig,rT,mb)\<in>set ms. wf_mhead G sig rT \<and> (\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \<and>
+ (\<forall>(sig,rT,mb)\<in>set ms. wf_mhead G sig rT \<and>
+ (\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \<and>
unique ms \<and>
(case sc of None \<Rightarrow> C = Object
| Some D \<Rightarrow>
is_class G D \<and>
(D, C) \<notin> (subcls1 G)^* \<and>
- (\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') \<longrightarrow> G\<turnstile>rT\<preceq>rT'))"
+ (\<forall>(sig,rT,b)\<in>set ms.
+ \<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') \<longrightarrow> G\<turnstile>rT\<preceq>rT'))"
"(a, aa, ab, b) \<in> 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: "\<forall>(sig,rT,mb)\<in>set b. wf_mhead G sig rT \<and> (\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb"
+ assume m: "\<forall>(sig,rT,mb)\<in>set b. wf_mhead G sig rT \<and>
+ (\<lambda>(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
--- 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] \<Rightarrow> bool"
-"fits_partial phi pc is G rT s0 s2 cert \<equiv> (\<forall> a b i s1. (a@(i#b) = is) \<longrightarrow>
- wtl_inst_list a G rT s0 s1 cert (pc+length is) pc \<longrightarrow>
- wtl_inst_list (i#b) G rT s1 s2 cert (pc+length is) (pc+length a) \<longrightarrow>
- ((cert!(pc+length a) = None \<longrightarrow> phi!(pc+length a) = s1) \<and>
- (\<forall> t. cert!(pc+length a) = Some t \<longrightarrow> phi!(pc+length a) = t)))"
-
-fits :: "[method_type,instr list,jvm_prog,ty,state_type,state_type,certificate] \<Rightarrow> bool"
-"fits phi is G rT s0 s2 cert \<equiv> fits_partial phi 0 is G rT s0 s2 cert"
+fits :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] \<Rightarrow> bool"
+"fits phi is G rT s0 cert \<equiv>
+ (\<forall>pc s1. pc < length is \<longrightarrow>
+ (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1 \<longrightarrow>
+ (case cert!pc of None \<Rightarrow> phi!pc = s1
+ | Some t \<Rightarrow> phi!pc = Some t)))"
+
+constdefs
+make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] \<Rightarrow> method_type"
+"make_phi is G rT s0 cert \<equiv>
+ map (\<lambda>pc. case cert!pc of
+ None \<Rightarrow> val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)
+ | Some t \<Rightarrow> Some t) [0..length is(]"
+
-lemma fitsD:
-"fits phi is G rT s0 s2 cert \<Longrightarrow>
- (a@(i#b) = is) \<Longrightarrow>
- wtl_inst_list a G rT s0 s1 cert (0+length is) 0 \<Longrightarrow>
- wtl_inst_list (i#b) G rT s1 s2 cert (0+length is) (0+length a) \<Longrightarrow>
- ((cert!(0+length a) = None \<longrightarrow> phi!(0+length a) = s1) \<and>
- (\<forall> t. cert!(0+length a) = Some t \<longrightarrow> phi!(0+length a) = t))"
-by (unfold fits_def fits_partial_def) blast
+lemma fitsD_None:
+ "\<lbrakk>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\<rbrakk> \<Longrightarrow> phi!pc = s1"
+ by (auto simp add: fits_def)
-lemma exists_list: "\<exists>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:
+ "\<lbrakk>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\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow>
- \<exists> phi. fits phi is G rT s0 s2 cert \<and> length is < length phi"
-proof -
- assume all: "wtl_inst_list is G rT s0 s2 cert (length is) 0"
- have "\<forall> s0 pc. wtl_inst_list is G rT s0 s2 cert (pc+length is) pc
- \<longrightarrow> (\<exists> phi. pc + length is < length phi \<and> 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 \<longrightarrow> phi ! (pc + length x) = s1') \<and>
- (\<forall>t. cert ! (pc + length x) = Some t \<longrightarrow> phi ! (pc + length x) = t)"
+ "\<exists>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 "\<exists>phi. pc + length (a # list) < length phi \<and>
- 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:
-"\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\<rbrakk> \<Longrightarrow>
- \<forall> pc t. pc < length is \<longrightarrow> (cert ! pc) = Some t \<longrightarrow> (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 \<noteq> []" by auto
- hence cons: "\<exists>i y. is = i#y" by (simp add: neq_Nil_conv)
- from wtl pc
- have "\<exists>a b s1. a@b = is \<and> length a = pc \<and>
- wtl_inst_list a G rT s0 s1 cert (length is) 0 \<and>
- wtl_inst_list b G rT s1 s3 cert (length is) (0+length a)"
- (is "\<exists>a b s1. ?A a b \<and> ?L a \<and> ?W1 a s1 \<and> ?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 \<noteq> []" by auto
- hence "\<exists>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 |]
+ ==> \<forall>pc t. pc < length is \<longrightarrow> cert!pc = Some t \<longrightarrow> 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:
-"\<lbrakk>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))\<rbrakk>
- \<Longrightarrow> 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:
-"\<lbrakk>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 \<rbrakk> \<Longrightarrow>
- b \<noteq> [] \<longrightarrow> G \<turnstile> 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 \<noteq> []"
+ "[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> 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 \<turnstile> s'' <=' phi ! Suc pc"
+proof -
+
+ assume all: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> 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 \<noteq> 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 \<turnstile> 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 \<longrightarrow> phi ! (0 + length (a @ [i])) = s2) \<and>
- (\<forall>t. cert ! (0 + length (a @ [i])) = Some t \<longrightarrow> 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:
-"\<lbrakk>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\<rbrakk> \<Longrightarrow>
- 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: "\<And>t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
+ by (simp add: wtl_cert_def split: if_splits)
+ moreover
+ from fits pc wts
+ have c2: "\<And>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: "\<forall>t. cert ! (length i1) = Some t \<longrightarrow> phi ! (length i1) = t"
- by intro (rule fits_lemma1 [rulify], auto)
-
- from w1 wo w2 f
- have c2: "cert ! (length i1) = None \<Longrightarrow> phi ! (length i1) = s1"
- by - (rule fits_lemma2)
-
- from wtl f
- have c3: "\<forall>pc t. pc < length(i1@i#i2) \<longrightarrow> cert ! pc = Some t \<longrightarrow> phi ! pc = t"
- by (rule fits_lemma1)
-
- from w1 wo w2 f
- have suc: "i2 \<noteq> [] \<Longrightarrow> G \<turnstile> 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:
-"\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\<rbrakk>
- \<Longrightarrow> \<forall>pc. pc < length is \<longrightarrow> 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 \<noteq> 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 \<noteq> 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:
+ "\<And>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' \<in> set (succs (is!pc) pc)"
- from l pc
- have "i2' \<noteq> []" 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 \<turnstile> step (is!pc) G (phi!pc) <=' phi ! pc'"
+ proof (cases "pc' = Suc pc")
+ case False
+ with wti pc'
+ have G: "G \<turnstile> 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 \<turnstile> s'' <=' phi ! Suc pc"
+ by - (drule wtl_suc_pc)
+ with True less
+ have "G \<turnstile> 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 \<Longrightarrow>
- \<exists> phi. \<forall>pc. pc < length is \<longrightarrow> 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:
-"\<lbrakk>is \<noteq> [];wtl_inst_list is G rT s0 s2 cert (length is) 0;
- fits phi is G rT s0 s2 cert\<rbrakk> \<Longrightarrow> G \<turnstile> s0 <=s phi ! 0"
+ "[| 0 < length is; wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err;
+ fits phi is G rT s cert |] ==>
+ G \<turnstile> 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 \<noteq> []"
+ assume wtl: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> 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 "\<And>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
+ "\<And>t. cert!0 = Some t ==> G \<turnstile> 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 \<longrightarrow> phi ! (0 + length []) = s0) \<and>
- (\<forall>t. cert ! (0 + length []) = Some t \<longrightarrow> 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 \<Longrightarrow> \<exists> 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 \<noteq> []"
- assume wtl: "wtl_inst_list ins G rT ?s0 s2 cert (length ins) 0"
+"wtl_method G C pTs rT mxl ins cert ==> \<exists> 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 \<noteq> Err"
- from this
- obtain phi where fits: "fits phi ins G rT ?s0 s2 cert \<and> 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:
"\<forall>pc. pc < length ins \<longrightarrow> 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)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow> a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'"
+ "(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow>
+ a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'"
by (induct "l") auto
lemma unique_epsilon:
-"(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
+ "(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow>
+ (\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> 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 "\<exists>Phi. Ball (set G) (wf_cdecl (\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G)"
+ show "\<exists>Phi. Ball (set G) (wf_cdecl (\<lambda>G C (sig,rT,maxl,b).
+ wt_method G C (snd sig) rT maxl b (Phi C sig)) G)"
(is "\<exists>Phi. ?Q Phi")
proof (intro exI)
- let "?Phi" =
- "\<lambda> C sig. let (C,x,y,mdecls) = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C in
- let (sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig in\
- \<epsilon> phi. wt_method G C (snd sig) rT maxl b phi"
+ let "?Phi" = "\<lambda> C sig.
+ let (C,x,y,mdecls) = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
+ (sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
+ in \<epsilon> 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 \<in> set G" "x = (a, b)" "b = (aa, ba)" "ba = (ab, bb)" "m \<in> set bb"
with wtl_prog
- show "wf_mdecl (\<lambda>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 (\<lambda>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 "\<forall>(sig,rT,mb)\<in>set bb. wf_mhead G sig rT \<and>
(\<lambda>(maxl,b). wtl_method G a (snd sig) rT maxl b (cert a sig)) mb"
@@ -451,7 +332,7 @@
(\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> 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
--- 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 \<Rightarrow> certificate"
prog_certificate = "cname \<Rightarrow> class_certificate"
+
constdefs
-wtl_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \<Rightarrow> bool"
+ check_cert :: "[instr, jvm_prog, state_type option, certificate, p_count, p_count]
+ \<Rightarrow> bool"
+ "check_cert i G s cert pc max_pc \<equiv> \<forall>pc' \<in> set (succs i pc). pc' < max_pc \<and>
+ (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> step i G s <=' cert!pc')"
-"wtl_inst i G rT s s' cert max_pc pc \<equiv> app (i,G,rT,s) \<and>
- (let s'' = the (step (i,G,s)) in
- (\<forall> pc' \<in> (succs i pc). pc' < max_pc \<and>
- ((pc' \<noteq> pc+1) \<longrightarrow> cert!pc' \<noteq> None \<and> G \<turnstile> s'' <=s the (cert!pc'))) \<and>
- (if (pc+1) \<in> (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]
+ \<Rightarrow> state_type option err"
+ "wtl_inst i G rT s cert max_pc pc \<equiv>
+ if app i G rT s \<and> 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} \<Longrightarrow>
- wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \<and> pc+1 < max_pc \<and> (s' = the (step (i,G,s))))"
-by (unfold wtl_inst_def, auto)
-
-lemma [simp]:
-"succs i pc = {} \<Longrightarrow> wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \<and> 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 \<and> (\<forall>pc' \<in> set (succs i pc).
+ pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> step i G s <=' cert!pc')) \<and>
+ (if pc+1 \<in> 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] \<Rightarrow> bool"
-"wtl_inst_option i G rT s0 s1 cert max_pc pc \<equiv>
- (case cert!pc of
- None \<Rightarrow> wtl_inst i G rT s0 s1 cert max_pc pc
- | Some s0' \<Rightarrow> (G \<turnstile> s0 <=s s0') \<and>
- 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] \<Rightarrow> bool"
+ wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count]
+ \<Rightarrow> state_type option err"
+ "wtl_cert i G rT s cert max_pc pc \<equiv>
+ case cert!pc of
+ None \<Rightarrow> wtl_inst i G rT s cert max_pc pc
+ | Some s' \<Rightarrow> if G \<turnstile> 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] \<Rightarrow> 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 =
- (\<exists>s1. wtl_inst_option instr G rT s0 s1 cert max_pc pc \<and>
- 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] \<Rightarrow> bool"
- "wtl_method G C pTs rT mxl ins cert \<equiv>
- let max_pc = length ins
- in
- 0 < max_pc \<and>
- (\<exists>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] \<Rightarrow> bool"
+ "wtl_method G C pTs rT mxl ins cert \<equiv>
+ let max_pc = length ins
+ in
+ 0 < max_pc \<and>
+ wtl_inst_list ins G rT cert max_pc 0
+ (Some ([],(Ok (Class C))#((map Ok pTs))@(replicate mxl Err))) \<noteq> Err"
- wtl_jvm_prog :: "[jvm_prog,prog_certificate] \<Rightarrow> bool"
- "wtl_jvm_prog G cert \<equiv>
- wf_prog (\<lambda>G C (sig,rT,maxl,b).
- wtl_method G C (snd sig) rT maxl b (cert C sig)) G"
-
-text {* \medskip *}
-
-lemma rev_eq: "\<lbrakk>length a = n; length x = n; rev a @ b # c = rev x @ y # z\<rbrakk> \<Longrightarrow> a = x \<and> b = y \<and> c = z"
-by auto
-
-lemma wtl_inst_unique:
-"wtl_inst i G rT s0 s1 cert max_pc pc \<longrightarrow>
- wtl_inst i G rT s0 s1' cert max_pc pc \<longrightarrow> s1 = s1'" (is "?P i")
-by (unfold wtl_inst_def, auto)
+ wtl_jvm_prog :: "[jvm_prog,prog_certificate] \<Rightarrow> bool"
+ "wtl_jvm_prog G cert \<equiv>
+ wf_prog (\<lambda>G C (sig,rT,maxl,b). wtl_method G C (snd sig) rT maxl b (cert C sig)) G"
-lemma wtl_inst_option_unique:
-"\<lbrakk>wtl_inst_option i G rT s0 s1 cert max_pc pc;
- wtl_inst_option i G rT s0 s1' cert max_pc pc\<rbrakk> \<Longrightarrow> s1 = s1'"
-by (cases "cert!pc") (auto simp add: wtl_inst_unique wtl_inst_option_def)
+text {* \medskip *}
-lemma wtl_inst_list_unique:
-"\<forall> s0 pc. wtl_inst_list is G rT s0 s1 cert max_pc pc \<longrightarrow>
- wtl_inst_list is G rT s0 s1' cert max_pc pc \<longrightarrow> 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) = (\<exists> z. x = Ok z \<and> 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 \<noteq> Err =
+ (\<exists>s'. wtl_cert i G rT s cert max_pc pc = Ok s' \<and>
+ wtl_inst_list is G rT cert max_pc (pc+1) s' \<noteq> 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:
-"\<forall> pc' pc s.
- wtl_inst_list is G rT s s' cert mpc pc \<longrightarrow> \
- pc' < length is \<longrightarrow> \
- (\<exists> a b s1. a @ b = is \<and> length a = pc' \<and> \
- wtl_inst_list a G rT s s1 cert mpc pc \<and> \
- 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:
+"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mpc pc s = Ok s') =
+ (\<exists>s''. wtl_inst_list a G rT cert mpc pc s = Ok s'' \<and>
+ wtl_inst_list b G rT cert mpc (pc+length a) s'' = Ok s')"
+ (is "\<forall> 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 "\<exists> a' b s1.
- a' @ b = a#list \<and> length a' = pc' \<and> \
- wtl_inst_list a' G rT s s1 cert mpc pc \<and> \
- wtl_inst_list b G rT s1 s' cert mpc (pc+length a')"
- (is "\<exists> 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":
-"\<lbrakk>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)\<rbrakk> \<Longrightarrow>
- 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'' ==>
+ \<exists>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
- "\<forall> pc s0.
- wtl_inst_list x G rT s0 s1 cert (pc+length (x@y)) pc \<longrightarrow>
- wtl_inst_list y G rT s1 s2 cert (pc+length (x@y)) (pc+length x) \<longrightarrow>
- 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:
+ "\<forall>n. n < length l \<longrightarrow> 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:
-"\<lbrakk>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))\<rbrakk> \<Longrightarrow>
- 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":
-"\<lbrakk>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))\<rbrakk> \<Longrightarrow>
- 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 \<noteq> Err;
+ pc < length is |] ==>
+ \<exists>s' s''. wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s' \<and>
+ 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 \<noteq> Err"
- have "\<forall> s0 pc. wtl_inst_list a G rT s0 s1 cert (pc+length (a@i#b)) pc \<longrightarrow>
- wtl_inst_option i G rT s1 s2 cert (pc+length (a@i#b)) (pc + length a) \<longrightarrow>
- wtl_inst_list b G rT s2 s3 cert (pc+length (a@i#b)) (Suc pc + length a) \<longrightarrow>
- 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 "\<forall>s0 pc. ?x s0 pc \<longrightarrow> ?y s0 pc \<longrightarrow> ?z s0 pc \<longrightarrow> ?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 \<noteq> 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
--- 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 \<times> jvm_prog \<times> state_type \<Rightarrow> state_type option"
+step' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> 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 \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option"
+ "step i G \<equiv> opt_map (\<lambda>s. step' (i,G,s))"
text "Conditions under which step is applicable:"
consts
-app :: "instr \<times> jvm_prog \<times> ty \<times> state_type \<Rightarrow> bool"
+app' :: "instr \<times> jvm_prog \<times> ty \<times> state_type \<Rightarrow> bool"
-recdef app "{}"
-"app (Load idx, G, rT, s) = (idx < length (snd s) \<and> (snd s) ! idx \<noteq> 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 \<and>
+recdef app' "{}"
+"app' (Load idx, G, rT, s) = (idx < length (snd s) \<and>
+ (snd s) ! idx \<noteq> 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 \<and>
field (G,C) F \<noteq> None \<and>
fst (the (field (G,C) F)) = C \<and>
G \<turnstile> oT \<preceq> (Class C))"
-"app (Putfield F C, G, rT, (vT#oT#ST, LT)) = (is_class G C \<and>
+"app' (Putfield F C, G, rT, (vT#oT#ST, LT)) = (is_class G C \<and>
field (G,C) F \<noteq> None \<and>
fst (the (field (G,C) F)) = C \<and>
G \<turnstile> oT \<preceq> (Class C) \<and>
G \<turnstile> vT \<preceq> (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)) = ((\<exists> p. ts1 = PrimT p \<and> ts1 = PrimT p) \<or>
- (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r'))"
-"app (Goto b, G, rT, s) = True"
-"app (Return, G, rT, (T#ST,LT)) = (G \<turnstile> T \<preceq> rT)"
-app_invoke:
-"app (Invoke C mn fpTs, G, rT, s) = (length fpTs < length (fst s) \<and>
- (let
- apTs = rev (take (length fpTs) (fst s));
- X = hd (drop (length fpTs) (fst s))
- in
- G \<turnstile> X \<preceq> Class C \<and>
- (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and>
- method (G,C) (mn,fpTs) \<noteq> 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)) = ((\<exists>p. ts = PrimT p \<and> ts' = PrimT p) \<or>
+ (\<exists>r r'. ts = RefT r \<and> ts' = RefT r'))"
+"app' (Goto b, G, rT, s) = True"
+"app' (Return, G, rT, (T#ST,LT)) = (G \<turnstile> T \<preceq> rT)"
+"app' (Invoke C mn fpTs, G, rT, s) =
+ (length fpTs < length (fst s) \<and>
+ (let apTs = rev (take (length fpTs) (fst s));
+ X = hd (drop (length fpTs) (fst s))
+ in
+ G \<turnstile> X \<preceq> Class C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and>
+ (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT)))"
-"app (i,G,rT,s) = False"
+"app' (i,G,rT,s) = False"
+
+constdefs
+ app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> ty \<Rightarrow> state_type option \<Rightarrow> bool"
+ "app i G rT s \<equiv> case s of None \<Rightarrow> True | Some t \<Rightarrow> app' (i,G,rT,t)"
text {* program counter of successor instructions: *}
consts
-succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count set"
+succs :: "instr \<Rightarrow> p_count \<Rightarrow> 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 \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
@@ -120,7 +127,8 @@
proof -;
assume "\<not>(2 < length a)"
hence "length a < (Suc 2)" by simp
- hence * : "length a = 0 \<or> length a = 1 \<or> length a = 2" by (auto simp add: less_Suc_eq)
+ hence * : "length a = 0 \<or> length a = 1 \<or> 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) = (\<exists> ts ST LT. s = (ts#ST,LT) \<and> 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) \<and> (snd s) ! idx \<noteq> Err)"
+ by (simp add: app_def)
+
+lemma appStore[simp]:
+"(app (Store idx) G rT (Some s)) = (\<exists> ts ST LT. s = (ts#ST,LT) \<and> 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) = (\<exists> oT ST LT. s = (oT#ST, LT) \<and> is_class G C \<and>
- fst (the (field (G,C) F)) = C \<and>
- field (G,C) F \<noteq> None \<and> G \<turnstile> oT \<preceq> (Class C))"
-by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
-
+"(app (Getfield F C) G rT (Some s)) =
+ (\<exists> oT vT ST LT. s = (oT#ST, LT) \<and> is_class G C \<and>
+ field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq> (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) = (\<exists> vT oT ST LT. s = (vT#oT#ST, LT) \<and> is_class G C \<and>
- field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and>
- G \<turnstile> oT \<preceq> (Class C) \<and>
- G \<turnstile> vT \<preceq> (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)) =
+ (\<exists> vT vT' oT ST LT. s = (vT#oT#ST, LT) \<and> is_class G C \<and>
+ field (G,C) F = Some (C, vT') \<and> G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> 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) = (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C)"
-by (cases s, cases "fst s", simp, cases "hd (fst s)", auto)
+"(app (Checkcast C) G rT (Some s)) = (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> 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) = (\<exists>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)) = (\<exists>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) = (\<exists>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)) = (\<exists>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) = (\<exists>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)) = (\<exists>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) = (\<exists>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)) = (\<exists>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) = (\<exists>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) = (\<exists>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) = (\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))" (is "?app s = ?P s")
+"app IAdd G rT (Some s) = (\<exists> 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) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and>
- ((\<exists> p. ts1 = PrimT p \<and> ts1 = PrimT p) \<or>
- (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r')))"
-by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+"app (Ifcmpeq b) G rT (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and>
+ ((\<exists> p. ts1 = PrimT p \<and> ts2 = PrimT p) \<or> (\<exists>r r'. ts1 = RefT r \<and> 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) = (\<exists>T ST LT. s = (T#ST,LT) \<and> (G \<turnstile> T \<preceq> rT))"
-by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+"app Return G rT (Some s) = (\<exists>T ST LT. s = (T#ST,LT) \<and> (G \<turnstile> T \<preceq> 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) = (\<exists>apTs X ST LT.
- s = ((rev apTs) @ (X # ST), LT) \<and>
- length apTs = length fpTs \<and>
- G \<turnstile> X \<preceq> Class C \<and>
- (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and>
- method (G,C) (mn,fpTs) \<noteq> None)" (is "?app s = ?P s")
+"app (Invoke C mn fpTs) G rT (Some s) = (\<exists>apTs X ST LT mD' rT' b'.
+ s = ((rev apTs) @ (X # ST), LT) \<and> length apTs = length fpTs \<and>
+ G \<turnstile> X \<preceq> Class C \<and> (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and>
+ method (G,C) (mn,fpTs) = Some (mD', rT', b'))" (is "?app s = ?P s")
proof (cases (open) s)
case Pair
have "?app (a,b) \<Longrightarrow> ?P (a,b)"
proof -
assume app: "?app (a,b)"
- hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and> length fpTs < length a"
- (is "?a \<and> ?l") by auto
- hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l") by auto
- hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs" by (auto simp add: min_def)
- hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 0 < length ST" by blast
- hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> ST \<noteq> []" by blast
- hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> (\<exists>X ST'. ST = X#ST')" by (simp add: neq_Nil_conv)
- hence "\<exists>apTs X ST. a = rev apTs @ X # ST \<and> length apTs = length fpTs" by blast
+ hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and>
+ length fpTs < length a" (is "?a \<and> ?l")
+ by (auto simp add: app_def)
+ hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l")
+ by auto
+ hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs"
+ by (auto simp add: min_def)
+ hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 0 < length ST"
+ by blast
+ hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> ST \<noteq> []"
+ by blast
+ hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and>
+ (\<exists>X ST'. ST = X#ST')"
+ by (simp add: neq_Nil_conv)
+ hence "\<exists>apTs X ST. a = rev apTs @ X # ST \<and> 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 \<Longrightarrow> ?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) \<noteq> None"
+ by (simp add: step_def)
-lemma app_step_some:
- "\<lbrakk>app (i,G,rT,s); succs i pc \<noteq> {}\<rbrakk> \<Longrightarrow> step (i,G,s) \<noteq> None";
- by (cases s, cases i, auto)
+lemma step_None [simp]:
+ "step i G None = None"
+ by (simp add: step_def)
end
--- 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]:
-"\<forall> y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = Some t \<longrightarrow> (\<exists>t. b!n = Some t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
+"\<forall> y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = Ok t \<longrightarrow>
+ (\<exists>t. b!n = Ok t \<and> (G \<turnstile> (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 \<turnstile> 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 "(\<exists>t. (a # list) ! n = Some t) \<and> G \<turnstile>(a # list) ! n <=o Some t"
+ show "(\<exists>t. (a # list) ! n = Ok t) \<and> G \<turnstile>(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:
-"\<forall>b. length a = length b \<longrightarrow> (\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map Some a) <=l (map Some b))"
+"\<forall>b. length a = length b \<longrightarrow>
+ (\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map Ok a) <=l (map Ok b))"
(is "\<forall>b. length a = length b \<longrightarrow> ?Q a b" is "?P a")
proof (induct "a")
show "?P []" by simp
@@ -116,196 +118,211 @@
lemma app_mono:
-"\<lbrakk>G \<turnstile> s2 <=s s1; app (i, G, rT, s1)\<rbrakk> \<Longrightarrow> app (i, G, rT, s2)";
+"\<lbrakk>G \<turnstile> s <=' s'; app i G rT s'\<rbrakk> \<Longrightarrow> app i G rT s";
proof -
- assume G: "G \<turnstile> 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 \<turnstile> 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 \<turnstile> 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\<turnstile> oT\<preceq> (Class cname)" and
- vT: "G\<turnstile> vT\<preceq> 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\<turnstile> oT' \<preceq> oT" and
- vT': "G\<turnstile> vT' \<preceq> vT"
- by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that)
- moreover
- from vT' vT
- have "G \<turnstile> vT' \<preceq> b" by (rule widen_trans)
- moreover
- from oT' oT
- have "G\<turnstile> oT' \<preceq> (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 \<turnstile> 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\<turnstile> oT\<preceq> (Class cname)" and
+ vT: "G\<turnstile> vT\<preceq> 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\<turnstile> oT' \<preceq> oT" and
+ vT': "G\<turnstile> vT' \<preceq> vT"
+ by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that)
+ moreover
+ from vT' vT
+ have "G \<turnstile> vT' \<preceq> b" by (rule widen_trans)
+ moreover
+ from oT' oT
+ have "G\<turnstile> oT' \<preceq> (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 \<turnstile> X \<preceq> Class cname" and
+ w: "\<forall>x \<in> set (zip apTs list). x \<in> 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 \<turnstile> X \<preceq> Class cname" and
- w: "\<forall>x \<in> set (zip apTs list). x \<in> widen G" and
- m: "method (G, cname) (mname, list) \<noteq> 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 "\<exists>a b c. (fst s2) = rev a @ b # c \<and> 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 "\<exists>a b c. (fst s2) = rev a @ b # c \<and> 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 \<turnstile> (apTs',LT') <=s (apTs,LT)" and
- X : "G \<turnstile> X' \<preceq> X" and "G \<turnstile> (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 \<turnstile> (apTs',LT') <=s (apTs,LT)" and
+ X : "G \<turnstile> X' \<preceq> X" and "G \<turnstile> (ST',LT') <=s (ST,LT)"
+ by (simp add: sup_state_rev_fst sup_state_append_fst sup_state_Cons1)
- with C
- have C': "G \<turnstile> X' \<preceq> Class cname"
- by - (rule widen_trans, auto)
+ with C
+ have C': "G \<turnstile> X' \<preceq> Class cname"
+ by - (rule widen_trans, auto)
- from G'
- have "G \<turnstile> map Some apTs' <=l map Some apTs"
- by (simp add: sup_state_def)
- also
- from l w
- have "G \<turnstile> map Some apTs <=l map Some list"
- by (simp add: all_widen_is_sup_loc)
- finally
- have "G \<turnstile> map Some apTs' <=l map Some list" .
+ from G'
+ have "G \<turnstile> map Ok apTs' <=l map Ok apTs"
+ by (simp add: sup_state_def)
+ also
+ from l w
+ have "G \<turnstile> map Ok apTs <=l map Ok list"
+ by (simp add: all_widen_is_sup_loc)
+ finally
+ have "G \<turnstile> map Ok apTs' <=l map Ok list" .
- with l'
- have w': "\<forall>x \<in> set (zip apTs' list). x \<in> widen G"
- by (simp add: all_widen_is_sup_loc)
+ with l'
+ have w': "\<forall>x \<in> set (zip apTs' list). x \<in> 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 \<turnstile> 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:
-"\<lbrakk>succs i pc \<noteq> {}; app (i,G,rT,s2); G \<turnstile> s1 <=s s2\<rbrakk> \<Longrightarrow>
- G \<turnstile> the (step (i,G,s1)) <=s the (step (i,G,s2))"
+lemma step_mono_Some:
+"[| succs i pc \<noteq> []; app i G rT (Some s2); G \<turnstile> s1 <=s s2 |] ==>
+ G \<turnstile> 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 \<noteq> {}"
- assume app2: "app (i,G,rT,s2)"
+ assume succs: "succs i pc \<noteq> []"
+ assume app2: "app i G rT (Some s2)"
assume G: "G \<turnstile> s1 <=s s2"
- from G app2
- have app1: "app (i,G,rT,s1)" by (rule app_mono)
-
- from app1 app2 succs
+ hence "G \<turnstile> 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) \<noteq> None \<and> step i G (Some s2) \<noteq> 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 \<turnstile> (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 \<turnstile> b1 <=l b2" by (simp add: sup_state_def)
@@ -446,6 +463,12 @@
show ?thesis by auto
qed
+lemma step_mono:
+ "[| succs i pc \<noteq> []; app i G rT s2; G \<turnstile> s1 <=' s2 |] ==>
+ G \<turnstile> step i G s1 <=' step i G s2"
+ by (cases s1, cases s2, auto dest: step_mono_Some)
+lemmas [simp del] = step_def
end
+