Theory Complete_Non_Orders.Directedness

theory Directedness
  imports Binary_Relations Well_Relations
begin

text ‹Directed sets:›

locale directed =
  fixes A and less_eq (infix ‹⊑› 50)
  assumes pair_bounded: "x ∈ A ⟹ y ∈ A ⟹ ∃z ∈ A. x ⊑ z ∧ y ⊑ z"

lemmas directedI[intro] = directed.intro

lemmas directedD = directed_def[unfolded atomize_eq, THEN iffD1, rule_format]

context
  fixes less_eq :: "'a ⇒ 'a ⇒ bool" (infix ‹⊑› 50)
begin

lemma directedE:
  assumes "directed A (⊑)" and "x ∈ A" and "y ∈ A"
    and "⋀z. z ∈ A ⟹ x ⊑ z ⟹ y ⊑ z ⟹ thesis"
  shows "thesis"
  using assms by (auto dest: directedD)

lemma directed_empty[simp]: "directed {} (⊑)" by auto

lemma directed_union:
  assumes dX: "directed X (⊑)" and dY: "directed Y (⊑)"
    and XY: "∀x∈X. ∀y∈Y. ∃z ∈ X ∪ Y. x ⊑ z ∧ y ⊑ z"
  shows "directed (X ∪ Y) (⊑)"
  using directedD[OF dX] directedD[OF dY] XY
  apply (intro directedI) by blast

lemma directed_extend:
  assumes X: "directed X (⊑)" and Y: "directed Y (⊑)" and XY: "∀x∈X. ∀y∈Y. x ⊑ y"
  shows "directed (X ∪ Y) (⊑)"
proof -
  { fix x y
    assume xX: "x ∈ X" and yY: "y ∈ Y"
    let ?g = "∃z∈X ∪ Y. x ⊑ z ∧ y ⊑ z"
    from directedD[OF Y yY yY] obtain z where zY: "z ∈ Y" and yz: "y ⊑ z" by auto
    from xX XY zY yz have ?g by auto
  }
  then show ?thesis by (auto intro!: directed_union[OF X Y])
qed

end

sublocale connex ⊆ directed
proof
  fix x y
  assume x: "x ∈ A" and y: "y ∈ A"
  then show "∃z∈A. x ⊑ z ∧ y ⊑ z"
  proof (cases rule: comparable_cases)
    case le
    with refl[OF y] y show ?thesis by (intro bexI[of _ y], auto)
  next
    case ge
    with refl[OF x] x show ?thesis by (intro bexI[of _ x], auto)
  qed
qed

lemmas(in connex) directed = directed_axioms

lemma monotone_directed_image:
  fixes ir (infix ‹≼› 50) and r (infix ‹⊑› 50)
  assumes mono: "monotone_on I (≼) (⊑) f" and dir: "directed I (≼)"
  shows "directed (f ` I) (⊑)"
proof (rule directedI, safe)
  fix x y assume x: "x ∈ I" and y: "y ∈ I"
  with dir obtain z where z: "z ∈ I" and "x ≼ z" and "y ≼ z" by (auto elim: directedE)
  with mono x y have "f x ⊑ f z" and "f y ⊑ f z" by (auto dest: monotone_onD)
  with z show "∃fz ∈ f ` I. f x ⊑ fz ∧ f y ⊑ fz" by auto
qed


definition "directed_set A (⊑) ≡ ∀X ⊆ A. finite X ⟶ (∃b ∈ A. bound X (⊑) b)"
  for less_eq (infix ‹⊑› 50)

lemmas directed_setI = directed_set_def[unfolded atomize_eq, THEN iffD2, rule_format]
lemmas directed_setD = directed_set_def[unfolded atomize_eq, THEN iffD1, rule_format]

lemma directed_imp_nonempty:
  fixes less_eq (infix ‹⊑› 50)
  shows "directed_set A (⊑) ⟹ A ≠ {}"
  by (auto simp: directed_set_def)

lemma directedD2:
  fixes less_eq (infix ‹⊑› 50)
  assumes dir: "directed_set A (⊑)" and xA: "x ∈ A" and yA: "y ∈ A"
  shows "∃z ∈ A. x ⊑ z ∧ y ⊑ z"
  using directed_setD[OF dir, of "{x,y}"] xA yA by auto

lemma monotone_directed_set_image:
  fixes ir (infix ‹≼› 50) and r (infix ‹⊑› 50)
  assumes mono: "monotone_on I (≼) (⊑) f" and dir: "directed_set I (≼)"
  shows "directed_set (f ` I) (⊑)"
proof (rule directed_setI)
  fix X assume "finite X" and "X ⊆ f ` I"
  from finite_subset_image[OF this]
  obtain J where JI: "J ⊆ I" and Jfin: "finite J" and X: "X = f ` J" by auto
  from directed_setD[OF dir JI Jfin]
  obtain b where bI: "b ∈ I" and Jb: "bound J (≼) b" by auto
  from monotone_image_bound[OF mono JI bI Jb] bI
  show "Bex (f ` I) (bound X (⊑))" by (auto simp: X)
qed


lemma directed_set_iff_extremed:
  fixes less_eq (infix ‹⊑› 50)
  assumes Dfin: "finite D"
  shows "directed_set D (⊑) ⟷ extremed D (⊑)"
proof (intro iffI directed_setI conjI)
  assume "directed_set D (⊑)"
  from directed_setD[OF this order.refl Dfin]
  show "extremed D (⊑)" by (auto intro: extremedI)
next
  fix X assume XD: "X ⊆ D" and Xfin: "finite X"
  assume "extremed D (⊑)"
  then obtain b where "b ∈ D" and "extreme D (⊑) b" by (auto elim!: extremedE)
  with XD show "∃b ∈ D. bound X (⊑) b" by auto
qed

lemma (in transitive) directed_iff_nonempty_pair_bounded:
  "directed_set A (⊑) ⟷ A ≠ {} ∧ (∀x∈A. ∀y∈A. ∃z∈A. x ⊑ z ∧ y ⊑ z)"
  (is "?l ⟷ _ ∧ ?r")
proof (safe intro!: directed_setI del: notI subset_antisym)
  assume dir: ?l
  from directed_imp_nonempty[OF dir] show "A ≠ {}".
  fix x y assume "x ∈ A" "y ∈ A"
  with directed_setD[OF dir, of "{x,y}"]
  show "∃z∈A. x ⊑ z ∧ y ⊑ z" by auto
next
  fix X
  assume A0: "A ≠ {}" and r: ?r
  assume "finite X" and "X ⊆ A"
  then show "Bex A (bound X (⊑))"
  proof (induct)
    case empty
    with A0 show ?case by (auto simp: bound_empty ex_in_conv)
  next
    case (insert x X)
    then obtain y where xA: "x ∈ A" and XA: "X ⊆ A" and yA: "y ∈ A" and Xy: "bound X (⊑) y" by auto
    from r yA xA obtain z where zA: "z ∈ A" and xz: "x ⊑ z" and yz: "y ⊑ z" by auto
    from bound_trans[OF Xy yz XA yA zA] xz zA
    show ?case by auto
  qed
qed

lemma (in transitive) directed_set_iff_nonempty_directed:
  "directed_set A (⊑) ⟷ A ≠ {} ∧ directed A (⊑)"
  apply (unfold directed_iff_nonempty_pair_bounded)
  by (auto simp: directed_def)

lemma (in well_related_set) finite_sets_extremed:
  assumes fin: "finite X" and X0: "X ≠ {}" and XA: "X ⊆ A"
  shows "extremed X (⊑)"
proof-
  interpret less_eq_asymmetrize.
  from fin X0 XA show ?thesis
  proof (induct "card X" arbitrary: X)
    case 0
    then show ?case by auto
  next
    case (Suc n)
    note XA = ‹X ⊆ A› and X0 = ‹X ≠ {}› and Sn = ‹Suc n = card X› and finX = ‹finite X›
    note IH = Suc(1)
    from nonempty_imp_ex_extreme[OF XA X0]
    obtain l where l: "extreme X (⊒) l" by auto
    from l have lX: "l ∈ X" by auto
    with XA have lA: "l ∈ A" by auto
    from Sn lX have n: "n = card (X-{l})" by auto
    show ?case
    proof (cases "X - {l} = {}")
      case True
      with lA lX show ?thesis by (auto intro!: extremedI)
    next
      case False
      from IH[OF n _ this] finX XA
      obtain e where e: "extreme (X - {l}) (⊑) e" by (auto elim!: extremedE)
      with l show ?thesis by (auto intro!: extremedI[of _ _ e] extremeI)
    qed
  qed
qed

lemma (in well_related_set) directed_set:
  assumes A0: "A ≠ {}" shows "directed_set A (⊑)"
proof (intro directed_setI)
  fix X assume XA: "X ⊆ A" and Xfin: "finite X"
  show "Bex A (bound X (⊑))"
  proof (cases "X = {}")
    case True
    with A0 show ?thesis by (auto simp: bound_empty ex_in_conv)
  next
    case False
    from finite_sets_extremed[OF Xfin this] XA
    show ?thesis by (auto elim!: extremedE)
  qed
qed

lemma prod_directed:
  fixes leA (infix ‹⊑⇩A› 50) and leB (infix ‹⊑⇩B› 50)
  assumes dir: "directed X (rel_prod (⊑⇩A) (⊑⇩B))"
  shows "directed (fst ` X) (⊑⇩A)" and "directed (snd ` X) (⊑⇩B)"
proof (safe intro!: directedI)
  fix a b x y assume "(a,x) ∈ X" and "(b,y) ∈ X"
  from directedD[OF dir this]
  obtain c z where cz: "(c,z) ∈ X" and ac: "a ⊑⇩A c" and bc: "b ⊑⇩A c" and "x ⊑⇩B z" and "y ⊑⇩B z" by auto
  then show "∃z∈fst ` X. fst (a,x) ⊑⇩A z ∧ fst (b,y) ⊑⇩A z"
    and "∃z∈snd ` X. snd (a,x) ⊑⇩B z ∧ snd (b,y) ⊑⇩B z"
    by (auto intro!: bexI[OF _ cz])
qed

class dir = ord + assumes "directed UNIV (≤)"
begin

sublocale order: directed UNIV "(≤)"
  rewrites "⋀x. x ∈ UNIV ≡ True"
    and "⋀X. X ⊆ UNIV ≡ True"
    and "⋀r. r ↾ UNIV ≡ r"
    and "⋀P. True ∧ P ≡ P"
    and "Ball UNIV ≡ All"
    and "Bex UNIV ≡ Ex"
    and "sympartp (≤)⇧- ≡ sympartp (≤)"
    and "⋀P1. (True ⟹ PROP P1) ≡ PROP P1"
    and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
    and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
  using dir_axioms[unfolded class.dir_def]
  by (auto simp: atomize_eq)

end

class filt = ord +
  assumes "directed UNIV (≥)"
begin

sublocale order.dual: directed UNIV "(≥)"
  rewrites "⋀x. x ∈ UNIV ≡ True"
    and "⋀X. X ⊆ UNIV ≡ True"
    and "⋀r. r ↾ UNIV ≡ r"
    and "⋀P. True ∧ P ≡ P"
    and "Ball UNIV ≡ All"
    and "Bex UNIV ≡ Ex"
    and "sympartp (≤)⇧- ≡ sympartp (≤)"
    and "⋀P1. (True ⟹ PROP P1) ≡ PROP P1"
    and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
    and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
  using filt_axioms[unfolded class.filt_def]
  by (auto simp: atomize_eq)

end

subclass (in linqorder) dir..

subclass (in linqorder) filt..

thm order.directed_axioms[where 'a = "'a ::dir"]

thm order.dual.directed_axioms[where 'a = "'a ::filt"]

end