--- a/src/HOL/MicroJava/BV/BVSpec.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Sun Dec 16 00:17:44 2001 +0100
@@ -1,63 +1,60 @@
(* Title: HOL/MicroJava/BV/BVSpec.thy
ID: $Id$
- Author: Cornelia Pusch
+ Author: Cornelia Pusch, Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
*)
header "The Bytecode Verifier"
-theory BVSpec = Step:
+theory BVSpec = Effect:
+
+text {*
+ This theory contains a specification of the BV. The specification
+ describes correct typings of method bodies; it corresponds
+ to type \emph{checking}.
+*}
constdefs
-wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,p_count] => bool"
-"wt_instr i G rT phi mxs max_pc pc ==
- app i G mxs 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_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,
+ exception_table,p_count] => bool"
+ "wt_instr i G rT phi mxs max_pc et pc ==
+ app i G mxs rT pc et (phi!pc) \<and>
+ (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
-wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool"
-"wt_start G C pTs mxl phi ==
- G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
-
+ wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool"
+ "wt_start G C pTs mxl phi ==
+ G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
-wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,method_type] => bool"
-"wt_method G C pTs rT mxs mxl ins phi ==
- let max_pc = length ins
- in
- 0 < max_pc \<and> wt_start G C pTs mxl phi \<and>
- (\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc pc)"
+ wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
+ exception_table,method_type] => bool"
+ "wt_method G C pTs rT mxs mxl ins et phi ==
+ let max_pc = length ins in
+ 0 < max_pc \<and> wt_start G C pTs mxl phi \<and>
+ (\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc et pc)"
-wt_jvm_prog :: "[jvm_prog,prog_type] => bool"
-"wt_jvm_prog G phi ==
- wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b)).
- wt_method G C (snd sig) rT maxs maxl b (phi C sig)) G"
-
+ wt_jvm_prog :: "[jvm_prog,prog_type] => bool"
+ "wt_jvm_prog G phi ==
+ wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)).
+ wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G"
lemma wt_jvm_progD:
-"wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
-by (unfold wt_jvm_prog_def, blast)
+ "wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
+ by (unfold wt_jvm_prog_def, blast)
lemma wt_jvm_prog_impl_wt_instr:
-"[| wt_jvm_prog G phi; is_class G C;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins); pc < length ins |]
- ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc";
-by (unfold wt_jvm_prog_def, drule method_wf_mdecl,
- simp, simp, simp add: wf_mdecl_def wt_method_def)
+ "[| wt_jvm_prog G phi; is_class G C;
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins |]
+ ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc";
+ by (unfold wt_jvm_prog_def, drule method_wf_mdecl,
+ simp, simp, simp add: wf_mdecl_def wt_method_def)
lemma wt_jvm_prog_impl_wt_start:
-"[| wt_jvm_prog G phi; is_class G C;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==>
- 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, simp add: wf_mdecl_def wt_method_def)
-
-text {* for most instructions wt\_instr collapses: *}
-lemma
-"succs i pc = [pc+1] ==> wt_instr i G rT phi mxs max_pc pc =
- (app i G mxs 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)
+ "[| wt_jvm_prog G phi; is_class G C;
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) |] ==>
+ 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, simp add: wf_mdecl_def wt_method_def)
end
-
-
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sun Dec 16 00:17:44 2001 +0100
@@ -1,42 +1,594 @@
(* Title: HOL/MicroJava/BV/BVSpecTypeSafe.thy
ID: $Id$
- Author: Cornelia Pusch
+ Author: Cornelia Pusch, Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
-Proof that the specification of the bytecode verifier only admits type safe
-programs.
*)
header "BV Type Safety Proof"
theory BVSpecTypeSafe = Correct:
+text {*
+ This theory contains proof that the specification of the bytecode
+ verifier only admits type safe programs.
+*}
+
+section {* Preliminaries *}
+
+text {*
+ Simp and intro setup for the type safety proof:
+*}
lemmas defs1 = sup_state_conv correct_state_def correct_frame_def
- wt_instr_def step_def
+ wt_instr_def eff_def norm_eff_def
lemmas widen_rules[intro] = approx_val_widen approx_loc_widen approx_stk_widen
lemmas [simp del] = split_paired_All
+
+text {*
+ If we have a welltyped program and a conforming state, we
+ can directly infer that the current instruction is well typed:
+*}
lemma wt_jvm_prog_impl_wt_instr_cor:
- "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
- ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc"
+ ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
apply (unfold correct_state_def Let_def correct_frame_def)
apply simp
apply (blast intro: wt_jvm_prog_impl_wt_instr)
done
+
+section {* Exception Handling *}
+
+text {*
+ Exceptions don't touch anything except the stack:
+*}
+lemma exec_instr_xcpt:
+ "(fst (exec_instr i G hp stk vars Cl sig pc frs) = Some xcp)
+ = (\<exists>stk'. exec_instr i G hp stk vars Cl sig pc frs =
+ (Some xcp, hp, (stk', vars, Cl, sig, pc)#frs))"
+ by (cases i, auto simp add: split_beta split: split_if_asm)
+
+
+text {*
+ Relates @{text match_any} from the Bytecode Verifier with
+ @{text match_exception_table} from the operational semantics:
+*}
+lemma in_match_any:
+ "match_exception_table G xcpt pc et = Some pc' ==>
+ \<exists>C. C \<in> set (match_any G pc et) \<and> G \<turnstile> xcpt \<preceq>C C \<and>
+ match_exception_table G C pc et = Some pc'"
+ (is "PROP ?P et" is "?match et ==> ?match_any et")
+proof (induct et)
+ show "PROP ?P []"
+ by simp
+
+ fix e es
+ assume IH: "PROP ?P es"
+ assume match: "?match (e#es)"
+
+ obtain start_pc end_pc handler_pc catch_type where
+ e [simp]: "e = (start_pc, end_pc, handler_pc, catch_type)"
+ by (cases e)
+
+ from IH match
+ show "?match_any (e#es)"
+ proof (cases "match_exception_entry G xcpt pc e")
+ case False
+ with match
+ have "match_exception_table G xcpt pc es = Some pc'" by simp
+ with IH
+ obtain C where
+ set: "C \<in> set (match_any G pc es)" and
+ C: "G \<turnstile> xcpt \<preceq>C C" and
+ m: "match_exception_table G C pc es = Some pc'" by blast
+
+ from set
+ have "C \<in> set (match_any G pc (e#es))" by simp
+ moreover
+ from False C
+ have "\<not> match_exception_entry G C pc e"
+ by - (erule contrapos_nn,
+ auto simp add: match_exception_entry_def elim: rtrancl_trans)
+ with m
+ have "match_exception_table G C pc (e#es) = Some pc'" by simp
+ moreover note C
+ ultimately
+ show ?thesis by blast
+ next
+ case True with match
+ have "match_exception_entry G catch_type pc e"
+ by (simp add: match_exception_entry_def)
+ moreover
+ from True match
+ obtain
+ "start_pc \<le> pc"
+ "pc < end_pc"
+ "G \<turnstile> xcpt \<preceq>C catch_type"
+ "handler_pc = pc'"
+ by (simp add: match_exception_entry_def)
+ ultimately
+ show ?thesis by auto
+ qed
+qed
+
+text {*
+ We can prove separately that the recursive search for exception
+ handlers (@{text find_handler}) in the frame stack results in
+ a conforming state (if there was no matching exception handler
+ in the current frame). We require that the exception is a valid
+ heap address, and that the state before the exception occured
+ conforms.
+*}
+lemma uncaught_xcpt_correct:
+ "!!f. [| wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T;
+ G,phi \<turnstile>JVM (None, hp, f#frs)\<surd> |]
+ ==> G,phi \<turnstile>JVM (find_handler G (Some xcp) hp frs)\<surd>"
+ (is "!!f. [| ?wt; ?adr; ?hp; ?correct (None, hp, f#frs) |] ==> ?correct (?find frs)")
+proof (induct frs)
+ -- "the base case is trivial, as it should be"
+ show "?correct (?find [])" by (simp add: correct_state_def)
+
+ -- "we will need both forms @{text wt_jvm_prog} and @{text wf_prog} later"
+ assume wt: ?wt
+ then obtain mb where wf: "wf_prog mb G" by (simp add: wt_jvm_prog_def)
+
+ -- "these two don't change in the induction:"
+ assume adr: ?adr
+ assume hp: ?hp
+
+ -- "the assumption for the cons case:"
+ fix f f' frs'
+ assume cr: "?correct (None, hp, f#f'#frs')"
+
+ -- "the induction hypothesis as produced by Isabelle, immediatly simplified
+ with the fixed assumptions above"
+ assume "\<And>f. [| ?wt; ?adr; ?hp; ?correct (None, hp, f#frs') |] ==> ?correct (?find frs')"
+ with wt adr hp
+ have IH: "\<And>f. ?correct (None, hp, f#frs') ==> ?correct (?find frs')" by blast
+
+ from cr
+ have cr': "?correct (None, hp, f'#frs')" by (auto simp add: correct_state_def)
+
+ obtain stk loc C sig pc where f' [simp]: "f' = (stk,loc,C,sig,pc)"
+ by (cases f')
+
+ from cr
+ obtain rT maxs maxl ins et where
+ meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
+ by (simp add: correct_state_def, blast)
+
+ hence [simp]: "ex_table_of (snd (snd (the (method (G, C) sig)))) = et"
+ by simp
+
+ show "?correct (?find (f'#frs'))"
+ proof (cases "match_exception_table G (cname_of hp xcp) pc et")
+ case None
+ with cr' IH
+ show ?thesis by simp
+ next
+ fix handler_pc
+ assume match: "match_exception_table G (cname_of hp xcp) pc et = Some handler_pc"
+ (is "?match (cname_of hp xcp) = _")
+
+ from wt meth cr' [simplified]
+ have wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
+ by (rule wt_jvm_prog_impl_wt_instr_cor)
+
+ from cr meth
+ obtain C' mn pts ST LT where
+ ins: "ins!pc = Invoke C' mn pts" (is "_ = ?i") and
+ phi: "phi C sig ! pc = Some (ST, LT)"
+ by (simp add: correct_state_def) blast
+
+ from match
+ obtain D where
+ in_any: "D \<in> set (match_any G pc et)" and
+ D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and
+ match': "?match D = Some handler_pc"
+ by (blast dest: in_match_any)
+
+ from ins wti phi have
+ "\<forall>D\<in>set (match_any G pc et). the (?match D) < length ins \<and>
+ G \<turnstile> Some ([Class D], LT) <=' phi C sig!the (?match D)"
+ by (simp add: wt_instr_def eff_def xcpt_eff_def)
+ with in_any match' obtain
+ pc: "handler_pc < length ins"
+ "G \<turnstile> Some ([Class D], LT) <=' phi C sig ! handler_pc"
+ by auto
+ then obtain ST' LT' where
+ phi': "phi C sig ! handler_pc = Some (ST',LT')" and
+ less: "G \<turnstile> ([Class D], LT) <=s (ST',LT')"
+ by auto
+
+ from cr' phi meth f'
+ have "correct_frame G hp (ST, LT) maxl ins f'"
+ by (unfold correct_state_def) auto
+ then obtain
+ len: "length loc = 1+length (snd sig)+maxl" and
+ loc: "approx_loc G hp loc LT"
+ by (unfold correct_frame_def) auto
+
+ let ?f = "([xcp], loc, C, sig, handler_pc)"
+ have "correct_frame G hp (ST', LT') maxl ins ?f"
+ proof -
+ from wf less loc
+ have "approx_loc G hp loc LT'" by (simp add: sup_state_conv) blast
+ moreover
+ from D adr hp
+ have "G,hp \<turnstile> xcp ::\<preceq> Class D" by (simp add: conf_def obj_ty_def)
+ with wf less loc
+ have "approx_stk G hp [xcp] ST'"
+ by (auto simp add: sup_state_conv approx_stk_def approx_val_def
+ elim: conf_widen split: Err.split)
+ moreover
+ note len pc
+ ultimately
+ show ?thesis by (simp add: correct_frame_def)
+ qed
+
+ with cr' match phi' meth
+ show ?thesis by (unfold correct_state_def) auto
+ qed
+qed
+
+
+text {*
+ The requirement of lemma @{text uncaught_xcpt_correct} (that
+ the exception is a valid reference on the heap) is always met
+ for welltyped instructions and conformant states:
+*}
+lemma exec_instr_xcpt_hp:
+ "[| fst (exec_instr (ins!pc) G hp stk vars Cl sig pc frs) = Some xcp;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+ ==> \<exists>adr T. xcp = Addr adr \<and> hp adr = Some T"
+ (is "[| ?xcpt; ?wt; ?correct |] ==> ?thesis")
+proof -
+ note [simp] = system_xcpt_allocated split_beta raise_system_xcpt_def
+ note [split] = split_if_asm option.split_asm
+
+ assume wt: ?wt ?correct
+
+ assume xcpt: ?xcpt
+ thus ?thesis
+ proof (cases "ins!pc")
+ case New with xcpt
+ show ?thesis by (auto dest: new_Addr_OutOfMemory)
+ next
+ case Throw with xcpt wt
+ show ?thesis
+ by (auto simp add: wt_instr_def correct_state_def correct_frame_def
+ dest: non_npD)
+ qed auto
+qed
+
+
+text {*
+ Finally we can state that, whenever an exception occurs, the
+ resulting next state always conforms:
+*}
+lemma xcpt_correct:
+ "[| wt_jvm_prog G phi;
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
+ fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = Some xcp;
+ 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> |]
+ ==> G,phi \<turnstile>JVM state'\<surd>"
+proof -
+ assume wtp: "wt_jvm_prog G phi"
+ assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
+ assume wt: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
+ assume xp: "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = Some xcp"
+ assume s': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
+ assume correct: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
+
+ from wtp obtain wfmb where wf: "wf_prog wfmb G" by (simp add: wt_jvm_prog_def)
+
+ note xp' = meth s' xp
+
+ note wtp
+ moreover
+ from xp wt correct
+ obtain adr T where
+ adr: "xcp = Addr adr" "hp adr = Some T"
+ by (blast dest: exec_instr_xcpt_hp)
+ moreover
+ note correct
+ ultimately
+ have "G,phi \<turnstile>JVM find_handler G (Some xcp) hp frs \<surd>" by (rule uncaught_xcpt_correct)
+ with xp'
+ have "match_exception_table G (cname_of hp xcp) pc et = None \<Longrightarrow> ?thesis"
+ (is "?m (cname_of hp xcp) = _ \<Longrightarrow> _" is "?match = _ \<Longrightarrow> _")
+ by (clarsimp simp add: exec_instr_xcpt split_beta)
+ moreover
+ { fix handler
+ assume some_handler: "?match = Some handler"
+
+ from correct meth
+ obtain ST LT where
+ hp_ok: "G \<turnstile>h hp \<surd>" and
+ class: "is_class G C" and
+ phi_pc: "phi C sig ! pc = Some (ST, LT)" and
+ frame: "correct_frame G hp (ST, LT) maxl ins (stk, loc, C, sig, pc)" and
+ frames: "correct_frames G hp phi rT sig frs"
+ by (unfold correct_state_def) auto
+
+ from frame obtain
+ stk: "approx_stk G hp stk ST" and
+ loc: "approx_loc G hp loc LT" and
+ pc: "pc < length ins" and
+ len: "length loc = 1+length (snd sig)+maxl"
+ by (unfold correct_frame_def) auto
+
+ from wt obtain
+ eff: "\<forall>(pc', s')\<in>set (xcpt_eff (ins!pc) G pc (phi C sig!pc) et).
+ pc' < length ins \<and> G \<turnstile> s' <=' phi C sig!pc'"
+ by (simp add: wt_instr_def eff_def)
+
+ from some_handler xp'
+ have state':
+ "state' = (None, hp, ([xcp], loc, C, sig, handler)#frs)"
+ by (cases "ins!pc", auto simp add: raise_system_xcpt_def split_beta
+ split: split_if_asm) (* takes long! *)
+
+ let ?f' = "([xcp], loc, C, sig, handler)"
+ from eff
+ obtain ST' LT' where
+ phi_pc': "phi C sig ! handler = Some (ST', LT')" and
+ frame': "correct_frame G hp (ST',LT') maxl ins ?f'"
+ proof (cases "ins!pc")
+ case Return -- "can't generate exceptions:"
+ with xp' have False by (simp add: split_beta split: split_if_asm)
+ thus ?thesis ..
+ next
+ case New
+ with some_handler xp'
+ have xcp: "xcp = Addr (XcptRef OutOfMemory)"
+ by (simp add: raise_system_xcpt_def split_beta new_Addr_OutOfMemory)
+ hence "cname_of hp xcp = Xcpt OutOfMemory"
+ by (simp add: system_xcpt_allocated)
+ with New some_handler phi_pc eff
+ obtain ST' LT' where
+ phi': "phi C sig ! handler = Some (ST', LT')" and
+ less: "G \<turnstile> ([Class (Xcpt OutOfMemory)], LT) <=s (ST', LT')" and
+ pc': "handler < length ins"
+ by (simp add: xcpt_eff_def) blast
+ note phi'
+ moreover
+ { from xcp
+ have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt OutOfMemory)"
+ by (simp add: conf_def obj_ty_def system_xcpt_allocated)
+ moreover
+ from wf less loc
+ have "approx_loc G hp loc LT'"
+ by (simp add: sup_state_conv) blast
+ moreover
+ note wf less pc' len
+ ultimately
+ have "correct_frame G hp (ST',LT') maxl ins ?f'"
+ by (unfold correct_frame_def) (auto simp add: sup_state_conv
+ approx_stk_def approx_val_def split: err.split elim: conf_widen)
+ }
+ ultimately
+ show ?thesis by (rule that)
+ next
+ case Getfield
+ with some_handler xp'
+ have xcp: "xcp = Addr (XcptRef NullPointer)"
+ by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
+ hence "cname_of hp xcp = Xcpt NullPointer"
+ by (simp add: system_xcpt_allocated)
+ with Getfield some_handler phi_pc eff
+ obtain ST' LT' where
+ phi': "phi C sig ! handler = Some (ST', LT')" and
+ less: "G \<turnstile> ([Class (Xcpt NullPointer)], LT) <=s (ST', LT')" and
+ pc': "handler < length ins"
+ by (simp add: xcpt_eff_def) blast
+ note phi'
+ moreover
+ { from xcp
+ have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt NullPointer)"
+ by (simp add: conf_def obj_ty_def system_xcpt_allocated)
+ moreover
+ from wf less loc
+ have "approx_loc G hp loc LT'"
+ by (simp add: sup_state_conv) blast
+ moreover
+ note wf less pc' len
+ ultimately
+ have "correct_frame G hp (ST',LT') maxl ins ?f'"
+ by (unfold correct_frame_def) (auto simp add: sup_state_conv
+ approx_stk_def approx_val_def split: err.split elim: conf_widen)
+ }
+ ultimately
+ show ?thesis by (rule that)
+ next
+ case Putfield
+ with some_handler xp'
+ have xcp: "xcp = Addr (XcptRef NullPointer)"
+ by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
+ hence "cname_of hp xcp = Xcpt NullPointer"
+ by (simp add: system_xcpt_allocated)
+ with Putfield some_handler phi_pc eff
+ obtain ST' LT' where
+ phi': "phi C sig ! handler = Some (ST', LT')" and
+ less: "G \<turnstile> ([Class (Xcpt NullPointer)], LT) <=s (ST', LT')" and
+ pc': "handler < length ins"
+ by (simp add: xcpt_eff_def) blast
+ note phi'
+ moreover
+ { from xcp
+ have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt NullPointer)"
+ by (simp add: conf_def obj_ty_def system_xcpt_allocated)
+ moreover
+ from wf less loc
+ have "approx_loc G hp loc LT'"
+ by (simp add: sup_state_conv) blast
+ moreover
+ note wf less pc' len
+ ultimately
+ have "correct_frame G hp (ST',LT') maxl ins ?f'"
+ by (unfold correct_frame_def) (auto simp add: sup_state_conv
+ approx_stk_def approx_val_def split: err.split elim: conf_widen)
+ }
+ ultimately
+ show ?thesis by (rule that)
+ next
+ case Checkcast
+ with some_handler xp'
+ have xcp: "xcp = Addr (XcptRef ClassCast)"
+ by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
+ hence "cname_of hp xcp = Xcpt ClassCast"
+ by (simp add: system_xcpt_allocated)
+ with Checkcast some_handler phi_pc eff
+ obtain ST' LT' where
+ phi': "phi C sig ! handler = Some (ST', LT')" and
+ less: "G \<turnstile> ([Class (Xcpt ClassCast)], LT) <=s (ST', LT')" and
+ pc': "handler < length ins"
+ by (simp add: xcpt_eff_def) blast
+ note phi'
+ moreover
+ { from xcp
+ have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt ClassCast)"
+ by (simp add: conf_def obj_ty_def system_xcpt_allocated)
+ moreover
+ from wf less loc
+ have "approx_loc G hp loc LT'"
+ by (simp add: sup_state_conv) blast
+ moreover
+ note wf less pc' len
+ ultimately
+ have "correct_frame G hp (ST',LT') maxl ins ?f'"
+ by (unfold correct_frame_def) (auto simp add: sup_state_conv
+ approx_stk_def approx_val_def split: err.split elim: conf_widen)
+ }
+ ultimately
+ show ?thesis by (rule that)
+ next
+ case Invoke
+ with phi_pc eff
+ have
+ "\<forall>D\<in>set (match_any G pc et).
+ the (?m D) < length ins \<and> G \<turnstile> Some ([Class D], LT) <=' phi C sig!the (?m D)"
+ by (simp add: xcpt_eff_def)
+ moreover
+ from some_handler
+ obtain D where
+ "D \<in> set (match_any G pc et)" and
+ D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and
+ "?m D = Some handler"
+ by (blast dest: in_match_any)
+ ultimately
+ obtain
+ pc': "handler < length ins" and
+ "G \<turnstile> Some ([Class D], LT) <=' phi C sig ! handler"
+ by auto
+ then
+ obtain ST' LT' where
+ phi': "phi C sig ! handler = Some (ST', LT')" and
+ less: "G \<turnstile> ([Class D], LT) <=s (ST', LT')"
+ by auto
+ from xp wt correct
+ obtain addr T where
+ xcp: "xcp = Addr addr" "hp addr = Some T"
+ by (blast dest: exec_instr_xcpt_hp)
+ note phi'
+ moreover
+ { from xcp D
+ have "G,hp \<turnstile> xcp ::\<preceq> Class D"
+ by (simp add: conf_def obj_ty_def)
+ moreover
+ from wf less loc
+ have "approx_loc G hp loc LT'"
+ by (simp add: sup_state_conv) blast
+ moreover
+ note wf less pc' len
+ ultimately
+ have "correct_frame G hp (ST',LT') maxl ins ?f'"
+ by (unfold correct_frame_def) (auto simp add: sup_state_conv
+ approx_stk_def approx_val_def split: err.split elim: conf_widen)
+ }
+ ultimately
+ show ?thesis by (rule that)
+ next
+ case Throw
+ with phi_pc eff
+ have
+ "\<forall>D\<in>set (match_any G pc et).
+ the (?m D) < length ins \<and> G \<turnstile> Some ([Class D], LT) <=' phi C sig!the (?m D)"
+ by (simp add: xcpt_eff_def)
+ moreover
+ from some_handler
+ obtain D where
+ "D \<in> set (match_any G pc et)" and
+ D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and
+ "?m D = Some handler"
+ by (blast dest: in_match_any)
+ ultimately
+ obtain
+ pc': "handler < length ins" and
+ "G \<turnstile> Some ([Class D], LT) <=' phi C sig ! handler"
+ by auto
+ then
+ obtain ST' LT' where
+ phi': "phi C sig ! handler = Some (ST', LT')" and
+ less: "G \<turnstile> ([Class D], LT) <=s (ST', LT')"
+ by auto
+ from xp wt correct
+ obtain addr T where
+ xcp: "xcp = Addr addr" "hp addr = Some T"
+ by (blast dest: exec_instr_xcpt_hp)
+ note phi'
+ moreover
+ { from xcp D
+ have "G,hp \<turnstile> xcp ::\<preceq> Class D"
+ by (simp add: conf_def obj_ty_def)
+ moreover
+ from wf less loc
+ have "approx_loc G hp loc LT'"
+ by (simp add: sup_state_conv) blast
+ moreover
+ note wf less pc' len
+ ultimately
+ have "correct_frame G hp (ST',LT') maxl ins ?f'"
+ by (unfold correct_frame_def) (auto simp add: sup_state_conv
+ approx_stk_def approx_val_def split: err.split elim: conf_widen)
+ }
+ ultimately
+ show ?thesis by (rule that)
+ qed (insert xp', auto) -- "the other instructions don't generate exceptions"
+
+ from state' meth hp_ok class frames phi_pc' frame'
+ have ?thesis by (unfold correct_state_def) simp
+ }
+ ultimately
+ show ?thesis by (cases "?match") blast+
+qed
+
+
+
section {* Single Instructions *}
+text {*
+ In this section we look at each single (welltyped) instruction, and
+ prove that the state after execution of the instruction still conforms.
+ Since we have already handled exceptions above, we can now assume, that
+ on exception occurs for this (single step) execution.
+*}
+
lemmas [iff] = not_Err_eq
lemma Load_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = Load idx;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (blast intro: approx_loc_imp_approx_val_sup)
@@ -44,9 +596,9 @@
lemma Store_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = Store idx;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -57,9 +609,9 @@
lemma LitPush_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = LitPush v;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -81,30 +633,33 @@
apply (auto intro: rtrancl_trans)
done
+lemmas defs1 = defs1 raise_system_xcpt_def
lemma Checkcast_correct:
-"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+"[| wt_jvm_prog G phi;
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = Checkcast D;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
+ fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |]
==> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def)
+apply (clarsimp simp add: defs1 wt_jvm_prog_def map_eq_Cons split: split_if_asm)
apply (blast intro: Cast_conf2)
done
lemma Getfield_correct:
-"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+"[| wt_jvm_prog G phi;
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = Getfield F D;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
+ fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |]
==> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons
- split: option.split)
+apply (clarsimp simp add: defs1 map_eq_Cons wt_jvm_prog_def
+ split: option.split split_if_asm)
apply (frule conf_widen)
apply assumption+
apply (drule conf_RefTD)
@@ -112,19 +667,30 @@
apply (rule conjI)
apply (drule widen_cfs_fields)
apply assumption+
- apply (force intro: conf_widen simp add: hconf_def oconf_def lconf_def)
+ apply (erule conf_widen)
+ prefer 2
+ apply assumption
+ apply (simp add: hconf_def oconf_def lconf_def)
+ apply (elim allE)
+ apply (erule impE, assumption)
+ apply simp
+ apply (elim allE)
+ apply (erule impE, assumption)
+ apply clarsimp
apply blast
done
+
lemma Putfield_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = Putfield F D;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
+ fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |]
==> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 raise_xcpt_def split: option.split List.split)
+apply (clarsimp simp add: defs1 split_beta split: option.split List.split split_if_asm)
apply (frule conf_widen)
prefer 2
apply assumption
@@ -140,22 +706,25 @@
dest:
widen_cfs_fields)
done
+
lemma New_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = New X;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
+ fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |]
==> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wf: "wf_prog wt G"
- assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins)"
+ assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
assume ins: "ins!pc = New X"
- assume wt: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc"
+ assume wt: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
assume exec: "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
assume conf: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
+ assume no_x: "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None"
from ins conf meth
obtain ST LT where
@@ -169,75 +738,68 @@
from phi_pc ins wt
obtain ST' LT' where
is_class_X: "is_class G X" and
+ maxs: "length ST < maxs" and
suc_pc: "Suc pc < length ins" and
phi_suc: "phi C sig ! Suc pc = Some (ST', LT')" and
less: "G \<turnstile> (Class X # ST, LT) <=s (ST', LT')"
- by (unfold wt_instr_def step_def) auto
+ by (unfold wt_instr_def eff_def norm_eff_def) auto
obtain oref xp' where
- new_Addr: "(oref,xp') = new_Addr hp"
- by (cases "new_Addr hp") auto
- hence cases:
- "hp oref = None \<and> xp' = None \<or> xp' = Some OutOfMemory"
- by (blast dest: new_AddrD)
+ new_Addr: "new_Addr hp = (oref,xp')"
+ by (cases "new_Addr hp")
+ with ins no_x
+ obtain hp: "hp oref = None" and "xp' = None"
+ by (auto dest: new_AddrD simp add: raise_system_xcpt_def)
+
+ with exec ins meth new_Addr
+ have state':
+ "state' = Norm (hp(oref\<mapsto>(X, init_vars (fields (G, X)))),
+ (Addr oref # stk, loc, C, sig, Suc pc) # frs)"
+ (is "state' = Norm (?hp', ?f # frs)")
+ by simp
moreover
- { assume "xp' = Some OutOfMemory"
- with exec ins meth new_Addr [symmetric]
- have "state' = (Some OutOfMemory, hp, (stk,loc,C,sig,Suc pc)#frs)" by simp
- hence ?thesis by (simp add: correct_state_def)
- }
+ from wf hp heap_ok is_class_X
+ have hp': "G \<turnstile>h ?hp' \<surd>"
+ by - (rule hconf_newref, auto simp add: oconf_def dest: fields_is_type)
moreover
- { assume hp: "hp oref = None" and "xp' = None"
- with exec ins meth new_Addr [symmetric]
- have state':
- "state' = Norm (hp(oref\<mapsto>(X, init_vars (fields (G, X)))),
- (Addr oref # stk, loc, C, sig, Suc pc) # frs)"
- (is "state' = Norm (?hp', ?f # frs)")
- by simp
- moreover
- from wf hp heap_ok is_class_X
- have hp': "G \<turnstile>h ?hp' \<surd>"
- by - (rule hconf_newref,
- auto simp add: oconf_def dest: fields_is_type)
- moreover
- from hp
- have sup: "hp \<le>| ?hp'" by (rule hext_new)
- from hp frame less suc_pc wf
- have "correct_frame G ?hp' (ST', LT') maxl ins ?f"
- apply (unfold correct_frame_def sup_state_conv)
- apply (clarsimp simp add: map_eq_Cons conf_def fun_upd_apply approx_val_def)
- apply (blast intro: approx_stk_sup_heap approx_loc_sup_heap sup)
- done
- moreover
- from hp frames wf heap_ok is_class_X
- have "correct_frames G ?hp' phi rT sig frs"
- by - (rule correct_frames_newref,
- auto simp add: oconf_def dest: fields_is_type)
- ultimately
- have ?thesis
- by (simp add: is_class_C meth phi_suc correct_state_def del: not_None_eq)
- }
+ from hp
+ have sup: "hp \<le>| ?hp'" by (rule hext_new)
+ from hp frame less suc_pc wf
+ have "correct_frame G ?hp' (ST', LT') maxl ins ?f"
+ apply (unfold correct_frame_def sup_state_conv)
+ apply (clarsimp simp add: map_eq_Cons conf_def fun_upd_apply approx_val_def)
+ apply (blast intro: approx_stk_sup_heap approx_loc_sup_heap sup)
+ done
+ moreover
+ from hp frames wf heap_ok is_class_X
+ have "correct_frames G ?hp' phi rT sig frs"
+ by - (rule correct_frames_newref,
+ auto simp add: oconf_def dest: fields_is_type)
ultimately
- show ?thesis by auto
+ show ?thesis
+ by (simp add: is_class_C meth phi_suc correct_state_def del: not_None_eq)
qed
lemmas [simp del] = split_paired_Ex
+
lemma Invoke_correct:
"[| wt_jvm_prog G phi;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Invoke C' mn pTs;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
+ fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |]
==> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wtprog: "wt_jvm_prog G phi"
- assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins)"
+ assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
assume ins: "ins ! pc = Invoke C' mn pTs"
- assume wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc"
+ assume wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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>"
+ assume no_xcp: "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None"
from wtprog
obtain wfmb where
@@ -262,18 +824,19 @@
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 del: not_None_eq) (elim exE conjE, rule that)
+ eff: "G \<turnstile> norm_eff (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc"
+ by (simp add: wt_instr_def eff_def del: not_None_eq)
+ (elim exE conjE, rule that)
- from step
+ from eff
obtain ST' LT' where
s': "phi C sig ! Suc pc = Some (ST', LT')"
- by (auto simp add: step_def split_paired_Ex)
+ by (simp add: norm_eff_def split_paired_Ex) blast
- from X
+ from X
obtain T where
X_Ref: "X = RefT T"
- by (blast dest: widen_RefT2)
+ by - (drule widen_RefT2, erule exE, rule that)
from s ins frame
obtain
@@ -289,194 +852,245 @@
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 (auto dest: approx_stk_append)
+ "length stk' = length ST"
+ by - (drule approx_stk_append, auto)
- 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"
- by (auto dest: widen_RefT2)
+ from oX X_Ref
+ have oX_conf: "G,hp \<turnstile> oX ::\<preceq> RefT T"
+ by (simp add: approx_val_def)
from stk' l_o l
have oX_pos: "last (take (Suc (length pTs)) stk) = oX" by simp
- with state' method ins
- have Null_ok: "oX = Null ==> ?thesis"
- by (simp add: correct_state_def raise_xcpt_def)
-
- { fix ref assume oX_Addr: "oX = Addr ref"
-
- with oX_Ref
- obtain obj where
- loc: "hp ref = Some obj" "obj_ty obj = RefT T'"
- by auto
-
- 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 (blast dest: widen_Class)
-
- with X
- have X'_subcls: "G \<turnstile> X' \<preceq>C C'"
- by simp
-
- with mC' wfprog
- obtain D0 rT0 maxs0 maxl0 ins0 where
- mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxs0, maxl0, ins0)" "G\<turnstile>rT0\<preceq>rT"
- by (fast dest: subtype_widen_methd)
+ with state' method ins no_xcp oX_conf
+ obtain ref where oX_Addr: "oX = Addr ref"
+ by (auto simp add: raise_system_xcpt_def dest: conf_RefTD)
- from X' D
- have D_subcls: "G \<turnstile> D \<preceq>C X'"
- by simp
-
- with wfprog mX
- obtain D'' rT' mxs' mxl' ins' where
- mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxs', mxl', ins')"
- "G \<turnstile> rT' \<preceq> rT0"
- by (fast dest: subtype_widen_methd)
-
- from mX mD
- have rT': "G \<turnstile> rT' \<preceq> rT"
- by - (rule widen_trans)
-
- from is_class X'_subcls D_subcls
- have is_class_D: "is_class G D"
- by (auto dest: subcls_is_class2)
+ with oX_conf X_Ref
+ obtain obj D where
+ loc: "hp ref = Some obj" and
+ obj_ty: "obj_ty obj = Class D" and
+ D: "G \<turnstile> Class D \<preceq> X"
+ by (auto simp add: conf_def) blast
+
+ with X_Ref obtain X' where X': "X = Class X'"
+ by (blast dest: widen_Class)
+
+ with X have X'_subcls: "G \<turnstile> X' \<preceq>C C'" by simp
- with mD wfprog
- obtain mD'':
- "method (G, D'') (mn, pTs) = Some (D'', rT', mxs', 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)
+ with mC' wfprog
+ obtain D0 rT0 maxs0 maxl0 ins0 et0 where
+ mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxs0, maxl0, ins0, et0)" "G\<turnstile>rT0\<preceq>rT"
+ by (auto dest: subtype_widen_methd intro: that)
- 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_conv)
+ from X' D have D_subcls: "G \<turnstile> D \<preceq>C X'" by simp
+
+ with wfprog mX
+ obtain D'' rT' mxs' mxl' ins' et' where
+ mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')"
+ "G \<turnstile> rT' \<preceq> rT0"
+ by (auto dest: subtype_widen_methd intro: that)
+
+ from mX mD have rT': "G \<turnstile> rT' \<preceq> rT" by - (rule widen_trans)
+
+ from is_class X'_subcls D_subcls
+ have is_class_D: "is_class G D" by (auto dest: subcls_is_class2)
+
+ with mD wfprog
+ obtain mD'':
+ "method (G, D'') (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')"
+ "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)
- 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_conv)
-
- 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 is_class_D
- 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 opTs w l l_o wfprog
- have "approx_stk G hp opTs (rev pTs)"
- by (auto elim!: approx_stk_all_widen simp add: zip_rev)
- hence "approx_stk G hp (rev opTs) pTs" by (subst approx_stk_rev)
+ with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD no_xcp
+ have state'_val:
+ "state' =
+ Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' arbitrary,
+ D'', (mn, pTs), 0) # (opTs @ Addr ref # stk', loc, C, sig, pc) # frs)"
+ (is "state' = Norm (hp, ?f # ?f' # frs)")
+ by (simp add: raise_system_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_conv)
- 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)
+ 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_conv)
- from this sup_loc wfprog
- have "approx_loc G hp ?lt LT0" by (rule approx_loc_widen)
- with start l_o l
- show ?thesis by (simp add: correct_frame_def)
- qed
+ have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)"
+ by (simp add: approx_loc_def list_all2_def set_replicate_conv_if)
+
+ from wfprog mD is_class_D
+ 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)
- 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_conv)
- with wfprog a_loc
- have a: "approx_loc G hp loc LT'"
- by - (rule approx_loc_widen)
- 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_conv map_eq_Cons)
- with wfprog a_stk'
- have "approx_stk G hp stk' (tl ST')"
- by - (rule approx_stk_widen)
- ultimately
- show ?thesis by (simp add: correct_frame_def suc_l pc)
- qed
+ from opTs w l l_o wfprog
+ have "approx_stk G hp opTs (rev pTs)"
+ by (auto elim!: approx_stk_all_widen simp add: zip_rev)
+ hence "approx_stk G hp (rev opTs) pTs" by (subst 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)
- with state'_val heap_ok mD'' ins method phi_pc s X' l
- frames s' LT0 c_f c_f' is_class_C
- have ?thesis by (simp add: correct_state_def) (intro exI conjI, blast)
- }
-
- with Null_ok oX_Ref
- show "G,phi \<turnstile>JVM state'\<surd>" by (cases oX) auto
+ from this sup_loc wfprog
+ have "approx_loc G hp ?lt LT0" by (rule approx_loc_widen)
+ with start l_o l
+ show ?thesis by (simp add: correct_frame_def)
+ qed
+
+ from state'_val heap_ok mD'' ins method phi_pc s X' l mX
+ frames s' LT0 c_f is_class_C stk' oX_Addr frame
+ show ?thesis by (simp add: correct_state_def) (intro exI conjI, blast)
qed
lemmas [simp del] = map_append
lemma Return_correct:
"[| wt_jvm_prog G phi;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Return;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm iff del: not_None_eq)
-apply (frule wt_jvm_prog_impl_wt_instr)
-apply (assumption, assumption, erule Suc_lessD)
-apply (clarsimp simp add: map_eq_Cons append_eq_conv_conj defs1)
-apply (unfold wt_jvm_prog_def)
-apply (frule subcls_widen_methd, assumption+)
-apply clarify
-apply simp
-apply (erule conf_widen, assumption)
-apply (erule widen_trans)+
-apply blast
-done
+proof -
+ assume wt_prog: "wt_jvm_prog G phi"
+ assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
+ assume ins: "ins ! pc = Return"
+ assume wt: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
+ assume s': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
+ assume correct: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
+
+ from wt_prog
+ obtain wfmb where wf: "wf_prog wfmb G" by (simp add: wt_jvm_prog_def)
+
+ from meth ins s'
+ have "frs = [] \<Longrightarrow> ?thesis" by (simp add: correct_state_def)
+ moreover
+ { fix f frs'
+ assume frs': "frs = f#frs'"
+ moreover
+ obtain stk' loc' C' sig' pc' where
+ f: "f = (stk',loc',C',sig',pc')" by (cases f)
+ moreover
+ obtain mn pt where
+ sig: "sig = (mn,pt)" by (cases sig)
+ moreover
+ note meth ins s'
+ ultimately
+ have state':
+ "state' = (None,hp,(hd stk#(drop (1+length pt) stk'),loc',C',sig',pc'+1)#frs')"
+ (is "state' = (None,hp,?f'#frs')")
+ by simp
+
+ from correct meth
+ obtain ST LT where
+ hp_ok: "G \<turnstile>h hp \<surd>" and
+ phi_pc: "phi C sig ! pc = Some (ST, LT)" and
+ frame: "correct_frame G hp (ST, LT) maxl ins (stk,loc,C,sig,pc)" and
+ frames: "correct_frames G hp phi rT sig frs"
+ by (simp add: correct_state_def, clarify, blast)
+
+ from phi_pc ins wt
+ obtain T ST' where "ST = T # ST'" "G \<turnstile> T \<preceq> rT"
+ by (simp add: wt_instr_def) blast
+ with wf frame
+ have hd_stk: "G,hp \<turnstile> (hd stk) ::\<preceq> rT"
+ by (auto simp add: correct_frame_def elim: conf_widen)
+ from f frs' frames sig
+ obtain apTs ST0' ST' LT' D D' D'' rT' rT'' maxs' maxl' ins' et' body where
+ phi': "phi C' sig' ! pc' = Some (ST',LT')" and
+ class': "is_class G C'" and
+ meth': "method (G,C') sig' = Some (C',rT',maxs',maxl',ins',et')" and
+ ins': "ins' ! pc' = Invoke D' mn pt" and
+ frame': "correct_frame G hp (ST', LT') maxl' ins' f" and
+ frames':"correct_frames G hp phi rT' sig' frs'" and
+ rT'': "G \<turnstile> rT \<preceq> rT''" and
+ meth'': "method (G, D) sig = Some (D'', rT'', body)" and
+ ST0': "ST' = rev apTs @ Class D # ST0'" and
+ len': "length apTs = length pt"
+ by clarsimp blast
+
+ from f frame'
+ obtain
+ stk': "approx_stk G hp stk' ST'" and
+ loc': "approx_loc G hp loc' LT'" and
+ pc': "pc' < length ins'" and
+ lloc':"length loc' = Suc (length (snd sig') + maxl')"
+ by (simp add: correct_frame_def)
+
+ from wt_prog class' meth' pc'
+ have "wt_instr (ins'!pc') G rT' (phi C' sig') maxs' (length ins') et' pc'"
+ by (rule wt_jvm_prog_impl_wt_instr)
+ with ins' phi' sig
+ obtain apTs ST0 X ST'' LT'' body' rT0 mD where
+ phi_suc: "phi C' sig' ! Suc pc' = Some (ST'', LT'')" and
+ ST0: "ST' = rev apTs @ X # ST0" and
+ len: "length apTs = length pt" and
+ less: "G \<turnstile> (rT0 # ST0, LT') <=s (ST'', LT'')" and
+ methD': "method (G, D') sig = Some (mD, rT0, body')" and
+ lessD': "G \<turnstile> X \<preceq> Class D'" and
+ suc_pc': "Suc pc' < length ins'"
+ by (clarsimp simp add: wt_instr_def eff_def norm_eff_def) blast
+
+ from len len' ST0 ST0'
+ have "X = Class D" by simp
+ with lessD'
+ have "G \<turnstile> D \<preceq>C D'" by simp
+ moreover
+ note wf meth'' methD'
+ ultimately
+ have "G \<turnstile> rT'' \<preceq> rT0" by (auto dest: subcls_widen_methd)
+ with wf hd_stk rT''
+ have hd_stk': "G,hp \<turnstile> (hd stk) ::\<preceq> rT0" by (auto elim: conf_widen widen_trans)
+
+ have frame'':
+ "correct_frame G hp (ST'',LT'') maxl' ins' ?f'"
+ proof -
+ from wf hd_stk' len stk' less ST0
+ have "approx_stk G hp (hd stk # drop (1+length pt) stk') ST''"
+ by (auto simp add: map_eq_Cons sup_state_conv
+ dest!: approx_stk_append elim: conf_widen)
+ moreover
+ from wf loc' less
+ have "approx_loc G hp loc' LT''" by (simp add: sup_state_conv) blast
+ moreover
+ note suc_pc' lloc'
+ ultimately
+ show ?thesis by (simp add: correct_frame_def)
+ qed
+
+ with state' frs' f meth hp_ok hd_stk phi_suc frames' meth' phi' class'
+ have ?thesis by (simp add: correct_state_def)
+ }
+ ultimately
+ show ?thesis by (cases frs) blast+
+qed
+
lemmas [simp] = map_append
lemma Goto_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Goto branch;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -487,9 +1101,9 @@
lemma Ifcmpeq_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Ifcmpeq branch;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -499,9 +1113,9 @@
lemma Pop_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Pop;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -511,9 +1125,9 @@
lemma Dup_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Dup;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -523,9 +1137,9 @@
lemma Dup_x1_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Dup_x1;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -535,9 +1149,9 @@
lemma Dup_x2_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Dup_x2;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -547,9 +1161,9 @@
lemma Swap_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Swap;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -559,9 +1173,9 @@
lemma IAdd_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = IAdd;
- wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -569,29 +1183,51 @@
apply blast
done
+lemma Throw_correct:
+"[| wf_prog wt G;
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
+ ins ! pc = Throw;
+ 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>;
+ fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |]
+==> G,phi \<turnstile>JVM state'\<surd>"
+ by simp
-lemma instr_correct:
+
+text {*
+ The next theorem collects the results of the sections above,
+ i.e.~exception handling and the execution step for each
+ instruction. It states type safety for single step execution:
+ in welltyped programs, a conforming state is transformed
+ into another conforming state when one instruction is executed.
+*}
+theorem instr_correct:
"[| wt_jvm_prog G phi;
- method (G,C) sig = Some (C,rT,maxs,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
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> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (frule wt_jvm_prog_impl_wt_instr_cor)
apply assumption+
+apply (cases "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs)")
+defer
+apply (erule xcpt_correct, assumption+)
apply (cases "ins!pc")
prefer 8
apply (rule Invoke_correct, assumption+)
prefer 8
apply (rule Return_correct, assumption+)
+prefer 5
+apply (rule Getfield_correct, assumption+)
+prefer 6
+apply (rule Checkcast_correct, assumption+)
apply (unfold wt_jvm_prog_def)
apply (rule Load_correct, assumption+)
apply (rule Store_correct, assumption+)
apply (rule LitPush_correct, assumption+)
apply (rule New_correct, assumption+)
-apply (rule Getfield_correct, assumption+)
apply (rule Putfield_correct, assumption+)
-apply (rule Checkcast_correct, assumption+)
apply (rule Pop_correct, assumption+)
apply (rule Dup_correct, assumption+)
apply (rule Dup_x1_correct, assumption+)
@@ -600,6 +1236,7 @@
apply (rule IAdd_correct, assumption+)
apply (rule Goto_correct, assumption+)
apply (rule Ifcmpeq_correct, assumption+)
+apply (rule Throw_correct, assumption+)
done
section {* Main *}
@@ -627,9 +1264,10 @@
done
+
lemma L0:
"[| xp=None; frs\<noteq>[] |] ==> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
-by (clarsimp simp add: neq_Nil_conv simp del: split_paired_Ex)
+by (clarsimp simp add: neq_Nil_conv split_beta)
lemma L1:
"[|wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]|]
@@ -639,7 +1277,6 @@
apply (fast intro: BV_correct_1)
done
-
theorem BV_correct [rule_format]:
"[| wt_jvm_prog G phi; G \<turnstile> s -jvm-> t |] ==> G,phi \<turnstile>JVM s\<surd> --> G,phi \<turnstile>JVM t\<surd>"
apply (unfold exec_all_def)
@@ -648,12 +1285,11 @@
apply (auto intro: BV_correct_1)
done
-
theorem BV_correct_initial:
"[| wt_jvm_prog G phi;
G \<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>|]
-==> approx_stk G hp stk (fst (the (((phi C) sig) ! pc))) \<and>
- approx_loc G hp loc (snd (the (((phi C) sig) ! pc)))"
+==> 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
--- a/src/HOL/MicroJava/BV/Correct.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Sun Dec 16 00:17:44 2001 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/MicroJava/BV/Correct.thy
ID: $Id$
- Author: Cornelia Pusch
+ Author: Cornelia Pusch, Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
The invariant for the type safety proof.
@@ -10,12 +10,6 @@
theory Correct = BVSpec:
-lemma list_all2_rev [simp]:
- "list_all2 P (rev l) (rev l') = list_all2 P l l'"
- apply (unfold list_all2_def)
- apply (simp add: zip_rev cong: conj_cong)
- done
-
constdefs
approx_val :: "[jvm_prog,aheap,val,ty err] => bool"
"approx_val G h v any == case any of Err => True | OK T => G,h\<turnstile>v::\<preceq>T"
@@ -39,19 +33,19 @@
"correct_frames G hp phi rT0 sig0 (f#frs) =
(let (stk,loc,C,sig,pc) = f in
- (\<exists>ST LT rT maxs maxl ins.
+ (\<exists>ST LT rT maxs maxl ins et.
phi C sig ! pc = Some (ST,LT) \<and> is_class G C \<and>
- method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \<and>
- (\<exists>C' mn pTs k. pc = k+1 \<and> ins!k = (Invoke C' mn pTs) \<and>
+ method (G,C) sig = Some(C,rT,(maxs,maxl,ins,et)) \<and>
+ (\<exists>C' mn pTs. ins!pc = (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>
+ (phi C sig)!pc = Some ((rev apTs) @ (Class D) # ST', LT') \<and>
length apTs = length pTs \<and>
- (\<exists>D' rT' maxs' maxl' ins'.
- method (G,D) sig0 = Some(D',rT',(maxs',maxl',ins')) \<and>
+ (\<exists>D' rT' maxs' maxl' ins' et'.
+ method (G,D) sig0 = Some(D',rT',(maxs',maxl',ins',et')) \<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))))"
+ correct_frame G hp (ST, LT) maxl ins f \<and>
+ correct_frames G hp phi rT sig frs))))"
constdefs
@@ -60,17 +54,17 @@
"correct_state G phi == \<lambda>(xp,hp,frs).
case xp of
None => (case frs of
- [] => True
+ [] => True
| (f#fs) => G\<turnstile>h hp\<surd> \<and>
- (let (stk,loc,C,sig,pc) = f
- in
- \<exists>rT maxs maxl ins s.
+ (let (stk,loc,C,sig,pc) = f
+ in
+ \<exists>rT maxs maxl ins et s.
is_class G C \<and>
- method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \<and>
+ method (G,C) sig = Some(C,rT,(maxs,maxl,ins,et)) \<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 => True"
+ correct_frame G hp s maxl ins f \<and>
+ correct_frames G hp phi rT sig fs))
+ | Some x => frs = []"
syntax (xsymbols)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Effect.thy Sun Dec 16 00:17:44 2001 +0100
@@ -0,0 +1,339 @@
+(* Title: HOL/MicroJava/BV/Effect.thy
+ ID: $Id$
+ Author: Gerwin Klein
+ Copyright 2000 Technische Universitaet Muenchen
+*)
+
+header {* Effect of Instructions on the State Type *}
+
+theory Effect = JVMType + JVMExec:
+
+types
+ succ_type = "(p_count \<times> state_type option) list"
+
+text {* Program counter of successor instructions: *}
+consts
+ succs :: "instr => p_count => p_count list"
+primrec
+ "succs (Load idx) pc = [pc+1]"
+ "succs (Store idx) pc = [pc+1]"
+ "succs (LitPush v) 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 = [pc]"
+ "succs (Invoke C mn fpTs) pc = [pc+1]"
+ "succs Throw pc = [pc]"
+
+text "Effect of instruction on the state type:"
+consts
+eff' :: "instr \<times> jvm_prog \<times> state_type => state_type"
+
+recdef eff' "{}"
+"eff' (Load idx, G, (ST, LT)) = (ok_val (LT ! idx) # ST, LT)"
+"eff' (Store idx, G, (ts#ST, LT)) = (ST, LT[idx:= OK ts])"
+"eff' (LitPush v, G, (ST, LT)) = (the (typeof (\<lambda>v. None) v) # ST, LT)"
+"eff' (Getfield F C, G, (oT#ST, LT)) = (snd (the (field (G,C) F)) # ST, LT)"
+"eff' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)"
+"eff' (New C, G, (ST,LT)) = (Class C # ST, LT)"
+"eff' (Checkcast C, G, (RefT rt#ST,LT)) = (Class C # ST,LT)"
+"eff' (Pop, G, (ts#ST,LT)) = (ST,LT)"
+"eff' (Dup, G, (ts#ST,LT)) = (ts#ts#ST,LT)"
+"eff' (Dup_x1, G, (ts1#ts2#ST,LT)) = (ts1#ts2#ts1#ST,LT)"
+"eff' (Dup_x2, G, (ts1#ts2#ts3#ST,LT)) = (ts1#ts2#ts3#ts1#ST,LT)"
+"eff' (Swap, G, (ts1#ts2#ST,LT)) = (ts2#ts1#ST,LT)"
+"eff' (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT))
+ = (PrimT Integer#ST,LT)"
+"eff' (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = (ST,LT)"
+"eff' (Goto b, G, s) = s"
+ -- "Return has no successor instruction in the same method"
+"eff' (Return, G, s) = s"
+ -- "Throw always terminates abruptly"
+"eff' (Throw, G, s) = s"
+"eff' (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))"
+
+
+consts
+ match_any :: "jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> cname list"
+primrec
+ "match_any G pc [] = []"
+ "match_any G pc (e#es) = (let (start_pc, end_pc, handler_pc, catch_type) = e;
+ es' = match_any G pc es
+ in
+ if start_pc <= pc \<and> pc < end_pc then catch_type#es' else es')"
+
+
+consts
+ xcpt_names :: "instr \<times> jvm_prog \<times> p_count \<times> exception_table => cname list"
+recdef xcpt_names "{}"
+ "xcpt_names (Getfield F C, G, pc, et) = [Xcpt NullPointer]"
+ "xcpt_names (Putfield F C, G, pc, et) = [Xcpt NullPointer]"
+ "xcpt_names (New C, G, pc, et) = [Xcpt OutOfMemory]"
+ "xcpt_names (Checkcast C, G, pc, et) = [Xcpt ClassCast]"
+ "xcpt_names (Throw, G, pc, et) = match_any G pc et"
+ "xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et"
+ "xcpt_names (i, G, pc, et) = []"
+
+
+constdefs
+ xcpt_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> state_type option \<Rightarrow> exception_table \<Rightarrow> succ_type"
+ "xcpt_eff i G pc s et ==
+ map (\<lambda>C. (the (match_exception_table G C pc et), case s of None \<Rightarrow> None | Some s' \<Rightarrow> Some ([Class C], snd s')))
+ (xcpt_names (i,G,pc,et))"
+
+ norm_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option"
+ "norm_eff i G == option_map (\<lambda>s. eff' (i,G,s))"
+
+ eff :: "instr => jvm_prog => p_count => exception_table => state_type option => succ_type"
+ "eff i G pc et s == (map (\<lambda>pc'. (pc',norm_eff i G s)) (succs i pc)) @ (xcpt_eff i G pc s et)"
+
+
+text "Conditions under which eff is applicable:"
+consts
+app' :: "instr \<times> jvm_prog \<times> nat \<times> ty \<times> state_type => bool"
+
+recdef app' "{}"
+"app' (Load idx, G, maxs, rT, s) = (idx < length (snd s) \<and>
+ (snd s) ! idx \<noteq> Err \<and>
+ length (fst s) < maxs)"
+"app' (Store idx, G, maxs, rT, (ts#ST, LT)) = (idx < length LT)"
+"app' (LitPush v, G, maxs, rT, s) = (length (fst s) < maxs \<and> typeof (\<lambda>t. None) v \<noteq> None)"
+"app' (Getfield F C, G, maxs, 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, maxs, 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, maxs, rT, s) = (is_class G C \<and> length (fst s) < maxs)"
+"app' (Checkcast C, G, maxs, rT, (RefT rt#ST,LT)) = (is_class G C)"
+"app' (Pop, G, maxs, rT, (ts#ST,LT)) = True"
+"app' (Dup, G, maxs, rT, (ts#ST,LT)) = (1+length ST < maxs)"
+"app' (Dup_x1, G, maxs, rT, (ts1#ts2#ST,LT)) = (2+length ST < maxs)"
+"app' (Dup_x2, G, maxs, rT, (ts1#ts2#ts3#ST,LT)) = (3+length ST < maxs)"
+"app' (Swap, G, maxs, rT, (ts1#ts2#ST,LT)) = True"
+"app' (IAdd, G, maxs, rT, (PrimT Integer#PrimT Integer#ST,LT))
+ = True"
+"app' (Ifcmpeq b, G, maxs, 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, maxs, rT, s) = True"
+"app' (Return, G, maxs, rT, (T#ST,LT)) = (G \<turnstile> T \<preceq> rT)"
+"app' (Throw, G, maxs, rT, (T#ST,LT)) = (\<exists>r. T = RefT r)"
+"app' (Invoke C mn fpTs, G, maxs, 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> is_class G 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,maxs,rT,s) = False"
+
+
+
+constdefs
+ xcpt_app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> bool"
+ "xcpt_app i G pc et \<equiv> \<forall>C\<in>set(xcpt_names (i,G,pc,et)). is_class G C"
+
+ app :: "instr => jvm_prog => nat => ty => nat => exception_table => state_type option => bool"
+ "app i G maxs rT pc et s == case s of None => True | Some t => app' (i,G,maxs,rT,t) \<and> xcpt_app i G pc et"
+
+
+lemma 1: "2 < length a ==> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
+proof (cases a)
+ fix x xs assume "a = x#xs" "2 < length a"
+ thus ?thesis by - (cases xs, simp, cases "tl xs", auto)
+qed auto
+
+lemma 2: "\<not>(2 < length a) ==> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
+proof -;
+ assume "\<not>(2 < length a)"
+ hence "length a < (Suc (Suc (Suc 0)))" by simp
+ hence * : "length a = 0 \<or> length a = Suc 0 \<or> length a = Suc (Suc 0)"
+ by (auto simp add: less_Suc_eq)
+
+ {
+ fix x
+ assume "length x = Suc 0"
+ hence "\<exists> l. x = [l]" by - (cases x, auto)
+ } note 0 = this
+
+ have "length a = Suc (Suc 0) ==> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
+ with * show ?thesis by (auto dest: 0)
+qed
+
+lemmas [simp] = app_def xcpt_app_def
+
+text {*
+\medskip
+simp rules for @{term app}
+*}
+lemma appNone[simp]: "app i G maxs rT pc et None = True" by simp
+
+
+lemma appLoad[simp]:
+"(app (Load idx) G maxs rT pc et (Some s)) = (\<exists>ST LT. s = (ST,LT) \<and> idx < length LT \<and> LT!idx \<noteq> Err \<and> length ST < maxs)"
+ by (cases s, simp)
+
+lemma appStore[simp]:
+"(app (Store idx) G maxs rT pc et (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)
+
+lemma appLitPush[simp]:
+"(app (LitPush v) G maxs rT pc et (Some s)) = (\<exists>ST LT. s = (ST,LT) \<and> length ST < maxs \<and> typeof (\<lambda>v. None) v \<noteq> None)"
+ by (cases s, simp)
+
+lemma appGetField[simp]:
+"(app (Getfield F C) G maxs rT pc et (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) \<and> is_class G (Xcpt NullPointer))"
+ by (cases s, cases "2 <length (fst s)", auto dest!: 1 2)
+
+lemma appPutField[simp]:
+"(app (Putfield F C) G maxs rT pc et (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' \<and> is_class G (Xcpt NullPointer))"
+ by (cases s, cases "2 <length (fst s)", auto dest!: 1 2)
+
+lemma appNew[simp]:
+ "(app (New C) G maxs rT pc et (Some s)) =
+ (\<exists>ST LT. s=(ST,LT) \<and> is_class G C \<and> length ST < maxs \<and> is_class G (Xcpt OutOfMemory))"
+ by (cases s, simp)
+
+lemma appCheckcast[simp]:
+ "(app (Checkcast C) G maxs rT pc et (Some s)) =
+ (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C \<and> is_class G (Xcpt ClassCast))"
+ by (cases s, cases "fst s", simp add: app_def) (cases "hd (fst s)", auto)
+
+lemma appPop[simp]:
+"(app Pop G maxs rT pc et (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT))"
+ by (cases s, cases "2 <length (fst s)", auto dest: 1 2)
+
+
+lemma appDup[simp]:
+"(app Dup G maxs rT pc et (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT) \<and> 1+length ST < maxs)"
+ by (cases s, cases "2 <length (fst s)", auto dest: 1 2)
+
+
+lemma appDup_x1[simp]:
+"(app Dup_x1 G maxs rT pc et (Some s)) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> 2+length ST < maxs)"
+ by (cases s, cases "2 <length (fst s)", auto dest: 1 2)
+
+
+lemma appDup_x2[simp]:
+"(app Dup_x2 G maxs rT pc et (Some s)) = (\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT) \<and> 3+length ST < maxs)"
+ by (cases s, cases "2 <length (fst s)", auto dest: 1 2)
+
+
+lemma appSwap[simp]:
+"app Swap G maxs rT pc et (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))"
+ by (cases s, cases "2 <length (fst s)", auto dest: 1 2)
+
+
+lemma appIAdd[simp]:
+"app IAdd G maxs rT pc et (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)"
+ proof (cases "a")
+ fix t ts assume a: "a = t#ts"
+ show ?thesis
+ proof (cases t)
+ fix p assume p: "t = PrimT p"
+ show ?thesis
+ proof (cases p)
+ assume ip: "p = Integer"
+ show ?thesis
+ proof (cases ts)
+ fix t' ts' assume t': "ts = t' # ts'"
+ show ?thesis
+ proof (cases t')
+ fix p' assume "t' = PrimT p'"
+ with t' ip p a
+ show ?thesis by - (cases p', auto)
+ qed (auto simp add: a p ip t')
+ qed (auto simp add: a p ip)
+ qed (auto simp add: a p)
+ qed (auto simp add: a)
+ qed auto
+ with Pair show ?thesis by simp
+qed
+
+
+lemma appIfcmpeq[simp]:
+"app (Ifcmpeq b) G maxs rT pc et (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)
+
+
+lemma appReturn[simp]:
+"app Return G maxs rT pc et (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)
+
+lemma appGoto[simp]:
+"app (Goto branch) G maxs rT pc et (Some s) = True"
+ by simp
+
+lemma appThrow[simp]:
+ "app Throw G maxs rT pc et (Some s) =
+ (\<exists>T ST LT r. s=(T#ST,LT) \<and> T = RefT r \<and> (\<forall>C \<in> set (match_any G pc et). is_class G C))"
+ by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+
+lemma appInvoke[simp]:
+"app (Invoke C mn fpTs) G maxs rT pc et (Some s) = (\<exists>apTs X ST LT mD' rT' b'.
+ s = ((rev apTs) @ (X # ST), LT) \<and> length apTs = length fpTs \<and> is_class G C \<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') \<and>
+ (\<forall>C \<in> set (match_any G pc et). is_class G C))" (is "?app s = ?P s")
+proof (cases (open) s)
+ case Pair
+ have "?app (a,b) ==> ?P (a,b)"
+ proof -
+ assume app: "?app (a,b)"
+ hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<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 (unfold app_def, clarsimp) blast
+ qed
+ with Pair
+ have "?app s ==> ?P s" by simp
+ moreover
+ have "?P s \<Longrightarrow> ?app s" by (unfold app_def) clarsimp
+ ultimately
+ show ?thesis by blast
+qed
+
+lemma effNone:
+ "(pc', s') \<in> set (eff i G pc et None) \<Longrightarrow> s' = None"
+ by (auto simp add: eff_def xcpt_eff_def norm_eff_def)
+
+lemmas [simp del] = app_def xcpt_app_def
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/EffectMono.thy Sun Dec 16 00:17:44 2001 +0100
@@ -0,0 +1,442 @@
+(* Title: HOL/MicroJava/BV/EffMono.thy
+ ID: $Id$
+ Author: Gerwin Klein
+ Copyright 2000 Technische Universitaet Muenchen
+*)
+
+header {* Monotonicity of eff and app *}
+
+theory EffectMono = Effect:
+
+
+lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
+ by (auto elim: widen.elims)
+
+
+lemma sup_loc_some [rule_format]:
+"\<forall>y n. (G \<turnstile> b <=l y) --> n < length y --> y!n = OK t -->
+ (\<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
+
+ case Cons
+ show "?P (a#list)"
+ proof (clarsimp simp add: list_all2_Cons1 sup_loc_def Listn.le_def lesub_def)
+ fix z zs n
+ assume * :
+ "G \<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs"
+ "n < Suc (length list)" "(z # zs) ! n = OK 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_OK)
+ next
+ case Suc
+ with Cons *
+ show ?thesis by (simp add: sup_loc_def Listn.le_def lesub_def)
+ qed
+ qed
+qed
+
+
+lemma all_widen_is_sup_loc:
+"\<forall>b. length a = length b -->
+ (\<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 --> ?Q a b" is "?P a")
+proof (induct "a")
+ show "?P []" by simp
+
+ fix l ls assume Cons: "?P ls"
+
+ show "?P (l#ls)"
+ proof (intro allI impI)
+ fix b
+ assume "length (l # ls) = length (b::ty list)"
+ with Cons
+ show "?Q (l # ls) b" by - (cases b, auto)
+ qed
+qed
+
+
+lemma append_length_n [rule_format]:
+"\<forall>n. n \<le> length x --> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
+proof (induct (open) ?P x)
+ show "?P []" by simp
+
+ fix l ls assume Cons: "?P ls"
+
+ show "?P (l#ls)"
+ proof (intro allI impI)
+ fix n
+ assume l: "n \<le> length (l # ls)"
+
+ show "\<exists>a b. l # ls = a @ b \<and> length a = n"
+ proof (cases n)
+ assume "n=0" thus ?thesis by simp
+ next
+ fix n' assume s: "n = Suc n'"
+ with l have "n' \<le> length ls" by simp
+ hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rule_format])
+ then obtain a b where "ls = a @ b" "length a = n'" by rules
+ with s have "l # ls = (l#a) @ b \<and> length (l#a) = n" by simp
+ thus ?thesis by blast
+ qed
+ qed
+qed
+
+lemma rev_append_cons:
+"n < length x ==> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
+proof -
+ assume n: "n < length x"
+ hence "n \<le> length x" by simp
+ hence "\<exists>a b. x = a @ b \<and> length a = n" by (rule append_length_n)
+ then obtain r d where x: "x = r@d" "length r = n" by rules
+ with n have "\<exists>b c. d = b#c" by (simp add: neq_Nil_conv)
+ then obtain b c where "d = b#c" by rules
+ with x have "x = (rev (rev r)) @ b # c \<and> length (rev r) = n" by simp
+ thus ?thesis by blast
+qed
+
+lemma sup_loc_length_map:
+ "G \<turnstile> map f a <=l map g b \<Longrightarrow> length a = length b"
+proof -
+ assume "G \<turnstile> map f a <=l map g b"
+ hence "length (map f a) = length (map g b)" by (rule sup_loc_length)
+ thus ?thesis by simp
+qed
+
+lemmas [iff] = not_Err_eq
+
+lemma app_mono:
+"[|G \<turnstile> s <=' s'; app i G m rT pc et s'|] ==> app i G m rT pc et s"
+proof -
+
+ { fix s1 s2
+ assume G: "G \<turnstile> s2 <=s s1"
+ assume app: "app i G m rT pc et (Some s1)"
+
+ note [simp] = sup_loc_length sup_loc_length_map
+
+ have "app i G m rT pc et (Some s2)"
+ proof (cases (open) i)
+ case Load
+
+ from G Load app
+ have "G \<turnstile> snd s2 <=l snd s1" by (auto simp add: sup_state_conv)
+
+ with G Load app show ?thesis
+ by (cases s2) (auto simp add: sup_state_conv dest: sup_loc_some)
+ next
+ case Store
+ with G app show ?thesis
+ by (cases s2, auto simp add: map_eq_Cons sup_loc_Cons2 sup_state_conv)
+ next
+ case LitPush
+ with G app show ?thesis by (cases s2, auto simp add: sup_state_conv)
+ next
+ case New
+ with G app show ?thesis by (cases s2, auto simp add: sup_state_conv)
+ 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" and
+ xc: "is_class G (Xcpt NullPointer)"
+ by force
+ 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 xc)
+ 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,
+ auto dest: sup_state_length)
+ next
+ case Dup_x1
+ with app G show ?thesis
+ by (cases s2, clarsimp simp add: sup_state_Cons2,
+ auto dest: sup_state_length)
+ next
+ case Dup_x2
+ with app G show ?thesis
+ by (cases s2, clarsimp simp add: sup_state_Cons2,
+ auto dest: sup_state_length)
+ 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: "is_class G cname" 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')" and
+ x: "\<forall>C \<in> set (match_any G pc et). is_class G C"
+ 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
+ hence "\<exists>a b c. (fst s2) = rev a @ b # c \<and> length a = length list"
+ by (rule rev_append_cons [rule_format])
+ thus ?thesis
+ by - (cases s2, elim exE conjE, simp, rule that)
+ qed
+
+ from l l'
+ have "length (rev apTs') = length (rev apTs)" by simp
+
+ from this s1 s2 G
+ obtain
+ G': "G \<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)
+
+ from G'
+ have "G \<turnstile> map OK apTs' <=l map OK apTs"
+ by (simp add: sup_state_conv)
+ 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)
+
+ from Invoke s2 l' w' C' m c x
+ show ?thesis
+ by (simp del: split_paired_Ex) blast
+ next
+ case Throw
+ with app G show ?thesis
+ by (cases s2, clarsimp simp add: sup_state_Cons2 widen_RefT2)
+ qed
+ } note this [simp]
+
+ assume "G \<turnstile> s <=' s'" "app i G m rT pc et s'"
+ thus ?thesis by (cases s, cases s', auto)
+qed
+
+lemmas [simp del] = split_paired_Ex
+
+lemma eff'_mono:
+"[| app i G m rT pc et (Some s2); G \<turnstile> s1 <=s s2 |] ==>
+ G \<turnstile> eff' (i,G,s1) <=s eff' (i,G,s2)"
+proof (cases s1, cases s2)
+ fix a1 b1 a2 b2
+ assume s: "s1 = (a1,b1)" "s2 = (a2,b2)"
+ assume app2: "app i G m rT pc et (Some s2)"
+ assume G: "G \<turnstile> s1 <=s s2"
+
+ note [simp] = eff_def
+
+ hence "G \<turnstile> (Some s1) <=' (Some s2)" by simp
+ from this app2
+ have app1: "app i G m rT pc et (Some s1)" by (rule app_mono)
+
+ show ?thesis
+ proof (cases (open) i)
+ case Load
+
+ with s app1
+ obtain y where
+ y: "nat < length b1" "b1 ! nat = OK y" by clarsimp
+
+ from Load s app2
+ obtain y' where
+ y': "nat < length b2" "b2 ! nat = OK y'" by clarsimp
+
+ from G s
+ have "G \<turnstile> b1 <=l b2" by (simp add: sup_state_conv)
+
+ with y y'
+ have "G \<turnstile> y \<preceq> y'"
+ by - (drule sup_loc_some, simp+)
+
+ with Load G y y' s app1 app2
+ show ?thesis by (clarsimp simp add: sup_state_conv)
+ next
+ case Store
+ with G s app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_conv sup_loc_update)
+ next
+ case LitPush
+ with G s app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case New
+ with G s app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Getfield
+ with G s app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Putfield
+ with G s app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Checkcast
+ with G s app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Invoke
+
+ with s app1
+ obtain a X ST where
+ s1: "s1 = (a @ X # ST, b1)" and
+ l: "length a = length list"
+ by (simp, elim exE conjE, simp)
+
+ from Invoke s app2
+ obtain a' X' ST' where
+ s2: "s2 = (a' @ X' # ST', b2)" and
+ l': "length a' = length list"
+ by (simp, elim exE conjE, simp)
+
+ from l l'
+ have lr: "length a = length a'" by simp
+
+ from lr G s s1 s2
+ have "G \<turnstile> (ST, b1) <=s (ST', b2)"
+ by (simp add: sup_state_append_fst sup_state_Cons1)
+
+ moreover
+
+ obtain b1' b2' where eff':
+ "b1' = snd (eff' (i,G,s1))"
+ "b2' = snd (eff' (i,G,s2))" by simp
+
+ from Invoke G s eff' app1 app2
+ obtain "b1 = b1'" "b2 = b2'" by simp
+
+ ultimately
+
+ have "G \<turnstile> (ST, b1') <=s (ST', b2')" by simp
+
+ with Invoke G s app1 app2 eff' s1 s2 l l'
+ show ?thesis
+ by (clarsimp simp add: sup_state_conv)
+ next
+ case Return
+ with G
+ show ?thesis
+ by simp
+ next
+ case Pop
+ with G s app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Dup
+ with G s app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Dup_x1
+ with G s app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Dup_x2
+ with G s app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Swap
+ with G s app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case IAdd
+ with G s app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Goto
+ with G s app1 app2
+ show ?thesis by simp
+ next
+ case Ifcmpeq
+ with G s app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Throw
+ with G
+ show ?thesis
+ by simp
+ qed
+qed
+
+lemmas [iff del] = not_Err_eq
+
+end
+
--- a/src/HOL/MicroJava/BV/Err.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy Sun Dec 16 00:17:44 2001 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/BCV/Err.thy
+(* Title: HOL/MicroJava/BV/Err.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 2000 TUM
@@ -137,7 +137,8 @@
lemma semilat_errI:
"semilat(A,r,f) ==> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
-apply (unfold semilat_Def closed_def plussub_def lesub_def lift2_def Err.le_def err_def)
+apply (unfold semilat_Def closed_def plussub_def lesub_def
+ lift2_def Err.le_def err_def)
apply (simp split: err.split)
done
--- a/src/HOL/MicroJava/BV/JType.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy Sun Dec 16 00:17:44 2001 +0100
@@ -1,10 +1,10 @@
-(* Title: HOL/BCV/JType.thy
+(* Title: HOL/MicroJava/BV/JType.thy
ID: $Id$
Author: Tobias Nipkow, Gerwin Klein
Copyright 2000 TUM
*)
-header "Java Type System as Semilattice"
+header "The Java Type System as Semilattice"
theory JType = WellForm + Err:
@@ -14,11 +14,12 @@
sup :: "'c prog => ty => ty => ty err"
"sup G T1 T2 ==
- case T1 of PrimT P1 => (case T2 of PrimT P2 => (if P1 = P2 then OK (PrimT P1) else Err) | RefT R => Err)
+ case T1 of PrimT P1 => (case T2 of PrimT P2 =>
+ (if P1 = P2 then OK (PrimT P1) else Err) | RefT R => Err)
| RefT R1 => (case T2 of PrimT P => Err | RefT R2 =>
(case R1 of NullT => (case R2 of NullT => OK NT | ClassT C => OK (Class C))
| ClassT C => (case R2 of NullT => OK (Class C)
- | ClassT D => OK (Class (some_lub ((subcls1 G)^* ) C D)))))"
+ | ClassT D => OK (Class (some_lub ((subcls1 G)^* ) C D)))))"
subtype :: "'c prog => ty => ty => bool"
"subtype G T1 T2 == G \<turnstile> T1 \<preceq> T2"
--- a/src/HOL/MicroJava/BV/JVM.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy Sun Dec 16 00:17:44 2001 +0100
@@ -1,34 +1,36 @@
-(* Title: HOL/BCV/JVM.thy
+(* Title: HOL/MicroJava/BV/JVM.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow, Gerwin Klein
Copyright 2000 TUM
-
*)
header "Kildall for the JVM"
-theory JVM = Kildall + JVMType + Opt + Product + Typing_Framework_err +
- StepMono + BVSpec:
+theory JVM = Kildall_Lift + JVMType + Opt + Product + Typing_Framework_err +
+ EffectMono + BVSpec:
constdefs
- exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> instr list \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> state"
- "exec G maxs rT bs == err_step (\<lambda>pc. app (bs!pc) G maxs rT) (\<lambda>pc. step (bs!pc) G)"
+ exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> state step_type"
+ "exec G maxs rT et bs ==
+ err_step (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"
- kiljvm :: "jvm_prog => nat => nat => ty => instr list => state list => state list"
- "kiljvm G maxs maxr rT bs ==
- kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)"
+ kiljvm :: "jvm_prog => nat => nat => ty => exception_table =>
+ instr list => state list => state list"
+ "kiljvm G maxs maxr rT et bs ==
+ kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G maxs rT et bs)"
- wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
- "wt_kil G C pTs rT mxs mxl ins ==
- bounded (\<lambda>n. succs (ins!n) n) (size ins) \<and> 0 < size ins \<and>
+ wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
+ exception_table \<Rightarrow> instr list \<Rightarrow> bool"
+ "wt_kil G C pTs rT mxs mxl et ins ==
+ bounded (exec G mxs rT et ins) (size ins) \<and> 0 < size ins \<and>
(let first = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));
start = OK first#(replicate (size ins - 1) (OK None));
- result = kiljvm G mxs (1+size pTs+mxl) rT ins start
+ result = kiljvm G mxs (1+size pTs+mxl) rT et ins start
in \<forall>n < size ins. result!n \<noteq> Err)"
wt_jvm_prog_kildall :: "jvm_prog => bool"
"wt_jvm_prog_kildall G ==
- wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b)). wt_kil G C (snd sig) rT maxs maxl b) G"
+ wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G"
lemma special_ex_swap_lemma [iff]:
@@ -37,66 +39,225 @@
lemmas [iff del] = not_None_eq
+lemma non_empty_succs: "succs i pc \<noteq> []"
+ by (cases i) auto
+
+lemma non_empty:
+ "non_empty (\<lambda>pc. eff (bs!pc) G pc et)"
+ by (simp add: non_empty_def eff_def non_empty_succs)
+
+lemma listn_Cons_Suc [elim!]:
+ "l#xs \<in> list n A \<Longrightarrow> (\<And>n'. n = Suc n' \<Longrightarrow> l \<in> A \<Longrightarrow> xs \<in> list n' A \<Longrightarrow> P) \<Longrightarrow> P"
+ by (cases n) auto
+
+lemma listn_appendE [elim!]:
+ "a@b \<in> list n A \<Longrightarrow> (\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P) \<Longrightarrow> P"
+proof -
+ have "\<And>n. a@b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n=n1+n2 \<and> a \<in> list n1 A \<and> b \<in> list n2 A"
+ (is "\<And>n. ?list a n \<Longrightarrow> \<exists>n1 n2. ?P a n n1 n2")
+ proof (induct a)
+ fix n assume "?list [] n"
+ hence "?P [] n 0 n" by simp
+ thus "\<exists>n1 n2. ?P [] n n1 n2" by fast
+ next
+ fix n l ls
+ assume "?list (l#ls) n"
+ then obtain n' where n: "n = Suc n'" "l \<in> A" and "ls@b \<in> list n' A" by fastsimp
+ assume "\<And>n. ls @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A"
+ hence "\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A" .
+ then obtain n1 n2 where "n' = n1 + n2" "ls \<in> list n1 A" "b \<in> list n2 A" by fast
+ with n have "?P (l#ls) n (n1+1) n2" by simp
+ thus "\<exists>n1 n2. ?P (l#ls) n n1 n2" by fastsimp
+ qed
+ moreover
+ assume "a@b \<in> list n A" "\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P"
+ ultimately
+ show ?thesis by blast
+qed
+
+
theorem exec_pres_type:
- "[| wf_prog wf_mb S |] ==>
- pres_type (exec S maxs rT bs) (size bs) (states S maxs maxr)"
- apply (unfold pres_type_def list_def step_def JVM_states_unfold)
- apply (clarify elim!: option_map_in_optionI lift_in_errI)
- apply (simp add: exec_def err_step_def lift_def split: err.split)
- apply (simp add: step_def option_map_def split: option.splits)
- apply clarify
- apply (case_tac "bs!p")
+ "wf_prog wf_mb S ==>
+ pres_type (exec S maxs rT et bs) (size bs) (states S maxs maxr)"
+ apply (unfold exec_def JVM_states_unfold)
+ apply (rule pres_type_lift)
+ apply clarify
+ apply (case_tac s)
+ apply simp
+ apply (drule effNone)
+ apply simp
+ apply (simp add: eff_def xcpt_eff_def norm_eff_def)
+ apply (case_tac "bs!p")
+
+ apply (clarsimp simp add: not_Err_eq)
+ apply (drule listE_nth_in, assumption)
+ apply fastsimp
+
+ apply (fastsimp simp add: not_None_eq)
+
+ apply (fastsimp simp add: not_None_eq typeof_empty_is_type)
+
+ apply clarsimp
+ apply (erule disjE)
+ apply fastsimp
+ apply clarsimp
+ apply (rule_tac x="1" in exI)
+ apply fastsimp
- apply (fastsimp simp add: not_Err_eq dest: subsetD nth_mem)
- apply fastsimp
- apply (fastsimp simp add: not_None_eq typeof_empty_is_type)
- apply fastsimp
- apply (fastsimp dest: field_fields fields_is_type)
- apply fastsimp
- apply fastsimp
- defer
- apply fastsimp
- apply fastsimp
- apply fastsimp
- apply fastsimp
- apply fastsimp
- apply fastsimp
- apply fastsimp
- apply fastsimp
- apply fastsimp
+ apply clarsimp
+ apply (erule disjE)
+ apply (fastsimp dest: field_fields fields_is_type)
+ apply simp
+ apply (rule_tac x=1 in exI)
+ apply fastsimp
+
+ apply clarsimp
+ apply (erule disjE)
+ apply fastsimp
+ apply simp
+ apply (rule_tac x=1 in exI)
+ apply fastsimp
+
+ apply clarsimp
+ apply (erule disjE)
+ apply fastsimp
+ apply clarsimp
+ apply (rule_tac x=1 in exI)
+ apply fastsimp
+
+ defer
+
+ apply fastsimp
+ apply fastsimp
+
+ apply clarsimp
+ apply (rule_tac x="n'+2" in exI)
+ apply simp
+ apply (drule listE_length)+
+ apply fastsimp
- (* Invoke *)
- apply (clarsimp simp add: Un_subset_iff)
- apply (drule method_wf_mdecl, assumption+)
- apply (simp add: wf_mdecl_def wf_mhead_def)
- done
+ apply clarsimp
+ apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)
+ apply simp
+ apply (drule listE_length)+
+ apply fastsimp
+
+ apply clarsimp
+ apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI)
+ apply simp
+ apply (drule listE_length)+
+ apply fastsimp
+
+ apply fastsimp
+ apply fastsimp
+ apply fastsimp
+ apply fastsimp
+ apply clarsimp
+ apply (erule disjE)
+ apply fastsimp
+ apply clarsimp
+ apply (rule_tac x=1 in exI)
+ apply fastsimp
+
+ apply (erule disjE)
+ apply (clarsimp simp add: Un_subset_iff)
+ apply (drule method_wf_mdecl, assumption+)
+ apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
+ apply fastsimp
+ apply clarsimp
+ apply (rule_tac x=1 in exI)
+ apply fastsimp
+ done
lemmas [iff] = not_None_eq
+lemma map_fst_eq:
+ "map fst (map (\<lambda>z. (f z, x z)) a) = map fst (map (\<lambda>z. (f z, y z)) a)"
+ by (induct a) auto
+
+lemma succs_stable_eff:
+ "succs_stable (sup_state_opt G) (\<lambda>pc. eff (bs!pc) G pc et)"
+ apply (unfold succs_stable_def eff_def xcpt_eff_def)
+ apply (simp add: map_fst_eq)
+ done
+
+lemma sup_state_opt_unfold:
+ "sup_state_opt G \<equiv> Opt.le (Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G))))"
+ by (simp add: sup_state_opt_def sup_state_def sup_loc_def sup_ty_opt_def)
+
+constdefs
+ opt_states :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (ty list \<times> ty err list) option set"
+ "opt_states G maxs maxr \<equiv> opt (\<Union>{list n (types G) |n. n \<le> maxs} \<times> list maxr (err (types G)))"
+
+lemma app_mono:
+ "app_mono (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (length bs) (opt_states G maxs maxr)"
+ by (unfold app_mono_def lesub_def) (blast intro: EffectMono.app_mono)
+
+lemma le_list_appendI:
+ "\<And>b c d. a <=[r] b \<Longrightarrow> c <=[r] d \<Longrightarrow> a@c <=[r] b@d"
+apply (induct a)
+ apply simp
+apply (case_tac b)
+apply auto
+done
+
+lemma le_listI:
+ "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> a!n <=_r b!n) \<Longrightarrow> a <=[r] b"
+ apply (unfold lesub_def Listn.le_def)
+ apply (simp add: list_all2_conv_all_nth)
+ done
+
+lemma eff_mono:
+ "\<lbrakk>p < length bs; s <=_(sup_state_opt G) t; app (bs!p) G maxs rT pc et t\<rbrakk>
+ \<Longrightarrow> eff (bs!p) G p et s <=|sup_state_opt G| eff (bs!p) G p et t"
+ apply (unfold eff_def)
+ apply (rule le_list_appendI)
+ apply (simp add: norm_eff_def)
+ apply (rule le_listI)
+ apply simp
+ apply simp
+ apply (simp add: lesub_def)
+ apply (case_tac s)
+ apply simp
+ apply (simp del: split_paired_All split_paired_Ex)
+ apply (elim exE conjE)
+ apply simp
+ apply (drule eff'_mono, assumption)
+ apply assumption
+ apply (simp add: xcpt_eff_def)
+ apply (rule le_listI)
+ apply simp
+ apply simp
+ apply (simp add: lesub_def)
+ apply (case_tac s)
+ apply simp
+ apply simp
+ apply (case_tac t)
+ apply simp
+ apply (clarsimp simp add: sup_state_conv)
+ done
+
+lemma order_sup_state_opt:
+ "wf_prog wf_mb G \<Longrightarrow> order (sup_state_opt G)"
+ by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
theorem exec_mono:
"wf_prog wf_mb G ==>
- mono (JVMType.le G maxs maxr) (exec G maxs rT bs) (size bs) (states G maxs maxr)"
- apply (unfold mono_def)
+ mono (JVMType.le G maxs maxr) (exec G maxs rT et bs) (size bs) (states G maxs maxr)"
+ apply (unfold exec_def JVM_le_unfold JVM_states_unfold)
+ apply (rule mono_lift)
+ apply (fold sup_state_opt_unfold opt_states_def)
+ apply (erule order_sup_state_opt)
+ apply (rule succs_stable_eff)
+ apply (rule app_mono)
apply clarify
- apply (unfold lesub_def)
- apply (case_tac t)
- apply (simp add: JVM_le_unfold Err.le_def exec_def err_step_def lift_def)
- apply (case_tac s)
- apply (simp add: JVM_le_unfold Err.le_def exec_def err_step_def lift_def)
- apply (simp add: JVM_le_convert exec_def err_step_def lift_def)
- apply (simp add: JVM_le_unfold Err.le_def exec_def err_step_def lift_def)
- apply (rule conjI)
- apply clarify
- apply (rule step_mono, assumption+)
- apply (rule impI)
- apply (erule contrapos_nn)
- apply (rule app_mono, assumption+)
+ apply (rule eff_mono)
+ apply assumption+
done
theorem semilat_JVM_slI:
- "[| wf_prog wf_mb G |] ==> semilat (JVMType.sl G maxs maxr)"
+ "wf_prog wf_mb G ==> semilat (JVMType.sl G maxs maxr)"
apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
apply (rule semilat_opt)
apply (rule err_semilat_Product_esl)
@@ -114,9 +275,9 @@
theorem is_bcv_kiljvm:
- "[| wf_prog wf_mb G; bounded (\<lambda>pc. succs (bs!pc) pc) (size bs) |] ==>
- is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)
- (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT bs)"
+ "[| wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) |] ==>
+ is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)
+ (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
apply (unfold kiljvm_def sl_triple_conv)
apply (rule is_bcv_kildall)
apply (simp (no_asm) add: sl_triple_conv [symmetric])
@@ -132,9 +293,9 @@
theorem wt_kil_correct:
- "[| wt_kil G C pTs rT maxs mxl bs; wf_prog wf_mb G;
+ "[| wt_kil G C pTs rT maxs mxl et bs; wf_prog wf_mb G;
is_class G C; \<forall>x \<in> set pTs. is_type G x |]
- ==> \<exists>phi. wt_method G C pTs rT maxs mxl bs phi"
+ ==> \<exists>phi. wt_method G C pTs rT maxs mxl bs et phi"
proof -
let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
#(replicate (size bs - 1) (OK None))"
@@ -143,41 +304,25 @@
assume isclass: "is_class G C"
assume istype: "\<forall>x \<in> set pTs. is_type G x"
- assume "wt_kil G C pTs rT maxs mxl bs"
+ assume "wt_kil G C pTs rT maxs mxl et bs"
then obtain maxr r where
- bounded: "bounded (\<lambda>pc. succs (bs!pc) pc) (size bs)" and
- result: "r = kiljvm G maxs maxr rT bs ?start" and
+ bounded: "bounded (exec G maxs rT et bs) (size bs)" and
+ result: "r = kiljvm G maxs maxr rT et bs ?start" and
success: "\<forall>n < size bs. r!n \<noteq> Err" and
instrs: "0 < size bs" and
maxr: "maxr = Suc (length pTs + mxl)"
by (unfold wt_kil_def) simp
- { fix pc
- have "succs (bs!pc) pc \<noteq> []"
- by (cases "bs!pc") auto
- }
-
- hence non_empty: "non_empty (\<lambda>pc. succs (bs!pc) pc)"
- by (unfold non_empty_def) blast
-
from wf bounded
have bcv:
- "is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)
- (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT bs)"
+ "is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)
+ (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
by (rule is_bcv_kiljvm)
- { fix l x
- have "set (replicate l x) \<subseteq> {x}"
- by (cases "0 < l") simp+
+ { fix l x have "set (replicate l x) \<subseteq> {x}" by (cases "0 < l") simp+
} note subset_replicate = this
-
- from istype
- have "set pTs \<subseteq> types G"
- by auto
-
- hence "OK ` set pTs \<subseteq> err (types G)"
- by auto
-
+ from istype have "set pTs \<subseteq> types G" by auto
+ hence "OK ` set pTs \<subseteq> err (types G)" by auto
with instrs maxr isclass
have "?start \<in> list (length bs) (states G maxs maxr)"
apply (unfold list_def JVM_states_unfold)
@@ -191,51 +336,37 @@
apply (simp add: subset_replicate)
apply simp
done
-
- with bcv success result
- have
+ with bcv success result have
"\<exists>ts\<in>list (length bs) (states G maxs maxr).
?start <=[JVMType.le G maxs maxr] ts \<and>
- wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) ts"
+ wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) ts"
by (unfold is_bcv_def) auto
-
then obtain phi' where
l: "phi' \<in> list (length bs) (states G maxs maxr)" and
s: "?start <=[JVMType.le G maxs maxr] phi'" and
- w: "wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) phi'"
+ w: "wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) phi'"
by blast
-
hence dynamic:
- "dynamic_wt (sup_state_opt G) (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) phi'"
+ "dynamic_wt (sup_state_opt G) (exec G maxs rT et bs) phi'"
by (simp add: dynamic_wt_def exec_def JVM_le_Err_conv)
- from s
- have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)"
+ from s have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)"
by (drule_tac p=0 in le_listD) (simp add: lesub_def)+
- from l
- have l: "size phi' = size bs"
- by simp
-
- with instrs w
- have "phi' ! 0 \<noteq> Err"
- by (unfold wt_step_def) simp
-
- with instrs l
- have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"
+ from l have l: "size phi' = size bs" by simp
+ with instrs w have "phi' ! 0 \<noteq> Err" by (unfold wt_step_def) simp
+ with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"
by (clarsimp simp add: not_Err_eq)
- from l bounded
- have "bounded (\<lambda>pc. succs (bs ! pc) pc) (length phi')"
- by simp
-
- with dynamic non_empty
- have "static_wt (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT) (\<lambda>pc. step (bs!pc) G)
- (\<lambda>pc. succs (bs!pc) pc) (map ok_val phi')"
- by (auto intro: dynamic_imp_static simp add: exec_def)
-
- with instrs l le bounded
- have "wt_method G C pTs rT maxs mxl bs (map ok_val phi')"
+ from l bounded
+ have bounded': "bounded (\<lambda>pc. eff (bs!pc) G pc et) (length phi')"
+ by (simp add: exec_def bounded_lift)
+ with dynamic
+ have "static_wt (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et)
+ (\<lambda>pc. eff (bs!pc) G pc et) (map ok_val phi')"
+ by (auto intro: dynamic_imp_static simp add: exec_def non_empty)
+ with instrs l le bounded'
+ have "wt_method G C pTs rT maxs mxl bs et (map ok_val phi')"
apply (unfold wt_method_def static_wt_def)
apply simp
apply (rule conjI)
@@ -254,74 +385,77 @@
qed
-(* there's still one easy, and one nontrivial (but provable) sorry in here *)
-(*
theorem wt_kil_complete:
- "[| wt_method G C pTs rT maxs mxl bs phi; wf_prog wf_mb G;
- length phi = length bs; is_class G C; \<forall>x \<in> set pTs. is_type G x |]
- ==> wt_kil G C pTs rT maxs mxl bs"
+ "[| wt_method G C pTs rT maxs mxl bs et phi; wf_prog wf_mb G;
+ length phi = length bs; is_class G C; \<forall>x \<in> set pTs. is_type G x;
+ map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl)) |]
+ ==> wt_kil G C pTs rT maxs mxl et bs"
proof -
- assume wf: "wf_prog wf_mb G"
+ assume wf: "wf_prog wf_mb G"
assume isclass: "is_class G C"
- assume istype: "\<forall>x \<in> set pTs. is_type G x"
- assume length: "length phi = length bs"
+ assume istype: "\<forall>x \<in> set pTs. is_type G x"
+ assume length: "length phi = length bs"
+ assume istype_phi: "map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl))"
- assume "wt_method G C pTs rT maxs mxl bs phi"
+ assume "wt_method G C pTs rT maxs mxl bs et phi"
then obtain
instrs: "0 < length bs" and
wt_start: "wt_start G C pTs mxl phi" and
wt_ins: "\<forall>pc. pc < length bs \<longrightarrow>
- wt_instr (bs ! pc) G rT phi maxs (length bs) pc"
+ wt_instr (bs ! pc) G rT phi maxs (length bs) et pc"
by (unfold wt_method_def) simp
- let ?succs = "\<lambda>pc. succs (bs!pc) pc"
- let ?step = "\<lambda>pc. step (bs!pc) G"
- let ?app = "\<lambda>pc. app (bs!pc) G maxs rT"
+ let ?eff = "\<lambda>pc. eff (bs!pc) G pc et"
+ let ?app = "\<lambda>pc. app (bs!pc) G maxs rT pc et"
+ have bounded_eff: "bounded ?eff (size bs)"
+ proof (unfold bounded_def, clarify)
+ fix pc pc' s s' assume "pc < length bs"
+ with wt_ins have "wt_instr (bs!pc) G rT phi maxs (length bs) et pc" by fast
+ then obtain "\<forall>(pc',s') \<in> set (?eff pc (phi!pc)). pc' < length bs"
+ by (unfold wt_instr_def) fast
+ hence "\<forall>pc' \<in> set (map fst (?eff pc (phi!pc))). pc' < length bs" by auto
+ also
+ note succs_stable_eff
+ hence "map fst (?eff pc (phi!pc)) = map fst (?eff pc s)"
+ by (rule succs_stableD)
+ finally have "\<forall>(pc',s') \<in> set (?eff pc s). pc' < length bs" by auto
+ moreover assume "(pc',s') \<in> set (?eff pc s)"
+ ultimately show "pc' < length bs" by blast
+ qed
+ hence bounded_exec: "bounded (exec G maxs rT et bs) (size bs)"
+ by (simp add: exec_def bounded_lift)
+
from wt_ins
- have bounded: "bounded ?succs (size bs)"
- by (unfold wt_instr_def bounded_def) blast
-
- from wt_ins
- have "static_wt (sup_state_opt G) ?app ?step ?succs phi"
+ have "static_wt (sup_state_opt G) ?app ?eff phi"
apply (unfold static_wt_def wt_instr_def lesub_def)
apply (simp (no_asm) only: length)
apply blast
done
- with bounded
- have "dynamic_wt (sup_state_opt G) (err_step ?app ?step) ?succs (map OK phi)"
+ with bounded_eff
+ have "dynamic_wt (sup_state_opt G) (err_step ?app ?eff) (map OK phi)"
by - (erule static_imp_dynamic, simp add: length)
-
hence dynamic:
- "dynamic_wt (sup_state_opt G) (exec G maxs rT bs) ?succs (map OK phi)"
+ "dynamic_wt (sup_state_opt G) (exec G maxs rT et bs) (map OK phi)"
by (unfold exec_def)
let ?maxr = "1+size pTs+mxl"
-
- from wf bounded
+ from wf bounded_exec
have is_bcv:
- "is_bcv (JVMType.le G maxs ?maxr) Err (exec G maxs rT bs) ?succs
- (size bs) (states G maxs ?maxr) (kiljvm G maxs ?maxr rT bs)"
+ "is_bcv (JVMType.le G maxs ?maxr) Err (exec G maxs rT et bs)
+ (size bs) (states G maxs ?maxr) (kiljvm G maxs ?maxr rT et bs)"
by (rule is_bcv_kiljvm)
let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
#(replicate (size bs - 1) (OK None))"
- { fix l x
- have "set (replicate l x) \<subseteq> {x}"
- by (cases "0 < l") simp+
+ { fix l x have "set (replicate l x) \<subseteq> {x}" by (cases "0 < l") simp+
} note subset_replicate = this
- from istype
- have "set pTs \<subseteq> types G"
- by auto
-
- hence "OK ` set pTs \<subseteq> err (types G)"
- by auto
-
- with instrs isclass
- have start:
+ from istype have "set pTs \<subseteq> types G" by auto
+ hence "OK ` set pTs \<subseteq> err (types G)" by auto
+ with instrs isclass have start:
"?start \<in> list (length bs) (states G maxs ?maxr)"
apply (unfold list_def JVM_states_unfold)
apply simp
@@ -335,12 +469,12 @@
apply simp
done
- let ?phi = "map OK phi"
-
- have 1: "?phi \<in> list (length bs) (states G maxs ?maxr)" sorry
-
- have 2: "?start <=[le G maxs ?maxr] ?phi"
+ let ?phi = "map OK phi"
+ have less_phi: "?start <=[JVMType.le G maxs ?maxr] ?phi"
proof -
+ from length instrs
+ have "length ?start = length (map OK phi)" by simp
+ moreover
{ fix n
from wt_start
have "G \<turnstile> ok_val (?start!0) <=' phi!0"
@@ -349,38 +483,62 @@
from instrs length
have "0 < length phi" by simp
ultimately
- have "le G maxs ?maxr (?start!0) (?phi!0)"
+ have "JVMType.le G maxs ?maxr (?start!0) (?phi!0)"
by (simp add: JVM_le_Err_conv Err.le_def lesub_def)
moreover
{ fix n'
- have "le G maxs ?maxr (OK None) (?phi!n)"
+ have "JVMType.le G maxs ?maxr (OK None) (?phi!n)"
by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def
split: err.splits)
hence "[| n = Suc n'; n < length ?start |]
- ==> le G maxs ?maxr (?start!n) (?phi!n)"
+ ==> JVMType.le G maxs ?maxr (?start!n) (?phi!n)"
by simp
}
ultimately
- have "n < length ?start ==> le G maxs ?maxr (?start!n) (?phi!n)"
- by - (cases n, blast+)
- }
- thus ?thesis sorry
+ have "n < length ?start ==> (?start!n) <=_(JVMType.le G maxs ?maxr) (?phi!n)"
+ by (unfold lesub_def) (cases n, blast+)
+ }
+ ultimately show ?thesis by (rule le_listI)
qed
from dynamic
- have "wt_step (le G maxs ?maxr) Err (exec G maxs rT bs) ?succs ?phi"
- by (simp add: dynamic_wt_def JVM_le_Err_conv)
-
- with start 1 2 is_bcv
- have "\<forall>p. p < length bs \<longrightarrow> kiljvm G maxs ?maxr rT bs ?start ! p \<noteq> Err"
- by (unfold is_bcv_def) blast
+ have "wt_step (JVMType.le G maxs ?maxr) Err (exec G maxs rT et bs) ?phi"
+ by (simp add: dynamic_wt_def JVM_le_Err_conv)
+ with start istype_phi less_phi is_bcv
+ have "\<forall>p. p < length bs \<longrightarrow> kiljvm G maxs ?maxr rT et bs ?start ! p \<noteq> Err"
+ by (unfold is_bcv_def) auto
+ with bounded_exec instrs
+ show "wt_kil G C pTs rT maxs mxl et bs" by (unfold wt_kil_def) simp
+qed
+text {*
+ The above theorem @{text wt_kil_complete} is all nice'n shiny except
+ for one assumption: @{term "map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl))"}
+ It does not hold for all @{text phi} that satisfy @{text wt_method}.
- with bounded instrs
- show "wt_kil G C pTs rT maxs mxl bs"
- by (unfold wt_kil_def) simp
-qed
-*)
+ The assumption states mainly that all entries in @{text phi} are legal
+ types in the program context, that the stack size is bounded by @{text maxs},
+ and that the register sizes are exactly @{term "1+size pTs+mxl"}.
+ The BV specification, i.e.~@{text wt_method}, only gives us this
+ property for \emph{reachable} code. For unreachable code,
+ e.g.~unused registers may contain arbitrary garbage. Even the stack
+ and register sizes can be different from the rest of the program (as
+ long as they are consistent inside each chunk of unreachable code).
+
+ All is not lost, though: for each @{text phi} that satisfies
+ @{text wt_method} there is a @{text phi'} that also satisfies
+ @{text wt_method} and that additionally satisfies our assumption.
+ The construction is quite easy: the entries for reachable code
+ are the same in @{text phi} and @{text phi'}, the entries for
+ unreachable code are all @{text None} in @{text phi'} (as it would
+ be produced by Kildall's algorithm).
+ Although this is proved easily by comment, it requires some more
+ overhead (i.e.~talking about reachable instructions) if you try
+ it the hard way. Thus it is missing here for the time being.
+
+ The other direction (@{text wt_kil_correct}) can be lifted to
+ programs without problems:
+*}
lemma is_type_pTs:
"[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls;
t \<in> set (snd sig) |]
@@ -409,8 +567,8 @@
wf: "wf_prog wf_mb G"
by (auto simp add: wt_jvm_prog_kildall_def)
- let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins)) = the (method (G,C) sig) in
- SOME phi. wt_method G C (snd sig) rT maxs maxl ins phi"
+ let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in
+ SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi"
{ fix C S fs mdecls sig rT code
assume "(C,S,fs,mdecls) \<in> set G" "(sig,rT,code) \<in> set mdecls"
--- a/src/HOL/MicroJava/BV/JVMType.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Sun Dec 16 00:17:44 2001 +0100
@@ -1,11 +1,11 @@
-(* Title: HOL/BCV/JVM.thy
+(* Title: HOL/MicroJava/BV/JVM.thy
ID: $Id$
Author: Gerwin Klein
Copyright 2000 TUM
*)
-header "JVM Type System"
+header "The JVM Type System as Semilattice"
theory JVMType = Opt + Product + Listn + JType:
@@ -13,8 +13,8 @@
locvars_type = "ty err list"
opstack_type = "ty list"
state_type = "opstack_type \<times> locvars_type"
- state = "state_type option err" (* for Kildall *)
- method_type = "state_type option list" (* for BVSpec *)
+ state = "state_type option err" -- "for Kildall"
+ method_type = "state_type option list" -- "for BVSpec"
class_type = "sig => method_type"
prog_type = "cname => class_type"
@@ -50,7 +50,7 @@
("_ |- _ <=l _" [71,71] 70)
"sup_loc G == Listn.le (sup_ty_opt G)"
- sup_state :: "['code prog,state_type,state_type] => bool"
+ sup_state :: "['code prog,state_type,state_type] => bool"
("_ |- _ <=s _" [71,71] 70)
"sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)"
@@ -64,7 +64,7 @@
("_ \<turnstile> _ <=o _" [71,71] 70)
sup_loc :: "['code prog,locvars_type,locvars_type] => bool"
("_ \<turnstile> _ <=l _" [71,71] 70)
- sup_state :: "['code prog,state_type,state_type] => bool"
+ sup_state :: "['code prog,state_type,state_type] => bool"
("_ \<turnstile> _ <=s _" [71,71] 70)
sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
("_ \<turnstile> _ <=' _" [71,71] 70)
@@ -98,7 +98,8 @@
sup_ty_opt_def JVM_le_unfold) simp
lemma zip_map [rule_format]:
- "\<forall>a. length a = length b --> zip (map f a) (map g b) = map (\<lambda>(x,y). (f x, g y)) (zip a b)"
+ "\<forall>a. length a = length b -->
+ zip (map f a) (map g b) = map (\<lambda>(x,y). (f x, g y)) (zip a b)"
apply (induct b)
apply simp
apply clarsimp
@@ -148,7 +149,8 @@
lemma sup_state_conv:
- "(G \<turnstile> s1 <=s s2) == (G \<turnstile> map OK (fst s1) <=l map OK (fst s2)) \<and> (G \<turnstile> snd s1 <=l snd s2)"
+ "(G \<turnstile> s1 <=s s2) ==
+ (G \<turnstile> map OK (fst s1) <=l map OK (fst s2)) \<and> (G \<turnstile> snd s1 <=l snd s2)"
by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def split_beta)
--- a/src/HOL/MicroJava/BV/Kildall.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy Sun Dec 16 00:17:44 2001 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/BCV/Kildall.thy
+(* Title: HOL/MicroJava/BV/Kildall.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow, Gerwin Klein
Copyright 2000 TUM
Kildall's algorithm
@@ -8,84 +8,133 @@
header "Kildall's Algorithm"
-theory Kildall = Typing_Framework + While_Combinator:
+theory Kildall = Typing_Framework + While_Combinator + Product:
+
+
+syntax "@lesubstep_type" :: "(nat \<times> 's) list => 's ord => (nat \<times> 's) list => bool"
+ ("(_ /<=|_| _)" [50, 0, 51] 50)
+translations
+ "x <=|r| y" == "x <=[(Product.le (op =) r)] y"
+
constdefs
- pres_type :: "(nat => 's => 's) => nat => 's set => bool"
-"pres_type step n A == !s:A. !p<n. step p s : A"
+ pres_type :: "'s step_type => nat => 's set => bool"
+"pres_type step n A == \<forall>s\<in>A. \<forall>p<n. \<forall>(q,s')\<in>set (step p s). s' \<in> A"
- mono :: "'s ord => (nat => 's => 's) => nat => 's set => bool"
+ mono :: "'s ord => 's step_type => nat => 's set => bool"
"mono r step n A ==
- !s p t. s : A & p < n & s <=_r t --> step p s <=_r step p t"
+ \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t --> step p s <=|r| step p t"
consts
- iter :: "'s binop \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> (nat \<Rightarrow> nat list) \<Rightarrow>
+ iter :: "'s binop \<Rightarrow> 's step_type \<Rightarrow>
's list \<Rightarrow> nat set \<Rightarrow> 's list \<times> nat set"
- propa :: "'s binop => nat list => 's => 's list => nat set => 's list * nat set"
+ propa :: "'s binop => (nat \<times> 's) list => 's list => nat set => 's list * nat set"
primrec
-"propa f [] t ss w = (ss,w)"
-"propa f (q#qs) t ss w = (let u = t +_f ss!q;
- w' = (if u = ss!q then w else insert q w)
- in propa f qs t (ss[q := u]) w')"
+"propa f [] ss w = (ss,w)"
+"propa f (q'#qs) ss w = (let (q,t) = q';
+ u = t +_f ss!q;
+ w' = (if u = ss!q then w else insert q w)
+ in propa f qs (ss[q := u]) w')"
defs iter_def:
-"iter f step succs ss w ==
+"iter f step ss w ==
while (%(ss,w). w \<noteq> {})
- (%(ss,w). let p = SOME p. p : w
- in propa f (succs p) (step p (ss!p)) ss (w-{p}))
+ (%(ss,w). let p = SOME p. p \<in> w
+ in propa f (step p (ss!p)) ss (w-{p}))
(ss,w)"
constdefs
- unstables ::
- "'s ord => (nat => 's => 's) => (nat => nat list) => 's list => nat set"
-"unstables r step succs ss ==
- {p. p < size ss & ~stable r step succs ss p}"
+ unstables :: "'s ord => 's step_type => 's list => nat set"
+"unstables r step ss == {p. p < size ss \<and> \<not>stable r step ss p}"
- kildall :: "'s ord => 's binop => (nat => 's => 's) => (nat => nat list)
- => 's list => 's list"
-"kildall r f step succs ss == fst(iter f step succs ss (unstables r step succs ss))"
+ kildall :: "'s ord => 's binop => 's step_type => 's list => 's list"
+"kildall r f step ss == fst(iter f step ss (unstables r step ss))"
-consts merges :: "'s binop => 's => nat list => 's list => 's list"
+consts merges :: "'s binop => (nat \<times> 's) list => 's list => 's list"
primrec
-"merges f s [] ss = ss"
-"merges f s (p#ps) ss = merges f s ps (ss[p := s +_f ss!p])"
+"merges f [] ss = ss"
+"merges f (p'#ps) ss = (let (p,s) = p' in merges f ps (ss[p := s +_f ss!p]))"
lemmas [simp] = Let_def le_iff_plus_unchanged [symmetric]
+consts
+ "@plusplussub" :: "'a list => ('a => 'a => 'a) => 'a => 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
+primrec
+ "[] ++_f y = y"
+ "(x#xs) ++_f y = xs ++_f (x +_f y)"
+
+lemma nth_merges:
+ "!!ss. [| semilat (A, r, f); p < length ss; ss \<in> list n A;
+ \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A |] ==>
+ (merges f ps ss)!p = map snd [(p',t') \<in> ps. p'=p] ++_f ss!p"
+ (is "!!ss. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?steptype ps \<Longrightarrow> ?P ss ps")
+proof (induct ps)
+ show "\<And>ss. ?P ss []" by simp
+
+ fix ss p' ps'
+ assume sl: "semilat (A, r, f)"
+ assume ss: "ss \<in> list n A"
+ assume l: "p < length ss"
+ assume "?steptype (p'#ps')"
+ then obtain a b where
+ p': "p'=(a,b)" and ab: "a<n" "b\<in>A" and "?steptype ps'"
+ by (cases p', auto)
+ assume "\<And>ss. semilat (A,r,f) \<Longrightarrow> p < length ss \<Longrightarrow> ss \<in> list n A \<Longrightarrow> ?steptype ps' \<Longrightarrow> ?P ss ps'"
+ hence IH: "\<And>ss. ss \<in> list n A \<Longrightarrow> p < length ss \<Longrightarrow> ?P ss ps'" .
+
+ from sl ss ab
+ have "ss[a := b +_f ss!a] \<in> list n A" by (simp add: closedD)
+ moreover
+ from calculation
+ have "p < length (ss[a := b +_f ss!a])" by simp
+ ultimately
+ have "?P (ss[a := b +_f ss!a]) ps'" by (rule IH)
+ with p' l
+ show "?P ss (p'#ps')" by simp
+qed
+
+
lemma pres_typeD:
- "[| pres_type step n A; s:A; p<n |] ==> step p s : A"
+ "[| pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) |] ==> s' \<in> A"
by (unfold pres_type_def, blast)
-lemma boundedD:
- "[| bounded succs n; p < n; q : set(succs p) |] ==> q < n"
+lemma boundedD:
+ "[| bounded step n; p < n; (q,t) : set (step p xs) |] ==> q < n"
by (unfold bounded_def, blast)
lemma monoD:
- "[| mono r step n A; p < n; s:A; s <=_r t |] ==> step p s <=_r step p t"
+ "[| mono r step n A; p < n; s\<in>A; s <=_r t |] ==> step p s <=|r| step p t"
by (unfold mono_def, blast)
(** merges **)
lemma length_merges [rule_format, simp]:
- "!ss. size(merges f t ps ss) = size ss"
+ "\<forall>ss. size(merges f ps ss) = size ss"
by (induct_tac ps, auto)
-lemma merges_preserves_type [rule_format, simp]:
- "[| semilat(A,r,f) |] ==>
- !xs. xs : list n A --> x : A --> (!p : set ps. p<n)
- --> merges f x ps xs : list n A"
- apply (frule semilatDclosedI)
- apply (unfold closed_def)
+
+lemma merges_preserves_type_lemma:
+ "[| semilat(A,r,f) |] ==>
+ \<forall>xs. xs \<in> list n A --> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
+ --> merges f ps xs \<in> list n A"
+ apply (frule semilatDclosedI)
+ apply (unfold closed_def)
apply (induct_tac ps)
- apply auto
+ apply simp
+ apply clarsimp
done
-lemma merges_incr [rule_format]:
+lemma merges_preserves_type [simp]:
+ "[| semilat(A,r,f); xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A |]
+ ==> merges f ps xs \<in> list n A"
+ by (simp add: merges_preserves_type_lemma)
+
+lemma merges_incr_lemma:
"[| semilat(A,r,f) |] ==>
- !xs. xs : list n A --> x : A --> (!p:set ps. p<size xs) --> xs <=[r] merges f x ps xs"
+ \<forall>xs. xs \<in> list n A --> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A) --> xs <=[r] merges f ps xs"
apply (induct_tac ps)
apply simp
apply simp
@@ -99,14 +148,20 @@
apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
done
+lemma merges_incr:
+ "[| semilat(A,r,f); xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A |]
+ ==> xs <=[r] merges f ps xs"
+ by (simp add: merges_incr_lemma)
+
+
lemma merges_same_conv [rule_format]:
"[| semilat(A,r,f) |] ==>
- (!xs. xs : list n A --> x:A --> (!p:set ps. p<size xs) -->
- (merges f x ps xs = xs) = (!p:set ps. x <=_r xs!p))"
+ (\<forall>xs. xs \<in> list n A --> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) -->
+ (merges f ps xs = xs) = (\<forall>(p,x)\<in>set ps. x <=_r xs!p))"
apply (induct_tac ps)
apply simp
apply clarsimp
- apply (rename_tac p ps xs)
+ apply (rename_tac p x ps xs)
apply (rule iffI)
apply (rule context_conjI)
apply (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs")
@@ -114,8 +169,11 @@
apply (erule subst, rule merges_incr)
apply assumption
apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
- apply assumption
- apply simp
+ apply clarify
+ apply (rule conjI)
+ apply simp
+ apply (blast dest: boundedD)
+ apply blast
apply clarify
apply (rotate_tac -2)
apply (erule allE)
@@ -126,6 +184,7 @@
apply (drule bspec)
apply assumption
apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
+ apply blast
apply clarify
apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
done
@@ -133,26 +192,24 @@
lemma list_update_le_listI [rule_format]:
"set xs <= A --> set ys <= A --> xs <=[r] ys --> p < size xs -->
- x <=_r ys!p --> semilat(A,r,f) --> x:A -->
+ x <=_r ys!p --> semilat(A,r,f) --> x\<in>A -->
xs[p := x +_f xs!p] <=[r] ys"
apply (unfold Listn.le_def lesub_def semilat_def)
apply (simp add: list_all2_conv_all_nth nth_list_update)
done
lemma merges_pres_le_ub:
- "[| semilat(A,r,f); t:A; set ts <= A; set ss <= A;
- !p. p:set ps --> t <=_r ts!p;
- !p. p:set ps --> p<size ts;
+ "[| semilat(A,r,f); set ts <= A; set ss <= A;
+ \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts;
ss <=[r] ts |]
- ==> merges f t ps ss <=[r] ts"
+ ==> merges f ps ss <=[r] ts"
proof -
{ fix A r f t ts ps
have
- "!!qs. [| semilat(A,r,f); set ts <= A; t:A;
- !p. p:set ps --> t <=_r ts!p;
- !p. p:set ps --> p<size ts |] ==>
+ "!!qs. [| semilat(A,r,f); set ts <= A;
+ \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts |] ==>
set qs <= set ps -->
- (!ss. set ss <= A --> ss <=[r] ts --> merges f t qs ss <=[r] ts)"
+ (\<forall>ss. set ss <= A --> ss <=[r] ts --> merges f qs ss <=[r] ts)"
apply (induct_tac qs)
apply simp
apply (simp (no_asm_simp))
@@ -160,9 +217,11 @@
apply (rotate_tac -2)
apply simp
apply (erule allE, erule impE, erule_tac [2] mp)
- apply (simp (no_asm_simp) add: closedD)
+ apply (drule bspec, assumption)
+ apply (simp add: closedD)
+ apply (drule bspec, assumption)
apply (simp add: list_update_le_listI)
- done
+ done
} note this [dest]
case rule_context
@@ -170,27 +229,19 @@
qed
-lemma nth_merges [rule_format]:
- "[| semilat (A, r, f); t:A; p < n |] ==> !ss. ss : list n A -->
- (!p:set ps. p<n) -->
- (merges f t ps ss)!p = (if p : set ps then t +_f ss!p else ss!p)"
- apply (induct_tac "ps")
- apply simp
- apply (simp add: nth_list_update closedD listE_nth_in)
- done
+(** propa **)
-(** propa **)
-
-lemma decomp_propa [rule_format]:
- "!ss w. (!q:set qs. q < size ss) -->
- propa f qs t ss w =
- (merges f t qs ss, {q. q:set qs & t +_f ss!q ~= ss!q} Un w)"
- apply (induct_tac qs)
- apply simp
+lemma decomp_propa:
+ "!!ss w. (\<forall>(q,t)\<in>set qs. q < size ss) \<Longrightarrow>
+ propa f qs ss w =
+ (merges f qs ss, {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un w)"
+ apply (induct qs)
+ apply simp
apply (simp (no_asm))
- apply clarify
- apply (rule conjI)
+ apply clarify
+ apply simp
+ apply (rule conjI)
apply (simp add: nth_list_update)
apply blast
apply (simp add: nth_list_update)
@@ -199,57 +250,240 @@
(** iter **)
+lemma plusplus_closed:
+ "\<And>y. \<lbrakk>semilat (A, r, f); set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A"
+proof (induct x)
+ show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
+ fix y x xs
+ assume sl: "semilat (A, r, f)" and y: "y \<in> A" and xs: "set (x#xs) \<subseteq> A"
+ assume IH: "\<And>y. \<lbrakk>semilat (A, r, f); set xs \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> xs ++_f y \<in> A"
+ from xs obtain x: "x \<in> A" and "set xs \<subseteq> A" by simp
+ from sl x y have "(x +_f y) \<in> A" by (simp add: closedD)
+ with sl xs have "xs ++_f (x +_f y) \<in> A" by - (rule IH)
+ thus "(x#xs) ++_f y \<in> A" by simp
+qed
+
+lemma ub2: "!!y. \<lbrakk>semilat (A, r, f); set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
+proof (induct x)
+ show "\<And>y. semilat(A, r, f) \<Longrightarrow> y <=_r [] ++_f y" by simp
+
+ fix y a l
+ assume sl: "semilat (A, r, f)"
+ assume y: "y \<in> A"
+ assume "set (a#l) \<subseteq> A"
+ then obtain a: "a \<in> A" and x: "set l \<subseteq> A" by simp
+ assume "\<And>y. \<lbrakk>semilat (A, r, f); set l \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r l ++_f y"
+ hence IH: "\<And>y. y \<in> A \<Longrightarrow> y <=_r l ++_f y" .
+
+ from sl have "order r" .. note order_trans [OF this, trans]
+
+ from sl a y have "y <=_r a +_f y" by (rule semilat_ub2)
+ also
+ from sl a y have "a +_f y \<in> A" by (simp add: closedD)
+ hence "(a +_f y) <=_r l ++_f (a +_f y)" by (rule IH)
+ finally
+ have "y <=_r l ++_f (a +_f y)" .
+ thus "y <=_r (a#l) ++_f y" by simp
+qed
+
+
+lemma ub1: "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
+proof (induct ls)
+ show "\<And>y. x \<in> set [] \<Longrightarrow> x <=_r [] ++_f y" by simp
+
+ fix y s ls
+ assume sl: "semilat (A, r, f)"
+ hence "order r" .. note order_trans [OF this, trans]
+ assume "set (s#ls) \<subseteq> A"
+ then obtain s: "s \<in> A" and ls: "set ls \<subseteq> A" by simp
+ assume y: "y \<in> A"
+
+ assume "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
+ hence IH: "\<And>y. x \<in> set ls \<Longrightarrow> y \<in> A \<Longrightarrow> x <=_r ls ++_f y" .
+
+ assume "x \<in> set (s#ls)"
+ then obtain xls: "x = s \<or> x \<in> set ls" by simp
+ moreover {
+ assume xs: "x = s"
+ from sl s y have "s <=_r s +_f y" by (rule semilat_ub1)
+ also
+ from sl s y have "s +_f y \<in> A" by (simp add: closedD)
+ with sl ls have "(s +_f y) <=_r ls ++_f (s +_f y)" by (rule ub2)
+ finally
+ have "s <=_r ls ++_f (s +_f y)" .
+ with xs have "x <=_r ls ++_f (s +_f y)" by simp
+ }
+ moreover {
+ assume "x \<in> set ls"
+ hence "\<And>y. y \<in> A \<Longrightarrow> x <=_r ls ++_f y" by (rule IH)
+ moreover
+ from sl s y
+ have "s +_f y \<in> A" by (simp add: closedD)
+ ultimately
+ have "x <=_r ls ++_f (s +_f y)" .
+ }
+ ultimately
+ have "x <=_r ls ++_f (s +_f y)" by blast
+ thus "x <=_r (s#ls) ++_f y" by simp
+qed
+
+
+lemma ub1':
+ "\<lbrakk>semilat (A, r, f); \<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk>
+ \<Longrightarrow> b <=_r map snd [(p', t')\<in>S. p' = a] ++_f y"
+proof -
+ let "b <=_r ?map ++_f y" = ?thesis
+
+ assume "semilat (A, r, f)" "y \<in> A"
+ moreover
+ assume "\<forall>(p,s) \<in> set S. s \<in> A"
+ hence "set ?map \<subseteq> A" by auto
+ moreover
+ assume "(a,b) \<in> set S"
+ hence "b \<in> set ?map" by (induct S, auto)
+ ultimately
+ show ?thesis by - (rule ub1)
+qed
+
+
+
+lemma plusplus_empty:
+ "\<forall>s'. (q, s') \<in> set S \<longrightarrow> s' +_f ss ! q = ss ! q \<Longrightarrow>
+ (map snd [(p', t')\<in> S. p' = q] ++_f ss ! q) = ss ! q"
+apply (induct S)
+apply auto
+done
+
+
lemma stable_pres_lemma:
- "[| semilat (A,r,f); pres_type step n A; bounded succs n;
- ss : list n A; p : w; ! q:w. q < n;
- ! q. q < n --> q ~: w --> stable r step succs ss q; q < n;
- q : set (succs p) --> step p (ss ! p) +_f ss ! q = ss ! q;
- q ~: w | q = p |]
- ==> stable r step succs (merges f (step p (ss!p)) (succs p) ss) q"
+ "[| semilat (A,r,f); pres_type step n A; bounded step n;
+ ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n;
+ \<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n;
+ \<forall>s'. (q,s') \<in> set (step p (ss ! p)) \<longrightarrow> s' +_f ss ! q = ss ! q;
+ q \<notin> w \<or> q = p |]
+ ==> stable r step (merges f (step p (ss!p)) ss) q"
apply (unfold stable_def)
- apply (subgoal_tac "step p (ss!p) : A")
- defer
- apply (blast intro: listE_nth_in pres_typeD)
+ apply (subgoal_tac "\<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' : A")
+ prefer 2
+ apply clarify
+ apply (erule pres_typeD)
+ prefer 3 apply assumption
+ apply (rule listE_nth_in)
+ apply assumption
+ apply simp
+ apply simp
apply simp
apply clarify
- apply (subst nth_merges)
- apply assumption
+ apply (subst nth_merges)
+ apply assumption
+ apply simp
+ apply (blast dest: boundedD)
apply assumption
- prefer 2
- apply assumption
- apply (blast dest: boundedD)
- apply (blast dest: boundedD)
- apply (subst nth_merges)
- apply assumption
- apply assumption
- prefer 2
- apply assumption
- apply (blast dest: boundedD)
- apply (blast dest: boundedD)
- apply simp
+ apply clarify
+ apply (rule conjI)
+ apply (blast dest: boundedD)
+ apply (erule pres_typeD)
+ prefer 3 apply assumption
+ apply simp
+ apply simp
+ apply (frule nth_merges [of _ _ _ q _ _ "step p (ss!p)"]) (* fixme: why does method subst not work?? *)
+ prefer 2 apply assumption
+ apply simp
+ apply clarify
apply (rule conjI)
- apply clarify
- apply (blast intro!: semilat_ub1 semilat_ub2 listE_nth_in
- intro: order_trans dest: boundedD)
- apply (blast intro!: semilat_ub1 semilat_ub2 listE_nth_in
- intro: order_trans dest: boundedD)
- done
+ apply (blast dest: boundedD)
+ apply (erule pres_typeD)
+ prefer 3 apply assumption
+ apply simp
+ apply simp
+ apply (drule_tac P = "\<lambda>x. (a, b) \<in> set (step q x)" in subst)
+ apply assumption
+
+ apply (simp add: plusplus_empty)
+ apply (cases "q \<in> w")
+ apply simp
+ apply (rule ub1')
+ apply assumption
+ apply clarify
+ apply (rule pres_typeD)
+ apply assumption
+ prefer 3 apply assumption
+ apply (blast intro: listE_nth_in dest: boundedD)
+ apply (blast intro: pres_typeD dest: boundedD)
+ apply (blast intro: listE_nth_in dest: boundedD)
+ apply assumption
-lemma merges_bounded_lemma [rule_format]:
- "[| semilat (A,r,f); mono r step n A; bounded succs n;
- step p (ss!p) : A; ss : list n A; ts : list n A; p < n;
- ss <=[r] ts; ! p. p < n --> stable r step succs ts p |]
- ==> merges f (step p (ss!p)) (succs p) ss <=[r] ts"
+ apply simp
+ apply (erule allE, erule impE, assumption, erule impE, assumption)
+ apply (rule order_trans)
+ apply simp
+ defer
+ apply (rule ub2)
+ apply assumption
+ apply simp
+ apply clarify
+ apply simp
+ apply (rule pres_typeD)
+ apply assumption
+ prefer 3 apply assumption
+ apply (blast intro: listE_nth_in dest: boundedD)
+ apply (blast intro: pres_typeD dest: boundedD)
+ apply (blast intro: listE_nth_in dest: boundedD)
+ apply blast
+ done
+
+
+lemma lesub_step_type:
+ "!!b x y. a <=|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
+apply (induct a)
+ apply simp
+apply simp
+apply (case_tac b)
+ apply simp
+apply simp
+apply (erule disjE)
+ apply clarify
+ apply (simp add: lesub_def)
+ apply blast
+apply clarify
+apply blast
+done
+
+
+lemma merges_bounded_lemma:
+ "[| semilat (A,r,f); mono r step n A; bounded step n;
+ \<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n;
+ ss <=[r] ts; ! p. p < n --> stable r step ts p |]
+ ==> merges f (step p (ss!p)) ss <=[r] ts"
apply (unfold stable_def)
- apply (blast intro!: listE_set monoD listE_nth_in le_listD less_lengthI
- intro: merges_pres_le_ub order_trans
- dest: pres_typeD boundedD)
+ apply (rule merges_pres_le_ub)
+ apply assumption
+ apply simp
+ apply simp
+ prefer 2 apply assumption
+
+ apply clarsimp
+ apply (drule boundedD, assumption+)
+ apply (erule allE, erule impE, assumption)
+ apply (drule bspec, assumption)
+ apply simp
+
+ apply (drule monoD [of _ _ _ _ p "ss!p" "ts!p"])
+ apply assumption
+ apply simp
+ apply (simp add: le_listD)
+
+ apply (drule lesub_step_type, assumption)
+ apply clarify
+ apply (drule bspec, assumption)
+ apply simp
+ apply (blast intro: order_trans)
done
lemma termination_lemma:
- "[| semilat(A,r,f); ss : list n A; t:A; ! q:set qs. q < n; p:w |] ==>
- ss <[r] merges f t qs ss |
- merges f t qs ss = ss & {q. q:set qs & t +_f ss!q ~= ss!q} Un (w-{p}) < w"
+ "[| semilat(A,r,f); ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w |] ==>
+ ss <[r] merges f qs ss \<or>
+ merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w"
apply (unfold lesssub_def)
apply (simp (no_asm_simp) add: merges_incr)
apply (rule impI)
@@ -257,88 +491,126 @@
apply assumption+
defer
apply (rule sym, assumption)
- apply (simp cong add: conj_cong add: le_iff_plus_unchanged [symmetric])
+ defer apply simp
+ apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t +_f ss ! q \<noteq> ss ! q)")
apply (blast intro!: psubsetI elim: equalityE)
- apply simp
- done
+ apply clarsimp
+ apply (drule bspec, assumption)
+ apply (drule bspec, assumption)
+ apply clarsimp
+ done
lemma iter_properties[rule_format]:
"\<lbrakk> semilat(A,r,f); acc r ; pres_type step n A; mono r step n A;
- bounded succs n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
- \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step succs ss0 p \<rbrakk> \<Longrightarrow>
- iter f step succs ss0 w0 = (ss',w')
+ bounded step n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
+ \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step ss0 p \<rbrakk> \<Longrightarrow>
+ iter f step ss0 w0 = (ss',w')
\<longrightarrow>
- ss' \<in> list n A \<and> stables r step succs ss' \<and> ss0 <=[r] ss' \<and>
- (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step succs ts \<longrightarrow> ss' <=[r] ts)"
+ ss' \<in> list n A \<and> stables r step ss' \<and> ss0 <=[r] ss' \<and>
+ (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)"
apply (unfold iter_def stables_def)
apply (rule_tac P = "%(ss,w).
- ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step succs ss p) \<and> ss0 <=[r] ss \<and>
- (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step succs ts \<longrightarrow> ss <=[r] ts) \<and>
+ ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step ss p) \<and> ss0 <=[r] ss \<and>
+ (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss <=[r] ts) \<and>
(\<forall>p\<in>w. p < n)" and
r = "{(ss',ss) . ss <[r] ss'} <*lex*> finite_psubset"
in while_rule)
-(* Invariant holds initially: *)
-apply (simp add:stables_def)
-(* Invariant is preserved: *)
+-- "Invariant holds initially:"
+apply (simp add:stables_def)
+
+-- "Invariant is preserved:"
apply(simp add: stables_def split_paired_all)
apply(rename_tac ss w)
apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
prefer 2; apply (fast intro: someI)
-apply(subgoal_tac "step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w)) \<in> A")
- prefer 2; apply (blast intro: pres_typeD listE_nth_in dest: boundedD);
- apply (subgoal_tac "\<forall>q\<in>set(succs (SOME p. p \<in> w)). q < size ss")
- prefer 2; apply(clarsimp, blast dest!: boundedD)
+apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A")
+ prefer 2
+ apply clarify
+ apply (rule conjI)
+ apply(clarsimp, blast dest!: boundedD)
+ apply (erule pres_typeD)
+ prefer 3
+ apply assumption
+ apply (erule listE_nth_in)
+ apply blast
+ apply blast
apply (subst decomp_propa)
apply blast
apply simp
apply (rule conjI)
- apply (blast intro: merges_preserves_type dest: boundedD);
-apply (rule conjI)
+ apply (erule merges_preserves_type)
+ apply blast
+ apply clarify
+ apply (rule conjI)
+ apply(clarsimp, blast dest!: boundedD)
+ apply (erule pres_typeD)
+ prefer 3
+ apply assumption
+ apply (erule listE_nth_in)
+ apply blast
+ apply blast
+apply (rule conjI)
+ apply clarify
apply (blast intro!: stable_pres_lemma)
-apply (rule conjI)
+apply (rule conjI)
apply (blast intro!: merges_incr intro: le_list_trans)
apply (rule conjI)
apply clarsimp
- apply (best intro!: merges_bounded_lemma)
+ apply (blast intro!: merges_bounded_lemma)
apply (blast dest!: boundedD)
-(* Postcondition holds upon termination: *)
-apply(clarsimp simp add: stables_def split_paired_all)
-(* Well-foundedness of the termination relation: *)
+-- "Postcondition holds upon termination:"
+apply(clarsimp simp add: stables_def split_paired_all)
+
+-- "Well-foundedness of the termination relation:"
apply (rule wf_lex_prod)
apply (drule (1) semilatDorderI [THEN acc_le_listI])
apply (simp only: acc_def lesssub_def)
-apply (rule wf_finite_psubset)
+apply (rule wf_finite_psubset)
-(* Loop decreases along termination relation: *)
+-- "Loop decreases along termination relation:"
apply(simp add: stables_def split_paired_all)
apply(rename_tac ss w)
apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
prefer 2; apply (fast intro: someI)
-apply(subgoal_tac "step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w)) \<in> A")
- prefer 2; apply (blast intro: pres_typeD listE_nth_in dest: boundedD);
- apply (subgoal_tac "\<forall>q\<in>set(succs (SOME p. p \<in> w)). q < n")
- prefer 2; apply(clarsimp, blast dest!: boundedD)
+apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A")
+ prefer 2
+ apply clarify
+ apply (rule conjI)
+ apply(clarsimp, blast dest!: boundedD)
+ apply (erule pres_typeD)
+ prefer 3
+ apply assumption
+ apply (erule listE_nth_in)
+ apply blast
+ apply blast
apply (subst decomp_propa)
- apply clarsimp
-apply clarify
+ apply blast
+apply clarify
apply (simp del: listE_length
- add: lex_prod_def finite_psubset_def decomp_propa termination_lemma
+ add: lex_prod_def finite_psubset_def
bounded_nat_set_is_finite)
-done
+apply (rule termination_lemma)
+apply assumption+
+defer
+apply assumption
+apply clarsimp
+apply (blast dest!: boundedD)
+done
+
lemma kildall_properties:
"\<lbrakk> semilat(A,r,f); acc r; pres_type step n A; mono r step n A;
- bounded succs n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow>
- kildall r f step succs ss0 : list n A \<and>
- stables r step succs (kildall r f step succs ss0) \<and>
- ss0 <=[r] kildall r f step succs ss0 \<and>
- (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step succs ts \<longrightarrow>
- kildall r f step succs ss0 <=[r] ts)";
+ bounded step n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow>
+ kildall r f step ss0 \<in> list n A \<and>
+ stables r step (kildall r f step ss0) \<and>
+ ss0 <=[r] kildall r f step ss0 \<and>
+ (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow>
+ kildall r f step ss0 <=[r] ts)"
apply (unfold kildall_def)
-apply(case_tac "iter f step succs ss0 (unstables r step succs ss0)")
+apply(case_tac "iter f step ss0 (unstables r step ss0)")
apply(simp)
apply (rule iter_properties)
apply (simp_all add: unstables_def stable_def)
@@ -346,25 +618,25 @@
lemma is_bcv_kildall:
"[| semilat(A,r,f); acc r; top r T;
- pres_type step n A; bounded succs n;
+ pres_type step n A; bounded step n;
mono r step n A |]
- ==> is_bcv r T step succs n A (kildall r f step succs)"
+ ==> is_bcv r T step n A (kildall r f step)"
apply(unfold is_bcv_def wt_step_def)
apply(insert kildall_properties[of A])
apply(simp add:stables_def)
apply clarify
-apply(subgoal_tac "kildall r f step succs ss : list n A")
+apply(subgoal_tac "kildall r f step ss \<in> list n A")
prefer 2 apply (simp(no_asm_simp))
apply (rule iffI)
- apply (rule_tac x = "kildall r f step succs ss" in bexI)
+ apply (rule_tac x = "kildall r f step ss" in bexI)
apply (rule conjI)
apply blast
apply (simp (no_asm_simp))
apply assumption
apply clarify
-apply(subgoal_tac "kildall r f step succs ss!p <=_r ts!p")
+apply(subgoal_tac "kildall r f step ss!p <=_r ts!p")
apply simp
apply (blast intro!: le_listD less_lengthI)
done
-end
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Kildall_Lift.thy Sun Dec 16 00:17:44 2001 +0100
@@ -0,0 +1,225 @@
+(* Title: HOL/MicroJava/BV/Kildall_Lift.thy
+ ID: $Id$
+ Author: Gerwin Klein
+ Copyright 2001 TUM
+*)
+
+theory Kildall_Lift = Kildall + Typing_Framework_err:
+
+constdefs
+ app_mono :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
+"app_mono r app n A ==
+ \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> app p s"
+
+ succs_stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> bool"
+"succs_stable r step == \<forall>p t t'. map fst (step p t') = map fst (step p t)"
+
+lemma succs_stableD:
+ "succs_stable r step \<Longrightarrow> map fst (step p t) = map fst (step p t')"
+ by (unfold succs_stable_def) blast
+
+lemma eqsub_def [simp]: "a <=_(op =) b = (a = b)" by (simp add: lesub_def)
+
+lemma list_le_eq [simp]: "\<And>b. a <=[op =] b = (a = b)"
+apply (induct a)
+ apply simp
+ apply rule
+ apply simp
+ apply simp
+apply (case_tac b)
+ apply simp
+apply simp
+done
+
+lemma map_err: "map_err a = zip (map fst a) (map (\<lambda>x. Err) (map snd a))"
+apply (induct a)
+apply (auto simp add: map_err_def map_snd_def)
+done
+
+lemma map_snd: "map_snd f a = zip (map fst a) (map f (map snd a))"
+apply (induct a)
+apply (auto simp add: map_snd_def)
+done
+
+lemma zipI:
+ "\<And>b c d. a <=[r1] c \<Longrightarrow> b <=[r2] d \<Longrightarrow> zip a b <=[Product.le r1 r2] zip c d"
+apply (induct a)
+ apply simp
+apply (case_tac c)
+ apply simp
+apply (case_tac b)
+ apply simp
+apply (case_tac d)
+ apply simp
+apply simp
+done
+
+lemma step_type_ord:
+ "\<And>b. a <=|r| b \<Longrightarrow> map snd a <=[r] map snd b \<and> map fst a = map fst b"
+apply (induct a)
+ apply simp
+apply (case_tac b)
+ apply simp
+apply simp
+apply (auto simp add: Product.le_def lesub_def)
+done
+
+lemma map_OK_Err:
+ "\<And>y. length y = length x \<Longrightarrow> map OK x <=[Err.le r] map (\<lambda>x. Err) y"
+apply (induct x)
+ apply simp
+apply simp
+apply (case_tac y)
+apply auto
+done
+
+lemma map_Err_Err:
+ "\<And>b. length a = length b \<Longrightarrow> map (\<lambda>x. Err) a <=[Err.le r] map (\<lambda>x. Err) b"
+apply (induct a)
+ apply simp
+apply (case_tac b)
+apply auto
+done
+
+lemma succs_stable_length:
+ "succs_stable r step \<Longrightarrow> length (step p t) = length (step p t')"
+proof -
+ assume "succs_stable r step"
+ hence "map fst (step p t) = map fst (step p t')" by (rule succs_stableD)
+ hence "length (map fst (step p t)) = length (map fst (step p t'))" by simp
+ thus ?thesis by simp
+qed
+
+lemma le_list_map_OK [simp]:
+ "\<And>b. map OK a <=[Err.le r] map OK b = (a <=[r] b)"
+ apply (induct a)
+ apply simp
+ apply simp
+ apply (case_tac b)
+ apply simp
+ apply simp
+ done
+
+lemma mono_lift:
+ "order r \<Longrightarrow> succs_stable r step \<Longrightarrow> app_mono r app n A \<Longrightarrow>
+ \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> step p s <=|r| step p t \<Longrightarrow>
+ mono (Err.le r) (err_step app step) n (err A)"
+apply (unfold app_mono_def mono_def err_step_def)
+apply clarify
+apply (case_tac s)
+ apply simp
+ apply (rule le_list_refl)
+ apply simp
+apply simp
+apply (subgoal_tac "map fst (step p arbitrary) = map fst (step p a)")
+ prefer 2
+ apply (erule succs_stableD)
+apply (case_tac t)
+ apply simp
+ apply (rule conjI)
+ apply clarify
+ apply (simp add: map_err map_snd)
+ apply (rule zipI)
+ apply simp
+ apply (rule map_OK_Err)
+ apply (subgoal_tac "length (step p arbitrary) = length (step p a)")
+ prefer 2
+ apply (erule succs_stable_length)
+ apply simp
+ apply clarify
+ apply (simp add: map_err)
+ apply (rule zipI)
+ apply simp
+ apply (rule map_Err_Err)
+ apply simp
+ apply (erule succs_stable_length)
+apply simp
+apply (elim allE)
+apply (erule impE, blast)+
+apply (rule conjI)
+ apply clarify
+ apply (simp add: map_snd)
+ apply (rule zipI)
+ apply simp
+ apply (erule succs_stableD)
+ apply (simp add: step_type_ord)
+apply clarify
+apply (rule conjI)
+ apply clarify
+ apply (simp add: map_snd map_err)
+ apply (rule zipI)
+ apply simp
+ apply (erule succs_stableD)
+ apply (rule map_OK_Err)
+ apply (simp add: succs_stable_length)
+apply clarify
+apply (simp add: map_err)
+apply (rule zipI)
+ apply simp
+ apply (erule succs_stableD)
+apply (rule map_Err_Err)
+apply (simp add: succs_stable_length)
+done
+
+lemma in_map_sndD: "(a,b) \<in> set (map_snd f xs) \<Longrightarrow> \<exists>b'. (a,b') \<in> set xs"
+apply (induct xs)
+apply (auto simp add: map_snd_def)
+done
+
+lemma bounded_lift:
+ "bounded (err_step app step) n = bounded step n"
+apply (unfold bounded_def err_step_def)
+apply rule
+apply clarify
+ apply (erule allE, erule impE, assumption)
+ apply (erule_tac x = "OK s" in allE)
+ apply simp
+ apply (case_tac "app p s")
+ apply (simp add: map_snd_def)
+ apply (drule bspec, assumption)
+ apply simp
+ apply (simp add: map_err_def map_snd_def)
+ apply (drule bspec, assumption)
+ apply simp
+apply clarify
+apply (case_tac s)
+ apply simp
+ apply (simp add: map_err_def)
+ apply (blast dest: in_map_sndD)
+apply (simp split: split_if_asm)
+ apply (blast dest: in_map_sndD)
+apply (simp add: map_err_def)
+apply (blast dest: in_map_sndD)
+done
+
+lemma set_zipD: "\<And>y. (a,b) \<in> set (zip x y) \<Longrightarrow> (a \<in> set x \<and> b \<in> set y)"
+apply (induct x)
+ apply simp
+apply (case_tac y)
+ apply simp
+apply simp
+apply blast
+done
+
+lemma pres_type_lift:
+ "\<forall>s\<in>A. \<forall>p. p < n \<longrightarrow> app p s \<longrightarrow> (\<forall>(q, s')\<in>set (step p s). s' \<in> A)
+ \<Longrightarrow> pres_type (err_step app step) n (err A)"
+apply (unfold pres_type_def err_step_def)
+apply clarify
+apply (case_tac b)
+ apply simp
+apply (case_tac s)
+ apply (simp add: map_err)
+ apply (drule set_zipD)
+ apply clarify
+ apply simp
+ apply blast
+apply (simp add: map_err split: split_if_asm)
+ apply (simp add: map_snd_def)
+ apply fastsimp
+apply (drule set_zipD)
+apply simp
+apply blast
+done
+
+end
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Sun Dec 16 00:17:44 2001 +0100
@@ -6,7 +6,12 @@
header {* Completeness of the LBV *}
-theory LBVComplete = BVSpec + LBVSpec + StepMono:
+(* This theory is currently broken. The port to exceptions
+ didn't make it into the Isabelle 2001 release. It is included for
+ documentation only. See Isabelle 99-2 for a working copy of this
+ theory. *)
+
+theory LBVComplete = BVSpec + LBVSpec + EffectMono:
constdefs
contains_targets :: "[instr list, certificate, method_type, p_count] => bool"
@@ -86,36 +91,36 @@
assume fits: "fits ins cert phi"
assume G: "G \<turnstile> s2 <=' s1"
- let "?step s" = "step i G s"
+ let "?eff s" = "eff i G s"
from wtl G
have app: "app i G mxs rT s2" by (auto simp add: wtl_inst_OK app_mono)
from wtl G
- have step: "G \<turnstile> ?step s2 <=' ?step s1"
- by (auto intro: step_mono simp add: wtl_inst_OK)
+ have eff: "G \<turnstile> ?eff s2 <=' ?eff s1"
+ by (auto intro: eff_mono simp add: wtl_inst_OK)
{ also
fix pc'
assume "pc' \<in> set (succs i pc)" "pc' \<noteq> pc+1"
with wtl
- have "G \<turnstile> ?step s1 <=' cert!pc'"
+ have "G \<turnstile> ?eff s1 <=' cert!pc'"
by (auto simp add: wtl_inst_OK)
finally
- have "G\<turnstile> ?step s2 <=' cert!pc'" .
+ have "G\<turnstile> ?eff s2 <=' cert!pc'" .
} note cert = this
have "\<exists>s2'. wtl_inst i G rT s2 cert mxs 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' = ?step s1" by (simp add: wtl_inst_OK)
+ have s1': "s1' = ?eff s1" by (simp add: wtl_inst_OK)
- have "wtl_inst i G rT s2 cert mxs mpc pc = OK (?step s2) \<and> G \<turnstile> ?step s2 <=' s1'"
+ have "wtl_inst i G rT s2 cert mxs mpc pc = OK (?eff s2) \<and> G \<turnstile> ?eff s2 <=' s1'"
(is "?wtl \<and> ?G")
proof
from True s1'
- show ?G by (auto intro: step)
+ show ?G by (auto intro: eff)
from True app wtl
show ?wtl
@@ -191,7 +196,7 @@
have pc': "!!pc'. pc' \<in> set (succs (ins!pc) pc) ==> pc' < length ins"
by (simp add: wt_instr_def)
- let ?s' = "step (ins!pc) G (phi!pc)"
+ let ?s' = "eff (ins!pc) G (phi!pc)"
from wt fits pc
have cert: "!!pc'. [|pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1|]
@@ -215,7 +220,7 @@
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)"
+ with wtl have "s = eff (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)
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Sun Dec 16 00:17:44 2001 +0100
@@ -6,72 +6,75 @@
header {* Correctness of the LBV *}
+(* This theory is currently broken. The port to exceptions
+ didn't make it into the Isabelle 2001 release. It is included for
+ documentation only. See Isabelle 99-2 for a working copy of this
+ theory. *)
+
+
theory LBVCorrect = BVSpec + LBVSpec:
lemmas [simp del] = split_paired_Ex split_paired_All
constdefs
-fits :: "[method_type,instr list,jvm_prog,ty,state_type option,nat,certificate] => bool"
-"fits phi is G rT s0 maxs cert ==
+fits :: "[method_type,instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] => bool"
+"fits phi is G rT s0 maxs maxr et cert ==
(\<forall>pc s1. pc < length is -->
- (wtl_inst_list (take pc is) G rT cert maxs (length is) 0 s0 = OK s1 -->
+ (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0 = OK s1 -->
(case cert!pc of None => phi!pc = s1
| Some t => phi!pc = Some t)))"
constdefs
-make_phi :: "[instr list,jvm_prog,ty,state_type option,nat,certificate] => method_type"
-"make_phi is G rT s0 maxs cert ==
+make_phi :: "[instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] => method_type"
+"make_phi is G rT s0 maxs maxr et cert ==
map (\<lambda>pc. case cert!pc of
- None => ok_val (wtl_inst_list (take pc is) G rT cert maxs (length is) 0 s0)
+ None => ok_val (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0)
| Some t => Some t) [0..length is(]"
lemma fitsD_None:
- "[|fits phi is G rT s0 mxs cert; pc < length is;
- wtl_inst_list (take pc is) G rT cert mxs (length is) 0 s0 = OK s1;
+ "[|fits phi is G rT s0 mxs mxr et cert; pc < length is;
+ wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0 = OK s1;
cert ! pc = None|] ==> phi!pc = s1"
by (auto simp add: fits_def)
lemma fitsD_Some:
- "[|fits phi is G rT s0 mxs cert; pc < length is;
- wtl_inst_list (take pc is) G rT cert mxs (length is) 0 s0 = OK s1;
+ "[|fits phi is G rT s0 mxs mxr et cert; pc < length is;
+ wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0 = OK s1;
cert ! pc = Some t|] ==> phi!pc = Some t"
by (auto simp add: fits_def)
lemma make_phi_Some:
"[| pc < length is; cert!pc = Some t |] ==>
- make_phi is G rT s0 mxs cert ! pc = Some t"
+ make_phi is G rT s0 mxs mxr et 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 mxs cert ! pc =
- ok_val (wtl_inst_list (take pc is) G rT cert mxs (length is) 0 s0)"
+ make_phi is G rT s0 mxs mxr et cert ! pc =
+ ok_val (wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0)"
by (simp add: make_phi_def)
lemma exists_phi:
- "\<exists>phi. fits phi is G rT s0 mxs cert"
+ "\<exists>phi. fits phi is G rT s0 mxs mxr et cert"
proof -
- have "fits (make_phi is G rT s0 mxs cert) is G rT s0 mxs cert"
+ have "fits (make_phi is G rT s0 mxs mxr et cert) is G rT s0 mxs mxr et cert"
by (auto simp add: fits_def make_phi_Some make_phi_None
split: option.splits)
-
- thus ?thesis
- by blast
+ thus ?thesis by fast
qed
lemma fits_lemma1:
- "[| wtl_inst_list is G rT cert mxs (length is) 0 s = OK s'; fits phi is G rT s mxs cert |]
+ "[| wtl_inst_list is G rT cert mxs mxr (length is) et 0 s = OK s'; fits phi is G rT s mxs mxr et cert |]
==> \<forall>pc t. pc < length is --> cert!pc = Some t --> phi!pc = Some t"
proof (intro strip)
fix pc t
- assume "wtl_inst_list is G rT cert mxs (length is) 0 s = OK s'"
- then
- obtain s'' where
- "wtl_inst_list (take pc is) G rT cert mxs (length is) 0 s = OK s''"
+ assume "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s = OK s'"
+ then obtain s'' where
+ "wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s = OK s''"
by (blast dest: wtl_take)
moreover
- assume "fits phi is G rT s mxs cert"
+ assume "fits phi is G rT s mxs mxr et cert"
"pc < length is"
"cert ! pc = Some t"
ultimately
@@ -80,42 +83,42 @@
lemma wtl_suc_pc:
- "[| wtl_inst_list is G rT cert mxs (length is) 0 s \<noteq> Err;
- wtl_inst_list (take pc is) G rT cert mxs (length is) 0 s = OK s';
- wtl_cert (is!pc) G rT s' cert mxs (length is) pc = OK s'';
- fits phi is G rT s mxs cert; Suc pc < length is |] ==>
+ "[| wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
+ wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s = OK s';
+ wtl_cert (is!pc) G rT s' cert mxs mxr (length is) et pc = OK s'';
+ fits phi is G rT s mxs mxr et cert; Suc pc < length is |] ==>
G \<turnstile> s'' <=' phi ! Suc pc"
proof -
- assume all: "wtl_inst_list is G rT cert mxs (length is) 0 s \<noteq> Err"
- assume fits: "fits phi is G rT s mxs cert"
+ assume all: "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err"
+ assume fits: "fits phi is G rT s mxs mxr et cert"
- assume wtl: "wtl_inst_list (take pc is) G rT cert mxs (length is) 0 s = OK s'" and
- wtc: "wtl_cert (is!pc) G rT s' cert mxs (length is) pc = OK s''" and
+ assume wtl: "wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s = OK s'" and
+ wtc: "wtl_cert (is!pc) G rT s' cert mxs mxr (length is) et pc = OK s''" and
pc: "Suc pc < length is"
- hence wts: "wtl_inst_list (take (Suc pc) is) G rT cert mxs (length is) 0 s = OK s''"
+ hence wts:
+ "wtl_inst_list (take (Suc pc) is) G rT cert mxs mxr (length is) et 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 mxs (length is) 0 s \<noteq> Err"
+ "wtl_inst_list (take (Suc pc) is@drop (Suc pc) is) G rT cert mxs mxr (length is) et 0 s \<noteq> Err"
by simp
from pc
have "0 < length (drop (Suc pc) is)"
by simp
- then
- obtain l ls where
+ 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 mxs (length is) (Suc pc) = OK x"
+ "wtl_cert l G rT s'' cert mxs mxr (length is) et (Suc pc) = OK x"
by (auto simp add: wtl_append min_def simp del: append_take_drop_id)
hence c1: "!!t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
- by (simp add: wtl_cert_def split: if_splits)
+ by (simp add: wtl_cert_def split: split_if_asm)
moreover
from fits pc wts
have c2: "!!t. cert!Suc pc = Some t ==> phi!Suc pc = cert!Suc pc"
@@ -125,110 +128,85 @@
have c3: "cert!Suc pc = None ==> phi!Suc pc = s''"
by (rule fitsD_None)
ultimately
-
- show ?thesis
- by - (cases "cert ! Suc pc", auto)
+ show ?thesis by (cases "cert!Suc pc", auto)
qed
lemma wtl_fits_wt:
- "[| wtl_inst_list is G rT cert mxs (length is) 0 s \<noteq> Err;
- fits phi is G rT s mxs cert; pc < length is |] ==>
- wt_instr (is!pc) G rT phi mxs (length is) pc"
+ "[| wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
+ fits phi is G rT s mxs mxr et cert; pc < length is |] ==>
+ wt_instr (is!pc) G rT phi mxs (length is) et pc"
proof -
-
- assume fits: "fits phi is G rT s mxs cert"
-
+ assume fits: "fits phi is G rT s mxs mxr et cert"
assume pc: "pc < length is" and
- wtl: "wtl_inst_list is G rT cert mxs (length is) 0 s \<noteq> Err"
-
- then
- obtain s' s'' where
- w: "wtl_inst_list (take pc is) G rT cert mxs (length is) 0 s = OK s'" and
- c: "wtl_cert (is!pc) G rT s' cert mxs (length is) pc = OK s''"
+ wtl: "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err"
+ then obtain s' s'' where
+ w: "wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s = OK s'" and
+ c: "wtl_cert (is!pc) G rT s' cert mxs mxr (length is) et pc = OK s''"
by - (drule wtl_all, auto)
- from fits wtl pc
- have cert_Some:
+ from fits wtl pc have cert_Some:
"!!t pc. [| pc < length is; cert!pc = Some t |] ==> phi!pc = Some t"
by (auto dest: fits_lemma1)
- from fits wtl pc
- have cert_None: "cert!pc = None ==> phi!pc = s'"
+ 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 mxs (length is) pc = OK s''"
- by (auto simp add: wtl_cert_def split: if_splits option.splits)
+ have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert mxs mxr (length is) et pc = OK s''"
+ by (auto simp add: wtl_cert_def split: split_if_asm option.splits)
- { fix pc'
- assume pc': "pc' \<in> set (succs (is!pc) pc)"
+ -- "we now must show that @{text wt_instr} holds; the definition
+ of @{text wt_instr} is: @{thm [display] wt_instr_def[no_vars]}"
- with wti
- have less: "pc' < length is"
- by (simp add: wtl_inst_OK)
+ { fix pc' r
+ assume pc': "(pc',r) \<in> set (eff (is!pc) G pc et (phi!pc))"
- have "G \<turnstile> step (is!pc) G (phi!pc) <=' phi ! pc'"
+ with wti have less: "pc' < length is" by (simp add: wtl_inst_OK) blast
+
+ have "G \<turnstile> r <=' 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)
-
- 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
+ have G: "G \<turnstile> r <=' cert ! pc'" by (simp add: wtl_inst_OK) blast
+ hence "cert!pc' = None ==> r = 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
}
-
- ultimately
- show ?thesis by blast
+ 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)
+ have "G \<turnstile> r <=' s''" sorry
also
- from w c fits pc wtl
- have "Suc pc < length is ==> G \<turnstile> s'' <=' phi ! Suc pc"
- by - (drule wtl_suc_pc)
+ from wtl w fits c pc
+ have "Suc pc < length is ==> G \<turnstile> s'' <=' phi ! Suc pc"
+ by - (rule wtl_suc_pc)
with True less
- have "G \<turnstile> s'' <=' phi ! Suc pc"
- by blast
- finally
- show ?thesis
- by (simp add: True)
+ have "G \<turnstile> s'' <=' phi ! Suc pc" by blast
+ finally show ?thesis by (simp add: True)
qed
- }
-
- with wti
- show ?thesis
+ }
+ with wti show ?thesis
by (auto simp add: wtl_inst_OK wt_instr_def)
qed
lemma fits_first:
- "[| 0 < length is; wtl_inst_list is G rT cert mxs (length is) 0 s \<noteq> Err;
- fits phi is G rT s mxs cert |] ==>
+ "[| 0 < length is; wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
+ fits phi is G rT s mxs mxr et cert |] ==>
G \<turnstile> s <=' phi ! 0"
proof -
- assume wtl: "wtl_inst_list is G rT cert mxs (length is) 0 s \<noteq> Err"
- assume fits: "fits phi is G rT s mxs cert"
+ assume wtl: "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err"
+ assume fits: "fits phi is G rT s mxs mxr et cert"
assume pc: "0 < length is"
from wtl
- have wt0: "wtl_inst_list (take 0 is) G rT cert mxs (length is) 0 s = OK s"
+ have wt0: "wtl_inst_list (take 0 is) G rT cert mxs mxr (length is) et 0 s = OK s"
by simp
with fits pc
@@ -244,11 +222,11 @@
by (auto simp add: neq_Nil_conv)
with wtl
obtain s' where
- "wtl_cert x G rT s cert mxs (length is) 0 = OK s'"
+ "wtl_cert x G rT s cert mxs mxr (length is) et 0 = OK s'"
by auto
hence
"!!t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
- by (simp add: wtl_cert_def split: if_splits)
+ by (simp add: wtl_cert_def split: split_if_asm)
ultimately
show ?thesis
@@ -257,18 +235,18 @@
lemma wtl_method_correct:
-"wtl_method G C pTs rT mxs mxl ins cert ==> \<exists> phi. wt_method G C pTs rT mxs mxl ins phi"
+"wtl_method G C pTs rT mxs mxl et ins cert ==> \<exists> phi. wt_method G C pTs rT mxs mxl ins et 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 mxs (length ins) 0 ?s0 \<noteq> Err"
+ assume wtl: "wtl_inst_list ins G rT cert mxs mxl (length ins) et 0 ?s0 \<noteq> Err"
- obtain phi where fits: "fits phi ins G rT ?s0 mxs cert"
+ obtain phi where fits: "fits phi ins G rT ?s0 mxs mxl et cert"
by (rule exists_phi [elim_format]) blast
with wtl
have allpc:
- "\<forall>pc. pc < length ins --> wt_instr (ins ! pc) G rT phi mxs (length ins) pc"
+ "\<forall>pc. pc < length ins --> wt_instr (ins ! pc) G rT phi mxs (length ins) et pc"
by (blast intro: wtl_fits_wt)
from pc wtl fits
@@ -285,8 +263,8 @@
proof -
assume wtl: "wtl_jvm_prog G cert"
- let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins)) = the (method (G,C) sig) in
- SOME phi. wt_method G C (snd sig) rT maxs maxl ins phi"
+ let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in
+ SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi"
{ fix C S fs mdecls sig rT code
assume "(C,S,fs,mdecls) \<in> set G" "(sig,rT,code) \<in> set mdecls"
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Sun Dec 16 00:17:44 2001 +0100
@@ -6,186 +6,227 @@
header {* The Lightweight Bytecode Verifier *}
+theory LBVSpec = Effect + Kildall:
-theory LBVSpec = Step :
+text {*
+ The Lightweight Bytecode Verifier with exceptions has not
+ made it completely into the Isabelle 2001 release. Currently
+ there is only the specification itself available. The proofs of
+ soundness and completeness are broken (they still need to be
+ ported to the exception version). Both theories are included
+ for documentation (but they don't work for this specification),
+ please see the Isabelle 99-2 release for a working copy.
+*}
types
certificate = "state_type option list"
class_certificate = "sig => certificate"
prog_certificate = "cname => class_certificate"
+consts
+ merge :: "[jvm_prog, p_count, nat, nat, p_count, certificate, (nat \<times> (state_type option)) list, state] \<Rightarrow> state"
+primrec
+ "merge G pc mxs mxr max_pc cert [] x = x"
+ "merge G pc mxs mxr max_pc cert (s#ss) x = (let (pc',s') = s in
+ if pc' < max_pc \<and> pc' = pc+1 then
+ merge G pc mxs mxr max_pc cert ss (OK s' +_(sup G mxs mxr) x)
+ else if pc' < max_pc \<and> G \<turnstile> s' <=' cert!pc' then
+ merge G pc mxs mxr max_pc cert ss x
+ else Err)"
-constdefs
- check_cert :: "[instr, jvm_prog, state_type option, certificate, p_count, p_count]
- => bool"
- "check_cert i G s cert pc max_pc == \<forall>pc' \<in> set (succs i pc). pc' < max_pc \<and>
- (pc' \<noteq> pc+1 --> G \<turnstile> step i G s <=' cert!pc')"
-
- wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,nat,p_count,p_count]
+constdefs
+ wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count]
=> state_type option err"
- "wtl_inst i G rT s cert maxs max_pc pc ==
- if app i G maxs 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))
+ "wtl_inst i G rT s cert maxs maxr max_pc et pc ==
+ if app i G maxs rT pc et s then
+ merge G pc maxs maxr max_pc cert (eff i G pc et s) (OK (cert!(pc+1)))
else Err"
-constdefs
- wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,nat,p_count,p_count]
+ wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count]
=> state_type option err"
- "wtl_cert i G rT s cert maxs max_pc pc ==
+ "wtl_cert i G rT s cert maxs maxr max_pc et pc ==
case cert!pc of
- None => wtl_inst i G rT s cert maxs max_pc pc
+ None => wtl_inst i G rT s cert maxs maxr max_pc et pc
| Some s' => if G \<turnstile> s <=' (Some s') then
- wtl_inst i G rT (Some s') cert maxs max_pc pc
+ wtl_inst i G rT (Some s') cert maxs maxr max_pc et pc
else Err"
consts
- wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,nat,p_count,p_count,
+ wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,nat,nat,p_count,exception_table,p_count,
state_type option] => state_type option err"
primrec
- "wtl_inst_list [] G rT cert maxs max_pc pc s = OK s"
- "wtl_inst_list (i#is) G rT cert maxs max_pc pc s =
- (let s' = wtl_cert i G rT s cert maxs max_pc pc in
- strict (wtl_inst_list is G rT cert maxs max_pc (pc+1)) s')"
+ "wtl_inst_list [] G rT cert maxs maxr max_pc et pc s = OK s"
+ "wtl_inst_list (i#is) G rT cert maxs maxr max_pc et pc s =
+ (let s' = wtl_cert i G rT s cert maxs maxr max_pc et pc in
+ strict (wtl_inst_list is G rT cert maxs maxr max_pc et (pc+1)) s')"
constdefs
- wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,certificate] => bool"
- "wtl_method G C pTs rT mxs mxl ins cert ==
+ wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,exception_table,instr list,certificate] => bool"
+ "wtl_method G C pTs rT mxs mxl et ins cert ==
let max_pc = length ins
in
0 < max_pc \<and>
- wtl_inst_list ins G rT cert mxs max_pc 0
+ wtl_inst_list ins G rT cert mxs mxl max_pc et 0
(Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) \<noteq> Err"
wtl_jvm_prog :: "[jvm_prog,prog_certificate] => bool"
"wtl_jvm_prog G cert ==
- wf_prog (\<lambda>G C (sig,rT,maxs,maxl,b). wtl_method G C (snd sig) rT maxs maxl b (cert C sig)) G"
+ wf_prog (\<lambda>G C (sig,rT,maxs,maxl,b,et). wtl_method G C (snd sig) rT maxs maxl et b (cert C sig)) G"
lemmas [iff] = not_Err_eq
+lemma if_eq_cases:
+ "(P \<Longrightarrow> x = z) \<Longrightarrow> (\<not>P \<Longrightarrow> y = z) \<Longrightarrow> (if P then x else y) = z"
+ by simp
+
+lemma merge_def:
+ "!!x. merge G pc mxs mxr max_pc cert ss x =
+ (if \<forall>(pc',s') \<in> set ss. pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> s' <=' cert!pc') then
+ map (OK \<circ> snd) [(p',t') \<in> ss. p'=pc+1] ++_(sup G mxs mxr) x
+ else Err)" (is "!!x. ?merge ss x = ?if ss x" is "!!x. ?P ss x")
+proof (induct ss)
+ show "!!x. ?P [] x" by simp
+next
+ have OK_snd: "(\<lambda>u. OK (snd u)) = OK \<circ> snd" by (rule ext) auto
+ fix x ss and s::"nat \<times> (state_type option)"
+ assume IH: "\<And>x. ?P ss x"
+ obtain pc' s' where s: "s = (pc',s')" by (cases s)
+ hence "?merge (s#ss) x = ?merge ((pc',s')#ss) x" by hypsubst (rule refl)
+ also
+ have "\<dots> = (if pc' < max_pc \<and> pc' = pc+1 then
+ ?merge ss (OK s' +_(sup G mxs mxr) x)
+ else if pc' < max_pc \<and> G \<turnstile> s' <=' cert!pc' then
+ ?merge ss x
+ else Err)"
+ (is "_ = (if ?pc' then ?merge ss (_ +_?f _) else if ?G then _ else _)")
+ by simp
+ also
+ let "if ?all ss then _ else _" = "?if ss x"
+ have "\<dots> = ?if ((pc',s')#ss) x"
+ proof (cases "?pc'")
+ case True
+ hence "?all (((pc',s')#ss)) = (pc+1 < max_pc \<and> ?all ss)" by simp
+ with True
+ have "?if ss (OK s' +_?f x) = ?if ((pc',s')#ss) x" by (auto simp add: OK_snd)
+ hence "?merge ss (OK s' +_?f x) = ?if ((pc',s')#ss) x" by (simp only: IH)
+ with True show ?thesis by (fast intro: if_eq_cases)
+ next
+ case False
+ have "(if ?G then ?merge ss x else Err) = ?if ((pc',s')#ss) x"
+ proof (cases ?G)
+ assume G: ?G with False
+ have "?if ss x = ?if ((pc',s')#ss) x" by (auto simp add: OK_snd)
+ hence "?merge ss x = ?if ((pc',s')#ss) x" by (simp only: IH)
+ with G show ?thesis by (fast intro: if_eq_cases)
+ next
+ assume G: "\<not>?G"
+ with False have "Err = ?if ((pc',s')#ss) x" by auto
+ with G show ?thesis by (fast intro: if_eq_cases)
+ qed
+ with False show ?thesis by (fast intro: if_eq_cases)
+ qed
+ also from s have "\<dots> = ?if (s#ss) x" by hypsubst (rule refl)
+ finally show "?P (s#ss) x" .
+qed
+
lemma wtl_inst_OK:
-"(wtl_inst i G rT s cert maxs max_pc pc = OK s') =
- (app i G maxs rT s \<and> (\<forall>pc' \<in> set (succs i pc).
- pc' < max_pc \<and> (pc' \<noteq> pc+1 --> 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)
+"(wtl_inst i G rT s cert mxs mxr max_pc et pc = OK s') = (
+ app i G mxs rT pc et s \<and>
+ (\<forall>(pc',r) \<in> set (eff i G pc et s).
+ pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> r <=' cert!pc')) \<and>
+ map (OK \<circ> snd) [(p',t') \<in> (eff i G pc et s). p'=pc+1]
+ ++_(sup G mxs mxr) (OK (cert!(pc+1))) = OK s')"
+ by (auto simp add: wtl_inst_def merge_def split: split_if_asm)
lemma wtl_Cons:
- "wtl_inst_list (i#is) G rT cert maxs max_pc pc s \<noteq> Err =
- (\<exists>s'. wtl_cert i G rT s cert maxs max_pc pc = OK s' \<and>
- wtl_inst_list is G rT cert maxs max_pc (pc+1) s' \<noteq> Err)"
+ "wtl_inst_list (i#is) G rT cert maxs maxr max_pc et pc s \<noteq> Err =
+ (\<exists>s'. wtl_cert i G rT s cert maxs maxr max_pc et pc = OK s' \<and>
+ wtl_inst_list is G rT cert maxs maxr max_pc et (pc+1) s' \<noteq> Err)"
by (auto simp del: split_paired_Ex)
lemma wtl_append:
-"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mxs mpc pc s = OK s') =
- (\<exists>s''. wtl_inst_list a G rT cert mxs mpc pc s = OK s'' \<and>
- wtl_inst_list b G rT cert mxs mpc (pc+length a) s'' = OK s')"
+"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mxs mxr mpc et pc s = OK s') =
+ (\<exists>s''. wtl_inst_list a G rT cert mxs mxr mpc et pc s = OK s'' \<and>
+ wtl_inst_list b G rT cert mxs mxr mpc et (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
-
- fix x xs
- assume IH: "?P xs"
-
+next
+ 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 mxs mpc pc")
+ proof (cases "wtl_cert x G rT s cert mxs mxr mpc et pc")
case Err thus ?thesis by simp
next
- fix s0
- assume OK: "wtl_cert x G rT s cert mxs mpc pc = OK s0"
-
- with IH
- have "?C s0 (Suc pc) xs" by blast
-
- with OK
- show ?thesis by simp
+ fix s0 assume "wtl_cert x G rT s cert mxs mxr mpc et pc = OK s0"
+ with IH have "?C s0 (Suc pc) xs" by blast
+ thus ?thesis by (simp!)
qed
qed
qed
lemma wtl_take:
- "wtl_inst_list is G rT cert mxs mpc pc s = OK s'' ==>
- \<exists>s'. wtl_inst_list (take pc' is) G rT cert mxs mpc pc s = OK s'"
+ "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s'' ==>
+ \<exists>s'. wtl_inst_list (take pc' is) G rT cert mxs mxr mpc et pc s = OK s'"
proof -
- assume "wtl_inst_list is G rT cert mxs mpc pc s = OK s''"
-
- hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mxs mpc pc s = OK s''"
+ assume "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s''"
+ hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mxs mxr mpc et pc s = OK s''"
by simp
-
- thus ?thesis
- by (auto simp add: wtl_append simp del: append_take_drop_id)
+ thus ?thesis by (auto simp add: wtl_append simp del: append_take_drop_id)
qed
lemma take_Suc:
"\<forall>n. n < length l --> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
proof (induct l)
show "?P []" by simp
-
- fix x xs
- assume IH: "?P xs"
-
+next
+ 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)
+ 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
qed
lemma wtl_Suc:
- "[| wtl_inst_list (take pc is) G rT cert maxs (length is) 0 s = OK s';
- wtl_cert (is!pc) G rT s' cert maxs (length is) pc = OK s'';
+ "[| wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s';
+ wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s'';
Suc pc < length is |] ==>
- wtl_inst_list (take (Suc pc) is) G rT cert maxs (length is) 0 s = OK s''"
+ wtl_inst_list (take (Suc pc) is) G rT cert maxs maxr (length is) et 0 s = OK s''"
proof -
- assume wtt: "wtl_inst_list (take pc is) G rT cert maxs (length is) 0 s = OK s'"
- assume wtc: "wtl_cert (is!pc) G rT s' cert maxs (length is) pc = OK s''"
- assume pc: "Suc pc < length is"
-
- hence "take (Suc pc) is = (take pc is)@[is!pc]"
- by (simp add: take_Suc)
-
- with wtt wtc pc
- show ?thesis
- by (simp add: wtl_append min_def)
+ assume "wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s'"
+ "wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s''"
+ "Suc pc < length is"
+ hence "take (Suc pc) is = (take pc is)@[is!pc]" by (simp add: take_Suc)
+ thus ?thesis by (simp! add: wtl_append min_def)
qed
lemma wtl_all:
- "[| wtl_inst_list is G rT cert maxs (length is) 0 s \<noteq> Err;
+ "[| wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err;
pc < length is |] ==>
- \<exists>s' s''. wtl_inst_list (take pc is) G rT cert maxs (length is) 0 s = OK s' \<and>
- wtl_cert (is!pc) G rT s' cert maxs (length is) pc = OK s''"
+ \<exists>s' s''. wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s' \<and>
+ wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s''"
proof -
- assume all: "wtl_inst_list is G rT cert maxs (length is) 0 s \<noteq> Err"
+ assume all: "wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err"
assume pc: "pc < length is"
hence "0 < length (drop pc is)" by simp
- then
- obtain i r where
- Cons: "drop pc is = i#r"
+ 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 maxs (length is) 0 s \<noteq> Err"
+ with all have take:
+ "wtl_inst_list (take pc is@i#r) G rT cert maxs maxr (length is) et 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)
+ 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
--- a/src/HOL/MicroJava/BV/Listn.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy Sun Dec 16 00:17:44 2001 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/BCV/Listn.thy
+(* Title: HOL/MicroJava/BV/Listn.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 2000 TUM
--- a/src/HOL/MicroJava/BV/Opt.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/Opt.thy Sun Dec 16 00:17:44 2001 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/BCV/Opt.thy
+(* Title: HOL/MicroJava/BV/Opt.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 2000 TUM
@@ -13,8 +13,8 @@
constdefs
le :: "'a ord => 'a option ord"
"le r o1 o2 == case o2 of None => o1=None |
- Some y => (case o1 of None => True |
- Some x => x <=_r y)"
+ Some y => (case o1 of None => True
+ | Some x => x <=_r y)"
opt :: "'a set => 'a option set"
"opt A == insert None {x . ? y:A. x = Some y}"
@@ -22,7 +22,7 @@
sup :: "'a ebinop => 'a option ebinop"
"sup f o1 o2 ==
case o1 of None => OK o2 | Some x => (case o2 of None => OK o1
- | Some y => (case f x y of Err => Err | OK z => OK (Some z)))"
+ | Some y => (case f x y of Err => Err | OK z => OK (Some z)))"
esl :: "'a esl => 'a option esl"
"esl == %(A,r,f). (opt A, le r, sup f)"
--- a/src/HOL/MicroJava/BV/Product.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/Product.thy Sun Dec 16 00:17:44 2001 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/BCV/Product.thy
+(* Title: HOL/MicroJava/BV/Product.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 2000 TUM
--- a/src/HOL/MicroJava/BV/Semilat.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy Sun Dec 16 00:17:44 2001 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/BCV/Semilat.thy
+(* Title: HOL/MicroJava/BV/Semilat.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 2000 TUM
--- a/src/HOL/MicroJava/BV/Step.thy Sun Dec 16 00:17:18 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,298 +0,0 @@
-(* Title: HOL/MicroJava/BV/Step.thy
- ID: $Id$
- Author: Gerwin Klein
- Copyright 2000 Technische Universitaet Muenchen
-*)
-
-header {* Effect of instructions on the state type *}
-
-
-theory Step = JVMType + JVMExec:
-
-
-text "Effect of instruction on the state type:"
-consts
-step' :: "instr \<times> jvm_prog \<times> state_type => state_type"
-
-recdef step' "{}"
-"step' (Load idx, G, (ST, LT)) = (ok_val (LT ! idx) # ST, LT)"
-"step' (Store idx, G, (ts#ST, LT)) = (ST, LT[idx:= OK ts])"
-"step' (LitPush v, G, (ST, LT)) = (the (typeof (\<lambda>v. None) v) # 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, s) = s"
-"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))"
-
-
-constdefs
- step :: "instr => jvm_prog => state_type option => state_type option"
- "step i G == option_map (\<lambda>s. step' (i,G,s))"
-
-
-text "Conditions under which step is applicable:"
-consts
-app' :: "instr \<times> jvm_prog \<times> nat \<times> ty \<times> state_type => bool"
-
-recdef app' "{}"
-"app' (Load idx, G, maxs, rT, s) = (idx < length (snd s) \<and>
- (snd s) ! idx \<noteq> Err \<and>
- length (fst s) < maxs)"
-"app' (Store idx, G, maxs, rT, (ts#ST, LT)) = (idx < length LT)"
-"app' (LitPush v, G, maxs, rT, s) = (length (fst s) < maxs \<and> typeof (\<lambda>t. None) v \<noteq> None)"
-"app' (Getfield F C, G, maxs, 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, maxs, 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, maxs, rT, s) = (is_class G C \<and> length (fst s) < maxs)"
-"app' (Checkcast C, G, maxs, rT, (RefT rt#ST,LT)) = (is_class G C)"
-"app' (Pop, G, maxs, rT, (ts#ST,LT)) = True"
-"app' (Dup, G, maxs, rT, (ts#ST,LT)) = (1+length ST < maxs)"
-"app' (Dup_x1, G, maxs, rT, (ts1#ts2#ST,LT)) = (2+length ST < maxs)"
-"app' (Dup_x2, G, maxs, rT, (ts1#ts2#ts3#ST,LT)) = (3+length ST < maxs)"
-"app' (Swap, G, maxs, rT, (ts1#ts2#ST,LT)) = True"
-"app' (IAdd, G, maxs, rT, (PrimT Integer#PrimT Integer#ST,LT))
- = True"
-"app' (Ifcmpeq b, G, maxs, 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, maxs, rT, s) = True"
-"app' (Return, G, maxs, rT, (T#ST,LT)) = (G \<turnstile> T \<preceq> rT)"
-"app' (Invoke C mn fpTs, G, maxs, 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> is_class G 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,maxs,rT,s) = False"
-
-
-constdefs
- app :: "instr => jvm_prog => nat => ty => state_type option => bool"
- "app i G maxs rT s == case s of None => True | Some t => app' (i,G,maxs,rT,t)"
-
-text {* program counter of successor instructions: *}
-
-consts
-succs :: "instr => p_count => p_count list"
-
-primrec
-"succs (Load idx) pc = [pc+1]"
-"succs (Store idx) pc = [pc+1]"
-"succs (LitPush v) 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 = [pc]"
-"succs (Invoke C mn fpTs) pc = [pc+1]"
-
-
-lemma 1: "Suc (Suc 0) < length a ==> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
-proof (cases a)
- fix x xs assume "a = x#xs" "Suc (Suc 0) < length a"
- thus ?thesis by - (cases xs, simp, cases "tl xs", auto)
-qed auto
-
-lemma 2: "\<not>(Suc (Suc 0) < length a) ==> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
-proof -;
- assume "\<not>(Suc (Suc 0) < length a)"
- hence "length a < Suc (Suc (Suc 0))" by simp
- hence * : "length a = 0 \<or> length a = Suc 0 \<or> length a = Suc (Suc 0)"
- by (auto simp add: less_Suc_eq)
-
- {
- fix x
- assume "length x = Suc 0"
- hence "\<exists> l. x = [l]" by - (cases x, auto)
- } note 0 = this
-
- have "length a = Suc (Suc 0) ==> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
- with * show ?thesis by (auto dest: 0)
-qed
-
-text {*
-\medskip
-simp rules for @{term app}
-*}
-lemma appNone[simp]:
-"app i G maxs rT None = True"
- by (simp add: app_def)
-
-
-lemma appLoad[simp]:
-"(app (Load idx) G maxs rT (Some s)) = (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err \<and> length (fst s) < maxs)"
- by (simp add: app_def)
-
-lemma appStore[simp]:
-"(app (Store idx) G maxs rT (Some s)) = (\<exists> ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)"
- by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest: 1 2 simp add: app_def)
-
-lemma appLitPush[simp]:
-"(app (LitPush v) G maxs rT (Some s)) = (length (fst s) < maxs \<and> typeof (\<lambda>v. None) v \<noteq> None)"
- by (cases s, simp add: app_def)
-
-lemma appGetField[simp]:
-"(app (Getfield F C) G maxs 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 "Suc (Suc 0) < length (fst s)", auto dest!: 1 2 simp add: app_def)
-
-lemma appPutField[simp]:
-"(app (Putfield F C) G maxs 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 "Suc (Suc 0) < length (fst s)", auto dest!: 1 2 simp add: app_def)
-
-lemma appNew[simp]:
-"(app (New C) G maxs rT (Some s)) = (is_class G C \<and> length (fst s) < maxs)"
- by (simp add: app_def)
-
-lemma appCheckcast[simp]:
-"(app (Checkcast C) G maxs 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 maxs rT (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT))"
- by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest: 1 2 simp add: app_def)
-
-
-lemma appDup[simp]:
-"(app Dup G maxs rT (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT) \<and> 1+length ST < maxs)"
- by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest: 1 2 simp add: app_def)
-
-
-lemma appDup_x1[simp]:
-"(app Dup_x1 G maxs rT (Some s)) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> 2+length ST < maxs)"
- by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest: 1 2 simp add: app_def)
-
-
-lemma appDup_x2[simp]:
-"(app Dup_x2 G maxs rT (Some s)) = (\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT) \<and> 3+length ST < maxs)"
- by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest: 1 2 simp add: app_def)
-
-
-lemma appSwap[simp]:
-"app Swap G maxs rT (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))"
- by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest: 1 2 simp add: app_def)
-
-
-lemma appIAdd[simp]:
-"app IAdd G maxs 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)"
- proof (cases "a")
- fix t ts assume a: "a = t#ts"
- show ?thesis
- proof (cases t)
- fix p assume p: "t = PrimT p"
- show ?thesis
- proof (cases p)
- assume ip: "p = Integer"
- show ?thesis
- proof (cases ts)
- fix t' ts' assume t': "ts = t' # ts'"
- show ?thesis
- proof (cases t')
- fix p' assume "t' = PrimT p'"
- with t' ip p a
- show ?thesis by - (cases p', auto 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 maxs 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 "Suc (Suc 0) < length (fst s)", auto dest: 1 2 simp add: app_def)
-
-
-lemma appReturn[simp]:
-"app Return G maxs rT (Some s) = (\<exists>T ST LT. s = (T#ST,LT) \<and> (G \<turnstile> T \<preceq> rT))"
- by (cases s, cases "Suc (Suc 0) < length (fst s)", auto dest: 1 2 simp add: app_def)
-
-lemma appGoto[simp]:
-"app (Goto branch) G maxs rT (Some s) = True"
- by (simp add: app_def)
-
-lemma appInvoke[simp]:
-"app (Invoke C mn fpTs) G maxs rT (Some s) = (\<exists>apTs X ST LT mD' rT' b'.
- s = ((rev apTs) @ (X # ST), LT) \<and> length apTs = length fpTs \<and> is_class G C \<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) ==> ?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 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 (unfold app_def, clarsimp) blast
- qed
- with Pair
- have "?app s ==> ?P s" by simp
- moreover
- have "?P s \<Longrightarrow> ?app s" by (unfold app_def) clarsimp
- ultimately
- show ?thesis by blast
-qed
-
-lemma step_Some:
- "step i G (Some s) \<noteq> None"
- by (simp add: step_def)
-
-lemma step_None [simp]:
- "step i G None = None"
- by (simp add: step_def)
-
-end
--- a/src/HOL/MicroJava/BV/StepMono.thy Sun Dec 16 00:17:18 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,454 +0,0 @@
-(* Title: HOL/MicroJava/BV/StepMono.thy
- ID: $Id$
- Author: Gerwin Klein
- Copyright 2000 Technische Universitaet Muenchen
-*)
-
-header {* Monotonicity of step and app *}
-
-theory StepMono = Step:
-
-
-lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
- by (auto elim: widen.elims)
-
-
-lemma sup_loc_some [rule_format]:
-"\<forall> y n. (G \<turnstile> b <=l y) --> n < length y --> y!n = OK t -->
- (\<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
-
- case Cons
- show "?P (a#list)"
- proof (clarsimp simp add: list_all2_Cons1 sup_loc_def Listn.le_def lesub_def)
- fix z zs n
- assume * :
- "G \<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs"
- "n < Suc (length list)" "(z # zs) ! n = OK 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_OK)
- next
- case Suc
- with Cons *
- show ?thesis by (simp add: sup_loc_def Listn.le_def lesub_def)
- qed
- qed
-qed
-
-
-lemma all_widen_is_sup_loc:
-"\<forall>b. length a = length b -->
- (\<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 --> ?Q a b" is "?P a")
-proof (induct "a")
- show "?P []" by simp
-
- fix l ls assume Cons: "?P ls"
-
- show "?P (l#ls)"
- proof (intro allI impI)
- fix b
- assume "length (l # ls) = length (b::ty list)"
- with Cons
- show "?Q (l # ls) b" by - (cases b, auto)
- qed
-qed
-
-
-lemma append_length_n [rule_format]:
-"\<forall>n. n \<le> length x --> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
-proof (induct (open) ?P x)
- show "?P []" by simp
-
- fix l ls assume Cons: "?P ls"
-
- show "?P (l#ls)"
- proof (intro allI impI)
- fix n
- assume l: "n \<le> length (l # ls)"
-
- show "\<exists>a b. l # ls = a @ b \<and> length a = n"
- proof (cases n)
- assume "n=0" thus ?thesis by simp
- next
- fix "n'" assume s: "n = Suc n'"
- with l
- have "n' \<le> length ls" by simp
- hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rule_format])
- then obtain a b where "ls = a @ b" "length a = n'" by rules
- with s have "l # ls = (l#a) @ b \<and> length (l#a) = n" by simp
- thus ?thesis by blast
- qed
- qed
-qed
-
-
-lemma rev_append_cons:
-"[|n < length x|] ==> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
-proof -
- assume n: "n < length x"
- hence "n \<le> length x" by simp
- hence "\<exists>a b. x = a @ b \<and> length a = n" by (rule append_length_n)
- then obtain r d where x: "x = r@d" "length r = n" by rules
- with n have "\<exists>b c. d = b#c" by (simp add: neq_Nil_conv)
- then obtain b c where "d = b#c" by rules
- with x have "x = (rev (rev r)) @ b # c \<and> length (rev r) = n" by simp
- thus ?thesis by blast
-qed
-
-lemmas [iff] = not_Err_eq
-
-lemma app_mono:
-"[|G \<turnstile> s <=' s'; app i G m rT s'|] ==> app i G m rT s"
-proof -
-
- { fix s1 s2
- assume G: "G \<turnstile> s2 <=s s1"
- assume app: "app i G m rT (Some s1)"
-
- have "app i G m rT (Some s2)"
- proof (cases (open) i)
- case Load
-
- from G Load app
- have "G \<turnstile> snd s2 <=l snd s1" by (auto simp add: sup_state_conv)
-
- with G Load app
- show ?thesis
- by (auto dest: sup_loc_some)
- 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_conv)
- next
- case LitPush
- with G app
- show ?thesis by simp
- next
- case New
- with G app
- show ?thesis by simp
- next
- case Getfield
- with app G
- show ?thesis
- by (cases s2) (auto 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 force
- 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) (auto simp add: sup_state_Cons2)
- 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) (auto simp add: sup_state_Cons2)
- next
- case Dup
- with app G
- show ?thesis
- by (cases s2) (clarsimp simp add: sup_state_Cons2,
- auto dest: sup_state_length)
- next
- case Dup_x1
- with app G
- show ?thesis
- by (cases s2) (clarsimp simp add: sup_state_Cons2,
- auto dest: sup_state_length)
- next
- case Dup_x2
- with app G
- show ?thesis
- by (cases s2) (clarsimp simp add: sup_state_Cons2,
- auto dest: sup_state_length)
- 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: "is_class G cname" 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 del: not_None_eq) blast+
-
- 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
- hence "\<exists>a b c. (fst s2) = rev a @ b # c \<and> length a = length list"
- by (rule rev_append_cons [rule_format])
- thus ?thesis
- by - (cases s2, elim exE conjE, simp, rule that)
- qed
-
- from l l'
- have "length (rev apTs') = length (rev apTs)" by simp
-
- from this s1 s2 G
- obtain
- G': "G \<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)
-
- from G'
- have "G \<turnstile> map OK apTs' <=l map OK apTs"
- by (simp add: sup_state_conv)
- 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)
-
- from Invoke s2 l' w' C' m c
- show ?thesis
- by (simp del: split_paired_Ex) blast
- qed
- } note this [simp]
-
- assume "G \<turnstile> s <=' s'" "app i G m rT s'"
-
- thus ?thesis
- by - (cases s, cases s', auto)
-qed
-
-lemmas [simp del] = split_paired_Ex
-lemmas [simp] = step_def
-
-lemma step_mono_Some:
-"[| app i G m 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 app2: "app i G m rT (Some s2)"
- assume G: "G \<turnstile> s1 <=s s2"
-
- hence "G \<turnstile> Some s1 <=' Some s2"
- by simp
- from this app2
- have app1: "app i G m 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 (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)
- case Load
-
- with s app1
- obtain y where
- y: "nat < length b1" "b1 ! nat = OK y" by auto
-
- from Load s app2
- obtain y' where
- y': "nat < length b2" "b2 ! nat = OK y'" by auto
-
- from G s
- have "G \<turnstile> b1 <=l b2" by (simp add: sup_state_conv)
-
- with y y'
- have "G \<turnstile> y \<preceq> y'"
- by (auto dest: sup_loc_some)
-
- with Load G y y' s step app1 app2
- show ?thesis by (auto simp add: sup_state_conv)
- next
- case Store
- with G s step app1 app2
- show ?thesis
- by (auto simp add: sup_state_conv sup_loc_update)
- next
- case LitPush
- with G s step app1 app2
- show ?thesis
- by (auto simp add: sup_state_Cons1)
- next
- case New
- with G s step app1 app2
- show ?thesis
- by (auto simp add: sup_state_Cons1)
- next
- case Getfield
- with G s step app1 app2
- show ?thesis
- by (auto simp add: sup_state_Cons1)
- next
- case Putfield
- with G s step app1 app2
- show ?thesis
- by (auto simp add: sup_state_Cons1)
- next
- case Checkcast
- with G s step app1 app2
- show ?thesis
- by (auto simp add: sup_state_Cons1)
- next
- case Invoke
-
- with s app1
- obtain a X ST where
- s1: "s1 = (a @ X # ST, b1)" and
- l: "length a = length list"
- by auto
-
- from Invoke s app2
- obtain a' X' ST' where
- s2: "s2 = (a' @ X' # ST', b2)" and
- l': "length a' = length list"
- by auto
-
- from l l'
- have lr: "length a = length a'" by simp
-
- from lr G s s1 s2
- have "G \<turnstile> (ST, b1) <=s (ST', b2)"
- by (simp add: sup_state_append_fst sup_state_Cons1)
-
- moreover
-
- from Invoke G s step app1 app2
- have "b1 = b1' \<and> b2 = b2'" by simp
-
- ultimately
-
- have "G \<turnstile> (ST, b1') <=s (ST', b2')" by simp
-
- with Invoke G s step app1 app2 s1 s2 l l'
- show ?thesis
- by (auto simp add: sup_state_conv)
- next
- case Return
- with G step
- show ?thesis
- by simp
- next
- case Pop
- with G s step app1 app2
- show ?thesis
- by (auto simp add: sup_state_Cons1)
- next
- case Dup
- with G s step app1 app2
- show ?thesis
- by (auto simp add: sup_state_Cons1)
- next
- case Dup_x1
- with G s step app1 app2
- show ?thesis
- by (auto simp add: sup_state_Cons1)
- next
- case Dup_x2
- with G s step app1 app2
- show ?thesis
- by (auto simp add: sup_state_Cons1)
- next
- case Swap
- with G s step app1 app2
- show ?thesis
- by (auto simp add: sup_state_Cons1)
- next
- case IAdd
- with G s step app1 app2
- show ?thesis
- by (auto simp add: sup_state_Cons1)
- next
- case Goto
- with G s step app1 app2
- show ?thesis by simp
- next
- case Ifcmpeq
- with G s step app1 app2
- show ?thesis
- by (auto simp add: sup_state_Cons1)
- qed
-
- with step
- show ?thesis by auto
-qed
-
-lemma step_mono:
- "[| app i G m 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
-lemmas [iff del] = not_Err_eq
-
-end
-
--- a/src/HOL/MicroJava/BV/Typing_Framework.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework.thy Sun Dec 16 00:17:44 2001 +0100
@@ -11,29 +11,28 @@
text {*
The relationship between dataflow analysis and a welltyped-insruction predicate.
*}
+types
+ 's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
constdefs
- bounded :: "(nat => nat list) => nat => bool"
-"bounded succs n == !p<n. !q:set(succs p). q<n"
+ bounded :: "'s step_type => nat => bool"
+"bounded step n == !p<n. !s. !(q,t):set(step p s). q<n"
- stable :: "'s ord =>
- (nat => 's => 's)
- => (nat => nat list) => 's list => nat => bool"
-"stable r step succs ss p == !q:set(succs p). step p (ss!p) <=_r ss!q"
+ stable :: "'s ord => 's step_type => 's list => nat => bool"
+"stable r step ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q"
- stables :: "'s ord => (nat => 's => 's)
- => (nat => nat list) => 's list => bool"
-"stables r step succs ss == !p<size ss. stable r step succs ss p"
+ stables :: "'s ord => 's step_type => 's list => bool"
+"stables r step ss == !p<size ss. stable r step ss p"
- is_bcv :: "'s ord => 's => (nat => 's => 's) => (nat => nat list)
- => nat => 's set => ('s list => 's list) => bool"
-"is_bcv r T step succs n A bcv == !ss : list n A.
+ is_bcv :: "'s ord => 's => 's step_type
+ => nat => 's set => ('s list => 's list) => bool"
+"is_bcv r T step n A bcv == !ss : list n A.
(!p<n. (bcv ss)!p ~= T) =
- (? ts: list n A. ss <=[r] ts & wt_step r T step succs ts)"
+ (? ts: list n A. ss <=[r] ts & wt_step r T step ts)"
wt_step ::
-"'s ord => 's => (nat => 's => 's) => (nat => nat list) => 's list => bool"
-"wt_step r T step succs ts ==
- !p<size(ts). ts!p ~= T & stable r step succs ts p"
+"'s ord => 's => 's step_type => 's list => bool"
+"wt_step r T step ts ==
+ !p<size(ts). ts!p ~= T & stable r step ts p"
end
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy Sun Dec 16 00:17:44 2001 +0100
@@ -11,134 +11,133 @@
constdefs
-dynamic_wt :: "'s ord => (nat => 's err => 's err) => (nat => nat list) =>
- 's err list => bool"
-"dynamic_wt r step succs ts == wt_step (Err.le r) Err step succs ts"
+dynamic_wt :: "'s ord => 's err step_type => 's err list => bool"
+"dynamic_wt r step ts == wt_step (Err.le r) Err step ts"
+
+static_wt :: "'s ord => (nat => 's => bool) => 's step_type => 's list => bool"
+"static_wt r app step ts ==
+ \<forall>p < size ts. app p (ts!p) \<and> (\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q)"
+
+map_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'c) list"
+"map_snd f == map (\<lambda>(x,y). (x, f y))"
-static_wt :: "'s ord => (nat => 's => bool) =>
- (nat => 's => 's) => (nat => nat list) => 's list => bool"
-"static_wt r app step succs ts ==
- !p < size ts. app p (ts!p) & (!q:set(succs p). step p (ts!p) <=_r ts!q)"
+map_err :: "('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b err) list"
+"map_err == map_snd (\<lambda>y. Err)"
-err_step :: "(nat => 's => bool) => (nat => 's => 's) =>
- (nat => 's err => 's err)"
-"err_step app step p == lift (%t. if app p t then OK (step p t) else Err)"
+err_step :: "(nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's err step_type"
+"err_step app step p t == case t of Err \<Rightarrow> map_err (step p arbitrary) | OK t' \<Rightarrow>
+ if app p t' then map_snd OK (step p t') else map_err (step p t')"
-non_empty :: "(nat => nat list) => bool"
-"non_empty succs == !p. succs p ~= []"
+non_empty :: "'s step_type => bool"
+"non_empty step == \<forall>p t. step p t \<noteq> []"
+lemmas err_step_defs = err_step_def map_snd_def map_err_def
+
lemma non_emptyD:
- "non_empty succs ==> ? q. q:set(succs p)"
+ "non_empty step ==> \<exists>q t'. (q,t') \<in> set(step p t)"
proof (unfold non_empty_def)
- assume "!p. succs p ~= []"
- hence "succs p ~= []" ..
- then obtain x xs where "succs p = x#xs"
+ assume "\<forall>p t. step p t \<noteq> []"
+ hence "step p t \<noteq> []" by blast
+ then obtain x xs where "step p t = x#xs"
by (auto simp add: neq_Nil_conv)
- thus ?thesis
- by auto
+ hence "x \<in> set(step p t)" by simp
+ thus ?thesis by (cases x) blast
qed
+
lemma dynamic_imp_static:
- "[| bounded succs (size ts); non_empty succs;
- dynamic_wt r (err_step app step) succs ts |]
- ==> static_wt r app step succs (map ok_val ts)"
+ "[| bounded step (size ts); non_empty step;
+ dynamic_wt r (err_step app step) ts |]
+ ==> static_wt r app step (map ok_val ts)"
proof (unfold static_wt_def, intro strip, rule conjI)
- assume b: "bounded succs (size ts)"
- assume n: "non_empty succs"
- assume wt: "dynamic_wt r (err_step app step) succs ts"
+ assume b: "bounded step (size ts)"
+ assume n: "non_empty step"
+ assume wt: "dynamic_wt r (err_step app step) ts"
fix p
assume "p < length (map ok_val ts)"
hence lp: "p < length ts" by simp
from wt lp
- have [intro?]: "!!p. p < length ts ==> ts ! p ~= Err"
+ have [intro?]: "\<And>p. p < length ts \<Longrightarrow> ts ! p \<noteq> Err"
by (unfold dynamic_wt_def wt_step_def) simp
show app: "app p (map ok_val ts ! p)"
proof -
+ from wt lp
+ obtain s where
+ OKp: "ts ! p = OK s" and
+ less: "\<forall>(q,t) \<in> set (err_step app step p (ts!p)). t <=_(Err.le r) ts!q"
+ by (unfold dynamic_wt_def wt_step_def stable_def)
+ (auto iff: not_Err_eq)
+
from n
- obtain q where q: "q:set(succs p)"
- by (auto dest: non_emptyD)
+ obtain q t where q: "(q,t) \<in> set(step p s)"
+ by (blast dest: non_emptyD)
+
+ from lp b q
+ have lq: "q < length ts" by (unfold bounded_def) blast
+ hence "ts!q \<noteq> Err" ..
+ then obtain s' where OKq: "ts ! q = OK s'" by (auto iff: not_Err_eq)
+
+ with OKp less q have "app p s"
+ by (auto simp add: err_step_defs split: err.split_asm split_if_asm)
+
+ with lp OKp show ?thesis by simp
+ qed
+
+ show "\<forall>(q,t)\<in>set(step p (map ok_val ts ! p)). t <=_r map ok_val ts ! q"
+ proof clarify
+ fix q t assume q: "(q,t) \<in> set (step p (map ok_val ts ! p))"
from wt lp q
obtain s where
OKp: "ts ! p = OK s" and
- less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q"
+ less: "\<forall>(q,t) \<in> set (err_step app step p (ts!p)). t <=_(Err.le r) ts!q"
by (unfold dynamic_wt_def wt_step_def stable_def)
(auto iff: not_Err_eq)
from lp b q
- have lq: "q < length ts"
- by (unfold bounded_def) blast
- hence "ts!q ~= Err" ..
- then
- obtain s' where OKq: "ts ! q = OK s'"
- by (auto iff: not_Err_eq)
-
- with OKp less
- have "app p s"
- by (simp add: err_step_def lift_def split: err.split_asm split_if_asm)
+ have lq: "q < length ts" by (unfold bounded_def) blast
+ hence "ts!q \<noteq> Err" ..
+ then obtain s' where OKq: "ts ! q = OK s'" by (auto iff: not_Err_eq)
- with lp OKp
- show ?thesis
- by simp
- qed
-
- show "!q:set(succs p). step p (map ok_val ts ! p) <=_r map ok_val ts ! q"
- proof (intro strip)
- fix q
- assume q: "q:set (succs p)"
-
- from wt lp q
- obtain s where
- OKp: "ts ! p = OK s" and
- less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q"
- by (unfold dynamic_wt_def wt_step_def stable_def)
- (auto iff: not_Err_eq)
-
- from lp b q
- have lq: "q < length ts"
- by (unfold bounded_def) blast
- hence "ts!q ~= Err" ..
- then
- obtain s' where OKq: "ts ! q = OK s'"
- by (auto iff: not_Err_eq)
-
- from lp lq OKp OKq app less
- show "step p (map ok_val ts ! p) <=_r map ok_val ts ! q"
- by (simp add: err_step_def lift_def)
+ from lp lq OKp OKq app less q
+ show "t <=_r map ok_val ts ! q"
+ by (auto simp add: err_step_def map_snd_def)
qed
qed
lemma static_imp_dynamic:
- "[| static_wt r app step succs ts; bounded succs (size ts) |]
- ==> dynamic_wt r (err_step app step) succs (map OK ts)"
+ "[| static_wt r app step ts; bounded step (size ts) |]
+ ==> dynamic_wt r (err_step app step) (map OK ts)"
proof (unfold dynamic_wt_def wt_step_def, intro strip, rule conjI)
- assume bounded: "bounded succs (size ts)"
- assume static: "static_wt r app step succs ts"
+ assume bounded: "bounded step (size ts)"
+ assume static: "static_wt r app step ts"
fix p assume "p < length (map OK ts)"
hence p: "p < length ts" by simp
thus "map OK ts ! p \<noteq> Err" by simp
- { fix q
- assume q: "q : set (succs p)"
+ { fix q t
+ assume q: "(q,t) \<in> set (err_step app step p (map OK ts ! p))"
with p static obtain
- "app p (ts ! p)" "step p (ts ! p) <=_r ts ! q"
+ "app p (ts ! p)" "\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q"
by (unfold static_wt_def) blast
moreover
- from q p bounded
- have "q < size ts" by (unfold bounded_def) blast
+ from q p bounded have "q < size ts"
+ by (clarsimp simp add: bounded_def err_step_defs
+ split: err.splits split_if_asm) blast+
hence "map OK ts ! q = OK (ts!q)" by simp
moreover
have "p < size ts" by (rule p)
+ moreover note q
ultimately
- have "err_step app step p (map OK ts ! p) <=_(Err.le r) map OK ts ! q"
- by (simp add: err_step_def lift_def)
+ have "t <=_(Err.le r) map OK ts ! q"
+ by (auto simp add: err_step_def map_snd_def)
}
- thus "stable (Err.le r) (err_step app step) succs (map OK ts) p"
+ thus "stable (Err.le r) (err_step app step) (map OK ts) p"
by (unfold stable_def) blast
qed