theory "HOLCF-Join" imports "~~/src/HOL/HOLCF/HOLCF" begin subsubsection {* Binary Joins and compatibility *} context cpo begin definition join :: "'a => 'a => 'a" (infixl "⊔" 80) where "x ⊔ y = (if ∃ z. {x, y} <<| z then lub {x, y} else x)" definition compatible :: "'a ⇒ 'a ⇒ bool" where "compatible x y = (∃ z. {x, y} <<| z)" lemma compatibleI: assumes "x ⊑ z" assumes "y ⊑ z" assumes "⋀ a. ⟦ x ⊑ a ; y ⊑ a ⟧ ⟹ z ⊑ a" shows "compatible x y" proof- from assms have "{x,y} <<| z" by (auto intro: is_lubI) thus ?thesis unfolding compatible_def by (metis) qed lemma is_joinI: assumes "x ⊑ z" assumes "y ⊑ z" assumes "⋀ a. ⟦ x ⊑ a ; y ⊑ a ⟧ ⟹ z ⊑ a" shows "x ⊔ y = z" proof- from assms have "{x,y} <<| z" by (auto intro: is_lubI) thus ?thesis unfolding join_def by (metis lub_eqI) qed lemma is_join_and_compatible: assumes "x ⊑ z" assumes "y ⊑ z" assumes "⋀ a. ⟦ x ⊑ a ; y ⊑ a ⟧ ⟹ z ⊑ a" shows "compatible x y ∧ x ⊔ y = z" by (metis compatibleI is_joinI assms) lemma compatible_sym: "compatible x y ⟹ compatible y x" unfolding compatible_def by (metis insert_commute) lemma compatible_sym_iff: "compatible x y ⟷ compatible y x" unfolding compatible_def by (metis insert_commute) lemma join_above1: "compatible x y ⟹ x ⊑ x ⊔ y" unfolding compatible_def join_def apply auto by (metis is_lubD1 is_ub_insert lub_eqI) lemma join_above2: "compatible x y ⟹ y ⊑ x ⊔ y" unfolding compatible_def join_def apply auto by (metis is_lubD1 is_ub_insert lub_eqI) lemma larger_is_join1: "y ⊑ x ⟹ x ⊔ y = x" unfolding join_def by (metis doubleton_eq_iff lub_bin) lemma larger_is_join2: "x ⊑ y ⟹ x ⊔ y = y" unfolding join_def by (metis is_lub_bin lub_bin) lemma join_self[simp]: "x ⊔ x = x" unfolding join_def by auto end lemma join_commute: "compatible x y ⟹ x ⊔ y = y ⊔ x" unfolding compatible_def unfolding join_def by (metis insert_commute) lemma lub_is_join: "{x, y} <<| z ⟹ x ⊔ y = z" unfolding join_def by (metis lub_eqI) lemma compatible_refl[simp]: "compatible x x" by (rule compatibleI[OF below_refl below_refl]) lemma join_mono: assumes "compatible a b" and "compatible c d" and "a ⊑ c" and "b ⊑ d" shows "a ⊔ b ⊑ c ⊔ d" proof- from assms obtain x y where "{a, b} <<| x" "{c, d} <<| y" unfolding compatible_def by auto with assms have "a ⊑ y" "b ⊑ y" by (metis below.r_trans is_lubD1 is_ub_insert)+ with `{a, b} <<| x` have "x ⊑ y" by (metis is_lub_below_iff is_lub_singleton is_ub_insert) moreover from `{a, b} <<| x` `{c, d} <<| y` have "a ⊔ b = x" "c ⊔ d = y" by (metis lub_is_join)+ ultimately show ?thesis by simp qed lemma assumes "compatible x y" shows join_above1: "x ⊑ x ⊔ y" and join_above2: "y ⊑ x ⊔ y" proof- from assms obtain z where "{x,y} <<| z" unfolding compatible_def by auto hence "x ⊔ y = z" and "x ⊑ z" and "y ⊑ z" apply (auto intro: lub_is_join) by (metis is_lubD1 is_ub_insert)+ thus "x ⊑ x ⊔ y" and "y ⊑ x ⊔ y" by simp_all qed lemma assumes "compatible x y" shows compatible_above1: "compatible x (x ⊔ y)" and compatible_above2: "compatible y (x ⊔ y)" proof- from assms obtain z where "{x,y} <<| z" unfolding compatible_def by auto hence "x ⊔ y = z" and "x ⊑ z" and "y ⊑ z" apply (auto intro: lub_is_join) by (metis is_lubD1 is_ub_insert)+ thus "compatible x (x ⊔ y)" and "compatible y (x ⊔ y)" by (metis below.r_refl compatibleI)+ qed lemma join_below: assumes "compatible x y" and "x ⊑ a" and "y ⊑ a" shows "x ⊔ y ⊑ a" proof- from assms obtain z where z: "{x,y} <<| z" unfolding compatible_def by auto with assms have "z ⊑ a" by (metis is_lub_below_iff is_ub_empty is_ub_insert) moreover from z have "x ⊔ y = z" by (rule lub_is_join) ultimately show ?thesis by simp qed lemma join_below_iff: assumes "compatible x y" shows "x ⊔ y ⊑ a ⟷ (x ⊑ a ∧ y ⊑ a)" by (metis assms below_trans cpo_class.join_above1 cpo_class.join_above2 join_below) lemma join_assoc: assumes "compatible x y" assumes "compatible x (y ⊔ z)" assumes "compatible y z" shows "(x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)" apply (rule is_joinI) apply (rule join_mono[OF assms(1) assms(2) below_refl join_above1[OF assms(3)]]) apply (rule below_trans[OF join_above2[OF assms(3)] join_above2[OF assms(2)]]) apply (rule join_below[OF assms(2)]) apply (erule rev_below_trans) apply (rule join_above1[OF assms(1)]) apply (rule join_below[OF assms(3)]) apply (erule rev_below_trans) apply (rule join_above2[OF assms(1)]) apply assumption done lemma join_idem[simp]: "compatible x y ⟹ x ⊔ (x ⊔ y) = x ⊔ y" apply (subst join_assoc[symmetric]) apply (rule compatible_refl) apply (erule compatible_above1) apply assumption apply (subst join_self) apply rule done lemma join_bottom[simp]: "x ⊔ ⊥ = x" "⊥ ⊔ x = x" by (auto intro: is_joinI) lemma compatible_adm2: shows "adm (λ y. compatible x y)" proof(rule admI) fix Y assume c: "chain Y" and "∀i. compatible x (Y i)" hence a: "⋀ i. compatible x (Y i)" by auto show "compatible x (⨆ i. Y i)" proof(rule compatibleI) have c2: "chain (λi. x ⊔ Y i)" apply (rule chainI) apply (rule join_mono[OF a a below_refl chainE[OF `chain Y`]]) done show "x ⊑ (⨆ i. x ⊔ Y i)" by (auto intro: admD[OF _ c2] join_above1[OF a]) show "(⨆ i. Y i) ⊑ (⨆ i. x ⊔ Y i)" by (auto intro: admD[OF _ c] below_lub[OF c2 join_above2[OF a]]) fix a assume "x ⊑ a" and "(⨆ i. Y i) ⊑ a" show "(⨆ i. x ⊔ Y i) ⊑ a" apply (rule lub_below[OF c2]) apply (rule join_below[OF a `x ⊑ a`]) apply (rule below_trans[OF is_ub_thelub[OF c] `(⨆ i. Y i) ⊑ a`]) done qed qed lemma compatible_adm1: "adm (λ x. compatible x y)" by (subst compatible_sym_iff, rule compatible_adm2) lemma join_cont1: assumes "chain Y" assumes compat: "⋀ i. compatible (Y i) y" shows "(⨆i. Y i) ⊔ y = (⨆ i. Y i ⊔ y)" proof- have c: "chain (λi. Y i ⊔ y)" apply (rule chainI) apply (rule join_mono[OF compat compat chainE[OF `chain Y`] below_refl]) done show ?thesis apply (rule is_joinI) apply (rule lub_mono[OF `chain Y` c join_above1[OF compat]]) apply (rule below_lub[OF c join_above2[OF compat]]) apply (rule lub_below[OF c]) apply (rule join_below[OF compat]) apply (metis lub_below_iff[OF `chain Y`]) apply assumption done qed lemma join_cont2: assumes "chain Y" assumes compat: "⋀ i. compatible x (Y i)" shows "x ⊔ (⨆i. Y i) = (⨆ i. x ⊔ Y i)" proof- have c: "chain (λi. x ⊔ Y i)" apply (rule chainI) apply (rule join_mono[OF compat compat below_refl chainE[OF `chain Y`]]) done show ?thesis apply (rule is_joinI) apply (rule below_lub[OF c join_above1[OF compat]]) apply (rule lub_mono[OF `chain Y` c join_above2[OF compat]]) apply (rule lub_below[OF c]) apply (rule join_below[OF compat]) apply assumption apply (metis lub_below_iff[OF `chain Y`]) done qed lemma join_cont12: assumes "chain Y" and "chain Z" assumes compat: "⋀ i j. compatible (Y i) (Z j)" shows "(⨆i. Y i) ⊔ (⨆i. Z i) = (⨆ i. Y i ⊔ Z i)" proof- have "(⨆i. Y i) ⊔ (⨆i. Z i) = (⨆i. Y i ⊔ (⨆j. Z j))" by (rule join_cont1[OF `chain Y` admD[OF compatible_adm2 `chain Z` compat]]) also have "... = (⨆i j. Y i ⊔ Z j)" by (subst join_cont2[OF `chain Z` compat], rule) also have "... = (⨆i. Y i ⊔ Z i)" apply (rule diag_lub) apply (rule chainI, rule join_mono[OF compat compat chainE[OF `chain Y`] below_refl]) apply (rule chainI, rule join_mono[OF compat compat below_refl chainE[OF `chain Z`]]) done finally show ?thesis. qed context pcpo begin lemma bot_compatible[simp]: "compatible x ⊥" "compatible ⊥ x" unfolding compatible_def by (metis insert_commute is_lub_bin minimal)+ end end