# Theory Complete_Partial_Order

Up to index of Isabelle/HOL-Proofs

theory Complete_Partial_Order
imports Product_Type
(* 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))"

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

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 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]
fix x assume "x ∈ iterates f"
thus "P x"
by (induct rule: iterates.induct)
qed

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

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

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

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

fixes P Q :: "'a => bool"
assumes P: "admissible (λx. P x)"
assumes Q: "admissible (λx. Q x)"
shows "admissible (λx. P x ∨ Q x)"
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