# HG changeset patch
# User desharna
# Date 1712039743 -7200
# Node ID 6de94d690f9f8b1fa2ae6dd05ae12a2cb779ad5f
# Parent  60b6c735b5d5ec01a98e8b6a44ac96439b008392# Parent  67e77f1e6d7bd7b4c5546673c46e9a03c935cdd9
merged

diff -r 60b6c735b5d5 -r 6de94d690f9f src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Mon Apr 01 15:47:15 2024 +0200
+++ b/src/HOL/Algebra/Coset.thy	Tue Apr 02 08:35:43 2024 +0200
@@ -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 60b6c735b5d5 -r 6de94d690f9f src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Mon Apr 01 15:47:15 2024 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Tue Apr 02 08:35:43 2024 +0200
@@ -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 60b6c735b5d5 -r 6de94d690f9f src/HOL/Cardinals/Wellorder_Constructions.thy
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Mon Apr 01 15:47:15 2024 +0200
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Tue Apr 02 08:35:43 2024 +0200
@@ -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 60b6c735b5d5 -r 6de94d690f9f src/HOL/Induct/QuoDataType.thy
--- a/src/HOL/Induct/QuoDataType.thy	Mon Apr 01 15:47:15 2024 +0200
+++ b/src/HOL/Induct/QuoDataType.thy	Tue Apr 02 08:35:43 2024 +0200
@@ -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 60b6c735b5d5 -r 6de94d690f9f src/HOL/Induct/QuoNestedDataType.thy
--- a/src/HOL/Induct/QuoNestedDataType.thy	Mon Apr 01 15:47:15 2024 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Tue Apr 02 08:35:43 2024 +0200
@@ -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 60b6c735b5d5 -r 6de94d690f9f src/HOL/Library/Disjoint_Sets.thy
--- a/src/HOL/Library/Disjoint_Sets.thy	Mon Apr 01 15:47:15 2024 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy	Tue Apr 02 08:35:43 2024 +0200
@@ -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 60b6c735b5d5 -r 6de94d690f9f src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Mon Apr 01 15:47:15 2024 +0200
+++ b/src/HOL/Library/FSet.thy	Tue Apr 02 08:35:43 2024 +0200
@@ -192,6 +192,23 @@
 
 end
 
+syntax (input)
+  "_fBall"       :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      ("(3! (_/|:|_)./ _)" [0, 0, 10] 10)
+  "_fBex"        :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      ("(3? (_/|:|_)./ _)" [0, 0, 10] 10)
+
+syntax
+  "_fBall"       :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>(_/|\<in>|_)./ _)" [0, 0, 10] 10)
+  "_fBex"        :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>(_/|\<in>|_)./ _)" [0, 0, 10] 10)
+
+translations
+  "\<forall>x|\<in>|A. P" \<rightleftharpoons> "CONST FSet.Ball A (\<lambda>x. P)"
+  "\<exists>x|\<in>|A. P" \<rightleftharpoons> "CONST FSet.Bex A (\<lambda>x. P)"
+
+print_translation \<open>
+ [Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>fBall\<close> \<^syntax_const>\<open>_fBall\<close>,
+  Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>fBex\<close> \<^syntax_const>\<open>_fBex\<close>]
+\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
+
 context includes lifting_syntax
 begin
 
diff -r 60b6c735b5d5 -r 6de94d690f9f src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Mon Apr 01 15:47:15 2024 +0200
+++ b/src/HOL/Library/Multiset_Order.thy	Tue Apr 02 08:35:43 2024 +0200
@@ -813,7 +813,16 @@
 lemma wf_less_multiset: "wf {(M :: 'a multiset, N). M < N}"
   unfolding less_multiset_def multp_def by (auto intro: wf_mult wf)
 
-instance by standard (metis less_multiset_def multp_def wf wf_def wf_mult)
+instance
+proof intro_classes
+  fix P :: "'a multiset \<Rightarrow> bool" and a :: "'a multiset"
+  have "wfp ((<) :: 'a \<Rightarrow> 'a \<Rightarrow> bool)"
+    using wfp_on_less .
+  hence "wfp ((<) :: 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool)"
+    unfolding less_multiset_def by (rule wfP_multp)
+  thus "(\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P a"
+    unfolding wfp_on_def[of UNIV, simplified] by metis
+qed
 
 end
 
diff -r 60b6c735b5d5 -r 6de94d690f9f src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Mon Apr 01 15:47:15 2024 +0200
+++ b/src/HOL/ZF/Games.thy	Tue Apr 02 08:35:43 2024 +0200
@@ -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