# HG changeset patch
# User desharna
# Date 1711560572 -3600
# Node ID c40bdfc846408c2a44ba6163e886656ca95f36ab
# Parent  19cc354ba62533a01b8d60549da984d716592544
tuned proofs of Equiv_Relations.equiv

diff -r 19cc354ba625 -r c40bdfc84640 src/HOL/Algebra/Coset.thy
--- 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)"
diff -r 19cc354ba625 -r c40bdfc84640 src/HOL/Algebra/Sylow.thy
--- 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)
diff -r 19cc354ba625 -r c40bdfc84640 src/HOL/Cardinals/Wellorder_Constructions.thy
--- 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'"
diff -r 19cc354ba625 -r c40bdfc84640 src/HOL/Induct/QuoDataType.thy
--- 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
 
 
diff -r 19cc354ba625 -r c40bdfc84640 src/HOL/Induct/QuoNestedDataType.thy
--- 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)"
diff -r 19cc354ba625 -r c40bdfc84640 src/HOL/Library/Disjoint_Sets.thy
--- 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"
diff -r 19cc354ba625 -r c40bdfc84640 src/HOL/ZF/Games.thy
--- 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