primrec merge :: "'s certificate \ 's binop \ 's ord \ 's \ nat \ (nat \ 's) list \ 's \ 's" where "merge cert f r T pc [] x = x"
| "merge cert f r T pc (s#ss) x = merge cert f r T pc ss (let (pc',s') = s in if pc'=pc+1 then s' +_f x
else if s' <=_r (cert!pc') then x
else T)"
definition wtl_inst :: "'s certificate \ 's binop \ 's ord \ 's \ 's step_type \ nat \ 's \ 's" where "wtl_inst cert f r T step pc s \ merge cert f r T pc (step pc s) (cert!(pc+1))"
definition wtl_cert :: "'s certificate \ 's binop \ 's ord \ 's \ 's \ 's step_type \ nat \ 's \ 's" where "wtl_cert cert f r T B step pc s \ if cert!pc = B then
wtl_inst cert f r T step pc s
else if s <=_r (cert!pc) then wtl_inst cert f r T step pc (cert!pc) else T"
primrec wtl_inst_list :: "'a list \ 's certificate \ 's binop \ 's ord \ 's \ 's \ 's step_type \ nat \ 's \ 's" where "wtl_inst_list [] cert f r T B step pc s = s"
| "wtl_inst_list (i#is) cert f r T B step pc s =
(let s' = wtl_cert cert f r T B step pc s in if s' = T \ s = T then T else wtl_inst_list is cert f r T B step (pc+1) s')"
definition cert_ok :: "'s certificate \ nat \ 's \ 's \ 's set \ bool" where "cert_ok cert n T B A \ (\i < n. cert!i \ A \ cert!i \ T) \ (cert!n = B)"
definition bottom :: "'a ord \ 'a \ bool" where "bottom r B \ \x. B <=_r x"
locale lbv = Semilat + fixes T :: "'a" (\<open>\<top>\<close>) fixes B :: "'a" (\<open>\<bottom>\<close>) fixes step :: "'a step_type" assumes top: "top r \" assumes T_A: "\ \ A" assumes bot: "bottom r \" assumes B_A: "\ \ A"
fixes merge :: "'a certificate \ nat \ (nat \ 'a) list \ 'a \ 'a" defines mrg_def: "merge cert \ LBVSpec.merge cert f r \"
fixes wti :: "'a certificate \ nat \ 'a \ 'a" defines wti_def: "wti cert \ wtl_inst cert f r \ step"
fixes wtc :: "'a certificate \ nat \ 'a \ 'a" defines wtc_def: "wtc cert \ wtl_cert cert f r \ \ step"
fixes wtl :: "'b list \ 'a certificate \ nat \ 'a \ 'a" defines wtl_def: "wtl ins cert \ wtl_inst_list ins cert f r \ \ step"
lemma (in lbv) wti: "wti c pc s \ merge c pc (step pc s) (c!(pc+1))" by (simp add: wti_def mrg_def wtl_inst_def)
lemma (in lbv) wtc: "wtc c pc s \ if c!pc = \ then wti c pc s else if s <=_r c!pc then wti c pc (c!pc) else \" by (unfold wtc_def wti_def wtl_cert_def)
lemma cert_okD1 [intro?]: "cert_ok c n T B A \ pc < n \ c!pc \ A" by (unfold cert_ok_def) fast
lemma cert_okD2 [intro?]: "cert_ok c n T B A \ c!n = B" by (simp add: cert_ok_def)
lemma cert_okD3 [intro?]: "cert_ok c n T B A \ B \ A \ pc < n \ c!Suc pc \ A" by (drule Suc_leI) (auto simp add: le_eq_less_or_eq dest: cert_okD1 cert_okD2)
lemma cert_okD4 [intro?]: "cert_ok c n T B A \ pc < n \ c!pc \ T" by (simp add: cert_ok_def)
declare Let_def [simp]
subsection "more semilattice lemmas"
lemma (in lbv) sup_top [simp, elim]: assumes x: "x \ A" shows"x +_f \ = \" proof - from top have"x +_f \ <=_r \" .. moreoverfrom x T_A have"\ <=_r x +_f \" .. ultimatelyshow ?thesis .. qed
lemma (in lbv) plusplussup_top [simp, elim]: "set xs \ A \ xs ++_f \ = \" by (induct xs) auto
lemma (in Semilat) pp_ub1': assumes S: "snd`set S \ A" assumes y: "y \ A" and ab: "(a, b) \ set S" shows"b <=_r map snd [(p', t') \ S . p' = a] ++_f y" proof - from S have"\(x,y) \ set S. y \ A" by auto with semilat y ab show ?thesis by - (rule ub1') qed
lemma (in lbv) bottom_le [simp, intro]: "\ <=_r x" using bot by (simp add: bottom_def)
lemma (in lbv) le_bottom [simp]: "x <=_r \ = (x = \)" by (blast intro: antisym_r)
subsection "merge"
lemma (in lbv) merge_Nil [simp]: "merge c pc [] x = x"by (simp add: mrg_def)
lemma (in lbv) merge_Cons [simp]: "merge c pc (l#ls) x = merge c pc ls (if fst l=pc+1 then snd l +_f x
else if snd l <=_r (c!fst l) then x
else \<top>)" by (simp add: mrg_def split_beta)
lemma (in lbv) merge_Err [simp]: "snd`set ss \ A \ merge c pc ss \ = \" by (induct ss) auto
lemma (in lbv) merge_not_top: "\x. snd`set ss \ A \ merge c pc ss x \ \ \ \<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' <=_r (c!pc'))"
(is"\x. ?set ss \ ?merge ss x \ ?P ss") proof (induct ss) show"?P []"by simp next fix x ls l assume"?set (l#ls)"thenobtain set: "snd`set ls \ A" by simp assume merge: "?merge (l#ls) x" moreover obtain pc' s'where l: "l = (pc',s')"by (cases l) ultimately obtain x' where merge': "?merge ls x'"by simp assume"\x. ?set ls \ ?merge ls x \ ?P ls" hence "?P ls" using set merge' . moreover from merge set have"pc' \ pc+1 \ s' <=_r (c!pc')" by (simp add: l split: if_split_asm) ultimately show"?P (l#ls)"by (simp add: l) qed
lemma (in lbv) merge_def: shows "\x. x \ A \ snd`set ss \ A \
merge c pc ss x =
(if\<forall>(pc',s') \<in> set ss. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc' then
map snd [(p',t') \<leftarrow> ss. p'=pc+1] ++_f x
else \<top>)"
(is"\x. _ \ _ \ ?merge ss x = ?if ss x" is "\x. _ \ _ \ ?P ss x") proof (induct ss) fix x show"?P [] x"by simp next fix x assume x: "x \ A" fix l::"nat \ 'a" and ls assume"snd`set (l#ls) \ A" thenobtain l: "snd l \ A" and ls: "snd`set ls \ A" by auto assume"\x. x \ A \ snd`set ls \ A \ ?P ls x" hence IH: "\x. x \ A \ ?P ls x" using ls by iprover 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' <=_r c!pc'then x else \<top>)"
(is"?merge (l#ls) x = ?merge ls ?if'") by simp alsohave"\ = ?if ls ?if'" proof - from l have"s' \ A" by simp with x have"s' +_f x \ A" by simp with x T_A have"?if' \ A" by auto hence"?P ls ?if'"by (rule IH) thus ?thesis by simp qed alsohave"\ = ?if (l#ls) x" proof (cases "\(pc', s')\set (l#ls). pc'\pc+1 \ s' <=_r c!pc'") case True hence"\(pc', s')\set ls. pc'\pc+1 \ s' <=_r c!pc'" by auto moreover from True have "map snd [(p',t')\ls . p'=pc+1] ++_f ?if' =
(map snd [(p',t')\<leftarrow>l#ls . p'=pc+1] ++_f x)" by simp ultimately show ?thesis using True by simp next case False moreover from ls have"set (map snd [(p', t')\ls . p' = Suc pc]) \ A" by auto ultimatelyshow ?thesis by auto qed finallyshow"?P (l#ls) x" . qed
lemma (in lbv) merge_not_top_s: assumes x: "x \ A" and ss: "snd`set ss \ A" assumes m: "merge c pc ss x \ \" shows"merge c pc ss x = (map snd [(p',t') \ ss. p'=pc+1] ++_f x)" proof - from ss m have"\(pc',s') \ set ss. (pc' \ pc+1 \ s' <=_r c!pc')" by (rule merge_not_top) with x ss m show ?thesis by - (drule merge_def, auto split: if_split_asm) qed
subsection "wtl-inst-list"
lemmas [iff] = not_Err_eq
lemma (in lbv) wtl_Nil [simp]: "wtl [] c pc s = s" by (simp add: wtl_def)
lemma (in lbv) wtl_Cons [simp]: "wtl (i#is) c pc s =
(let s' = wtc c pc s in if s' = \<top> \<or> s = \<top> then \<top> else wtl is c (pc+1) s')" by (simp add: wtl_def wtc_def)
lemma (in lbv) wtl_Cons_not_top: "wtl (i#is) c pc s \ \ =
(wtc c pc s \<noteq> \<top> \<and> s \<noteq> T \<and> wtl is c (pc+1) (wtc c pc s) \<noteq> \<top>)" by (auto simp del: split_paired_Ex)
lemma (in lbv) wtl_top [simp]: "wtl ls c pc \ = \" by (cases ls) auto
lemma (in lbv) wtl_not_top: "wtl ls c pc s \ \ \ s \ \" by (cases "s=\") auto
lemma (in lbv) wtl_append [simp]: "\pc s. wtl (a@b) c pc s = wtl b c (pc+length a) (wtl a c pc s)" by (induct a) auto
lemma (in lbv) wtl_take: "wtl is c pc s \ \ \ wtl (take pc' is) c pc s \ \"
(is"?wtl is \ _ \ _") proof - assume"?wtl is \ \" hence"?wtl (take pc' is @ drop pc' is) \ \" by simp thus ?thesis by (auto dest!: wtl_not_top simp del: append_take_drop_id) qed
lemma take_Suc: "\n. n < length l \ take (Suc n) l = (take n l)@[l!n]" (is "?P l") proof (induct l) show"?P []"by simp next fix x xs assume IH: "?P xs" show"?P (x#xs)" proof (intro strip) fix n assume"n < length (x#xs)" with IH show"take (Suc n) (x # xs) = take n (x # xs) @ [(x # xs) ! n]" by (cases n, auto) qed qed
lemma (in lbv) wtl_Suc: assumes suc: "pc+1 < length is" assumes wtl: "wtl (take pc is) c 0 s \ \" shows"wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)" proof - from suc have"take (pc+1) is=(take pc is)@[is!pc]"by (simp add: take_Suc) with suc wtl show ?thesis by (simp add: min.absorb2) qed
lemma (in lbv) wtl_all: assumes all: "wtl is c 0 s \ \" (is "?wtl is \ _") assumes pc: "pc < length is" shows"wtc c pc (wtl (take pc is) c 0 s) \ \" proof - from pc have"0 < length (drop pc is)"by simp thenobtain i r where Cons: "drop pc is = i#r" by (auto simp add: neq_Nil_conv simp del: length_drop drop_eq_Nil) hence"i#r = drop pc is" .. with all have take: "?wtl (take pc is@i#r) \ \" 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: min.absorb2) qed
subsection "preserves-type"
lemma (in lbv) merge_pres: assumes s0: "snd`set ss \ A" and x: "x \ A" shows"merge c pc ss x \ A" proof - from s0 have"set (map snd [(p', t')\ss . p'=pc+1]) \ A" by auto with x have"(map snd [(p', t')\ss . p'=pc+1] ++_f x) \ A" by (auto intro!: plusplus_closed semilat) with s0 x show ?thesis by (simp add: merge_def T_A) qed
lemma pres_typeD2: "pres_type step n A \ s \ A \ p < n \ snd`set (step p s) \ A" by auto (drule pres_typeD)
lemma (in lbv) wti_pres [intro?]: assumes pres: "pres_type step n A" assumes cert: "c!(pc+1) \ A" assumes s_pc: "s \ A" "pc < n" shows"wti c pc s \ A" proof - from pres s_pc have"snd`set (step pc s) \ A" by (rule pres_typeD2) with cert show ?thesis by (simp add: wti merge_pres) qed
lemma (in lbv) wtc_pres: assumes pres: "pres_type step n A" assumes cert: "c!pc \ A" and cert': "c!(pc+1) \ A" assumes s: "s \ A" and pc: "pc < n" shows"wtc c pc s \ A" proof - have"wti c pc s \ A" using pres cert' s pc .. moreoverhave"wti c pc (c!pc) \ A" using pres cert' cert pc .. ultimatelyshow ?thesis using T_A by (simp add: wtc) qed
lemma (in lbv) wtl_pres: assumes pres: "pres_type step (length is) A" assumes cert: "cert_ok c (length is) \ \ A" assumes s: "s \ A" assumes all: "wtl is c 0 s \ \" shows"pc < length is \ wtl (take pc is) c 0 s \ A"
(is"?len pc \ ?wtl pc \ A") proof (induct pc) from s show"?wtl 0 \ A" by simp next fix n assume IH: "Suc n < length is" thenhave n: "n < length is"by simp from IH have n1: "n+1 < length is"by simp assume prem: "n < length is \ ?wtl n \ A" have"wtc c n (?wtl n) \ A" using pres _ _ _ n proof (rule wtc_pres) from prem n show"?wtl n \ A" . from cert n show"c!n \ A" by (rule cert_okD1) from cert n1 show"c!(n+1) \ A" by (rule cert_okD1) qed also from all n have"?wtl n \ \" by - (rule wtl_take) with n1 have"wtc c n (?wtl n) = ?wtl (n+1)"by (rule wtl_Suc [symmetric]) finallyshow"?wtl (Suc n) \ A" by simp qed
end
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
