--- a/src/HOL/Algebra/Coset.thy Thu Mar 28 08:30:42 2024 +0100
+++ b/src/HOL/Algebra/Coset.thy Wed Mar 27 18:29:32 2024 +0100
@@ -670,7 +670,9 @@
interpret group G by fact
show ?thesis
proof (intro equivI)
- show "refl_on (carrier G) (rcong H)"
+ have "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)
next
show "sym (rcong H)"
--- a/src/HOL/Algebra/Sylow.thy Thu Mar 28 08:30:42 2024 +0100
+++ b/src/HOL/Algebra/Sylow.thy Wed Mar 27 18:29:32 2024 +0100
@@ -23,6 +23,9 @@
and "RelM \<equiv> {(N1, N2). N1 \<in> calM \<and> N2 \<in> calM \<and> (\<exists>g \<in> carrier G. N1 = N2 #> g)}"
begin
+lemma RelM_subset: "RelM \<subseteq> calM \<times> calM"
+ by (auto simp only: RelM_def)
+
lemma RelM_refl_on: "refl_on calM RelM"
by (auto simp: refl_on_def RelM_def calM_def) (blast intro!: coset_mult_one [symmetric])
@@ -41,7 +44,7 @@
by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc)
lemma RelM_equiv: "equiv calM RelM"
- unfolding equiv_def by (blast intro: RelM_refl_on RelM_sym RelM_trans)
+ using RelM_subset RelM_refl_on RelM_sym RelM_trans by (intro equivI)
lemma M_subset_calM_prep: "M' \<in> calM // RelM \<Longrightarrow> M' \<subseteq> calM"
unfolding RelM_def by (blast elim!: quotientE)
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy Thu Mar 28 08:30:42 2024 +0100
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy Wed Mar 27 18:29:32 2024 +0100
@@ -44,6 +44,9 @@
corollary ordLeq_preorder_on: "preorder_on {r. Well_order r} ordLeq"
by(auto simp add: preorder_on_def ordLeq_refl_on ordLeq_trans)
+corollary ordIso_subset: "ordIso \<subseteq> {r. Well_order r} \<times> {r. Well_order r}"
+ using ordIso_reflexive unfolding refl_on_def ordIso_def by blast
+
corollary ordIso_refl_on: "refl_on {r. Well_order r} ordIso"
using ordIso_reflexive unfolding refl_on_def ordIso_def
by blast
@@ -55,7 +58,7 @@
by (auto simp add: sym_def ordIso_symmetric)
corollary ordIso_equiv: "equiv {r. Well_order r} ordIso"
- by (auto simp add: equiv_def ordIso_sym ordIso_refl_on ordIso_trans)
+ using ordIso_subset ordIso_refl_on ordIso_sym ordIso_trans by (intro equivI)
lemma ordLess_Well_order_simp[simp]:
assumes "r <o r'"
--- a/src/HOL/Induct/QuoDataType.thy Thu Mar 28 08:30:42 2024 +0100
+++ b/src/HOL/Induct/QuoDataType.thy Wed Mar 27 18:29:32 2024 +0100
@@ -49,11 +49,10 @@
by (induct X) (blast intro: msgrel.intros)+
theorem equiv_msgrel: "equiv UNIV msgrel"
-proof -
- have "refl msgrel" by (simp add: refl_on_def msgrel_refl)
- moreover have "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM)
- moreover have "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS)
- ultimately show ?thesis by (simp add: equiv_def)
+proof (rule equivI)
+ 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)
qed
--- a/src/HOL/Induct/QuoNestedDataType.thy Thu Mar 28 08:30:42 2024 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy Wed Mar 27 18:29:32 2024 +0100
@@ -49,11 +49,10 @@
(blast intro: exprel.intros listrel.intros)+
theorem equiv_exprel: "equiv UNIV exprel"
-proof -
- have "refl exprel" by (simp add: refl_on_def exprel_refl)
- moreover have "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)
- moreover have "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS)
- ultimately show ?thesis by (simp add: equiv_def)
+proof (rule equivI)
+ 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)
qed
theorem equiv_list_exprel: "equiv UNIV (listrel exprel)"
--- a/src/HOL/Library/Disjoint_Sets.thy Thu Mar 28 08:30:42 2024 +0100
+++ b/src/HOL/Library/Disjoint_Sets.thy Wed Mar 27 18:29:32 2024 +0100
@@ -405,13 +405,20 @@
assumes P: "partition_on A P"
shows "equiv A {(x, y). \<exists>p \<in> P. x \<in> p \<and> y \<in> p}"
proof (rule equivI)
- have "A = \<Union>P" "disjoint P" "{} \<notin> P"
+ 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"
+ 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}"
- unfolding refl_on_def by auto
+ 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}"
- using \<open>disjoint P\<close> by (auto simp: trans_def disjoint_def)
-qed (auto simp: sym_def)
+ using P by (auto simp only: trans_def disjoint_def partition_on_def)
+next
+ show "sym {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}"
+ by (auto simp only: sym_def)
+qed
lemma partition_on_eq_quotient:
assumes P: "partition_on A P"
--- a/src/HOL/ZF/Games.thy Thu Mar 28 08:30:42 2024 +0100
+++ b/src/HOL/ZF/Games.thy Wed Mar 27 18:29:32 2024 +0100
@@ -815,8 +815,16 @@
unfolding Pg_def by (auto simp add: quotient_def)
lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"
- by (auto simp add: equiv_def refl_on_def sym_def trans_def eq_game_rel_def
- eq_game_sym intro: eq_game_refl eq_game_trans)
+proof (rule equivI)
+ show "refl eq_game_rel"
+ by (auto simp only: eq_game_rel_def intro: reflI eq_game_refl)
+next
+ show "sym eq_game_rel"
+ by (auto simp only: eq_game_rel_def eq_game_sym intro: symI)
+next
+ show "trans eq_game_rel"
+ by (auto simp only: eq_game_rel_def intro: transI eq_game_trans)
+qed
instantiation Pg :: "{ord, zero, plus, minus, uminus}"
begin