theory SemilatAlg imports Typing_Framework Product begin
definition lesubstep_type :: "(nat × 's) list ==> 's ord ==> (nat × 's) list ==> bool"
(‹(_ /≤|_| _)› [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 == ∀p∀s. ∀(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 == ∀s p t. s ∈ A ∧ p < n ∧ s <=_r t ⟶ step p s ≤|r| step p t"
lemma pres_typeD: "[ pres_type step n A; s∈A; p∈set (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 ⟶ semilat(A,r,f) ⟶ x∈A ⟶ 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 ==> 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] ==> b <=_r map snd [(p', t')←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') ← S. p' = q] ++_f ss ! q) = ss ! q" by (induct S) auto
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet am 2026-05-03)
¤
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 und die Messung sind noch experimentell.
