Theory HOLCF-Join-Classes

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))"
  by (simp only: join_comm) (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)

(* subclass (in Join_cpo)  pcpo *)
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