Theory Jinja.SemilatAlg
section ‹More on Semilattices›
theory SemilatAlg
imports Typing_Framework_1
begin
definition lesubstep_type :: "(nat × 's) set ⇒ 's ord ⇒ (nat × 's) set ⇒ bool"
(‹(_ /{⊑⇘_⇙} _)› [50, 0, 51] 50)
where "A {⊑⇘r⇙} B ≡ ∀(p,τ) ∈ A. ∃τ'. (p,τ') ∈ B ∧ τ ⊑⇩r τ'"
notation (ASCII)
lesubstep_type (‹(_ /{<='__} _)› [50, 0, 51] 50)
primrec pluslussub :: "'a list ⇒ ('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ 'a" (‹(_ /⨆⇘_⇙ _)› [65, 0, 66] 65)
where
"pluslussub [] f y = y"
| "pluslussub (x#xs) f y = pluslussub xs f (x ⊔⇩f y)"
notation (ASCII)
pluslussub (‹(_ /++'__ _)› [65, 1000, 66] 65)
definition bounded :: "'s step_type ⇒ nat ⇒ bool"
where
"bounded step n ⟷ (∀p<n. ∀τ. ∀(q,τ') ∈ set (step p τ). q<n)"
definition pres_type :: "'s step_type ⇒ nat ⇒ 's set ⇒ bool"
where
"pres_type step n A ⟷ (∀τ∈A. ∀p<n. ∀(q,τ') ∈ set (step p τ). τ' ∈ A)"
definition mono :: "'s ord ⇒ 's step_type ⇒ nat ⇒ 's set ⇒ bool"
where
"mono r step n A ⟷
(∀τ p τ'. τ ∈ A ∧ p<n ∧ τ ⊑⇩r τ' ⟶ set (step p τ) {⊑⇘r⇙} set (step p τ'))"
lemma [iff]: "{} {⊑⇘r⇙} B"
by (simp add: lesubstep_type_def)
lemma [iff]: "(A {⊑⇘r⇙} {}) = (A = {})"
by (cases "A={}") (auto simp add: lesubstep_type_def)
lemma lesubstep_union:
"⟦ A⇩1 {⊑⇘r⇙} B⇩1; A⇩2 {⊑⇘r⇙} B⇩2 ⟧ ⟹ A⇩1 ∪ A⇩2 {⊑⇘r⇙} B⇩1 ∪ B⇩2"
by (auto simp add: lesubstep_type_def)
lemma pres_typeD:
"⟦ pres_type step n A; s∈A; p<n; (q,s')∈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 ⟧ ⟹ set (step p s) {⊑⇘r⇙} set (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) ⟹ A {⊑⇘r⇙} A"
by (unfold lesubstep_type_def) auto
lemma lesub_step_typeD:
"A {⊑⇘r⇙} B ⟹ (x,y) ∈ A ⟹ ∃y'. (x, y') ∈ 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 (simp only: 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"
proof (induct x)
interpret Semilat A r f by fact
show "⋀y. y ∈ A ⟹ [] ⨆⇘f⇙ y ∈ A" by simp
fix y x xs
assume y: "y ∈ A" and xxs: "set (x#xs) ⊆ A"
assume IH: "⋀y. ⟦ set xs ⊆ A; y ∈ A⟧ ⟹ xs ⨆⇘f⇙ y ∈ A"
from xxs 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
lemma (in Semilat) pp_ub2:
"⋀y. ⟦ set x ⊆ A; y ∈ A⟧ ⟹ y ⊑⇘r⇙ x ⨆⇘f⇙ y"
proof (induct x)
thm plusplus_closed[OF Semilat.intro, OF semilat]
thm semilat_Def
thm Semilat.intro
fix y assume "y ∈ A"
with semilat show "y⊑⇘r⇙ [] ⨆⇘f⇙ y" by simp
fix y a l assume y: "y ∈ A" and "set (a#l) ⊆ A"
then obtain a: "a ∈ A" and x: "set l ⊆ A" by simp
from semilat x y have l_y_inA: "l ⨆⇘f⇙ y ∈ A" by (auto dest: plusplus_closed[OF Semilat.intro, OF semilat])
assume "⋀y. ⟦set l ⊆ A; y ∈ A⟧ ⟹ y ⊑⇘r⇙ l ⨆⇘f⇙ y"
from this and x have IH: "⋀y. y ∈ A ⟹ y ⊑⇘r⇙ l ⨆⇘f⇙ y" .
from a y have "a ⊔⇘f⇙ y ∈ A" ..
then have l_ay_inA: "l ⨆⇘f⇙ ( a ⊔⇘f⇙ y) ∈ A" using plusplus_closed[OF Semilat.intro, OF semilat] x by auto
from a y have "y ⊑⇘r⇙ a ⊔⇘f⇙ y" ..
also from a y have a_y_inA: "a ⊔⇘f⇙ y ∈ A" ..
hence "(a ⊔⇘f⇙ y) ⊑⇘r⇙ l ⨆⇘f⇙ (a ⊔⇘f⇙ y)" by (rule IH)
finally have "y ⊑⇘r⇙ l ⨆⇘f⇙ (a ⊔⇘f⇙ y)" using y a_y_inA l_ay_inA .
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"
then obtain 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"
from this and ls have IH: "⋀y. x ∈ set ls ⟹ y ∈ A ⟹ x ⊑⇘r⇙ ls ⨆⇘f⇙ y" .
from s y have s_y_inA: "s ⊔⇘f⇙ y ∈ A" ..
then have ls_sy_inA: "ls ⨆⇘f⇙ (s ⊔⇘f⇙ y) ∈ A"using plusplus_closed[OF Semilat.intro, OF semilat] ls by auto
assume "x ∈ set (s#ls)"
then obtain xls: "x = s ∨ x ∈ set ls" by simp
moreover {
assume xs: "x = s"
from s y have "s ⊑⇘r⇙ s ⊔⇘f⇙ y" ..
also from ls s_y_inA have "(s ⊔⇘f⇙ y) ⊑⇘r⇙ ls ⨆⇘f⇙ (s ⊔⇘f⇙ y)" by (rule pp_ub2)
finally have "s ⊑⇘r⇙ ls ⨆⇘f⇙ (s ⊔⇘f⇙ y)" using s s_y_inA ls_sy_inA .
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)
moreover from s y have "s ⊔⇘f⇙ y ∈ A" ..
ultimately have "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"
then obtain l: "l ∈ A" and ls: "set ls ⊆ A" by auto
assume "∀x ∈ set (l#ls). x ⊑⇘r⇙ z"
then obtain 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 by fact
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"
apply (induct S)
apply auto
done
end