--- a/src/HOL/MicroJava/BV/Effect.thy Sun Mar 24 14:05:53 2002 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy Sun Mar 24 14:06:21 2002 +0100
@@ -184,6 +184,32 @@
"app i G maxs rT pc et s == case s of None \<Rightarrow> True | Some t \<Rightarrow> app' (i,G,pc,maxs,rT,t) \<and> xcpt_app i G pc et"
+lemma match_any_match_table:
+ "C \<in> set (match_any G pc et) \<Longrightarrow> match_exception_table G C pc et \<noteq> None"
+ apply (induct et)
+ apply simp
+ apply simp
+ apply clarify
+ apply (simp split: split_if_asm)
+ apply (auto simp add: match_exception_entry_def)
+ done
+
+lemma match_X_match_table:
+ "C \<in> set (match G X pc et) \<Longrightarrow> match_exception_table G C pc et \<noteq> None"
+ apply (induct et)
+ apply simp
+ apply (simp split: split_if_asm)
+ done
+
+lemma xcpt_names_in_et:
+ "C \<in> set (xcpt_names (i,G,pc,et)) \<Longrightarrow>
+ \<exists>e \<in> set et. the (match_exception_table G C pc et) = fst (snd (snd e))"
+ apply (cases i)
+ apply (auto dest!: match_any_match_table match_X_match_table
+ dest: match_exception_table_in_et)
+ done
+
+
lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
proof (cases a)
fix x xs assume "a = x#xs" "2 < length a"
--- a/src/HOL/MicroJava/BV/JVM.thy Sun Mar 24 14:05:53 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy Sun Mar 24 14:06:21 2002 +0100
@@ -6,13 +6,17 @@
header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}
-theory JVM = Kildall_Lift + JVMType + Opt + Product + Typing_Framework_err +
- EffectMono + BVSpec:
+theory JVM = Kildall_Lift + JVMType + EffectMono + BVSpec:
+
constdefs
+ check_bounded :: "instr list \<Rightarrow> exception_table \<Rightarrow> bool"
+ "check_bounded ins et \<equiv> (\<forall>pc < length ins. \<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins) \<and>
+ (\<forall>e \<in> set et. fst (snd (snd e)) < length ins)"
+
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)"
+ err_step (size bs) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"
kiljvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow>
instr list \<Rightarrow> state list \<Rightarrow> state list"
@@ -22,7 +26,7 @@
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>
+ check_bounded ins et \<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 et ins start
@@ -33,6 +37,65 @@
wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G"
+
+text {*
+ Executability of @{term check_bounded}:
+*}
+consts
+ list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
+primrec
+ "list_all'_rec P n [] = True"
+ "list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"
+
+constdefs
+ list_all' :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
+ "list_all' P xs \<equiv> list_all'_rec P 0 xs"
+
+lemma list_all'_rec:
+ "\<And>n. list_all'_rec P n xs = (\<forall>p < size xs. P (xs!p) (p+n))"
+ apply (induct xs)
+ apply auto
+ apply (case_tac p)
+ apply auto
+ done
+
+lemma list_all' [iff]:
+ "list_all' P xs = (\<forall>n < size xs. P (xs!n) n)"
+ by (unfold list_all'_def) (simp add: list_all'_rec)
+
+lemma list_all_ball:
+ "list_all P xs = (\<forall>x \<in> set xs. P x)"
+ by (induct xs) auto
+
+lemma [code]:
+ "check_bounded ins et =
+ (list_all' (\<lambda>i pc. list_all (\<lambda>pc'. pc' < length ins) (succs i pc)) ins \<and>
+ list_all (\<lambda>e. fst (snd (snd e)) < length ins) et)"
+ by (simp add: list_all_ball check_bounded_def)
+
+text {*
+ Lemmas for Kildall instantiation
+*}
+
+lemma check_bounded_is_bounded:
+ "check_bounded ins et \<Longrightarrow> bounded (\<lambda>pc. eff (ins!pc) G pc et) (length ins)"
+ apply (unfold bounded_def eff_def)
+ apply clarify
+ apply simp
+ apply (unfold check_bounded_def)
+ apply clarify
+ apply (erule disjE)
+ apply blast
+ apply (erule allE, erule impE, assumption)
+ apply (unfold xcpt_eff_def)
+ apply clarsimp
+ apply (drule xcpt_names_in_et)
+ apply clarify
+ apply (drule bspec, assumption)
+ apply simp
+ done
+
+
lemma special_ex_swap_lemma [iff]:
"(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
by blast
@@ -46,36 +109,6 @@
"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 \<Longrightarrow>
pres_type (exec S maxs rT et bs) (size bs) (states S maxs maxr)"
@@ -172,15 +205,6 @@
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))))"
@@ -193,25 +217,32 @@
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)
+lemma lesubstep_type_simple:
+ "a <=[Product.le (op =) r] b \<Longrightarrow> a <=|r| b"
+ apply (unfold lesubstep_type_def)
+ apply clarify
+ apply (simp add: set_conv_nth)
+ apply clarify
+ apply (drule le_listD, assumption)
+ apply (clarsimp simp add: lesub_def Product.le_def)
+ apply (rule exI)
+ apply (rule conjI)
+ apply (rule exI)
+ apply (rule conjI)
+ apply (rule sym)
+ apply assumption
+ apply assumption
+ apply assumption
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 lesubstep_type_simple)
apply (rule le_list_appendI)
apply (simp add: norm_eff_def)
apply (rule le_listI)
@@ -243,14 +274,14 @@
by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
theorem exec_mono:
- "wf_prog wf_mb G \<Longrightarrow>
+ "wf_prog wf_mb G \<Longrightarrow> bounded (exec G maxs rT et bs) (size bs) \<Longrightarrow>
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 (rule app_mono)
+ apply assumption
apply clarify
apply (rule eff_mono)
apply assumption+
@@ -275,7 +306,7 @@
theorem is_bcv_kiljvm:
- "\<lbrakk> wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \<rbrakk> \<Longrightarrow>
+ "\<lbrakk> wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \<rbrakk> \<Longrightarrow>
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)
@@ -287,8 +318,8 @@
dest: wf_subcls1 wf_acyclic)
apply (simp add: JVM_le_unfold)
apply (erule exec_pres_type)
- apply assumption
- apply (erule exec_mono)
+ apply assumption
+ apply (erule exec_mono, assumption)
done
@@ -306,19 +337,20 @@
assume "wt_kil G C pTs rT maxs mxl et bs"
then obtain maxr r where
- bounded: "bounded (exec G maxs rT et bs) (size bs)" and
+ bounded: "check_bounded bs et" 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
- from wf bounded
- have bcv:
+ from bounded have "bounded (exec G maxs rT et bs) (size bs)"
+ by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded)
+ with wf have bcv:
"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)"
+ (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+
} note subset_replicate = this
from istype have "set pTs \<subseteq> types G" by auto
@@ -346,9 +378,9 @@
s: "?start <=[JVMType.le G maxs maxr] phi'" and
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 et bs) phi'"
- by (simp add: dynamic_wt_def exec_def JVM_le_Err_conv)
+ hence wt_err_step:
+ "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) phi'"
+ by (simp add: wt_err_step_def exec_def JVM_le_Err_conv)
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)+
@@ -360,14 +392,14 @@
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)
+ by (simp add: exec_def check_bounded_is_bounded)
+ with wt_err_step
+ have "wt_app_eff (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: wt_err_imp_wt_app_eff simp add: l 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 (unfold wt_method_def wt_app_eff_def)
apply simp
apply (rule conjI)
apply (unfold wt_start_def)
@@ -387,7 +419,8 @@
theorem wt_kil_complete:
"\<lbrakk> 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;
+ check_bounded bs et; 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)) \<rbrakk>
\<Longrightarrow> wt_kil G C pTs rT maxs mxl et bs"
proof -
@@ -396,6 +429,7 @@
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 bounded: "check_bounded bs et"
assume "wt_method G C pTs rT maxs mxl bs et phi"
then obtain
@@ -408,37 +442,22 @@
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 bounded
+ have bounded_exec: "bounded (exec G maxs rT et bs) (size bs)"
+ by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded)
from wt_ins
- have "static_wt (sup_state_opt G) ?app ?eff phi"
- apply (unfold static_wt_def wt_instr_def lesub_def)
+ have "wt_app_eff (sup_state_opt G) ?app ?eff phi"
+ apply (unfold wt_app_eff_def wt_instr_def lesub_def)
apply (simp (no_asm) only: length)
apply blast
done
-
- 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 et bs) (map OK phi)"
- by (unfold exec_def)
+ with bounded_exec
+ have "wt_err_step (sup_state_opt G) (err_step (size phi) ?app ?eff) (map OK phi)"
+ by - (erule wt_app_eff_imp_wt_err,simp add: exec_def length)
+ hence wt_err:
+ "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) (map OK phi)"
+ by (unfold exec_def) (simp add: length)
let ?maxr = "1+size pTs+mxl"
from wf bounded_exec
@@ -501,13 +520,13 @@
ultimately show ?thesis by (rule le_listI)
qed
- from dynamic
+ from wt_err
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)
+ by (simp add: wt_err_step_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
+ with bounded instrs
show "wt_kil G C pTs rT maxs mxl et bs" by (unfold wt_kil_def) simp
qed
text {*
@@ -593,4 +612,5 @@
thus ?thesis by blast
qed
+
end
--- a/src/HOL/MicroJava/BV/Kildall.thy Sun Mar 24 14:05:53 2002 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy Sun Mar 24 14:06:21 2002 +0100
@@ -299,8 +299,8 @@
lemma merges_bounded_lemma:
"\<lbrakk> 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 \<longrightarrow> stable r step ts p \<rbrakk>
- \<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts"
+ ss <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk>
+ \<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts"
apply (unfold stable_def)
apply (rule merges_pres_le_ub)
apply assumption
@@ -319,7 +319,7 @@
apply simp
apply (simp add: le_listD)
- apply (drule lesub_step_type, assumption)
+ apply (drule lesub_step_typeD, assumption)
apply clarify
apply (drule bspec, assumption)
apply simp
--- a/src/HOL/MicroJava/BV/Kildall_Lift.thy Sun Mar 24 14:05:53 2002 +0100
+++ b/src/HOL/MicroJava/BV/Kildall_Lift.thy Sun Mar 24 14:06:21 2002 +0100
@@ -11,84 +11,32 @@
"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 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 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 bounded_lift:
+ "bounded step n \<Longrightarrow> bounded (err_step n app step) n"
+ apply (unfold bounded_def err_step_def error_def)
+ apply clarify
+ apply (erule allE, erule impE, assumption)
+ apply (case_tac s)
+ apply (auto simp add: map_snd_def split: split_if_asm)
+ 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 boundedD2:
+ "bounded (err_step n app step) n \<Longrightarrow>
+ p < n \<Longrightarrow> app p a \<Longrightarrow> (q,b) \<in> set (step p a) \<Longrightarrow>
+ q < n"
+ apply (simp add: bounded_def err_step_def)
+ apply (erule allE, erule impE, assumption)
+ apply (erule_tac x = "OK a" in allE, drule bspec)
+ apply (simp add: map_snd_def)
+ apply fast
+ apply simp
+ done
lemma le_list_map_OK [simp]:
"\<And>b. map OK a <=[Err.le r] map OK b = (a <=[r] b)"
@@ -100,126 +48,76 @@
apply simp
done
+
+lemma map_snd_lessI:
+ "x <=|r| y \<Longrightarrow> map_snd OK x <=|Err.le r| map_snd OK y"
+ apply (induct x)
+ apply (unfold lesubstep_type_def map_snd_def)
+ apply auto
+ done
+
+
lemma mono_lift:
- "order r \<Longrightarrow> succs_stable r step \<Longrightarrow> app_mono r app n A \<Longrightarrow>
+ "order r \<Longrightarrow> app_mono r app n A \<Longrightarrow> bounded (err_step n app step) n \<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)"
+ mono (Err.le r) (err_step n 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 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 (simp add: lesubstep_type_def error_def)
+ apply clarify
+ apply (drule in_map_sndD)
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 (drule boundedD2, assumption+)
+ apply (rule exI [of _ Err])
+ apply simp
+apply simp
+apply (erule allE, erule allE, erule allE, erule impE)
+ apply (rule conjI, assumption)
+ apply (rule conjI, assumption)
+ apply assumption
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 (erule allE, erule allE, erule allE, erule impE)
+ apply (rule conjI, assumption)
+ apply (rule conjI, assumption)
+ apply assumption
+apply (erule impE, assumption)
+apply (rule map_snd_lessI, assumption)
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)
+apply (simp add: lesubstep_type_def error_def)
+apply clarify
+apply (drule in_map_sndD)
+apply clarify
+apply (drule boundedD2, assumption+)
+apply (rule exI [of _ Err])
+apply simp
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 in_errorD:
+ "(x,y) \<in> set (error n) \<Longrightarrow> y = Err"
+ by (auto simp add: error_def)
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)"
+ \<Longrightarrow> pres_type (err_step n 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 (drule in_errorD)
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 add: map_snd_def split: split_if_asm)
+ apply fast
+apply (drule in_errorD)
apply simp
-apply blast
done
end
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Sun Mar 24 14:05:53 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Sun Mar 24 14:06:21 2002 +0100
@@ -9,60 +9,60 @@
theory LBVComplete = LBVSpec + Typing_Framework:
constdefs
- contains_targets :: "['s steptype, 's certificate, 's option list, nat, nat] \<Rightarrow> bool"
- "contains_targets step cert phi pc n \<equiv>
- \<forall>(pc',s') \<in> set (step pc (OK (phi!pc))). pc' \<noteq> pc+1 \<and> pc' < n \<longrightarrow> cert!pc' = phi!pc'"
+ contains_targets :: "['s steptype, 's certificate, 's option list, nat] \<Rightarrow> bool"
+ "contains_targets step cert phi pc \<equiv>
+ \<forall>(pc',s') \<in> set (step pc (OK (phi!pc))). pc' \<noteq> pc+1 \<and> pc' < length phi \<longrightarrow> cert!pc' = phi!pc'"
- fits :: "['s steptype, 's certificate, 's option list, nat] \<Rightarrow> bool"
- "fits step cert phi n \<equiv> \<forall>pc. pc < n \<longrightarrow>
- contains_targets step cert phi pc n \<and>
- (cert!pc = None \<or> cert!pc = phi!pc)"
+ fits :: "['s steptype, 's certificate, 's option list] \<Rightarrow> bool"
+ "fits step cert phi \<equiv> \<forall>pc. pc < length phi \<longrightarrow>
+ contains_targets step cert phi pc \<and>
+ (cert!pc = None \<or> cert!pc = phi!pc)"
- is_target :: "['s steptype, 's option list, nat, nat] \<Rightarrow> bool"
- "is_target step phi pc' n \<equiv>
- \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < n \<and> (pc',s') \<in> set (step pc (OK (phi!pc)))"
+ is_target :: "['s steptype, 's option list, nat] \<Rightarrow> bool"
+ "is_target step phi pc' \<equiv>
+ \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (OK (phi!pc)))"
- make_cert :: "['s steptype, 's option list, nat] \<Rightarrow> 's certificate"
- "make_cert step phi n \<equiv>
- map (\<lambda>pc. if is_target step phi pc n then phi!pc else None) [0..n(]"
+ make_cert :: "['s steptype, 's option list] \<Rightarrow> 's certificate"
+ "make_cert step phi \<equiv>
+ map (\<lambda>pc. if is_target step phi pc then phi!pc else None) [0..length phi(]"
lemmas [simp del] = split_paired_Ex
lemma make_cert_target:
- "\<lbrakk> pc < n; is_target step phi pc n \<rbrakk> \<Longrightarrow> make_cert step phi n ! pc = phi!pc"
+ "\<lbrakk> pc < length phi; is_target step phi pc \<rbrakk> \<Longrightarrow> make_cert step phi ! pc = phi!pc"
by (simp add: make_cert_def)
lemma make_cert_approx:
- "\<lbrakk> pc < n; make_cert step phi n ! pc \<noteq> phi!pc \<rbrakk> \<Longrightarrow>
- make_cert step phi n ! pc = None"
+ "\<lbrakk> pc < length phi; make_cert step phi ! pc \<noteq> phi!pc \<rbrakk> \<Longrightarrow>
+ make_cert step phi ! pc = None"
by (auto simp add: make_cert_def)
lemma make_cert_contains_targets:
- "pc < n \<Longrightarrow> contains_targets step (make_cert step phi n) phi pc n"
+ "pc < length phi \<Longrightarrow> contains_targets step (make_cert step phi) phi pc"
proof (unfold contains_targets_def, clarify)
fix pc' s'
- assume "pc < n"
+ assume "pc < length phi"
"(pc',s') \<in> set (step pc (OK (phi ! pc)))"
"pc' \<noteq> pc+1" and
- pc': "pc' < n"
- hence "is_target step phi pc' n" by (auto simp add: is_target_def)
- with pc' show "make_cert step phi n ! pc' = phi ! pc'"
+ pc': "pc' < length phi"
+ hence "is_target step phi pc'" by (auto simp add: is_target_def)
+ with pc' show "make_cert step phi ! pc' = phi!pc'"
by (auto intro: make_cert_target)
qed
theorem fits_make_cert:
- "fits step (make_cert step phi n) phi n"
+ "fits step (make_cert step phi) phi"
by (auto dest: make_cert_approx simp add: fits_def make_cert_contains_targets)
lemma fitsD:
- "\<lbrakk> fits step cert phi n; (pc',s') \<in> set (step pc (OK (phi ! pc)));
- pc' \<noteq> Suc pc; pc < n; pc' < n \<rbrakk>
+ "\<lbrakk> fits step cert phi; (pc',s') \<in> set (step pc (OK (phi ! pc)));
+ pc' \<noteq> Suc pc; pc < length phi; pc' < length phi \<rbrakk>
\<Longrightarrow> cert!pc' = phi!pc'"
by (auto simp add: fits_def contains_targets_def)
lemma fitsD2:
- "\<lbrakk> fits step cert phi n; pc < n; cert!pc = Some s \<rbrakk>
+ "\<lbrakk> fits step cert phi; pc < length phi; cert!pc = Some s \<rbrakk>
\<Longrightarrow> cert!pc = phi!pc"
by (auto simp add: fits_def)
@@ -82,8 +82,9 @@
lemma stable_wtl:
assumes stable: "stable (Err.le (Opt.le r)) step (map OK phi) pc"
- assumes fits: "fits step cert phi n"
+ assumes fits: "fits step cert phi"
assumes pc: "pc < length phi"
+ assumes bounded:"bounded step (length phi)"
shows "wtl_inst cert f r step pc (phi!pc) \<noteq> Err"
proof -
from pc have [simp]: "map OK phi ! pc = OK (phi!pc)" by simp
@@ -91,7 +92,10 @@
have "\<forall>(q,s')\<in>set (step pc (OK (phi!pc))). s' \<le>|r (map OK phi!q)"
by (simp add: stable_def)
-
+ have "merge cert f r pc (step pc (OK (phi ! pc))) (OK (cert ! Suc pc)) \<noteq> Err"
+ sorry
+ thus ?thesis by (simp add: wtl_inst_def)
+qed
lemma wtl_inst_mono:
--- a/src/HOL/MicroJava/BV/Listn.thy Sun Mar 24 14:05:53 2002 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy Sun Mar 24 14:06:21 2002 +0100
@@ -142,6 +142,20 @@
apply auto
done
+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 listI:
"\<lbrakk> length xs = n; set xs <= A \<rbrakk> \<Longrightarrow> xs : list n A"
apply (unfold list_def)
@@ -202,6 +216,37 @@
"\<lbrakk> xs : list n A; i < n \<rbrakk> \<Longrightarrow> (xs!i) : A"
by auto
+
+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
+
+
lemma listt_update_in_list [simp, intro!]:
"\<lbrakk> xs : list n A; x:A \<rbrakk> \<Longrightarrow> xs[i := x] : list n A"
apply (unfold list_def)
--- a/src/HOL/MicroJava/BV/SemilatAlg.thy Sun Mar 24 14:05:53 2002 +0100
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy Sun Mar 24 14:06:21 2002 +0100
@@ -9,18 +9,17 @@
theory SemilatAlg = Typing_Framework + Product:
-syntax "@lesubstep_type" :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
- ("(_ /<=|_| _)" [50, 0, 51] 50)
-translations
- "x <=|r| y" == "x <=[(Product.le (op =) r)] y"
-
+constdefs
+ lesubstep_type :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
+ ("(_ /<=|_| _)" [50, 0, 51] 50)
+ "x <=|r| y \<equiv> \<forall>(p,s) \<in> set x. \<exists>s'. (p,s') \<in> set y \<and> s <=_r s'"
+
consts
"@plusplussub" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
primrec
"[] ++_f y = y"
"(x#xs) ++_f y = xs ++_f (x +_f y)"
-
constdefs
bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool"
"bounded step n == !p<n. !s. !(q,t):set(step p s). q<n"
@@ -45,6 +44,14 @@
"\<lbrakk> bounded step n; p < n; (q,t) : set (step p xs) \<rbrakk> \<Longrightarrow> q < n"
by (unfold bounded_def, blast)
+lemma lesubstep_type_refl [simp, intro]:
+ "(\<And>x. x <=_r x) \<Longrightarrow> x <=|r| x"
+ by (unfold lesubstep_type_def) auto
+
+lemma lesub_step_typeD:
+ "a <=|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
+ by (unfold lesubstep_type_def) blast
+
lemma list_update_le_listI [rule_format]:
"set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow>
@@ -162,20 +169,4 @@
done
-lemma lesub_step_type:
- "\<And>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
-
end
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy Sun Mar 24 14:05:53 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy Sun Mar 24 14:06:21 2002 +0100
@@ -11,28 +11,30 @@
constdefs
-dynamic_wt :: "'s ord \<Rightarrow> 's err step_type \<Rightarrow> 's err list \<Rightarrow> bool"
-"dynamic_wt r step ts == wt_step (Err.le r) Err step ts"
+wt_err_step :: "'s ord \<Rightarrow> 's err step_type \<Rightarrow> 's err list \<Rightarrow> bool"
+"wt_err_step r step ts \<equiv> wt_step (Err.le r) Err step ts"
-static_wt :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
-"static_wt r app step ts ==
+wt_app_eff :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
+"wt_app_eff r app step ts \<equiv>
\<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))"
+"map_snd f \<equiv> map (\<lambda>(x,y). (x, f y))"
+
+error :: "nat \<Rightarrow> (nat \<times> 'a err) list"
+"error n \<equiv> map (\<lambda>x. (x,Err)) [0..n(]"
-map_err :: "('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b err) list"
-"map_err == map_snd (\<lambda>y. 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')"
+err_step :: "nat \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's err step_type"
+"err_step n app step p t \<equiv>
+ case t of
+ Err \<Rightarrow> error n
+ | OK t' \<Rightarrow> if app p t' then map_snd OK (step p t') else error n"
non_empty :: "'s step_type \<Rightarrow> bool"
-"non_empty step == \<forall>p t. step p t \<noteq> []"
+"non_empty step \<equiv> \<forall>p t. step p t \<noteq> []"
-lemmas err_step_defs = err_step_def map_snd_def map_err_def
+lemmas err_step_defs = err_step_def map_snd_def error_def
lemma non_emptyD:
"non_empty step \<Longrightarrow> \<exists>q t'. (q,t') \<in> set(step p t)"
@@ -46,44 +48,38 @@
qed
-lemma dynamic_imp_static:
- "\<lbrakk> bounded step (size ts); non_empty step;
- dynamic_wt r (err_step app step) ts \<rbrakk>
- \<Longrightarrow> static_wt r app step (map ok_val ts)"
-proof (unfold static_wt_def, intro strip, rule conjI)
-
- 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
+lemma wt_err_imp_wt_app_eff:
+ assumes b: "bounded step (size ts)"
+ assumes n: "non_empty step"
+ assumes wt: "wt_err_step r (err_step (size ts) app step) ts"
+ shows "wt_app_eff r app step (map ok_val ts)"
+proof (unfold wt_app_eff_def, intro strip, rule conjI)
+ fix p assume "p < size (map ok_val ts)"
+ hence lp: "p < size ts" by simp
from wt lp
- have [intro?]: "\<And>p. p < length ts \<Longrightarrow> ts ! p \<noteq> Err"
- by (unfold dynamic_wt_def wt_step_def) simp
+ have [intro?]: "\<And>p. p < size ts \<Longrightarrow> ts ! p \<noteq> Err"
+ by (unfold wt_err_step_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)
+ less: "\<forall>(q,t) \<in> set (err_step (size ts) app step p (ts!p)). t <=_(Err.le r) ts!q"
+ by (unfold wt_err_step_def wt_step_def stable_def)
(auto iff: not_Err_eq)
- from n
- obtain q t where q: "(q,t) \<in> set(step p s)"
- by (blast dest: non_emptyD)
-
+ from n 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
+ have lq: "q < size 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 OKp less q lp 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
@@ -95,12 +91,12 @@
from wt lp q
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)
+ less: "\<forall>(q,t) \<in> set (err_step (size ts) app step p (ts!p)). t <=_(Err.le r) ts!q"
+ by (unfold wt_err_step_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
+ have lq: "q < size 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)
@@ -111,24 +107,22 @@
qed
-lemma static_imp_dynamic:
- "\<lbrakk> static_wt r app step ts; bounded step (size ts) \<rbrakk>
- \<Longrightarrow> 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 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
+lemma wt_app_eff_imp_wt_err:
+ assumes app_eff: "wt_app_eff r app step ts"
+ assumes bounded: "bounded (err_step (size ts) app step) (size ts)"
+ shows "wt_err_step r (err_step (size ts) app step) (map OK ts)"
+proof (unfold wt_err_step_def wt_step_def, intro strip, rule conjI)
+ fix p assume "p < size (map OK ts)"
+ hence p: "p < size ts" by simp
thus "map OK ts ! p \<noteq> Err" by simp
{ fix q t
- assume q: "(q,t) \<in> set (err_step app step p (map OK ts ! p))"
- with p static obtain
+ assume q: "(q,t) \<in> set (err_step (size ts) app step p (map OK ts ! p))"
+ with p app_eff obtain
"app p (ts ! p)" "\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q"
- by (unfold static_wt_def) blast
+ by (unfold wt_app_eff_def) blast
moreover
- from q p bounded have "q < size ts"
- by (clarsimp simp add: bounded_def err_step_defs
- split: err.splits split_if_asm) blast+
+ from q p bounded have "q < size ts"
+ by - (rule boundedD)
hence "map OK ts ! q = OK (ts!q)" by simp
moreover
have "p < size ts" by (rule p)
@@ -137,7 +131,7 @@
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) (map OK ts) p"
+ thus "stable (Err.le r) (err_step (size ts) app step) (map OK ts) p"
by (unfold stable_def) blast
qed