diff --git a/thys/Complete_Non_Orders/Binary_Relations.thy b/thys/Complete_Non_Orders/Binary_Relations.thy --- a/thys/Complete_Non_Orders/Binary_Relations.thy +++ b/thys/Complete_Non_Orders/Binary_Relations.thy @@ -1,992 +1,2245 @@ (* -Author: Akihisa Yamada (2018-2019) +Author: Akihisa Yamada (2018-2021) License: LGPL (see file COPYING.LESSER) *) section \Binary Relations\ text \We start with basic properties of binary relations.\ theory Binary_Relations -imports Main -(* uses mainly concepts from the theories Complete_Partial_Order, Wellfounded, Partial_Function *) + imports +(* To verify that we don't use the axiom of choice, import + HOL.Complete_Partial_Order HOL.Wellfounded + instead of *) Main begin +lemma conj_imp_eq_imp_imp: "(P \ Q \ PROP R) \ (P \ Q \ PROP R)" + by standard simp_all + +lemma tranclp_trancl: "r\<^sup>+\<^sup>+ = (\x y. (x,y) \ {(a,b). r a b}\<^sup>+)" + by (auto simp: tranclp_trancl_eq[symmetric]) + +lemma tranclp_id[simp]: "transp r \ tranclp r = r" + using trancl_id[of "{(x,y). r x y}", folded transp_trans] by (auto simp:tranclp_trancl) + +lemma transp_tranclp[simp]: "transp (tranclp r)" by (auto simp: tranclp_trancl transp_trans) + +lemma funpow_dom: "f ` A \ A \ (f^^n) ` A \ A" by (induct n, auto) + text \Below we introduce an Isabelle-notation for $\{ \ldots x\ldots \mid x \in X \}$.\ syntax - "_range" :: "'a \ pttrn \ 'a set" ("(1{_ /|./ _})") + "_range" :: "'a \ idts \ 'a set" ("(1{_ /|./ _})") "_image" :: "'a \ pttrn \ 'a set \ 'a set" ("(1{_ /|./ (_/ \ _)})") translations - "{e |. p}" \ "CONST range (\p. e)" + "{e |. p}" \ "{e | p. CONST True}" "{e |. p \ A}" \ "CONST image (\p. e) A" lemma image_constant: assumes "\i. i \ I \ f i = y" shows "f ` I = (if I = {} then {} else {y})" using assms by auto subsection \Various Definitions\ text \Here we introduce various definitions for binary relations. The first one is our abbreviation for the dual of a relation.\ abbreviation(input) dual ("(_\<^sup>-)" [1000] 1000) where "r\<^sup>- x y \ r y x" -lemma conversep_as_dual[simp]: "conversep r = r\<^sup>-" by auto - -text \Monotonicity is already defined in the library.\ -lemma monotone_dual: "monotone r s f \ monotone r\<^sup>- s\<^sup>- f" - by (auto simp: monotone_def) - -lemma monotone_id: "monotone r r id" - by (auto simp: monotone_def) - -text \So is the chain, but it is somehow hidden. We reactivate it.\ -abbreviation "chain \ Complete_Partial_Order.chain" - -context fixes r :: "'a \ 'a \ bool" (infix "\" 50) begin - -text \Here we define the following notions in a standard manner: -(upper) bounds of a set:\ -definition "bound X b \ \x \ X. x \ b" - -lemma boundI[intro!]: "(\x. x \ X \ x \ b) \ bound X b" - and boundE[elim]: "bound X b \ ((\x. x \ X \ x \ b) \ thesis) \ thesis" +lemma conversep_is_dual[simp]: "conversep = dual" by auto + +text \Monotonicity is already defined in the library, but we want one restricted to a domain.\ + +definition "monotone_on X r s f \ \x y. x \ X \ y \ X \ r x y \ s (f x) (f y)" + +lemmas monotone_onI = monotone_on_def[unfolded atomize_eq, THEN iffD2, rule_format] +lemma monotone_onD: "monotone_on X r s f \ r x y \ x \ X \ y \ X \ s (f x) (f y)" + by (auto simp: monotone_on_def) + +lemmas monotone_onE = monotone_on_def[unfolded atomize_eq, THEN iffD1, elim_format, rule_format] + +lemma monotone_on_UNIV[simp]: "monotone_on UNIV = monotone" + by (intro ext, auto simp: monotone_on_def monotone_def) + +lemma monotone_on_dual: "monotone_on X r s f \ monotone_on X r\<^sup>- s\<^sup>- f" + by (auto simp: monotone_on_def) + +lemma monotone_on_id: "monotone_on X r r id" + by (auto simp: monotone_on_def) + +lemma monotone_on_cmono: "A \ B \ monotone_on B \ monotone_on A" + by (intro le_funI, auto simp: monotone_on_def) + +text \Here we define the following notions in a standard manner\ + +text \The symmetric part of a relation:\ + +definition sympartp where "sympartp r x y \ r x y \ r y x" + +lemma sympartpI[intro]: + fixes r (infix "\" 50) + assumes "x \ y" and "y \ x" shows "sympartp (\) x y" + using assms by (auto simp: sympartp_def) + +lemma sympartpE[elim]: + fixes r (infix "\" 50) + assumes "sympartp (\) x y" and "x \ y \ y \ x \ thesis" shows thesis + using assms by (auto simp: sympartp_def) + +lemma sympartp_dual: "sympartp r\<^sup>- = sympartp r" + by (auto intro!:ext simp: sympartp_def) + +lemma sympartp_eq[simp]: "sympartp (=) = (=)" by auto + +lemma reflclp_sympartp[simp]: "(sympartp r)\<^sup>=\<^sup>= = sympartp r\<^sup>=\<^sup>=" by auto + +definition "equivpartp r x y \ x = y \ r x y \ r y x" + +lemma sympartp_reflclp_equivp[simp]: "sympartp r\<^sup>=\<^sup>= = equivpartp r" by (auto intro!:ext simp: equivpartp_def) + +lemma equivpartI[simp]: "equivpartp r x x" + and sympartp_equivpartpI: "sympartp r x y \ equivpartp r x y" + and equivpartpCI[intro]: "(x \ y \ sympartp r x y) \ equivpartp r x y" + by (auto simp:equivpartp_def) + +lemma equivpartpE[elim]: + assumes "equivpartp r x y" + and "x = y \ thesis" + and "r x y \ r y x \ thesis" + shows "thesis" + using assms by (auto simp: equivpartp_def) + +lemma equivpartp_eq[simp]: "equivpartp (=) = (=)" by auto + +lemma sympartp_equivpartp[simp]: "sympartp (equivpartp r) = (equivpartp r)" + and equivpartp_equivpartp[simp]: "equivpartp (equivpartp r) = (equivpartp r)" + and equivpartp_sympartp[simp]: "equivpartp (sympartp r) = (equivpartp r)" + by (auto 0 5 intro!:ext) + +lemma equivpartp_dual: "equivpartp r\<^sup>- = equivpartp r" + by (auto intro!:ext simp: equivpartp_def) + +text \The asymmetric part:\ + +definition "asympartp r x y \ r x y \ \ r y x" + +lemma asympartpE[elim]: + fixes r (infix "\" 50) + shows "asympartp (\) x y \ (x \ y \ \y \ x \ thesis) \ thesis" + by (auto simp: asympartp_def) + +lemmas asympartpI[intro] = asympartp_def[unfolded atomize_eq, THEN iffD2, unfolded conj_imp_eq_imp_imp, rule_format] + +lemma asympartp_eq[simp]: "asympartp (=) = bot" by auto + +lemma asympartp_sympartp [simp]: "asympartp (sympartp r) = bot" + and sympartp_asympartp [simp]: "sympartp (asympartp r) = bot" + by (auto intro!: ext) + +text \Restriction to a set:\ + +definition Restrp (infixl "\" 60) where "(r \ A) a b \ a \ A \ b \ A \ r a b" + +lemmas RestrpI[intro!] = Restrp_def[unfolded atomize_eq, THEN iffD2, unfolded conj_imp_eq_imp_imp] +lemmas RestrpE[elim!] = Restrp_def[unfolded atomize_eq, THEN iffD1, elim_format, unfolded conj_imp_eq_imp_imp] + +lemma Restrp_UNIV[simp]: "r \ UNIV \ r" by (auto simp: atomize_eq) + +lemma Restrp_Restrp[simp]: "r \ A \ B \ r \ A \ B" by (auto simp: atomize_eq Restrp_def) + +lemma sympartp_Restrp[simp]: "sympartp (r \ A) \ sympartp r \ A" + by (auto simp: atomize_eq) + +text \Relational images:\ +definition Imagep (infixr "```" 59) where "r ``` A \ {b. \a \ A. r a b}" + +lemma Imagep_Image: "r ``` A = {(a,b). r a b} `` A" + by (auto simp: Imagep_def) + +lemma in_Imagep: "b \ r ``` A \ (\a \ A. r a b)" by (auto simp: Imagep_def) + +lemma ImagepI: "a \ A \ r a b \ b \ r ``` A" by (auto simp: in_Imagep) + +lemma subset_Imagep: "B \ r ``` A \ (\b\B. \a\A. r a b)" + by (auto simp: Imagep_def) + +text \Bounds of a set:\ +definition "bound X r b \ \x \ X. r x b" + +lemma + fixes r (infix "\" 50) + shows boundI[intro!]: "(\x. x \ X \ x \ b) \ bound X (\) b" + and boundE[elim]: "bound X (\) b \ ((\x. x \ X \ x \ b) \ thesis) \ thesis" by (auto simp: bound_def) -lemma bound_empty: "bound {} = (\x. True)" by auto -lemma bound_insert[simp]: "bound (insert x X) b \ x \ b \ bound X b" by auto - -lemma bound_cmono: assumes "X \ Y" shows "bound Y x \ bound X x" - using assms by auto +lemma bound_empty: "bound {} = (\r x. True)" by auto + +lemma bound_insert[simp]: + fixes r (infix "\" 50) + shows "bound (insert x X) (\) b \ x \ b \ bound X (\) b" by auto text \Extreme (greatest) elements in a set:\ -definition "extreme X e \ e \ X \ (\x \ X. x \ e)" - -lemma extremeI[intro]: "e \ X \ (\x. x \ X \ x \ e) \ extreme X e" - and extremeD: "extreme X e \ e \ X" "extreme X e \ (\x. x \ X \ x \ e)" - and extremeE[elim]: "extreme X e \ (e \ X \ (\x. x \ X \ x \ e) \ thesis) \ thesis" +definition "extreme X r e \ e \ X \ (\x \ X. r x e)" + +lemma + fixes r (infix "\" 50) + shows extremeI[intro]: "e \ X \ (\x. x \ X \ x \ e) \ extreme X (\) e" + and extremeD: "extreme X (\) e \ e \ X" "extreme X (\) e \ (\x. x \ X \ x \ e)" + and extremeE[elim]: "extreme X (\) e \ (e \ X \ (\x. x \ X \ x \ e) \ thesis) \ thesis" by (auto simp: extreme_def) -lemma extreme_UNIV[simp]: "extreme UNIV t \ (\x. x \ t)" by auto - -lemma extremes_equiv: "extreme X b \ extreme X c \ b \ c \ c \ b" by auto - -text \Directed sets:\ -definition "directed X \ \x \ X. \ y \ X. \z \ X. x \ z \ y \ z" - -lemma directedE: - assumes "directed X" and "x \ X" and "y \ X" - and "\z. z \ X \ x \ z \ y \ z \ thesis" - shows "thesis" - using assms by (auto simp: directed_def) - -lemma directedI[intro]: - assumes "\x y. x \ X \ y \ X \ \z \ X. x \ z \ y \ z" - shows "directed X" - using assms by (auto simp: directed_def) - -lemma chain_imp_directed: "chain (\) X \ directed X" - by (intro directedI, auto elim: chainE) - -text \And sets of elements which are self-related:\ -definition "reflexive_on X \ \x \ X. x \ x" - -lemma reflexive_onI[intro]: - assumes "\x. x \ X \ x \ x" shows "reflexive_on X" using assms reflexive_on_def by auto - -lemma reflexive_onE[elim]: - assumes "reflexive_on X" and "(\x. x \ X \ x \ x) \ thesis" shows thesis - using assms reflexive_on_def by auto - -lemma chain_imp_reflexive: "chain (\) X \ reflexive_on X" by (auto elim: chainE) - -end - -context fixes r :: "'a \ 'a \ bool" (infix "\" 50) +lemma + fixes r (infix "\" 50) + shows extreme_UNIV[simp]: "extreme UNIV (\) t \ (\x. x \ t)" by auto + +lemma extremes_equiv: "extreme X r b \ extreme X r c \ sympartp r b c" by blast + +lemma bound_cmono: assumes "X \ Y" shows "bound Y \ bound X" + using assms by auto + +lemma sympartp_sympartp[simp]: "sympartp (sympartp r) = sympartp r" by (auto intro!:ext) + +text \Now suprema and infima are given uniformly as follows. + The definition is restricted to a given set. +\ +context + fixes A :: "'a set" and less_eq :: "'a \ 'a \ bool" (infix "\" 50) begin -text \Now suprema and infima are given uniformly as follows. \ -abbreviation "extreme_bound X \ extreme (\x y. y \ x) {b. bound (\) X b}" +abbreviation "extreme_bound X \ extreme {b \ A. bound X (\) b} (\x y. y \ x)" lemma extreme_boundI[intro]: - assumes "\b. bound (\) X b \ s \ b" and "\x. x \ X \ x \ s" + assumes "\b. bound X (\) b \ b \ A \ s \ b" and "\x. x \ X \ x \ s" and "s \ A" shows "extreme_bound X s" using assms by auto +lemma extreme_bound_bound: "extreme_bound X y \ x \ X \ x \ y" by auto + lemma extreme_bound_mono: assumes XY: "X \ Y" - and bX: "extreme_bound X bX" - and bY: "extreme_bound Y bY" - shows "bX \ bY" + and sX: "extreme_bound X sX" + and sY: "extreme_bound Y sY" + shows "sX \ sY" proof- - have "bound (\) X bY" using XY bY by force - with bX show ?thesis by auto + have "bound X (\) sY" using XY sY by force + with sX sY show ?thesis by (auto 0 4) qed lemma extreme_bound_iff: - shows "extreme_bound X b \ (\c. (\x\X. x \ c) \ b \ c) \ (\x \ X. x \ b)" + shows "extreme_bound X s \ s \ A \ (\c \ A. (\x \ X. x \ c) \ s \ c) \ (\x \ X. x \ s)" by (auto simp: extreme_def) lemma extreme_bound_singleton_refl[simp]: - "extreme_bound {x} x \ x \ x" by auto - -lemma extreme_bound_equiv: "extreme_bound X b \ c \ X \ b \ c \ c \ b" - by auto + "extreme_bound {x} x \ x \ A \ x \ x" by auto lemma extreme_bound_image_const: - "x \ x \ C \ {} \ (\i. i \ C \ f i = x) \ extreme_bound (f ` C) x" + "x \ x \ I \ {} \ (\i. i \ I \ f i = x) \ x \ A \ extreme_bound (f ` I) x" by (auto simp: image_constant) lemma extreme_bound_UN_const: - "x \ x \ C \ {} \ (\i y. i \ C \ P i y \ x = y) \ - extreme_bound (\i\C. {y. P i y}) x" + "x \ x \ I \ {} \ (\i y. i \ I \ P i y \ x = y) \ x \ A \ + extreme_bound (\i\I. {y. P i y}) x" by auto end context - fixes r :: "'a \ 'a \ bool" (infix "\" 50) -begin - -lemma fun_ordI: "(\x. f x \ g x) \ fun_ord (\) f g" - and fun_ordD: "fun_ord (\) f g \ f x \ g x" - by (auto simp: fun_ord_def) - -lemma dual_fun_ord: "(fun_ord (\))\<^sup>- = fun_ord (\)\<^sup>-" by (auto intro!:ext simp: fun_ord_def) - -lemma fun_extreme_bound_iff: - shows "extreme_bound (fun_ord (\)) F e \ (\x. extreme_bound (\) {f x |. f \ F} (e x))" (is "?l \ ?r") -proof(intro iffI allI extreme_boundI fun_ordI) - fix f x - assume ?r - then have e: "extreme_bound (\) {f x |. f \ F} (e x)" by auto - show "f \ F \ f x \ e x" using extremeD(1)[OF e] by auto - assume "bound (fun_ord (\)) F f" - then have "bound (\) {f x |. f \ F} (f x)" by (auto simp: fun_ord_def) - with e show "e x \ f x" by auto -next - fix x y - assume l: ?l - from l have e: "f \ F \ f x \ e x" for f by (auto dest!:extremeD simp: fun_ord_def) - then show "y \ {f x |. f \ F} \ y \ e x" by auto - assume "bound (\) {f x |. f \ F} y" - with extremeD(1)[OF l] have "bound (fun_ord (\)) F (e(x:=y))" by (auto simp: fun_ord_def elim!:boundE) - with l have "fun_ord (\) e (e(x:=y))" by auto - from fun_ordD[OF this, of x] - show "e x \ y" by auto -qed - -context fixes ir :: "'i \ 'i \ bool" (infix "\" 50) - fixes f - assumes mono: "monotone (\) (\) f" -begin - -lemma monotone_chain_image: - assumes chain: "chain (\) C" shows "chain (\) (f ` C)" -proof (rule chainI) - fix x y - assume "x \ f ` C" and "y \ f ` C" - then obtain i j where ij: "i \ C" "j \ C" and [simp]: "x = f i" "y = f j" by auto - from chain ij have "i \ j \ j \ i" by (auto elim: chainE) - with ij mono show "x \ y \ y \ x" by (elim disjE, auto dest: monotoneD) -qed - -lemma monotone_directed_image: - assumes dir: "directed (\) D" shows "directed (\) (f ` D)" -proof (rule directedI, safe) - fix x y assume "x \ D" and "y \ D" - with dir obtain z where z: "z \ D" and "x \ z" and "y \ z" by (auto elim: directedE) - with mono have "f x \ f z" and "f y \ f z" by (auto dest: monotoneD) - with z show "\fz \ f ` D. f x \ fz \ f y \ fz" by auto -qed - -context - fixes e C - assumes e: "extreme (\) C e" + and r :: "'a \ 'a \ bool" (infix "\" 50) + and f and A and e and I + assumes fIA: "f ` I \ A" + and mono: "monotone_on I (\) (\) f" + and e: "extreme I (\) e" begin lemma monotone_extreme_imp_extreme_bound: - shows "extreme_bound (\) (f ` C) (f e)" - using monotoneD[OF mono] e - by (auto simp: image_def intro!:extreme_boundI elim!:extremeE boundE) + "extreme_bound A (\) (f ` I) (f e)" + using monotone_onD[OF mono] e fIA + by (intro extreme_boundI, auto simp: image_def elim!: extremeE) lemma monotone_extreme_extreme_boundI: - "x = f e \ extreme_bound (\) (f ` C) x" + "x = f e \ extreme_bound A (\) (f ` I) x" using monotone_extreme_imp_extreme_bound by auto end -end - -end - subsection \Locales for Binary Relations\ text \We now define basic properties of binary relations, in form of \emph{locales}~\cite{Kammuller00,locale}.\ subsubsection \Syntactic Locales\ text \The following locales do not assume anything, but provide infix notations for -relations. \ - -locale less_eq_syntax = fixes less_eq :: "'a \ 'a \ bool" (infix "\" 50) - -locale less_syntax = fixes less :: "'a \ 'a \ bool" (infix "\" 50) - -locale equivalence_syntax = fixes equiv :: "'a \ 'a \ bool" (infix "\" 50) +relations.\ + +locale less_eq_syntax = + fixes less_eq :: "'a \ 'a \ bool" (infix "\" 50) + +locale less_syntax = + fixes less :: "'a \ 'a \ bool" (infix "\" 50) + +locale equivalence_syntax = + fixes equiv :: "'a \ 'a \ bool" (infix "\" 50) begin abbreviation equiv_class ("[_]\<^sub>\") where "[x]\<^sub>\ \ { y. x \ y }" end text \Next ones introduce abbreviations for dual etc. To avoid needless constants, one should be careful when declaring them as sublocales.\ -locale less_eq_dualize = less_eq_syntax +locale less_eq_notations = less_eq_syntax begin abbreviation (input) greater_eq (infix "\" 50) where "x \ y \ y \ x" -abbreviation (input) equiv (infix "\" 50) where "x \ y \ x \ y \ y \ x" - -lemma equiv_sym[sym]: "x \ y \ y \ x" by auto +abbreviation sym (infix "\" 50) where "(\) \ sympartp (\)" +abbreviation less (infix "\" 50) where "(\) \ asympartp (\)" +abbreviation greater (infix "\" 50) where "(\) \ (\)\<^sup>-" +abbreviation equiv (infix "(\)" 50) where "(\) \ equivpartp (\)" + +lemma asym_cases[consumes 1, case_names asym sym]: + assumes "x \ y" and "x \ y \ thesis" and "x \ y \ thesis" + shows thesis + using assms by auto end -locale less_dualize = less_syntax +locale less_notations = less_syntax begin abbreviation (input) greater (infix "\" 50) where "x \ y \ y \ x" end +locale related_set = + fixes A :: "'a set" and less_eq :: "'a \ 'a \ bool" (infix "\" 50) + subsubsection \Basic Properties of Relations\ text \In the following we define basic properties in form of locales.\ -locale reflexive = less_eq_syntax + assumes refl[iff]: "x \ x" +text \Reflexivity restricted on a set:\ +locale reflexive = related_set + + assumes refl[intro]: "x \ A \ x \ x" begin -lemma eq_implies: "x = y \ x \ y" by auto - -lemma extreme_singleton[simp]: "extreme (\) {x} y \ x = y" by auto - -lemma extreme_bound_singleton[iff]: "extreme_bound (\) {x} x" by auto - -end -lemmas reflexiveI[intro] = reflexive.intro - -locale irreflexive = less_syntax + assumes irrefl[iff]: "\ x \ x" -begin - -lemma implies_not_eq: "x \ y \ x \ y" by auto - -end -lemmas irreflexiveI[intro] = irreflexive.intro - -locale transitive = less_eq_syntax + assumes trans[trans]: "x \ y \ y \ z \ x \ z" -lemmas [intro?] = transitive.intro - -locale symmetric = equivalence_syntax + assumes sym[sym]: "x \ y \ y \ x" -begin - -lemma dual_sym: "(\)\<^sup>- = (\)" using sym by auto +lemma eq_implies: "x = y \ x \ A \ x \ y" by auto + +lemma extreme_singleton[simp]: "x \ A \ extreme {x} (\) y \ x = y" by auto + +lemma extreme_bound_singleton: "x \ A \ extreme_bound A (\) {x} x" by auto + +lemma reflexive_subset: "B \ A \ reflexive B (\)" apply unfold_locales by auto end -lemmas [intro] = symmetric.intro - -locale antisymmetric = less_eq_syntax + assumes antisym[dest]: "x \ y \ y \ x \ x = y" + +declare reflexive.intro[intro!] + +lemma reflexiveE[elim]: + assumes "reflexive A r" and "(\x. x \ A \ r x x) \ thesis" shows thesis + using assms by (auto simp: reflexive.refl) + +lemma reflexive_cong: + "(\a b. a \ A \ b \ A \ r a b \ r' a b) \ reflexive A r \ reflexive A r'" + by (simp add: reflexive_def) + +locale irreflexive = related_set A "(\)" for A and less (infix "\" 50) + + assumes irrefl: "x \ A \ \ x \ x" begin -interpretation less_eq_dualize. - -lemma equiv_iff_eq_refl: "x \ y \ x = y \ y \ y" by auto - -lemma extreme_unique: "extreme (\) X x \ extreme (\) X y \ x = y" - by (auto elim!: extremeE) - -lemma ex_extreme_iff_ex1: "Ex (extreme (\) X) \ Ex1 (extreme (\) X)" by (auto simp: extreme_unique) - -lemma ex_extreme_iff_the: - "Ex (extreme (\) X) \ extreme (\) X (The (extreme (\) X))" - apply (rule iffI) - apply (rule theI') - using extreme_unique by auto +lemma irreflD[simp]: "x \ x \ \x \ A" by (auto simp: irrefl) + +lemma implies_not_eq: "x \ y \ x \ A \ x \ y" by auto + +lemma Restrp_irreflexive: "irreflexive UNIV ((\)\A)" + apply unfold_locales by auto + +lemma irreflexive_subset: "B \ A \ irreflexive B (\)" apply unfold_locales by auto end -lemmas antisymmetricI[intro] = antisymmetric.intro + +declare irreflexive.intro[intro!] + +lemma irreflexive_cong: + "(\a b. a \ A \ b \ A \ r a b \ r' a b) \ irreflexive A r \ irreflexive A r'" + by (simp add: irreflexive_def) + +locale transitive = related_set + + assumes trans[trans]: "x \ y \ y \ z \ x \ A \ y \ A \ z \ A \ x \ z" +begin + +interpretation less_eq_notations. + +lemma Restrp_transitive: "transitive UNIV ((\)\A)" + apply unfold_locales + by (auto intro: trans) + +lemma bound_trans[trans]: "bound X (\) b \ b \ c \ X \ A \ b \ A \ c \ A \ bound X (\) c" + by (auto 0 4 dest: trans) + +lemma transitive_subset: + assumes BA: "B \ A" shows "transitive B (\)" + apply unfold_locales + using trans BA by blast + +lemma asympartp_transitive: "transitive A (\)" + apply unfold_locales by (auto dest:trans) + +lemma reflclp_transitive: "transitive A (\)\<^sup>=\<^sup>=" + apply unfold_locales by (auto dest: trans) + +text \The symmetric part is also transitive, but this is done in the later semiattractive locale\ + +end + +declare transitive.intro[intro?] + +lemma transitive_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" shows "transitive A r \ transitive A r'" +proof (intro iffI) + show "transitive A r \ transitive A r'" + apply (intro transitive.intro) + apply (unfold r[symmetric]) + using transitive.trans. + show "transitive A r' \ transitive A r" + apply (intro transitive.intro) + apply (unfold r) + using transitive.trans. +qed + +lemma tranclp_transitive: "transitive A (tranclp r)" + using tranclp_trans by unfold_locales + +locale symmetric = related_set A "(\)" for A and equiv (infix "\" 50) + + assumes sym[sym]: "x \ y \ x \ A \ y \ A \ y \ x" +begin + +lemma sym_iff: "x \ A \ y \ A \ x \ y \ y \ x" + by (auto dest: sym) + +lemma Restrp_symmetric: "symmetric UNIV ((\)\A)" + apply unfold_locales by (auto simp: sym_iff) + +lemma symmetric_subset: "B \ A \ symmetric B (\)" + apply unfold_locales by (auto dest: sym) + +end + +declare symmetric.intro[intro] + +lemma symmetric_cong: + "(\a b. a \ A \ b \ A \ r a b \ r' a b) \ symmetric A r \ symmetric A r'" + by (auto simp: symmetric_def) + + +global_interpretation sympartp: symmetric UNIV "sympartp r" + rewrites "\r. r \ UNIV \ r" + and "\x. x \ UNIV \ True" + and "\P1. (True \ P1) \ Trueprop P1" + and "\P1 P2. (True \ PROP P1 \ PROP P2) \ (PROP P1 \ PROP P2)" + by auto + +lemma sympartp_symmetric: "symmetric A (sympartp r)" by auto + +locale antisymmetric = related_set + + assumes antisym: "x \ y \ y \ x \ x \ A \ y \ A \ x = y" +begin + +interpretation less_eq_notations. + +lemma sym_iff_eq_refl: "x \ A \ y \ A \ x \ y \ x = y \ y \ y" by (auto dest: antisym) + +lemma equiv_iff_eq[simp]: "x \ A \ y \ A \ x \ y \ x = y" by (auto dest: antisym elim: equivpartpE) + +lemma extreme_unique: "X \ A \ extreme X (\) x \ extreme X (\) y \ x = y" + by (elim extremeE, auto dest!: antisym[OF _ _ subsetD]) + +lemma ex_extreme_iff_ex1: + "X \ A \ Ex (extreme X (\)) \ Ex1 (extreme X (\))" by (auto simp: extreme_unique) + +lemma ex_extreme_iff_the: + "X \ A \ Ex (extreme X (\)) \ extreme X (\) (The (extreme X (\)))" + apply (rule iffI) + apply (rule theI') + using extreme_unique by auto + +lemma Restrp_antisymmetric: "antisymmetric UNIV ((\)\A)" + apply unfold_locales + by (auto dest: antisym) + +lemma antisymmetric_subset: "B \ A \ antisymmetric B (\)" + apply unfold_locales using antisym by auto + +end + +declare antisymmetric.intro[intro] + +lemma antisymmetric_cong: + "(\a b. a \ A \ b \ A \ r a b \ r' a b) \ antisymmetric A r \ antisymmetric A r'" + by (auto simp: antisymmetric_def) + +lemma antisymmetric_union: + fixes less_eq (infix "\" 50) + assumes A: "antisymmetric A (\)" and B: "antisymmetric B (\)" + and AB: "\a \ A. \b \ B. a \ b \ b \ a \ a = b" + shows "antisymmetric (A \ B) (\)" +proof- + interpret A: antisymmetric A "(\)" using A. + interpret B: antisymmetric B "(\)" using B. + show ?thesis by (auto dest: AB[rule_format] A.antisym B.antisym) +qed text \The following notion is new, generalizing antisymmetry and transitivity.\ -locale semiattractive = less_eq_syntax + - assumes attract: "x \ y \ y \ x \ x \ z \ y \ z" +locale semiattractive = related_set + + assumes attract: "x \ y \ y \ x \ y \ z \ x \ A \ y \ A \ z \ A \ x \ z" begin -interpretation less_eq_dualize. - -lemma equiv_trans: - assumes xy: "x \ y" and yz: "y \ z" shows "x \ z" - using attract[of y x z] attract[of y z x] xy yz by auto +interpretation less_eq_notations. + +lemma equiv_order_trans[trans]: + assumes xy: "x \ y" and yz: "y \ z" and x: "x \ A" and y: "y \ A" and z: "z \ A" + shows "x \ z" + using attract[OF _ _ _ x y z] xy yz by (auto elim: equivpartpE) + +lemma equiv_transitive: "transitive A (\)" +proof unfold_locales + fix x y z + assume x: "x \ A" and y: "y \ A" and z: "z \ A" and xy: "x \ y" and yz: "y \ z" + show "x \ z" + using equiv_order_trans[OF xy _ x y z] attract[OF _ _ _ z y x] xy yz by (auto simp:equivpartp_def) +qed + +lemma sym_order_trans[trans]: + assumes xy: "x \ y" and yz: "y \ z" and x: "x \ A" and y: "y \ A" and z: "z \ A" + shows "x \ z" + using attract[OF _ _ _ x y z] xy yz by auto + +interpretation sym: transitive A "(\)" +proof unfold_locales + fix x y z + assume x: "x \ A" and y: "y \ A" and z: "z \ A" and xy: "x \ y" and yz: "y \ z" + show "x \ z" + using sym_order_trans[OF xy _ x y z] attract[OF _ _ _ z y x] xy yz by auto +qed + +lemmas sym_transitive = sym.transitive_axioms lemma extreme_bound_quasi_const: - assumes C: "C \ {}" and const: "\y \ C. y \ x" shows "extreme_bound (\) C x" -proof (intro extreme_boundI) - from C obtain c where c: "c \ C" by auto - with const have cx: "c \ x" by auto - fix b assume "bound (\) C b" - with c have cb: "c \ b" by auto - from attract[of c x b] cb cx show "x \ b" by auto + assumes C: "C \ A" and x: "x \ A" and C0: "C \ {}" and const: "\y \ C. y \ x" + shows "extreme_bound A (\) C x" +proof (intro extreme_boundI x) + from C0 obtain c where cC: "c \ C" by auto + with C have c: "c \ A" by auto + from cC const have cx: "c \ x" by auto + fix b assume b: "b \ A" and "bound C (\) b" + with cC have cb: "c \ b" by auto + from attract[OF _ _ cb x c b] cx show "x \ b" by auto next fix c assume "c \ C" with const show "c \ x" by auto qed lemma extreme_bound_quasi_const_iff: - assumes C: "C \ {}" and const: "\z \ C. z \ x" - shows "extreme_bound (\) C y \ x \ y" + assumes C: "C \ A" and x: "x \ A" and y: "y \ A" and C0: "C \ {}" and const: "\z \ C. z \ x" + shows "extreme_bound A (\) C y \ x \ y" proof (intro iffI) - assume "extreme_bound (\) C y" - with const show "x \ y" - by (metis C extreme_bound_quasi_const extremes_equiv) + assume y: "extreme_bound A (\) C y" + note x = extreme_bound_quasi_const[OF C x C0 const] + from extremes_equiv[OF y x] + show "x \ y" by auto next assume xy: "x \ y" - with const equiv_trans[of _ x y] have Cy: "\z \ C. z \ y" by auto - show "extreme_bound (\) C y" - using extreme_bound_quasi_const[OF C Cy]. + with const C sym.trans[OF _ xy _ x y] have Cy: "\z \ C. z \ y" by auto + show "extreme_bound A (\) C y" + using extreme_bound_quasi_const[OF C y C0 Cy]. +qed + +lemma Restrp_semiattractive: "semiattractive UNIV ((\)\A)" + apply unfold_locales + by (auto dest: attract) + +lemma semiattractive_subset: "B \ A \ semiattractive B (\)" + apply unfold_locales using attract by blast + +end + +lemma semiattractive_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "semiattractive A r \ semiattractive A r'" (is "?l \ ?r") +proof + show "?l \ ?r" + apply (intro semiattractive.intro) + apply (unfold r[symmetric]) + using semiattractive.attract. + show "?r \ ?l" + apply (intro semiattractive.intro) + apply (unfold r) + using semiattractive.attract. +qed + +locale attractive = semiattractive + + assumes "semiattractive A (\)\<^sup>-" +begin + +interpretation less_eq_notations. + +sublocale dual: semiattractive A "(\)\<^sup>-" + rewrites "\r. sympartp (r \ A) \ sympartp r \ A" + and "\r. sympartp (sympartp r) \ sympartp r" + and "sympartp ((\) \ A)\<^sup>- \ (\) \ A" + and "sympartp (\)\<^sup>- \ (\)" + and "equivpartp (\)\<^sup>- \ (\)" + using attractive_axioms[unfolded attractive_def] + by (auto intro!: ext simp: attractive_axioms_def atomize_eq equivpartp_def) + +lemma order_equiv_trans[trans]: + assumes xy: "x \ y" and yz: "y \ z" and x: "x \ A" and y: "y \ A" and z: "z \ A" + shows "x \ z" + using dual.attract[OF _ _ _ z y x] xy yz by auto + +lemma order_sym_trans[trans]: + assumes xy: "x \ y" and yz: "y \ z" and x: "x \ A" and y: "y \ A" and z: "z \ A" + shows "x \ z" + using dual.attract[OF _ _ _ z y x] xy yz by auto + +interpretation Restrp: semiattractive UNIV "(\)\A" using Restrp_semiattractive. +interpretation dual.Restrp: semiattractive UNIV "(\)\<^sup>-\A" using dual.Restrp_semiattractive. + +lemma Restrp_attractive: "attractive UNIV ((\)\A)" + apply unfold_locales + using dual.Restrp.attract by auto + +lemma attractive_subset: "B \ A \ attractive B (\)" + apply (intro attractive.intro attractive_axioms.intro) + using semiattractive_subset dual.semiattractive_subset by auto + +end + +lemma attractive_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "attractive A r \ attractive A r'" + by (simp add: attractive_def attractive_axioms_def r cong: semiattractive_cong) + +context antisymmetric begin + +sublocale attractive + apply unfold_locales by (auto dest: antisym) + +end + +context transitive begin + +sublocale attractive + rewrites "\r. sympartp (r \ A) \ sympartp r \ A" + and "\r. sympartp (sympartp r) \ sympartp r" + and "sympartp (\)\<^sup>- \ sympartp (\)" + and "(sympartp (\))\<^sup>- \ sympartp (\)" + and "(sympartp (\) \ A)\<^sup>- \ sympartp (\) \ A" + and "asympartp (asympartp (\)) = asympartp (\)" + and "asympartp (sympartp (\)) = bot" + and "asympartp (\) \ A = asympartp ((\) \ A)" + apply unfold_locales + by (auto intro!:ext dest: trans simp: atomize_eq) + +end + +subsection \Combined Properties\ + +text \Some combinations of the above basic properties are given names.\ + +locale asymmetric = related_set A "(\)" for A and less (infix "\" 50) + + assumes asym: "x \ y \ y \ x \ x \ A \ y \ A \ False" +begin + +sublocale irreflexive + apply unfold_locales by (auto dest: asym) + +lemma antisymmetric_axioms: "antisymmetric A (\)" + apply unfold_locales by (auto dest: asym) + +lemma Restrp_asymmetric: "asymmetric UNIV ((\)\A)" + apply unfold_locales + by (auto dest:asym) + +lemma asymmetric_subset: "B \ A \ asymmetric B (\)" + apply unfold_locales using asym by auto + +end + +lemma asymmetric_iff_irreflexive_antisymmetric: + fixes less (infix "\" 50) + shows "asymmetric A (\) \ irreflexive A (\) \ antisymmetric A (\)" (is "?l \ ?r") +proof + assume ?l + then interpret asymmetric. + show ?r by (auto dest: asym) +next + assume ?r + then interpret irreflexive + antisymmetric A "(\)" by auto + show ?l by (auto intro!:asymmetric.intro dest: antisym irrefl) +qed + +lemma asymmetric_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "asymmetric A r \ asymmetric A r'" + by (simp add: asymmetric_iff_irreflexive_antisymmetric r cong: irreflexive_cong antisymmetric_cong) + +locale quasi_ordered_set = reflexive + transitive +begin + +lemma quasi_ordered_subset: "B \ A \ quasi_ordered_set B (\)" + apply intro_locales + using reflexive_subset transitive_subset by auto + +end + +lemma quasi_ordered_set_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "quasi_ordered_set A r \ quasi_ordered_set A r'" + by (simp add: quasi_ordered_set_def r cong: reflexive_cong transitive_cong) + +locale near_ordered_set = antisymmetric + transitive +begin + +interpretation Restrp: antisymmetric UNIV "(\)\A" using Restrp_antisymmetric. +interpretation Restrp: transitive UNIV "(\)\A" using Restrp_transitive. + +lemma Restrp_near_order: "near_ordered_set UNIV ((\)\A)".. + +lemma near_ordered_subset: "B \ A \ near_ordered_set B (\)" + apply intro_locales + using antisymmetric_subset transitive_subset by auto + +end + +lemma near_ordered_set_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "near_ordered_set A r \ near_ordered_set A r'" + by (simp add: near_ordered_set_def r cong: antisymmetric_cong transitive_cong) + +locale pseudo_ordered_set = reflexive + antisymmetric +begin + +interpretation less_eq_notations. + +lemma sym_eq[simp]: "x \ A \ y \ A \ x \ y \ x = y" + by (auto simp: refl dest: antisym) + +lemma extreme_bound_singleton_eq[simp]: "x \ A \ extreme_bound A (\) {x} y \ x = y" + by (auto intro!: antisym) + +lemma eq_iff: "x \ A \ y \ A \ x = y \ x \ y \ y \ x" by (auto dest: antisym simp:refl) + +lemma extreme_order_iff_eq: "e \ A \ extreme {x \ A. x \ e} (\) s \ e = s" + by (auto intro!: antisym) + +lemma pseudo_ordered_subset: "B \ A \ pseudo_ordered_set B (\)" + apply intro_locales + using reflexive_subset antisymmetric_subset by auto + +end + +lemma pseudo_ordered_set_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "pseudo_ordered_set A r \ pseudo_ordered_set A r'" + by (simp add: pseudo_ordered_set_def r cong: reflexive_cong antisymmetric_cong) + +locale partially_ordered_set = reflexive + antisymmetric + transitive +begin + +sublocale pseudo_ordered_set + quasi_ordered_set + near_ordered_set .. + +lemma partially_ordered_subset: "B \ A \ partially_ordered_set B (\)" + apply intro_locales + using reflexive_subset transitive_subset antisymmetric_subset by auto + +end + +lemma partially_ordered_set_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "partially_ordered_set A r \ partially_ordered_set A r'" + by (simp add: partially_ordered_set_def r cong: reflexive_cong antisymmetric_cong transitive_cong) + +locale strict_ordered_set = irreflexive + transitive A "(\)" +begin + +sublocale asymmetric +proof + fix x y + assume x: "x \ A" and y: "y \ A" + assume xy: "x \ y" + also assume yx: "y \ x" + finally have "x \ x" using x y by auto + with x show False by auto +qed + +lemma near_ordered_set_axioms: "near_ordered_set A (\)" + using antisymmetric_axioms by intro_locales + +interpretation Restrp: asymmetric UNIV "(\)\A" using Restrp_asymmetric. +interpretation Restrp: transitive UNIV "(\)\A" using Restrp_transitive. + +lemma Restrp_strict_order: "strict_ordered_set UNIV ((\)\A)".. + +lemma strict_ordered_subset: "B \ A \ strict_ordered_set B (\)" + apply intro_locales + using irreflexive_subset transitive_subset by auto + +end + +lemma strict_ordered_set_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "strict_ordered_set A r \ strict_ordered_set A r'" + by (simp add: strict_ordered_set_def r cong: irreflexive_cong transitive_cong) + +locale tolerance = symmetric + reflexive A "(\)" +begin + +lemma tolerance_subset: "B \ A \ tolerance B (\)" + apply intro_locales + using symmetric_subset reflexive_subset by auto + +end + +lemma tolerance_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "tolerance A r \ tolerance A r'" + by (simp add: tolerance_def r cong: reflexive_cong symmetric_cong) + +global_interpretation equiv: tolerance UNIV "equivpartp r" + rewrites "\r. r \ UNIV \ r" + and "\x. x \ UNIV \ True" + and "\P1. (True \ P1) \ Trueprop P1" + and "\P1 P2. (True \ PROP P1 \ PROP P2) \ (PROP P1 \ PROP P2)" + by unfold_locales (auto simp:equivpartp_def) + +locale partial_equivalence = symmetric + + assumes "transitive A (\)" +begin + +sublocale transitive A "(\)" + rewrites "sympartp (\)\A \ (\)\A" + and "sympartp ((\)\A) \ (\)\A" + using partial_equivalence_axioms + unfolding partial_equivalence_axioms_def partial_equivalence_def + by (auto simp: atomize_eq sym intro!:ext) + +lemma partial_equivalence_subset: "B \ A \ partial_equivalence B (\)" + apply (intro partial_equivalence.intro partial_equivalence_axioms.intro) + using symmetric_subset transitive_subset by auto + +end + +lemma partial_equivalence_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "partial_equivalence A r \ partial_equivalence A r'" + by (simp add: partial_equivalence_def partial_equivalence_axioms_def r + cong: transitive_cong symmetric_cong) + +locale equivalence = symmetric + reflexive A "(\)" + transitive A "(\)" +begin + +sublocale tolerance + partial_equivalence + quasi_ordered_set A "(\)".. + +lemma equivalence_subset: "B \ A \ equivalence B (\)" + apply (intro equivalence.intro) + using symmetric_subset transitive_subset by auto + +end + +lemma equivalence_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "equivalence A r \ equivalence A r'" + by (simp add: equivalence_def r cong: reflexive_cong transitive_cong symmetric_cong) + +text \Some combinations lead to uninteresting relations.\ + +context + fixes r :: "'a \ 'a \ bool" (infix "\" 50) +begin + +proposition reflexive_irreflexive_is_empty: + assumes r: "reflexive A (\)" and ir: "irreflexive A (\)" + shows "A = {}" +proof (rule ccontr) + interpret irreflexive A "(\)" using ir. + interpret reflexive A "(\)" using r. + assume "A \ {}" + then obtain a where a: "a \ A" by auto + from a refl have "a \ a" by auto + with irrefl a show False by auto +qed + +proposition symmetric_antisymmetric_imp_eq: + assumes s: "symmetric A (\)" and as: "antisymmetric A (\)" + shows "(\)\A \ (=)" +proof- + interpret symmetric A "(\)" + antisymmetric A "(\)" using assms by auto + show "?thesis" using antisym by (auto dest: sym) +qed + +proposition nontolerance: + shows "irreflexive A (\) \ symmetric A (\) \ tolerance A (\x y. \ x \ y)" +proof (intro iffI conjI, elim conjE) + assume "irreflexive A (\)" and "symmetric A (\)" + then interpret irreflexive A "(\)" + symmetric A "(\)". + show "tolerance A (\x y. \ x \ y)" by (unfold_locales, auto dest: sym irrefl) +next + assume "tolerance A (\x y. \ x \ y)" + then interpret tolerance A "\x y. \ x \ y". + show "irreflexive A (\)" by (auto simp: eq_implies) + show "symmetric A (\)" using sym by auto +qed + +proposition irreflexive_transitive_symmetric_is_empty: + assumes irr: "irreflexive A (\)" and tr: "transitive A (\)" and sym: "symmetric A (\)" + shows "(\)\A = bot" +proof (intro ext, unfold bot_fun_def bot_bool_def eq_False, rule notI, erule RestrpE) + interpret strict_ordered_set A "(\)" using assms by (unfold strict_ordered_set_def, auto) + interpret symmetric A "(\)" using assms by auto + fix x y assume x: "x \ A" and y: "y \ A" + assume xy: "x \ y" + also note sym[OF xy x y] + finally have "x \ x" using x y by auto + with x show False by auto qed end -locale attractive = semiattractive + dual: semiattractive "(\)\<^sup>-" - -sublocale transitive \ attractive by (unfold_locales, auto dest: trans) - -sublocale antisymmetric \ attractive by (unfold_locales, auto) - -locale asymmetric = irreflexive + strict: antisymmetric "(\)" +subsection \Totality\ + +locale semiconnex = related_set A "(\)" for A and less (infix "\" 50) + + assumes semiconnex: "x \ A \ y \ A \ x \ y \ x = y \ y \ x" begin -lemma asym[trans]: "x \ y \ y \ x \ thesis" by auto +lemma cases[consumes 2, case_names less eq greater]: + assumes "x \ A" and "y \ A" and "x \ y \ P" and "x = y \ P" and "y \ x \ P" + shows "P" using semiconnex assms by auto + +lemma neqE: + assumes "x \ A" and "y \ A" + shows "x \ y \ (x \ y \ P) \ (y \ x \ P) \ P" + by (cases rule: cases[OF assms], auto) + +lemma semiconnex_subset: "B \ A \ semiconnex B (\)" + apply (intro semiconnex.intro) + using semiconnex by auto + +end + +declare semiconnex.intro[intro] + +text \Totality is negated antisymmetry \cite[Proposition 2.2.4]{Schmidt1993}.\ +proposition semiconnex_iff_neg_antisymmetric: + fixes less (infix "\" 50) + shows "semiconnex A (\) \ antisymmetric A (\x y. \ x \ y)" (is "?l \ ?r") +proof (intro iffI semiconnex.intro antisymmetric.intro) + assume ?l + then interpret semiconnex. + fix x y + assume "x \ A" "y \ A" "\ x \ y" and "\ y \ x" + then show "x = y" by (cases rule: cases, auto) +next + assume ?r + then interpret neg: antisymmetric A "(\x y. \ x \ y)". + fix x y + show "x \ A \ y \ A \ x \ y \ x = y \ y \ x" using neg.antisym by auto +qed + +lemma semiconnex_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "semiconnex A r \ semiconnex A r'" + by (simp add: semiconnex_iff_neg_antisymmetric r cong: antisymmetric_cong) + +locale semiconnex_irreflexive = semiconnex + irreflexive +begin + +lemma neq_iff: "x \ A \ y \ A \ x \ y \ x \ y \ y \ x" by (auto elim:neqE dest: irrefl) + +lemma semiconnex_irreflexive_subset: "B \ A \ semiconnex_irreflexive B (\)" + apply (intro semiconnex_irreflexive.intro) + using semiconnex_subset irreflexive_subset by auto + +end + +lemma semiconnex_irreflexive_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "semiconnex_irreflexive A r \ semiconnex_irreflexive A r'" + by (simp add: semiconnex_irreflexive_def r cong: semiconnex_cong irreflexive_cong) + +locale connex = related_set + + assumes comparable: "x \ A \ y \ A \ x \ y \ y \ x" +begin + +interpretation less_eq_notations. + +sublocale reflexive apply unfold_locales using comparable by auto + +lemma comparable_cases[consumes 2, case_names le ge]: + assumes "x \ A" and "y \ A" and "x \ y \ P" and "y \ x \ P" shows "P" + using assms comparable by auto + +lemma comparable_three_cases[consumes 2, case_names less eq greater]: + assumes "x \ A" and "y \ A" and "x \ y \ P" and "x \ y \ P" and "y \ x \ P" shows "P" + using assms comparable by auto + +lemma + assumes x: "x \ A" and y: "y \ A" + shows not_iff_asym: "\x \ y \ y \ x" + and not_asym_iff[simp]: "\x \ y \ y \ x" + using comparable[OF x y] by auto + +lemma connex_subset: "B \ A \ connex B (\)" + by (intro connex.intro comparable, auto) + +end + +lemmas connexE = connex.comparable_cases + +lemmas connexI[intro] = connex.intro + +context + fixes less_eq :: "'a \ 'a \ bool" (infix "\" 50) +begin + +lemma connex_iff_semiconnex_reflexive: "connex A (\) \ semiconnex A (\) \ reflexive A (\)" + (is "?c \ ?t \ ?r") +proof (intro iffI conjI; (elim conjE)?) + assume ?c then interpret connex. + show ?t apply unfold_locales using comparable by auto + show ?r by unfold_locales +next + assume ?t then interpret semiconnex A "(\)". + assume ?r then interpret reflexive. + from semiconnex show ?c by auto +qed + +lemma chain_connect: "Complete_Partial_Order.chain r A \ connex A r" + by (auto intro!: ext simp: atomize_eq connex_def Complete_Partial_Order.chain_def) + +lemma connex_union: + assumes "connex X (\)" and "connex Y (\)" and "\x \ X. \y \ Y. x \ y \ y \ x" + shows "connex (X\Y) (\)" + using assms by (auto simp: connex_def) + +end + +lemma connex_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "connex A r \ connex A r'" + by (simp add: connex_iff_semiconnex_reflexive r cong: semiconnex_cong reflexive_cong) + +locale total_pseudo_ordered_set = connex + antisymmetric +begin + +sublocale pseudo_ordered_set .. + +lemma not_weak_iff: + assumes x: "x \ A" and y: "y \ A" shows "\ y \ x \ x \ y \ x \ y" +using x y by (cases rule: comparable_cases, auto intro:antisym) + +lemma total_pseudo_ordered_subset: "B \ A \ total_pseudo_ordered_set B (\)" + apply (intro_locales) + using antisymmetric_subset connex_subset by auto + +end + +lemma total_pseudo_ordered_set_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "total_pseudo_ordered_set A r \ total_pseudo_ordered_set A r'" + by (simp add: total_pseudo_ordered_set_def r cong: connex_cong antisymmetric_cong) + +locale total_quasi_ordered_set = connex + transitive +begin + +sublocale quasi_ordered_set .. + +lemma total_quasi_ordered_subset: "B \ A \ total_quasi_ordered_set B (\)" + using transitive_subset connex_subset by intro_locales + +end + +lemma total_quasi_ordered_set_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "total_quasi_ordered_set A r \ total_quasi_ordered_set A r'" + by (simp add: total_quasi_ordered_set_def r cong: connex_cong transitive_cong) + +locale total_ordered_set = total_quasi_ordered_set + antisymmetric +begin + +sublocale partially_ordered_set + total_pseudo_ordered_set .. + +lemma total_ordered_subset: "B \ A \ total_ordered_set B (\)" + using total_quasi_ordered_subset antisymmetric_subset by (intro total_ordered_set.intro) + +end + +lemma total_ordered_set_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + shows "total_ordered_set A r \ total_ordered_set A r'" + by (simp add: total_ordered_set_def r cong: total_quasi_ordered_set_cong antisymmetric_cong) + +subsection \Well-Foundedness\ + +locale well_founded = related_set A "(\)" for A and less (infix "\" 50) + + assumes induct[consumes 1, case_names less, induct set]: + "a \ A \ (\x. x \ A \ (\y. y \ A \ y \ x \ P y) \ P x) \ P a" +begin + +sublocale asymmetric +proof (intro asymmetric.intro notI) + fix x y + assume xA: "x \ A" + then show "y \ A \ x \ y \ y \ x \ False" + by (induct arbitrary: y rule: induct, auto) +qed + +lemma prefixed_Imagep_imp_empty: + assumes a: "X \ ((\) ``` X) \ A" shows "X = {}" +proof - + from a have XA: "X \ A" by auto + have "x \ A \ x \ X" for x + proof (induct x rule: induct) + case (less x) + with a show ?case by (auto simp: Imagep_def) + qed + with XA show ?thesis by auto +qed + +lemma nonempty_imp_ex_minimal: + assumes QA: "Q \ A" and Q: "Q \ {}" + shows "\z \ Q. \y \ Q. \ y \ z" + using Q prefixed_Imagep_imp_empty[of Q] QA by (auto simp: Imagep_def) + +interpretation Restrp: well_founded UNIV "(\)\A" + rewrites "\x. x \ UNIV \ True" + and "(\)\A\UNIV = (\)\A" + and "\P1. (True \ PROP P1) \ PROP P1" + and "\P1. (True \ P1) \ Trueprop P1" + and "\P1 P2. (True \ PROP P1 \ PROP P2) \ (PROP P1 \ PROP P2)" +proof - + have "(\x. (\y. ((\) \ A) y x \ P y) \ P x) \ P a" for a P + using induct[of a P] by (auto simp: Restrp_def) + then show "well_founded UNIV ((\)\A)" apply unfold_locales by auto +qed auto + +lemmas Restrp_well_founded = Restrp.well_founded_axioms +lemmas Restrp_induct[consumes 0, case_names less] = Restrp.induct + +interpretation Restrp.tranclp: well_founded UNIV "((\)\A)\<^sup>+\<^sup>+" + rewrites "\x. x \ UNIV \ True" + and "((\)\A)\<^sup>+\<^sup>+ \ UNIV = ((\)\A)\<^sup>+\<^sup>+" + and "(((\)\A)\<^sup>+\<^sup>+)\<^sup>+\<^sup>+ = ((\)\A)\<^sup>+\<^sup>+" + and "\P1. (True \ PROP P1) \ PROP P1" + and "\P1. (True \ P1) \ Trueprop P1" + and "\P1 P2. (True \ PROP P1 \ PROP P2) \ (PROP P1 \ PROP P2)" +proof- + { fix P x + assume induct_step: "\x. (\y. ((\)\A)\<^sup>+\<^sup>+ y x \ P y) \ P x" + have "P x" + proof (rule induct_step) + show "\y. ((\)\A)\<^sup>+\<^sup>+ y x \ P y" + proof (induct x rule: Restrp_induct) + case (less x) + from \((\)\A)\<^sup>+\<^sup>+ y x\ + show ?case + proof (cases rule: tranclp.cases) + case r_into_trancl + with induct_step less show ?thesis by auto + next + case (trancl_into_trancl b) + with less show ?thesis by auto + qed + qed + qed + } + then show "well_founded UNIV ((\)\A)\<^sup>+\<^sup>+" by unfold_locales auto +qed auto + +lemmas Restrp_tranclp_well_founded = Restrp.tranclp.well_founded_axioms +lemmas Restrp_tranclp_induct[consumes 0, case_names less] = Restrp.tranclp.induct end context - fixes less :: "'a \ 'a \ bool" (infix "\" 50) -begin - -lemma asymmetricI[intro]: - assumes "\x y. x \ y \ y \ x \ False" - shows "asymmetric (\)" - apply unfold_locales using assms by auto - -lemma asymmetric_def': "asymmetric (\) \ \x y. \ (x \ y \ y \ x)" - by (auto simp: atomize_eq dest!: asymmetric.asym) - -end - -locale well_founded = less_syntax + - assumes induct: "\P a. (\x. (\y. y \ x \ P y) \ P x) \ P a" + fixes A :: "'a set" and less :: "'a \ 'a \ bool" (infix "\" 50) begin -lemma wfP[intro!]: "wfP (\)" using induct wfPUNIVI by blast - -sublocale asymmetric -proof (intro asymmetricI notI) - show "x \ y \ y \ x \ False" for x y by (induct x arbitrary: y rule: induct) +lemma well_foundedI_pf: + assumes pre: "\X. X \ A \ X \ ((\) ``` X) \ A \ X = {}" + shows "well_founded A (\)" +proof + fix P a assume aA: "a \ A" and Ind: "\x. x \ A \ (\y. y \ A \ y \ x \ P y) \ P x" + from Ind have "{a\A. \P a} \ ((\) ``` {a\A. \P a}) \ A" by (auto simp: Imagep_def) + from pre[OF _ this] aA + show "P a" by auto qed -end - -subsubsection \Combined Properties\ - -text \Some combinations of the above basic properties are given names.\ - -locale quasi_order = reflexive + transitive - -locale near_order = antisymmetric + transitive - -locale pseudo_order = reflexive + antisymmetric -begin - -lemma equiv_eq[simp]: "x \ y \ y \ x \ x = y" by auto - -lemma extreme_bound_singleton_eq[simp]: "extreme_bound (\) {x} y \ x = y" by auto - -lemma eq_iff: "x = y \ x \ y \ y \ x" by auto - -lemma extreme_order_iff_eq[simp]: "extreme (\) {x. x \ e} s \ e = s" by auto +lemma well_foundedI_min: + assumes a: "\X. X \ A \ X \ {} \ \x \ X. \y \ X. \ y \ x" + shows "well_founded A (\)" +proof (rule well_foundedI_pf) + fix X assume XA: "X \ A" and pf: "X \ ((\) ``` X) \ A" + from a[OF XA] pf show "X = {}" by (auto simp: Imagep_def) +qed + +lemma well_founded_iff_ex_minimal: + "well_founded A (\) \ (\X \ A. X \ {} \ (\x \ X. \z \ X. \ z \ x))" + using well_founded.nonempty_imp_ex_minimal well_foundedI_min by blast end -locale partial_order = quasi_order + antisymmetric - -sublocale partial_order \ pseudo_order + near_order .. - -locale strict_order = irreflexive + transitive "(\)" - -sublocale strict_order \ asymmetric by (auto dest: trans) -sublocale strict_order \ near_order "(\)" .. - -locale well_founded_order = well_founded + transitive "(\)" - -sublocale well_founded_order \ strict_order .. - -locale tolerance = equivalence_syntax + reflexive "(\)" + symmetric "(\)" - -locale partial_equivalence = equivalence_syntax + symmetric "(\)" + transitive "(\)" - -locale equivalence = equivalence_syntax + symmetric "(\)" + quasi_order "(\)" - -sublocale equivalence \ partial_equivalence .. - -text \Some combinations lead to uninteresting relations.\ - -proposition reflexive_irreflexive_is_empty: - assumes "reflexive r" and "irreflexive r" - shows "r = (\x y. False)" -proof(intro ext iffI) - interpret irreflexive r + reflexive r using assms by auto - fix x y - assume "r x y" - with irrefl have "x \ y" by auto - with refl show False by auto -qed auto - -proposition symmetric_antisymmetric_imp_eq: - assumes "symmetric r" and "antisymmetric r" - shows "r x y \ x = y" -proof- - interpret symmetric r + antisymmetric r using assms by auto - fix x y - assume "r x y" - with sym[OF this] show "x = y" by auto +lemma well_founded_cong: + assumes r: "\a b. a \ A \ b \ A \ r a b \ r' a b" + and A: "\a b. r' a b \ a \ A \ a \ A'" + and B: "\a b. r' a b \ b \ A \ b \ A'" + shows "well_founded A r \ well_founded A' r'" +proof (intro iffI) + assume wf: "well_founded A r" + show "well_founded A' r'" + proof (intro well_foundedI_min) + fix X + assume X: "X \ A'" and X0: "X \ {}" + show "\x\X. \y\X. \ r' y x" + proof (cases "X \ A = {}") + case True + from X0 obtain x where xX: "x \ X" by auto + with True have "x \ A" by auto + with xX X have "\y\X. \ r' y x" by (auto simp: B) + with xX show ?thesis by auto + next + case False + from well_founded.nonempty_imp_ex_minimal[OF wf _ this] + obtain x where x: "x \ X \ A" and Ar: "\y. y \ X \ y \ A \ \ r y x" by auto + have "\y \ X. \ r' y x" + proof (intro ballI notI) + fix y assume yX: "y \ X" and yx: "r' y x" + from yX X have yA': "y \ A'" by auto + show False + proof (cases "y \ A") + case True with x Ar[OF yX] yx r show ?thesis by auto + next + case False with yA' x A[OF yx] r X show ?thesis by (auto simp:) + qed + qed + with x show "\x \ X. \y \ X. \ r' y x" by auto + qed + qed +next + assume wf: "well_founded A' r'" + show "well_founded A r" + proof (intro well_foundedI_min) + fix X + assume X: "X \ A" and X0: "X \ {}" + show "\x\X. \y\X. \ r y x" + proof (cases "X \ A' = {}") + case True + from X0 obtain x where xX: "x \ X" by auto + with True have "x \ A'" by auto + with xX X B have "\y\X. \ r y x" by (auto simp: r in_mono) + with xX show ?thesis by auto + next + case False + from well_founded.nonempty_imp_ex_minimal[OF wf _ this] + obtain x where x: "x \ X \ A'" and Ar: "\y. y \ X \ y \ A' \ \ r' y x" by auto + have "\y \ X. \ r y x" + proof (intro ballI notI) + fix y assume yX: "y \ X" and yx: "r y x" + from yX X have y: "y \ A" by auto + show False + proof (cases "y \ A'") + case True with x Ar[OF yX] yx r X y show ?thesis by auto + next + case False with y x A yx r X show ?thesis by auto + qed + qed + with x show "\x \ X. \y \ X. \ r y x" by auto + qed + qed qed -proposition nontolerance: - fixes r (infix "\" 50) - shows "irreflexive (\) \ symmetric (\) \ tolerance (\x y. \ x \ y)" -proof safe - assume "irreflexive (\)" and "symmetric (\)" - then interpret irreflexive "(\)" + symmetric "(\)". - show "tolerance (\x y. \ x \ y)" by (unfold_locales, auto dest: sym) +lemma wfP_iff_well_founded_UNIV: "wfP r \ well_founded UNIV r" + by (auto simp: wfP_def wf_def well_founded_def) + +lemma well_founded_singleton: + assumes "\r x x" shows "well_founded {x} r" + using assms by (auto simp: well_founded_iff_ex_minimal) + +lemma well_founded_Restrp[simp]: "well_founded A (r\B) \ well_founded (A\B) r" (is "?l \ ?r") +proof (intro iffI well_foundedI_min) + assume l: ?l + fix X assume XAB: "X \ A \ B" and X0: "X \ {}" + with l[THEN well_founded.nonempty_imp_ex_minimal] + have "\x\X. \z\X. \ (r \ B) z x" by auto + with XAB show "\x\X. \y\X. \ r y x" by (auto simp: Restrp_def) next - assume "tolerance (\x y. \ x \ y)" - then interpret tolerance "\x y. \ x \ y". - show "irreflexive (\)" by auto - show "symmetric (\)" using sym by auto + assume r: ?r + fix X assume XA: "X \ A" and X0: "X \ {}" + show "\x\X. \y\X. \ (r \ B) y x" + proof (cases "X \ B") + case True + with r[THEN well_founded.nonempty_imp_ex_minimal, of X] XA X0 + have "\z\X. \y\X. \ r y z" by auto + then show ?thesis by auto + next + case False + then obtain x where x: "x \ X - B" by auto + then have "\y\X. \ (r \ B) y x" by auto + with x show ?thesis by auto + qed qed -proposition irreflexive_transitive_symmetric_is_empty: - assumes "irreflexive r" and "transitive r" and "symmetric r" - shows "r = (\x y. False)" -proof(intro ext iffI) - interpret strict_order r using assms by (unfold strict_order_def, auto) - interpret symmetric r using assms by auto - fix x y - assume "r x y" - also note sym[OF this] - finally have "r x x". - then show False by auto -qed auto - -subsection \Totality\ - -locale total = less_syntax + assumes total: "x \ y \ x = y \ y \ x" +lemma (in well_founded) well_founded_subset: + assumes "B \ A" shows "well_founded B (\)" + using assms well_founded_axioms by (auto simp: well_founded_iff_ex_minimal) + +lemma well_founded_extend: + fixes less (infix "\" 50) + assumes A: "well_founded A (\)" + assumes B: "well_founded B (\)" + assumes AB: "\a \ A. \b \ B. \b \ a" + shows "well_founded (A \ B) (\)" +proof (intro well_foundedI_min) + interpret A: well_founded A "(\)" using A. + interpret B: well_founded B "(\)" using B. + fix X assume XAB: "X \ A \ B" and X0: "X \ {}" + show "\x\X. \y\X. \ y \ x" + proof (cases "X \ A = {}") + case True + with XAB have XB: "X \ B" by auto + from B.nonempty_imp_ex_minimal[OF XB X0] show ?thesis. + next + case False + with A.nonempty_imp_ex_minimal[OF _ this] + obtain e where XAe: "e \ X \ A" "\y\X \ A. \ y \ e" by auto + then have eX: "e \ X" and eA: "e \ A" by auto + { fix x assume xX: "x \ X" + have "\x \ e" + proof (cases "x \ A") + case True with XAe xX show ?thesis by auto + next + case False + with xX XAB have "x \ B" by auto + with AB eA show ?thesis by auto + qed + } + with eX show ?thesis by auto + qed +qed + +lemma lower_UN_well_founded: + fixes r (infix "\" 50) + assumes XX: "\X\XX. well_founded X (\) \ (\x\X. \y\\XX. y \ x \ y \ X)" + shows "well_founded (\XX) (\)" +proof (intro well_foundedI_min) + have *: "X \ XX \ x\X \ y \ \XX \ y \ x \ y \ X" for X x y using XX by blast + fix S + assume S: "S \ \XX" and S0: "S \ {}" + from S0 obtain x where xS: "x \ S" by auto + with S obtain X where X: "X \ XX" and xX: "x \ X" by auto + from xS xX have Sx0: "S \ X \ {}" by auto + from X XX interpret well_founded X "(\)" by auto + from nonempty_imp_ex_minimal[OF _ Sx0] + obtain z where zS: "z \ S" and zX: "z \ X" and min: "\y \ S \ X. \ y \ z" by auto + show "\x\S. \y\S. \ y \ x" + proof (intro bexI[OF _ zS] ballI notI) + fix y + assume yS: "y \ S" and yz: "y \ z" + have yXX: "y \ \ XX" using S yS by auto + from *[OF X zX yXX yz] yS have "y \ X \ S" by auto + with min yz show False by auto + qed +qed + +lemma well_founded_cmono: + assumes r': "r' \ r" and wf: "well_founded A r" + shows "well_founded A r'" +proof (intro well_foundedI_min) + fix X assume "X \ A" and "X \ {}" + from well_founded.nonempty_imp_ex_minimal[OF wf this] + show "\x\X. \y\X. \ r' y x" using r' by auto +qed + +locale well_founded_ordered_set = well_founded + transitive _ "(\)" begin -lemma cases[case_names less eq greater]: - assumes "x \ y \ P" and "x = y \ P" and "y \ x \ P" - shows "P" using total assms by auto - -lemma neqE: "x \ y \ (x \ y \ P) \ (y \ x \ P) \ P" by (cases x y rule: cases, auto) +sublocale strict_ordered_set.. + +interpretation Restrp: strict_ordered_set UNIV "(\)\A" + Restrp: well_founded UNIV "(\)\A" + using Restrp_strict_order Restrp_well_founded . + +lemma Restrp_well_founded_order: "well_founded_ordered_set UNIV ((\)\A)".. + +lemma well_founded_ordered_subset: "B \ A \ well_founded_ordered_set B (\)" + apply intro_locales + using well_founded_subset transitive_subset by auto end -lemmas totalI[intro] = total.intro - -text \Totality is negated antisymmetry \cite[Proposition 2.2.4]{Schmidt1993}.\ -proposition total_iff_neg_antisymmetric: - fixes less (infix "\" 50) - shows "total (\) \ antisymmetric (\x y. \ x \ y)" (is "?l \ ?r") -proof (intro iffI totalI antisymmetricI) - assume ?l - then interpret total. - fix x y - assume "\ x \ y" and "\ y \ x" - then show "x = y" by (cases x y rule: cases, auto) -next - assume ?r - then interpret neg: antisymmetric "(\x y. \ x \ y)". - fix x y - show "x \ y \ x = y \ y \ x" using neg.antisym by auto + +lemma (in well_founded) Restrp_tranclp_well_founded_ordered: "well_founded_ordered_set UNIV ((\)\A)\<^sup>+\<^sup>+" + using Restrp_tranclp_well_founded tranclp_transitive by intro_locales + +locale well_related_set = related_set + + assumes nonempty_imp_ex_extreme: "X \ A \ X \ {} \ \e. extreme X (\)\<^sup>- e" +begin + +sublocale connex +proof + fix x y assume "x \ A" and "y \ A" + with nonempty_imp_ex_extreme[of "{x,y}"] show "x \ y \ y \ x" by auto qed -locale total_irreflexive = total + irreflexive -begin - -lemma neq_iff: "x \ y \ x \ y \ y \ x" by (auto elim:neqE) - -end - -locale total_reflexive = reflexive + weak: total "(\)" -begin - -lemma comparable: "x \ y \ y \ x" by (cases x y rule:weak.cases, auto) - -lemma comparable_cases[case_names le ge]: - assumes "x \ y \ P" and "y \ x \ P" shows "P" using assms comparable by auto - -lemma chain_UNIV: "chain (\) UNIV" by (intro chainI comparable) +lemmas connex_axioms = connex_axioms + +interpretation less_eq_notations. + +sublocale asym: well_founded A "(\)" +proof (unfold well_founded_iff_ex_minimal, intro allI impI) + fix X + assume XA: "X \ A" and X0: "X \ {}" + from nonempty_imp_ex_extreme[OF XA X0] obtain e where "extreme X (\)\<^sup>- e" by auto + then show "\x\X. \z\X. \z \ x" by (auto intro!: bexI[of _ e]) +qed + +lemma well_related_subset: "B \ A \ well_related_set B (\)" + by (auto intro!: well_related_set.intro nonempty_imp_ex_extreme) end context fixes less_eq :: "'a \ 'a \ bool" (infix "\" 50) begin -lemma total_reflexiveI[intro]: - assumes "\x y. x \ y \ y \ x" shows "total_reflexive (\)" - using assms by (unfold_locales, auto) - -lemma total_reflexive_def': "total_reflexive (\) \ \x y. x \ y \ y \ x" - by (unfold atomize_eq, auto dest: total_reflexive.comparable) - -end - -locale total_pseudo_order = total_reflexive + antisymmetric -begin - -sublocale pseudo_order .. - -lemma not_weak_iff: "\ y \ x \ x \ y \ x \ y" by (cases x y rule:comparable_cases, auto) +lemma well_related_iff_neg_well_founded: + "well_related_set A (\) \ well_founded A (\x y. \ y \ x)" + by (simp add: well_related_set_def well_founded_iff_ex_minimal extreme_def Bex_def) + +lemma well_related_singleton_refl: + assumes "x \ x" shows "well_related_set {x} (\)" + by (intro well_related_set.intro exI[of _ x], auto simp: subset_singleton_iff assms) + +lemma lower_UN_well_related: + assumes XX: "\X\XX. well_related_set X (\) \ (\x\X. \y\\XX. \x \ y \ y \ X)" + shows "well_related_set (\XX) (\)" + using XX + apply (unfold well_related_iff_neg_well_founded) + using lower_UN_well_founded[of _ "\x y. \ y \ x"]. end -locale total_quasi_order = total_reflexive + transitive +lemma well_related_extend: + fixes r (infix "\" 50) + assumes "well_related_set A (\)" and "well_related_set B (\)" and "\a \ A. \b \ B. a \ b" + shows "well_related_set (A \ B) (\)" + using well_founded_extend[of _ "\x y. \ y \ x", folded well_related_iff_neg_well_founded] + using assms by auto + +locale pre_well_ordered_set = semiattractive + well_related_set begin -sublocale quasi_order .. +interpretation less_eq_notations. + +sublocale transitive +proof + fix x y z assume xy: "x \ y" and yz: "y \ z" and x: "x \ A" and y: "y \ A" and z: "z \ A" + from x y z have "\e. extreme {x,y,z} (\) e" (is "\e. ?P e") by (auto intro!: nonempty_imp_ex_extreme) + then have "?P x \ ?P y \ ?P z" by auto + then show "x \ z" + proof (elim disjE) + assume "?P x" + then show ?thesis by auto + next + assume "?P y" + then have "y \ x" by auto + from attract[OF xy this yz] x y z show ?thesis by auto + next + assume "?P z" + then have zx: "z \ x" and zy: "z \ y" by auto + from attract[OF yz zy zx] x y z have yx: "y \ x" by auto + from attract[OF xy yx yz] x y z show ?thesis by auto + qed +qed + +sublocale total_quasi_ordered_set.. + +lemmas connex_axioms = connex_axioms + +lemma strict_weak_trans[trans]: + assumes xy: "x \ y" and yz: "y \ z" and x: "x \ A" and y: "y \ A" and z: "z \ A" + shows "x \ z" +proof (intro asympartpI notI) + from trans xy yz x y z show "x \ z" by auto + assume "z \ x" + from trans[OF yz this] y z x have "y \ x" by auto + with xy show False by auto +qed + +lemma weak_strict_trans[trans]: + assumes xy: "x \ y" and yz: "y \ z" and x: "x \ A" and y: "y \ A" and z: "z \ A" + shows "x \ z" +proof (intro asympartpI notI) + from trans xy yz x y z show "x \ z" by auto + assume "z \ x" + from trans[OF this xy] z x y have "z \ y" by auto + with yz show False by auto +qed end -locale total_order = total_quasi_order + antisymmetric +lemma pre_well_ordered_iff: + "pre_well_ordered_set A r \ total_quasi_ordered_set A r \ well_founded A (asympartp r)" + (is "?p \ ?t \ ?w") +proof safe + assume ?p + then interpret pre_well_ordered_set A r. + show ?t ?w by unfold_locales +next + assume ?t + then interpret total_quasi_ordered_set A r. + assume ?w + then have "well_founded UNIV (asympartp r \ A)" by simp + also have "asympartp r \ A = (\x y. \ r y x) \ A" by (intro ext, auto simp: not_iff_asym) + finally have "well_related_set A r" by (simp add: well_related_iff_neg_well_founded) + then show ?p by intro_locales +qed + +lemma (in semiattractive) pre_well_ordered_iff_well_related: + assumes XA: "X \ A" + shows "pre_well_ordered_set X (\) \ well_related_set X (\)" (is "?l \ ?r") +proof + interpret X: semiattractive X using semiattractive_subset[OF XA]. + { assume ?l + then interpret X: pre_well_ordered_set X. + show ?r by unfold_locales + } + assume ?r + then interpret X: well_related_set X. + show ?l by unfold_locales +qed + +lemma semiattractive_extend: + fixes r (infix "\" 50) + assumes A: "semiattractive A (\)" and B: "semiattractive B (\)" + and AB: "\a \ A. \b \ B. a \ b \ \ b \ a" + shows "semiattractive (A \ B) (\)" +proof- + interpret A: semiattractive A "(\)" using A. + interpret B: semiattractive B "(\)" using B. + { + fix x y z + assume yB: "y \ B" and zA: "z \ A" and yz: "y \ z" + have False using AB[rule_format, OF zA yB] yz by auto + } + note * = this + show ?thesis + by (auto intro!: semiattractive.intro dest:* AB[rule_format] A.attract B.attract) +qed + +lemma pre_well_order_extend: + fixes r (infix "\" 50) + assumes A: "pre_well_ordered_set A (\)" and B: "pre_well_ordered_set B (\)" + and AB: "\a \ A. \b \ B. a \ b \ \ b \ a" + shows "pre_well_ordered_set (A\B) (\)" +proof- + interpret A: pre_well_ordered_set A "(\)" using A. + interpret B: pre_well_ordered_set B "(\)" using B. + show ?thesis + apply (intro pre_well_ordered_set.intro well_related_extend semiattractive_extend) + apply unfold_locales + by (auto dest: AB[rule_format]) +qed + +locale well_ordered_set = antisymmetric + well_related_set begin -sublocale partial_order + total_pseudo_order .. +sublocale pre_well_ordered_set.. + +sublocale total_ordered_set.. + +lemma well_ordered_subset: "B \ A \ well_ordered_set B (\)" + using well_related_subset antisymmetric_subset by (intro well_ordered_set.intro) + +lemmas connex_axioms = connex_axioms end -text \A strict total order defines a total weak order, so we will formalize -it after giving locales for pair of weak and strict parts.\ +lemma (in antisymmetric) well_ordered_iff_well_related: + assumes XA: "X \ A" + shows "well_ordered_set X (\) \ well_related_set X (\)" (is "?l \ ?r") +proof + interpret X: antisymmetric X using antisymmetric_subset[OF XA]. + { assume ?l + then interpret X: well_ordered_set X. + show ?r by unfold_locales + } + assume ?r + then interpret X: well_related_set X. + show ?l by unfold_locales +qed + +context + fixes A and less_eq (infix "\" 50) + assumes A: "\a \ A. \b \ A. a \ b" +begin + +interpretation well_related_set A "(\)" + apply unfold_locales + using A by blast + +lemmas trivial_well_related = well_related_set_axioms + +lemma trivial_pre_well_order: "pre_well_ordered_set A (\)" + apply unfold_locales + using A by blast + +end + +context + fixes less_eq :: "'a \ 'a \ bool" (infix "\" 50) +begin + +interpretation less_eq_notations. + +lemma well_order_extend: + assumes A: "well_ordered_set A (\)" and B: "well_ordered_set B (\)" + and ABa: "\a \ A. \b \ B. a \ b \ b \ a \ a = b" + and AB: "\a \ A. \b \ B. a \ b" + shows "well_ordered_set (A\B) (\)" +proof- + interpret A: well_ordered_set A "(\)" using A. + interpret B: well_ordered_set B "(\)" using B. + show ?thesis + apply (intro well_ordered_set.intro antisymmetric_union well_related_extend ABa AB) + by unfold_locales +qed + +interpretation singleton: antisymmetric "{a}" "(\)" for a apply unfold_locales by auto + +lemmas singleton_antisymmetric[intro!] = singleton.antisymmetric_axioms + +lemma singleton_well_ordered[intro!]: "a \ a \ well_ordered_set {a} (\)" + apply unfold_locales by auto + +lemma lower_UN_well_ordered: + assumes anti: "antisymmetric (\ XX) (\)" + and XX: "\X\XX. well_ordered_set X (\) \ (\x\X. \y\\XX. \ x \ y \ y \ X)" + shows "well_ordered_set (\XX) (\)" + apply (intro well_ordered_set.intro lower_UN_well_related anti) + using XX well_ordered_set.axioms by fast + +end + +text \Directed sets:\ + +definition "directed A r \ \x \ A. \y \ A. \z \ A. r x z \ r y z" + +lemmas directedI[intro] = directed_def[unfolded atomize_eq, THEN iffD2, rule_format] + +lemmas directedD = directed_def[unfolded atomize_eq, THEN iffD1, rule_format] + +context + fixes less_eq :: "'a \ 'a \ bool" (infix "\" 50) +begin + +lemma directedE: + assumes "directed A (\)" and "x \ A" and "y \ A" + and "\z. z \ A \ x \ z \ y \ z \ thesis" + shows "thesis" + using assms by (auto dest: directedD) + +lemma directed_empty[simp]: "directed {} (\)" by auto + +lemma directed_union: + assumes dX: "directed X (\)" and dY: "directed Y (\)" + and XY: "\x\X. \y\Y. \z \ X \ Y. x \ z \ y \ z" + shows "directed (X \ Y) (\)" + using directedD[OF dX] directedD[OF dY] XY + apply (intro directedI) by blast + +lemma directed_extend: + assumes X: "directed X (\)" and Y: "directed Y (\)" and XY: "\x\X. \y\Y. x \ y" + shows "directed (X \ Y) (\)" +proof - + { fix x y + assume xX: "x \ X" and yY: "y \ Y" + let ?g = "\z\X \ Y. x \ z \ y \ z" + from directedD[OF Y yY yY] obtain z where zY: "z \ Y" and yz: "y \ z" by auto + from xX XY zY yz have ?g by auto + } + then show ?thesis by (auto intro!: directed_union[OF X Y]) +qed + +end + +context connex begin + +lemma directed: "directed A (\)" +proof + fix x y + assume x: "x \ A" and y: "y \ A" + then show "\z\A. x \ z \ y \ z" + proof (cases rule: comparable_cases) + case le + with refl[OF y] y show ?thesis by (intro bexI[of _ y], auto) + next + case ge + with refl[OF x] x show ?thesis by (intro bexI[of _ x], auto) + qed +qed + +end + +context + fixes ir :: "'i \ 'i \ bool" (infix "\" 50) + fixes r :: "'a \ 'a \ bool" (infix "\" 50) +begin + +lemma monotone_connex_image: + assumes mono: "monotone_on I (\) (\) f" + assumes connex: "connex I (\)" + shows "connex (f ` I) (\)" +proof (rule connexI) + fix x y + assume "x \ f ` I" and "y \ f ` I" + then obtain i j where ij: "i \ I" "j \ I" and [simp]: "x = f i" "y = f j" by auto + from connex ij have "i \ j \ j \ i" by (auto elim: connexE) + with ij mono show "x \ y \ y \ x" by (elim disjE, auto dest: monotone_onD) +qed + +lemma monotone_directed_image: + assumes mono: "monotone_on I (\) (\) f" + assumes dir: "directed I (\)" shows "directed (f ` I) (\)" +proof (rule directedI, safe) + fix x y assume x: "x \ I" and y: "y \ I" + with dir obtain z where z: "z \ I" and "x \ z" and "y \ z" by (auto elim: directedE) + with mono x y have "f x \ f z" and "f y \ f z" by (auto dest: monotone_onD) + with z show "\fz \ f ` I. f x \ fz \ f y \ fz" by auto +qed + +end subsection \Order Pairs\ -locale compatible_ordering = less_eq_syntax + less_syntax + reflexive "(\)" + irreflexive "(\)" + - assumes weak_strict_trans[trans]: "x \ y \ y \ z \ x \ z" - assumes strict_weak_trans[trans]: "x \ y \ y \ z \ x \ z" - assumes strict_implies_weak: "x \ y \ x \ y" +locale compatible = related_set + related_set A "(\)" for less (infix "\" 50) + + assumes compat_right[trans]: "x \ y \ y \ z \ x \ A \ y \ A \ z \ A \ x \ z" + assumes compat_left[trans]: "x \ y \ y \ z \ x \ A \ y \ A \ z \ A \ x \ z" + +locale compatible_ordering = reflexive + irreflexive + compatible + + assumes strict_implies_weak: "x \ y \ x \ A \ y \ A \ x \ y" begin text \The strict part is necessarily transitive.\ -sublocale strict: transitive "(\)" - using weak_strict_trans[OF strict_implies_weak] by unfold_locales - text \The following sequence of declarations are in order to obtain fact names in a manner similar to the Isabelle/HOL facts of orders.\ -interpretation strict_order "(\)" .. - -sublocale strict: near_order "(\)" by unfold_locales - -sublocale asymmetric "(\)" by unfold_locales - -sublocale strict_order "(\)" .. - -thm strict.antisym strict.trans asym irrefl - -lemma strict_implies_not_weak: "x \ y \ \ y \ x" by (auto dest: strict_weak_trans) +sublocale strict: transitive A "(\)" + using compat_right[OF strict_implies_weak] by unfold_locales + +sublocale strict_ordered_set A "(\)" .. + +thm strict.trans asym irrefl + +lemma strict_implies_not_weak: "x \ y \ x \ A \ y \ A \ \ y \ x" + using irrefl compat_left by blast + +end + +context transitive begin + +interpretation less_eq_notations. + +lemma asym_trans[trans]: + shows "x \ y \ y \ z \ x \ A \ y \ A \ z \ A \ x \ z" + and "x \ y \ y \ z \ x \ A \ y \ A \ z \ A \ x \ z" + by (auto 0 3 dest: trans) end locale attractive_ordering = compatible_ordering + attractive -locale pseudo_ordering = compatible_ordering + antisymmetric +locale pseudo_ordering = compatible_ordering + pseudo_ordered_set begin -sublocale pseudo_order + attractive_ordering .. +sublocale attractive_ordering .. end -locale quasi_ordering = compatible_ordering + transitive +locale quasi_ordering = compatible_ordering + quasi_ordered_set begin -sublocale quasi_order + attractive_ordering .. +sublocale attractive_ordering .. end -locale partial_ordering = compatible_ordering + near_order +locale partial_ordering = compatible_ordering + partially_ordered_set begin -sublocale partial_order + pseudo_ordering + quasi_ordering .. +sublocale pseudo_ordering + quasi_ordering .. end locale well_founded_ordering = quasi_ordering + well_founded -locale total_ordering = compatible_ordering + total_order +locale total_ordering = compatible_ordering + total_ordered_set begin sublocale partial_ordering .. end -locale strict_total_ordering = partial_ordering + total "(\)" +locale strict_total_ordering = partial_ordering + semiconnex A "(\)" begin -sublocale total_irreflexive "(\)" .. - -sublocale total_reflexive "(\)" +sublocale semiconnex_irreflexive .. + +sublocale connex proof - fix x y show "x \ y \ y \ x" by (cases x y rule: cases, auto dest: strict_implies_weak) + fix x y assume x: "x \ A" and y: "y \ A" + then show "x \ y \ y \ x" + apply (cases rule: cases[OF x y]) + by (auto dest: strict_implies_weak) qed sublocale total_ordering .. - +(* sublocale old: ordering "(\)" "(\)" proof- have "a \ b \ a \ b \ a \ b" for a b by (cases a b rule: cases, auto dest: strict_implies_weak) then show "ordering (\) (\)" by (unfold_locales, auto dest:strict_implies_weak trans) qed - -lemma not_weak[simp]: "\ x \ y \ y \ x" by (simp add: not_weak_iff old.strict_iff_order) - -lemma not_strict[simp]: "\ x \ y \ y \ x" by (auto simp: old.strict_iff_order) - -end - - -text \A locale which defines an equivalence relation. Be careful when declaring simp rules etc., -as the equivalence will often be rewritten to equality.\ - -locale quasi_order_equivalence = quasi_order + equivalence_syntax + - assumes equiv_def: "x \ y \ x \ y \ y \ x" -begin - -sublocale equiv: equivalence by (unfold_locales, auto simp: equiv_def dest: trans) - -lemma [trans]: - shows equiv_weak_trans: "x \ y \ y \ z \ x \ z" - and weak_equiv_trans: "x \ y \ y \ z \ x \ z" - by (auto simp: equiv_def dest: trans) - -lemma extreme_order_iff_equiv[simp]: "extreme (\) {x. x \ e} y \ e \ y" - by (auto simp: equiv_def intro!: extremeI dest: trans) - -lemma extreme_bound_iff_equiv: - assumes bX: "extreme_bound (\) X b" shows "extreme_bound (\) X c \ b \ c" -proof(rule iffI) - from bX have bX: "bound (\) X b" and leastb: "\x. bound (\) X x \ b \ x" by auto - { fix c assume "extreme_bound (\) X c" - then have cbounds: "bound (\) X c" and leastc: "\b. bound (\) X b \ c \ b" by auto - from leastb[OF cbounds] leastc[OF bX] show "b \ c" by (auto simp: equiv_def) - } - { fix c assume bc: "b \ c" - show "extreme_bound (\) X c" - proof(intro extreme_boundI) - fix x assume "x \ X" - with bX have "x \ b" by auto - with bc show "x \ c" by (auto dest: trans simp: equiv_def) - next - fix x assume "bound (\) X x" - from leastb[OF this] bc show "c \ x" by (auto dest: trans simp: equiv_def) - qed - } -qed - -lemma extremes_are_equiv: "extreme (\) X x \ extreme (\) X y \ x \ y" - by (auto simp: equiv_def) - -end - -locale quasi_ordering_equivalence = compatible_ordering + quasi_order_equivalence -begin - -lemma [trans]: - shows equiv_strict_trans: "x \ y \ y \ z \ x \ z" - and strict_equiv_trans: "x \ y \ y \ z \ x \ z" - by (auto simp: equiv_def dest: weak_strict_trans strict_weak_trans) +*) + +lemma not_weak[simp]: + assumes "x \ A" and "y \ A" shows "\ x \ y \ y \ x" + using assms by (cases rule:cases, auto simp: strict_implies_not_weak dest: strict_implies_weak) + +lemma not_strict[simp]: "x \ A \ y \ A \ \ x \ y \ y \ x" + using not_weak by blast end subsection \Relating to Classes\ -text \In Isabelle 2019 (and earlier), we should declare sublocales in class before declaring dual +text \In Isabelle 2020, we should declare sublocales in class before declaring dual sublocales, since otherwise facts would be prefixed by ``dual.dual.''\ context ord begin -abbreviation upper_bound where "upper_bound \ bound (\)" - -abbreviation least where "least \ extreme (\x y. y \ x)" - -abbreviation lower_bound where "lower_bound \ bound (\x y. y \ x)" - -abbreviation greatest where "greatest \ extreme (\)" - -abbreviation supremum where "supremum \ extreme_bound (\)" - -abbreviation infimum where "infimum \ extreme_bound (\x y. y \ x)" +abbreviation least where "least X \ extreme X (\x y. y \ x)" + +abbreviation greatest where "greatest X \ extreme X (\)" + +abbreviation supremum where "supremum X \ least (Collect (bound X (\)))" + +abbreviation infimum where "infimum X \ greatest (Collect (bound X (\x y. y \ x)))" lemma Least_eq_The_least: "Least P = The (least {x. P x})" by (auto simp: Least_def extreme_def[unfolded atomize_eq, THEN ext]) lemma Greatest_eq_The_greatest: "Greatest P = The (greatest {x. P x})" by (auto simp: Greatest_def extreme_def[unfolded atomize_eq, THEN ext]) end -lemma fun_ord_le: "fun_ord (\) = (\)" by (intro ext, simp add: fun_ord_def le_fun_def) -lemma fun_ord_ge: "fun_ord (\) = (\)" by (intro ext, simp add: fun_ord_def le_fun_def) - -lemmas fun_supremum_iff = fun_extreme_bound_iff[of "(\)", unfolded fun_ord_le] -lemmas fun_infimum_iff = fun_extreme_bound_iff[of "(\)", unfolded fun_ord_ge] - -class compat = ord + assumes "compatible_ordering (\) (<)" +lemma Ball_UNIV[simp]: "Ball UNIV = All" by auto +lemma Bex_UNIV[simp]: "Bex UNIV = Ex" by auto + +class compat = ord + assumes "compatible_ordering UNIV (\) (<)" begin -sublocale order: compatible_ordering using compat_axioms unfolding class.compat_def. +sublocale order: compatible_ordering UNIV + rewrites "\x. x \ UNIV \ True" + and "\X. X \ UNIV \ True" + and "\r. r \ UNIV \ r" + and "\P. True \ P \ P" + and "Ball UNIV \ All" + and "Bex UNIV \ Ex" + and "sympartp (\)\<^sup>- \ sympartp (\)" + and "\P1. (True \ PROP P1) \ PROP P1" + and "\P1. (True \ P1) \ Trueprop P1" + and "\P1 P2. (True \ PROP P1 \ PROP P2) \ (PROP P1 \ PROP P2)" + using compat_axioms unfolding class.compat_def by (auto 0 4 simp:atomize_eq) end text \We should have imported locale-based facts in classes, e.g.:\ thm order.trans order.strict.trans order.refl order.irrefl order.asym order.extreme_bound_singleton -class attractive_order = ord + assumes "attractive_ordering (\) (<)" +class attractive_order = ord + assumes "attractive_ordering UNIV (\) (<)" begin -interpretation order: attractive_ordering +text \We need to declare subclasses before sublocales in order to preserve facts for superclasses.\ + +interpretation attractive_ordering UNIV using attractive_order_axioms unfolding class.attractive_order_def. subclass compat .. -sublocale order: attractive_ordering .. +sublocale order: attractive_ordering UNIV + rewrites "\x. x \ UNIV \ True" + and "\X. X \ UNIV \ True" + and "\r. r \ UNIV \ r" + and "\P. True \ P \ P" + and "Ball UNIV \ All" + and "Bex UNIV \ Ex" + and "sympartp (\)\<^sup>- \ sympartp (\)" + and "\P1. (True \ PROP P1) \ PROP P1" + and "\P1. (True \ P1) \ Trueprop P1" + and "\P1 P2. (True \ PROP P1 \ PROP P2) \ (PROP P1 \ PROP P2)" + apply unfold_locales by (auto simp:atomize_eq) end thm order.extreme_bound_quasi_const -class psorder = ord + assumes "pseudo_ordering (\) (<)" +class psorder = ord + assumes "pseudo_ordering UNIV (\) (<)" begin -text \We need to declare subclasses before sublocales in order to preserve facts for superclasses.\ - -interpretation order: pseudo_ordering using psorder_axioms unfolding class.psorder_def. +interpretation pseudo_ordering UNIV using psorder_axioms unfolding class.psorder_def. subclass attractive_order .. -sublocale order: pseudo_ordering .. +sublocale order: pseudo_ordering UNIV + rewrites "\x. x \ UNIV \ True" + and "\X. X \ UNIV \ True" + and "\r. r \ UNIV \ r" + and "\P. True \ P \ P" + and "Ball UNIV \ All" + and "Bex UNIV \ Ex" + and "sympartp (\)\<^sup>- \ sympartp (\)" + and "\P1. (True \ PROP P1) \ PROP P1" + and "\P1. (True \ P1) \ Trueprop P1" + and "\P1 P2. (True \ PROP P1 \ PROP P2) \ (PROP P1 \ PROP P2)" + apply unfold_locales by (auto simp:atomize_eq) end -class qorder = ord + assumes "quasi_ordering (\) (<)" +class qorder = ord + assumes "quasi_ordering UNIV (\) (<)" begin -interpretation order: quasi_ordering using qorder_axioms unfolding class.qorder_def. +interpretation quasi_ordering UNIV using qorder_axioms unfolding class.qorder_def. subclass attractive_order .. -sublocale order: quasi_ordering .. +sublocale order: quasi_ordering UNIV + rewrites "\x. x \ UNIV \ True" + and "\X. X \ UNIV \ True" + and "\r. r \ UNIV \ r" + and "\P. True \ P \ P" + and "Ball UNIV \ All" + and "Bex UNIV \ Ex" + and "sympartp (\)\<^sup>- \ sympartp (\)" + and "\P1. (True \ PROP P1) \ PROP P1" + and "\P1. (True \ P1) \ Trueprop P1" + and "\P1 P2. (True \ PROP P1 \ PROP P2) \ (PROP P1 \ PROP P2)" + apply unfold_locales by (auto simp:atomize_eq) end -class porder = ord + assumes "partial_ordering (\) (<)" +class porder = ord + assumes "partial_ordering UNIV (\) (<)" begin -interpretation order: partial_ordering using porder_axioms unfolding class.porder_def. +interpretation partial_ordering UNIV + using porder_axioms unfolding class.porder_def. subclass psorder .. subclass qorder .. -sublocale order: partial_ordering .. +sublocale order: partial_ordering UNIV + rewrites "\x. x \ UNIV \ True" + and "\X. X \ UNIV \ True" + and "\r. r \ UNIV \ r" + and "\P. True \ P \ P" + and "Ball UNIV \ All" + and "Bex UNIV \ Ex" + and "sympartp (\)\<^sup>- \ sympartp (\)" + and "\P1. (True \ PROP P1) \ PROP P1" + and "\P1. (True \ P1) \ Trueprop P1" + and "\P1 P2. (True \ PROP P1 \ PROP P2) \ (PROP P1 \ PROP P2)" + apply unfold_locales by (auto simp:atomize_eq) end -class wf_qorder = ord + assumes "well_founded_ordering (\) (<)" +class wf_qorder = ord + assumes "well_founded_ordering UNIV (\) (<)" begin -interpretation order: well_founded_ordering using wf_qorder_axioms unfolding class.wf_qorder_def. +interpretation well_founded_ordering UNIV + using wf_qorder_axioms unfolding class.wf_qorder_def. subclass qorder .. -sublocale order: well_founded_ordering .. +sublocale order: well_founded_ordering UNIV + rewrites "\x. x \ UNIV \ True" + and "\X. X \ UNIV \ True" + and "\r. r \ UNIV \ r" + and "\P. True \ P \ P" + and "Ball UNIV \ All" + and "Bex UNIV \ Ex" + and "sympartp (\)\<^sup>- \ sympartp (\)" + and "\P1. (True \ PROP P1) \ PROP P1" + and "\P1. (True \ P1) \ Trueprop P1" + and "\P1 P2. (True \ PROP P1 \ PROP P2) \ (PROP P1 \ PROP P2)" + apply unfold_locales by (auto simp:atomize_eq) end -class totalorder = ord + assumes "total_ordering (\) (<)" +class totalorder = ord + assumes "total_ordering UNIV (\) (<)" begin -interpretation order: total_ordering using totalorder_axioms unfolding class.totalorder_def. +interpretation total_ordering UNIV + using totalorder_axioms unfolding class.totalorder_def. subclass porder .. -sublocale order: total_ordering .. +sublocale order: total_ordering UNIV + rewrites "\x. x \ UNIV \ True" + and "\X. X \ UNIV \ True" + and "\r. r \ UNIV \ r" + and "\P. True \ P \ P" + and "Ball UNIV \ All" + and "Bex UNIV \ Ex" + and "sympartp (\)\<^sup>- \ sympartp (\)" + and "\P1. (True \ PROP P1) \ PROP P1" + and "\P1. (True \ P1) \ Trueprop P1" + and "\P1 P2. (True \ PROP P1 \ PROP P2) \ (PROP P1 \ PROP P2)" + apply unfold_locales by (auto simp:atomize_eq) end text \Isabelle/HOL's @{class preorder} belongs to @{class qorder}, but not vice versa.\ subclass (in preorder) qorder apply unfold_locales - apply (fact order_refl) + using order_refl apply assumption apply simp - apply (fact le_less_trans) - apply (fact less_le_trans) - apply (fact less_imp_le) - apply (fact order_trans) + using le_less_trans apply assumption + using less_le_trans apply assumption + using less_imp_le apply assumption + using order_trans apply assumption done subclass (in order) porder by (unfold_locales, auto) -subclass (in wellorder) wf_qorder by (unfold_locales, fact less_induct) +subclass (in wellorder) wf_qorder + apply (unfold_locales) + using less_induct by auto text \Isabelle/HOL's @{class linorder} is equivalent to our locale @{locale strict_total_ordering}.\ context linorder begin -interpretation order: strict_total_ordering by (unfold_locales, auto) +interpretation strict_total_ordering UNIV + apply unfold_locales by auto subclass totalorder .. -sublocale order: strict_total_ordering .. +sublocale order: strict_total_ordering UNIV + rewrites "\x. x \ UNIV \ True" + and "\X. X \ UNIV \ True" + and "\r. r \ UNIV \ r" + and "\P. True \ P \ P" + and "Ball UNIV \ All" + and "Bex UNIV \ Ex" + and "sympartp (\)\<^sup>- \ sympartp (\)" + and "\P1. (True \ PROP P1) \ PROP P1" + and "\P1. (True \ P1) \ Trueprop P1" + and "\P1 P2. (True \ PROP P1 \ PROP P2) \ (PROP P1 \ PROP P2)" + apply unfold_locales by (auto simp:atomize_eq) end text \Tests: facts should be available in the most general classes.\ thm order.strict.trans[where 'a="'a::compat"] thm order.extreme_bound_quasi_const[where 'a="'a::attractive_order"] thm order.extreme_bound_singleton_eq[where 'a="'a::psorder"] thm order.trans[where 'a="'a::qorder"] thm order.comparable_cases[where 'a="'a::totalorder"] thm order.cases[where 'a="'a::linorder"] subsection \Declaring Duals\ -text \At this point, we declare dual as sublocales.\ - -sublocale less_eq_syntax \ dual: less_eq_syntax "(\)\<^sup>-". - -sublocale reflexive \ dual: reflexive "(\)\<^sup>-" by auto - -sublocale attractive \ dual: attractive "(\)\<^sup>-" by unfold_locales - -sublocale irreflexive \ dual: irreflexive "(\)\<^sup>-" by (unfold_locales, auto) - -sublocale transitive \ dual: transitive "(\)\<^sup>-" by (unfold_locales, erule trans) - -sublocale antisymmetric \ dual: antisymmetric "(\)\<^sup>-" by auto - -sublocale asymmetric \ dual: asymmetric "(\)\<^sup>-" by unfold_locales - -sublocale total \ dual: total "(\)\<^sup>-" using total by auto - -sublocale total_reflexive \ dual: total_reflexive "(\)\<^sup>-" by unfold_locales - -sublocale total_irreflexive \ dual: total_irreflexive "(\)\<^sup>-" by unfold_locales - -sublocale pseudo_order \ dual: pseudo_order "(\)\<^sup>-" by unfold_locales - -sublocale quasi_order \ dual: quasi_order "(\)\<^sup>-" by unfold_locales - -sublocale partial_order \ dual: partial_order "(\)\<^sup>-" by unfold_locales - -text \In the following dual sublocale declaration, ``rewrites'' eventually cleans up redundant -facts.\ - -sublocale symmetric \ dual: symmetric "(\)\<^sup>-" rewrites "(\)\<^sup>- = (\)" - using symmetric_axioms by (auto simp: dual_sym) - -sublocale equivalence \ dual: equivalence "(\)\<^sup>-" rewrites "(\)\<^sup>- = (\)" - by (unfold_locales, auto simp: dual_sym sym) - -sublocale total_pseudo_order \ dual: total_pseudo_order "(\)\<^sup>-" by unfold_locales - -sublocale total_quasi_order \ dual: total_quasi_order "(\)\<^sup>-" by unfold_locales - -sublocale compatible_ordering \ dual: compatible_ordering "(\)\<^sup>-" "(\)\<^sup>-" - using weak_strict_trans strict_weak_trans strict_implies_weak by unfold_locales - -sublocale attractive_ordering \ dual: attractive_ordering "(\)\<^sup>-" "(\)\<^sup>-" by unfold_locales - -sublocale pseudo_ordering \ dual: pseudo_ordering "(\)\<^sup>-" "(\)\<^sup>-" by unfold_locales - -sublocale quasi_ordering \ dual: quasi_ordering "(\)\<^sup>-" "(\)\<^sup>-" by unfold_locales - -sublocale partial_ordering \ dual: partial_ordering "(\)\<^sup>-" "(\)\<^sup>-" by unfold_locales - -sublocale total_ordering \ dual: total_ordering "(\)\<^sup>-" "(\)\<^sup>-" by unfold_locales - +sublocale reflexive \ sym: reflexive A "sympartp (\)" + rewrites "sympartp (\)\<^sup>- \ sympartp (\)" + and "\r. sympartp (sympartp r) \ sympartp r" + and "\r. sympartp r \ A \ sympartp (r \ A)" + by (auto 0 4 simp:atomize_eq) + +sublocale quasi_ordered_set \ sym: quasi_ordered_set A "sympartp (\)" + rewrites "sympartp (\)\<^sup>- = sympartp (\)" + and "sympartp (sympartp (\)) = sympartp (\)" + apply unfold_locales by (auto 0 4 dest: trans) + +text \At this point, we declare dual as sublocales. +In the following, ``rewrites'' eventually cleans up redundant facts.\ + +sublocale reflexive \ dual: reflexive A "(\)\<^sup>-" + rewrites "sympartp (\)\<^sup>- \ sympartp (\)" + and "\r. sympartp (r \ A) \ sympartp r \ A" + and "(\)\<^sup>- \ A \ ((\) \ A)\<^sup>-" + by (auto simp: atomize_eq) + +context attractive begin + +interpretation less_eq_notations. + +sublocale dual: attractive A "(\)" + rewrites "sympartp (\) = (\)" + and "equivpartp (\) \ (\)" + and "\r. sympartp (r \ A) \ sympartp r \ A" + and "\r. sympartp (sympartp r) \ sympartp r" + and "(\)\<^sup>- \ A \ ((\) \ A)\<^sup>-" + apply unfold_locales by (auto intro!: ext dest: attract dual.attract simp: atomize_eq) + +end + +context irreflexive begin + +sublocale dual: irreflexive A "(\)\<^sup>-" + rewrites "(\)\<^sup>- \ A \ ((\) \ A)\<^sup>-" + apply unfold_locales by (auto dest: irrefl simp: atomize_eq) + +end + +sublocale transitive \ dual: transitive A "(\)\<^sup>-" + rewrites "(\)\<^sup>- \ A \ ((\) \ A)\<^sup>-" + and "sympartp (\)\<^sup>- = sympartp (\)" + and "asympartp (\)\<^sup>- = (asympartp (\))\<^sup>-" + apply unfold_locales by (auto dest: trans simp: atomize_eq intro!:ext) + +sublocale antisymmetric \ dual: antisymmetric A "(\)\<^sup>-" + rewrites "(\)\<^sup>- \ A \ ((\) \ A)\<^sup>-" + and "sympartp (\)\<^sup>- = sympartp (\)" + by (auto dest: antisym simp: atomize_eq) + +sublocale semiconnex \ dual: semiconnex A "(\)\<^sup>-" + rewrites "sympartp (\)\<^sup>- = sympartp (\)" + using semiconnex by auto + +sublocale connex \ dual: connex A "(\)\<^sup>-" + rewrites "sympartp (\)\<^sup>- = sympartp (\)" + by (auto intro!: chainI dest:comparable) + +sublocale semiconnex_irreflexive \ dual: semiconnex_irreflexive A "(\)\<^sup>-" + rewrites "sympartp (\)\<^sup>- = sympartp (\)" + by unfold_locales auto + +sublocale pseudo_ordered_set \ dual: pseudo_ordered_set A "(\)\<^sup>-" + rewrites "sympartp (\)\<^sup>- = sympartp (\)" + by unfold_locales (auto 0 4) + +sublocale quasi_ordered_set \ dual: quasi_ordered_set A "(\)\<^sup>-" + rewrites "sympartp (\)\<^sup>- = sympartp (\)" + by unfold_locales auto + +sublocale partially_ordered_set \ dual: partially_ordered_set A "(\)\<^sup>-" + rewrites "sympartp (\)\<^sup>- = sympartp (\)" + by unfold_locales (auto 0 4) + +sublocale total_pseudo_ordered_set \ dual: total_pseudo_ordered_set A "(\)\<^sup>-" + rewrites "sympartp (\)\<^sup>- = sympartp (\)" + by unfold_locales (auto 0 4) + +sublocale total_quasi_ordered_set \ dual: total_quasi_ordered_set A "(\)\<^sup>-" + rewrites "sympartp (\)\<^sup>- = sympartp (\)" + by unfold_locales auto + +sublocale compatible_ordering \ dual: compatible_ordering A "(\)\<^sup>-" "(\)\<^sup>-" + rewrites "sympartp (\)\<^sup>- = sympartp (\)" + apply unfold_locales + by (auto dest: compat_left compat_right strict_implies_weak) + +sublocale attractive_ordering \ dual: attractive_ordering A "(\)\<^sup>-" "(\)\<^sup>-" + rewrites "sympartp (\)\<^sup>- = sympartp (\)" + by unfold_locales auto + +sublocale pseudo_ordering \ dual: pseudo_ordering A "(\)\<^sup>-" "(\)\<^sup>-" + rewrites "sympartp (\)\<^sup>- = sympartp (\)" + by unfold_locales (auto 0 4) + +sublocale quasi_ordering \ dual: quasi_ordering A "(\)\<^sup>-" "(\)\<^sup>-" + rewrites "sympartp (\)\<^sup>- = sympartp (\)" + by unfold_locales auto + +sublocale partial_ordering \ dual: partial_ordering A "(\)\<^sup>-" "(\)\<^sup>-" + rewrites "sympartp (\)\<^sup>- = sympartp (\)" + by unfold_locales (auto 0 4) + +sublocale total_ordering \ dual: total_ordering A "(\)\<^sup>-" "(\)\<^sup>-" + rewrites "sympartp (\)\<^sup>- = sympartp (\)" + by unfold_locales (auto 0 4) lemma(in antisymmetric) monotone_extreme_imp_extreme_bound_iff: fixes ir (infix "\" 50) - assumes "monotone (\) (\) f" and i: "extreme (\) C i" - shows "extreme_bound (\) (f ` C) x \ f i = x" + assumes "f ` C \ A" and "monotone_on C (\) (\) f" and i: "extreme C (\) i" + shows "extreme_bound A (\) (f ` C) x \ f i = x" using dual.extreme_unique monotone_extreme_extreme_boundI[OF assms] by auto subsection \Instantiations\ text \Finally, we instantiate our classes for sanity check.\ instance nat :: linorder .. text \Pointwise ordering of functions are compatible only if the weak part is transitive.\ instance "fun" :: (type,qorder) compat proof (intro_classes, unfold_locales) note [simp] = le_fun_def less_fun_def fix f g h :: "'a \ 'b" { assume fg: "f \ g" and gh: "g < h" show "f < h" proof (unfold less_fun_def, intro conjI le_funI notI) from fg have "f x \ g x" for x by auto also from gh have "g x \ h x" for x by auto - finally show "f x \ h x" for x. + finally (order.trans) show "f x \ h x" for x. assume hf: "h \ f" then have "h x \ f x" for x by auto also from fg have "f x \ g x" for x by auto finally have "h \ g" by auto with gh show False by auto qed } { assume fg: "f < g" and gh: "g \ h" show "f < h" proof (unfold less_fun_def, intro conjI le_funI notI) from fg have "f x \ g x" for x by auto also from gh have "g x \ h x" for x by auto finally show "f x \ h x" for x. - assume hf: "h \ f" + from gh have "g x \ h x" for x by auto + also assume hf: "h \ f" then have "h x \ f x" for x by auto - also from gh have "g x \ h x" for x by auto finally have "g \ f" by auto with fg show False by auto qed } show "f < g \ f \ g" by auto show "\f < f" by auto show "f \ f" by auto qed instance "fun" :: (type,qorder) qorder - by (intro_classes, unfold_locales, auto simp: le_fun_def dest: order.trans) + apply intro_classes + apply unfold_locales + by (auto simp: le_fun_def dest: order.trans) instance "fun" :: (type,porder) porder - by (intro_classes, unfold_locales, auto simp: less_fun_def le_fun_def) + apply intro_classes + apply unfold_locales +proof (intro ext) + fix f g :: "'a \ 'b" and x :: 'a + assume fg: "f \ g" and gf: "g \ f" + then have "f x \ g x" and "g x \ f x" by (auto elim: le_funE) + from order.antisym[OF this] show "f x = g x" by auto +qed end diff --git a/thys/Complete_Non_Orders/Complete_Relations.thy b/thys/Complete_Non_Orders/Complete_Relations.thy --- a/thys/Complete_Non_Orders/Complete_Relations.thy +++ b/thys/Complete_Non_Orders/Complete_Relations.thy @@ -1,737 +1,590 @@ (* -Author: Akihisa Yamada (2018-2019) +Author: Akihisa Yamada (2018-2021) License: LGPL (see file COPYING.LESSER) *) section \ Completeness of Relations \ text \Here we formalize various order-theoretic completeness conditions.\ theory Complete_Relations - imports HOL.Real Binary_Relations + imports Binary_Relations begin subsection \Completeness Conditions\ -text \Order-theoretic completeness demands certain subsets of elements to admit suprema or infima. +text \Order-theoretic completeness demands certain subsets of elements to admit suprema or infima.\ -A related set $\tp{A,\SLE}$ is called \emph{bounded} if there is a ``top'' element $\top \in A$, +definition complete ("_-complete"[999]1000) where + "CC-complete A r \ \X \ A. X \ CC \ (\s. extreme_bound A r X s)" + +lemmas completeI = complete_def[unfolded atomize_eq, THEN iffD2, rule_format] +lemmas completeD = complete_def[unfolded atomize_eq, THEN iffD1, rule_format] + +lemma complete_cmono: "CC \ DD \ DD-complete \ CC-complete" + by (force simp: complete_def) + +lemma complete_empty[simp]: "CC-complete {} r \ {} \ CC" by (auto simp: complete_def) + +text \ +A related set $\tp{A,\SLE}$ is called \emph{topped} if there is a ``top'' element $\top \in A$, a greatest element in $A$. Note that there might be multiple tops if $(\SLE)$ is not antisymmetric.\ -locale bounded = less_eq_syntax + assumes bounded: "\t. \x. x \ t" -begin - -lemma ex_bound[intro!]: "Ex (bound (\) X)" using bounded by auto +definition "extremed A r \ \e. extreme A r e" -lemma ex_extreme_UNIV[intro!]: "Ex (extreme (\) UNIV)" using bounded by auto - -lemma UNIV_complete[intro!]: "Ex (extreme_bound (\) UNIV)" using bounded by blast - -lemma dual_empty_complete[intro!]: "Ex (extreme_bound (\)\<^sup>- {})" by (auto simp: bound_empty) - -end +lemma extremed_imp_ex_bound: "extremed A r \ X \ A \ \b \ A. bound X r b" + by (auto simp: extremed_def) context fixes less_eq :: "'a \ 'a \ bool" (infix "\" 50) begin -lemma bounded_iff_extreme_UNIV: "bounded (\) \ Ex (extreme (\) UNIV)" - by (auto simp:bounded_def) - -text\Boundedness can be also seen as a completeness condition, +text\Toppedness can be also seen as a completeness condition, since it is equivalent to saying that the universe has a supremum.\ -lemma bounded_iff_UNIV_complete: "bounded (\) \ Ex (extreme_bound (\) UNIV)" - by (unfold bounded_def, blast) +lemma extremed_iff_UNIV_complete: "extremed A (\) \ {A}-complete A (\)" (is "?l \ ?r") +proof + assume ?l + then obtain e where "extreme A (\) e" by (auto simp: extremed_def) + then have "extreme_bound A (\) A e" by auto + then show ?r by (auto intro!: completeI) +next + assume ?r + from completeD[OF this] obtain s where "extreme_bound A (\) A s" by auto + then have "extreme A (\) s" by auto + then show ?l by (auto simp: extremed_def) +qed -text \The dual notion of bounded is called ``pointed'', equivalently ensuring a supremum +text \The dual notion of topped is called ``pointed'', equivalently ensuring a supremum of the empty set.\ -lemma pointed_iff_empty_complete: "bounded (\) \ Ex (extreme_bound (\)\<^sup>- {})" - by (auto simp:bounded_def) +lemma pointed_iff_empty_complete: "extremed A (\) \ {{}}-complete A (\)\<^sup>-" + by (auto simp: complete_def extremed_def) end - text \One of the most well-studied notion of completeness would be the semilattice condition: every pair of elements $x$ and $y$ has a supremum $x \sqcup y$ (not necessarily unique if the underlying relation is not antisymmetric).\ -locale pair_complete = less_eq_syntax + - assumes pair_complete: "Ex (extreme_bound (\) {x,y})" +definition "pair_complete \ {{x,y} |. x y :: 'a}-complete" + +lemma pair_completeI: + assumes "\x y. x \ A \ y \ A \ \s. extreme_bound A r {x,y} s" + shows "pair_complete A r" + using assms by (auto simp: pair_complete_def complete_def) + +lemma pair_completeD: + assumes "pair_complete A r" + shows "x \ A \ y \ A \ \s. extreme_bound A r {x,y} s" + by (intro completeD[OF assms[unfolded pair_complete_def]], auto) + + +context + fixes less_eq :: "'a \ 'a \ bool" (infix "\" 50) begin -lemma directed_UNIV[intro!]: "directed (\) UNIV" +lemma pair_complete_imp_directed: + assumes comp: "pair_complete A (\)" shows "directed A (\)" proof fix x y :: 'a - from pair_complete[of x y] show "\z \ UNIV. x \ z \ y \ z" by auto + assume "x \ A" "y \ A" + with pair_completeD[OF comp this] show "\z \ A. x \ z \ y \ z" by auto qed end -sublocale total_reflexive \ pair_complete -proof (unfold_locales) +lemma (in connex) pair_complete: "pair_complete A (\)" +proof (safe intro!: pair_completeI) fix x y - show "Ex (extreme_bound (\) {x, y})" by (cases x y rule:comparable_cases, auto) + assume x: "x \ A" and y: "y \ A" + then show "\s. extreme_bound A (\) {x, y} s" + proof (cases rule:comparable_cases) + case le + with x y show ?thesis by (auto intro!: exI[of _ y]) + next + case ge + with x y show ?thesis by (auto intro!: exI[of _ x]) + qed qed text \The next one assumes that every nonempty finite set has a supremum.\ -locale finite_complete = less_eq_syntax + - assumes finite_nonempty_complete: "finite X \ X \ {} \ Ex (extreme_bound (\) X)" +abbreviation "finite_complete \ {X. finite X \ X \ {}}-complete" -sublocale finite_complete \ pair_complete - by (unfold_locales, intro finite_nonempty_complete, auto) +lemma finite_complete_le_pair_complete: "finite_complete \ pair_complete" + by (unfold pair_complete_def, rule complete_cmono, auto) text \The next one assumes that every nonempty bounded set has a supremum. It is also called the Dedekind completeness.\ -locale conditionally_complete = less_eq_syntax + - assumes bounded_nonempty_complete: - "Ex (bound (\) X) \ X \ {} \ Ex (extreme_bound (\) X)" -begin +abbreviation "conditionally_complete A r \ {X. \b \ A. bound X r b \ X \ {}}-complete A r" -lemma bounded_nonemptyE[elim!]: - assumes "Ex (bound (\) X)" and "X \ {}" - and "Ex (extreme_bound (\) X) \ X \ {} \ thesis" - shows thesis - using assms bounded_nonempty_complete by auto - -lemma nonempty_imp_complete_iff_bounded: - assumes "X \ {}" shows "Ex (extreme_bound (\) X) \ Ex (bound (\) X)" - using assms by (auto intro: bounded_nonempty_complete) - -end +lemma conditionally_complete_imp_nonempty_imp_ex_extreme_bound_iff_ex_bound: + assumes comp: "conditionally_complete A r" + assumes "X \ A" and "X \ {}" + shows "(\s. extreme_bound A r X s) \ (\b\A. bound X r b)" + using assms by (auto 0 4 intro!:completeD[OF comp]) text \The $\omega$-completeness condition demands a supremum for an $\omega$-chain, $a_1 \sqsubseteq a_2 \sqsubseteq \dots$. We model $\omega$-chain as the range of a monotone map $f : i \mapsto a_i$.\ -locale omega_complete = less_eq_syntax + - assumes monotone_seq_complete: - "\f :: nat \ 'a. monotone (\) (\) f \ Ex (extreme_bound (\) (range f))" - -locale chain_complete = less_eq_syntax + - assumes chain_nonempty_complete: "chain (\) X \ X \ {} \ Ex (extreme_bound (\) X)" -begin +definition "omega_complete A r \ {range f | f :: nat \ 'a. monotone (\) r f}-complete A r" -lemma monotone_chain_complete: - assumes C0: "C \ {}" and chain: "chain r C" and mono: "monotone r (\) f" - shows "Ex (extreme_bound (\) (f ` C))" - apply (rule chain_nonempty_complete[OF monotone_chain_image[OF mono chain]]) - using C0 by auto - -end - -sublocale chain_complete \ omega_complete - by (unfold_locales, rule monotone_chain_complete, auto intro:chainI) +lemma (in transitive) local_chain: + assumes CA: "range C \ A" + shows "(\i::nat. C i \ C (Suc i)) \ monotone (<) (\) C" +proof (intro iffI allI monotoneI) + fix i j :: nat + assume loc: "\i. C i \ C (Suc i)" and ij: "i < j" + have "C i \ C (i+k+1)" for k + proof (induct k) + case 0 + from loc show ?case by auto + next + case (Suc k) + also have "C (i+k+1) \ C (i+k+Suc 1)" using loc by auto + finally show ?case using CA by auto + qed + from this[of "j-i-1"] ij show "C i \ C j" by auto +next + fix i + assume "monotone (<) (\) C" + then show "C i \ C (Suc i)" by (auto dest: monotoneD) +qed text\\emph{Directed completeness} is an important notion in domain theory~\cite{abramski94}, asserting that every nonempty directed set has a supremum. Here, a set $X$ is \emph{directed} if any pair of two elements in $X$ has a bound in $X$.\ -locale directed_complete = less_eq_syntax + - assumes directed_nonempty_complete: "directed (\) X \ X \ {} \ Ex (extreme_bound (\) X)" -begin +definition "directed_complete A r \ {X. directed X r \ X \ {}}-complete A r" lemma monotone_directed_complete: - assumes dir: "directed r C" and c0: "C \ {}" and mono: "monotone r (\) f" - shows "Ex (extreme_bound (\) (f ` C))" - apply (rule directed_nonempty_complete[OF monotone_directed_image[OF mono dir]]) - using c0 by auto - -end - -sublocale directed_complete \ chain_complete - by (unfold_locales, intro directed_nonempty_complete, auto dest: chain_imp_directed) + assumes comp: "directed_complete A r" + assumes fI: "f ` I \ A" and dir: "directed I ri" and I0: "I \ {}" and mono: "monotone_on I ri r f" + shows "\s. extreme_bound A r (f ` I) s" + apply (rule completeD[OF comp[unfolded directed_complete_def], OF fI]) + using monotone_directed_image[OF mono dir] I0 by auto text \The next one is quite complete, only the empty set may fail to have a supremum. The terminology follows \cite{Bergman2015}, although there it is defined more generally depending on a cardinal $\alpha$ such that a nonempty set $X$ of cardinality below $\alpha$ has a supremum.\ -locale semicomplete = less_eq_syntax + - assumes nonempty_complete: "X \ {} \ Ex (extreme_bound (\) X)" +abbreviation "semicomplete \ {X. X \ {}}-complete" -sublocale semicomplete \ conditionally_complete + finite_complete + directed_complete - by (unfold_locales, auto intro!: nonempty_complete) +lemma semicomplete_nonempty_imp_extremed: + "semicomplete A r \ A \ {} \ extremed A r" + unfolding extremed_iff_UNIV_complete + using complete_cmono[of "{A}" "{X. X \ {}}"] + by auto -sublocale semicomplete \ bounded - unfolding bounded_iff_UNIV_complete using nonempty_complete[of UNIV] by auto +lemma connex_dual_semicomplete: "semicomplete {C. connex C r} (\)" +proof (intro completeI, elim CollectE) + fix X + assume "X \ {C. connex C r}" and "X \ {}" + then have "connex (\X) r" by (auto simp: connex_def) + then have "extreme_bound {C. connex C r} (\) X (\ X)" by auto + then show "\S. extreme_bound {C. connex C r} (\) X S" by auto +qed subsection \Pointed Ones\ -text \The term `pointed' refers to the dual notion of boundedness, i.e., there is a global least element. +text \The term `pointed' refers to the dual notion of toppedness, i.e., there is a global least element. This serves as the supremum of the empty set.\ -locale pointed_chain_complete = chain_complete + dual: bounded "(\)\<^sup>-" -begin - -lemma chain_complete: "chain (\) X \ Ex (extreme_bound (\) X)" - by (cases "X = {}", auto intro:chain_nonempty_complete) - -end - -lemma pointed_chain_complete_def': - fixes less_eq (infix "\" 50) - shows "pointed_chain_complete (\) \ \X. chain (\) X \ Ex (extreme_bound (\) X)" (is "?l \ ?r") - apply (unfold atomize_eq, intro iffI) - apply (force intro: pointed_chain_complete.chain_complete) - by (unfold_locales, auto intro!: chain_empty simp: pointed_iff_empty_complete[unfolded bounded_def]) +lemma complete_union: "(CC \ CC')-complete A r \ CC-complete A r \ CC'-complete A r" + by (auto simp: complete_def) -locale pointed_directed_complete = directed_complete + dual: bounded "(\)\<^sup>-" -begin - -lemma directed_complete: "directed (\) X \ Ex (extreme_bound (\) X)" - by (cases "X = {}", auto intro: directed_nonempty_complete) - -sublocale pointed_chain_complete .. - -end - -lemma pointed_directed_complete_def': - fixes less_eq (infix "\" 50) - shows "pointed_directed_complete (\) \ \X. directed (\) X \ Ex (extreme_bound (\) X)" - apply (unfold atomize_eq, intro iffI) - apply (force intro: pointed_directed_complete.directed_complete) - by (unfold_locales, auto simp: pointed_iff_empty_complete[unfolded bounded_def]) +lemma pointed_directed_complete: + "{X. directed X r}-complete A r \ directed_complete A r \ extremed A r\<^sup>-" +proof- + have [simp]: "{X. directed X r \ X \ {} \ X = {}} = {X. directed X r}" by auto + show ?thesis + by (auto simp: directed_complete_def pointed_iff_empty_complete complete_union[symmetric] Un_def) +qed text \``Bounded complete'' refers to pointed conditional complete, -but this notion is just the dual of semicompleteness. We prove this later. - -Following is the strongest completeness that requires any subset of elements to have suprema -and infima.\ +but this notion is just the dual of semicompleteness. We prove this later.\ -locale complete = less_eq_syntax + assumes complete: "Ex (extreme_bound (\) X)" -begin - -sublocale semicomplete + pointed_directed_complete - by (auto simp: pointed_directed_complete_def' intro: semicomplete.intro complete) - -end +abbreviation "bounded_complete A r \ {X. \b\A. bound X r b}-complete A r" subsection \Relations between Completeness Conditions\ context fixes less_eq :: "'a \ 'a \ bool" (infix "\" 50) begin -interpretation less_eq_dualize. +interpretation less_eq_notations. text \Pair-completeness implies that the universe is directed. Thus, with directed completeness -implies boundedness.\ +implies toppedness.\ -proposition directed_complete_pair_complete_imp_bounded: - assumes "directed_complete (\)" and "pair_complete (\)" - shows "bounded (\)" +proposition directed_complete_pair_complete_imp_extremed: + assumes dc: "directed_complete A (\)" and pc: "pair_complete A (\)" and A: "A \ {}" + shows "extremed A (\)" proof- - from assms interpret directed_complete + pair_complete by auto - have "Ex (extreme_bound (\) UNIV)" by (rule directed_nonempty_complete, auto) - then obtain t where "extreme_bound (\) UNIV t" by auto - then have "\x. x \ t" by auto - then show ?thesis by (unfold_locales, auto) + have "\s. extreme_bound A (\) A s" + apply (rule completeD[OF dc[unfolded directed_complete_def]]) + using pair_complete_imp_directed[OF pc] A by auto + then obtain t where "extreme_bound A (\) A t" by auto + then have "\x \ A. x \ t" and "t \ A" by auto + then show ?thesis by (auto simp: extremed_def) qed -text \Semicomplete is conditional complete and bounded.\ +text \Semicomplete is conditional complete and topped.\ -proposition semicomplete_iff_conditionally_complete_bounded: - "semicomplete (\) \ conditionally_complete (\) \ bounded (\)" (is "?l \ ?r") -proof - assume ?r - then interpret conditionally_complete "(\)" + bounded "(\)" by auto - show ?l by (unfold_locales, rule bounded_nonempty_complete, auto) +proposition semicomplete_iff_conditionally_complete_extremed: + assumes A: "A \ {}" + shows "semicomplete A (\) \ conditionally_complete A (\) \ extremed A (\)" (is "?l \ ?r") +proof (intro iffI) + assume r: "?r" + then have cc: "conditionally_complete A (\)" and e: "extremed A (\)" by auto + show ?l + proof (intro completeI, unfold mem_Collect_eq) + fix X + assume X: "X \ A" and "X \ {}" + with extremed_imp_ex_bound[OF e X] + show "\s. extreme_bound A (\) X s" by (auto intro!: completeD[OF cc X]) + qed next - assume ?l - then interpret semicomplete. - show ?r by (intro conjI, unfold_locales) + assume l: ?l + with semicomplete_nonempty_imp_extremed[OF l] A + show ?r by (auto intro!: completeI dest: completeD) qed proposition complete_iff_pointed_semicomplete: - "complete (\) \ semicomplete (\) \ bounded (\)" (is "?l \ ?r") -proof - assume "complete (\)" - then interpret complete. - show ?r by (intro conjI, unfold_locales) -next - assume ?r - then interpret semicomplete + bounded "(\)" by auto - show ?l - proof - fix X show "Ex (extreme_bound (\) X)" by (cases "X = {}", auto intro:nonempty_complete) - qed -qed + "UNIV-complete A (\) \ semicomplete A (\) \ extremed A (\)" (is "?l \ ?r") + by (unfold pointed_iff_empty_complete complete_union[symmetric] Un_def, auto) text \Conditional completeness only lacks top and bottom to be complete.\ -proposition complete_iff_conditionally_complete_bounded_pointed: - "complete (\) \ conditionally_complete (\) \ bounded (\) \ bounded (\)" +proposition complete_iff_conditionally_complete_extremed_pointed: + "UNIV-complete A (\) \ conditionally_complete A (\) \ extremed A (\) \ extremed A (\)" unfolding complete_iff_pointed_semicomplete - semicomplete_iff_conditionally_complete_bounded by auto - -end + apply (cases "A = {}") + apply (auto intro!: completeI dest: extremed_imp_ex_bound)[1] + unfolding semicomplete_iff_conditionally_complete_extremed + apply (auto intro:completeI) + done text \If the universe is directed, then every pair is bounded, and thus has a supremum. On the other hand, supremum gives an upper bound, witnessing directedness.\ -proposition (in conditionally_complete) pair_complete_iff_directed: - "pair_complete (\) \ directed (\) UNIV" +proposition conditionally_complete_imp_pair_complete_iff_directed: + assumes comp: "conditionally_complete A (\)" + shows "pair_complete A (\) \ directed A (\)" (is "?l \ ?r") proof(intro iffI) - assume "directed (\) UNIV" - then show "pair_complete (\)" - by (unfold_locales, intro bounded_nonempty_complete, auto elim: directedE) + assume ?r + then show ?l + by (auto intro!: pair_completeI completeD[OF comp] elim: directedE) next - assume "pair_complete (\)" - then interpret pair_complete. - show "directed (\) UNIV" + assume pc: ?l + show ?r proof (intro directedI) - fix x y - from pair_complete obtain z where "extreme_bound (\) {x,y} z" by auto - then show "\z\UNIV. x \ z \ y \ z" by auto + fix x y assume "x \ A" and "y \ A" + with pc obtain z where "extreme_bound A (\) {x,y} z" by (auto dest: pair_completeD) + then show "\z\A. x \ z \ y \ z" by auto qed qed +end + +text \Following is a new generalization of (weak) chain-completeness:\ +abbreviation "well_complete A r \ {X. well_related_set X r}-complete A r" + +subsection \Duality of Completeness Conditions\ + +text \Conditional completeness is symmetric.\ + +context fixes less_eq :: "'a \ 'a \ bool" (infix "\" 50) +begin + +interpretation less_eq_notations. + +lemma conditionally_complete_dual: + assumes comp: "conditionally_complete A (\)" shows "conditionally_complete A (\)" +proof (intro completeI, elim CollectE) + fix X assume XA: "X \ A" + define B where [simp]: "B \ {b\A. bound X (\) b}" + assume bound: "\b\A. bound X (\) b \ X \ {}" + with in_mono[OF XA] have B: "B \ A" and "\b \ A. bound B (\) b" and "B \ {}" by auto + from comp[THEN completeD, OF B] this + obtain s where "s \ A" and "extreme_bound A (\) B s" by auto + with in_mono[OF XA] show "\s. extreme_bound A (\) X s" by (intro exI[of _ s] extremeI, auto) +qed + +text \Full completeness is symmetric.\ + +lemma complete_dual: + "UNIV-complete A (\) \ UNIV-complete A (\)" + apply (unfold complete_iff_conditionally_complete_extremed_pointed) + using conditionally_complete_dual by auto + +text \Now we show that bounded completeness is the dual of semicompleteness.\ + +lemma pointed_conditionally_complete_iff_bounded_complete: + assumes A: "A \ {}" + shows "conditionally_complete A (\) \ extremed A (\) \ bounded_complete A (\)" + apply (unfold pointed_iff_empty_complete) + apply (fold complete_union) + apply (unfold Un_def) + apply (rule arg_cong[of _ _ "\CC. CC-complete A (\)"]) + using A by auto + +proposition bounded_complete_iff_dual_semicomplete: + "bounded_complete A (\) \ semicomplete A (\)" +proof (cases "A = {}") + case True + then show ?thesis by auto +next + case False + then show ?thesis + apply (fold pointed_conditionally_complete_iff_bounded_complete[OF False]) + apply (unfold semicomplete_iff_conditionally_complete_extremed) + using Complete_Relations.conditionally_complete_dual by auto +qed + +end + +lemmas connex_bounded_complete = connex_dual_semicomplete[folded bounded_complete_iff_dual_semicomplete] subsection \Completeness Results Requiring Order-Like Properties\ text \Above results hold without any assumption on the relation. This part demands some order-like properties.\ text \It is well known that in a semilattice, i.e., a pair-complete partial order, every finite nonempty subset of elements has a supremum. We prove the result assuming transitivity, but only that.\ -locale trans_semilattice = transitive + pair_complete - -sublocale trans_semilattice \ finite_complete - apply (unfold_locales) - subgoal for X - proof (induct X rule:finite_induct) - case empty +lemma (in transitive) pair_complete_iff_finite_complete: + "pair_complete A (\) \ finite_complete A (\)" (is "?l \ ?r") +proof (intro iffI completeI, elim CollectE conjE) + fix X + assume pc: ?l + show "finite X \ X \ A \ X \ {} \ Ex (extreme_bound A (\) X)" + proof (induct X rule: finite_induct) + case empty then show ?case by auto next case (insert x X) + then have x: "x \ A" and X: "X \ A" by auto show ?case proof (cases "X = {}") case True - obtain x' where "extreme_bound (\) {x,x} x'" using pair_complete[of x x] by auto + obtain x' where "extreme_bound A (\) {x,x} x'" using pc[THEN pair_completeD, OF x x] by auto with True show ?thesis by (auto intro!: exI[of _ x']) next case False - with insert obtain b where b: "extreme_bound (\) X b" by auto - from pair_complete obtain c where c: "extreme_bound (\) {x,b} c" by auto + with insert obtain b where b: "extreme_bound A (\) X b" by auto + with pc[THEN pair_completeD] x obtain c where c: "extreme_bound A (\) {x,b} c" by auto + from c have cA: "c \ A" and xc: "x \ c" and bc: "b \ c" by auto + from b have bA: "b \ A" and bX: "bound X (\) b" by auto show ?thesis proof (intro exI extreme_boundI) - from c have "x \ c" and "b \ c" by auto - with b show "xb \ insert x X \ xb \ c" for xb by (auto dest: trans) - fix d assume "bound (\) (insert x X) d" - with b have "bound (\) {x,b} d" by auto - with c show "c \ d" by auto - qed + fix xb assume xb: "xb \ insert x X" + from bound_trans[OF bX bc X bA cA] have "bound X (\) c". + with xb xc show "xb \ c" by auto + next + fix d assume "bound (insert x X) (\) d" and dA: "d \ A" + with b have "bound {x,b} (\) d" by auto + with c show "c \ d" using dA by auto + qed (fact cA) qed qed -done +qed (insert finite_complete_le_pair_complete, auto) text \Gierz et al.~\cite{gierz03} showed that a directed complete partial order is semicomplete if and only if it is also a semilattice. We generalize the claim so that the underlying relation is only transitive.\ proposition(in transitive) semicomplete_iff_directed_complete_pair_complete: - "semicomplete (\) \ directed_complete (\) \ pair_complete (\)" (is "?l \ ?r") -proof (intro iffI semicomplete.intro) - assume ?l - then interpret semicomplete. - show ?r by (intro conjI, unfold_locales) + "semicomplete A (\) \ directed_complete A (\) \ pair_complete A (\)" (is "?l \ ?r") +proof (intro iffI) + assume l: ?l + then show ?r by (auto simp: directed_complete_def intro!: completeI pair_completeI completeD[OF l]) next assume ?r - then interpret directed_complete + pair_complete by auto - interpret trans_semilattice .. - fix X :: "'a set" - have 1: "directed (\) {x. \Y \ X. finite Y \ Y \ {} \ extreme_bound (\) Y x}" (is "directed _ ?B") - proof (intro directedI) - fix a b assume a: "a \ ?B" and b: "b \ ?B" - from a obtain A where A: "extreme_bound (\) A a" "finite A" "A \ {}" "A \ X" by auto - from b obtain B where B: "extreme_bound (\) B b" "finite B" "B \ {}" "B \ X" by auto - from A B have AB: "finite (A \ B)" "A \ B \ {}" "A \ B \ X" by auto - with finite_nonempty_complete have "Ex (extreme_bound (\) (A \ B))" by auto - then obtain c where c: "extreme_bound (\) (A \ B) c" by auto - show "\c \ ?B. a \ c \ b \ c" - proof (intro bexI conjI) - from A B c show "a \ c" and "b \ c" by (auto simp: extreme_bound_iff) - from AB c show "c \ ?B" by (auto intro!: exI[of _ "A \ B"]) + then have dc: "directed_complete A (\)" and pc: "pair_complete A (\)" by auto + with pair_complete_iff_finite_complete have fc: "finite_complete A (\)" by auto + show ?l + proof (intro completeI, elim CollectE) + fix X assume XA: "X \ A" + have 1: "directed {x. \Y \ X. finite Y \ Y \ {} \ extreme_bound A (\) Y x} (\)" (is "directed ?B _") + proof (intro directedI) + fix a b assume a: "a \ ?B" and b: "b \ ?B" + from a obtain Y where Y: "extreme_bound A (\) Y a" "finite Y" "Y \ {}" "Y \ X" by auto + from b obtain B where B: "extreme_bound A (\) B b" "finite B" "B \ {}" "B \ X" by auto + from XA Y B have AB: "Y \ A" "B \ A" "finite (Y \ B)" "Y \ B \ {}" "Y \ B \ X" by auto + with fc[THEN completeD] have "Ex (extreme_bound A (\) (Y \ B))" by auto + then obtain c where c: "extreme_bound A (\) (Y \ B) c" by auto + show "\c \ ?B. a \ c \ b \ c" + proof (intro bexI conjI) + from Y B c show "a \ c" and "b \ c" by (auto simp: extreme_bound_iff) + from AB c show "c \ ?B" by (auto intro!: exI[of _ "Y \ B"]) + qed qed - qed - assume "X \ {}" - then obtain x where xX: "x \ X" by auto - from finite_nonempty_complete[of "{x}"] - obtain x' where "extreme_bound (\) {x} x'" by auto - with xX have x'B: "x' \ ?B" by (auto intro!: exI[of _ "{x}"] extreme_boundI) - then have 2: "?B \ {}" by auto - from directed_nonempty_complete[OF 1 2] - obtain b where b: "extreme_bound (\) ?B b" by auto - show "Ex (extreme_bound (\) X)" - proof (intro exI extreme_boundI UNIV_I) - fix x - assume xX: "x \ X" - from finite_nonempty_complete[of "{x}"] - obtain c where c: "extreme_bound (\) {x} c" by auto - then have xc: "x \ c" by auto - from c xX have cB: "c \ ?B" by (auto intro!: exI[of _ "{x}"] extreme_boundI) - with b have cb: "c \ b" by auto - from xc cb show "x \ b" by (rule trans) text\ Here transitivity is needed. \ - next - fix x - assume Xx: "bound (\) X x" - have "bound (\) ?B x" - proof (intro boundI UNIV_I, clarify) - fix c Y - assume "finite Y" and YX: "Y \ X" and "Y \ {}" and c: "extreme_bound (\) Y c" - from YX Xx have "bound (\) Y x" by auto - with c show "c \ x" by auto - qed - with b show "b \ x" by auto + have B: "?B \ A" by auto + assume "X \ {}" + then obtain x where xX: "x \ X" by auto + with fc[THEN completeD, of "{x}"] XA + obtain x' where "extreme_bound A (\) {x} x'" by auto + with xX have x'B: "x' \ ?B" by (auto intro!: exI[of _ "{x}"] extreme_boundI) + then have 2: "?B \ {}" by auto + from dc[unfolded directed_complete_def, THEN completeD, of ?B] 1 2 + obtain b where b: "extreme_bound A (\) ?B b" by auto + then have bA: "b \ A" by auto + show "Ex (extreme_bound A (\) X)" + proof (intro exI extreme_boundI UNIV_I) + fix x + assume xX: "x \ X" + with XA fc[THEN completeD, of "{x}"] + obtain c where c: "extreme_bound A (\) {x} c" by auto + then have cA: "c \ A" and xc: "x \ c" by auto + from c xX have cB: "c \ ?B" by (auto intro!: exI[of _ "{x}"] extreme_boundI) + with b have bA: "b \ A" and cb: "c \ b" by auto + from xX XA cA bA trans[OF xc cb] + show "x \ b" by auto text\ Here transitivity is needed. \ + next + fix x + assume xA: "x \ A" and Xx: "bound X (\) x" + have "bound ?B (\) x" + proof (intro boundI UNIV_I, clarify) + fix c Y + assume "finite Y" and YX: "Y \ X" and "Y \ {}" and c: "extreme_bound A (\) Y c" + from YX Xx have "bound Y (\) x" by auto + with c xA show "c \ x" by auto + qed + with b xA show "b \ x" by auto + qed (fact bA) qed qed text\The last argument in the above proof requires transitivity, but if we had reflexivity then $x$ itself is a supremum of $\set{x}$ (see @{thm reflexive.extreme_bound_singleton}) and so $x \SLE s$ would be immediate. Thus we can replace transitivity by reflexivity, but then pair-completeness does not imply finite completeness. We obtain the following result.\ proposition (in reflexive) semicomplete_iff_directed_complete_finite_complete: - "semicomplete (\) \ directed_complete (\) \ finite_complete (\)" (is "?l \ ?r") -proof (intro iffI semicomplete.intro) - assume ?l - then interpret semicomplete. - show ?r by (safe, unfold_locales) + "semicomplete A (\) \ directed_complete A (\) \ finite_complete A (\)" (is "?l \ ?r") +proof (intro iffI) + assume l: ?l + then show ?r by (auto simp: directed_complete_def intro!: completeI pair_completeI completeD[OF l]) next assume ?r - then interpret directed_complete + finite_complete by auto - fix X :: "'a set" - have 1: "directed (\) {x. \Y \ X. finite Y \ Y \ {} \ extreme_bound (\) Y x}" (is "directed _ ?B") - proof (intro directedI) - fix a b assume a: "a \ ?B" and b: "b \ ?B" - from a obtain A where A: "extreme_bound (\) A a" "finite A" "A \ {}" "A \ X" by auto - from b obtain B where B: "extreme_bound (\) B b" "finite B" "B \ {}" "B \ X" by auto - from A B have AB: "finite (A \ B)" "A \ B \ {}" "A \ B \ X" by auto - with finite_nonempty_complete have "Ex (extreme_bound (\) (A \ B))" by auto - then obtain c where c: "extreme_bound (\) (A \ B) c" by auto - show "\c \ ?B. a \ c \ b \ c" - proof (intro bexI conjI) - from A B c show "a \ c" and "b \ c" by (auto simp: extreme_bound_iff) - from AB c show "c \ ?B" by (auto intro!: exI[of _ "A \ B"]) + then have dc: "directed_complete A (\)" and fc: "finite_complete A (\)" by auto + show ?l + proof (intro completeI, elim CollectE) + fix X assume XA: "X \ A" + have 1: "directed {x. \Y \ X. finite Y \ Y \ {} \ extreme_bound A (\) Y x} (\)" (is "directed ?B _") + proof (intro directedI) + fix a b assume a: "a \ ?B" and b: "b \ ?B" + from a obtain Y where Y: "extreme_bound A (\) Y a" "finite Y" "Y \ {}" "Y \ X" by auto + from b obtain B where B: "extreme_bound A (\) B b" "finite B" "B \ {}" "B \ X" by auto + from XA Y B have AB: "Y \ A" "B \ A" "finite (Y \ B)" "Y \ B \ {}" "Y \ B \ X" by auto + with fc[THEN completeD] have "Ex (extreme_bound A (\) (Y \ B))" by auto + then obtain c where c: "extreme_bound A (\) (Y \ B) c" by auto + show "\c \ ?B. a \ c \ b \ c" + proof (intro bexI conjI) + from Y B c show "a \ c" and "b \ c" by (auto simp: extreme_bound_iff) + from AB c show "c \ ?B" by (auto intro!: exI[of _ "Y \ B"]) + qed qed - qed - assume "X \ {}" - then obtain x where xX: "x \ X" by auto - then have "extreme_bound (\) {x} x" by auto - with xX have xB: "x \ ?B" by (auto intro!: exI[of _ "{x}"]) - then have 2: "?B \ {}" by auto - from directed_nonempty_complete[OF 1 2] - obtain b where b: "extreme_bound (\) ?B b" by auto - show "Ex (extreme_bound (\) X)" - proof (intro exI extreme_boundI UNIV_I) - fix x - assume xX: "x \ X" - have x: "extreme_bound (\) {x} x" by auto - from x xX have cB: "x \ ?B" by (auto intro!: exI[of _ "{x}"]) - with b show "x \ b" by auto - next - fix x - assume Xx: "bound (\) X x" - have "bound (\) ?B x" - proof (intro boundI UNIV_I, clarify) - fix c Y - assume "finite Y" and YX: "Y \ X" and "Y \ {}" and c: "extreme_bound (\) Y c" - from YX Xx have "bound (\) Y x" by auto - with c show "c \ x" by auto - qed - with b show "b \ x" by auto + have B: "?B \ A" by auto + assume "X \ {}" + then obtain x where xX: "x \ X" by auto + with XA have "extreme_bound A (\) {x} x" + by (intro extreme_bound_singleton, auto) + with xX have xB: "x \ ?B" by (auto intro!: exI[of _ "{x}"]) + then have 2: "?B \ {}" by auto + from dc[unfolded directed_complete_def, THEN completeD, of ?B] B 1 2 + obtain b where b: "extreme_bound A (\) ?B b" by auto + then have bA: "b \ A" by auto + show "Ex (extreme_bound A (\) X)" + proof (intro exI extreme_boundI UNIV_I) + fix x + assume xX: "x \ X" + with XA have x: "extreme_bound A (\) {x} x" by (intro extreme_bound_singleton, auto) + from x xX have cB: "x \ ?B" by (auto intro!: exI[of _ "{x}"]) + with b show "x \ b" by auto + next + fix x + assume Xx: "bound X (\) x" and xA: "x \ A" + have "bound ?B (\) x" + proof (intro boundI UNIV_I, clarify) + fix c Y + assume "finite Y" and YX: "Y \ X" and "Y \ {}" and c: "extreme_bound A (\) Y c" + from YX Xx have "bound Y (\) x" by auto + with YX XA xA c show "c \ x" by auto + qed + with xA b show "b \ x" by auto + qed (fact bA) qed qed -locale complete_attractive = complete + attractive - -locale complete_antisymmetric = complete + antisymmetric - -sublocale complete_antisymmetric \ complete_attractive .. - -text \Complete pseudo orders are called complete trellises~\cite{trellis}, -but let us reserve the name for introducing classes (in the future).\ - -locale complete_pseudo_order = complete + pseudo_order - -sublocale complete_pseudo_order \ complete_antisymmetric .. - -text \Finally, we (re)define complete lattices as a complete partial order.\ - -locale complete_partial_order = complete + partial_order - -sublocale complete_partial_order \ trans_semilattice + complete_pseudo_order .. - subsection \Relating to Classes\ -class ccomplete = ord + assumes "conditionally_complete (\)" -begin - -sublocale order: conditionally_complete using ccomplete_axioms unfolding class.ccomplete_def. - -end +(* HOL.Conditionally_Complete_Lattices imports choice. -class complete_ord = ord + assumes "complete (\)" -begin - -interpretation order: complete using complete_ord_axioms unfolding class.complete_ord_def. - -subclass ccomplete .. - -sublocale order: complete .. - -end - -text \Isabelle's class @{class conditionally_complete_lattice} is @{class ccomplete}. +text \Isabelle's class @{class conditionally_complete_lattice} satisfies @{const conditionally_complete}. The other direction does not hold, since for the former, @{term "Sup {}"} and @{term "Inf {}"} are arbitrary even if there are top or bottom elements.\ -subclass (in conditionally_complete_lattice) ccomplete -proof - fix X - assume "Ex (upper_bound X)" and X0: "X \ {}" - from this(1) have "bdd_above X" by auto - from cSup_upper[OF _ this] cSup_least[OF X0] +lemma (in conditionally_complete_lattice) "conditionally_complete UNIV (\)" +proof (intro completeI, elim CollectE) + fix X :: "'a set" + assume "\b\UNIV. bound X (\) b \ X \ {}" + then have bdd:"bdd_above X" and X0: "X \ {}" by (auto 0 3) + from cSup_upper[OF _ bdd] cSup_least[OF X0] have "supremum X (Sup X)" by (intro extremeI boundI, auto) - then show "Ex (supremum X)" by auto + then show "\s. least {b \ UNIV. bound X (\) b} s" by auto qed - -text \Isabelle's class @{class complete_lattice} is precisely @{locale complete_partial_order}.\ - -context complete_lattice begin - -interpretation order: complete_partial_order - by (unfold_locales, auto intro!: Sup_upper Sup_least Inf_lower Inf_greatest) - -subclass complete_ord .. - -sublocale order: complete_partial_order .. - -end - - -subsection \Duality of Completeness Conditions\ - -text \Conditional completeness is symmetric.\ - -sublocale conditionally_complete \ dual: conditionally_complete "(\)\<^sup>-" -proof - interpret less_eq_dualize. - fix X :: "'a set" - assume bound: "Ex (bound (\) X)" and nonemp: "X \ {}" - then have "Ex (bound (\) {b. bound (\) X b})" and "{b. bound (\) X b} \ {}" by auto - from bounded_nonempty_complete[OF this] - obtain s where "extreme_bound (\) {b. bound (\) X b} s" by auto - then show "Ex (extreme_bound (\) X)" by (intro exI[of _ s] extremeI, auto) -qed - -text \Full completeness is symmetric.\ - -sublocale complete \ dual: complete "(\)\<^sup>-" -proof - fix X :: "'a set" - obtain s where "extreme_bound (\) {b. bound (\)\<^sup>- X b} s" using complete by auto - then show "Ex (extreme_bound (\)\<^sup>- X)" by (intro exI[of _ s] extreme_boundI, auto) -qed - -sublocale complete_attractive \ dual: complete_attractive "(\)\<^sup>-" .. +*) +text \Isabelle's class @{class complete_lattice} is @{term "UNIV-complete"}.\ -sublocale complete_antisymmetric \ dual: complete_antisymmetric "(\)\<^sup>-" .. - -sublocale complete_pseudo_order \ dual: complete_pseudo_order "(\)\<^sup>-" .. - -sublocale complete_partial_order \ dual: complete_partial_order "(\)\<^sup>-" .. - -text \Now we show that bounded completeness is the dual of semicompleteness.\ - -context fixes less_eq :: "'a \ 'a \ bool" (infix "\" 50) -begin - -interpretation less_eq_dualize. - -definition "bounded_complete \ \X. Ex (bound (\) X) \ Ex (extreme_bound (\) X)" +lemma (in complete_lattice) "UNIV-complete UNIV (\)" + by (auto intro!: completeI Sup_upper Sup_least Inf_lower Inf_greatest) -lemma pointed_conditionally_complete_iff_bounded_complete: - "conditionally_complete (\) \ bounded (\) \ bounded_complete" -proof safe - assume "bounded_complete" - note * = this[unfolded bounded_complete_def, rule_format] - from * show "conditionally_complete (\)" by (unfold_locales, auto) - from *[of "{}"] show "bounded (\)" by (unfold_locales, auto simp:bound_empty) -next - assume "conditionally_complete (\)" and "bounded (\)" - then interpret conditionally_complete "(\)" + dual: bounded "(\)". - show "bounded_complete" unfolding bounded_complete_def - proof (intro allI impI) - fix X - assume X: "Ex (bound (\) X)" - show "Ex (extreme_bound (\) X)" - proof (cases "X = {}") - case True - then show ?thesis by auto - next - case False - with bounded_nonempty_complete X show ?thesis by auto - qed +subsection \Set-wise Completeness\ + +lemma directed_sets_directed_complete: + assumes cl: "\DC. DC \ AA \ (\X\DC. directed X r) \ (\DC) \ AA" + shows "{DC. directed DC (\)}-complete {X \ AA. directed X r} (\)" +proof (intro completeI, safe) + fix XX + assume ch: "XX \ {X \ AA. directed X r}" and dir: "directed XX (\)" + with cl have "(\XX) \ AA" by auto + moreover have "directed (\XX) r" + proof (intro directedI, elim UnionE) + fix x y X Y assume xX: "x \ X" and X: "X \ XX" and yY: "y \ Y" and Y: "Y \ XX" + from directedD[OF dir X Y] + obtain Z where "X \ Z" "Y \ Z" and Z: "Z \ XX" by auto + with ch xX yY have "directed Z r" "x \ Z" "y \ Z" by auto + then obtain z where "z \ Z" "r x z \ r y z" by (auto elim:directedE) + with Z show "\z\\ XX. r x z \ r y z" by auto qed -qed - -proposition bounded_complete_iff_dual_semicomplete: - "bounded_complete \ semicomplete (\)" -proof (fold pointed_conditionally_complete_iff_bounded_complete, safe) - assume "conditionally_complete (\)" and "bounded (\)" - then interpret conditionally_complete + bounded "(\)". - from dual.conditionally_complete_axioms bounded_axioms - semicomplete_iff_conditionally_complete_bounded - show "semicomplete (\)" by auto -next - assume "semicomplete (\)" - then interpret semicomplete "(\)". - show "conditionally_complete (\)" .. - show "bounded (\)" .. + ultimately have "extreme_bound {X \ AA. directed X r} (\) XX (\XX)" by auto + then show "Ex (extreme_bound {X \ AA. directed X r} (\) XX)" by auto qed -end - - -subsection \Completeness in Function Spaces\ - -text \Here we lift completeness to functions. As we do not assume an operator to choose suprema, -we need the axiom of choice for most of the following results. In antisymmetric cases we do not -need the axiom but we do not formalize this fact.\ - -lemma (in bounded) bounded_fun[intro!]: "bounded (fun_ord (\))" -proof- - from bounded obtain t where "\x. x \ t" by auto - then have "\f. fun_ord (\) f (\x. t)" by (auto intro: fun_ordI) - then show ?thesis by (auto intro: bounded.intro) -qed - -lemma (in pair_complete) pair_complete_fun[intro!]: - "pair_complete (fun_ord (\) :: ('i \ _) \ _)" -proof - fix f g :: "'i \ _" - from pair_complete have "\x. \sx. extreme_bound (\) {f x, g x} sx" by auto - from choice[OF this] - obtain s where "\x. extreme_bound (\) {f x, g x} (s x)" by auto - then show "Ex (extreme_bound (fun_ord (\)) {f, g})" - by (unfold fun_extreme_bound_iff, intro exI[of _ s], auto 1 4) -qed - -lemma (in finite_complete) finite_complete_fun[intro!]: - "finite_complete (fun_ord (\) :: ('i \ 'a) \ _)" -proof - fix F :: "('i \ 'a) set" - assume "finite F" and "F \ {}" - with finite_nonempty_complete - have "\x. \sx. extreme_bound (\) {f x |. f \ F} sx" by auto - from choice[OF this] - show "Ex (extreme_bound (fun_ord (\)) F)" by (unfold fun_extreme_bound_iff, auto) -qed - -lemma (in omega_complete) omega_complete_fun[intro!]: - "omega_complete (fun_ord (\) :: ('i \ 'a) \ _)" -proof - fix ff :: "nat \ 'i \ 'a" - assume ff: "monotone (\) (fun_ord (\)) ff" - then have "\i. Ex (extreme_bound (\) {ff n i |. n})" - by (intro allI monotone_seq_complete, auto simp: monotone_def fun_ord_def) - from choice[OF this] - obtain s where "\i. extreme_bound (\) {ff n i |. n} (s i)" by auto - then have "extreme_bound (fun_ord (\)) (range ff) s" - by (auto simp: fun_extreme_bound_iff image_image) - then show "Ex (extreme_bound (fun_ord (\)) (range ff))" by auto -qed - -lemma (in chain_complete) chain_complete_fun[intro!]: - "chain_complete (fun_ord (\) :: ('i \ 'a) \ _)" -proof - fix F :: "('i \ 'a) set" - assume F: "chain (fun_ord (\)) F" and "F \ {}" - then have "\i. Ex (extreme_bound (\) {f i |. f \ F})" - by (intro allI chain_nonempty_complete, auto simp: chain_def fun_ord_def) - from choice[OF this] - obtain s where "\i. extreme_bound (\) {f i |. f \ F} (s i)" by auto - then show "Ex (extreme_bound (fun_ord (\)) F)" by (auto simp: fun_extreme_bound_iff) +lemma connex_directed_Un: + assumes ch: "CC \ {C. connex C r}" and dir: "directed CC (\)" + shows "connex (\CC) r" +proof (intro connexI, elim UnionE) + fix x y X Y assume xX: "x \ X" and X: "X \ CC" and yY: "y \ Y" and Y: "Y \ CC" + from directedD[OF dir X Y] + obtain Z where "X \ Z" "Y \ Z" "Z \ CC" by auto + with xX yY ch have "x \ Z" "y \ Z" "connex Z r" by auto + then show "r x y \ r y x" by (auto elim:connexE) qed -lemma (in directed_complete) directed_complete_fun[intro!]: - "directed_complete (fun_ord (\) :: ('i \ 'a) \ _)" -proof - fix F :: "('i \ 'a) set" - assume dir: "directed (fun_ord (\)) F" and F0: "F \ {}" - have "\i. Ex (extreme_bound (\) {f i |. f \ F})" - proof (intro allI directed_nonempty_complete directedI, safe) - fix i f g assume "f \ F" "g \ F" - with dir obtain h - where h: "h \ F" and "fun_ord (\) f h" and "fun_ord (\) g h" by (auto elim:directedE) - then have "f i \ h i" and "g i \ h i" by (auto dest: fun_ordD) - with h show "\hi\{f i |. f \ F}. f i \ hi \ g i \ hi" by (intro bexI[of _ "h i"], auto) - qed (insert F0, auto) - from choice[OF this] - obtain s where "\i. extreme_bound (\) {f i |. f \ F} (s i)" by auto - then show "Ex (extreme_bound (fun_ord (\)) F)" by (auto simp: fun_extreme_bound_iff) -qed - -lemma (in conditionally_complete) conditionally_complete_fun[intro!]: - "conditionally_complete (fun_ord (\) :: ('i \ 'a) \ _)" -proof - fix F :: "('i \ 'a) set" - assume bF: "Ex (bound (fun_ord (\)) F)" and F: "F \ {}" - from bF obtain b where b: "bound (fun_ord (\)) F b" by auto - have "\x. \sx. extreme_bound (\) {f x |. f \ F} sx" - proof - fix x - from b have "bound (\) {f x |. f \ F} (b x)" by (auto simp: fun_ord_def) - with bounded_nonempty_complete F - show "Ex (extreme_bound (\) {f x |. f \ F})" by auto - qed - from choice[OF this] - show "Ex (extreme_bound (fun_ord (\)) F)" by (unfold fun_extreme_bound_iff, auto) -qed - -lemma (in semicomplete) semicomplete_fun[intro!]: "semicomplete (fun_ord (\))" - by (auto simp: semicomplete_iff_conditionally_complete_bounded) - -lemma (in pointed_chain_complete) pointed_chain_complete_fun[intro!]: - "pointed_chain_complete (fun_ord (\))" - by (auto intro!: pointed_chain_complete.intro simp: dual_fun_ord) - -lemma (in pointed_directed_complete) pointed_directed_complete_fun[intro!]: - "pointed_directed_complete (fun_ord (\))" - by (auto intro!: pointed_directed_complete.intro simp: dual_fun_ord) - -lemma (in complete) complete_fun[intro!]: "complete (fun_ord (\))" - by (auto simp: complete_iff_pointed_semicomplete dual_fun_ord) - -subsection \Interpretations\ - -context complete_lattice begin - -lemma Sup_eq_The_supremum: "Sup X = The (supremum X)" - using order.complete[unfolded order.dual.ex_extreme_iff_ex1] - by (rule the1_equality[symmetric], auto intro!: Sup_upper Sup_least) - -lemma Inf_eq_The_infimum: "Inf X = The (infimum X)" - using order.dual.complete[unfolded order.ex_extreme_iff_ex1] - by (rule the1_equality[symmetric], auto intro!: Inf_lower Inf_greatest) - -end - -instance real :: ccomplete by (intro_classes, unfold_locales) - -instance "fun" :: (type, ccomplete) ccomplete by (intro_classes, fold fun_ord_le, auto) - -instance "fun" :: (type, complete_ord) complete_ord by (intro_classes, fold fun_ord_le, auto) +lemma connex_directed_complete: "{DC. directed DC (\)}-complete {C. connex C r} (\)" + by (intro completeI, force dest!: connex_directed_Un) end \ No newline at end of file diff --git a/thys/Complete_Non_Orders/Fixed_Points.thy b/thys/Complete_Non_Orders/Fixed_Points.thy --- a/thys/Complete_Non_Orders/Fixed_Points.thy +++ b/thys/Complete_Non_Orders/Fixed_Points.thy @@ -1,714 +1,1236 @@ (* -Author: Jérémy Dubut (2019) -Author: Akihisa Yamada (2019) +Author: Jérémy Dubut (2019-2021) +Author: Akihisa Yamada (2019-2021) License: LGPL (see file COPYING.LESSER) *) -section \Knaster--Tarski-Style Fixed-Point Theorem\ theory Fixed_Points imports Complete_Relations begin -text \Given a monotone map -$f : A \to A$ on a complete lattice $\tp{A,\SLE}$, -the Knaster--Tarski theorem~\cite{tarski55} states that -\begin{enumerate} -\item $f$ has a fixed point in $A$, and -\item the set of fixed points forms a complete lattice. -\end{enumerate} -Stauti and Maaden \cite{SM13} generalized statement (1) where $\tp{A,\SLE}$ -is a complete \emph{trellis}---a complete pseudo-order---% -relaxing transitivity. -They also proved a restricted version of (2), -namely there exists a least (and by duality a greatest) fixed point in $A$. +section \Existence of Fixed Points in Complete Related Sets\ +text \\label{sec:qfp-exists}\ -In the following Section~\ref{sec:qfp-exists} we further generalize claim (1) -so that any complete relation -admits a \emph{quasi-fixed point} $f(x) \sim x$, that is, $f(x) \SLE x$ and $x \SLE f(x)$. -Quasi-fixed points are fixed points for antisymmetric relations; -hence the Stauti--Maaden theorem is further generalized by relaxing reflexivity. +text \The following proof is simplified and generalized from + Stouti--Maaden \cite{SM13}. We construct some set whose extreme bounds + -- if they exist, typically when the underlying related set is complete -- + are fixed points of a monotone or inflationary function on any + related set. When the related set is attractive, those are actually the least fixed points. + This generalizes \cite{SM13}, relaxing reflexivity and antisymmetry.\ -In Section \ref{sec:qfp-complete} -we also generalize claim (2) so that only a mild condition, which we call \emph{attractivity}, -is assumed. In this attractive setting quasi-fixed points are complete. -Since attractivity is implied by either of transitivity or antisymmetry, -in particular fixed points are complete in complete trellis, -thus completing Stauti and Maaden's result. We then further generalize the result, proving that -antisymmetry is sufficient for \emph{strict} fixed points -$f(x) = x$ to be complete.\ - -subsection \Completeness of a Subset\ - -text \We start by formalizing what it means for a subset to have an extreme bound inside -a set, and for this subset to be complete. We prove that this completeness is also auto-dual.\ - -context - fixes less_eq :: "'a \ 'a \ bool" (infix "\" 50) +locale fixed_point_proof = related_set + + fixes f + assumes f: "f ` A \ A" begin -interpretation less_eq_dualize. - -abbreviation "extreme_bound_in S X \ extreme (\) {b \ S. bound (\) X b}" - -lemma extreme_bound_inI[intro]: - assumes "\b. bound (\) X b \ b \ S \ s \ b" and "s \ S" and "\x. x \ X \ x \ s" - shows "extreme_bound_in S X s" - using assms by auto - -definition "complete_in S \ \X \ S. Ex (extreme_bound_in S X)" +sublocale less_eq_notations. -lemma complete_inE[elim]: - assumes "complete_in S" and "(\X. X \ S \ Ex (extreme_bound_in S X)) \ thesis" - shows "thesis" - using assms by (auto simp: complete_in_def) +definition AA where "AA \ + {X. X \ A \ f ` X \ X \ (\Y s. Y \ X \ extreme_bound A (\) Y s \ s \ X)}" -lemma complete_inD: - shows "complete_in S \ X \ S \ Ex (extreme_bound_in S X)" - by (auto simp: complete_in_def) +lemma AA_I: + "X \ A \ f ` X \ X \ (\Y s. Y \ X \ extreme_bound A (\) Y s \ s \ X) \ X \ AA" + by (unfold AA_def, safe) -lemma complete_inI[intro?]: - assumes "\X. X \ S \ Ex (extreme_bound_in S X)" - shows "complete_in S" - using assms by (auto simp: complete_in_def) +lemma AA_E: + "X \ AA \ + (X \ A \ f ` X \ X \ (\Y s. Y \ X \ extreme_bound A (\) Y s \ s \ X) \ thesis) \ thesis" + by (auto simp: AA_def) -end +definition C where "C \ \ AA" + +lemma A_AA: "A \ AA" by (auto intro!:AA_I f) + +lemma C_AA: "C \ AA" +proof (intro AA_I) + show "C \ A" using C_def A_AA f by auto + show "f ` C \ C" unfolding C_def AA_def by auto + fix B b assume B: "B \ C" "extreme_bound A (\) B b" + { fix X assume X: "X \ AA" + with B have "B \ X" by (auto simp: C_def) + with X B have "b\X" by (auto elim!: AA_E) + } + then show "b \ C" by (auto simp: C_def AA_def) +qed + +lemma CA: "C \ A" using A_AA by (auto simp: C_def) + +lemma fC: "f ` C \ C" using C_AA by (auto elim!: AA_E) context - fixes less_eq :: "'a \ 'a \ bool" (infix "\" 50) + fixes c assumes Cc: "extreme_bound A (\) C c" begin -interpretation less_eq_dualize. +private lemma cA: "c \ A" using Cc by auto +private lemma cC: "c \ C" using Cc C_AA by (blast elim!:AA_E) +private lemma fcC: "f c \ C" using cC AA_def C_AA by auto +private lemma fcA: "f c \ A" using fcC CA by auto -lemma complete_in_dual: - assumes complete: "complete_in (\) S" shows "complete_in (\) S" -proof - fix A :: "'a set" - assume AS: "A \ S" - define B where "B \ {b\S. bound (\) A b}" - then have "B \ S" by auto - then obtain b where "extreme_bound_in (\) S B b" - using complete by force - with AS show "Ex (extreme_bound_in (\) S A)" - apply (intro exI[of _ b], unfold extreme_def B_def) by auto +lemma qfp_as_extreme_bound: + assumes infl_mono: "\x \ A. x \ f x \ (\y \ A. y \ x \ f y \ f x)" + shows "f c \ c" +proof (intro conjI bexI sympartpI) + show "f c \ c" using fcC Cc by auto + from infl_mono[rule_format, OF cA] + show "c \ f c" + proof (safe) + text \Monotone case:\ + assume mono: "\b\A. b \ c \ f b \ f c" + define D where "D \ {x \ C. x \ f c}" + have "D \ AA" + proof (intro AA_I) + show "D \ A" unfolding D_def C_def using A_AA f by auto + have fxC: "x \ C \ x \ f c \ f x \ C" for x using C_AA by (auto simp: AA_def) + show "f ` D \ D" + proof (unfold D_def, safe intro!: fxC) + fix x assume xC: "x \ C" + have "x \ c" "x \ A" using Cc xC CA by auto + then show "f x \ f c" using mono by (auto dest:monotoneD) + qed + have DC: "D \ C" unfolding D_def by auto + fix B b assume BD: "B \ D" and Bb: "extreme_bound A (\) B b" + have "B \ C" using DC BD by auto + then have bC: "b \ C" using C_AA Bb BD by (auto elim!: AA_E) + have bfc: "\a\B. a \ f c" using BD unfolding D_def by auto + with f cA Bb + have "b \ f c" by (auto simp: extreme_def image_subset_iff) + with bC show "b \ D" unfolding D_def by auto + qed + then have "C \ D" unfolding C_def by auto + then show "c \ f c" using cC unfolding D_def by auto + qed +qed + +lemma extreme_qfp: + assumes attract: "\q \ A. \x \ A. f q \ q \ x \ f q \ x \ q" + and mono: "monotone_on A (\) (\) f" + shows "extreme {q \ A. f q \ q \ f q = q} (\) c" +proof- + have fcc: "f c \ c" + apply (rule qfp_as_extreme_bound) + using mono by (auto elim!: monotone_onE) + define L where [simp]: "L \ {a \ A. \s \ A. (f s \ s \ f s = s) \ a \ s}" + have "L \ AA" + proof (unfold AA_def, intro CollectI conjI allI impI) + show XA: "L \ A" by auto + show "f ` L \ L" + proof safe + fix x assume xL: "x \ L" + show "f x \ L" + proof (unfold L_def, safe) + have xA: "x \ A" using xL by auto + then show fxA: "f x \ A" using f by auto + { fix s assume sA: "s \ A" and sf: "f s \ s \ f s = s" + then have "x \ s" using xL sA sf by auto + then have "f x \ f s" using mono fxA sA xA by (auto elim!:monotone_onE)} + note fxfs = this + { fix s assume sA: "s \ A" and sf: "f s \ s" + then show "f x \ s" using fxfs attract mono sf fxA sA xA by (auto elim!:monotone_onE) + } + { fix s assume sA: "s \ A" and sf: "f s = s" + with fxfs[OF sA] show "f x \ s" by simp} + qed + qed + fix B b assume BL: "B \ L" and b: "extreme_bound A (\) B b" + then have BA: "B \ A" by auto + with BL b have bA: "b \ A" by auto + show "b \ L" + proof (unfold L_def, safe intro!: bA) + { fix s assume sA: "s \ A" and sf: "f s \ s \ f s = s" + have "bound B (\) s" using sA BL b sf by auto + } + note Bs = this + { fix s assume sA: "s \ A" and sf: "f s \ s" + with b sA Bs show "b \ s" by auto + } + { fix s assume sA: "s \ A" and sf: "f s = s" + with b sA Bs show "b \ s" by auto + } + qed + qed + then have "C \ L" by (simp add: C_def Inf_lower) + with cC have "c \ L" by auto + with L_def fcc + show ?thesis by auto qed end -subsection \Existence of Quasi-Fixed Points\ -text \\label{sec:qfp-exists}\ - -text \The following proof is simplified and generalized from - Stouti--Maaden \cite{SM13}. We generalize so that the underlying -relation is not even reflexive or antisymmetric.\ - -locale fixed_point_proof = less_eq_dualize -begin +lemma ex_qfp: + assumes comp: "CC-complete A (\)" and C: "C \ CC" + and infl_mono: "\a \ A. a \ f a \ (\b \ A. b \ a \ f b \ f a)" + shows "\s \ A. f s \ s" + using qfp_as_extreme_bound[OF _ infl_mono] completeD[OF comp CA C] by auto -context - fixes f :: "'a \ 'a" and S :: "'a set" - assumes mono: "monotone (\) (\) f" - assumes f_closed_S: "f ` S \ S" - assumes S_comp: "complete_in (\) S" -begin - -definition AA where "AA \ - {A. A \ S \ f ` A \ A \ (\B \ A. \b. extreme_bound_in (\) S B b \ b \ A)}" -definition C where "C \ \ AA" +lemma ex_extreme_qfp_fp: + assumes comp: "CC-complete A (\)" and C: "C \ CC" + and attract: "\q \ A. \x \ A. f q \ q \ x \ f q \ x \ q" + and mono: "monotone_on A (\) (\) f" + shows "\c. extreme {q \ A. f q \ q \ f q = q} (\) c" + using extreme_qfp[OF _ attract mono] completeD[OF comp CA C] by auto -qualified lemma S_AA: "S \ AA" by (auto simp: AA_def f_closed_S) - -qualified lemma C_AA: "C \ AA" -proof (unfold AA_def, intro CollectI conjI allI impI) - show "C \ S" using C_def S_AA f_closed_S by auto - show "f ` C \ C" unfolding C_def AA_def by auto - fix B b assume BC: "B \ C" and EBS: "extreme_bound_in (\) S B b" - { fix X assume "X \ AA" - with EBS have "b\X" - apply (unfold AA_def,safe) by (metis BC C_def Inf_lower subset_trans) - } - then show "b \ C" by (auto simp: C_def AA_def) +lemma ex_extreme_qfp: + assumes comp: "CC-complete A (\)" and C: "C \ CC" + and attract: "\q \ A. \x \ A. f q \ q \ x \ f q \ x \ q" + and mono: "monotone_on A (\) (\) f" + shows "\c. extreme {q \ A. f q \ q} (\) c" +proof- + from completeD[OF comp CA C] + obtain c where Cc: "extreme_bound A (\) C c" by auto + from extreme_qfp[OF Cc attract mono] + have Qc: "bound {q \ A. f q \ q} (\) c" by auto + have fcc: "f c \ c" + apply (rule qfp_as_extreme_bound[OF Cc]) + using mono by (auto simp: monotone_onD) + from Cc CA have cA: "c \ A" by auto + from Qc fcc cA show ?thesis by (auto intro!: exI[of _ c]) qed -lemma quasi_fixed_point_in_C: "\c \ C. f c \ c" +end + +context + fixes less_eq :: "'a \ 'a \ bool" (infix "\" 50) and A :: "'a set" and f + assumes f: "f ` A \ A" +begin + +interpretation less_eq_notations. +interpretation fixed_point_proof A "(\)" f using f by unfold_locales + +theorem complete_infl_mono_imp_ex_qfp: + assumes comp: "UNIV-complete A (\)" and infl_mono: "\a\A. a \ f a \ (\b\A. b \ a \ f b \ f a)" + shows "\s\A. f s \ s" + apply (rule ex_qfp[OF comp _ infl_mono]) by auto + +end + +corollary (in antisymmetric) complete_infl_mono_imp_ex_fp: + assumes comp: "UNIV-complete A (\)" and f: "f ` A \ A" + and infl_mono: "\a\A. a \ f a \ (\b\A. b \ a \ f b \ f a)" + shows "\s \ A. f s = s" proof- - obtain c where c: "extreme_bound_in (\) S C c" - using S_comp unfolding complete_in_def C_def - by (metis InterE S_AA subset_iff) - then have cS: "c \ S" by auto - show "\c \ C. f c \ c" - proof (intro conjI bexI) - show cCS: "c \ C" using AA_def C_AA c by auto - then have "f c \ C" using AA_def C_AA by auto - then show "f c \ c" using f_closed_S cS c by auto - show "c \ f c" - proof- - define D where "D \ {x \ C. x \ f c}" - have "D \ AA" - proof (unfold AA_def, intro CollectI conjI allI impI) - show "D \ S" - unfolding D_def C_def using S_AA f_closed_S by auto - have fxC: "x \ C \ x \ f c \ f x \ C" for x using C_AA by (auto simp: AA_def) - show "f ` D \ D" - proof (unfold D_def, safe intro!: fxC) - fix x assume xC: "x \ C" - have "x \ c" using c xC by auto - then show "f x \ f c" using mono by (auto dest:monotoneD) + interpret less_eq_notations. + from complete_infl_mono_imp_ex_qfp[OF f comp infl_mono] + obtain s where sA: "s \ A" and fss: "f s \ s" by auto + from f sA have fsA: "f s \ A" by auto + have "f s = s" using antisym fsA sA fss by auto + with sA show ?thesis by auto +qed + +context semiattractive begin + +interpretation less_eq_notations. + +theorem complete_mono_imp_ex_extreme_qfp: + assumes comp: "UNIV-complete A (\)" and f: "f ` A \ A" + and mono: "monotone_on A (\) (\) f" + shows "\s. extreme {p \ A. f p \ p} (\) s" +proof- + interpret dual: fixed_point_proof A "(\)" rewrites "dual.sym = (\)" + using f by unfold_locales (auto intro!:ext) + show ?thesis + apply (rule dual.ex_extreme_qfp[OF complete_dual[OF comp] _ _ monotone_on_dual[OF mono]]) + apply simp + using f sym_order_trans by blast +qed + +end + +corollary (in antisymmetric) complete_mono_imp_ex_extreme_fp: + assumes comp: "UNIV-complete A (\)" and f: "f ` A \ A" + and mono: "monotone_on A (\) (\) f" + shows "\s. extreme {s \ A. f s = s} (\)\<^sup>- s" +proof- + interpret less_eq_notations. + interpret fixed_point_proof A "(\)" f using f by unfold_locales + have "\c. extreme {q \ A. f q \ q \ f q = q} (\) c" + apply (rule ex_extreme_qfp_fp[OF comp _ _ mono]) + using antisym f by (auto dest: order_sym_trans) + then obtain c where c: "extreme {q \ A. f q \ q \ f q = q} (\) c" by auto + then have "f c = c" using antisym f by blast + with c have "extreme {q \ A. f q = q} (\) c" by auto + then show ?thesis by auto +qed + +section \Fixed Points in Well-Complete Antisymmetric Sets\ +text \\label{sec:well-complete}\ + +text \In this section, we prove that an +inflationary or monotone map over a well-complete antisymmetric set +has a fixed point. + +In order to formalize such a theorem in Isabelle, +we followed Grall's~\cite{grall10} elementary proof for Bourbaki--Witt and Markowsky's theorems. +His idea is to consider well-founded derivation trees over $A$, +where from a set $C \subseteq A$ of premises +one can derive $f\:(\SUP C)$ if $C$ is a chain. +The main observation is as follows: +Let $D$ be the set of all the derivable elements; that is, +for each $d \in D$ there exists a well-founded derivation +whose root is $d$. +It is shown that $D$ is a chain, +and hence one can build a derivation yielding $f\:(\SUP D)$, +and $f\:(\SUP D)$ is shown to be a fixed point.\ + +lemma bound_monotone_on: + assumes mono: "monotone_on A r s f" and XA: "X \ A" and aA: "a \ A" and rXa: "bound X r a" + shows "bound (f`X) s (f a)" +proof (safe) + fix x assume xX: "x \ X" + from rXa xX have "r x a" by auto + with xX XA mono aA show "s (f x) (f a)" by (auto elim!:monotone_onE) +qed + +context fixed_point_proof begin + +text \To avoid the usage of the axiom of choice, we carefully define derivations so that any derivable element +determines its lower set. This led to the following definition:\ + +definition "derivation X \ X \ A \ well_ordered_set X (\) \ + (\x \ X. let Y = {y \ X. y \ x} in + (\y. extreme Y (\) y \ x = f y) \ + f ` Y \ Y \ extreme_bound A (\) Y x)" + +lemma assumes "derivation P" + shows derivation_A: "P \ A" and derivation_well_ordered: "well_ordered_set P (\)" + using assms by (auto simp: derivation_def) + +lemma derivation_cases[consumes 2, case_names suc lim]: + assumes "derivation X" and "x \ X" + and "\Y y. Y = {y \ X. y \ x} \ extreme Y (\) y \ x = f y \ thesis" + and "\Y. Y = {y \ X. y \ x} \ f ` Y \ Y \ extreme_bound A (\) Y x \ thesis" + shows thesis + using assms unfolding derivation_def Let_def by auto + +definition "derivable x \ \X. derivation X \ x \ X" + +lemma derivableI[intro?]: "derivation X \ x \ X \ derivable x" by (auto simp: derivable_def) +lemma derivableE: "derivable x \ (\P. derivation P \ x \ P \ thesis) \ thesis" + by (auto simp: derivable_def) + +lemma derivable_A: "derivable x \ x \ A" by (auto elim: derivableE dest:derivation_A) + +lemma UN_derivations_eq_derivable: "(\{P. derivation P}) = {x. derivable x}" + by (auto simp: derivable_def) + +context + assumes ord: "antisymmetric A (\)" +begin + +interpretation antisymmetric using ord. + +lemma derivation_lim: + assumes P: "derivation P" and fP: "f ` P \ P" and Pp: "extreme_bound A (\) P p" + shows "derivation (P \ {p})" +proof (cases "p \ P") + case True + with P show ?thesis by (auto simp: insert_absorb) +next + case pP: False + interpret P: well_ordered_set P "(\)" using derivation_well_ordered[OF P]. + have PA: "P \ A" using derivation_A[OF P]. + from Pp have pA: "p \ A" by auto + have bp: "bound P (\) p" using Pp by auto + then have pp: "p \ p" using Pp by auto + have 1: "y \ P \ {x. (x = p \ x \ P) \ x \ y} = {x \ P. x \ y}" for y + using Pp by (auto dest:extreme_bound_bound) + { fix x assume xP: "x \ P" and px: "p \ x" + from xP Pp have "x \ p" by auto + with px have "p = x" using xP PA pA by (auto intro!: antisym) + with xP pP + have "False" by auto + } + note 2 = this + then have 3: "{x. (x = p \ x \ P) \ x \ p} = P" using Pp by (auto intro!: asympartpI) + have wr: "well_ordered_set (P \ {p}) (\)" + apply (rule well_order_extend[OF P.well_ordered_set_axioms]) + using pp bp pP 2 by auto + from P fP Pp + show "derivation (P \ {p})" by (auto simp: derivation_def pA wr[simplified] 1 3) +qed + +context + assumes derivation_infl: "\X x y. derivation X \ x \ X \ y \ X \ x \ y \ x \ f y" + and derivation_f_refl: "\X x. derivation X \ x \ X \ f x \ f x" +begin + +lemma derivation_suc: + assumes P: "derivation P" and Pp: "extreme P (\) p" shows "derivation (P \ {f p})" +proof (cases "f p \ P") + case True + with P show ?thesis by (auto simp: insert_absorb) +next + case fpP: False + interpret P: well_ordered_set P "(\)" using derivation_well_ordered[OF P]. + have PA: "P \ A" using derivation_A[OF P]. + with Pp have pP: "p \ P" and pA: "p \ A" by auto + with f have fpA: "f p \ A" by auto + from pP have pp: "p \ p" by auto + from derivation_infl[rule_format, OF P pP pP pp] have "p \ f p". + { fix x assume xP: "x \ P" + then have xA: "x \ A" using PA by auto + have xp: "x \ p" using xP Pp by auto + from derivation_infl[rule_format, OF P xP pP this] + have "x \ f p". + } + note Pfp = this + then have bfp: "bound P (\) (f p)" by auto + { fix y assume yP: "y \ P" + note yfp = Pfp[OF yP] + { assume fpy: "f p \ y" + with yfp have "f p = y" using yP PA pA fpA antisym by auto + with yP fpP have "False" by auto + } + with Pfp yP have "y \ f p" by auto + } + note Pfp = this + have 1: "\y. y \ P \ {x. (x = f p \ x \ P) \ x \ y} = {x \ P. x \ y}" + and 2: "{x. (x = f p \ x \ P) \ x \ f p} = P" using Pfp by auto + have wr: "well_ordered_set (P \ {f p}) (\)" + apply (rule well_order_extend[OF P.well_ordered_set_axioms singleton_well_ordered]) + using Pfp derivation_f_refl[rule_format, OF P pP] by auto + from P Pp + show "derivation (P \ {f p})" by (auto simp: derivation_def wr[simplified] 1 2 fpA) +qed + +lemma derivable_closed: + assumes x: "derivable x" shows "derivable (f x)" +proof (insert x, elim derivableE) + fix P + assume P: "derivation P" and xP: "x \ P" + note PA = derivation_A[OF P] + then have xA: "x \ A" using xP by auto + interpret P: well_ordered_set P "(\)" using derivation_well_ordered[OF P]. + interpret P.asympartp: transitive P "(\)" using P.asympartp_transitive. + define Px where "Px \ {y. y \ P \ y \ x} \ {x}" + then have PxP: "Px \ P" using xP by auto + have "x \ x" using xP by auto + then have Pxx: "extreme Px (\) x" using xP PA by (auto simp: Px_def) + have wr: "well_ordered_set Px (\)" using P.well_ordered_subset[OF PxP]. + { fix z y assume zPx: "z \ Px" and yP: "y \ P" and yz: "y \ z" + then have zP: "z \ P" using PxP by auto + have "y \ x" + proof (cases "z = x") + case True + then show ?thesis using yz by auto + next + case False + then have zx: "z \ x" using zPx by (auto simp: Px_def) + from P.asympartp.trans[OF yz zx yP zP xP] show ?thesis. + qed + } + then have 1: "\z. z \ Px \ {y \ Px. y \ z} = {y \ P. y \ z}" using Px_def by blast + have Px: "derivation Px" using PxP PA P by (auto simp: wr derivation_def 1) + from derivation_suc[OF Px Pxx] + show ?thesis by (auto intro!: derivableI) +qed + +text \The following lemma is derived from Grall’s proof. We simplify the claim so that we +consider two elements from one derivation, instead of two derivations.\ + +lemma derivation_useful: + assumes X: "derivation X" and xX: "x \ X" and yX: "y \ X" and xy: "x \ y" + shows "f x \ y" +proof- + interpret X: well_ordered_set X "(\)" using derivation_well_ordered[OF X]. + note XA = derivation_A[OF X] + { fix x y assume xX: "x \ X" and yX: "y \ X" + from xX yX have "(x \ y \ f x \ y \ f x \ X) \ (y \ x \ f y \ x \ f y \ X)" + proof (induct x arbitrary: y) + case (less x) + note xX = \x \ X\ and IHx = this(2) + with XA have xA: "x \ A" by auto + from \y \ X\ show ?case + proof (induct y) + case (less y) + note yX = \y \ X\ and IHy = this(2) + with XA have yA: "y \ A" by auto + show ?case + proof (rule conjI; intro impI) + assume xy: "x \ y" + from X yX + show "f x \ y \ f x \ X" + proof (cases rule:derivation_cases) + case (suc Z z) + with XA have zX: "z \ X" and zA: "z \ A" and zy: "z \ y" and yfz: "y = f z" by auto + from xX zX show ?thesis + proof (cases rule: X.comparable_three_cases) + case xz: less + with IHy[OF zX zy] have fxz: "f x \ z" and fxX: "f x \ X" by auto + from derivation_infl[rule_format, OF X fxX zX fxz] have "f x \ y" by (auto simp: yfz) + with fxX show ?thesis by auto + next + case eq + with xX zX have "x = z" by auto + with yX yfz show ?thesis by auto + next + case zx: greater + with IHy[OF zX zy] yfz xy have False by auto + then show ?thesis by auto + qed + next + case (lim Z) + note Z = \Z = {z \ X. z \ y}\ and fZ = \f ` Z \ Z\ + from xX xy have "x \ Z" by (auto simp: Z) + with fZ have "f x \ Z" by auto + then have "f x \ y" and "f x \ X" by (auto simp: Z) + then show ?thesis by auto + qed + next + assume yx: "y \ x" + from X xX + show "f y \ x \ f y \ X" + proof (cases rule:derivation_cases) + case (suc Z z) + with XA have zX: "z \ X" and zA: "z \ A" and zx: "z \ x" and xfz: "x = f z" by auto + from yX zX show ?thesis + proof (cases rule: X.comparable_three_cases) + case yz: less + with IHx[OF zX zx yX] have fyz: "f y \ z" and fyX: "f y \ X" by auto + from derivation_infl[rule_format, OF X fyX zX fyz] have "f y \ x" by (auto simp: xfz) + with fyX show ?thesis by auto + next + case eq + with yX zX have "y = z" by auto + with xX xfz show ?thesis by auto + next + case greater + with IHx[OF zX zx yX] xfz yx have False by auto + then show ?thesis by auto + qed + next + case (lim Z) + note Z = \Z = {z \ X. z \ x}\ and fZ = \f ` Z \ Z\ + from yX yx have "y \ Z" by (auto simp: Z) + with fZ have "f y \ Z" by auto + then have "f y \ x" and "f y \ X" by (auto simp: Z) + then show ?thesis by auto + qed qed - have DC: "D \ C" unfolding D_def by auto - fix B b assume BD: "B \ D" and BS: "extreme_bound_in (\) S B b" - have "B \ C" using DC BD by auto - then have bC: "b \ C" using C_AA BS by (auto simp: AA_def) - have bfc: "\a\B. a \ f c" using BD unfolding D_def by auto - with f_closed_S cS BS - have "b \ f c" by (auto simp: extreme_def image_subset_iff) - with bC show "b \ D" unfolding D_def by auto qed - then have "C \ D" unfolding C_def by auto - then show "c \ f c" using cCS unfolding D_def by auto + qed + } + with assms show "f x \ y" by auto +qed + +text \Next one is the main lemma of this section, stating that elements from two possibly different +derivations are comparable, and moreover the lower one is in the derivation of the upper one. +The latter claim, not found in Grall’s proof, is crucial in proving that the union of all +derivations is well-related.\ + +lemma derivations_cross_compare: + assumes X: "derivation X" and Y: "derivation Y" and xX: "x \ X" and yY: "y \ Y" + shows "(x \ y \ x \ Y) \ x = y \ (y \ x \ y \ X)" +proof- + { fix X Y x y + assume X: "derivation X" and Y: "derivation Y" and xX: "x \ X" and yY: "y \ Y" + interpret X: well_ordered_set X "(\)" using derivation_well_ordered[OF X]. + interpret X.asympartp: transitive X "(\)" using X.asympartp_transitive. + interpret Y: well_ordered_set Y "(\)" using derivation_well_ordered[OF Y]. + have XA: "X \ A" using derivation_A[OF X]. + then have xA: "x \ A" using xX by auto + with f have fxA: "f x \ A" by auto + have YA: "Y \ A" using derivation_A[OF Y]. + then have yA: "y \ A" using yY by auto + with f have fyA: "f y \ A" by auto + { fix Z + assume Z: "Z = {z \ X. z \ x}" + and fZ: "f ` Z \ Z" + and Zx: "extreme_bound A (\) Z x" + and IHx: "\z \ X. z \ x \ (z \ y \ z \ Y) \ z = y \ (y \ z \ y \ X)" + have "(y \ x \ y \ X) \ x \ y" + proof (cases "\z \ Z. y \ z") + case True + then obtain z where zZ: "z \ Z" and yz: "y \ z" by auto + from zZ Z have zX: "z \ X" and zx: "z \ x" by auto + from IHx[rule_format, OF zX zx] yz have yX: "y \ X" by auto + from X.asympartp.trans[OF yz zx yX zX xX] have "y \ x". + with yX show ?thesis by auto + next + case False + have "bound Z (\) y" + proof + fix z assume "z \ Z" + then have zX: "z \ X" and zx: "z \ x" and nyz: "\ y \ z" using Z False by auto + with IHx[rule_format, OF zX zx] X show "z \ y" by auto + qed + with yA Zx have xy: "x \ y" by auto + then show ?thesis by auto + qed + } + note lim_any = this + { fix z Z + assume Z: "Z = {z \ X. z \ x}" + and Zz: "extreme Z (\) z" + and xfz: "x = f z" + and IHx: "(z \ y \ z \ Y) \ z = y \ (y \ z \ y \ X)" + have zX: "z \ X" and zx: "z \ x" using Zz Z by (auto simp: extreme_def) + then have zA: "z \ A" using XA by auto + from IHx have "(y \ x \ y \ X) \ x \ y" + proof (elim disjE conjE) + assume zy: "z \ y" and zY: "z \ Y" + from derivation_useful[OF Y zY yY zy] xfz have xy: "x \ y" by auto + then show ?thesis by auto + next + assume zy: "z = y" + then have "y \ x" using zx by auto + with zy zX show ?thesis by auto + next + assume yz: "y \ z" and yX: "y \ X" + from X.asympartp.trans[OF yz zx yX zX xX] have "y \ x". + with yX show ?thesis by auto + qed + } + note lim_any this + } + note lim_any = this(1) and suc_any = this(2) + interpret X: well_ordered_set X "(\)" using derivation_well_ordered[OF X]. + interpret Y: well_ordered_set Y "(\)" using derivation_well_ordered[OF Y]. + have XA: "X \ A" using derivation_A[OF X]. + have YA: "Y \ A" using derivation_A[OF Y]. + from xX yY show ?thesis + proof (induct x arbitrary: y) + case (less x) + note xX = \x \ X\ and IHx = this(2) + from xX XA f have xA: "x \ A" and fxA: "f x \ A" by auto + from \y \ Y\ + show ?case + proof (induct y) + case (less y) + note yY = \y \ Y\ and IHy = less(2) + from yY YA f have yA: "y \ A" and fyA: "f y \ A" by auto + from X xX show ?case + proof (cases rule: derivation_cases) + case (suc Z z) + note Z = \Z = {z \ X. z \ x}\ and Zz = \extreme Z (\) z\ and xfz = \x = f z\ + then have zx: "z \ x" and zX: "z \ X" by auto + note IHz = IHx[OF zX zx yY] + have 1: "y \ x \ y \ X \ x \ y" using suc_any[OF X Y xX yY Z Zz xfz IHz] IHy by auto + from Y yY show ?thesis + proof (cases rule: derivation_cases) + case (suc W w) + note W = \W = {w \ Y. w \ y}\ and Ww = \extreme W (\) w\ and yfw = \y = f w\ + then have wY: "w \ Y" and wy: "w \ y" by auto + have IHw: "w \ x \ w \ X \ w = x \ x \ w \ x \ Y" using IHy[OF wY wy] by auto + have "x \ y \ x \ Y \ y \ x" using suc_any[OF Y X yY xX W Ww yfw IHw] by auto + with 1 show ?thesis using antisym xA yA by auto + next + case (lim W) + note W = \W = {w \ Y. w \ y}\ and fW = \f ` W \ W\ and Wy = \extreme_bound A (\) W y\ + have "x \ y \ x \ Y \ y \ x" using lim_any[OF Y X yY xX W fW Wy] IHy by auto + with 1 show ?thesis using antisym xA yA by auto + qed + next + case (lim Z) + note Z = \Z = {z \ X. z \ x}\ and fZ = \f ` Z \ Z\ and Zx = \extreme_bound A (\) Z x\ + have 1: "y \ x \ y \ X \ x \ y" using lim_any[OF X Y xX yY Z fZ Zx] IHx[OF _ _ yY] by auto + from Y yY show ?thesis + proof (cases rule: derivation_cases) + case (suc W w) + note W = \W = {w \ Y. w \ y}\ and Ww = \extreme W (\) w\ and yfw = \y = f w\ + then have wY: "w \ Y" and wy: "w \ y" by auto + have IHw: "w \ x \ w \ X \ w = x \ x \ w \ x \ Y" using IHy[OF wY wy] by auto + have "x \ y \ x \ Y \ y \ x" using suc_any[OF Y X yY xX W Ww yfw IHw] by auto + with 1 show ?thesis using antisym xA yA by auto + next + case (lim W) + note W = \W = {w \ Y. w \ y}\ and fW = \f ` W \ W\ and Wy = \extreme_bound A (\) W y\ + have "x \ y \ x \ Y \ y \ x" using lim_any[OF Y X yY xX W fW Wy] IHy by auto + with 1 show ?thesis using antisym xA yA by auto + qed + qed qed qed qed -lemma quasi_fixed_point: "\s \ S. f s \ s" using quasi_fixed_point_in_C S_AA C_def by auto +interpretation derivable: well_ordered_set "{x. derivable x}" "(\)" +proof (rule well_ordered_set.intro) + show "antisymmetric {x. derivable x} (\)" + apply unfold_locales by (auto dest: derivable_A antisym) + show "well_related_set {x. derivable x} (\)" + apply (fold UN_derivations_eq_derivable) + apply (rule lower_UN_well_related) + by (auto dest: derivation_well_ordered derivations_cross_compare well_ordered_set.axioms) +qed -lemma ex_extreme_quasi_fixed_point: - assumes attract: "\q x. f q \ q \ x \ f q \ x \ q" - shows "Ex (extreme (\) {q \ S. f q \ q})" +lemmas derivable_well_ordered = derivable.well_ordered_set_axioms +lemmas derivable_total_ordered = derivable.total_ordered_set_axioms +lemmas derivable_well_related = derivable.well_related_set_axioms + +lemma pred_unique: + assumes X: "derivation X" and xX: "x \ X" + shows "{z \ X. z \ x} = {z. derivable z \ z \ x}" +proof + { fix z assume "z \ X" and "z \ x" + then have "derivable z \ z \ x" using X by (auto simp: derivable_def) + } + then show "{z \ X. z \ x} \ {z. derivable z \ z \ x}" by auto + { fix z assume "derivable z" and zx: "z \ x" + then obtain Y where Y: "derivation Y" and zY: "z \ Y" by (auto simp: derivable_def) + then have "z \ X" using derivations_cross_compare[OF X Y xX zY] zx by auto + } + then show "{z \ X. z \ x} \ {z. derivable z \ z \ x}" by auto +qed + +text \The set of all derivable elements is itself a derivation.\ + +lemma derivation_derivable: "derivation {x. derivable x}" + apply (unfold derivation_def) + apply (safe intro!: derivable_A derivable.well_ordered_set_axioms elim!: derivableE) + apply (unfold mem_Collect_eq pred_unique[symmetric]) + by (auto simp: derivation_def) + +text \Finally, if the set of all derivable elements admits a supremum, then it is a fixed point.\ + +lemma + assumes p: "extreme_bound A (\) {x. derivable x} p" + shows sup_derivable_qfp: "f p \ p" and sup_derivable_fp: "f p = p" +proof (intro antisym sympartpI) + define P where "P \ {x. derivable x}" + have pA: "p \ A" using p by auto + have P: "derivation P" using derivation_derivable by (simp add: P_def) + from derivable_closed have fP: "f ` P \ P" by (auto simp: P_def) + from derivation_lim[OF P fP] p + have pP: "p \ P" by (auto simp: P_def intro:derivableI) + with fP have "f p \ P" by auto + with p show fpp: "f p \ p" by (auto simp: P_def) + show pfp: "p \ f p" apply (rule derivation_infl[rule_format, OF P]) using pP by (auto simp: P_def) + from fpp pfp p f show "f p = p" by (auto intro!: antisym) +qed + +end + +text "The assumptions are satisfied by monotone functions." + +context + assumes mono: "monotone_on A (\) (\) f" +begin + +lemma mono_imp_derivation_infl: + "\X x y. derivation X \ x \ X \ y \ X \ x \ y \ x \ f y" +proof (intro allI impI) + fix X x y + assume X: "derivation X" and xX: "x \ X" and yX: "y \ X" and xy: "x \ y" + interpret X: well_ordered_set X "(\)" using derivation_well_ordered[OF X]. + note XA = derivation_A[OF X] + from xX yX xy show "x \ f y" + proof (induct x) + case (less x) + note IH = this(2) and xX = \x \ X\ and yX = \y \ X\ and xy = \x \ y\ + from xX yX XA have xA: "x \ A" and yA: "y \ A" by auto + from X xX show ?case + proof (cases rule: derivation_cases) + case (suc Z z) + then have zX: "z \ X" and zsx: "z \ x" and xfz: "x = f z" by auto + then have zx: "z \ x" by auto + from X.trans[OF zx xy zX xX yX] have zy: "z \ y". + from zX XA have zA: "z \ A" by auto + from zy monotone_onD[OF mono] zA yA xfz show "x \ f y" by auto + next + case (lim Z) + note Z = \Z = {z \ X. z \ x}\ and Zx = \extreme_bound A (\) Z x\ + from f yA have fyA: "f y \ A" by auto + have "bound Z (\) (f y)" + proof + fix z assume zZ: "z \ Z" + with Z xX have zsx: "z \ x" and zX: "z \ X" by auto + then have zx: "z \ x" by auto + from X.trans[OF zx xy zX xX yX] have zy: "z \ y". + from IH[OF zX zsx yX] zy show "z \ f y" by auto + qed + with Zx fyA show ?thesis by auto + qed + qed +qed + +lemma mono_imp_derivation_f_refl: + "\X x. derivation X \ x \ X \ f x \ f x" +proof (intro allI impI) + fix X x + assume X: "derivation X" and xX: "x \ X" + interpret X: well_ordered_set X "(\)" using derivation_well_ordered[OF X]. + note XA = derivation_A[OF X] + from xX have "x \ x" by auto + from monotone_onD[OF mono this] xX XA show "f x \ f x" by auto +qed + +corollary mono_imp_sup_derivable_fp: + assumes p: "extreme_bound A (\) {x. derivable x} p" + shows "f p = p" + by (simp add: sup_derivable_fp[OF mono_imp_derivation_infl mono_imp_derivation_f_refl p]) + +lemma mono_imp_sup_derivable_lfp: + assumes p: "extreme_bound A (\) {x. derivable x} p" + shows "extreme {q \ A. f q = q} (\) p" +proof (safe intro!: extremeI) + from p show "p \ A" by auto + from sup_derivable_fp[OF mono_imp_derivation_infl mono_imp_derivation_f_refl p] + show "f p = p". + fix q assume qA: "q \ A" and fqq: "f q = q" + have "bound {x. derivable x} (\) q" + proof (safe intro!: boundI elim!:derivableE) + fix x X + assume X: "derivation X" and xX: "x \ X" + from X interpret well_ordered_set X "(\)" by (rule derivation_well_ordered) + from xX show "x \ q" + proof (induct x) + case (less x) + note xP = this(1) and IH = this(2) + with X show ?case + proof (cases rule: derivation_cases) + case (suc Z z) + with IH[of z] have zq: "z \ q" and zX: "z \ X" by auto + from monotone_onD[OF mono zq] zX qA derivation_A[OF X] + show ?thesis by (auto simp: fqq suc) + next + case lim + with IH have "bound {z \ X. z \ x} (\) q" by auto + with lim qA show ?thesis by auto + qed + qed + qed + with p qA show "p \ q" by auto +qed + +lemma mono_imp_ex_least_fp: + assumes comp: "well_complete A (\)" + shows "\p. extreme {q \ A. f q = q} (\) p" proof- - define A where "A \ {a \ S. \s \ S. f s \ s \ a \ s}" - have "A \ AA" - proof (unfold AA_def, intro CollectI conjI allI impI) - show AS: "A \ S" unfolding A_def by auto - { fix x assume xA: "x \ A" - have "f x \ A" - proof (unfold A_def, intro CollectI conjI) - have "x \ S" using xA unfolding A_def by auto - then show "f x \ S" using f_closed_S by auto - { fix s assume sS: "s \ S" and sf: "f s \ s" - then have "x \ s" using xA sS sf A_def by auto - then have "f x \ s" using attract mono - unfolding A_def by (meson monotoneD sf) - } - then show "\s\S. f s \ s \ f x \ s" by auto - qed - } - then show "f ` A \ A" by auto - fix B b assume BA: "B \ A" and b: "extreme_bound_in (\) S B b" - then have "B \ S" unfolding A_def using BA AS by auto - with BA b have bS: "b \ S" by auto - { fix s assume sS: "s \ S" and sf: "f s \ s" - have "bound (\) B s" using sS BA b A_def sf by auto - } - with b have "\s\S. f s \ s \ b \ s" by auto - then show "b \ A" using bS by (auto simp: A_def) - qed - then have "C \ A" by (simp add: C_def Inf_lower) - then have "\a \ A. f a \ a" - using quasi_fixed_point_in_C by auto - then obtain a where aA: "a \ A" and faa: "f a \ a" by auto - with aA A_def have "extreme (\) {q \ S. f q \ q} a" by (auto simp: extreme_def) - then show ?thesis by auto + interpret fixed_point_proof using f by unfold_locales + note as = antisymmetric_axioms + note infl = mono_imp_derivation_infl + note refl = mono_imp_derivation_f_refl + have wr: "well_related_set {x. derivable x} (\)" + using derivable_well_related[OF infl refl]. + have "\p. extreme_bound A (\) {x. derivable x} p" + apply (rule completeD[OF comp]) + using derivable_A wr by auto + then obtain p where p: "extreme_bound A (\) {x. derivable x} p" by auto + from p mono_imp_sup_derivable_lfp[OF p] sup_derivable_qfp[OF infl refl p] + show ?thesis by auto qed end end - -context complete begin - -lemma complete_in_UNIV[intro!]: "complete_in (\) UNIV" - unfolding complete_in_def using complete by auto - -interpretation fixed_point_proof. +end -theorem monotone_imp_ex_quasi_fixed_point: - assumes mono: "monotone (\) (\) f" - shows "\s. f s \ s" +text \Bourbaki-Witt Theorem on well-complete pseudo-ordered set:\ +theorem (in pseudo_ordered_set) well_complete_infl_imp_ex_fp: + assumes comp: "well_complete A (\)" + and f: "f ` A \ A" and infl: "\x \ A. \y \ A. x \ y \ x \ f y" + shows "\p \ A. f p = p" proof- - have Ucl: "f ` UNIV \ UNIV" by auto - obtain s where sC: "s \ C f UNIV" and fss: "f s \ s" - using quasi_fixed_point_in_C[OF mono Ucl complete_in_UNIV] by auto - show "\s. f s \ s" using fss by auto + note as = antisymmetric_axioms + interpret fixed_point_proof using f by unfold_locales + have dinfl: "\X x y. derivation X \ x \ X \ y \ X \ x \ y \ x \ f y" + using infl by (auto dest!:derivation_A) + have drefl: "\X x. derivation X \ x \ X \ f x \ f x" using f by (auto dest!: derivation_A) + have "\p. extreme_bound A (\) {x. derivable x} p" + apply (rule completeD[OF comp]) + using derivable_well_related[OF as dinfl drefl] derivable_A by auto + with sup_derivable_fp[OF as dinfl drefl] + show ?thesis by auto qed -end - -context complete_antisymmetric begin - -corollary monotone_imp_ex_fixed_point: - assumes mono: "monotone (\) (\) f" - shows "\s. f s = s" - using monotone_imp_ex_quasi_fixed_point[OF mono] by auto -end - -subsection \Completeness of Quasi-Fixed Points\ -text \\label{sec:qfp-complete}\ +section \Completeness of (Quasi-)Fixed Points\ -text \We now show that fixed points are complete in a complete trellis, -which strengthens the existing result by Stouti and Maaden who showed the existence of -the least fixed point. Below we derive an even more general result by dropping reflexivity.\ +text \We now prove that, under attractivity, the set of quasi-fixed points is complete.\ -text \We first prove that, under attractivity, the set of quasi-fixed points is complete.\ +definition setwise where "setwise r X Y \ \x\X. \y\Y. r x y" + +lemmas setwiseI[intro] = setwise_def[unfolded atomize_eq, THEN iffD2, rule_format] +lemmas setwiseE[elim] = setwise_def[unfolded atomize_eq, THEN iffD1, elim_format, rule_format] context fixed_point_proof begin -lemma attract_imp_qfp_complete: - assumes comp: "complete (\)" - assumes mono: "monotone (\) (\) f" - assumes attract: "\q x. f q \ q \ x \ f q \ x \ q" - assumes dual_attract: "\q x. f q \ q \ f q \ x \ q \ x" - shows "complete_in (\) {s. f s \ s}" -proof (intro complete_inI) - interpret complete using comp. - fix A assume Afix: "A \ {s. f s \ s}" - define S where "S \ {s. \a \ A. a \ s}" - { fix s a assume as: "\a \ A. a \ s" and aA: "a \ A" +abbreviation setwise_less_eq (infix "\\<^sup>s" 50) where "(\\<^sup>s) \ setwise (\)" + +subsection \Least Quasi-Fixed Points for Attractive Relations.\ + +lemma attract_mono_imp_least_qfp: + assumes attract: "attractive A (\)" + and comp: "well_complete A (\)" + and mono: "monotone_on A (\) (\) f" + shows "\c. extreme {p \ A. f p \ p \ f p = p} (\) c \ f c \ c" +proof- + interpret attractive using attract by auto + interpret sym: transitive A "(\)" using sym_transitive. + define ecl ("[_]\<^sub>\") where "[x]\<^sub>\ \ {y \ A. x \ y} \ {x}" for x + define Q where "Q \ {[x]\<^sub>\ |. x \ A}" + { fix X x assume XQ: "X \ Q" and xX: "x \ X" + then have XA: "X \ A" by (auto simp: Q_def ecl_def) + then have xA: "x \ A" using xX by auto + obtain q where qA: "q \ A" and X: "X = [q]\<^sub>\" using XQ by (auto simp: Q_def) + have xqqx: "x \ q \ x = q" using X xX by (auto simp: ecl_def) + {fix y assume yX: "y \ X" + then have yA: "y \ A" using XA by auto + have "y \ q \ y = q" using yX X by (auto simp: ecl_def) + then have "x \ y \ y = x" using sym_order_trans xqqx xA qA yA by blast + } + then have 1: "X \ [x]\<^sub>\" using X qA by (auto simp: ecl_def) + { fix y assume "y \ A" and "x \ y \ y = x" + then have "q \ y \ y = q" using sym_order_trans xqqx xA qA by blast + } + then have 2: "X \ [x]\<^sub>\" using X xX by (auto simp: ecl_def) + from 1 2 have "X = [x]\<^sub>\" by auto + } + then have XQx: "\X \ Q. \x \ X. X = [x]\<^sub>\" by auto + have RSLE_eq: "X \ Q \ Y \ Q \ x \ X \ y \ Y \ x \ y \ X \\<^sup>s Y" for X Y x y + proof- + assume XQ: "X \ Q" and YQ: "Y \ Q" and xX: "x \ X" and yY: "y \ Y" and xy: "x \ y" + then have XA: "X \ A" and YA: "Y \ A" by (auto simp: Q_def ecl_def) + then have xA: "x \ A" and yA: "y \ A" using xX yY by auto + { fix xp yp assume xpX: "xp \ X" and ypY: "yp \ Y" + then have xpA: "xp \ A" and ypA: "yp \ A" using XA YA by auto + then have "xp \ x \ xp = x" using xpX XQx xX XQ by (auto simp: ecl_def) + then have xpy: "xp \ y" using attract[OF _ _ xy xpA xA yA] xy by blast + have "yp \ y \ yp = y" using ypY XQx yY YQ by (auto simp: ecl_def) + then have "xp \ yp" using dual.attract[OF _ _ xpy ypA yA xpA] xpy by blast + } + then show "X \\<^sup>s Y" using XQ YQ XA YA by auto + qed + have compQ: "well_complete Q (\\<^sup>s)" + proof (intro completeI, safe) + fix XX assume XXQ: "XX \ Q" and XX: "well_related_set XX (\\<^sup>s)" + have BA: "\XX \ A" using XXQ by (auto simp: Q_def ecl_def) + from XX interpret XX: well_related_set XX "(\\<^sup>s)". + interpret UXX: semiattractive "\XX" "(\)" by (rule semiattractive_subset[OF BA]) + have "well_related_set (\XX) (\)" + proof(unfold_locales) + fix Y assume YXX: "Y \ \XX" and Y0: "Y \ {}" + have "{X \ XX. X \ Y \ {}} \ {}" using YXX Y0 by auto + from XX.nonempty_imp_ex_extreme[OF _ this] + obtain E where E: "extreme {X \ XX. X \ Y \ {}} (\\<^sup>s)\<^sup>- E" by auto + then have "E \ Y \ {}" by auto + then obtain e where eE: "e \ E" and eX: "e \ Y" by auto + have "extreme Y (\) e" + proof (intro extremeI eX) + fix x assume xY: "x \ Y" + with YXX obtain X where XXX: "X \ XX" and xX: "x \ X" by auto + with xY E XXX have "E \\<^sup>s X" by auto + with eE xX show "e \ x" by auto + qed + then show "\e. extreme Y (\) e" by auto + qed + with completeD[OF comp BA] + obtain b where extb: "extreme_bound A (\) (\XX) b" by auto + then have bb: "b \ b" using extreme_def bound_def by auto + have bA: "b \ A" using extb extreme_def by auto + then have XQ: "[b]\<^sub>\ \ Q" using Q_def bA by auto + have bX: "b \ [b]\<^sub>\" by (auto simp: ecl_def) + have "extreme_bound Q (\\<^sup>s) XX [b]\<^sub>\" + proof(intro extreme_boundI) + show "[b]\<^sub>\ \ Q" using XQ. + next + fix Y assume YXX: "Y \ XX" + then have YQ: "Y \ Q" using XXQ by auto + then obtain y where yA: "y \ A" and Yy: "Y = [y]\<^sub>\" by (auto simp: Q_def) + then have yY: "y \ Y" by (auto simp: ecl_def) + then have "y \ \XX" using yY YXX by auto + then have "y \ b" using extb by auto + then show "Y \\<^sup>s [b]\<^sub>\" using RSLE_eq[OF YQ XQ yY bX] by auto + next + fix Z assume boundZ: "bound XX (\\<^sup>s) Z" and ZQ: "Z \ Q" + then obtain z where zA: "z \ A" and Zz: "Z = [z]\<^sub>\" by (auto simp: Q_def) + then have zZ: "z \ Z" by (auto simp: ecl_def) + { fix y assume "y \ \XX" + then obtain Y where yY: "y \ Y" and YXX: "Y \ XX" by auto + then have YA: "Y \ A" using XXQ Q_def by (auto simp: ecl_def) + then have "Y \\<^sup>s Z" using YXX boundZ bound_def by auto + then have "y \ z" using yY zZ by auto + } + then have "bound (\XX) (\) z" by auto + then have "b \ z" using extb zA by auto + then show "[b]\<^sub>\ \\<^sup>s Z" using RSLE_eq[OF XQ ZQ bX zZ] by auto + qed + then show "Ex (extreme_bound Q (\\<^sup>s) XX)" by auto + qed + interpret Q: antisymmetric Q "(\\<^sup>s)" + proof + fix X Y assume XY: "X \\<^sup>s Y" and YX: "Y \\<^sup>s X" and XQ: "X \ Q" and YQ: "Y \ Q" + then obtain q where qA: "q \ A" and X: "X = [q]\<^sub>\" using Q_def by auto + then have qX: "q \ X" using X by (auto simp: ecl_def) + then obtain p where pA: "p \ A" and Y: "Y = [p]\<^sub>\" using YQ Q_def by auto + then have pY: "p \ Y" using X by (auto simp: ecl_def) + have pq: "p \ q" using XQ YQ YX qX pY by auto + have "q \ p" using XQ YQ XY qX pY by auto + then have "p \ X" using pq X pA by (auto simp: ecl_def) + then have "X = [p]\<^sub>\" using XQ XQx by auto + then show "X = Y" using Y by (auto simp: ecl_def) + qed + define F where "F X \ {y \ A. \x \ X. y \ f x} \ f ` X" for X + have XQFXQ: "\X. X \ Q \ F X \ Q" + proof- + fix X assume XQ: "X \ Q" + then obtain x where xA: "x \ A" and X: "X = [x]\<^sub>\" using Q_def by auto + then have xX: "x \ X" by (auto simp: ecl_def) + have fxA: "f x \ A" using xA f by auto + have FXA: "F X \ A" using f fxA X by (auto simp: F_def ecl_def) + have "F X = [f x]\<^sub>\" + proof (unfold X, intro equalityI subsetI) + fix z assume zFX: "z \ F [x]\<^sub>\" + then obtain y where yX: "y \ [x]\<^sub>\" and zfy: "z \ f y \ z = f y" by (auto simp: F_def) + have yA: "y \ A" using yX xA by (auto simp: ecl_def) + with f have fyA: "f y \ A" by auto + have zA: "z \ A" using zFX FXA by (auto simp: X) + have "y \ x \ y = x" using X yX by (auto simp: ecl_def) + then have "f y \ f x \ f y = f x" using mono xA yA by (auto simp: monotone_on_def) + then have "z \ f x \ z = f x" using zfy sym.trans[OF _ _ zA fyA fxA] by (auto simp:) + with zA show "z \ [f x]\<^sub>\" by (auto simp: ecl_def) + qed (auto simp: xX F_def ecl_def) + with FXA show "F X \ Q" by (auto simp: Q_def ecl_def) + qed + then have F: "F ` Q \ Q" by auto + then interpret Q: fixed_point_proof Q "(\\<^sup>s)" F by unfold_locales + have monoQ: "monotone_on Q (\\<^sup>s) (\\<^sup>s) F" + proof (intro monotone_onI) + fix X Y assume XQ: "X \ Q" and YQ: "Y \ Q" and XY: "X \\<^sup>s Y" + then obtain x y where xX: "x \ X" and yY: "y \ Y" using Q_def by (auto simp: ecl_def) + then have xA: "x \ A" and yA: "y \ A" using XQ YQ by (auto simp: Q_def ecl_def) + have "x \ y" using XY xX yY by auto + then have fxfy: "f x \ f y" using monotone_on_def[of A "(\)" "(\)" f] xA yA mono by auto + have fxgX: "f x \ F X" using xX F_def by blast + have fygY: "f y \ F Y" using yY F_def by blast + show "F X \\<^sup>s F Y" using RSLE_eq[OF XQFXQ[OF XQ] XQFXQ[OF YQ] fxgX fygY fxfy]. + qed + have QdA: "{x. Q.derivable x} \ Q" using Q.derivable_A by auto + note asQ = Q.antisymmetric_axioms + note infl = Q.mono_imp_derivation_infl[OF asQ monoQ] + note f_refl = Q.mono_imp_derivation_f_refl[OF asQ monoQ] + from Q.mono_imp_ex_least_fp[OF asQ monoQ compQ] + obtain P where P: "extreme {q \ Q. F q = q} (\\<^sup>s)\<^sup>- P" by auto + then have PQ: "P \ Q" by (auto simp: extreme_def) + from P have FPP: "F P = P" using PQ by auto + with P have PP: "P \\<^sup>s P" by auto + from P obtain p where pA: "p \ A" and Pp: "P = [p]\<^sub>\" using Q_def by auto + then have pP: "p \ P" by (auto simp: ecl_def) + then have fpA: "f p \ A" using pA f by auto + have "f p \ F P" using pP F_def fpA by auto + then have "F P = [f p]\<^sub>\" using XQx XQFXQ[OF PQ] by auto + then have fp: "f p \ p \ f p = p" using pP FPP by (auto simp: ecl_def) + have "p \ p" using PP pP by auto + with fp have fpp: "f p \ p" by auto + have e: "extreme {p \ A. f p \ p \ f p = p} (\) p" + proof (intro extremeI CollectI conjI pA fp, elim CollectE conjE) + fix q assume qA: "q \ A" and fq: "f q \ q \ f q = q" + define Z where "Z \ {z \ A. q \ z}\{q}" + then have qZ: "q \ Z" using qA by auto + then have ZQ: "Z \ Q" using qA by (auto simp: Z_def Q_def ecl_def) + have fqA: "f q \ A" using qA f by auto + then have "f q \ Z" using fq by (auto simp: Z_def) + then have 1: "Z = [f q]\<^sub>\" using XQx ZQ by auto + then have "f q \ F Z" using qZ fqA by (auto simp: F_def) + then have "F Z = [f q]\<^sub>\" using XQx XQFXQ[OF ZQ] by auto + with 1 have "Z = F Z" by auto + then have "P \\<^sup>s Z" using P ZQ by auto + then show "p \ q" using pP qZ by auto + qed + with fpp show ?thesis using e by auto +qed + +subsection \General Completeness\ + +lemma attract_mono_imp_fp_qfp_complete: + assumes attract: "attractive A (\)" + and comp: "CC-complete A (\)" + and wr_CC: "\C \ A. well_related_set C (\) \ C \ CC" + and extend: "\X \ CC. \Y \ CC. X \\<^sup>s Y \ X \ Y \ CC" + and mono: "monotone_on A (\) (\) f" + and P: "P \ {x \ A. f x = x}" + shows "CC-complete ({q \ A. f q \ q} \ P) (\)" +proof (intro completeI) + interpret attractive using attract. + fix X assume Xfix: "X \ {q \ A. f q \ q} \ P" and XCC: "X \ CC" + with P have XA: "X \ A" by auto + define B where "B \ {b \ A. \a \ X. a \ b}" + { fix s a assume sA: "s \ A" and as: "\a \ X. a \ s" and aX: "a \ X" + then have aA: "a \ A" using XA by auto + then have fafs: "f a \ f s" using mono f aX sA as by (auto elim!: monotone_onE) have "a \ f s" - proof (rule dual_attract[rule_format]) - have "a \ s" using as aA by auto - then show "f a \ f s" using mono by (simp add: monotone_def) - show "f a \ a" using Afix aA by auto + proof (cases "f a = a") + case True + then show ?thesis using fafs by auto + next + case False + then have "a \ f a" using P aX Xfix by auto + also from fafs have "f a \ f s" by auto + finally show ?thesis using f aA sA by auto qed } - then have f_closed_S: "f ` S \ S" unfolding S_def by auto - have comp_S_dual: "complete_in (\) S" - proof (unfold complete_in_def, intro allI impI) - fix B assume BS: "B \ S" - then obtain b where bB: "extreme_bound (\) B b" using dual.complete by auto - show "Ex (extreme_bound_in (\) S B)" - proof (intro exI extreme_bound_inI) - { fix a assume aA: "a \ A" - then have "\c \ B. a \ c" using BS aA S_def by auto - then have "a \ b" using bB by blast + with f have fBB: "f ` B \ B" unfolding B_def by auto + have BA: "B \ A" by (auto simp: B_def) + have compB: "CC-complete B (\)" + proof (unfold complete_def, intro allI impI) + fix Y assume YS: "Y \ B" and YCC: "Y \ CC" + with BA have YA: "Y \ A" by auto + define C where "C \ X\Y" + then have CA: "C \ A" using XA YA C_def by auto + have XY: "X \\<^sup>s Y" using B_def YS by auto + then have CCC: "C \ CC" using extend XA YA XCC YCC C_def by auto + then obtain s where s: "extreme_bound A (\) C s" + using completeD[OF comp CA CCC] by auto + then have sA: "s \ A" by auto + show "Ex (extreme_bound B (\) Y)" + proof (intro exI extreme_boundI) + { fix x assume "x \ X" + then have "x \ s" using s C_def by auto } - then show "b \ S" unfolding S_def by auto - show "x \ B \ b \ x" for x using bB by auto - fix c assume "bound (\) B c" - then show "c \ b" using bB by blast + then show "s \ B" using sA B_def by auto + next + fix y assume "y \ Y" + then show "y \ s" using s C_def using extremeD by auto + next + fix c assume cS: "c \ B" and "bound Y (\) c" + then have "bound C (\) c" using C_def B_def by auto + then show "s \ c" using s BA cS by auto qed qed - then have comp_S: "complete_in (\) S" using complete_in_dual by auto - then obtain L where LefpS: "extreme (\) {q \ S. f q \ q} L" - using ex_extreme_quasi_fixed_point[OF mono f_closed_S comp_S attract] - by auto - show "Ex (extreme_bound_in (\) {s. f s \ s} A)" - proof (intro exI extreme_bound_inI) - show "L \ {s. f s \ s}" using LefpS by auto - fix a assume "a \ A" - with LefpS show "a \ L" by (auto simp: S_def) + from fBB interpret B: fixed_point_proof B "(\)" f by unfold_locales + from BA have *: "{x \ A. f x \ x} \ B = {x \ B. f x \ x}" by auto + have asB: "attractive B (\)" using attractive_subset[OF BA] by auto + have monoB: "monotone_on B (\) (\) f" using monotone_on_cmono[OF BA] mono by (auto dest!: le_funD) + have compB: "well_complete B (\)" + using wr_CC compB BA by (simp add: complete_def) + from B.attract_mono_imp_least_qfp[OF asB compB monoB] + obtain l where "extreme {p \ B. f p \ p \ f p = p} (\) l" and fll: "f l \ l" by auto + with P have l: "extreme ({p \ B. f p \ p} \ P \ B) (\) l" by auto + show "Ex (extreme_bound ({q \ A. f q \ q} \ P) (\) X)" + proof (intro exI extreme_boundI) + show "l \ {q \ A. f q \ q} \ P" using l BA by auto + fix a assume "a \ X" + with l show "a \ l" by (auto simp: B_def) next - fix c assume c: "bound (\) A c" and cfix: "c \ {s. f s \ s}" - from c have "c \ S" by (auto simp: S_def) - with cfix show "L \ c" using LefpS c by auto + fix c assume c: "bound X (\) c" and cfix: "c \ {q \ A. f q \ q} \ P" + with P have cA: "c \ A" by auto + with c have "c \ B" by (auto simp: B_def) + with cfix l show "l \ c" by auto qed qed -end - -context complete_attractive begin - -interpretation fixed_point_proof. - -theorem monotone_imp_quasi_fixed_points_complete: - assumes mono: "monotone (\) (\) f" - shows "complete_in (\) {s. f s \ s}" - by (rule attract_imp_qfp_complete[OF complete_axioms mono], auto dest: attract dual.attract) +lemma attract_mono_imp_qfp_complete: + assumes "attractive A (\)" + and "CC-complete A (\)" + and "\C \ A. well_related_set C (\) \ C \ CC" + and "\X \ CC. \Y \ CC. X \\<^sup>s Y \ X \ Y \ CC" + and "monotone_on A (\) (\) f" + shows "CC-complete {p \ A. f p \ p} (\)" + using attract_mono_imp_fp_qfp_complete[OF assms, of "{}"] by simp -end - - -text \The next lemma shows that in a complete relation, two related sets of -strict fixed points have a quasi-fixed point in between.\ - -context fixed_point_proof begin - -lemma qfp_interpolant: - assumes comp: "complete (\)" and mono: "monotone (\) (\) f" - and AB: "\a \ A. \b \ B. a \ b" - and Afp: "\a \ A. f a = a" - and Bfp: "\b \ B. f b = b" - shows "\t. (f t \ t) \ (\a \ A. a \ t) \ (\b \ B. t \ b)" +lemma antisym_mono_imp_fp_complete: + assumes anti: "antisymmetric A (\)" + and comp: "CC-complete A (\)" + and wr_CC: "\C \ A. well_related_set C (\) \ C \ CC" + and extend: "\X \ CC. \Y \ CC. X \\<^sup>s Y \ X \ Y \ CC" + and mono: "monotone_on A (\) (\) f" + shows "CC-complete {p \ A. f p = p} (\)" proof- - interpret complete using comp. - define T where "T \ {t. (\a \ A. a \ t) \ (\b \ B. t \ b)}" - have f_closed_T: "f ` T \ T" - proof safe - fix t assume tT: "t \ T" - show "f t \ T" - proof (unfold T_def, safe) - fix a assume aA: "a \ A" - with tT monotoneD[OF mono] - have "f a \ f t" by (auto simp: T_def) - with Afp aA show "a \ f t" by auto - next - fix b assume bB: "b \ B" - with tT monotoneD[OF mono] - have "f t \ f b" by (auto simp: T_def) - with Bfp bB show "f t \ b" by auto - qed - qed - have T_comp: "complete_in (\) T" - proof - fix U assume UT: "U \ T" - obtain k where k: "extreme_bound (\) (U \ A) k" using complete by auto - have "extreme_bound_in (\) T U k" - proof (intro extreme_bound_inI) - { fix b assume "b \ B" - with AB T_def UT have "\x \ U \ A. x \ b" by auto - with k have "k \ b" by auto - } - with k T_def show "k \ T" by auto - next - fix x assume "x \ U" - with k show "x \ k" by auto - next - fix l - assume "bound (\) U l" and "l \ T" - then have "\a \ U \ A. a \ l" by (auto simp: T_def) - with k show "k \ l" by auto - qed - then show "Ex (extreme_bound_in (\) T U)" by auto - qed - obtain t where "t \ T" and "f t \ t" - using quasi_fixed_point - by (meson T_comp f_closed_T mono) - then show ?thesis by (auto simp: T_def) + interpret antisymmetric using anti. + have *: "{q \ A. f q \ q} \ {p \ A. f p = p}" using f by (auto intro!: antisym) + from * attract_mono_imp_fp_qfp_complete[OF attractive_axioms comp wr_CC extend mono, of "{p\A. f p = p}"] + show ?thesis by (auto simp: subset_Un_eq) qed end -text \From this, we deduce that the set of strict fixed-points is also complete, assuming -only antisymmetry and attractivity.\ - -context complete_antisymmetric begin - -interpretation fixed_point_proof. - -context - fixes f assumes mono: "monotone (\) (\) f" -begin +subsection \Instances\ -theorem monotone_imp_fixed_points_complete: - shows "complete_in (\) {s. f s = s}" -proof - fix A assume "A \ {s. f s = s}" - then have Afp: "\a\A. f a = a" by auto - define S where "S \ {s. \a \ A. a \ s}" - have f_closed_S: "f ` S \ S" - proof safe - fix s assume sS: "s \ S" - show "f s \ S" - proof(unfold S_def, safe) - fix a assume aA: "a \ A" - then have "f a \ f s" using S_def sS mono by (auto dest:monotoneD) - then show "a \ f s" using Afp aA by auto - qed - qed - have "complete_in (\) S" - proof - fix B assume BS: "B \ S" - obtain L where BL: "extreme_bound (\) B L" using dual.complete by blast - have "extreme_bound_in (\) S B L" - proof (intro extreme_bound_inI) - { fix a assume aA: "a \ A" - then have "\s \ B. a \ s" using BS S_def by auto - } - then have "\a \ A. a \ L" using BL by (simp add: extreme_bound_iff) - then show "L \ S" using S_def by auto - show "b \ B \ L \ b" for b using BL by auto - show "\c. bound (\) B c \ c \ L" using BL by (auto elim!: boundE) - qed - then show "Ex (extreme_bound_in (\) S B)" by auto - qed - then have comp_S: "complete_in (\) S" using complete_in_dual by auto - have "Ex (extreme (\) {q \ S. f q \ q})" - apply (rule ex_extreme_quasi_fixed_point[OF mono f_closed_S comp_S]) - by auto - then obtain q where q: "extreme (\) {q \ S. f q \ q \ q \ f q} q" by auto - have "extreme_bound_in (\) {s. f s = s} A q" - proof (intro extreme_bound_inI) - show qfp: "q \ {s. f s = s}" using q by auto - show Aq: "\a. a \ A \ a \ q" using q S_def by auto - fix c assume "bound (\) A c" and "c \ {s. f s = s}" - then have cfp: "f c = c" and Ac: "\a \ A. a \ c" by auto - define D where [simp]: "D \ {c,q}" - have AD: "\a \ A. \d \ D. a \ d" using Aq Ac by auto - then have Dfp: "\d\D. f d = d" using qfp cfp by auto - then obtain t where t: "(f t \ t) \ (\a \ A. a \ t) \ (\d \ D. t \ d)" - using qfp_interpolant[OF complete_axioms mono AD Afp Dfp] - by auto - then have tq: "t \ q" by auto - have "q \ t" using t q by (auto simp: S_def) - with tq have "q = t" by auto - also have "t \ c" using t by auto - finally show "q \ c". - qed - then show "Ex (extreme_bound_in (\) {s. f s = s} A)" by auto -qed +subsubsection \Instances under attractivity\ -corollary monotone_imp_ex_extreme_fixed_point: - shows "Ex (extreme (\) {s. f s = s})" - using complete_inD[OF monotone_imp_fixed_points_complete, of "{}"] - by auto +context attractive begin -end +interpretation less_eq_notations. + +text \Full completeness\ +theorem mono_imp_qfp_UNIV_complete: + assumes comp: "UNIV-complete A (\)" and f: "f ` A \ A" and mono: "monotone_on A (\) (\) f" + shows "UNIV-complete {p \ A. f p \ p} (\)" + apply (intro fixed_point_proof.attract_mono_imp_qfp_complete comp mono) + apply unfold_locales + by (auto simp: f) + +text \Connex completeness\ +theorem mono_imp_qfp_connex_complete: + assumes comp: "{X. connex X (\)}-complete A (\)" + and f: "f ` A \ A" and mono: "monotone_on A (\) (\) f" + shows "{X. connex X (\)}-complete {p \ A. f p \ p} (\)" + apply (intro fixed_point_proof.attract_mono_imp_qfp_complete mono comp) + apply unfold_locales + by (auto simp: f intro: connex_union well_related_set.connex_axioms) + +text \Directed completeness\ +theorem mono_imp_qfp_directed_complete: + assumes comp: "{X. directed X (\)}-complete A (\)" + and f: "f ` A \ A" and mono: "monotone_on A (\) (\) f" + shows "{X. directed X (\)}-complete {p \ A. f p \ p} (\)" + apply (intro fixed_point_proof.attract_mono_imp_qfp_complete mono comp) + apply unfold_locales + by (auto simp: f intro!: directed_extend intro: well_related_set.connex_axioms connex.directed) + +text \Well Completeness\ +theorem mono_imp_qfp_well_complete: + assumes comp: "well_complete A (\)" + and f: "f ` A \ A" and mono: "monotone_on A (\) (\) f" + shows "well_complete {p \ A. f p \ p} (\)" + apply (intro fixed_point_proof.attract_mono_imp_qfp_complete mono comp) + apply unfold_locales + by (auto simp: f well_related_extend) end -section \Kleene-Style Fixed Point Theorem\ - -text \Kleene's fixed-point theorem states that, -for a pointed directed complete partial order $\tp{A,\SLE}$ -and a Scott-continuous map $f: A \to A$, -the supremum of $\set{f^n(\bot) \mid n\in\Nat}$ exists in $A$ and is a least -fixed point. -Mashburn \cite{mashburn83} generalized the result so that -$\tp{A,\SLE}$ is a $\omega$-complete partial order -and $f$ is $\omega$-continuous. - -In this section we further generalize the result and show that -for $\omega$-complete relation $\tp{A,\SLE}$ -and for every bottom element $\bot \in A$, -the set $\set{f^n(\bot) \mid n\in\Nat}$ has suprema (not necessarily unique, of -course) and, -they are quasi-fixed points. -Moreover, if $(\SLE)$ is attractive, then the suprema are precisely the least -quasi-fixed points.\ - -subsection \Scott Continuity, $\omega$-Completeness, $\omega$-Continuity\ - -text \In this Section, we formalize $\omega$-completeness, Scott continuity and $\omega$-continuity. -We then prove that a Scott continuous map is $\omega$-continuous and that an $\omega$-continuous -map is ``nearly'' monotone.\ - -context - fixes less_eq :: "'a \ 'a \ bool" (infix "\" 50) -begin - -definition "omega_continuous f \ \c :: nat \ 'a. \ b. - monotone (\) (\) c \ - extreme_bound (\) (range c) b \ extreme_bound (\) (f ` range c) (f b)" - -lemma omega_continuousI[intro?]: - assumes "\c :: nat \ 'a. \ b. - monotone (\) (\) c \ - extreme_bound (\) (range c) b \ extreme_bound (\) (f ` range c) (f b)" - shows "omega_continuous f" - using assms by (auto simp: omega_continuous_def) +subsubsection \Usual instances under antisymmetry \ -lemma omega_continuousE[elim]: - assumes "omega_continuous f" - and "(\c :: nat \ 'a. \ b. monotone (\) (\) c \ - extreme_bound (\) (range c) b \ extreme_bound (\) (f ` range c) (f b) - ) \ thesis" - shows "thesis" - using assms by (auto simp: omega_continuous_def) - -lemma omega_continuous_imp_mono_refl: - assumes cont: "omega_continuous f" - and xy: "x \ y" and xx: "x \ x" and yy: "y \ y" - shows "f x \ f y" -proof- - define c :: "nat \ 'a" where "c \ \i. if i = 0 then x else y" - from xx xy yy have monoc: "monotone (\) (\) c" - by (auto simp: c_def intro!: monotoneI) - have "extreme_bound (\) (range c) y" using xy yy by (auto simp: c_def) - then have fboy: "extreme_bound (\) (f ` range c) (f y)" using monoc cont by auto - then show "f x \ f y" by (auto simp: c_def) -qed - -definition "scott_continuous f \ - \D b. directed (\) D \ extreme_bound (\) D b \ extreme_bound (\) (f ` D) (f b)" +context antisymmetric begin -lemma scott_continuousI[intro?]: - assumes "\D b. directed (\) D \ extreme_bound (\) D b \ extreme_bound (\) (f ` D) (f b)" - shows "scott_continuous f" - using assms by (auto simp: scott_continuous_def) - -lemma scott_continuousE[elim]: - assumes "scott_continuous f" - and "(\D b. directed (\) D \ - extreme_bound (\) D b \ extreme_bound (\) (f ` D) (f b)) \ thesis" - shows "thesis" - using assms by (auto simp: scott_continuous_def) - -lemma scott_continuous_imp_mono_refl: - assumes scott: "scott_continuous f" - and xy: "x \ y" and yy: "y \ y" - shows "f x \ f y" +text \Knaster--Tarski\ +theorem mono_imp_fp_complete: + assumes comp: "UNIV-complete A (\)" + and f: "f ` A \ A" and mono: "monotone_on A (\) (\) f" + shows "UNIV-complete {p \ A. f p = p} (\)" proof- - define D where "D \ {x,y}" - from xy yy have dir_D -: "directed (\) D" by (auto simp: D_def intro!: bexI[of _ y]) - have "extreme_bound (\) D y" using xy yy by (auto simp: D_def) - then have fboy: "extreme_bound (\) (f ` D) (f y)" using dir_D scott by auto - then show "f x \ f y" by (auto simp: D_def) -qed - -lemma scott_continuous_imp_omega_continuous: - assumes scott: "scott_continuous f" shows "omega_continuous f" -proof - fix c :: "nat \ 'a" - assume "monotone (\) (\) c" - from monotone_directed_image[OF this order.dual.dual.directed_UNIV] scott - show "extreme_bound (\) (range c) b \ extreme_bound (\) (f ` range c) (f b)" for b + interpret fixed_point_proof using f by unfold_locales + show ?thesis + apply (intro antisym_mono_imp_fp_complete mono antisymmetric_axioms comp) by auto qed -end - -subsection \Kleene's Fixed-Point Theorem\ - -text \The first part of Kleene's theorem demands to prove that the set -$\set{f^n(\bot) \mid n \in \Nat}$ has a supremum and -that all such are quasi-fixed points. We prove this claim without assuming -anything on the relation $\SLE$ besides $\omega$-completeness and one bottom element.\ - -context fixed_point_proof begin - -context - fixes f - assumes comp: "omega_complete (\)" - assumes cont: "omega_continuous (\) f" - fixes bot ("\<^bold>\") - assumes bot: "\q. \<^bold>\ \ q" -begin - -interpretation omega_complete "(\)" using comp. - -abbreviation(input) fn where "fn n \ (f ^^ n) \<^bold>\" - -abbreviation(input) "Fn \ range fn" - -lemma fn_ref: "fn n \ fn n" - using omega_continuous_imp_mono_refl[OF cont] bot by (induct n, auto) - -lemma fn_monotone: "monotone (\) (\) fn" -proof - fix n m :: nat - assume "n \ m" - from le_Suc_ex[OF this] obtain k where m: "m = n + k" by auto - from bot fn_ref omega_continuous_imp_mono_refl[OF cont] - show "fn n \ fn m" by (unfold m, induct n, auto) +text \Markowsky 1976\ +theorem mono_imp_fp_connex_complete: + assumes comp: "{X. connex X (\)}-complete A (\)" + and f: "f ` A \ A" and mono: "monotone_on A (\) (\) f" + shows "{X. connex X (\)}-complete {p \ A. f p = p} (\)" +proof- + interpret fixed_point_proof using f by unfold_locales + show ?thesis + apply (intro antisym_mono_imp_fp_complete antisymmetric_axioms mono comp) + by (auto intro: connex_union well_related_set.connex_axioms) qed -lemma ex_kleene_fixed_point: - shows "Ex (extreme_bound (\) Fn)" - using monotone_seq_complete[OF fn_monotone] by auto - -lemma kleene_fixed_point_is_fixed: - assumes q: "extreme_bound (\) Fn q" - shows "f q \ q" -proof - have fq: "extreme_bound (\) (f ` Fn) (f q)" - using q cont fn_monotone by auto - with bot have nq: "fn n \ f q" for n - by(induct n, auto simp: extreme_bound_iff) - then show "q \ f q" using q by blast - have "f (fn n) \ range fn" for n by (auto intro!: range_eqI[of _ _ "Suc n"]) - then have "f ` Fn \ Fn" by auto - then show "f q \ q" using q fq - by (metis (no_types, lifting) bound_cmono extreme_def mem_Collect_eq) +text \Pataraia\ +theorem mono_imp_fp_directed_complete: + assumes comp: "{X. directed X (\)}-complete A (\)" + and f: "f ` A \ A" and mono: "monotone_on A (\) (\) f" + shows "{X. directed X (\)}-complete {p \ A. f p = p} (\)" +proof- + interpret fixed_point_proof using f by unfold_locales + show ?thesis + apply (intro antisym_mono_imp_fp_complete mono antisymmetric_axioms comp) + by (auto intro: directed_extend connex.directed well_related_set.connex_axioms) qed -lemma kleene_fixed_point_is_dual_extreme: - assumes attract: "\q x. f q \ q \ x \ f q \ x \ q" - assumes q: "extreme_bound (\) Fn q" - shows "extreme (\) {s. f s \ s} q" -proof(intro extremeI, unfold mem_Collect_eq, intro kleene_fixed_point_is_fixed[OF q]) - fix c assume cqfp: "f c \ c" - { - fix n::nat - have "fn n \ c" - proof(induct n) - case 0 - show ?case using bot by auto - next - case IH: (Suc n) - have "c \ c" using attract cqfp by blast - with IH have "fn (Suc n) \ f c" - using omega_continuous_imp_mono_refl[OF cont] fn_ref by auto - then show ?case using attract cqfp by blast - qed - } - then show "q \ c" using q by blast -qed - -lemma kleene_fixed_point_iff_dual_extreme: - assumes attract: "\q x. f q \ q \ x \ f q \ x \ q" - assumes dual_attract: "\p q x. p \ q \ q \ x \ p \ x" - shows "extreme_bound (\) Fn = extreme (\) {s. f s \ s}" -proof (intro ext iffI kleene_fixed_point_is_dual_extreme[OF attract]) - fix q - assume q: "extreme (\) {s. f s \ s} q" - from q have fqq: "f q \ q" by auto - from ex_kleene_fixed_point obtain k where k: "extreme_bound (\) Fn k" by auto - have qk: "q \ k" - proof - from kleene_fixed_point_is_fixed[OF k] q - show "q \ k" by auto - from kleene_fixed_point_is_dual_extreme[OF _ k] q attract - show "k \ q" by blast - qed - show "extreme_bound (\) Fn q" - proof (intro extreme_boundI,safe) - fix n - show "(f ^^ n) \<^bold>\ \ q" - apply (induct n, auto intro: bot[rule_format]) - by (meson attract fn_ref fqq omega_continuous_imp_mono_refl[OF cont]) - next - fix x - assume "bound (\) Fn x" - with k have kx: "k \ x" by auto - with dual_attract[rule_format, OF qk] - show "q \ x" by auto - qed +text \Bhatta \& George 2011\ +theorem mono_imp_fp_well_complete: + assumes comp: "well_complete A (\)" + and f: "f ` A \ A" and mono: "monotone_on A (\) (\) f" + shows "well_complete {p \ A. f p = p} (\)" +proof- + interpret fixed_point_proof using f by unfold_locales + show ?thesis + apply (intro antisym_mono_imp_fp_complete mono antisymmetric_axioms comp) + by (auto intro!: antisym well_related_extend) qed end end - -context omega_complete begin - -interpretation fixed_point_proof. - -theorem kleene_quasi_fixed_point: - assumes "omega_continuous (\) f" and "\x. bo \ x" - shows "\p. extreme_bound (\) {(f ^^ n) bo |. n :: nat} p" - and "extreme_bound (\) {(f ^^ n) bo |. n :: nat} p \ f p \ p" - using ex_kleene_fixed_point[OF omega_complete_axioms assms] - using kleene_fixed_point_is_fixed[OF omega_complete_axioms assms]. - -end - -text \Kleene's theorem also states that the quasi-fixed point found this way is a least one. -Again, attractivity is needed to prove this statement.\ - -context attractive begin - -interpretation fixed_point_proof. - -corollary kleene_quasi_fixed_point_dual_extreme: - assumes "omega_complete (\)" and "omega_continuous (\) f" and "\x. bo \ x" - shows "extreme_bound (\) {(f ^^ n) bo |. n :: nat} = extreme (\) {s. f s \ s}" - apply (rule kleene_fixed_point_iff_dual_extreme[OF assms]) - by (auto dest: attract dual.attract) - -end - -context antisymmetric begin - -interpretation fixed_point_proof. - -corollary kleene_fixed_point_is_fixed: - assumes "omega_complete (\)" and "omega_continuous (\) f" and "\x. bo \ x" - and "extreme_bound (\) {(f ^^ n) bo |. n :: nat} p" - shows "f p = p" - using kleene_fixed_point_is_fixed[OF assms] by auto - -end - -end \ No newline at end of file diff --git a/thys/Complete_Non_Orders/Kleene_Fixed_Point.thy b/thys/Complete_Non_Orders/Kleene_Fixed_Point.thy new file mode 100644 --- /dev/null +++ b/thys/Complete_Non_Orders/Kleene_Fixed_Point.thy @@ -0,0 +1,291 @@ +theory Kleene_Fixed_Point + imports Complete_Relations +begin + + +section \Iterative Fixed Point Theorem\ + +text \Kleene's fixed-point theorem states that, +for a pointed directed complete partial order $\tp{A,\SLE}$ +and a Scott-continuous map $f: A \to A$, +the supremum of $\set{f^n(\bot) \mid n\in\Nat}$ exists in $A$ and is a least +fixed point. +Mashburn \cite{mashburn83} generalized the result so that +$\tp{A,\SLE}$ is a $\omega$-complete partial order +and $f$ is $\omega$-continuous. + +In this section we further generalize the result and show that +for $\omega$-complete relation $\tp{A,\SLE}$ +and for every bottom element $\bot \in A$, +the set $\set{f^n(\bot) \mid n\in\Nat}$ has suprema (not necessarily unique, of +course) and, +they are quasi-fixed points. +Moreover, if $(\SLE)$ is attractive, then the suprema are precisely the least +quasi-fixed points.\ + +subsection \Scott Continuity, $\omega$-Completeness, $\omega$-Continuity\ + +text \In this Section, we formalize $\omega$-completeness, Scott continuity and $\omega$-continuity. +We then prove that a Scott continuous map is $\omega$-continuous and that an $\omega$-continuous +map is ``nearly'' monotone.\ + +context + fixes A :: "'a set" and less_eq :: "'a \ 'a \ bool" (infix "\" 50) +begin + +definition "omega_continuous f \ + f ` A \ A \ + (\c :: nat \ 'a. \ b \ A. + range c \ A \ + monotone (\) (\) c \ + extreme_bound A (\) (range c) b \ extreme_bound A (\) (f ` range c) (f b))" + +lemmas omega_continuousI[intro?] = + omega_continuous_def[unfolded atomize_eq, THEN iffD2, unfolded conj_imp_eq_imp_imp, rule_format] + +lemmas omega_continuousDdom = + omega_continuous_def[unfolded atomize_eq, THEN iffD1, unfolded conj_imp_eq_imp_imp, THEN conjunct1] + +lemmas omega_continuousD = + omega_continuous_def[unfolded atomize_eq, THEN iffD1, unfolded conj_imp_eq_imp_imp, THEN conjunct2, rule_format] + +lemmas omega_continuousE[elim] = + omega_continuous_def[unfolded atomize_eq, THEN iffD1, elim_format, unfolded conj_imp_eq_imp_imp, rule_format] + +lemma omega_continuous_imp_mono_refl: + assumes cont: "omega_continuous f" + and x: "x \ A" and y: "y \ A" + and xy: "x \ y" and xx: "x \ x" and yy: "y \ y" + shows "f x \ f y" +proof- + define c :: "nat \ 'a" where "c \ \i. if i = 0 then x else y" + from x y xx xy yy have c: "range c \ A" "monotone (\) (\) c" + by (auto simp: c_def intro!: monotoneI) + have "extreme_bound A (\) (range c) y" using xy yy x y by (auto simp: c_def) + then have fboy: "extreme_bound A (\) (f ` range c) (f y)" using c cont y by auto + then show "f x \ f y" by (auto simp: c_def) +qed + +definition "scott_continuous f \ + f ` A \ A \ + (\X s. X \ A \ directed X (\) \ extreme_bound A (\) X s \ extreme_bound A (\) (f ` X) (f s))" + +lemmas scott_continuousI[intro?] = + scott_continuous_def[unfolded atomize_eq, THEN iffD2, unfolded conj_imp_eq_imp_imp, rule_format] + +lemmas scott_continuousE[elim] = + scott_continuous_def[unfolded atomize_eq, THEN iffD1, elim_format, unfolded conj_imp_eq_imp_imp, rule_format] + +lemma scott_continuous_imp_mono_refl: + assumes scott: "scott_continuous f" + and x: "x \ A" and y: "y \ A" and xy: "x \ y" and yy: "y \ y" + shows "f x \ f y" +proof- + define D where "D \ {x,y}" + from x y xy yy have dir_D: "D \ A" "directed D (\)" + by (auto simp: D_def intro!: bexI[of _ y] directedI) + have "extreme_bound A (\) D y" using xy yy x y by (auto simp: D_def) + then have fboy: "extreme_bound A (\) (f ` D) (f y)" using dir_D scott by auto + then show "f x \ f y" by (auto simp: D_def) +qed + +lemma scott_continuous_imp_omega_continuous: + assumes scott: "scott_continuous f" shows "omega_continuous f" +proof + from scott show "f ` A \ A" by auto + fix c :: "nat \ 'a" + assume mono: "monotone (\) (\) c" and c: "range c \ A" + from monotone_directed_image[OF mono[folded monotone_on_UNIV] order.directed] scott c + show "extreme_bound A (\) (range c) b \ extreme_bound A (\) (f ` range c) (f b)" for b + by auto +qed + +end + +subsection \Existence of Iterative Fixed Points\ + +text \The first part of Kleene's theorem demands to prove that the set +$\set{f^n(\bot) \mid n \in \Nat}$ has a supremum and +that all such are quasi-fixed points. We prove this claim without assuming +anything on the relation $\SLE$ besides $\omega$-completeness and one bottom element.\ + +(* +no_notation power (infixr "^" 80) +*) +notation compower ("_^_"[1000,1000]1000) + +lemma mono_funpow: assumes f: "f ` A \ A" and mono: "monotone_on A r r f" + shows "monotone_on A r r (f^n)" +proof (induct n) + case 0 + show ?case using monotone_on_id by (auto simp: id_def) +next + case (Suc n) + with funpow_dom[OF f] show ?case + by (auto intro!: monotone_onI monotone_onD[OF mono] elim!:monotone_onE) +qed + +no_notation bot ("\") + +context + fixes A and less_eq (infix "\" 50) and bot ("\") and f + assumes bot: "\ \ A" "\q \ A. \ \ q" + assumes cont: "omega_continuous A (\) f" +begin + +interpretation less_eq_notations. + +private lemma f: "f ` A \ A" using cont by auto + +private abbreviation(input) "Fn \ {f^n \ |. n :: nat}" + +private lemma fn_ref: "f^n \ \ f^n \" and fnA: "f^n \ \ A" +proof (atomize(full), induct n) + case 0 + from bot show ?case by simp +next + case (Suc n) + then have fn: "f^n \ \ A" and fnfn: "f^n \ \ f^n \" by auto + from f fn omega_continuous_imp_mono_refl[OF cont fn fn fnfn fnfn fnfn] + show ?case by auto +qed + +private lemma FnA: "Fn \ A" using fnA by auto + +private lemma fn_monotone: "monotone (\) (\) (\n. f^n \)" +proof + fix n m :: nat + assume "n \ m" + from le_Suc_ex[OF this] obtain k where m: "m = n + k" by auto + from bot fn_ref fnA omega_continuous_imp_mono_refl[OF cont] + show "f^n \ \ f^m \" by (unfold m, induct n, auto) +qed + +private lemma Fn: "Fn = range (\n. f^n \)" by auto + +theorem kleene_qfp: + assumes q: "extreme_bound A (\) Fn q" + shows "f q \ q" +proof + have fq: "extreme_bound A (\) (f ` Fn) (f q)" + apply (unfold Fn) + apply (rule omega_continuousD[OF cont]) + using FnA fn_monotone q by (unfold Fn, auto) + with bot have nq: "f^n \ \ f q" for n + by(induct n, auto simp: extreme_bound_iff) + then show "q \ f q" using f q by blast + have "f (f^n \) \ Fn" for n by (auto intro!: exI[of _ "Suc n"]) + then have "f ` Fn \ Fn" by auto + from extreme_bound_mono[OF this fq q] + show "f q \ q". +qed + +lemma ex_kleene_qfp: + assumes comp: "omega_complete A (\)" + shows "\p. extreme_bound A (\) Fn p" + using fn_monotone + apply (intro comp[unfolded omega_complete_def, THEN completeD, OF FnA]) + by fast + +subsection \Iterative Fixed Points are Least.\ +text \Kleene's theorem also states that the quasi-fixed point found this way is a least one. +Again, attractivity is needed to prove this statement.\ + +lemma kleene_qfp_is_least: + assumes attract: "\q \ A. \x \ A. f q \ q \ x \ f q \ x \ q" + assumes q: "extreme_bound A (\) Fn q" + shows "extreme {s \ A. f s \ s} (\) q" +proof(safe intro!: extremeI kleene_qfp[OF q]) + from q + show "q \ A" by auto + fix c assume c: "c \ A" and cqfp: "f c \ c" + { + fix n::nat + have "f^n \ \ c" + proof(induct n) + case 0 + show ?case using bot c by auto + next + case IH: (Suc n) + have "c \ c" using attract cqfp c by auto + with IH have "f^(Suc n) \ \ f c" + using omega_continuous_imp_mono_refl[OF cont] fn_ref fnA c by auto + then show ?case using attract cqfp c fnA by blast + qed + } + then show "q \ c" using q c by auto +qed + +lemma kleene_qfp_iff_least: + assumes comp: "omega_complete A (\)" + assumes attract: "\q \ A. \x \ A. f q \ q \ x \ f q \ x \ q" + assumes dual_attract: "\p \ A. \q \ A. \x \ A. p \ q \ q \ x \ p \ x" + shows "extreme_bound A (\) Fn = extreme {s \ A. f s \ s} (\)" +proof (intro ext iffI kleene_qfp_is_least[OF attract]) + fix q + assume q: "extreme {s \ A. f s \ s} (\) q" + from q have qA: "q \ A" by auto + from q have qq: "q \ q" by auto + from q have fqq: "f q \ q" by auto + from ex_kleene_qfp[OF comp] + obtain k where k: "extreme_bound A (\) Fn k" by auto + have qk: "q \ k" + proof + from kleene_qfp[OF k] q k + show "q \ k" by auto + from kleene_qfp_is_least[OF _ k] q attract + show "k \ q" by blast + qed + show "extreme_bound A (\) Fn q" + proof (intro extreme_boundI,safe) + fix n + show "f^n \ \ q" + proof (induct n) + case 0 + from bot q show ?case by auto + next + case S:(Suc n) + from fnA f have fsnbA: "f (f^n \) \ A" by auto + have fnfn: "f^n \ \ f^n \" using fn_ref by auto + have "f (f^n \) \ f q" + using omega_continuous_imp_mono_refl[OF cont fnA qA S fnfn qq] by auto + then show ?case using fsnbA qA attract fqq by auto + qed + next + fix x + assume "bound Fn (\) x" and x: "x \ A" + with k have kx: "k \ x" by auto + with dual_attract[rule_format, OF _ _ x qk] q k + show "q \ x" by auto + next + from q show "q \ A" by auto + qed +qed + +end + +context attractive begin + +interpretation less_eq_notations. + +theorem kleene_qfp_is_dual_extreme: + assumes comp: "omega_complete A (\)" + and cont: "omega_continuous A (\) f" and bA: "b \ A" and bot: "\x \ A. b \ x" + shows "extreme_bound A (\) {f^n b |. n :: nat} = extreme {s \ A. f s \ s} (\)" + apply (rule kleene_qfp_iff_least[OF bA bot cont comp]) + using cont[THEN omega_continuousDdom] + by (auto dest: sym_order_trans order_sym_trans) + +end + +corollary(in antisymmetric) kleene_fp: + assumes cont: "omega_continuous A (\) f" + and b: "b \ A" "\x \ A. b \ x" + and p: "extreme_bound A (\) {f^n b |. n :: nat} p" + shows "f p = p" + using kleene_qfp[OF b cont] p cont[THEN omega_continuousDdom] + by (auto 2 3 intro!:antisym) + +no_notation compower ("_^_"[1000,1000]1000) + +end \ No newline at end of file diff --git a/thys/Complete_Non_Orders/ROOT b/thys/Complete_Non_Orders/ROOT --- a/thys/Complete_Non_Orders/ROOT +++ b/thys/Complete_Non_Orders/ROOT @@ -1,10 +1,10 @@ chapter AFP session Complete_Non_Orders (AFP) = HOL + description "Theory of Complete Non-Orders and their Fixed-Points Theorems" options [timeout = 300] theories - Fixed_Points + Fixed_Points Kleene_Fixed_Point document_files "root.tex" "root.bib"