(* 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