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,2245 +1,2246 @@ (* 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 (* 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 \ idts \ 'a set" ("(1{_ /|./ _})") "_image" :: "'a \ pttrn \ 'a set \ 'a set" ("(1{_ /|./ (_/ \ _)})") translations "{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_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)" +definition monotone_on where + "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 {} = (\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 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 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 abbreviation "extreme_bound X \ extreme {b \ A. bound X (\) b} (\x y. y \ x)" lemma extreme_boundI[intro]: 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 sX: "extreme_bound X sX" and sY: "extreme_bound Y sY" shows "sX \ sY" proof- 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 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 \ A \ x \ x" by auto lemma extreme_bound_image_const: "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 \ 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 ir :: "'i \ 'i \ bool" (infix "\" 50) 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: "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 A (\) (f  I) x" using monotone_extreme_imp_extreme_bound by auto 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) 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_notations = less_eq_syntax begin abbreviation (input) greater_eq (infix "\" 50) where "x \ y \ y \ x" 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_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.\ text \Reflexivity restricted on a set:\ locale reflexive = related_set + assumes refl[intro]: "x \ A \ x \ x" begin 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 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 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 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 = related_set + assumes attract: "x \ y \ y \ x \ y \ z \ x \ A \ y \ A \ z \ A \ x \ z" begin 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 \ 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 \ 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 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 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 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 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_extremal: 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 A :: "'a set" and less :: "'a \ 'a \ bool" (infix "\" 50) begin 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 lemma well_foundedI_extremal: 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_extremal: "well_founded A (\) \ (\X \ A. X \ {} \ (\x \ X. \z \ X. \ z \ x))" using well_founded.nonempty_imp_ex_extremal well_foundedI_extremal by blast end 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_extremal) 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_extremal[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_extremal) 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_extremal[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 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_extremal) lemma well_founded_Restrp[simp]: "well_founded A (r\B) \ well_founded (A\B) r" (is "?l \ ?r") proof (intro iffI well_foundedI_extremal) assume l: ?l fix X assume XAB: "X \ A \ B" and X0: "X \ {}" with l[THEN well_founded.nonempty_imp_ex_extremal] 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 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_extremal, 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 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_extremal) 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_extremal) 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_extremal[OF XB X0] show ?thesis. next case False with A.nonempty_imp_ex_extremal[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 closed_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_extremal) 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_extremal[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_extremal) fix X assume "X \ A" and "X \ {}" from well_founded.nonempty_imp_ex_extremal[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 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 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 lemmas connex_axioms = connex_axioms interpretation less_eq_notations. sublocale asym: well_founded A "(\)" proof (unfold well_founded_iff_ex_extremal, 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 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_extremal 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 closed_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 closed_UN_well_founded[of _ "\x y. \ y \ x"]. end 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 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 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 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 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 closed_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 closed_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 = 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.\ text \The following sequence of declarations are in order to obtain fact names in a manner similar to the Isabelle/HOL facts of orders.\ 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 + pseudo_ordered_set begin sublocale attractive_ordering .. end locale quasi_ordering = compatible_ordering + quasi_ordered_set begin sublocale attractive_ordering .. end locale partial_ordering = compatible_ordering + partially_ordered_set begin sublocale pseudo_ordering + quasi_ordering .. end locale well_founded_ordering = quasi_ordering + well_founded locale total_ordering = compatible_ordering + total_ordered_set begin sublocale partial_ordering .. end locale strict_total_ordering = partial_ordering + semiconnex A "(\)" begin sublocale semiconnex_irreflexive .. sublocale connex proof 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]: 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 2020, we should declare sublocales in class before declaring dual sublocales, since otherwise facts would be prefixed by dual.dual.''\ context ord begin 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 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 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 UNIV (\) (<)" begin 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 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 UNIV (\) (<)" begin interpretation pseudo_ordering UNIV using psorder_axioms unfolding class.psorder_def. subclass attractive_order .. 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 UNIV (\) (<)" begin interpretation quasi_ordering UNIV using qorder_axioms unfolding class.qorder_def. subclass attractive_order .. 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 UNIV (\) (<)" begin interpretation partial_ordering UNIV using porder_axioms unfolding class.porder_def. subclass psorder .. subclass qorder .. 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 UNIV (\) (<)" begin interpretation well_founded_ordering UNIV using wf_qorder_axioms unfolding class.wf_qorder_def. subclass qorder .. 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 UNIV (\) (<)" begin interpretation total_ordering UNIV using totalorder_axioms unfolding class.totalorder_def. subclass porder .. 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 using order_refl apply assumption apply simp 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 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 strict_total_ordering UNIV apply unfold_locales by auto subclass totalorder .. 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\ 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 "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 (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. 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 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 apply intro_classes apply unfold_locales by (auto simp: le_fun_def dest: order.trans) instance "fun" :: (type,porder) porder 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