# Theory Complete_Partial_Order

Up to index of Isabelle/HOL

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_Orderimports Product_Typebeginsubsection {* 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 iproverlemma monotoneD[dest?]: "monotone orda ordb f ==> orda x y ==> ordb (f x) (f y)"unfolding monotone_def by iproversubsection {* 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 fastlemma chainD:  assumes "chain ord S" and "x ∈ S" and "y ∈ S"  shows "ord x y ∨ ord y x"using assms unfolding chain_def by fastlemma chainE:  assumes "chain ord S" and "x ∈ S" and "y ∈ S"  obtains "ord x y" | "ord y x"using assms unfolding chain_def by fastsubsection {* 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"beginsubsection {* 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  qedqedsubsection {* 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_defby (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 .qedlemma fixp_lowerbound:  assumes f: "monotone (op ≤) (op ≤) f" and z: "f z ≤ z" shows "fixp f ≤ z"unfolding fixp_defproof (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)qedsubsection {* 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 fastlemma 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)qedlemma admissible_True: "admissible (λx. True)"unfolding admissible_def by simplemma admissible_False: "¬ admissible (λx. False)"unfolding admissible_def chain_def by simplemma 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 simplemma admissible_all:  assumes "!!y. admissible (λx. P x y)"  shows "admissible (λx. ∀y. P x y)"using assms unfolding admissible_def by fastlemma 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 fastlemma chain_compr: "chain (op ≤) A ==> chain (op ≤) {x ∈ A. P x}"unfolding chain_def by fastlemma 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])    doneqedlemma 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)    doneqedendinstance 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)qedhide_const (open) iterates fixp admissibleend`