--- a/src/HOL/MicroJava/BV/LBVSpec.thy Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Wed Mar 20 13:21:07 2002 +0100
@@ -6,154 +6,215 @@
header {* \isaheader{The Lightweight Bytecode Verifier} *}
-theory LBVSpec = Effect + Kildall:
+theory LBVSpec = SemilatAlg + Opt:
+
+
+syntax
+ "@lesuberropt" :: "'a option err \<Rightarrow> 'a ord \<Rightarrow> 'a option err \<Rightarrow> 'a option err ord"
+ ("_ \<le>|_ _" [50,50,51] 50)
-text {*
- The Lightweight Bytecode Verifier with exceptions has not
- made it completely into the Isabelle 2001 release. Currently
- there is only the specification itself available. The proofs of
- soundness and completeness are broken (they still need to be
- ported to the exception version). Both theories are included
- for documentation (but they don't work for this specification),
- please see the Isabelle 99-2 release for a working copy, or
- \url{http://isabelle.in.tum.de/verificard} for the most recent
- development of \mJava.
-*}
+ "@superropt" :: "'a option err \<Rightarrow> 'a ebinop \<Rightarrow> 'a option err \<Rightarrow> 'a option err binop"
+ ("_ +|_ _" [50,50,51] 50)
+
+ "@supsuperropt" :: "'a option err list \<Rightarrow> 'a ebinop \<Rightarrow> 'a option err \<Rightarrow> 'a option err binop"
+ ("_ ++|_ _" [50,50,51] 50)
+
+translations
+ "a \<le>|r b" == "a <=_(Err.le (Opt.le r)) b"
+ "a +|f b" == "a +_(Err.lift2 (Opt.sup f)) b"
+ "a ++|f b" == "a ++_(Err.lift2 (Opt.sup f)) b"
+
types
- certificate = "state_type option list"
- class_certificate = "sig \<Rightarrow> certificate"
- prog_certificate = "cname \<Rightarrow> class_certificate"
+ 's certificate = "'s option list"
+ 's steptype = "'s option err step_type"
consts
- merge :: "[jvm_prog, p_count, nat, nat, p_count, certificate, (nat \<times> (state_type option)) list, state] \<Rightarrow> state"
+merge :: "'s certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow> nat \<Rightarrow>
+ (nat \<times> 's option err) list \<Rightarrow> 's option err \<Rightarrow> 's option err"
primrec
- "merge G pc mxs mxr max_pc cert [] x = x"
- "merge G pc mxs mxr max_pc cert (s#ss) x = (let (pc',s') = s in
- if pc' < max_pc \<and> pc' = pc+1 then
- merge G pc mxs mxr max_pc cert ss (OK s' +_(sup G mxs mxr) x)
- else if pc' < max_pc \<and> G \<turnstile> s' <=' cert!pc' then
- merge G pc mxs mxr max_pc cert ss x
- else Err)"
+"merge cert f r pc [] x = x"
+"merge cert f r pc (s#ss) x = (let (pc',s') = s in
+ merge cert f r pc ss (if pc'=pc+1 then (s' +|f x)
+ else if s' \<le>|r (OK (cert!pc')) then x
+ else Err))"
-constdefs
- wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count]
- \<Rightarrow> state_type option err"
- "wtl_inst i G rT s cert maxs maxr max_pc et pc ==
- if app i G maxs rT pc et s then
- merge G pc maxs maxr max_pc cert (eff i G pc et s) (OK (cert!(pc+1)))
- else Err"
+constdefs
+wtl_inst :: "'s certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow>
+ 's steptype \<Rightarrow> nat \<Rightarrow> 's option \<Rightarrow> 's option err"
+"wtl_inst cert f r step pc s \<equiv> merge cert f r pc (step pc (OK s)) (OK (cert!(pc+1)))"
- wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count]
- \<Rightarrow> state_type option err"
- "wtl_cert i G rT s cert maxs maxr max_pc et pc ==
- case cert!pc of
- None \<Rightarrow> wtl_inst i G rT s cert maxs maxr max_pc et pc
- | Some s' \<Rightarrow> if G \<turnstile> s <=' (Some s') then
- wtl_inst i G rT (Some s') cert maxs maxr max_pc et pc
- else Err"
+wtl_cert :: "'s certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow>
+ 's steptype \<Rightarrow> nat \<Rightarrow> 's option \<Rightarrow> 's option err"
+"wtl_cert cert f r step pc s \<equiv>
+ case cert!pc of
+ None \<Rightarrow> wtl_inst cert f r step pc s
+ | Some s' \<Rightarrow> if OK s \<le>|r (OK (Some s')) then wtl_inst cert f r step pc (Some s') else Err"
consts
- wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,nat,nat,p_count,exception_table,p_count,
- state_type option] \<Rightarrow> state_type option err"
+wtl_inst_list :: "'a list \<Rightarrow> 's certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow>
+ 's steptype \<Rightarrow> nat \<Rightarrow> 's option \<Rightarrow> 's option err"
primrec
- "wtl_inst_list [] G rT cert maxs maxr max_pc et pc s = OK s"
- "wtl_inst_list (i#is) G rT cert maxs maxr max_pc et pc s =
- (let s' = wtl_cert i G rT s cert maxs maxr max_pc et pc in
- strict (wtl_inst_list is G rT cert maxs maxr max_pc et (pc+1)) s')"
-
+"wtl_inst_list [] cert f r step pc s = OK s"
+"wtl_inst_list (i#ins) cert f r step pc s =
+ (let s' = wtl_cert cert f r step pc s in
+ strict (wtl_inst_list ins cert f r step (pc+1)) s')"
+
+
constdefs
- wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,exception_table,instr list,certificate] \<Rightarrow> bool"
- "wtl_method G C pTs rT mxs mxl et ins cert ==
- let max_pc = length ins
- in
- 0 < max_pc \<and>
- wtl_inst_list ins G rT cert mxs mxl max_pc et 0
- (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) \<noteq> Err"
+ cert_ok :: "'s certificate \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
+ "cert_ok cert n A \<equiv> \<forall>i < n. cert!i \<in> opt A"
+
+lemma cert_okD:
+ "cert_ok cert n A \<Longrightarrow> pc < n \<Longrightarrow> cert!pc \<in> opt A"
+ by (unfold cert_ok_def) fast
+
+
+declare Let_def [simp]
+
+section "more semilattice lemmas"
+
+(*
+lemma sup_top [simp]:
+ assumes sl: "semilat (A,r,f)"
+ assumes set: "x \<in> A" "t \<in> A"
+ assumes top: "top r t"
+ shows "x +_f t = t"
+proof -
+ from sl have "order r" ..
+ moreover from top have "x +_f t <=_r t" ..
+ moreover from sl set have "t <=_r x +_f t" by simp
+ ultimately show ?thesis by (rule order_antisym)
+qed
+
+lemma plusplussup_top:
+ "semilat (A,r,f) \<Longrightarrow> top r Err \<Longrightarrow> set xs \<subseteq> A \<Longrightarrow> Err \<in> A \<Longrightarrow> xs ++_f Err = Err"
+ by (induct xs) auto
+*)
+
+lemma err_semilatDorderI [simp, intro]:
+ "err_semilat (A,r,f) \<Longrightarrow> order r"
+ apply (simp add: Err.sl_def)
+ apply (rule order_le_err [THEN iffD1])
+ apply (rule semilatDorderI)
+ apply assumption
+ done
+
+lemma err_opt_semilat [simp,elim]:
+ "err_semilat (A,r,f) \<Longrightarrow> semilat (err (opt A), Err.le (Opt.le r), lift2 (Opt.sup f))"
+proof -
+ assume "err_semilat (A,r,f)"
+ hence "err_semilat (Opt.esl (A,r,f))" ..
+ thus ?thesis by (simp add: Err.sl_def Opt.esl_def)
+qed
+
+lemma plusplus_erropt_Err [simp]:
+ "xs ++|f Err = Err"
+ by (induct xs) auto
+
+
+section "merge"
+
+lemma merge_Err [simp]:
+ "merge cert f r pc ss Err = Err"
+ by (induct ss) auto
- wtl_jvm_prog :: "[jvm_prog,prog_certificate] \<Rightarrow> bool"
- "wtl_jvm_prog G cert ==
- wf_prog (\<lambda>G C (sig,rT,maxs,maxl,b,et). wtl_method G C (snd sig) rT maxs maxl et b (cert C sig)) G"
+lemma merge_ok:
+ "\<And>x. merge cert f r pc ss x = OK s \<Longrightarrow>
+ \<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc')))"
+ (is "\<And>x. ?merge ss x \<Longrightarrow> ?P ss")
+proof (induct ss)
+ show "?P []" by simp
+next
+ fix x l ls assume merge: "?merge (l#ls) x"
+ moreover
+ obtain pc' s' where [simp]: "l = (pc',s')" by (cases l)
+ ultimately
+ obtain x' where "?merge ls x'" by simp
+ assume "\<And>x. ?merge ls x \<Longrightarrow> ?P ls" hence "?P ls" .
+ moreover
+ from merge
+ have "pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))" by (simp split: split_if_asm)
+ ultimately
+ show "?P (l#ls)" by simp
+qed
+
+lemma merge_def:
+ assumes semi: "err_semilat (A,r,f)"
+ shows
+ "\<And>x. x \<in> err (opt A) \<Longrightarrow> \<forall>(pc', s') \<in> set ss. s' \<in> err (opt A) \<Longrightarrow>
+ merge cert f r pc ss x =
+ (if \<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))) then
+ map snd [(p',t') \<in> ss. p'=pc+1] ++|f x
+ else Err)"
+ (is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?merge ss x = ?if ss x" is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?P ss x")
+proof (induct ss)
+ fix x show "?P [] x" by simp
+next
+ fix x assume x: "x \<in> err (opt A)"
+ fix l::"nat \<times> 'a option err" and ls
+ assume "\<forall>(pc', s') \<in> set (l#ls). s' \<in> err (opt A)"
+ then obtain l: "snd l \<in> err (opt A)" and ls: "\<forall>(pc', s') \<in> set ls. s' \<in> err (opt A)" by auto
+ assume "\<And>x. x \<in> err (opt A) \<Longrightarrow> \<forall>(pc',s') \<in> set ls. s' \<in> err (opt A) \<Longrightarrow> ?P ls x"
+ hence IH: "\<And>x. x \<in> err (opt A) \<Longrightarrow> ?P ls x" .
+ obtain pc' s' where [simp]: "l = (pc',s')" by (cases l)
+ hence "?merge (l#ls) x = ?merge ls
+ (if pc'=pc+1 then s' +|f x else if s' \<le>|r (OK (cert!pc')) then x else Err)"
+ (is "?merge (l#ls) x = ?merge ls ?if'")
+ by simp
+ also have "\<dots> = ?if ls ?if'"
+ proof -
+ from l have "s' \<in> err (opt A)" by simp
+ with x semi have "(s' +|f x) \<in> err (opt A)" by (fast intro: closedD)
+ with x have "?if' \<in> err (opt A)" by auto
+ hence "?P ls ?if'" by (rule IH) thus ?thesis by simp
+ qed
+ also have "\<dots> = ?if (l#ls) x"
+ proof (cases "\<forall>(pc', s')\<in>set (l#ls). pc' \<noteq> pc + 1 \<longrightarrow> s' \<le>|r OK (cert ! pc')")
+ case True
+ hence "\<forall>(pc', s')\<in>set ls. pc' \<noteq> pc + 1 \<longrightarrow> s' \<le>|r (OK (cert ! pc'))" by auto
+ moreover
+ from True have
+ "map snd [(p',t')\<in>ls . p'=pc+1] ++|f ?if' =
+ (map snd [(p',t')\<in>l#ls . p'=pc+1] ++|f x)"
+ by simp
+ ultimately
+ show ?thesis using True by simp
+ next
+ case False thus ?thesis by auto
+ qed
+ finally show "?P (l#ls) x" .
+qed
+
+lemma merge_ok_s:
+ assumes sl: "err_semilat (A,r,f)"
+ assumes x: "x \<in> err (opt A)"
+ assumes ss: "\<forall>(pc', s') \<in> set ss. s' \<in> err (opt A)"
+ assumes m: "merge cert f r pc ss x = OK s"
+ shows "merge cert f r pc ss x = (map snd [(p',t') \<in> ss. p'=pc+1] ++|f x)"
+proof -
+ from m have "\<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc')))"
+ by (rule merge_ok)
+ with sl x ss m show ?thesis by - (drule merge_def, auto split: split_if_asm)
+qed
+
+section "wtl-inst-list"
lemmas [iff] = not_Err_eq
-lemma if_eq_cases:
- "(P \<Longrightarrow> x = z) \<Longrightarrow> (\<not>P \<Longrightarrow> y = z) \<Longrightarrow> (if P then x else y) = z"
- by simp
-
-lemma merge_def:
- "\<And>x. merge G pc mxs mxr max_pc cert ss x =
- (if \<forall>(pc',s') \<in> set ss. pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> s' <=' cert!pc') then
- map (OK \<circ> snd) [(p',t') \<in> ss. p'=pc+1] ++_(sup G mxs mxr) x
- else Err)" (is "\<And>x. ?merge ss x = ?if ss x" is "\<And>x. ?P ss x")
-proof (induct ss)
- show "\<And>x. ?P [] x" by simp
-next
- have OK_snd: "(\<lambda>u. OK (snd u)) = OK \<circ> snd" by (rule ext) auto
- fix x ss and s::"nat \<times> (state_type option)"
- assume IH: "\<And>x. ?P ss x"
- obtain pc' s' where s: "s = (pc',s')" by (cases s)
- hence "?merge (s#ss) x = ?merge ((pc',s')#ss) x" by hypsubst (rule refl)
- also
- have "\<dots> = (if pc' < max_pc \<and> pc' = pc+1 then
- ?merge ss (OK s' +_(sup G mxs mxr) x)
- else if pc' < max_pc \<and> G \<turnstile> s' <=' cert!pc' then
- ?merge ss x
- else Err)"
- (is "_ = (if ?pc' then ?merge ss (_ +_?f _) else if ?G then _ else _)")
- by simp
- also
- let "if ?all ss then _ else _" = "?if ss x"
- have "\<dots> = ?if ((pc',s')#ss) x"
- proof (cases "?pc'")
- case True
- hence "?all (((pc',s')#ss)) = (pc+1 < max_pc \<and> ?all ss)" by simp
- with True
- have "?if ss (OK s' +_?f x) = ?if ((pc',s')#ss) x" by (auto simp add: OK_snd)
- hence "?merge ss (OK s' +_?f x) = ?if ((pc',s')#ss) x" by (simp only: IH)
- with True show ?thesis by (fast intro: if_eq_cases)
- next
- case False
- have "(if ?G then ?merge ss x else Err) = ?if ((pc',s')#ss) x"
- proof (cases ?G)
- assume G: ?G with False
- have "?if ss x = ?if ((pc',s')#ss) x" by (auto simp add: OK_snd)
- hence "?merge ss x = ?if ((pc',s')#ss) x" by (simp only: IH)
- with G show ?thesis by (fast intro: if_eq_cases)
- next
- assume G: "\<not>?G"
- with False have "Err = ?if ((pc',s')#ss) x" by auto
- with G show ?thesis by (fast intro: if_eq_cases)
- qed
- with False show ?thesis by (fast intro: if_eq_cases)
- qed
- also from s have "\<dots> = ?if (s#ss) x" by hypsubst (rule refl)
- finally show "?P (s#ss) x" .
-qed
-
-
-lemma wtl_inst_OK:
-"(wtl_inst i G rT s cert mxs mxr max_pc et pc = OK s') = (
- app i G mxs rT pc et s \<and>
- (\<forall>(pc',r) \<in> set (eff i G pc et s).
- pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> r <=' cert!pc')) \<and>
- map (OK \<circ> snd) [(p',t') \<in> (eff i G pc et s). p'=pc+1]
- ++_(sup G mxs mxr) (OK (cert!(pc+1))) = OK s')"
- by (auto simp add: wtl_inst_def merge_def split: split_if_asm)
-
lemma wtl_Cons:
- "wtl_inst_list (i#is) G rT cert maxs maxr max_pc et pc s \<noteq> Err =
- (\<exists>s'. wtl_cert i G rT s cert maxs maxr max_pc et pc = OK s' \<and>
- wtl_inst_list is G rT cert maxs maxr max_pc et (pc+1) s' \<noteq> Err)"
+ "wtl_inst_list (i#is) cert f r step pc s \<noteq> Err =
+ (\<exists>s'. wtl_cert cert f r step pc s = OK s' \<and>
+ wtl_inst_list is cert f r step (pc+1) s' \<noteq> Err)"
by (auto simp del: split_paired_Ex)
lemma wtl_append:
-"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mxs mxr mpc et pc s = OK s') =
- (\<exists>s''. wtl_inst_list a G rT cert mxs mxr mpc et pc s = OK s'' \<and>
- wtl_inst_list b G rT cert mxs mxr mpc et (pc+length a) s'' = OK s')"
- (is "\<forall> s pc. ?C s pc a" is "?P a")
+"\<forall>s pc. (wtl_inst_list (a@b) cert f r step pc s = OK s') =
+ (\<exists>s''. wtl_inst_list a cert f r step pc s = OK s'' \<and>
+ wtl_inst_list b cert f r step (pc+length a) s'' = OK s')"
+ (is "\<forall>s pc. ?C s pc a" is "?P a")
proof (induct ?P a)
show "?P []" by simp
next
@@ -162,28 +223,28 @@
proof (intro allI)
fix s pc
show "?C s pc (x#xs)"
- proof (cases "wtl_cert x G rT s cert mxs mxr mpc et pc")
+ proof (cases "wtl_cert cert f r step pc s")
case Err thus ?thesis by simp
next
- fix s0 assume "wtl_cert x G rT s cert mxs mxr mpc et pc = OK s0"
- with IH have "?C s0 (Suc pc) xs" by blast
+ case (OK s0)
+ with IH have "?C s0 (pc+1) xs" by blast
thus ?thesis by (simp!)
qed
qed
qed
lemma wtl_take:
- "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s'' \<Longrightarrow>
- \<exists>s'. wtl_inst_list (take pc' is) G rT cert mxs mxr mpc et pc s = OK s'"
+ "wtl_inst_list is cert f r step pc s = OK s'' \<Longrightarrow>
+ \<exists>s'. wtl_inst_list (take pc' is) cert f r step pc s = OK s'"
+ (is "?wtl is = _ \<Longrightarrow> _")
proof -
- assume "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s''"
- hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mxs mxr mpc et pc s = OK s''"
- by simp
+ assume "?wtl is = OK s''"
+ hence "?wtl (take pc' is @ drop pc' is) = OK s''" by simp
thus ?thesis by (auto simp add: wtl_append simp del: append_take_drop_id)
qed
lemma take_Suc:
- "\<forall>n. n < length l \<longrightarrow> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
+ "\<forall>n. n < length l --> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
proof (induct l)
show "?P []" by simp
next
@@ -197,39 +258,137 @@
qed
lemma wtl_Suc:
- "\<lbrakk> wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s';
- wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s'';
- Suc pc < length is \<rbrakk> \<Longrightarrow>
- wtl_inst_list (take (Suc pc) is) G rT cert maxs maxr (length is) et 0 s = OK s''"
+ assumes "wtl_inst_list (take pc is) cert f r step 0 s = OK s'"
+ "wtl_cert cert f r step pc s' = OK s''" and
+ suc: "pc+1 < length is"
+ shows "wtl_inst_list (take (pc+1) is) cert f r step 0 s = OK s''"
proof -
- assume "wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s'"
- "wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s''"
- "Suc pc < length is"
- hence "take (Suc pc) is = (take pc is)@[is!pc]" by (simp add: take_Suc)
+ from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
thus ?thesis by (simp! add: wtl_append min_def)
qed
lemma wtl_all:
- "\<lbrakk> wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err;
- pc < length is \<rbrakk> \<Longrightarrow>
- \<exists>s' s''. wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s' \<and>
- wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s''"
+ assumes
+ all: "wtl_inst_list is cert f r step 0 s \<noteq> Err" (is "?wtl is \<noteq> _") and
+ pc: "pc < length is"
+ shows
+ "\<exists>s' s''. wtl_inst_list (take pc is) cert f r step 0 s = OK s' \<and>
+ wtl_cert cert f r step pc s' = OK s''"
proof -
- assume all: "wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err"
-
- assume pc: "pc < length is"
- hence "0 < length (drop pc is)" by simp
+ from pc have "0 < length (drop pc is)" by simp
then obtain i r where Cons: "drop pc is = i#r"
by (auto simp add: neq_Nil_conv simp del: length_drop)
hence "i#r = drop pc is" ..
- with all have take:
- "wtl_inst_list (take pc is@i#r) G rT cert maxs maxr (length is) et 0 s \<noteq> Err"
- by simp
-
+ with all have take: "?wtl (take pc is@i#r) \<noteq> Err" by simp
from pc have "is!pc = drop pc is ! 0" by simp
with Cons have "is!pc = i" by simp
with take pc show ?thesis by (auto simp add: wtl_append min_def)
qed
+section "preserves-type"
+
+lemma merge_pres:
+ assumes semi: "err_semilat (A,r,f)"
+ assumes s0_A: "\<forall>(pc', s')\<in>set ss. s' \<in> err (opt A)"
+ assumes x_A: "x \<in> err (opt A)"
+ assumes merge:"merge cert f r pc ss x = OK s'"
+ shows "s' \<in> opt A"
+proof -
+ from s0_A
+ have "set (map snd [(p', t')\<in>ss . p'=pc+1]) \<subseteq> err (opt A)" by auto
+ with semi x_A
+ have "(map snd [(p', t')\<in>ss . p'=pc+1] ++|f x) \<in> err (opt A)"
+ by (auto intro!: plusplus_closed)
+ also {
+ note merge
+ also from semi x_A s0_A
+ have "merge cert f r pc ss x =
+ (if \<forall>(pc', s')\<in>set ss. pc' \<noteq> pc + 1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))
+ then map snd [(p', t')\<in>ss . p'=pc+1] ++|f x else Err)"
+ by (rule merge_def)
+ finally have "(map snd [(p', t')\<in>ss . p'=pc+1] ++|f x) = OK s'"
+ by (simp split: split_if_asm)
+ }
+ finally show ?thesis by simp
+qed
+
+
+
+lemma wtl_inst_pres [intro?]:
+ assumes semi: "err_semilat (A,r,f)"
+ assumes pres: "pres_type step n (err (opt A))"
+ assumes cert: "cert!(pc+1) \<in> opt A"
+ assumes s_A: "s \<in> opt A"
+ assumes pc: "pc < n"
+ assumes wtl: "wtl_inst cert f r step pc s = OK s'"
+ shows "s' \<in> opt A"
+proof -
+ from pres pc s_A
+ have "\<forall>(q, s')\<in>set (step pc (OK s)). s' \<in> err (opt A)"
+ by (unfold pres_type_def) blast
+ moreover
+ from cert have "OK (cert!(pc+1)) \<in> err (opt A)" by simp
+ moreover
+ from wtl
+ have "merge cert f r pc (step pc (OK s)) (OK (cert!(pc+1))) = OK s'"
+ by (unfold wtl_inst_def) simp
+ ultimately
+ show "s' \<in> opt A" using semi by - (rule merge_pres)
+qed
+
+
+lemma wtl_cert_pres:
+ assumes "err_semilat (A,r,f)"
+ assumes "pres_type step n (err (opt A))"
+ assumes "cert!pc \<in> opt A" and "cert!(pc+1) \<in> opt A"
+ assumes "s \<in> opt A" and "pc < n"
+ assumes wtc: "wtl_cert cert f r step pc s = OK s'"
+ shows "s' \<in> opt A"
+proof -
+ have "wtl_inst cert f r step pc s = OK s' \<Longrightarrow> s' \<in> opt A" ..
+ moreover
+ have "wtl_inst cert f r step pc (cert!pc) = OK s' \<Longrightarrow> s' \<in> opt A" ..
+ ultimately
+ show ?thesis using wtc
+ by (unfold wtl_cert_def) (simp split: option.splits split_if_asm)
+qed
+
+lemma wtl_inst_list_pres:
+ assumes semi: "err_semilat (A,r,f)"
+ assumes pres: "pres_type step (length is) (err (opt A))"
+ assumes cert: "cert_ok cert (length is) A"
+ assumes s: "s \<in> opt A"
+ assumes all: "wtl_inst_list is cert f r step 0 s \<noteq> Err"
+ shows "\<And>s'. pc < length is \<Longrightarrow> wtl_inst_list (take pc is) cert f r step 0 s = OK s'
+ \<Longrightarrow> s' \<in> opt A" (is "\<And>s'. ?len pc \<Longrightarrow> ?wtl pc s' \<Longrightarrow> ?A s'")
+proof (induct pc)
+ from s show "\<And>s'. ?wtl 0 s' \<Longrightarrow> ?A s'" by simp
+next
+ fix s' n
+ assume "Suc n < length is"
+ then obtain "n < length is" by simp
+ with all obtain s1 s2 where
+ "wtl_inst_list (take n is) cert f r step 0 s = OK s1"
+ "wtl_cert cert f r step n s1 = OK s2"
+ by - (drule wtl_all, auto)
+
+ assume "?wtl (Suc n) s'"
+ moreover
+ have n1: "n+1 < length is" by simp
+ hence "?wtl (n+1) s2" by - (rule wtl_Suc)
+ ultimately
+ have [simp]: "s2 = s'" by simp
+
+ assume IH: "\<And>s'. n < length is \<Longrightarrow> ?wtl n s' \<Longrightarrow> s' \<in> opt A"
+ hence "s1 \<in> opt A" .
+ moreover
+ from cert have "cert!n \<in> opt A" by (rule cert_okD)
+ moreover
+ from cert n1 have "cert!(n+1) \<in> opt A" by (rule cert_okD)
+ ultimately
+ have "s2 \<in> opt A" using semi pres by - (rule wtl_cert_pres)
+ thus "s' \<in> opt A" by simp
+qed
+
end