Theory HOL.Complete_Partial_Order

(*  Title:      HOL/Complete_Partial_Order.thy
    Author:     Brian Huffman, Portland State University
    Author:     Alexander Krauss, TU Muenchen
*)

section ‹Chain-complete partial orders and their fixpoints›

theory Complete_Partial_Order
  imports Product_Type
begin


subsection ‹Chains›

text ‹
  A chain is a totally-ordered set. Chains are parameterized over
  the order for maximal flexibility, since type classes are not enough.
›

definition chain :: "('a  'a  bool)  'a set  bool"
  where "chain ord S  (xS. yS. ord x y  ord y x)"

lemma chainI:
  assumes "x y. x  S  y  S  ord x y  ord y x"
  shows "chain ord S"
  using assms unfolding chain_def by fast

lemma chainD:
  assumes "chain ord S" and "x  S" and "y  S"
  shows "ord x y  ord y x"
  using assms unfolding chain_def by fast

lemma chainE:
  assumes "chain ord S" and "x  S" and "y  S"
  obtains "ord x y" | "ord y x"
  using assms unfolding chain_def by fast

lemma chain_empty: "chain ord {}"
  by (simp add: chain_def)

lemma chain_equality: "chain (=) A  (xA. yA. x = y)"
  by (auto simp add: chain_def)

lemma chain_subset: "chain ord A  B  A  chain ord B"
  by (rule chainI) (blast dest: chainD)

lemma chain_imageI:
  assumes chain: "chain le_a Y"
    and mono: "x y. x  Y  y  Y  le_a x y  le_b (f x) (f y)"
  shows "chain le_b (f ` Y)"
  by (blast intro: chainI dest: chainD[OF chain] mono)


subsection ‹Chain-complete partial orders›

text ‹
  A ccpo› has a least upper bound for any chain.  In particular, the
  empty set is a chain, so every ccpo› must have a bottom element.
›

class ccpo = order + Sup +
  assumes ccpo_Sup_upper: "chain (≤) A  x  A  x  Sup A"
  assumes ccpo_Sup_least: "chain (≤) A  (x. x  A  x  z)  Sup A  z"
begin

lemma chain_singleton: "Complete_Partial_Order.chain (≤) {x}"
  by (rule chainI) simp

lemma ccpo_Sup_singleton [simp]: "{x} = x"
  by (rule order.antisym) (auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)


subsection ‹Transfinite iteration of a function›

context notes [[inductive_internals]]
begin

inductive_set iterates :: "('a  'a)  'a set"
  for f :: "'a  'a"
  where
    step: "x  iterates f  f x  iterates f"
  | Sup: "chain (≤) M  xM. x  iterates f  Sup M  iterates f"

end

lemma iterates_le_f: "x  iterates f  monotone (≤) (≤) f  x  f x"
  by (induct x rule: iterates.induct)
    (force dest: monotoneD intro!: ccpo_Sup_upper ccpo_Sup_least)+

lemma chain_iterates:
  assumes f: "monotone (≤) (≤) f"
  shows "chain (≤) (iterates f)" (is "chain _ ?C")
proof (rule chainI)
  fix x y
  assume "x  ?C" "y  ?C"
  then show "x  y  y  x"
  proof (induct x arbitrary: y rule: iterates.induct)
    fix x y
    assume y: "y  ?C"
      and IH: "z. z  ?C  x  z  z  x"
    from y show "f x  y  y  f x"
    proof (induct y rule: iterates.induct)
      case (step y)
      with IH f show ?case by (auto dest: monotoneD)
    next
      case (Sup M)
      then have chM: "chain (≤) M"
        and IH': "z. z  M  f x  z  z  f x" by auto
      show "f x  Sup M  Sup M  f x"
      proof (cases "zM. f x  z")
        case True
        then have "f x  Sup M"
          by (blast intro: ccpo_Sup_upper[OF chM] order_trans)
        then show ?thesis ..
      next
        case False
        with IH' show ?thesis
          by (auto intro: ccpo_Sup_least[OF chM])
      qed
    qed
  next
    case (Sup M y)
    show ?case
    proof (cases "xM. y  x")
      case True
      then have "y  Sup M"
        by (blast intro: ccpo_Sup_upper[OF Sup(1)] order_trans)
      then show ?thesis ..
    next
      case False with Sup
      show ?thesis by (auto intro: ccpo_Sup_least)
    qed
  qed
qed

lemma bot_in_iterates: "Sup {}  iterates f"
  by (auto intro: iterates.Sup simp add: chain_empty)


subsection ‹Fixpoint combinator›

definition fixp :: "('a  'a)  'a"
  where "fixp f = Sup (iterates f)"

lemma iterates_fixp:
  assumes f: "monotone (≤) (≤) f"
  shows "fixp f  iterates f"
  unfolding fixp_def
  by (simp add: iterates.Sup chain_iterates f)

lemma fixp_unfold:
  assumes f: "monotone (≤) (≤) f"
  shows "fixp f = f (fixp f)"
proof (rule order.antisym)
  show "fixp f  f (fixp f)"
    by (intro iterates_le_f iterates_fixp f)
  have "f (fixp f)  Sup (iterates f)"
    by (intro ccpo_Sup_upper chain_iterates f iterates.step iterates_fixp)
  then show "f (fixp f)  fixp f"
    by (simp only: fixp_def)
qed

lemma fixp_lowerbound:
  assumes f: "monotone (≤) (≤) f"
    and z: "f z  z"
  shows "fixp f  z"
  unfolding fixp_def
proof (rule ccpo_Sup_least[OF chain_iterates[OF f]])
  fix x
  assume "x  iterates f"
  then show "x  z"
  proof (induct x rule: iterates.induct)
    case (step x)
    from f x  z have "f x  f z" by (rule monotoneD)
    also note z
    finally show "f x  z" .
  next
    case (Sup M)
    then show ?case
      by (auto intro: ccpo_Sup_least)
  qed
qed

end


subsection ‹Fixpoint induction›

setup Sign.map_naming (Name_Space.mandatory_path "ccpo")

definition admissible :: "('a set  'a)  ('a  'a  bool)  ('a  bool)  bool"
  where "admissible lub ord P  (A. chain ord A  A  {}  (xA. P x)  P (lub A))"

lemma admissibleI:
  assumes "A. chain ord A  A  {}  xA. P x  P (lub A)"
  shows "ccpo.admissible lub ord P"
  using assms unfolding ccpo.admissible_def by fast

lemma admissibleD:
  assumes "ccpo.admissible lub ord P"
  assumes "chain ord A"
  assumes "A  {}"
  assumes "x. x  A  P x"
  shows "P (lub A)"
  using assms by (auto simp: ccpo.admissible_def)

setup Sign.map_naming Name_Space.parent_path

lemma (in ccpo) fixp_induct:
  assumes adm: "ccpo.admissible Sup (≤) P"
  assumes mono: "monotone (≤) (≤) f"
  assumes bot: "P (Sup {})"
  assumes step: "x. P x  P (f x)"
  shows "P (fixp f)"
  unfolding fixp_def
  using adm chain_iterates[OF mono]
proof (rule ccpo.admissibleD)
  show "iterates f  {}"
    using bot_in_iterates by auto
next
  fix x
  assume "x  iterates f"
  then show "P x"
  proof (induct rule: iterates.induct)
    case prems: (step x)
    from this(2) show ?case by (rule step)
  next
    case (Sup M)
    then show ?case by (cases "M = {}") (auto intro: step bot ccpo.admissibleD adm)
  qed
qed

lemma admissible_True: "ccpo.admissible lub ord (λx. True)"
  unfolding ccpo.admissible_def by simp

(*lemma admissible_False: "¬ ccpo.admissible lub ord (λx. False)"
unfolding ccpo.admissible_def chain_def by simp
*)
lemma admissible_const: "ccpo.admissible lub ord (λx. t)"
  by (auto intro: ccpo.admissibleI)

lemma admissible_conj:
  assumes "ccpo.admissible lub ord (λx. P x)"
  assumes "ccpo.admissible lub ord (λx. Q x)"
  shows "ccpo.admissible lub ord (λx. P x  Q x)"
  using assms unfolding ccpo.admissible_def by simp

lemma admissible_all:
  assumes "y. ccpo.admissible lub ord (λx. P x y)"
  shows "ccpo.admissible lub ord (λx. y. P x y)"
  using assms unfolding ccpo.admissible_def by fast

lemma admissible_ball:
  assumes "y. y  A  ccpo.admissible lub ord (λx. P x y)"
  shows "ccpo.admissible lub ord (λx. yA. P x y)"
  using assms unfolding ccpo.admissible_def by fast

lemma chain_compr: "chain ord A  chain ord {x  A. P x}"
  unfolding chain_def by fast

context ccpo
begin

lemma admissible_disj:
  fixes P Q :: "'a  bool"
  assumes P: "ccpo.admissible Sup (≤) (λx. P x)"
  assumes Q: "ccpo.admissible Sup (≤) (λx. Q x)"
  shows "ccpo.admissible Sup (≤) (λx. P x  Q x)"
proof (rule ccpo.admissibleI)
  fix A :: "'a set"
  assume chain: "chain (≤) A"
  assume A: "A  {}" and P_Q: "xA. P x  Q x"
  have "(xA. P x)  (xA. yA. x  y  P y)  (xA. Q x)  (xA. yA. x  y  Q y)"
    (is "?P  ?Q" is "?P1  ?P2  _")
  proof (rule disjCI)
    assume "¬ ?Q"
    then consider "xA. ¬ Q x" | a where "a  A" "yA. a  y  ¬ Q y"
      by blast
    then show ?P
    proof cases
      case 1
      with P_Q have "xA. P x" by blast
      with A show ?P by blast
    next
      case 2
      note a = a  A
      show ?P
      proof
        from P_Q 2 have *: "yA. a  y  P y" by blast
        with a have "P a" by blast
        with a show ?P1 by blast
        show ?P2
        proof
          fix x
          assume x: "x  A"
          with chain a show "yA. x  y  P y"
          proof (rule chainE)
            assume le: "a  x"
            with * a x have "P x" by blast
            with x le show ?thesis by blast
          next
            assume "a  x"
            with a P a show ?thesis by blast
          qed
        qed
      qed
    qed
  qed
  moreover
  have "Sup A = Sup {x  A. P x}" if "x. xA  yA. x  y  P y" for P
  proof (rule order.antisym)
    have chain_P: "chain (≤) {x  A. P x}"
      by (rule chain_compr [OF chain])
    show "Sup A  Sup {x  A. P x}"
    proof (rule ccpo_Sup_least [OF chain])
      show "x. x  A  x   {x  A. P x}"
          by (blast intro: ccpo_Sup_upper[OF chain_P] order_trans dest: that)
      qed
    show "Sup {x  A. P x}  Sup A"
      apply (rule ccpo_Sup_least [OF chain_P])
      apply (simp add: ccpo_Sup_upper [OF chain])
      done
  qed
  ultimately
  consider "x. x  A  P x" "Sup A = Sup {x  A. P x}"
    | "x. x  A  Q x" "Sup A = Sup {x  A. Q x}"
    by blast
  then show "P (Sup A)  Q (Sup A)"
  proof cases
    case 1
    then show ?thesis
      using ccpo.admissibleD [OF P chain_compr [OF chain]] by force
  next
    case 2
    then show ?thesis 
      using ccpo.admissibleD [OF Q chain_compr [OF chain]] by force
  qed
qed

end

instance complete_lattice  ccpo
  by standard (fast intro: Sup_upper Sup_least)+

lemma lfp_eq_fixp:
  assumes mono: "mono f"
  shows "lfp f = fixp f"
proof (rule order.antisym)
  from mono have f': "monotone (≤) (≤) f"
    unfolding mono_def monotone_def .
  show "lfp f  fixp f"
    by (rule lfp_lowerbound, subst fixp_unfold [OF f'], rule order_refl)
  show "fixp f  lfp f"
    by (rule fixp_lowerbound [OF f']) (simp add: lfp_fixpoint [OF mono])
qed

hide_const (open) iterates fixp

end