Theory Complete_Partial_Order

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

header {* Chain-complete partial orders and their fixpoints *}

theory Complete_Partial_Order
imports Product_Type
begin

subsection {* Monotone functions *}

text {* Dictionary-passing version of @{const Orderings.mono}. *}

definition monotone :: "('a => 'a => bool) => ('b => 'b => bool) => ('a => 'b) => bool"
where "monotone orda ordb f <-> (∀x y. orda x y --> ordb (f x) (f y))"

lemma monotoneI[intro?]: "(!!x y. orda x y ==> ordb (f x) (f y))
 ==> monotone orda ordb f"
unfolding monotone_def by iprover

lemma monotoneD[dest?]: "monotone orda ordb f ==> orda x y ==> ordb (f x) (f y)"
unfolding monotone_def by iprover


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

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 (op ≤) A; x ∈ A|] ==> x ≤ Sup A"
  assumes ccpo_Sup_least: "[|chain (op ≤) A; !!x. x ∈ A ==> x ≤ z|] ==> Sup A ≤ z"
begin

subsection {* Transfinite iteration of a function *}

inductive_set iterates :: "('a => 'a) => 'a set"
for f :: "'a => 'a"
where
  step: "x ∈ iterates f ==> f x ∈ iterates f"
| Sup: "chain (op ≤) M ==> ∀x∈M. x ∈ iterates f ==> Sup M ∈ iterates f"

lemma iterates_le_f:
  "x ∈ iterates f ==> monotone (op ≤) (op ≤) 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 (op ≤) (op ≤) f"
  shows "chain (op ≤) (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 (op ≤) 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"
          apply rule
          apply (erule order_trans)
          by (rule ccpo_Sup_upper[OF chM])
        thus ?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"
        apply rule
        apply (erule order_trans)
        by (rule ccpo_Sup_upper[OF Sup(1)])
      thus ?thesis ..
    next
      case False with Sup
      show ?thesis by (auto intro: ccpo_Sup_least)
    qed
  qed
qed

subsection {* Fixpoint combinator *}

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

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

lemma fixp_unfold:
  assumes f: "monotone (op ≤) (op ≤) f"
  shows "fixp f = f (fixp f)"
proof (rule 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)
  thus "f (fixp f) ≤ fixp f"
    unfolding fixp_def .
qed

lemma fixp_lowerbound:
  assumes f: "monotone (op ≤) (op ≤) 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"
  thus "x ≤ z"
  proof (induct x rule: iterates.induct)
    fix x assume "x ≤ z" with f have "f x ≤ f z" by (rule monotoneD)
    also note z finally show "f x ≤ z" .
  qed (auto intro: ccpo_Sup_least)
qed


subsection {* Fixpoint induction *}

definition
  admissible :: "('a => bool) => bool"
where
  "admissible P = (∀A. chain (op ≤) A --> (∀x∈A. P x) --> P (Sup A))"

lemma admissibleI:
  assumes "!!A. chain (op ≤) A ==> ∀x∈A. P x ==> P (Sup A)"
  shows "admissible P"
using assms unfolding admissible_def by fast

lemma admissibleD:
  assumes "admissible P"
  assumes "chain (op ≤) A"
  assumes "!!x. x ∈ A ==> P x"
  shows "P (Sup A)"
using assms by (auto simp: admissible_def)

lemma fixp_induct:
  assumes adm: "admissible P"
  assumes mono: "monotone (op ≤) (op ≤) f"
  assumes step: "!!x. P x ==> P (f x)"
  shows "P (fixp f)"
unfolding fixp_def using adm chain_iterates[OF mono]
proof (rule admissibleD)
  fix x assume "x ∈ iterates f"
  thus "P x"
    by (induct rule: iterates.induct)
      (auto intro: step admissibleD adm)
qed

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

lemma admissible_False: "¬ admissible (λx. False)"
unfolding admissible_def chain_def by simp

lemma admissible_const: "admissible (λx. t) = t"
by (cases t, simp_all add: admissible_True admissible_False)

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

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

lemma admissible_ball:
  assumes "!!y. y ∈ A ==> admissible (λx. P x y)"
  shows "admissible (λx. ∀y∈A. P x y)"
using assms unfolding admissible_def by fast

lemma chain_compr: "chain (op ≤) A ==> chain (op ≤) {x ∈ A. P x}"
unfolding chain_def by fast

lemma admissible_disj_lemma:
  assumes A: "chain (op ≤)A"
  assumes P: "∀x∈A. ∃y∈A. x ≤ y ∧ P y"
  shows "Sup A = Sup {x ∈ A. P x}"
proof (rule antisym)
  have *: "chain (op ≤) {x ∈ A. P x}"
    by (rule chain_compr [OF A])
  show "Sup A ≤ Sup {x ∈ A. P x}"
    apply (rule ccpo_Sup_least [OF A])
    apply (drule P [rule_format], clarify)
    apply (erule order_trans)
    apply (simp add: ccpo_Sup_upper [OF *])
    done
  show "Sup {x ∈ A. P x} ≤ Sup A"
    apply (rule ccpo_Sup_least [OF *])
    apply clarify
    apply (simp add: ccpo_Sup_upper [OF A])
    done
qed

lemma admissible_disj:
  fixes P Q :: "'a => bool"
  assumes P: "admissible (λx. P x)"
  assumes Q: "admissible (λx. Q x)"
  shows "admissible (λx. P x ∨ Q x)"
proof (rule admissibleI)
  fix A :: "'a set" assume A: "chain (op ≤) A"
  assume "∀x∈A. P x ∨ Q x"
  hence "(∀x∈A. ∃y∈A. x ≤ y ∧ P y) ∨ (∀x∈A. ∃y∈A. x ≤ y ∧ Q y)"
    using chainD[OF A] by blast
  hence "Sup A = Sup {x ∈ A. P x} ∨ Sup A = Sup {x ∈ A. Q x}"
    using admissible_disj_lemma [OF A] by fast
  thus "P (Sup A) ∨ Q (Sup A)"
    apply (rule disjE, simp_all)
    apply (rule disjI1, rule admissibleD [OF P chain_compr [OF A]], simp)
    apply (rule disjI2, rule admissibleD [OF Q chain_compr [OF A]], simp)
    done
qed

end

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

lemma lfp_eq_fixp:
  assumes f: "mono f" shows "lfp f = fixp f"
proof (rule antisym)
  from f have f': "monotone (op ≤) (op ≤) 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'], subst lfp_unfold [OF f], rule order_refl)
qed

hide_const (open) iterates fixp admissible

end