--- 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
--- 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 \<subseteq> carrier G \<times> carrier G"
+ show "rcong H \<subseteq> carrier G \<times> 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)
--- 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 \<subseteq> Field natLeq \<times> 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
--- 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 \<Longrightarrow> 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 \<subseteq> Field r \<times> Field r" and "Refl r" and "trans r"
+ using \<open>Preorder r\<close>
+ by (simp_all only: preorder_on_def)
+
+ show "Restr r A \<subseteq> Field (Restr r A) \<times> Field (Restr r A)"
+ using \<open>r \<subseteq> Field r \<times> Field r\<close>
+ by (auto simp add: Field_def)
+
+ show "Refl (Restr r A)"
+ using Refl_Restr[OF \<open>Refl r\<close>] .
+
+ show "trans (Restr r A)"
+ using trans_Restr[OF \<open>trans r\<close>] .
+qed
lemma Partial_order_Restr:
"Partial_order r \<Longrightarrow> Partial_order(Restr r A)"
@@ -867,6 +883,18 @@
"inj_on f (Field r) \<Longrightarrow> (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 \<subseteq> A \<times> B"
+ shows "dir_image r f \<subseteq> f ` A \<times> f ` B"
+proof (rule subsetI)
+ fix x
+ assume "x \<in> dir_image r f"
+ then obtain a b where "x = (f a, f b)" and "(a, b) \<in> r"
+ unfolding dir_image_def by blast
+ thus "x \<in> f ` A \<times> f ` B"
+ using \<open>r \<subseteq> A \<times> B\<close> 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:
- "\<lbrakk>Preorder r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> 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 \<subseteq> Field r \<times> Field r" and "Refl r" and "trans r"
+ using \<open>Preorder r\<close> by (simp_all only: preorder_on_def)
+
+ show "dir_image r f \<subseteq> Field (dir_image r f) \<times> Field (dir_image r f)"
+ using dir_image_subset[OF \<open>r \<subseteq> Field r \<times> Field r\<close>]
+ unfolding dir_image_Field .
+
+ show "Refl (dir_image r f)"
+ using Refl_dir_image[OF \<open>Refl r\<close>] .
+
+ show "trans (dir_image r f)"
+ using trans_dir_image[OF \<open>trans r\<close> 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 \<subseteq> Field r \<times> Field r"
+ shows "bsqr r \<subseteq> Field (bsqr r) \<times> Field (bsqr r)"
+ using \<open>r \<subseteq> Field r \<times> Field r\<close>
+ 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 \<subseteq> Field r \<times> Field r"
+ using \<open>Well_order r\<close>
+ 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 \<open>r \<subseteq> Field r \<times> Field r\<close>]
+ by auto
+qed
lemma bsqr_Well_order:
assumes "Well_order r"
--- 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) \<in> r"
hence "a \<in> under r b \<and> b \<in> 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) \<in> r"
hence "a \<in> under r a \<and> b \<in> 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)
--- 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:
"\<lbrakk>Field r Int Field r' = {}; Preorder r; Preorder r'\<rbrakk> \<Longrightarrow> 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
--- 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: "\<lbrakk>Preorder r; Preorder r'\<rbrakk> \<Longrightarrow> 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') \<times> Field (r +o r')"]
+ Restr_Field[of "r +o r'"])
lemma osum_antisym: "\<lbrakk>antisym r; antisym r'\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>Preorder r; Preorder r'; antisym r; antisym r'\<rbrakk> \<Longrightarrow> 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') \<times> Field (r *o r')"])
lemma oprod_antisym: "\<lbrakk>antisym r; antisym r'\<rbrakk> \<Longrightarrow> 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)
--- 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 \<le>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 \<Longrightarrow> Restr r (under r a) \<le>o r"
@@ -334,7 +335,7 @@
have bb: "b \<in> Field r" using bA unfolding underS_def Field_def by auto
assume "\<forall>a\<in>A. b \<notin> underS a"
hence 0: "\<forall>a \<in> A. (a,b) \<in> 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) \<in> r"
by (simp add: "0" A bb supr_least)
thus False
@@ -605,7 +606,7 @@
assumes isLimOrd and "i \<in> Field r"
shows "succ i \<in> 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 \<in> Field r"
--- 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 @@
"\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p" and
"\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p"
using Chains_wo [OF \<open>R \<in> Chains I\<close>] by (simp_all add: order_on_defs)
- have "Refl (\<Union>R)" using \<open>\<forall>r\<in>R. Refl r\<close> unfolding refl_on_def by fastforce
+ have "(\<Union>R) \<subseteq> Field (\<Union>R) \<times> Field (\<Union>R)"
+ using Restr_Field by blast
+ moreover have "Refl (\<Union>R)" using \<open>\<forall>r\<in>R. Refl r\<close> unfolding refl_on_def by fastforce
moreover have "trans (\<Union>R)"
by (rule chain_subset_trans_Union [OF subch \<open>\<forall>r\<in>R. trans r\<close>])
moreover have "antisym (\<Union>R)"
@@ -130,10 +132,13 @@
let ?s = "{(y, x) | y. y \<in> Field m}"
let ?m = "insert (x, x) m \<union> ?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 \<subseteq> Field m \<times> Field m"
using \<open>Well_order m\<close> by (simp_all add: order_on_defs)
txt \<open>We show that the extension is a wellorder.\<close>
- have "Refl ?m" using \<open>Refl m\<close> Fm by (auto simp: refl_on_def)
+ have "?m \<subseteq> Field ?m \<times> Field ?m"
+ using \<open>m \<subseteq> Field m \<times> Field m\<close> by auto
+ moreover have "Refl ?m" using \<open>Refl m\<close> Fm by (auto simp: refl_on_def)
moreover have "trans ?m" using \<open>trans m\<close> \<open>x \<notin> Field m\<close>
unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast
moreover have "antisym ?m" using \<open>antisym m\<close> \<open>x \<notin> Field m\<close>
@@ -160,7 +165,7 @@
\<open>downset_on (Field m) p\<close> and \<open>downset_on (Field ?m) p\<close> and
\<open>extension_on (Field m) m p\<close> and \<open>extension_on (Field ?m) ?m p\<close> and
\<open>Refl m\<close> and \<open>x \<notin> Field m\<close>
- 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
\<comment> \<open>This contradicts maximality of m:\<close>
show False using max and \<open>x \<notin> Field m\<close> unfolding Field_def by blast
@@ -199,7 +204,8 @@
from \<open>p \<subseteq> r\<close> have "p \<subseteq> ?r" using \<open>Field p \<subseteq> A\<close> by (auto simp: Field_def)
have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)"
using \<open>Well_order r\<close> by (simp_all add: order_on_defs)
- have "refl_on A ?r" using \<open>Refl r\<close> by (auto simp: refl_on_def univ)
+ have "?r \<subseteq> A \<times> A" by blast
+ moreover have "refl_on A ?r" using \<open>Refl r\<close> by (auto simp: refl_on_def univ)
moreover have "trans ?r" using \<open>trans r\<close>
unfolding trans_def by blast
moreover have "antisym ?r" using \<open>antisym r\<close>
--- 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) \<in> r"
thus "b \<in> Field r"
- using REFL refl_on_def[of _ r] by auto
+ by (simp add: FieldI2)
next
fix a b
assume 1: "(suc B, b) \<in> r" and 2: "a \<in> B"
--- 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 \<open>Equivalence relations -- set version\<close>
definition equiv :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"
- where "equiv A r \<longleftrightarrow> refl_on A r \<and> sym r \<and> trans r"
+ where "equiv A r \<longleftrightarrow> r \<subseteq> A \<times> A \<and> refl_on A r \<and> sym r \<and> trans r"
-lemma equivI: "refl_on A r \<Longrightarrow> sym r \<Longrightarrow> trans r \<Longrightarrow> equiv A r"
+lemma equivI: "r \<subseteq> A \<times> A \<Longrightarrow> refl_on A r \<Longrightarrow> sym r \<Longrightarrow> trans r \<Longrightarrow> 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 \<subseteq> A \<times> A" and "refl_on A r" and "sym r" and "trans r"
using assms by (simp add: equiv_def)
text \<open>
@@ -30,24 +30,27 @@
lemma sym_trans_comp_subset: "sym r \<Longrightarrow> trans r \<Longrightarrow> r\<inverse> O r \<subseteq> r"
unfolding trans_def sym_def converse_unfold by blast
-lemma refl_on_comp_subset: "refl_on A r \<Longrightarrow> r \<subseteq> r\<inverse> O r"
+lemma refl_on_comp_subset: "r \<subseteq> A \<times> A \<Longrightarrow> refl_on A r \<Longrightarrow> r \<subseteq> r\<inverse> O r"
unfolding refl_on_def by blast
lemma equiv_comp_eq: "equiv A r \<Longrightarrow> r\<inverse> 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 \<open>Second half.\<close>
lemma comp_equivI:
assumes "r\<inverse> O r = r" "Domain r = A"
shows "equiv A r"
-proof -
+proof (rule equivI)
+ show "r \<subseteq> A \<times> A"
+ using assms by auto
+
have *: "\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> 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 @@
\<comment> \<open>lemma for the next result\<close>
unfolding equiv_def trans_def sym_def by blast
-theorem equiv_class_eq: "equiv A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> 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) \<in> r"
+ shows "r``{a} = r``{b}"
+proof (intro subset_antisym equiv_class_subset[OF \<open>equiv A r\<close>])
+ show "(a, b) \<in> r"
+ using \<open>(a, b) \<in> r\<close> .
+next
+ have "sym r"
+ using \<open>equiv A r\<close> by (auto elim: equivE)
+ thus "(b, a) \<in> r"
+ using \<open>(a, b) \<in> r\<close>
+ by (auto dest: symD)
+qed
lemma equiv_class_self: "equiv A r \<Longrightarrow> a \<in> A \<Longrightarrow> a \<in> r``{a}"
unfolding equiv_def refl_on_def by blast
@@ -100,8 +114,17 @@
lemma Union_quotient: "equiv A r \<Longrightarrow> \<Union>(A//r) = A"
unfolding equiv_def refl_on_def quotient_def by blast
-lemma quotient_disj: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> Y \<in> A//r \<Longrightarrow> X = Y \<or> X \<inter> Y = {}"
- unfolding quotient_def equiv_def trans_def sym_def by blast
+lemma quotient_disj:
+ assumes "equiv A r" and "X \<in> A//r" and "Y \<in> A//r"
+ shows "X = Y \<or> X \<inter> Y = {}"
+proof -
+ have "sym r" and "trans r"
+ using \<open>equiv A r\<close>
+ 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 \<in> A//r" "Y \<in> A//r" and xy: "x \<in> X" "y \<in> Y" "(x, y) \<in> r"
@@ -109,8 +132,11 @@
proof -
obtain a b where "a \<in> A" and a: "X = r `` {a}" and "b \<in> A" and b: "Y = r `` {b}"
using assms by (auto elim!: quotientE)
- then have "(a,b) \<in> r"
- using xy \<open>equiv A r\<close> unfolding equiv_def sym_def trans_def by blast
+ moreover have "sym r" and "trans r"
+ using \<open>equiv A r\<close>
+ by (auto elim: equivE)
+ ultimately have "(a,b) \<in> r"
+ using xy unfolding sym_def trans_def by blast
then show ?thesis
unfolding a b by (rule equiv_class_eq [OF \<open>equiv A r\<close>])
qed
--- 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 \<subseteq> UNIV \<times> 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)
--- 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 \<subseteq> UNIV \<times> 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)
--- 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 \<subseteq> A \<times> A" and "refl_on A r"
by (auto elim: equivE)
then show "\<Union>(A // r) = A" "{} \<notin> A // r"
by (auto simp: refl_on_def quotient_def)
@@ -408,9 +408,10 @@
have "A = \<Union>P"
using P by (auto simp: partition_on_def)
- have "{(x, y). \<exists>p \<in> P. x \<in> p \<and> y \<in> p} \<subseteq> A \<times> A"
+ show "{(x, y). \<exists>p \<in> P. x \<in> p \<and> y \<in> p} \<subseteq> A \<times> A"
unfolding \<open>A = \<Union>P\<close> by blast
- then show "refl_on A {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}"
+
+ show "refl_on A {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}"
unfolding refl_on_def \<open>A = \<Union>P\<close> by auto
next
show "trans {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}"
--- 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 \<Longrightarrow> 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) \<in> listrel(r\<^sup>*)"
using listrel_refl_on[of UNIV, OF refl_rtrancl]
--- 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 (\<lambda>x. True) po"
definition PartialOrder :: "('a potype) set" where
- "PartialOrder == {P. refl_on (pset P) (order P) & antisym (order P) &
- trans (order P)}"
+ "PartialOrder \<equiv> {P. order P \<subseteq> pset P \<times> pset P \<and>
+ refl_on (pset P) (order P) \<and> antisym (order P) \<and> trans (order P)}"
definition CompleteLattice :: "('a potype) set" where
"CompleteLattice == {cl. cl \<in> PartialOrder \<and>
@@ -155,19 +155,26 @@
by (simp add: monotone_def)
lemma (in PO) po_subset_po:
- "S \<subseteq> A ==> (| pset = S, order = induced S r |) \<in> PartialOrder"
-apply (simp (no_asm) add: PartialOrder_def)
-apply auto
-\<comment> \<open>refl\<close>
-apply (simp add: refl_on_def induced_def)
-apply (blast intro: reflE)
-\<comment> \<open>antisym\<close>
-apply (simp add: antisym_def induced_def)
-apply (blast intro: antisymE)
-\<comment> \<open>trans\<close>
-apply (simp add: trans_def induced_def)
-apply (blast intro: transE)
-done
+ assumes "S \<subseteq> A"
+ shows "(| pset = S, order = induced S r |) \<in> PartialOrder"
+ unfolding PartialOrder_def mem_Collect_eq potype.simps
+proof (intro conjI)
+ show "induced S r \<subseteq> S \<times> 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 \<open>S \<subseteq> A\<close>
+ 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) \<in> induced S r; S \<subseteq> A |] ==> (x, y) \<in> r"
by (simp add: add: induced_def)
@@ -196,7 +203,7 @@
lemma (in PO) dualPO: "dual cl \<in> 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) \<in> r & x \<in> A} |] ==> (f (lub H cl), lub H cl) \<in> 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) \<in> r & x \<in> A} ==> lub H cl \<in> 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) \<in> r & x \<in> A}; x \<in> P |] ==> x \<in> H"
@@ -618,7 +628,8 @@
declare (in CLF) CO_refl_on[simp] refl_on_def [simp]
lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> 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 \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A"
-by (metis CO_refl_on interval_imp_mem refl_onD refl_onD2 rel_imp_elem subset_eq)
+ by (metis PO.interval_imp_mem PO.intro dualPO dualr_iff interval_dual r_def
+ rel_imp_elem subsetI)
declare (in CLF) rel_imp_elem[rule del]
declare interval_def [simp del]
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy Fri Mar 07 16:16:08 2025 +0100
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy Wed Mar 12 21:53:25 2025 +0100
@@ -51,6 +51,7 @@
lemma equiv_starrel: "equiv UNIV starrel"
proof (rule equivI)
+ show "starrel \<subseteq> UNIV \<times> UNIV" by simp
show "refl starrel" by (simp add: refl_on_def)
show "sym starrel" by (simp add: sym_def eq_commute)
show "trans starrel" by (intro transI) (auto elim: eventually_elim2)
--- a/src/HOL/Order_Relation.thy Fri Mar 07 16:16:08 2025 +0100
+++ b/src/HOL/Order_Relation.thy Wed Mar 12 21:53:25 2025 +0100
@@ -11,7 +11,7 @@
subsection \<open>Orders on a set\<close>
-definition "preorder_on A r \<equiv> refl_on A r \<and> trans r"
+definition "preorder_on A r \<equiv> r \<subseteq> A \<times> A \<and> refl_on A r \<and> trans r"
definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"
@@ -26,7 +26,7 @@
strict_linear_order_on_def well_order_on_def
lemma partial_order_onD:
- assumes "partial_order_on A r" shows "refl_on A r" and "trans r" and "antisym r"
+ assumes "partial_order_on A r" shows "refl_on A r" and "trans r" and "antisym r" and "r \<subseteq> A \<times> A"
using assms unfolding partial_order_on_def preorder_on_def by auto
lemma preorder_on_empty[simp]: "preorder_on {} {}"
@@ -43,7 +43,7 @@
lemma preorder_on_converse[simp]: "preorder_on A (r\<inverse>) = preorder_on A r"
- by (simp add: preorder_on_def)
+ by (auto simp add: preorder_on_def)
lemma partial_order_on_converse[simp]: "partial_order_on A (r\<inverse>) = partial_order_on A r"
by (simp add: partial_order_on_def)
@@ -154,7 +154,8 @@
where "relation_of P A \<equiv> { (a, b) \<in> A \<times> A. P a b }"
lemma Field_relation_of:
- assumes "refl_on A (relation_of P A)" shows "Field (relation_of P A) = A"
+ assumes "relation_of P A \<subseteq> A \<times> A" and "refl_on A (relation_of P A)"
+ shows "Field (relation_of P A) = A"
using assms unfolding refl_on_def Field_def by auto
lemma partial_order_on_relation_ofI:
@@ -163,8 +164,10 @@
and antisym: "\<And>a b. \<lbrakk> a \<in> A; b \<in> A \<rbrakk> \<Longrightarrow> P a b \<Longrightarrow> P b a \<Longrightarrow> a = b"
shows "partial_order_on A (relation_of P A)"
proof -
- from refl have "refl_on A (relation_of P A)"
- unfolding refl_on_def relation_of_def by auto
+ have "relation_of P A \<subseteq> A \<times> A"
+ unfolding relation_of_def by auto
+ moreover have "refl_on A (relation_of P A)"
+ using refl unfolding refl_on_def relation_of_def by auto
moreover have "trans (relation_of P A)" and "antisym (relation_of P A)"
unfolding relation_of_def
by (auto intro: transI dest: trans, auto intro: antisymI dest: antisym)
@@ -173,8 +176,15 @@
qed
lemma Partial_order_relation_ofI:
- assumes "partial_order_on A (relation_of P A)" shows "Partial_order (relation_of P A)"
- using Field_relation_of assms partial_order_on_def preorder_on_def by fastforce
+ assumes "partial_order_on A (relation_of P A)"
+ shows "Partial_order (relation_of P A)"
+proof -
+ have *: "Field (relation_of P A) = A"
+ using assms by (simp_all only: Field_relation_of partial_order_on_def preorder_on_def)
+ show ?thesis
+ unfolding *
+ using assms .
+qed
subsection \<open>Orders on a type\<close>
@@ -197,11 +207,8 @@
subsubsection \<open>Auxiliaries\<close>
-lemma refl_on_domain: "refl_on A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> a \<in> A \<and> b \<in> A"
- by (auto simp add: refl_on_def)
-
corollary well_order_on_domain: "well_order_on A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> a \<in> A \<and> b \<in> A"
- by (auto simp add: refl_on_domain order_on_defs)
+ by (auto simp add: order_on_defs)
lemma well_order_on_Field: "well_order_on A r \<Longrightarrow> A = Field r"
by (auto simp add: refl_on_def Field_def order_on_defs)
--- a/src/HOL/Relation.thy Fri Mar 07 16:16:08 2025 +0100
+++ b/src/HOL/Relation.thy Wed Mar 12 21:53:25 2025 +0100
@@ -151,7 +151,7 @@
subsubsection \<open>Reflexivity\<close>
definition refl_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
- where "refl_on A r \<longleftrightarrow> r \<subseteq> A \<times> A \<and> (\<forall>x\<in>A. (x, x) \<in> r)"
+ where "refl_on A r \<longleftrightarrow> (\<forall>x\<in>A. (x, x) \<in> r)"
abbreviation refl :: "'a rel \<Rightarrow> bool" \<comment> \<open>reflexivity over a type\<close>
where "refl \<equiv> refl_on UNIV"
@@ -170,7 +170,7 @@
lemma reflp_refl_eq [pred_set_conv]: "reflp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> refl r"
by (simp add: refl_on_def reflp_def)
-lemma refl_onI [intro?]: "r \<subseteq> A \<times> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> (x, x) \<in> r) \<Longrightarrow> refl_on A r"
+lemma refl_onI [intro?]: "(\<And>x. x \<in> A \<Longrightarrow> (x, x) \<in> r) \<Longrightarrow> refl_on A r"
unfolding refl_on_def by (iprover intro!: ballI)
lemma reflI: "(\<And>x. (x, x) \<in> r) \<Longrightarrow> refl r"
@@ -186,12 +186,6 @@
lemma refl_onD: "refl_on A r \<Longrightarrow> a \<in> A \<Longrightarrow> (a, a) \<in> r"
unfolding refl_on_def by blast
-lemma refl_onD1: "refl_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> x \<in> A"
- unfolding refl_on_def by blast
-
-lemma refl_onD2: "refl_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> A"
- unfolding refl_on_def by blast
-
lemma reflD: "refl r \<Longrightarrow> (a, a) \<in> r"
unfolding refl_on_def by blast
@@ -252,10 +246,6 @@
lemma refl_on_singleton [simp]: "refl_on {x} {(x, x)}"
by (blast intro: refl_onI)
-lemma refl_on_def' [nitpick_unfold, code]:
- "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)"
- by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
-
lemma reflp_on_equality [simp]: "reflp_on A (=)"
by (simp add: reflp_on_def)
@@ -952,7 +942,7 @@
by blast
lemma refl_on_Id_on: "refl_on A (Id_on A)"
- by (rule refl_onI [OF Id_on_subset_Times Id_onI])
+ by (rule refl_onI[OF Id_onI])
lemma antisym_Id_on [simp]: "antisym (Id_on A)"
unfolding antisym_def by blast
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Fri Mar 07 16:16:08 2025 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Wed Mar 12 21:53:25 2025 +0100
@@ -338,18 +338,19 @@
rtac ctxt equalityD2, rtac ctxt (mk_nth_conv n i)] 1;
fun mk_equiv_lsbis_tac ctxt sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O =
- EVERY' [rtac ctxt (@{thm equiv_def} RS iffD2),
+ EVERY' [rtac ctxt @{thm equivI},
+ rtac ctxt lsbis_incl,
- rtac ctxt conjI, rtac ctxt (@{thm refl_on_def} RS iffD2),
- rtac ctxt conjI, rtac ctxt lsbis_incl, rtac ctxt ballI, rtac ctxt set_mp,
+ rtac ctxt @{thm refl_onI},
+ rtac ctxt set_mp,
rtac ctxt incl_lsbis, rtac ctxt bis_Id_on, assume_tac ctxt, etac ctxt @{thm Id_onI},
- rtac ctxt conjI, rtac ctxt (@{thm sym_def} RS iffD2),
- rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt set_mp,
+ rtac ctxt @{thm symI},
+ rtac ctxt set_mp,
rtac ctxt incl_lsbis, rtac ctxt bis_converse, rtac ctxt sbis_lsbis, etac ctxt @{thm converseI},
- rtac ctxt (@{thm trans_def} RS iffD2),
- rtac ctxt allI, rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt impI, rtac ctxt set_mp,
+ rtac ctxt @{thm transI},
+ rtac ctxt set_mp,
rtac ctxt incl_lsbis, rtac ctxt bis_O, rtac ctxt sbis_lsbis, rtac ctxt sbis_lsbis,
etac ctxt @{thm relcompI}, assume_tac ctxt] 1;
--- a/src/HOL/ZF/Games.thy Fri Mar 07 16:16:08 2025 +0100
+++ b/src/HOL/ZF/Games.thy Wed Mar 12 21:53:25 2025 +0100
@@ -816,6 +816,9 @@
lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"
proof (rule equivI)
+ show "eq_game_rel \<subseteq> UNIV \<times> UNIV"
+ by simp
+next
show "refl eq_game_rel"
by (auto simp only: eq_game_rel_def intro: reflI eq_game_refl)
next
--- a/src/HOL/Zorn.thy Fri Mar 07 16:16:08 2025 +0100
+++ b/src/HOL/Zorn.thy Wed Mar 12 21:53:25 2025 +0100
@@ -543,7 +543,7 @@
unfolding relation_of_def using that by auto
ultimately have "\<exists>m\<in>A. \<forall>a\<in>A. (m, a) \<in> relation_of P A \<longrightarrow> a = m"
using Zorns_po_lemma[OF Partial_order_relation_ofI[OF po], rule_format] ch
- unfolding Field_relation_of[OF partial_order_onD(1)[OF po]] by blast
+ unfolding Field_relation_of[OF partial_order_onD(4)[OF po] partial_order_onD(1)[OF po]] by blast
then show ?thesis
by (auto simp: relation_of_def)
qed
@@ -749,7 +749,9 @@
have "\<forall>r\<in>R. Refl r" and "\<forall>r\<in>R. trans r" and "\<forall>r\<in>R. antisym r"
and "\<forall>r\<in>R. Total r" and "\<forall>r\<in>R. wf (r - Id)"
using Chains_wo [OF \<open>R \<in> Chains I\<close>] by (simp_all add: order_on_defs)
- have "Refl (\<Union>R)"
+ have "(\<Union> R) \<subseteq> Field (\<Union> R) \<times> Field (\<Union> R)"
+ unfolding Field_def by auto
+ moreover have "Refl (\<Union>R)"
using \<open>\<forall>r\<in>R. Refl r\<close> unfolding refl_on_def by fastforce
moreover have "trans (\<Union>R)"
by (rule chain_subset_trans_Union [OF subch \<open>\<forall>r\<in>R. trans r\<close>])
@@ -798,10 +800,13 @@
let ?m = "insert (x, x) m \<union> ?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 \<subseteq> Field m \<times> Field m"
using \<open>Well_order m\<close> by (simp_all add: order_on_defs)
\<comment> \<open>We show that the extension is a well-order\<close>
- have "Refl ?m"
+ have "?m \<subseteq> Field ?m \<times> Field ?m"
+ using \<open>m \<subseteq> Field m \<times> Field m\<close> by auto
+ moreover have "Refl ?m"
using \<open>Refl m\<close> Fm unfolding refl_on_def by blast
moreover have "trans ?m" using \<open>trans m\<close> and \<open>x \<notin> Field m\<close>
unfolding trans_def Field_def by blast
@@ -839,9 +844,12 @@
let ?r = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}"
have 1: "Field ?r = A"
using wo univ by (fastforce simp: Field_def order_on_defs refl_on_def)
- from \<open>Well_order r\<close> have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)"
+ from \<open>Well_order r\<close> have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)" and
+ "r \<subseteq> Field r \<times> Field r"
by (simp_all add: order_on_defs)
- from \<open>Refl r\<close> have "Refl ?r"
+ have "?r \<subseteq> Field ?r \<times> Field ?r"
+ using \<open>r \<subseteq> Field r \<times> Field r\<close> by (auto simp: 1)
+ moreover from \<open>Refl r\<close> have "Refl ?r"
by (auto simp: refl_on_def 1 univ)
moreover from \<open>trans r\<close> have "trans ?r"
unfolding trans_def by blast
--- a/src/HOL/ex/Tarski.thy Fri Mar 07 16:16:08 2025 +0100
+++ b/src/HOL/ex/Tarski.thy Wed Mar 12 21:53:25 2025 +0100
@@ -59,7 +59,8 @@
where "Top po = greatest (\<lambda>x. True) po"
definition PartialOrder :: "'a potype set"
- where "PartialOrder = {P. refl_on (pset P) (order P) \<and> antisym (order P) \<and> trans (order P)}"
+ where "PartialOrder = {P. order P \<subseteq> pset P \<times> pset P \<and>
+ refl_on (pset P) (order P) \<and> antisym (order P) \<and> trans (order P)}"
definition CompleteLattice :: "'a potype set"
where "CompleteLattice =
@@ -159,6 +160,10 @@
lemma po_subset_po:
assumes "S \<subseteq> A" shows "\<lparr>pset = S, order = induced S r\<rparr> \<in> PartialOrder"
proof -
+ have "induced S r \<subseteq> S \<times> S"
+ by (metis (lifting) BNF_Def.Collect_case_prodD induced_def mem_Sigma_iff
+ prod.sel subrelI)
+ moreover
have "refl_on S (induced S r)"
using \<open>S \<subseteq> A\<close> by (auto simp: refl_on_def induced_def intro: reflE)
moreover
@@ -197,7 +202,7 @@
by (simp add: isLub_def isGlb_def dual_def converse_unfold)
lemma (in PO) dualPO: "dual cl \<in> PartialOrder"
- using cl_po by (simp add: PartialOrder_def dual_def)
+ using cl_po by (simp add: PartialOrder_def dual_def converse_Times flip: converse_subset_swap)
lemma Rdual:
assumes major: "\<And>S. S \<subseteq> A \<Longrightarrow> \<exists>L. isLub S po L" and "S \<subseteq> A" and "A = pset po"
@@ -453,9 +458,10 @@
have "(lub H cl, f (lub H cl)) \<in> r"
using assms lubH_le_flubH by blast
then have "(f (lub H cl), f (f (lub H cl))) \<in> r"
- by (meson PO_imp_refl_on monotoneE monotone_f refl_on_domain)
+ by (metis (lifting) PiE assms f_in_funcset lub_in_lattice mem_Collect_eq
+ monotoneE monotone_f subsetI)
then have "f (lub H cl) \<in> H"
- by (metis (no_types, lifting) PO_imp_refl_on assms mem_Collect_eq refl_on_domain)
+ using assms f_in_funcset lub_in_lattice by auto
then show ?thesis
by (simp add: assms lub_upper)
qed
@@ -510,7 +516,7 @@
subsection \<open>interval\<close>
lemma rel_imp_elem: "(x, y) \<in> r \<Longrightarrow> x \<in> A"
- using CO_refl_on by (auto simp: refl_on_def)
+ using A_def PartialOrder_def cl_po r_def by blast
lemma interval_subset: "\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> interval r a b \<subseteq> A"
by (simp add: interval_def) (blast intro: rel_imp_elem)
@@ -665,7 +671,7 @@
using assms intY1_elem interval_imp_mem lubY_in_A unfolding intY1_def
using lubY_le_flubY monotoneE monotone_f po.transE by blast
then show "(f x, Top cl) \<in> r"
- by (meson PO_imp_refl_on Top_prop refl_onD2)
+ by (metis assms f_in_funcset intY1_elem[of x] Top_prop[of "f x"] PiE[of f A "\<lambda>_. A" x])
qed
lemma intY1_mono: "monotone (\<lambda> x \<in> intY1. f x) intY1 (induced intY1 r)"