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: "xX. yY. 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: "xX. yY. x  y"
  shows "directed (X  Y) (⊑)"
proof -
  { fix x y
    assume xX: "x  X" and yY: "y  Y"
    let ?g = "zX  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 "zA. 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  {}  (xA. yA. zA. 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 "zA. 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 "zfst ` X. fst (a,x) A z  fst (b,y) A z"
    and "zsnd ` 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