--- a/src/HOL/MicroJava/BV/BVSpec.thy Tue Dec 05 14:08:22 2000 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Tue Dec 05 14:08:56 2000 +0100
@@ -10,9 +10,9 @@
theory BVSpec = Step:
constdefs
-wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] => bool"
-"wt_instr i G rT phi max_pc pc ==
- app i G rT (phi!pc) \<and>
+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_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool"
@@ -20,17 +20,17 @@
G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
-wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] => bool"
-"wt_method G C pTs rT mxl ins phi ==
+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 max_pc pc)"
+ (\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc pc)"
wt_jvm_prog :: "[jvm_prog,prog_type] => bool"
"wt_jvm_prog G phi ==
- wf_prog (\<lambda>G C (sig,rT,maxl,b).
- wt_method G C (snd sig) rT maxl b (phi C sig)) G"
+ wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b)).
+ wt_method G C (snd sig) rT maxs maxl b (phi C sig)) G"
@@ -39,21 +39,21 @@
by (unfold wt_jvm_prog_def, blast)
lemma wt_jvm_prog_impl_wt_instr:
-"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins |]
- ==> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
+"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,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 add: wf_mdecl_def wt_method_def)
lemma wt_jvm_prog_impl_wt_start:
-"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins) |] ==>
+"[| wt_jvm_prog G phi; 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 add: wf_mdecl_def wt_method_def)
-(* for most instructions wt_instr collapses: *)
+text "for most instructions wt_instr collapses:"
lemma
-"succs i pc = [pc+1] ==> wt_instr i G rT phi max_pc pc =
- (app i G rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))"
+"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)
end
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Dec 05 14:08:22 2000 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Dec 05 14:08:56 2000 +0100
@@ -17,9 +17,9 @@
lemmas [simp del] = split_paired_All
lemma wt_jvm_prog_impl_wt_instr_cor:
- "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins);
+ "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins);
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
- ==> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"
+ ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc"
apply (unfold correct_state_def Let_def correct_frame_def)
apply simp
apply (blast intro: wt_jvm_prog_impl_wt_instr)
@@ -27,9 +27,9 @@
lemma Load_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins!pc = Load idx;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -43,9 +43,9 @@
lemma Store_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins!pc = Store idx;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -64,9 +64,9 @@
lemma Bipush_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins!pc = Bipush i;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -92,9 +92,9 @@
lemma Aconst_null_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins!pc = Aconst_null;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -122,9 +122,9 @@
lemma Checkcast_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins!pc = Checkcast D;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -136,9 +136,9 @@
lemma Getfield_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins!pc = Getfield F D;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -158,9 +158,9 @@
lemma Putfield_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins!pc = Putfield F D;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -188,9 +188,9 @@
lemma New_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins!pc = New cl_idx;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -216,17 +216,17 @@
lemma Invoke_correct:
"[| wt_jvm_prog G phi;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins ! pc = Invoke C' mn pTs;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wtprog: "wt_jvm_prog G phi"
- assume method: "method (G,C) sig = Some (C,rT,maxl,ins)"
+ assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins)"
assume ins: "ins ! pc = Invoke C' mn pTs"
- assume wti: "wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"
+ assume wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc"
assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
assume approx: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
@@ -278,7 +278,7 @@
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"
+ "length stk' = length ST"
by - (drule approx_stk_append_lemma, simp, elim, simp)
from oX
@@ -328,8 +328,8 @@
by simp
with mC' wfprog
- obtain D0 rT0 maxl0 ins0 where
- mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxl0, ins0)" "G\<turnstile>rT0\<preceq>rT"
+ 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 (auto dest: subtype_widen_methd intro: that)
from X' D
@@ -337,8 +337,8 @@
by simp
with wfprog mX
- obtain D'' rT' mxl' ins' where
- mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxl', ins')"
+ 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 (auto dest: subtype_widen_methd intro: that)
@@ -348,7 +348,7 @@
from mD wfprog
obtain mD'':
- "method (G, D'') (mn, pTs) = Some (D'', rT', mxl', ins')"
+ "method (G, D'') (mn, pTs) = Some (D'', rT', mxs', mxl', ins')"
"is_class G D''"
by (auto dest: method_in_md)
@@ -452,9 +452,9 @@
lemma Return_correct:
"[| wt_jvm_prog G phi;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins ! pc = Return;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -473,9 +473,9 @@
lemma Goto_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins ! pc = Goto branch;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -487,9 +487,9 @@
lemma Ifcmpeq_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins ! pc = Ifcmpeq branch;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -500,9 +500,9 @@
lemma Pop_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins ! pc = Pop;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -513,9 +513,9 @@
lemma Dup_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins ! pc = Dup;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -528,9 +528,9 @@
lemma Dup_x1_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins ! pc = Dup_x1;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -543,9 +543,9 @@
lemma Dup_x2_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins ! pc = Dup_x2;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -558,9 +558,9 @@
lemma Swap_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins ! pc = Swap;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -573,9 +573,9 @@
lemma IAdd_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
ins ! pc = IAdd;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
@@ -590,7 +590,7 @@
lemma instr_correct:
"[| wt_jvm_prog G phi;
- method (G,C) sig = Some (C,rT,maxl,ins);
+ method (G,C) sig = Some (C,rT,maxs,maxl,ins);
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
--- a/src/HOL/MicroJava/BV/Correct.thy Tue Dec 05 14:08:22 2000 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Tue Dec 05 14:08:56 2000 +0100
@@ -38,16 +38,16 @@
"correct_frames G hp phi rT0 sig0 (f#frs) =
(let (stk,loc,C,sig,pc) = f in
- (\<exists>ST LT rT maxl ins.
+ (\<exists>ST LT rT maxs maxl ins.
phi C sig ! pc = Some (ST,LT) \<and>
- method (G,C) sig = Some(C,rT,(maxl,ins)) \<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>
(mn,pTs) = sig0 \<and>
(\<exists>apTs D ST' LT'.
(phi C sig)!k = Some ((rev apTs) @ (Class D) # ST', LT') \<and>
length apTs = length pTs \<and>
- (\<exists>D' rT' maxl' ins'.
- method (G,D) sig0 = Some(D',rT',(maxl',ins')) \<and>
+ (\<exists>D' rT' maxs' maxl' ins'.
+ method (G,D) sig0 = Some(D',rT',(maxs',maxl',ins')) \<and>
G \<turnstile> rT0 \<preceq> rT') \<and>
correct_frame G hp (tl ST, LT) maxl ins f \<and>
correct_frames G hp phi rT sig frs))))"
@@ -63,8 +63,8 @@
| (f#fs) => G\<turnstile>h hp\<surd> \<and>
(let (stk,loc,C,sig,pc) = f
in
- \<exists>rT maxl ins s.
- method (G,C) sig = Some(C,rT,(maxl,ins)) \<and>
+ \<exists>rT maxs maxl ins s.
+ method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \<and>
phi C sig ! pc = Some s \<and>
correct_frame G hp s maxl ins f \<and>
correct_frames G hp phi rT sig fs))
--- a/src/HOL/MicroJava/BV/DFA_Framework.thy Tue Dec 05 14:08:22 2000 +0100
+++ b/src/HOL/MicroJava/BV/DFA_Framework.thy Tue Dec 05 14:08:56 2000 +0100
@@ -11,6 +11,8 @@
theory DFA_Framework = Listn:
constdefs
+ bounded :: "(nat => nat list) => nat => bool"
+"bounded succs n == !p<n. !q:set(succs p). q<n"
stable :: "'s ord =>
(nat => 's => 's)
--- a/src/HOL/MicroJava/BV/DFA_err.thy Tue Dec 05 14:08:22 2000 +0100
+++ b/src/HOL/MicroJava/BV/DFA_err.thy Tue Dec 05 14:08:56 2000 +0100
@@ -25,9 +25,6 @@
(nat => 's err => 's err)"
"err_step app step p == lift (%t. if app p t then OK (step p t) else Err)"
-bounded :: "(nat => nat list) => nat => bool"
-"bounded succs n == !p<n. !q:set(succs p). q<n"
-
non_empty :: "(nat => nat list) => bool"
"non_empty succs == !p. succs p ~= []"
--- a/src/HOL/MicroJava/BV/JType.thy Tue Dec 05 14:08:22 2000 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy Tue Dec 05 14:08:56 2000 +0100
@@ -97,6 +97,59 @@
apply (auto dest: acyclic_impl_antisym_rtrancl antisymD)
done
+lemma wf_converse_subcls1_impl_acc_subtype:
+ "wf ((subcls1 G)^-1) ==> acc (subtype G)"
+apply (unfold acc_def lesssub_def)
+apply (drule_tac p = "(subcls1 G)^-1 - Id" in wf_subset)
+ apply blast
+apply (drule wf_trancl)
+apply (simp add: wf_eq_minimal)
+apply clarify
+apply (unfold lesub_def subtype_def)
+apply (rename_tac M T)
+apply (case_tac "EX C. Class C : M")
+ prefer 2
+ apply (case_tac T)
+ apply (fastsimp simp add: PrimT_PrimT2)
+ apply simp
+ apply (subgoal_tac "ref_ty = NullT")
+ apply simp
+ apply (rule_tac x = NT in bexI)
+ apply (rule allI)
+ apply (rule impI, erule conjE)
+ apply (drule widen_RefT)
+ apply clarsimp
+ apply (case_tac t)
+ apply simp
+ apply simp
+ apply simp
+ apply (case_tac ref_ty)
+ apply simp
+ apply simp
+apply (erule_tac x = "{C. Class C : M}" in allE)
+apply auto
+apply (rename_tac D)
+apply (rule_tac x = "Class D" in bexI)
+ prefer 2
+ apply assumption
+apply clarify
+apply (frule widen_RefT)
+apply (erule exE)
+apply (case_tac t)
+ apply simp
+apply simp
+apply (insert rtrancl_r_diff_Id [symmetric, standard, of "(subcls1 G)"])
+apply simp
+apply (erule rtranclE)
+ apply blast
+apply (drule rtrancl_converseI)
+apply (subgoal_tac "((subcls1 G)-Id)^-1 = ((subcls1 G)^-1 - Id)")
+ prefer 2
+ apply blast
+apply simp
+apply (blast intro: rtrancl_into_trancl2)
+done
+
lemma closed_err_types:
"[| wf_prog wf_mb G; univalent (subcls1 G); acyclic (subcls1 G) |]
==> closed (err (types G)) (lift2 (sup G))"
@@ -234,7 +287,8 @@
ML_setup {* bind_thm ("acyclic_subcls1", acyclic_subcls1) *}
-theorem "wf_prog wf_mb G ==> err_semilat (esl G)"
+theorem err_semilat_JType_esl:
+ "wf_prog wf_mb G ==> err_semilat (esl G)"
by (frule acyclic_subcls1, frule univalent_subcls1, rule err_semilat_JType_esl_lemma)
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/JVM.thy Tue Dec 05 14:08:56 2000 +0100
@@ -0,0 +1,371 @@
+(* Title: HOL/BCV/JVM.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 2000 TUM
+
+A micro-JVM
+*)
+
+header "JVM"
+
+theory JVM = Kildall + JType + Opt + Product + DFA_err + StepMono + BVSpec:
+
+types state = "state_type option err"
+
+constdefs
+ stk_esl :: "'c prog => nat => ty list esl"
+"stk_esl S maxs == upto_esl maxs (JType.esl S)"
+
+ reg_sl :: "'c prog => nat => ty err list sl"
+"reg_sl S maxr == Listn.sl maxr (Err.sl (JType.esl S))"
+
+ sl :: "'c prog => nat => nat => state sl"
+"sl S maxs maxr ==
+ Err.sl(Opt.esl(Product.esl (stk_esl S maxs) (Err.esl(reg_sl S maxr))))"
+
+ states :: "'c prog => nat => nat => state set"
+"states S maxs maxr == fst(sl S maxs maxr)"
+
+ le :: "'c prog => nat => nat => state ord"
+"le S maxs maxr == fst(snd(sl S maxs maxr))"
+
+ sup :: "'c prog => nat => nat => state binop"
+"sup S maxs maxr == snd(snd(sl S maxs maxr))"
+
+
+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)"
+
+ kiljvm :: "jvm_prog => nat => nat => ty => instr list => state list => state list"
+ "kiljvm G maxs maxr rT bs ==
+ kildall (sl G maxs maxr) (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)"
+
+
+lemma JVM_states_unfold:
+ "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) <*>
+ list maxr (err(types S))))"
+ apply (unfold states_def JVM.sl_def Opt.esl_def Err.sl_def
+ stk_esl_def reg_sl_def Product.esl_def
+ Listn.sl_def upto_esl_def JType.esl_def Err.esl_def)
+ by simp
+
+
+lemma JVM_le_unfold:
+ "le S m n ==
+ Err.le(Opt.le(Product.le(Listn.le(subtype S))(Listn.le(Err.le(subtype S)))))"
+ apply (unfold JVM.le_def JVM.sl_def Opt.esl_def Err.sl_def
+ stk_esl_def reg_sl_def Product.esl_def
+ Listn.sl_def upto_esl_def JType.esl_def Err.esl_def)
+ by simp
+
+
+lemma Err_convert:
+ "Err.le (subtype G) a b = G \<turnstile> a <=o b"
+ by (auto simp add: Err.le_def sup_ty_opt_def lift_top_def lesub_def subtype_def
+ split: err.split)
+
+lemma loc_convert:
+ "Listn.le (Err.le (subtype G)) a b = G \<turnstile> a <=l b"
+ by (unfold Listn.le_def lesub_def sup_loc_def list_all2_def)
+ (simp add: Err_convert)
+
+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)"
+ apply (induct b)
+ apply simp
+ apply clarsimp
+ apply (case_tac aa)
+ apply simp+
+ done
+
+lemma stk_convert:
+ "Listn.le (subtype G) a b = G \<turnstile> map OK a <=l map OK b"
+proof
+ assume "Listn.le (subtype G) a b"
+
+ hence le: "list_all2 (subtype G) a b"
+ by (unfold Listn.le_def lesub_def)
+
+ { fix x' y'
+ assume "length a = length b"
+ "(x',y') \<in> set (zip (map OK a) (map OK b))"
+ then
+ obtain x y where OK:
+ "x' = OK x" "y' = OK y" "(x,y) \<in> set (zip a b)"
+ by (auto simp add: zip_map)
+ with le
+ have "subtype G x y"
+ by (simp add: list_all2_def Ball_def)
+ with OK
+ have "G \<turnstile> x' <=o y'"
+ by (simp add: subtype_def)
+ }
+
+ with le
+ show "G \<turnstile> map OK a <=l map OK b"
+ by (auto simp add: sup_loc_def list_all2_def)
+next
+ assume "G \<turnstile> map OK a <=l map OK b"
+
+ thus "Listn.le (subtype G) a b"
+ apply (unfold sup_loc_def list_all2_def Listn.le_def lesub_def)
+ apply (clarsimp simp add: zip_map subtype_def)
+ apply (drule bspec, assumption)
+ apply auto
+ done
+qed
+
+
+lemma state_conv:
+ "Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G))) a b = G \<turnstile> a <=s b"
+ by (unfold Product.le_def lesub_def sup_state_def)
+ (simp add: split_beta stk_convert loc_convert)
+
+lemma state_opt_conv:
+ "Opt.le (Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G)))) a b = G \<turnstile> a <=' b"
+ by (unfold Opt.le_def lesub_def sup_state_opt_def lift_bottom_def)
+ (auto simp add: state_conv split: option.split)
+
+lemma JVM_le_convert:
+ "le G m n (OK t1) (OK t2) = G \<turnstile> t1 <=' t2"
+ by (simp add: JVM_le_unfold Err.le_def lesub_def state_opt_conv)
+
+lemma JVM_le_Err_conv:
+ "le G m n = Err.le (sup_state_opt G)"
+ apply (simp add: expand_fun_eq)
+ apply (unfold Err.le_def JVM_le_unfold lesub_def)
+ apply (clarsimp split: err.splits)
+ apply (simp add: state_opt_conv)
+ done
+
+lemma special_ex_swap_lemma [iff]:
+ "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
+ by blast
+
+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")
+
+ apply clarsimp
+ apply clarsimp
+ apply clarsimp
+ apply clarsimp
+ apply clarsimp
+ apply clarsimp
+ defer
+ apply clarsimp
+ apply clarsimp
+ apply clarsimp
+ defer
+ apply clarsimp
+ apply clarsimp
+ apply clarsimp
+ apply clarsimp
+ apply clarsimp
+ apply clarsimp
+ apply clarsimp
+ apply clarsimp
+ apply clarsimp
+ defer
+
+ apply (simp add: Un_subset_iff)
+ apply (drule method_wf_mdecl, assumption)
+ apply (simp add: wf_mdecl_def wf_mhead_def)
+
+ apply (drule is_type_fields)
+ apply assumption
+ apply (subgoal_tac "((vname, cname), vT) \<in> set (fields (S, cname))")
+ apply assumption
+ apply (simp add: field_def)
+ apply (drule map_of_SomeD)
+ apply auto
+ done
+
+theorem exec_mono:
+ "wf_prog wf_mb G ==>
+ mono (JVM.le G maxs maxr) (exec G maxs rT bs) (size bs) (states G maxs maxr)"
+ apply (unfold mono_def)
+ 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+)
+ done
+
+theorem semilat_JVM_slI:
+ "[| wf_prog wf_mb G |] ==> semilat(sl G maxs maxr)"
+ apply (unfold JVM.sl_def stk_esl_def reg_sl_def)
+ apply (rule semilat_opt)
+ apply (rule err_semilat_Product_esl)
+ apply (rule err_semilat_upto_esl)
+ apply (rule err_semilat_JType_esl, assumption+)
+ apply (rule err_semilat_eslI)
+ apply (rule semilat_Listn_sl)
+ apply (rule err_semilat_JType_esl, assumption+)
+ done
+
+lemma sl_triple_conv:
+ "sl G maxs maxr ==
+ (states G maxs maxr, le G maxs maxr, sup G maxs maxr)"
+ by (simp (no_asm) add: states_def JVM.le_def JVM.sup_def)
+
+
+ML_setup {* bind_thm ("wf_subcls1", wf_subcls1); *}
+
+theorem is_bcv_kiljvm:
+ "[| wf_prog wf_mb G; bounded (\<lambda>pc. succs (bs!pc) pc) (size bs) |] ==>
+ is_bcv (JVM.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)"
+ apply (unfold kiljvm_def sl_triple_conv)
+ apply (rule is_bcv_kildall)
+ apply (simp (no_asm) add: sl_triple_conv [symmetric])
+ apply (force intro!: semilat_JVM_slI dest: wf_acyclic simp add: symmetric sl_triple_conv)
+ apply (simp (no_asm) add: JVM_le_unfold)
+ apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype
+ dest: wf_subcls1 wf_acyclic)
+ apply (simp add: JVM_le_unfold)
+ apply (erule exec_pres_type)
+ apply assumption
+ apply (erule exec_mono)
+ done
+
+theorem
+ "[| wf_prog wf_mb G; bounded (\<lambda>pc. succs (bs!pc) pc) (size bs);
+ 0 < size bs;
+ r = kiljvm G maxs maxr rT bs
+ (OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))#(replicate (size bs-1) (OK None)));
+ \<forall>n < size bs. r!n \<noteq> Err; maxr = Suc (length pTs + mxl);
+ 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"
+proof -
+ let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
+ #(replicate (size bs-1) (OK None))"
+
+ assume wf: "wf_prog wf_mb G"
+ assume bounded: "bounded (\<lambda>pc. succs (bs!pc) pc) (size bs)"
+ assume result: "r = kiljvm G maxs maxr rT bs ?start"
+ assume success: "\<forall>n < size bs. r!n \<noteq> Err"
+ assume instrs: "0 < size bs"
+ assume maxr: "maxr = Suc (length pTs + mxl)"
+ assume isclass: "is_class G C"
+ assume istype: "\<forall>x \<in> set pTs. is_type G x"
+
+ { 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 (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)"
+ by (rule is_bcv_kiljvm)
+
+ { 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 maxr isclass
+ have "?start \<in> list (length bs) (states G maxs maxr)"
+ apply (unfold list_def JVM_states_unfold)
+ apply simp
+ apply (rule conjI)
+ apply (simp add: Un_subset_iff)
+ apply (rule_tac B = "{Err}" in subset_trans)
+ apply (simp add: subset_replicate)
+ apply simp
+ apply (rule_tac B = "{OK None}" in subset_trans)
+ apply (simp add: subset_replicate)
+ apply simp
+ done
+
+ with bcv success result
+ have
+ "\<exists>ts\<in>list (length bs) (states G maxs maxr).
+ ?start <=[le G maxs maxr] ts \<and>
+ welltyping (JVM.le G maxs maxr) Err (JVM.exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) ts"
+ by (unfold is_bcv_def) auto
+
+ then obtain phi' where
+ l: "phi' \<in> list (length bs) (states G maxs maxr)" and
+ s: "?start <=[le G maxs maxr] phi'" and
+ w: "welltyping (le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) phi'"
+ by blast
+
+ hence dynamic:
+ "dynamic_wt (sup_state_opt G) (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) phi'"
+ by (simp add: dynamic_wt_def exec_def JVM_le_Err_conv)
+
+ from s
+ have le: "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 welltyping_def) simp
+
+ with instrs l
+ have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"
+ by clarsimp
+
+
+ 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')"
+ apply (unfold wt_method_def static_wt_def)
+ apply simp
+ apply (rule conjI)
+ apply (unfold wt_start_def)
+ apply (rule JVM_le_convert [THEN iffD1])
+ apply (simp (no_asm) add: phi0)
+ apply clarify
+ apply (erule allE, erule impE, assumption)
+ apply (elim conjE)
+ apply (clarsimp simp add: lesub_def wt_instr_def)
+ apply (unfold bounded_def)
+ apply blast
+ done
+
+ thus ?thesis by blast
+qed
+
+end
--- a/src/HOL/MicroJava/BV/Kildall.thy Tue Dec 05 14:08:22 2000 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy Tue Dec 05 14:08:56 2000 +0100
@@ -11,9 +11,6 @@
theory Kildall = DFA_Framework:
constdefs
- bounded :: "(nat => nat list) => nat => bool"
-"bounded succs n == !p<n. !q:set(succs p). q<n"
-
pres_type :: "(nat => 's => 's) => nat => 's set => bool"
"pres_type step n A == !s:A. !p<n. step p s : A"
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Tue Dec 05 14:08:22 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Tue Dec 05 14:08:56 2000 +0100
@@ -31,8 +31,8 @@
make_Cert :: "[jvm_prog, prog_type] => prog_certificate"
"make_Cert G Phi == \<lambda> C sig.
- let (C,x,y,mdecls) = SOME (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
- (sig,rT,maxl,b) = SOME (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
+ let (C,x,y,mdecls) = SOME (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
+ (sig,rT,mxs,mxl,b) = SOME (sg,rT,mxs,mxl,b). (sg,rT,mxs,mxl,b) \<in> set mdecls \<and> sg = sig
in make_cert b (Phi C sig)"
@@ -83,19 +83,19 @@
lemma wtl_inst_mono:
- "[| wtl_inst i G rT s1 cert mpc pc = OK s1'; fits ins cert phi;
+ "[| wtl_inst i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi;
pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
- \<exists> s2'. wtl_inst (ins!pc) G rT s2 cert mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')"
+ \<exists> s2'. wtl_inst (ins!pc) G rT s2 cert mxs mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')"
proof -
assume pc: "pc < length ins" "i = ins!pc"
- assume wtl: "wtl_inst i G rT s1 cert mpc pc = OK s1'"
+ assume wtl: "wtl_inst i G rT s1 cert mxs mpc pc = OK s1'"
assume fits: "fits ins cert phi"
assume G: "G \<turnstile> s2 <=' s1"
let "?step s" = "step i G s"
from wtl G
- have app: "app i G rT s2" by (auto simp add: wtl_inst_OK app_mono)
+ 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"
@@ -111,13 +111,13 @@
have "G\<turnstile> ?step s2 <=' cert!pc'" .
} note cert = this
- have "\<exists>s2'. wtl_inst i G rT s2 cert mpc pc = OK s2' \<and> G \<turnstile> s2' <=' s1'"
+ 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 "wtl_inst i G rT s2 cert mpc pc = OK (?step s2) \<and> G \<turnstile> ?step s2 <=' s1'"
+ have "wtl_inst i G rT s2 cert mxs mpc pc = OK (?step s2) \<and> G \<turnstile> ?step s2 <=' s1'"
(is "?wtl \<and> ?G")
proof
from True s1'
@@ -134,7 +134,7 @@
have "s1' = cert ! Suc pc" by (simp add: wtl_inst_OK)
with False app wtl
- have "wtl_inst i G rT s2 cert mpc pc = OK s1' \<and> G \<turnstile> s1' <=' s1'"
+ have "wtl_inst i G rT s2 cert mxs mpc pc = OK s1' \<and> G \<turnstile> s1' <=' s1'"
by (clarsimp intro!: cert simp add: wtl_inst_OK)
thus ?thesis by blast
@@ -145,11 +145,11 @@
lemma wtl_cert_mono:
- "[| wtl_cert i G rT s1 cert mpc pc = OK s1'; fits ins cert phi;
+ "[| wtl_cert i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi;
pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
- \<exists> s2'. wtl_cert (ins!pc) G rT s2 cert mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')"
+ \<exists> s2'. wtl_cert (ins!pc) G rT s2 cert mxs mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')"
proof -
- assume wtl: "wtl_cert i G rT s1 cert mpc pc = OK s1'" and
+ assume wtl: "wtl_cert i G rT s1 cert mxs mpc pc = OK s1'" and
fits: "fits ins cert phi" "pc < length ins"
"G \<turnstile> s2 <=' s1" "i = ins!pc"
@@ -167,11 +167,11 @@
by - (rule sup_state_opt_trans, auto simp add: wtl_cert_def split: if_splits)
from Some wtl
- have "wtl_inst i G rT (Some a) cert mpc pc = OK s1'"
+ have "wtl_inst i G rT (Some a) cert mxs mpc pc = OK s1'"
by (simp add: wtl_cert_def split: if_splits)
with G fits
- have "\<exists> s2'. wtl_inst (ins!pc) G rT (Some a) cert mpc pc = OK s2' \<and>
+ have "\<exists> s2'. wtl_inst (ins!pc) G rT (Some a) cert mxs mpc pc = OK s2' \<and>
(G \<turnstile> s2' <=' s1')"
by - (rule wtl_inst_mono, (simp add: wtl_cert_def)+)
@@ -182,16 +182,16 @@
lemma wt_instr_imp_wtl_inst:
- "[| wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
+ "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi;
pc < length ins; length ins = max_pc |] ==>
- wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc \<noteq> Err"
+ wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err"
proof -
- assume wt: "wt_instr (ins!pc) G rT phi max_pc pc"
+ assume wt: "wt_instr (ins!pc) G rT phi mxs max_pc pc"
assume fits: "fits ins cert phi"
assume pc: "pc < length ins" "length ins = max_pc"
from wt
- have app: "app (ins!pc) G rT (phi!pc)" by (simp add: wt_instr_def)
+ have app: "app (ins!pc) G mxs rT (phi!pc)" by (simp add: wt_instr_def)
from wt pc
have pc': "!!pc'. pc' \<in> set (succs (ins!pc) pc) ==> pc' < length ins"
@@ -210,13 +210,13 @@
qed
lemma wt_less_wtl:
- "[| wt_instr (ins!pc) G rT phi max_pc pc;
- wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = OK s;
+ "[| wt_instr (ins!pc) G rT phi mxs max_pc pc;
+ wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s;
fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==>
G \<turnstile> s <=' phi ! Suc pc"
proof -
- assume wt: "wt_instr (ins!pc) G rT phi max_pc pc"
- assume wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = OK s"
+ assume wt: "wt_instr (ins!pc) G rT phi mxs max_pc pc"
+ assume wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s"
assume fits: "fits ins cert phi"
assume pc: "Suc pc < length ins" "length ins = max_pc"
@@ -245,16 +245,16 @@
lemma wt_instr_imp_wtl_cert:
- "[| wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
+ "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi;
pc < length ins; length ins = max_pc |] ==>
- wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc \<noteq> Err"
+ wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err"
proof -
- assume "wt_instr (ins!pc) G rT phi max_pc pc" and
+ assume "wt_instr (ins!pc) G rT phi mxs max_pc pc" and
fits: "fits ins cert phi" and
pc: "pc < length ins" and
"length ins = max_pc"
- hence wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc \<noteq> Err"
+ hence wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err"
by (rule wt_instr_imp_wtl_inst)
hence "cert!pc = None ==> ?thesis"
@@ -277,20 +277,20 @@
lemma wt_less_wtl_cert:
- "[| wt_instr (ins!pc) G rT phi max_pc pc;
- wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = OK s;
+ "[| wt_instr (ins!pc) G rT phi mxs max_pc pc;
+ wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s;
fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==>
G \<turnstile> s <=' phi ! Suc pc"
proof -
- assume wtl: "wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = OK s"
+ assume wtl: "wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s"
- assume wti: "wt_instr (ins!pc) G rT phi max_pc pc"
+ assume wti: "wt_instr (ins!pc) G rT phi mxs max_pc pc"
"fits ins cert phi"
"Suc pc < length ins" "length ins = max_pc"
{ assume "cert!pc = None"
with wtl
- have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = OK s"
+ have "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s"
by (simp add: wtl_cert_def)
with wti
have ?thesis
@@ -303,7 +303,7 @@
have "cert!pc = phi!pc"
by - (rule fitsD2, simp+)
with c wtl
- have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = OK s"
+ have "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s"
by (simp add: wtl_cert_def)
with wti
have ?thesis
@@ -322,12 +322,12 @@
theorem wt_imp_wtl_inst_list:
"\<forall> pc. (\<forall>pc'. pc' < length all_ins -->
- wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') -->
+ wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc') -->
fits all_ins cert phi -->
(\<exists>l. pc = length l \<and> all_ins = l@ins) -->
pc < length all_ins -->
(\<forall> s. (G \<turnstile> s <=' (phi!pc)) -->
- wtl_inst_list ins G rT cert (length all_ins) pc s \<noteq> Err)"
+ wtl_inst_list ins G rT cert mxs (length all_ins) pc s \<noteq> Err)"
(is "\<forall>pc. ?wt --> ?fits --> ?l pc ins --> ?len pc --> ?wtl pc ins"
is "\<forall>pc. ?C pc ins" is "?P ins")
proof (induct "?P" "ins")
@@ -341,7 +341,7 @@
proof (intro allI impI, elim exE conjE)
fix pc s l
assume wt : "\<forall>pc'. pc' < length all_ins -->
- wt_instr (all_ins ! pc') G rT phi (length all_ins) pc'"
+ wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc'"
assume fits: "fits all_ins cert phi"
assume l : "pc < length all_ins"
assume G : "G \<turnstile> s <=' phi ! pc"
@@ -350,10 +350,10 @@
by (simp add: nth_append)
from l wt
- have wti: "wt_instr (all_ins!pc) G rT phi (length all_ins) pc" by blast
+ have wti: "wt_instr (all_ins!pc) G rT phi mxs (length all_ins) pc" by blast
with fits l
- have c: "wtl_cert (all_ins!pc) G rT (phi!pc) cert (length all_ins) pc \<noteq> Err"
+ have c: "wtl_cert (all_ins!pc) G rT (phi!pc) cert mxs (length all_ins) pc \<noteq> Err"
by - (drule wt_instr_imp_wtl_cert, auto)
from Cons
@@ -361,7 +361,7 @@
with wt fits pc
have IH: "?len (Suc pc) --> ?wtl (Suc pc) ins'" by auto
- show "wtl_inst_list (i#ins') G rT cert (length all_ins) pc s \<noteq> Err"
+ show "wtl_inst_list (i#ins') G rT cert mxs (length all_ins) pc s \<noteq> Err"
proof (cases "?len (Suc pc)")
case False
with pc
@@ -375,13 +375,13 @@
from c wti fits l True
obtain s'' where
- "wtl_cert (all_ins!pc) G rT (phi!pc) cert (length all_ins) pc = OK s''"
+ "wtl_cert (all_ins!pc) G rT (phi!pc) cert mxs (length all_ins) pc = OK s''"
"G \<turnstile> s'' <=' phi ! Suc pc"
by clarsimp (drule wt_less_wtl_cert, auto)
moreover
from calculation fits G l
obtain s' where
- c': "wtl_cert (all_ins!pc) G rT s cert (length all_ins) pc = OK s'" and
+ c': "wtl_cert (all_ins!pc) G rT s cert mxs (length all_ins) pc = OK s'" and
"G \<turnstile> s' <=' s''"
by - (drule wtl_cert_mono, auto)
ultimately
@@ -389,7 +389,7 @@
by - (rule sup_state_opt_trans)
with wtl
- have "wtl_inst_list ins' G rT cert (length all_ins) (Suc pc) s' \<noteq> Err"
+ have "wtl_inst_list ins' G rT cert mxs (length all_ins) (Suc pc) s' \<noteq> Err"
by auto
with i c'
@@ -400,17 +400,17 @@
lemma fits_imp_wtl_method_complete:
- "[| wt_method G C pTs rT mxl ins phi; fits ins cert phi |] ==>
- wtl_method G C pTs rT mxl ins cert"
+ "[| wt_method G C pTs rT mxs mxl ins phi; fits ins cert phi |]
+ ==> wtl_method G C pTs rT mxs mxl ins cert"
by (simp add: wt_method_def wtl_method_def)
(rule wt_imp_wtl_inst_list [rule_format, elim_format], auto simp add: wt_start_def)
lemma wtl_method_complete:
- "wt_method G C pTs rT mxl ins phi ==>
- wtl_method G C pTs rT mxl ins (make_cert ins phi)"
+ "wt_method G C pTs rT mxs mxl ins phi
+ ==> wtl_method G C pTs rT mxs mxl ins (make_cert ins phi)"
proof -
- assume "wt_method G C pTs rT mxl ins phi"
+ assume "wt_method G C pTs rT mxs mxl ins phi"
moreover
have "fits ins (make_cert ins phi) phi"
by (rule fits_make_cert)
@@ -425,16 +425,16 @@
proof (unfold wt_jvm_prog_def)
assume wfprog:
- "wf_prog (\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G"
+ "wf_prog (\<lambda>G C (sig,rT,mxs,mxl,b). wt_method G C (snd sig) rT mxs mxl b (Phi C sig)) G"
thus ?thesis
proof (simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def wf_mdecl_def, auto)
- fix a aa ab b ac ba ad ae bb
+ fix a aa ab b ac ba ad ae af bb
assume 1 : "\<forall>(C,sc,fs,ms)\<in>set G.
Ball (set fs) (wf_fdecl G) \<and>
unique fs \<and>
(\<forall>(sig,rT,mb)\<in>set ms. wf_mhead G sig rT \<and>
- (\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \<and>
+ (\<lambda>(mxs,mxl,b). wt_method G C (snd sig) rT mxs mxl b (Phi C sig)) mb) \<and>
unique ms \<and>
(case sc of None => C = Object
| Some D =>
@@ -443,24 +443,24 @@
(\<forall>(sig,rT,b)\<in>set ms.
\<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') --> G\<turnstile>rT\<preceq>rT'))"
"(a, aa, ab, b) \<in> set G"
-
+
assume uG : "unique G"
- assume b : "((ac, ba), ad, ae, bb) \<in> set b"
-
+ assume b : "((ac, ba), ad, ae, af, bb) \<in> set b"
+
from 1
- show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))"
+ show "wtl_method G a ba ad ae af bb (make_Cert G Phi a (ac, ba))"
proof (rule bspec [elim_format], clarsimp)
assume ub : "unique b"
assume m: "\<forall>(sig,rT,mb)\<in>set b. wf_mhead G sig rT \<and>
- (\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb"
+ (\<lambda>(mxs,mxl,b). wt_method G a (snd sig) rT mxs mxl b (Phi a sig)) mb"
from m b
show ?thesis
proof (rule bspec [elim_format], clarsimp)
- assume "wt_method G a ba ad ae bb (Phi a (ac, ba))"
+ assume "wt_method G a ba ad ae af bb (Phi a (ac, ba))"
with wfprog uG ub b 1
show ?thesis
by - (rule wtl_method_complete [elim_format], assumption+,
- simp add: make_Cert_def unique_epsilon)
+ simp add: make_Cert_def unique_epsilon unique_epsilon')
qed
qed
qed
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Tue Dec 05 14:08:22 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Tue Dec 05 14:08:56 2000 +0100
@@ -11,48 +11,48 @@
lemmas [simp del] = split_paired_Ex split_paired_All
constdefs
-fits :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] => bool"
-"fits phi is G rT s0 cert ==
+fits :: "[method_type,instr list,jvm_prog,ty,state_type option,nat,certificate] => bool"
+"fits phi is G rT s0 maxs cert ==
(\<forall>pc s1. pc < length is -->
- (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = OK s1 -->
+ (wtl_inst_list (take pc is) G rT cert maxs (length is) 0 s0 = OK s1 -->
(case cert!pc of None => phi!pc = s1
| Some t => phi!pc = Some t)))"
constdefs
-make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] => method_type"
-"make_phi is G rT s0 cert ==
+make_phi :: "[instr list,jvm_prog,ty,state_type option,nat,certificate] => method_type"
+"make_phi is G rT s0 maxs cert ==
map (\<lambda>pc. case cert!pc of
- None => ok_val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)
+ None => ok_val (wtl_inst_list (take pc is) G rT cert maxs (length is) 0 s0)
| Some t => Some t) [0..length is(]"
lemma fitsD_None:
- "[|fits phi is G rT s0 cert; pc < length is;
- wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = OK s1;
+ "[|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;
cert ! pc = None|] ==> phi!pc = s1"
by (auto simp add: fits_def)
lemma fitsD_Some:
- "[|fits phi is G rT s0 cert; pc < length is;
- wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = OK s1;
+ "[|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;
cert ! pc = Some t|] ==> phi!pc = Some t"
by (auto simp add: fits_def)
lemma make_phi_Some:
"[| pc < length is; cert!pc = Some t |] ==>
- make_phi is G rT s0 cert ! pc = Some t"
+ make_phi is G rT s0 mxs cert ! pc = Some t"
by (simp add: make_phi_def)
lemma make_phi_None:
"[| pc < length is; cert!pc = None |] ==>
- make_phi is G rT s0 cert ! pc =
- ok_val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)"
+ 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)"
by (simp add: make_phi_def)
lemma exists_phi:
- "\<exists>phi. fits phi is G rT s0 cert"
+ "\<exists>phi. fits phi is G rT s0 mxs cert"
proof -
- have "fits (make_phi is G rT s0 cert) is G rT s0 cert"
+ have "fits (make_phi is G rT s0 mxs cert) is G rT s0 mxs cert"
by (auto simp add: fits_def make_phi_Some make_phi_None
split: option.splits)
@@ -61,17 +61,17 @@
qed
lemma fits_lemma1:
- "[| wtl_inst_list is G rT cert (length is) 0 s = OK s'; fits phi is G rT s cert |]
+ "[| wtl_inst_list is G rT cert mxs (length is) 0 s = OK s'; fits phi is G rT s mxs 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 (length is) 0 s = OK s'"
+ 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 (length is) 0 s = OK s''"
+ "wtl_inst_list (take pc is) G rT cert mxs (length is) 0 s = OK s''"
by (blast dest: wtl_take)
moreover
- assume "fits phi is G rT s cert"
+ assume "fits phi is G rT s mxs cert"
"pc < length is"
"cert ! pc = Some t"
ultimately
@@ -80,26 +80,26 @@
lemma wtl_suc_pc:
- "[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err;
- wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s';
- wtl_cert (is!pc) G rT s' cert (length is) pc = OK s'';
- fits phi is G rT s cert; Suc pc < length is |] ==>
+ "[| 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 |] ==>
G \<turnstile> s'' <=' phi ! Suc pc"
proof -
- assume all: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
- assume fits: "fits phi is G rT s cert"
+ assume 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 wtl: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s'" and
- wtc: "wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''" and
+ 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
pc: "Suc pc < length is"
- hence wts: "wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = OK s''"
+ hence wts: "wtl_inst_list (take (Suc pc) is) G rT cert mxs (length is) 0 s = OK s''"
by (rule wtl_Suc)
from all
have app:
- "wtl_inst_list (take (Suc pc) is@drop (Suc pc) is) G rT cert (length is) 0 s \<noteq> Err"
+ "wtl_inst_list (take (Suc pc) is@drop (Suc pc) is) G rT cert mxs (length is) 0 s \<noteq> Err"
by simp
from pc
@@ -111,7 +111,7 @@
by (auto simp add: neq_Nil_conv simp del: length_drop)
with app wts pc
obtain x where
- "wtl_cert l G rT s'' cert (length is) (Suc pc) = OK x"
+ "wtl_cert l G rT s'' cert mxs (length is) (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"
@@ -132,20 +132,20 @@
lemma wtl_fits_wt:
- "[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err;
- fits phi is G rT s cert; pc < length is |] ==>
- wt_instr (is!pc) G rT phi (length is) pc"
+ "[| 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"
proof -
- assume fits: "fits phi is G rT s cert"
+ assume fits: "fits phi is G rT s mxs cert"
assume pc: "pc < length is" and
- wtl: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
+ 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 (length is) 0 s = OK s'" and
- c: "wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''"
+ 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''"
by - (drule wtl_all, auto)
from fits wtl pc
@@ -158,7 +158,7 @@
by - (drule fitsD_None)
from pc c cert_None cert_Some
- have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert (length is) pc = OK s''"
+ 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)
{ fix pc'
@@ -219,16 +219,16 @@
lemma fits_first:
- "[| 0 < length is; wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err;
- fits phi is G rT s cert |] ==>
+ "[| 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 |] ==>
G \<turnstile> s <=' phi ! 0"
proof -
- assume wtl: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
- assume fits: "fits phi is G rT s cert"
+ assume 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 pc: "0 < length is"
from wtl
- have wt0: "wtl_inst_list (take 0 is) G rT cert (length is) 0 s = OK s"
+ have wt0: "wtl_inst_list (take 0 is) G rT cert mxs (length is) 0 s = OK s"
by simp
with fits pc
@@ -244,7 +244,7 @@
by (simp add: neq_Nil_conv) (elim, rule that)
with wtl
obtain s' where
- "wtl_cert x G rT s cert (length is) 0 = OK s'"
+ "wtl_cert x G rT s cert mxs (length is) 0 = OK s'"
by simp (elim, rule that, simp)
hence
"!!t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
@@ -257,18 +257,18 @@
lemma wtl_method_correct:
-"wtl_method G C pTs rT mxl ins cert ==> \<exists> phi. wt_method G C pTs rT mxl ins phi"
+"wtl_method G C pTs rT mxs mxl ins cert ==> \<exists> phi. wt_method G C pTs rT mxs mxl ins phi"
proof (unfold wtl_method_def, simp only: Let_def, elim conjE)
let "?s0" = "Some ([], OK (Class C) # map OK pTs @ replicate mxl Err)"
assume pc: "0 < length ins"
- assume wtl: "wtl_inst_list ins G rT cert (length ins) 0 ?s0 \<noteq> Err"
+ assume wtl: "wtl_inst_list ins G rT cert mxs (length ins) 0 ?s0 \<noteq> Err"
- obtain phi where fits: "fits phi ins G rT ?s0 cert"
+ obtain phi where fits: "fits phi ins G rT ?s0 mxs cert"
by (rule exists_phi [elim_format]) blast
with wtl
have allpc:
- "\<forall>pc. pc < length ins --> wt_instr (ins ! pc) G rT phi (length ins) pc"
+ "\<forall>pc. pc < length ins --> wt_instr (ins ! pc) G rT phi mxs (length ins) pc"
by (blast intro: wtl_fits_wt)
from pc wtl fits
@@ -290,40 +290,40 @@
from wtl_prog
show uniqueG: "unique G" by (simp add: wtl_jvm_prog_def wf_prog_def)
- show "\<exists>Phi. Ball (set G) (wf_cdecl (\<lambda>G C (sig,rT,maxl,b).
- wt_method G C (snd sig) rT maxl b (Phi C sig)) G)"
+ show "\<exists>Phi. Ball (set G) (wf_cdecl (\<lambda>G C (sig,rT,maxs,maxl,b).
+ wt_method G C (snd sig) rT maxs maxl b (Phi C sig)) G)"
(is "\<exists>Phi. ?Q Phi")
proof (intro exI)
let "?Phi" = "\<lambda> C sig.
let (C,x,y,mdecls) = SOME (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
- (sig,rT,maxl,b) = SOME (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
- in SOME phi. wt_method G C (snd sig) rT maxl b phi"
+ (sig,rT,maxs,maxl,b) = SOME (sg,rT,maxs,maxl,b). (sg,rT,maxs,maxl,b) \<in> set mdecls \<and> sg = sig
+ in SOME phi. wt_method G C (snd sig) rT maxs maxl b phi"
from wtl_prog
show "?Q ?Phi"
proof (unfold wf_cdecl_def, intro)
fix x a b aa ba ab bb m
assume 1: "x \<in> set G" "x = (a, b)" "b = (aa, ba)" "ba = (ab, bb)" "m \<in> set bb"
with wtl_prog
- show "wf_mdecl (\<lambda>G C (sig,rT,maxl,b).
- wt_method G C (snd sig) rT maxl b (?Phi C sig)) G a m"
+ show "wf_mdecl (\<lambda>G C (sig,rT,maxs,maxl,b).
+ wt_method G C (snd sig) rT maxs maxl b (?Phi C sig)) G a m"
proof (simp add: wf_mdecl_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def,
elim conjE)
apply_end (drule bspec, assumption, simp, elim conjE)
assume "\<forall>(sig,rT,mb)\<in>set bb. wf_mhead G sig rT \<and>
- (\<lambda>(maxl,b). wtl_method G a (snd sig) rT maxl b (cert a sig)) mb"
+ (\<lambda>(maxs,maxl,b). wtl_method G a (snd sig) rT maxs maxl b (cert a sig)) mb"
"unique bb"
with 1 uniqueG
show "(\<lambda>(sig,rT,mb).
wf_mhead G sig rT \<and>
- (\<lambda>(maxl,b).
- wt_method G a (snd sig) rT maxl b
+ (\<lambda>(maxs,maxl,b).
+ wt_method G a (snd sig) rT maxs maxl b
((\<lambda>(C,x,y,mdecls).
- (\<lambda>(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b))
- (SOME (sg,rT,maxl,b). (sg, rT, maxl, b) \<in> set mdecls \<and> sg = sig))
+ (\<lambda>(sig,rT,maxs,maxl,b). Eps (wt_method G C (snd sig) rT maxs maxl b))
+ (SOME (sg,rT,maxs,maxl,b). (sg, rT, maxs, maxl, b) \<in> set mdecls \<and> sg = sig))
(SOME (Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m"
- by - (drule bspec, assumption,
+ by - (drule bspec, assumption,
clarsimp dest!: wtl_method_correct,
- clarsimp intro!: someI simp add: unique_epsilon)
+ clarsimp intro!: someI simp add: unique_epsilon unique_epsilon')
qed
qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def)
qed
--- a/src/HOL/MicroJava/BV/LBVSpec.thy 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
--- a/src/HOL/MicroJava/BV/Step.thy Tue Dec 05 14:08:22 2000 +0100
+++ b/src/HOL/MicroJava/BV/Step.thy Tue Dec 05 14:08:56 2000 +0100
@@ -45,37 +45,38 @@
text "Conditions under which step is applicable:"
consts
-app' :: "instr \<times> jvm_prog \<times> ty \<times> state_type => bool"
+app' :: "instr \<times> jvm_prog \<times> nat \<times> ty \<times> state_type => bool"
recdef app' "{}"
-"app' (Load idx, G, rT, s) = (idx < length (snd s) \<and>
- (snd s) ! idx \<noteq> Err)"
-"app' (Store idx, G, rT, (ts#ST, LT)) = (idx < length LT)"
-"app' (Bipush i, G, rT, s) = True"
-"app' (Aconst_null, G, rT, s) = True"
-"app' (Getfield F C, G, rT, (oT#ST, LT)) = (is_class G C \<and>
+"app' (Load idx, G, maxs, rT, s) = (idx < length (snd s) \<and>
+ (snd s) ! idx \<noteq> Err \<and>
+ maxs < length (fst s))"
+"app' (Store idx, G, maxs, rT, (ts#ST, LT)) = (idx < length LT)"
+"app' (Bipush i, G, maxs, rT, s) = (maxs < length (fst s))"
+"app' (Aconst_null, G, maxs, rT, s) = (maxs < length (fst s))"
+"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, rT, (vT#oT#ST, LT)) = (is_class G C \<and>
+"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, rT, s) = (is_class G C)"
-"app' (Checkcast C, G, rT, (RefT rt#ST,LT)) = (is_class G C)"
-"app' (Pop, G, rT, (ts#ST,LT)) = True"
-"app' (Dup, G, rT, (ts#ST,LT)) = True"
-"app' (Dup_x1, G, rT, (ts1#ts2#ST,LT)) = True"
-"app' (Dup_x2, G, rT, (ts1#ts2#ts3#ST,LT)) = True"
-"app' (Swap, G, rT, (ts1#ts2#ST,LT)) = True"
-"app' (IAdd, G, rT, (PrimT Integer#PrimT Integer#ST,LT))
- = True"
-"app' (Ifcmpeq b, G, rT, (ts#ts'#ST,LT)) = ((\<exists>p. ts = PrimT p \<and> ts' = PrimT p) \<or>
+"app' (New C, G, maxs, rT, s) = (is_class G C \<and> maxs < length (fst s))"
+"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)) = (maxs < Suc (length ST))"
+"app' (Dup_x1, G, maxs, rT, (ts1#ts2#ST,LT)) = (maxs < Suc (Suc (length ST)))"
+"app' (Dup_x2, G, maxs, rT, (ts1#ts2#ts3#ST,LT)) = (maxs < Suc (Suc (Suc (length ST))))"
+"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, rT, s) = True"
-"app' (Return, G, rT, (T#ST,LT)) = (G \<turnstile> T \<preceq> rT)"
-"app' (Invoke C mn fpTs, G, rT, s) =
+"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))
@@ -83,12 +84,12 @@
G \<turnstile> X \<preceq> Class C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and>
(\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT)))"
-"app' (i,G,rT,s) = False"
+"app' (i,G,maxs,rT,s) = False"
constdefs
- app :: "instr => jvm_prog => ty => state_type option => bool"
- "app i G rT s == case s of None => True | Some t => app' (i,G,rT,t)"
+ 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: *}
@@ -144,74 +145,74 @@
simp rules for @{term app}
*}
lemma appNone[simp]:
-"app i G rT None = True"
+"app i G maxs rT None = True"
by (simp add: app_def)
lemma appLoad[simp]:
-"(app (Load idx) G rT (Some s)) = (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err)"
+"(app (Load idx) G maxs rT (Some s)) = (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err \<and> maxs < length (fst s))"
by (simp add: app_def)
lemma appStore[simp]:
-"(app (Store idx) G rT (Some s)) = (\<exists> ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)"
+"(app (Store idx) G maxs rT (Some s)) = (\<exists> ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
lemma appBipush[simp]:
-"(app (Bipush i) G rT (Some s)) = True"
+"(app (Bipush i) G maxs rT (Some s)) = (maxs < length (fst s))"
by (simp add: app_def)
lemma appAconst[simp]:
-"(app Aconst_null G rT (Some s)) = True"
+"(app Aconst_null G maxs rT (Some s)) = (maxs < length (fst s))"
by (simp add: app_def)
lemma appGetField[simp]:
-"(app (Getfield F C) G rT (Some s)) =
+"(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 "2 < length (fst s)", auto dest!: 1 2 simp add: app_def)
lemma appPutField[simp]:
-"(app (Putfield F C) G rT (Some s)) =
+"(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 "2 < length (fst s)", auto dest!: 1 2 simp add: app_def)
lemma appNew[simp]:
-"(app (New C) G rT (Some s)) = is_class G C"
+"(app (New C) G maxs rT (Some s)) = (is_class G C \<and> maxs < length (fst s))"
by (simp add: app_def)
lemma appCheckcast[simp]:
-"(app (Checkcast C) G rT (Some s)) = (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C)"
+"(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 rT (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT))"
+"(app Pop G maxs rT (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
lemma appDup[simp]:
-"(app Dup G rT (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT))"
+"(app Dup G maxs rT (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT) \<and> maxs < Suc (length ST))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
lemma appDup_x1[simp]:
-"(app Dup_x1 G rT (Some s)) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))"
+"(app Dup_x1 G maxs rT (Some s)) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> maxs < Suc (Suc (length ST)))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
lemma appDup_x2[simp]:
-"(app Dup_x2 G rT (Some s)) = (\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))"
+"(app Dup_x2 G maxs rT (Some s)) = (\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT) \<and> maxs < Suc (Suc (Suc (length ST))))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
lemma appSwap[simp]:
-"app Swap G rT (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))"
+"app Swap G maxs rT (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
lemma appIAdd[simp]:
-"app IAdd G rT (Some s) = (\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))"
+"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
@@ -242,21 +243,21 @@
lemma appIfcmpeq[simp]:
-"app (Ifcmpeq b) G rT (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and>
+"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 "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
lemma appReturn[simp]:
-"app Return G rT (Some s) = (\<exists>T ST LT. s = (T#ST,LT) \<and> (G \<turnstile> T \<preceq> rT))"
+"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 "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
lemma appGoto[simp]:
-"app (Goto branch) G rT (Some s) = True"
+"app (Goto branch) G maxs rT (Some s) = True"
by (simp add: app_def)
lemma appInvoke[simp]:
-"app (Invoke C mn fpTs) G rT (Some s) = (\<exists>apTs X ST LT mD' rT' b'.
+"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>
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")
--- a/src/HOL/MicroJava/BV/StepMono.thy Tue Dec 05 14:08:22 2000 +0100
+++ b/src/HOL/MicroJava/BV/StepMono.thy Tue Dec 05 14:08:56 2000 +0100
@@ -118,14 +118,18 @@
lemma app_mono:
-"[|G \<turnstile> s <=' s'; app i G rT s'|] ==> app i G rT s";
+"[|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 rT (Some s1)"
+ assume app: "app i G m rT (Some s1)"
- have "app i G rT (Some s2)"
+ from G
+ have l: "length (fst s2) = length (fst s1)"
+ by simp
+
+ have "app i G m rT (Some s2)"
proof (cases (open) i)
case Load
@@ -145,13 +149,15 @@
auto simp add: map_eq_Cons sup_loc_Cons2 sup_loc_length sup_state_def)
next
case Bipush
- thus ?thesis by simp
+ with G app
+ show ?thesis by simp
next
case Aconst_null
- thus ?thesis by simp
+ with G app
+ show ?thesis by simp
next
case New
- with app
+ with G app
show ?thesis by simp
next
case Getfield
@@ -204,17 +210,20 @@
case Dup
with app G
show ?thesis
- by - (cases s2, clarsimp simp add: sup_state_Cons2)
+ 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)
+ 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)
+ by - (cases s2, clarsimp simp add: sup_state_Cons2,
+ auto dest: sup_state_length)
next
case Swap
with app G
@@ -287,12 +296,12 @@
by (simp add: all_widen_is_sup_loc)
from Invoke s2 l' w' C' m
- show ?thesis
- by simp blast
+ show ?thesis
+ by (simp del: split_paired_Ex) blast
qed
} note mono_Some = this
- assume "G \<turnstile> s <=' s'" "app i G rT s'"
+ assume "G \<turnstile> s <=' s'" "app i G m rT s'"
thus ?thesis
by - (cases s, cases s', auto simp add: mono_Some)
@@ -302,18 +311,18 @@
lemmas [simp] = step_def
lemma step_mono_Some:
-"[| app i G rT (Some s2); G \<turnstile> s1 <=s s2 |] ==>
+"[| 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 rT (Some s2)"
+ 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 rT (Some s1)" by (rule app_mono)
+ 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
@@ -464,7 +473,7 @@
qed
lemma step_mono:
- "[| app i G rT s2; G \<turnstile> s1 <=' s2 |] ==>
+ "[| 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)