# HG changeset patch # User desharna # Date 1741812805 -3600 # Node ID 71d9d59d6bb5423badc31655f17d865c5fc55b5a # Parent bdefffffd05ffd186e0cc7125dbe305c0cc33982# Parent f3db31c8acbcc9c3fc3cfc7786a66a81073037d0 merged diff -r f3db31c8acbc -r 71d9d59d6bb5 NEWS --- a/NEWS Fri Mar 07 16:16:08 2025 +0100 +++ b/NEWS Wed Mar 12 21:53:25 2025 +0100 @@ -14,6 +14,11 @@ monotone_on_inf_fun monotone_on_sup_fun +* Theory "HOL.Relations": + - Changed definition of predicate refl_on to not constrain the domain and + range of the relation. To get the old semantics, explicitely use the + formula "r ⊂ A × A ∧ refl_on A r". INCOMPATIBILITY. + * Theory "HOL.Wellfounded": - Added lemmas. bex_rtrancl_min_element_if_wf_on diff -r f3db31c8acbc -r 71d9d59d6bb5 src/HOL/Algebra/Coset.thy --- a/src/HOL/Algebra/Coset.thy Fri Mar 07 16:16:08 2025 +0100 +++ b/src/HOL/Algebra/Coset.thy Wed Mar 12 21:53:25 2025 +0100 @@ -673,7 +673,7 @@ interpret group G by fact show ?thesis proof (intro equivI) - have "rcong H \ carrier G \ carrier G" + show "rcong H \ carrier G \ carrier G" by (auto simp add: r_congruent_def) thus "refl_on (carrier G) (rcong H)" by (auto simp add: r_congruent_def refl_on_def) diff -r f3db31c8acbc -r 71d9d59d6bb5 src/HOL/BNF_Cardinal_Order_Relation.thy --- a/src/HOL/BNF_Cardinal_Order_Relation.thy Fri Mar 07 16:16:08 2025 +0100 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Wed Mar 12 21:53:25 2025 +0100 @@ -1104,7 +1104,16 @@ lemma natLeq_Preorder: "Preorder natLeq" unfolding preorder_on_def - by (auto simp add: natLeq_Refl natLeq_trans) +proof (intro conjI) + show "natLeq \ Field natLeq \ Field natLeq" + unfolding natLeq_def Field_def by blast +next + show "Refl natLeq" + using natLeq_Refl . +next + show "trans natLeq" + using natLeq_trans . +qed lemma natLeq_antisym: "antisym natLeq" unfolding antisym_def natLeq_def by auto diff -r f3db31c8acbc -r 71d9d59d6bb5 src/HOL/BNF_Wellorder_Constructions.thy --- a/src/HOL/BNF_Wellorder_Constructions.thy Fri Mar 07 16:16:08 2025 +0100 +++ b/src/HOL/BNF_Wellorder_Constructions.thy Wed Mar 12 21:53:25 2025 +0100 @@ -56,8 +56,24 @@ unfolding trans_def Field_def by blast lemma Preorder_Restr: - "Preorder r \ Preorder(Restr r A)" - unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr) + assumes "Preorder r" + shows "Preorder(Restr r A)" + unfolding preorder_on_def +proof (intro conjI) + have "r \ Field r \ Field r" and "Refl r" and "trans r" + using \Preorder r\ + by (simp_all only: preorder_on_def) + + show "Restr r A \ Field (Restr r A) \ Field (Restr r A)" + using \r \ Field r \ Field r\ + by (auto simp add: Field_def) + + show "Refl (Restr r A)" + using Refl_Restr[OF \Refl r\] . + + show "trans (Restr r A)" + using trans_Restr[OF \trans r\] . +qed lemma Partial_order_Restr: "Partial_order r \ Partial_order(Restr r A)" @@ -867,6 +883,18 @@ "inj_on f (Field r) \ (dir_image r f) - Id = dir_image (r - Id) f" unfolding inj_on_def Field_def dir_image_def by auto +lemma dir_image_subset: + assumes "r \ A \ B" + shows "dir_image r f \ f ` A \ f ` B" +proof (rule subsetI) + fix x + assume "x \ dir_image r f" + then obtain a b where "x = (f a, f b)" and "(a, b) \ r" + unfolding dir_image_def by blast + thus "x \ f ` A \ f ` B" + using \r \ A \ B\ by auto +qed + lemma Refl_dir_image: assumes "Refl r" shows "Refl(dir_image r f)" @@ -903,8 +931,23 @@ qed lemma Preorder_dir_image: - "\Preorder r; inj_on f (Field r)\ \ Preorder (dir_image r f)" - by (simp add: preorder_on_def Refl_dir_image trans_dir_image) + assumes "Preorder r" and inj: "inj_on f (Field r)" + shows "Preorder (dir_image r f)" + unfolding preorder_on_def +proof (intro conjI) + have "r \ Field r \ Field r" and "Refl r" and "trans r" + using \Preorder r\ by (simp_all only: preorder_on_def) + + show "dir_image r f \ Field (dir_image r f) \ Field (dir_image r f)" + using dir_image_subset[OF \r \ Field r \ Field r\] + unfolding dir_image_Field . + + show "Refl (dir_image r f)" + using Refl_dir_image[OF \Refl r\] . + + show "trans (dir_image r f)" + using trans_dir_image[OF \trans r\ inj] . +qed lemma antisym_dir_image: assumes AN: "antisym r" and INJ: "inj_on f (Field r)" @@ -1060,6 +1103,13 @@ qed qed +lemma bsqr_subset: + assumes "r \ Field r \ Field r" + shows "bsqr r \ Field (bsqr r) \ Field (bsqr r)" + using \r \ Field r \ Field r\ + unfolding Field_bsqr + by (auto simp add: bsqr_def) + lemma bsqr_Refl: "Refl(bsqr r)" by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def) @@ -1302,8 +1352,16 @@ lemma bsqr_Linear_order: assumes "Well_order r" shows "Linear_order(bsqr r)" - unfolding order_on_defs - using assms bsqr_Refl bsqr_Trans bsqr_antisym bsqr_Total by blast +proof - + have "r \ Field r \ Field r" + using \Well_order r\ + by (simp only: order_on_defs) + + thus ?thesis + unfolding order_on_defs + using assms bsqr_Refl bsqr_Trans bsqr_antisym bsqr_Total bsqr_subset[OF \r \ Field r \ Field r\] + by auto +qed lemma bsqr_Well_order: assumes "Well_order r" diff -r f3db31c8acbc -r 71d9d59d6bb5 src/HOL/BNF_Wellorder_Embedding.thy --- a/src/HOL/BNF_Wellorder_Embedding.thy Fri Mar 07 16:16:08 2025 +0100 +++ b/src/HOL/BNF_Wellorder_Embedding.thy Wed Mar 12 21:53:25 2025 +0100 @@ -223,7 +223,7 @@ unfolding Field_def by auto {assume "(a,b) \ r" hence "a \ under r b \ b \ under r b" - using Refl by(auto simp add: under_def refl_on_def) + using Refl by (auto simp add: under_def refl_on_def Field_def) hence "a = b" using EMB 1 *** by (auto simp add: embed_def bij_betw_def inj_on_def) @@ -231,7 +231,7 @@ moreover {assume "(b,a) \ r" hence "a \ under r a \ b \ under r a" - using Refl by(auto simp add: under_def refl_on_def) + using Refl by (auto simp add: under_def refl_on_def Field_def) hence "a = b" using EMB 1 *** by (auto simp add: embed_def bij_betw_def inj_on_def) diff -r f3db31c8acbc -r 71d9d59d6bb5 src/HOL/Cardinals/Order_Union.thy --- a/src/HOL/Cardinals/Order_Union.thy Fri Mar 07 16:16:08 2025 +0100 +++ b/src/HOL/Cardinals/Order_Union.thy Wed Mar 12 21:53:25 2025 +0100 @@ -89,7 +89,7 @@ lemma Osum_Preorder: "\Field r Int Field r' = {}; Preorder r; Preorder r'\ \ Preorder (r Osum r')" - unfolding preorder_on_def using Osum_Refl Osum_trans by blast + unfolding preorder_on_def using Osum_Refl Osum_trans Restr_Field by blast lemma Osum_antisym: assumes FLD: "Field r Int Field r' = {}" and diff -r f3db31c8acbc -r 71d9d59d6bb5 src/HOL/Cardinals/Ordinal_Arithmetic.thy --- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy Fri Mar 07 16:16:08 2025 +0100 +++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy Wed Mar 12 21:53:25 2025 +0100 @@ -52,7 +52,9 @@ qed lemma osum_Preorder: "\Preorder r; Preorder r'\ \ Preorder (r +o r')" - unfolding preorder_on_def using osum_Refl osum_trans by blast + unfolding preorder_on_def using osum_Refl osum_trans + by (metis inf.cobounded2[of "r +o r'" "Field (r +o r') \ Field (r +o r')"] + Restr_Field[of "r +o r'"]) lemma osum_antisym: "\antisym r; antisym r'\ \ antisym (r +o r')" unfolding antisym_def osum_def by auto @@ -178,7 +180,9 @@ using assms by (clarsimp simp: trans_def antisym_def oprod_def) (metis FieldI1 FieldI2) lemma oprod_Preorder: "\Preorder r; Preorder r'; antisym r; antisym r'\ \ Preorder (r *o r')" - unfolding preorder_on_def using oprod_Refl oprod_trans by blast + unfolding preorder_on_def using oprod_Refl oprod_trans + by (metis Restr_Field[of "r *o r'"] + inf.cobounded2[of "r *o r'" "Field (r *o r') \ Field (r *o r')"]) lemma oprod_antisym: "\antisym r; antisym r'\ \ antisym (r *o r')" unfolding antisym_def oprod_def by auto @@ -588,7 +592,7 @@ qed lemma oexp_Preorder: "Preorder oexp" - unfolding preorder_on_def using oexp_Refl oexp_trans by blast + unfolding preorder_on_def using oexp_Refl oexp_trans Restr_Field[of oexp] by blast lemma oexp_antisym: "antisym oexp" proof (unfold antisym_def, safe, rule ccontr) diff -r f3db31c8acbc -r 71d9d59d6bb5 src/HOL/Cardinals/Wellorder_Constructions.thy --- a/src/HOL/Cardinals/Wellorder_Constructions.thy Fri Mar 07 16:16:08 2025 +0100 +++ b/src/HOL/Cardinals/Wellorder_Constructions.thy Wed Mar 12 21:53:25 2025 +0100 @@ -96,7 +96,8 @@ lemma ofilter_ordLeq: assumes "Well_order r" and "ofilter r A" shows "Restr r A \o r" -by (metis assms inf.orderE ofilter_embed ofilter_subset_ordLeq refl_on_def wo_rel.Field_ofilter wo_rel.REFL wo_rel.intro) + by (metis Well_order_Restr[of r A] assms ofilter_embed[of r A] ordLess_iff[of r "Restr r A"] + ordLess_or_ordLeq[of r "Restr r A"]) corollary under_Restr_ordLeq: "Well_order r \ Restr r (under r a) \o r" @@ -334,7 +335,7 @@ have bb: "b \ Field r" using bA unfolding underS_def Field_def by auto assume "\a\A. b \ underS a" hence 0: "\a \ A. (a,b) \ r" using A bA unfolding underS_def - by simp (metis REFL in_mono max2_def max2_greater refl_on_domain) + using bb in_notinI[of b] by blast have "(supr A, b) \ r" by (simp add: "0" A bb supr_least) thus False @@ -605,7 +606,7 @@ assumes isLimOrd and "i \ Field r" shows "succ i \ Field r" using assms unfolding isLimOrd_def isSuccOrd_def - by (metis REFL in_notinI refl_on_domain succ_smallest) + using FieldI1[of "succ i" _ r] in_notinI[of i] succ_smallest[of i] by blast lemma isLimOrd_aboveS: assumes l: isLimOrd and i: "i \ Field r" diff -r f3db31c8acbc -r 71d9d59d6bb5 src/HOL/Cardinals/Wellorder_Extension.thy --- a/src/HOL/Cardinals/Wellorder_Extension.thy Fri Mar 07 16:16:08 2025 +0100 +++ b/src/HOL/Cardinals/Wellorder_Extension.thy Wed Mar 12 21:53:25 2025 +0100 @@ -87,7 +87,9 @@ "\r. r \ R \ downset_on (Field r) p" and "\r. r \ R \ extension_on (Field r) r p" using Chains_wo [OF \R \ Chains I\] by (simp_all add: order_on_defs) - have "Refl (\R)" using \\r\R. Refl r\ unfolding refl_on_def by fastforce + have "(\R) \ Field (\R) \ Field (\R)" + using Restr_Field by blast + moreover have "Refl (\R)" using \\r\R. Refl r\ unfolding refl_on_def by fastforce moreover have "trans (\R)" by (rule chain_subset_trans_Union [OF subch \\r\R. trans r\]) moreover have "antisym (\R)" @@ -130,10 +132,13 @@ let ?s = "{(y, x) | y. y \ Field m}" let ?m = "insert (x, x) m \ ?s" have Fm: "Field ?m = insert x (Field m)" by (auto simp: Field_def) - have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)" + have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)" and + "m \ Field m \ Field m" using \Well_order m\ by (simp_all add: order_on_defs) txt \We show that the extension is a wellorder.\ - have "Refl ?m" using \Refl m\ Fm by (auto simp: refl_on_def) + have "?m \ Field ?m \ Field ?m" + using \m \ Field m \ Field m\ by auto + moreover have "Refl ?m" using \Refl m\ Fm by (auto simp: refl_on_def) moreover have "trans ?m" using \trans m\ \x \ Field m\ unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast moreover have "antisym ?m" using \antisym m\ \x \ Field m\ @@ -160,7 +165,7 @@ \downset_on (Field m) p\ and \downset_on (Field ?m) p\ and \extension_on (Field m) m p\ and \extension_on (Field ?m) ?m p\ and \Refl m\ and \x \ Field m\ - by (auto simp: I_def init_seg_of_def refl_on_def) + by (auto simp: I_def init_seg_of_def refl_on_def dest: well_order_on_domain) ultimately \ \This contradicts maximality of m:\ show False using max and \x \ Field m\ unfolding Field_def by blast @@ -199,7 +204,8 @@ from \p \ r\ have "p \ ?r" using \Field p \ A\ by (auto simp: Field_def) have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)" using \Well_order r\ by (simp_all add: order_on_defs) - have "refl_on A ?r" using \Refl r\ by (auto simp: refl_on_def univ) + have "?r \ A \ A" by blast + moreover have "refl_on A ?r" using \Refl r\ by (auto simp: refl_on_def univ) moreover have "trans ?r" using \trans r\ unfolding trans_def by blast moreover have "antisym ?r" using \antisym r\ diff -r f3db31c8acbc -r 71d9d59d6bb5 src/HOL/Cardinals/Wellorder_Relation.thy --- a/src/HOL/Cardinals/Wellorder_Relation.thy Fri Mar 07 16:16:08 2025 +0100 +++ b/src/HOL/Cardinals/Wellorder_Relation.thy Wed Mar 12 21:53:25 2025 +0100 @@ -218,7 +218,7 @@ next fix b assume "(suc B, b) \ r" thus "b \ Field r" - using REFL refl_on_def[of _ r] by auto + by (simp add: FieldI2) next fix a b assume 1: "(suc B, b) \ r" and 2: "a \ B" diff -r f3db31c8acbc -r 71d9d59d6bb5 src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Fri Mar 07 16:16:08 2025 +0100 +++ b/src/HOL/Equiv_Relations.thy Wed Mar 12 21:53:25 2025 +0100 @@ -11,14 +11,14 @@ subsection \Equivalence relations -- set version\ definition equiv :: "'a set \ ('a \ 'a) set \ bool" - where "equiv A r \ refl_on A r \ sym r \ trans r" + where "equiv A r \ r \ A \ A \ refl_on A r \ sym r \ trans r" -lemma equivI: "refl_on A r \ sym r \ trans r \ equiv A r" +lemma equivI: "r \ A \ A \ refl_on A r \ sym r \ trans r \ equiv A r" by (simp add: equiv_def) lemma equivE: assumes "equiv A r" - obtains "refl_on A r" and "sym r" and "trans r" + obtains "r \ A \ A" and "refl_on A r" and "sym r" and "trans r" using assms by (simp add: equiv_def) text \ @@ -30,24 +30,27 @@ lemma sym_trans_comp_subset: "sym r \ trans r \ r\ O r \ r" unfolding trans_def sym_def converse_unfold by blast -lemma refl_on_comp_subset: "refl_on A r \ r \ r\ O r" +lemma refl_on_comp_subset: "r \ A \ A \ refl_on A r \ r \ r\ O r" unfolding refl_on_def by blast lemma equiv_comp_eq: "equiv A r \ r\ O r = r" - unfolding equiv_def - by (iprover intro: sym_trans_comp_subset refl_on_comp_subset equalityI) + by (iprover elim: equivE intro: sym_trans_comp_subset refl_on_comp_subset equalityI) text \Second half.\ lemma comp_equivI: assumes "r\ O r = r" "Domain r = A" shows "equiv A r" -proof - +proof (rule equivI) + show "r \ A \ A" + using assms by auto + have *: "\x y. (x, y) \ r \ (y, x) \ r" using assms by blast - show ?thesis - unfolding equiv_def refl_on_def sym_def trans_def - using assms by (auto intro: *) + + thus "refl_on A r" "sym r" "trans r" + unfolding refl_on_def sym_def trans_def + using assms by auto qed @@ -57,8 +60,19 @@ \ \lemma for the next result\ unfolding equiv_def trans_def sym_def by blast -theorem equiv_class_eq: "equiv A r \ (a, b) \ r \ r``{a} = r``{b}" - by (intro equalityI equiv_class_subset; force simp add: equiv_def sym_def) +theorem equiv_class_eq: + assumes "equiv A r" and "(a, b) \ r" + shows "r``{a} = r``{b}" +proof (intro subset_antisym equiv_class_subset[OF \equiv A r\]) + show "(a, b) \ r" + using \(a, b) \ r\ . +next + have "sym r" + using \equiv A r\ by (auto elim: equivE) + thus "(b, a) \ r" + using \(a, b) \ r\ + by (auto dest: symD) +qed lemma equiv_class_self: "equiv A r \ a \ A \ a \ r``{a}" unfolding equiv_def refl_on_def by blast @@ -100,8 +114,17 @@ lemma Union_quotient: "equiv A r \ \(A//r) = A" unfolding equiv_def refl_on_def quotient_def by blast -lemma quotient_disj: "equiv A r \ X \ A//r \ Y \ A//r \ X = Y \ X \ Y = {}" - unfolding quotient_def equiv_def trans_def sym_def by blast +lemma quotient_disj: + assumes "equiv A r" and "X \ A//r" and "Y \ A//r" + shows "X = Y \ X \ Y = {}" +proof - + have "sym r" and "trans r" + using \equiv A r\ + by (auto elim: equivE) + thus ?thesis + using assms(2,3) + unfolding quotient_def equiv_def trans_def sym_def by blast +qed lemma quotient_eqI: assumes "equiv A r" "X \ A//r" "Y \ A//r" and xy: "x \ X" "y \ Y" "(x, y) \ r" @@ -109,8 +132,11 @@ proof - obtain a b where "a \ A" and a: "X = r `` {a}" and "b \ A" and b: "Y = r `` {b}" using assms by (auto elim!: quotientE) - then have "(a,b) \ r" - using xy \equiv A r\ unfolding equiv_def sym_def trans_def by blast + moreover have "sym r" and "trans r" + using \equiv A r\ + by (auto elim: equivE) + ultimately have "(a,b) \ r" + using xy unfolding sym_def trans_def by blast then show ?thesis unfolding a b by (rule equiv_class_eq [OF \equiv A r\]) qed diff -r f3db31c8acbc -r 71d9d59d6bb5 src/HOL/Induct/QuoDataType.thy --- a/src/HOL/Induct/QuoDataType.thy Fri Mar 07 16:16:08 2025 +0100 +++ b/src/HOL/Induct/QuoDataType.thy Wed Mar 12 21:53:25 2025 +0100 @@ -50,6 +50,7 @@ theorem equiv_msgrel: "equiv UNIV msgrel" proof (rule equivI) + show "msgrel \ UNIV \ UNIV" by simp show "refl msgrel" by (simp add: refl_on_def msgrel_refl) show "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM) show "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS) diff -r f3db31c8acbc -r 71d9d59d6bb5 src/HOL/Induct/QuoNestedDataType.thy --- a/src/HOL/Induct/QuoNestedDataType.thy Fri Mar 07 16:16:08 2025 +0100 +++ b/src/HOL/Induct/QuoNestedDataType.thy Wed Mar 12 21:53:25 2025 +0100 @@ -50,6 +50,7 @@ theorem equiv_exprel: "equiv UNIV exprel" proof (rule equivI) + show "exprel \ UNIV \ UNIV" by simp show "refl exprel" by (simp add: refl_on_def exprel_refl) show "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM) show "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS) diff -r f3db31c8acbc -r 71d9d59d6bb5 src/HOL/Library/Disjoint_Sets.thy --- a/src/HOL/Library/Disjoint_Sets.thy Fri Mar 07 16:16:08 2025 +0100 +++ b/src/HOL/Library/Disjoint_Sets.thy Wed Mar 12 21:53:25 2025 +0100 @@ -389,7 +389,7 @@ assumes r: "equiv A r" shows "partition_on A (A // r)" proof (rule partition_onI) - from r have "refl_on A r" + from r have "r \ A \ A" and "refl_on A r" by (auto elim: equivE) then show "\(A // r) = A" "{} \ A // r" by (auto simp: refl_on_def quotient_def) @@ -408,9 +408,10 @@ have "A = \P" using P by (auto simp: partition_on_def) - have "{(x, y). \p \ P. x \ p \ y \ p} \ A \ A" + show "{(x, y). \p \ P. x \ p \ y \ p} \ A \ A" unfolding \A = \P\ by blast - then show "refl_on A {(x, y). \p\P. x \ p \ y \ p}" + + show "refl_on A {(x, y). \p\P. x \ p \ y \ p}" unfolding refl_on_def \A = \P\ by auto next show "trans {(x, y). \p\P. x \ p \ y \ p}" diff -r f3db31c8acbc -r 71d9d59d6bb5 src/HOL/List.thy --- a/src/HOL/List.thy Fri Mar 07 16:16:08 2025 +0100 +++ b/src/HOL/List.thy Wed Mar 12 21:53:25 2025 +0100 @@ -7647,7 +7647,7 @@ qed theorem equiv_listrel: "equiv A r \ equiv (lists A) (listrel r)" - by (simp add: equiv_def listrel_refl_on listrel_sym listrel_trans) + by (simp add: equiv_def listrel_subset listrel_refl_on listrel_sym listrel_trans) lemma listrel_rtrancl_refl[iff]: "(xs,xs) \ listrel(r\<^sup>*)" using listrel_refl_on[of UNIV, OF refl_rtrancl] diff -r f3db31c8acbc -r 71d9d59d6bb5 src/HOL/Metis_Examples/Tarski.thy --- a/src/HOL/Metis_Examples/Tarski.thy Fri Mar 07 16:16:08 2025 +0100 +++ b/src/HOL/Metis_Examples/Tarski.thy Wed Mar 12 21:53:25 2025 +0100 @@ -60,8 +60,8 @@ "Top po == greatest (\x. True) po" definition PartialOrder :: "('a potype) set" where - "PartialOrder == {P. refl_on (pset P) (order P) & antisym (order P) & - trans (order P)}" + "PartialOrder \ {P. order P \ pset P \ pset P \ + refl_on (pset P) (order P) \ antisym (order P) \ trans (order P)}" definition CompleteLattice :: "('a potype) set" where "CompleteLattice == {cl. cl \ PartialOrder \ @@ -155,19 +155,26 @@ by (simp add: monotone_def) lemma (in PO) po_subset_po: - "S \ A ==> (| pset = S, order = induced S r |) \ PartialOrder" -apply (simp (no_asm) add: PartialOrder_def) -apply auto -\ \refl\ -apply (simp add: refl_on_def induced_def) -apply (blast intro: reflE) -\ \antisym\ -apply (simp add: antisym_def induced_def) -apply (blast intro: antisymE) -\ \trans\ -apply (simp add: trans_def induced_def) -apply (blast intro: transE) -done + assumes "S \ A" + shows "(| pset = S, order = induced S r |) \ PartialOrder" + unfolding PartialOrder_def mem_Collect_eq potype.simps +proof (intro conjI) + show "induced S r \ S \ S" + by (metis (no_types, lifting) case_prodD induced_def mem_Collect_eq + mem_Sigma_iff subrelI) + + show "refl_on S (induced S r)" + using \S \ A\ + by (simp add: induced_def reflE refl_on_def subsetD) + + show "antisym (induced S r)" + by (metis (lifting) BNF_Def.Collect_case_prodD PO_imp_sym antisym_subset induced_def + prod.collapse subsetI) + + show "trans (induced S r)" + by (metis (no_types, lifting) case_prodD case_prodI induced_def local.transE mem_Collect_eq + trans_on_def) +qed lemma (in PO) indE: "[| (x, y) \ induced S r; S \ A |] ==> (x, y) \ r" by (simp add: add: induced_def) @@ -196,7 +203,7 @@ lemma (in PO) dualPO: "dual cl \ PartialOrder" apply (insert cl_po) -apply (simp add: PartialOrder_def dual_def) + apply (simp add: PartialOrder_def dual_def converse_Times flip: converse_subset_swap) done lemma Rdual: @@ -486,8 +493,9 @@ "[| H = {x. (x, f x) \ r & x \ A} |] ==> (f (lub H cl), lub H cl) \ r" apply (rule lub_upper, fast) apply (rule_tac t = "H" in ssubst, assumption) -apply (rule CollectI) -by (metis (lifting) CO_refl_on lubH_le_flubH monotone_def monotone_f refl_onD1 refl_onD2) + apply (rule CollectI) + by (metis (lifting) Pi_iff f_in_funcset lubH_le_flubH lub_in_lattice + mem_Collect_eq monotoneE monotone_f subsetI) declare CLF.f_in_funcset[rule del] funcset_mem[rule del] CL.lub_in_lattice[rule del] PO.monotoneE[rule del] @@ -533,10 +541,12 @@ lemma (in CLF) (*lubH_is_fixp:*) "H = {x. (x, f x) \ r & x \ A} ==> lub H cl \ fix f A" apply (simp add: fix_def) -apply (rule conjI) -apply (metis CO_refl_on lubH_le_flubH refl_onD1) -apply (metis antisymE flubH_le_lubH lubH_le_flubH) -done + apply (rule conjI) + subgoal + by (metis (lifting) fix_def lubH_is_fixp mem_Collect_eq) + subgoal + by (metis antisymE flubH_le_lubH lubH_le_flubH) + done lemma (in CLF) fix_in_H: "[| H = {x. (x, f x) \ r & x \ A}; x \ P |] ==> x \ H" @@ -618,7 +628,8 @@ declare (in CLF) CO_refl_on[simp] refl_on_def [simp] lemma (in CLF) rel_imp_elem: "(x, y) \ r ==> x \ A" -by (metis CO_refl_on refl_onD1) + by (metis (no_types, lifting) A_def PartialOrder_def cl_po mem_Collect_eq + mem_Sigma_iff r_def subsetD) declare (in CLF) CO_refl_on[simp del] refl_on_def [simp del] @@ -626,7 +637,8 @@ declare interval_def [simp] lemma (in CLF) interval_subset: "[| a \ A; b \