theory "HOLCF-Join-Classes"
imports "HOLCF-Join"
begin
class Finite_Join_cpo = cpo +
assumes all_compatible: "compatible x y"
lemmas join_mono = join_mono[OF all_compatible all_compatible ]
lemmas join_above1[simp] = all_compatible[THEN join_above1]
lemmas join_above2[simp] = all_compatible[THEN join_above2]
lemmas join_below[simp] = all_compatible[THEN join_below]
lemmas join_below_iff = all_compatible[THEN join_below_iff]
lemmas join_assoc[simp] = join_assoc[OF all_compatible all_compatible all_compatible]
lemmas join_comm[simp] = all_compatible[THEN join_commute]
lemma join_lc[simp]: "x ⊔ (y ⊔ z) = y ⊔ (x ⊔ (z::'a::Finite_Join_cpo))"
by (metis join_assoc join_comm)
lemma join_cont': "chain Y ⟹ (⨆ i. Y i) ⊔ y = (⨆ i. Y i ⊔ (y::'a::Finite_Join_cpo))"
by (metis all_compatible join_cont1)
lemma join_cont1:
fixes y :: "'a :: Finite_Join_cpo"
shows "cont (λx. (x ⊔ y))"
apply (rule contI2)
apply (rule monofunI)
apply (metis below_refl join_mono)
apply (rule eq_imp_below)
apply (rule join_cont')
apply assumption
done
lemma join_cont2:
fixes x :: "'a :: Finite_Join_cpo"
shows "cont (λy. (x ⊔ y))"
unfolding join_comm by (rule join_cont1)
lemma join_cont[cont2cont,simp]:"cont f ⟹ cont g ⟹ cont (λx. (f x ⊔ (g x::'a::Finite_Join_cpo)))"
apply (rule cont2cont_case_prod[where g = "λ x. (f x, g x)" and f = "λ p x y . x ⊔ y", simplified])
apply (rule join_cont2)
apply (metis cont2cont_Pair)
done
instantiation "fun" :: (type, Finite_Join_cpo) Finite_Join_cpo
begin
definition fun_join :: "('a ⇒ 'b) → ('a ⇒ 'b) → ('a ⇒ 'b)"
where "fun_join = (Λ f g . (λ x. (f x) ⊔ (g x)))"
lemma [simp]: "(fun_join⋅f⋅g) x = (f x) ⊔ (g x)"
unfolding fun_join_def
apply (subst beta_cfun, intro cont2cont cont2cont_lambda cont2cont_fun)+
..
instance
apply standard
proof(intro compatibleI exI conjI strip)
fix x y
show "x ⊑ fun_join⋅x⋅y" by (auto simp add: fun_below_iff)
show "y ⊑ fun_join⋅x⋅y" by (auto simp add: fun_below_iff)
fix z
assume "x ⊑ z" and "y ⊑ z"
thus "fun_join⋅x⋅y ⊑ z" by (auto simp add: fun_below_iff)
qed
end
instantiation "cfun" :: (cpo, Finite_Join_cpo) Finite_Join_cpo
begin
definition cfun_join :: "('a → 'b) → ('a → 'b) → ('a → 'b)"
where "cfun_join = (Λ f g x. (f ⋅ x) ⊔ (g ⋅ x))"
lemma [simp]: "cfun_join⋅f⋅g⋅x = (f ⋅ x) ⊔ (g ⋅ x)"
unfolding cfun_join_def
apply (subst beta_cfun, intro cont2cont cont2cont_lambda cont2cont_fun)+
..
instance
apply standard
proof(intro compatibleI exI conjI strip)
fix x y
show "x ⊑ cfun_join⋅x⋅y" by (auto simp add: cfun_below_iff)
show "y ⊑ cfun_join⋅x⋅y" by (auto simp add: cfun_below_iff)
fix z
assume "x ⊑ z" and "y ⊑ z"
thus "cfun_join⋅x⋅y ⊑ z" by (auto simp add: cfun_below_iff)
qed
end
lemma bot_lub[simp]: "S <<| ⊥ ⟷ S ⊆ {⊥}"
by (auto dest!: is_lubD1 is_ubD intro: is_lubI is_ubI)
lemma compatible_up[simp]: "compatible (up⋅x) (up⋅y) ⟷ compatible x y"
proof
assume "compatible (up⋅x) (up⋅y)"
then obtain z' where z': "{up⋅x,up⋅y} <<| z'" unfolding compatible_def by auto
then obtain z where "{up⋅x,up⋅y} <<| up⋅z" by (cases z') auto
hence "{x,y} <<| z"
unfolding is_lub_def
apply auto
by (metis up_below)
thus "compatible x y" unfolding compatible_def..
next
assume "compatible x y"
then obtain z where z: "{x,y} <<| z" unfolding compatible_def by auto
hence "{up⋅x,up⋅y} <<| up⋅z" unfolding is_lub_def
apply auto
by (metis not_up_less_UU upE up_below)
thus "compatible (up⋅x) (up⋅y)" unfolding compatible_def..
qed
instance u :: (Finite_Join_cpo) Finite_Join_cpo
proof
fix x y :: "'a⇩⊥"
show "compatible x y"
apply (cases x, simp)
apply (cases y, simp)
apply (simp add: all_compatible)
done
qed
class is_unit = fixes unit assumes is_unit: "⋀ x. x = unit"
instantiation unit :: is_unit
begin
definition "unit ≡ ()"
instance
by standard auto
end
instance lift :: (is_unit) Finite_Join_cpo
proof
fix x y :: "'a lift"
show "compatible x y"
apply (cases x, simp)
apply (cases y, simp)
apply (simp add: all_compatible)
apply (subst is_unit)
apply (subst is_unit) back
apply simp
done
qed
instance prod :: (Finite_Join_cpo, Finite_Join_cpo) Finite_Join_cpo
proof
fix x y :: "('a × 'b)"
let ?z = "(fst x ⊔ fst y, snd x ⊔ snd y)"
show "compatible x y"
proof(rule compatibleI)
show "x ⊑ ?z" by (cases x, auto)
show "y ⊑ ?z" by (cases y, auto)
fix z'
assume "x ⊑ z'" and "y ⊑ z'" thus "?z ⊑ z'"
by (cases z', cases x, cases y, auto)
qed
qed
lemma prod_join:
fixes x y :: "'a::Finite_Join_cpo × 'b::Finite_Join_cpo"
shows "x ⊔ y = (fst x ⊔ fst y, snd x ⊔ snd y)"
apply (rule is_joinI)
apply (cases x, auto)[1]
apply (cases y, auto)[1]
apply (cases x, cases y, case_tac a, auto)[1]
done
lemma
fixes x y :: "'a::Finite_Join_cpo × 'b::Finite_Join_cpo"
shows fst_join[simp]: "fst (x ⊔ y) = fst x ⊔ fst y"
and snd_join[simp]: "snd (x ⊔ y) = snd x ⊔ snd y"
unfolding prod_join by simp_all
lemma fun_meet_simp[simp]: "(f ⊔ g) x = f x ⊔ (g x::'a::Finite_Join_cpo)"
proof-
have "f ⊔ g = (λ x. f x ⊔ g x)"
by (rule is_joinI)(auto simp add: fun_below_iff)
thus ?thesis by simp
qed
lemma fun_upd_meet_simp[simp]: "(f ⊔ g) (x := y) = f (x := y) ⊔ g (x := y::'a::Finite_Join_cpo)"
by auto
lemma cfun_meet_simp[simp]: "(f ⊔ g) ⋅ x = f ⋅ x ⊔ (g ⋅ x::'a::Finite_Join_cpo)"
proof-
have "f ⊔ g = (Λ x. f ⋅ x ⊔ g ⋅ x)"
by (rule is_joinI)(auto simp add: cfun_below_iff)
thus ?thesis by simp
qed
lemma cfun_join_below:
fixes f :: "('a::Finite_Join_cpo) → ('b::Finite_Join_cpo)"
shows "f⋅x ⊔ f⋅y ⊑ f⋅(x ⊔ y)"
by (intro join_below monofun_cfun_arg join_above1 join_above2)
lemma join_self_below[iff]:
"x = x ⊔ y ⟷ y ⊑ (x::'a::Finite_Join_cpo)"
"x = y ⊔ x ⟷ y ⊑ (x::'a::Finite_Join_cpo)"
"x ⊔ y = x ⟷ y ⊑ (x::'a::Finite_Join_cpo)"
"y ⊔ x = x ⟷ y ⊑ (x::'a::Finite_Join_cpo)"
"x ⊔ y ⊑ x ⟷ y ⊑ (x::'a::Finite_Join_cpo)"
"y ⊔ x ⊑ x ⟷ y ⊑ (x::'a::Finite_Join_cpo)"
apply (metis join_above2 larger_is_join1)
apply (metis join_above1 larger_is_join2)
apply (metis join_above2 larger_is_join1)
apply (metis join_above1 larger_is_join2)
apply (metis join_above1 join_above2 below_antisym larger_is_join1)
apply (metis join_above2 join_above1 below_antisym larger_is_join2)
done
lemma join_bottom_iff[iff]:
"x ⊔ y = ⊥ ⟷ x = ⊥ ∧ (y::'a::{Finite_Join_cpo,pcpo}) = ⊥"
by (metis all_compatible join_bottom(2) join_comm join_idem)
class Join_cpo = cpo +
assumes exists_lub: "∃u. S <<| u"
context Join_cpo
begin
subclass Finite_Join_cpo
apply standard
unfolding compatible_def
apply (rule exists_lub)
done
end
lemma below_lubI[intro, simp]:
fixes x :: "'a :: Join_cpo"
shows "x ∈ S ⟹ x ⊑ lub S"
by (metis exists_lub is_ub_thelub_ex)
lemma lub_belowI[intro, simp]:
fixes x :: "'a :: Join_cpo"
shows "(⋀ y. y ∈ S ⟹ y ⊑ x) ⟹ lub S ⊑ x"
by (metis exists_lub is_lub_thelub_ex is_ub_def)
instance Join_cpo ⊆ pcpo
apply standard
apply (rule exI[where x = "lub {}"])
apply auto
done
lemma lub_empty_set[simp]:
"lub {} = (⊥::'a::Join_cpo)"
by (rule lub_eqI) simp
lemma lub_insert[simp]:
fixes x :: "'a :: Join_cpo"
shows "lub (insert x S) = x ⊔ lub S"
by (rule lub_eqI) (auto intro: below_trans[OF _ join_above2] simp add: join_below_iff is_ub_def is_lub_def)
end