# Theory 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 {}"

lemma chain_equality: "chain (=) A ⟷ (∀x∈A. ∀y∈A. x = y)"

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))"

assumes "⋀A. chain ord A ⟹ A ≠ {} ⟹ ∀x∈A. P x ⟹ P (lub A)"
using assms unfolding ccpo.admissible_def by fast

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 mono: "monotone (≤) (≤) f"
assumes bot: "P (Sup {})"
assumes step: "⋀x. P x ⟹ P (f x)"
shows "P (fixp f)"
unfolding fixp_def
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

*)

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

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

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

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)"
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
```