--- 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)"
--- 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)
--- 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'"
--- 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
--- 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)"
--- 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"
--- 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
--- 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
--- 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