Theory HOLCF-Join

theory "HOLCF-Join"
imports 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