theory SemilatAlg imports Typing_Framework Product begin
definition lesubstep_type :: "(nat \ 's) list \ 's ord \ (nat \ 's) list \ bool"
(\<open>(_ /\<le>|_| _)\<close> [50, 0, 51] 50) where "x \|r| y \ \(p,s) \ set x. \s'. (p,s') \ set y \ s <=_r s'"
primrec plusplussub :: "'a list \ ('a \ 'a \ 'a) \ 'a \ 'a" (\(_ /++'__ _)\ [65, 1000, 66] 65) where "[] ++_f y = y"
| "(x#xs) ++_f y = xs ++_f (x +_f y)"
definition bounded :: "'s step_type \ nat \ bool" where "bounded step n == \ps. \(q,t)\set(step p s). q
definition pres_type :: "'s step_type \ nat \ 's set \ bool" where "pres_type step n A == \s\A. \p(q,s')\set (step p s). s' \ A"
definition mono :: "'s ord \ 's step_type \ nat \ 's set \ bool" where "mono r step n A == \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> step p s \<le>|r| step p t"
lemma pres_typeD: "\ pres_type step n A; s\A; pset (step p s) \ \ s' \ A" by (unfold pres_type_def, blast)
lemma monoD: "\ mono r step n A; p < n; s\A; s <=_r t \ \ step p s \|r| step p t" by (unfold mono_def, blast)
lemma boundedD: "\ bounded step n; p < n; (q,t) \ set (step p xs) \ \ q < n" by (unfold bounded_def, blast)
lemma lesubstep_type_refl [simp, intro]: "(\x. x <=_r x) \ x \|r| x" by (unfold lesubstep_type_def) auto
lemma lesub_step_typeD: "a \|r| b \ (x,y) \ set a \ \y'. (x, y') \ set b \ y <=_r y'" by (unfold lesubstep_type_def) blast
lemma list_update_le_listI [rule_format]: "set xs <= A \ set ys <= A \ xs <=[r] ys \ p < size xs \
x <=_r ys!p \<longrightarrow> semilat(A,r,f) \<longrightarrow> x\<in>A \<longrightarrow>
xs[p := x +_f xs!p] <=[r] ys" apply (unfold Listn.le_def lesub_def semilat_def) apply (simp add: list_all2_conv_all_nth nth_list_update) done
lemma plusplus_closed: assumes"semilat (A, r, f)"shows "\y. \ set x \ A; y \ A\ \ x ++_f y \ A" (is "PROP ?P") proof - interpret Semilat A r f using assms by (rule Semilat.intro) show"PROP ?P"proof (induct x) show"\y. y \ A \ [] ++_f y \ A" by simp fix y x xs assume y: "y \ A" and xs: "set (x#xs) \ A" assume IH: "\y. \ set xs \ A; y \ A\ \ xs ++_f y \ A" from xs obtain x: "x \ A" and xs': "set xs \ A" by simp from x y have"(x +_f y) \ A" .. with xs' have "xs ++_f (x +_f y) \ A" by (rule IH) thus"(x#xs) ++_f y \ A" by simp qed qed
lemma (in Semilat) pp_ub2: "\y. \ set x \ A; y \ A\ \ y <=_r x ++_f y" proof (induct x) from semilat show"\y. y <=_r [] ++_f y" by simp
fix y a l assume y: "y \ A" assume"set (a#l) \ A" thenobtain a: "a \ A" and x: "set l \ A" by simp assume"\y. \set l \ A; y \ A\ \ y <=_r l ++_f y" hence IH: "\y. y \ A \ y <=_r l ++_f y" using x .
from a y have"y <=_r a +_f y" .. alsofrom a y have"a +_f y \ A" .. hence"(a +_f y) <=_r l ++_f (a +_f y)"by (rule IH) finallyhave"y <=_r l ++_f (a +_f y)" . thus"y <=_r (a#l) ++_f y"by simp qed
lemma (in Semilat) pp_ub1: shows"\y. \set ls \ A; y \ A; x \ set ls\ \ x <=_r ls ++_f y" proof (induct ls) show"\y. x \ set [] \ x <=_r [] ++_f y" by simp
fix y s ls assume"set (s#ls) \ A" thenobtain s: "s \ A" and ls: "set ls \ A" by simp assume y: "y \ A"
assume "\y. \set ls \ A; y \ A; x \ set ls\ \ x <=_r ls ++_f y" hence IH: "\y. x \ set ls \ y \ A \ x <=_r ls ++_f y" using ls .
assume"x \ set (s#ls)" thenobtain xls: "x = s \ x \ set ls" by simp moreover { assume xs: "x = s" from s y have"s <=_r s +_f y" .. alsofrom s y have"s +_f y \ A" .. with ls have"(s +_f y) <=_r ls ++_f (s +_f y)"by (rule pp_ub2) finallyhave"s <=_r ls ++_f (s +_f y)" . with xs have"x <=_r ls ++_f (s +_f y)"by simp
} moreover { assume"x \ set ls" hence"\y. y \ A \ x <=_r ls ++_f y" by (rule IH) moreoverfrom s y have"s +_f y \ A" .. ultimatelyhave"x <=_r ls ++_f (s +_f y)" .
} ultimately have"x <=_r ls ++_f (s +_f y)"by blast thus"x <=_r (s#ls) ++_f y"by simp qed
lemma (in Semilat) pp_lub: assumes z: "z \ A" shows "\y. y \ A \ set xs \ A \ \x \ set xs. x <=_r z \ y <=_r z \ xs ++_f y <=_r z" proof (induct xs) fix y assume"y <=_r z"thus"[] ++_f y <=_r z"by simp next fix y l ls assume y: "y \ A" and "set (l#ls) \ A" thenobtain l: "l \ A" and ls: "set ls \ A" by auto assume"\x \ set (l#ls). x <=_r z" thenobtain lz: "l <=_r z"and lsz: "\x \ set ls. x <=_r z" by auto assume"y <=_r z"with lz have"l +_f y <=_r z"using l y z .. moreover from l y have"l +_f y \ A" .. moreover assume"\y. y \ A \ set ls \ A \ \x \ set ls. x <=_r z \ y <=_r z \<Longrightarrow> ls ++_f y <=_r z" ultimately have"ls ++_f (l +_f y) <=_r z"using ls lsz by - thus"(l#ls) ++_f y <=_r z"by simp qed
lemma ub1': assumes"semilat (A, r, f)" shows"\\(p,s) \ set S. s \ A; y \ A; (a,b) \ set S\ \<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y" proof - interpret Semilat A r f using assms by (rule Semilat.intro)
let"b <=_r ?map ++_f y" = ?thesis
assume"y \ A" moreover assume"\(p,s) \ set S. s \ A" hence"set ?map \ A" by auto moreover assume"(a,b) \ set S" hence"b \ set ?map" by (induct S, auto) ultimately show ?thesis by - (rule pp_ub1) qed
lemma plusplus_empty: "\s'. (q, s') \ set S \ s' +_f ss ! q = ss ! q \
(map snd [(p', t') \<leftarrow> S. p' = q] ++_f ss ! q) = ss ! q" by (induct S) auto
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.
