--- a/src/HOL/MicroJava/BV/LBVSpec.thy Tue Dec 05 14:08:22 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Tue Dec 05 14:08:56 2000 +0100
@@ -21,52 +21,52 @@
"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,p_count,p_count]
+ wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,nat,p_count,p_count]
=> state_type option err"
- "wtl_inst i G rT s cert max_pc pc ==
- if app i G rT s \<and> check_cert i G s cert pc max_pc then
+ "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))
else Err";
constdefs
- wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count]
+ wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,nat,p_count,p_count]
=> state_type option err"
- "wtl_cert i G rT s cert max_pc pc ==
+ "wtl_cert i G rT s cert maxs max_pc pc ==
case cert!pc of
- None => wtl_inst i G rT s cert max_pc pc
+ None => wtl_inst i G rT s cert maxs max_pc pc
| Some s' => if G \<turnstile> s <=' (Some s') then
- wtl_inst i G rT (Some s') cert max_pc pc
+ wtl_inst i G rT (Some s') cert maxs max_pc pc
else Err"
consts
- wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,p_count,p_count,
+ wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,nat,p_count,p_count,
state_type option] => state_type option err"
primrec
- "wtl_inst_list [] G rT cert max_pc pc s = OK s"
- "wtl_inst_list (i#is) G rT cert max_pc pc s =
- (let s' = wtl_cert i G rT s cert max_pc pc in
- strict (wtl_inst_list is G rT cert max_pc (pc+1)) s')";
+ "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')";
constdefs
- wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] => bool"
- "wtl_method G C pTs rT mxl ins cert ==
+ wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,certificate] => bool"
+ "wtl_method G C pTs rT mxs mxl ins cert ==
let max_pc = length ins
in
0 < max_pc \<and>
- wtl_inst_list ins G rT cert max_pc 0
+ wtl_inst_list ins G rT cert mxs max_pc 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,maxl,b). wtl_method G C (snd sig) rT maxl b (cert C sig)) G"
+ wf_prog (\<lambda>G C (sig,rT,maxs,maxl,b). wtl_method G C (snd sig) rT maxs maxl b (cert C sig)) G"
lemma wtl_inst_OK:
-"(wtl_inst i G rT s cert max_pc pc = OK s') =
- (app i G rT s \<and> (\<forall>pc' \<in> set (succs i pc).
- pc' < max_pc \<and> (pc' \<noteq> pc+1 --> G \<turnstile> step i G s <=' cert!pc')) \<and>
+"(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);
@@ -75,15 +75,15 @@
by (cases x, auto)
lemma wtl_Cons:
- "wtl_inst_list (i#is) G rT cert max_pc pc s \<noteq> Err =
- (\<exists>s'. wtl_cert i G rT s cert max_pc pc = OK s' \<and>
- wtl_inst_list is G rT cert max_pc (pc+1) s' \<noteq> Err)"
+ "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)"
by (auto simp del: split_paired_Ex)
lemma wtl_append:
-"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mpc pc s = OK s') =
- (\<exists>s''. wtl_inst_list a G rT cert mpc pc s = OK s'' \<and>
- wtl_inst_list b G rT cert mpc (pc+length a) s'' = OK s')"
+"\<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')"
(is "\<forall> s pc. ?C s pc a" is "?P a")
proof (induct ?P a)
@@ -97,11 +97,11 @@
fix s pc
show "?C s pc (x#xs)"
- proof (cases "wtl_cert x G rT s cert mpc pc")
+ proof (cases "wtl_cert x G rT s cert mxs mpc pc")
case Err thus ?thesis by simp
next
fix s0
- assume OK: "wtl_cert x G rT s cert mpc pc = OK 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
@@ -113,12 +113,12 @@
qed
lemma wtl_take:
- "wtl_inst_list is G rT cert mpc pc s = OK s'' ==>
- \<exists>s'. wtl_inst_list (take pc' is) G rT cert mpc pc s = OK s'"
+ "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'"
proof -
- assume "wtl_inst_list is G rT cert mpc pc s = OK s''"
+ 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 mpc pc s = OK s''"
+ hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mxs mpc pc s = OK s''"
by simp
thus ?thesis
@@ -144,13 +144,13 @@
qed
lemma wtl_Suc:
- "[| wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s';
- wtl_cert (is!pc) G rT s' cert (length is) pc = OK s'';
+ "[| 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'';
Suc pc < length is |] ==>
- wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = OK s''"
+ wtl_inst_list (take (Suc pc) is) G rT cert maxs (length is) 0 s = OK s''"
proof -
- assume wtt: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s'"
- assume wtc: "wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''"
+ assume 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]"
@@ -162,12 +162,12 @@
qed
lemma wtl_all:
- "[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err;
+ "[| wtl_inst_list is G rT cert maxs (length is) 0 s \<noteq> Err;
pc < length is |] ==>
- \<exists>s' s''. wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s' \<and>
- wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''"
+ \<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''"
proof -
- assume all: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
+ assume all: "wtl_inst_list is G rT cert maxs (length is) 0 s \<noteq> Err"
assume pc: "pc < length is"
hence "0 < length (drop pc is)" by simp
@@ -177,7 +177,7 @@
by (auto simp add: neq_Nil_conv simp del: length_drop)
hence "i#r = drop pc is" ..
with all
- have take: "wtl_inst_list (take pc is@i#r) G rT cert (length is) 0 s \<noteq> Err"
+ have take: "wtl_inst_list (take pc is@i#r) G rT cert maxs (length is) 0 s \<noteq> Err"
by simp
from pc
@@ -200,4 +200,14 @@
(SOME (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
by (auto simp add: unique_set)
+lemma unique_set':
+"(a,b,c,d,e)\<in>set l --> unique l --> (a',b',c',d',e') \<in> set l -->
+ a = a' --> b=b' \<and> c=c' \<and> d=d' \<and> e=e'"
+ by (induct "l") auto
+
+lemma unique_epsilon':
+ "(a,b,c,d,e)\<in>set l --> unique l -->
+ (SOME (a',b',c',d',e'). (a',b',c',d',e') \<in> set l \<and> a'=a) = (a,b,c,d,e)"
+ by (auto simp add: unique_set')
+
end