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 ⟷ (∀x∈S. ∀y∈S. 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 ⟷ (∀x∈A. ∀y∈A. 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 ⟹ ∀x∈M. 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 "∃z∈M. 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 "∃x∈M. 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 ≠ {} ⟶ (∀x∈A. P x) ⟶ P (lub A))"

lemma admissibleI:
  assumes "⋀A. chain ord A ⟹ A ≠ {} ⟹ ∀x∈A. 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. ∀y∈A. 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: "∀x∈A. P x ∨ Q x"
  have "(∃x∈A. P x) ∧ (∀x∈A. ∃y∈A. x ≤ y ∧ P y) ∨ (∃x∈A. Q x) ∧ (∀x∈A. ∃y∈A. x ≤ y ∧ Q y)"
    (is "?P ∨ ?Q" is "?P1 ∧ ?P2 ∨ _")
  proof (rule disjCI)
    assume "¬ ?Q"
    then consider "∀x∈A. ¬ Q x" | a where "a ∈ A" "∀y∈A. a ≤ y ⟶ ¬ Q y"
      by blast
    then show ?P
    proof cases
      case 1
      with P_Q have "∀x∈A. 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 *: "∀y∈A. 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 "∃y∈A. 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. x∈A ⟹ ∃y∈A. 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