src/ZF/equalities.thy

--- a/src/ZF/equalities.thy	Tue Sep 27 16:51:35 2022 +0100
+++ b/src/ZF/equalities.thy	Tue Sep 27 17:03:23 2022 +0100
@@ -22,7 +22,7 @@
   The following are not added to the default simpset because
   (a) they duplicate the body and (b) there are no similar rules for \<open>Int\<close>.\<close>
 
-lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))"
+lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) \<and> (\<forall>x \<in> B. P(x))"
   by blast
 
 lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))"
@@ -76,7 +76,7 @@
 lemma subset_consI: "B \<subseteq> cons(a,B)"
 by blast
 
-lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C \<longleftrightarrow> a\<in>C & B\<subseteq>C"
+lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C \<longleftrightarrow> a\<in>C \<and> B\<subseteq>C"
 by blast
 
 (*A safe special case of subset elimination, adding no new variables
@@ -86,7 +86,7 @@
 lemma subset_empty_iff: "A\<subseteq>0 \<longleftrightarrow> A=0"
 by blast
 
-lemma subset_cons_iff: "C\<subseteq>cons(a,B) \<longleftrightarrow> C\<subseteq>B | (a\<in>C & C-{a} \<subseteq> B)"
+lemma subset_cons_iff: "C\<subseteq>cons(a,B) \<longleftrightarrow> C\<subseteq>B | (a\<in>C \<and> C-{a} \<subseteq> B)"
 by blast
 
 (* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
@@ -134,7 +134,7 @@
     "\<lbrakk>succ(i) \<subseteq> j;  \<lbrakk>i\<in>j;  i\<subseteq>j\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
 by (unfold succ_def, blast)
 
-lemma succ_subset_iff: "succ(a) \<subseteq> B \<longleftrightarrow> (a \<subseteq> B & a \<in> B)"
+lemma succ_subset_iff: "succ(a) \<subseteq> B \<longleftrightarrow> (a \<subseteq> B \<and> a \<in> B)"
 by (unfold succ_def, blast)
 
 
@@ -142,7 +142,7 @@
 
 (** Intersection is the greatest lower bound of two sets **)
 
-lemma Int_subset_iff: "C \<subseteq> A \<inter> B \<longleftrightarrow> C \<subseteq> A & C \<subseteq> B"
+lemma Int_subset_iff: "C \<subseteq> A \<inter> B \<longleftrightarrow> C \<subseteq> A \<and> C \<subseteq> B"
 by blast
 
 lemma Int_lower1: "A \<inter> B \<subseteq> A"
@@ -211,7 +211,7 @@
 
 (** Union is the least upper bound of two sets *)
 
-lemma Un_subset_iff: "A \<union> B \<subseteq> C \<longleftrightarrow> A \<subseteq> C & B \<subseteq> C"
+lemma Un_subset_iff: "A \<union> B \<subseteq> C \<longleftrightarrow> A \<subseteq> C \<and> B \<subseteq> C"
 by blast
 
 lemma Un_upper1: "A \<subseteq> A \<union> B"
@@ -259,7 +259,7 @@
 lemma subset_Un_iff2: "A\<subseteq>B \<longleftrightarrow> B \<union> A = B"
 by (blast elim!: equalityE)
 
-lemma Un_empty [iff]: "(A \<union> B = 0) \<longleftrightarrow> (A = 0 & B = 0)"
+lemma Un_empty [iff]: "(A \<union> B = 0) \<longleftrightarrow> (A = 0 \<and> B = 0)"
 by blast
 
 lemma Un_eq_Union: "A \<union> B = \<Union>({A, B})"
@@ -273,7 +273,7 @@
 lemma Diff_contains: "\<lbrakk>C\<subseteq>A;  C \<inter> B = 0\<rbrakk> \<Longrightarrow> C \<subseteq> A-B"
 by blast
 
-lemma subset_Diff_cons_iff: "B \<subseteq> A - cons(c,C)  \<longleftrightarrow>  B\<subseteq>A-C & c \<notin> B"
+lemma subset_Diff_cons_iff: "B \<subseteq> A - cons(c,C)  \<longleftrightarrow>  B\<subseteq>A-C \<and> c \<notin> B"
 by blast
 
 lemma Diff_cancel: "A - A = 0"
@@ -571,7 +571,7 @@
 by blast
 
 lemma times_subset_iff:
-     "(A'*B' \<subseteq> A*B) \<longleftrightarrow> (A' = 0 | B' = 0 | (A'\<subseteq>A) & (B'\<subseteq>B))"
+     "(A'*B' \<subseteq> A*B) \<longleftrightarrow> (A' = 0 | B' = 0 | (A'\<subseteq>A) \<and> (B'\<subseteq>B))"
 by blast
 
 lemma Int_Sigma_eq:
@@ -765,7 +765,7 @@
 by blast
 
 lemma Collect_image_eq:
-     "{z \<in> Sigma(A,B). P(z)} `` C = (\<Union>x \<in> A. {y \<in> B(x). x \<in> C & P(<x,y>)})"
+     "{z \<in> Sigma(A,B). P(z)} `` C = (\<Union>x \<in> A. {y \<in> B(x). x \<in> C \<and> P(<x,y>)})"
 by blast
 
 lemma image_Int_subset: "r``(A \<inter> B) \<subseteq> (r``A) \<inter> (r``B)"
@@ -941,11 +941,11 @@
 by blast
 
 lemma Collect_Collect_eq [simp]:
-     "Collect(Collect(A,P), Q) = Collect(A, %x. P(x) & Q(x))"
+     "Collect(Collect(A,P), Q) = Collect(A, %x. P(x) \<and> Q(x))"
 by blast
 
 lemma Collect_Int_Collect_eq:
-     "Collect(A,P) \<inter> Collect(A,Q) = Collect(A, %x. P(x) & Q(x))"
+     "Collect(A,P) \<inter> Collect(A,Q) = Collect(A, %x. P(x) \<and> Q(x))"
 by blast
 
 lemma Collect_Union_eq [simp]:
@@ -961,7 +961,7 @@
 lemma Collect_disj_eq: "{x\<in>A. P(x) | Q(x)} = Collect(A, P) \<union> Collect(A, Q)"
 by blast
 
-lemma Collect_conj_eq: "{x\<in>A. P(x) & Q(x)} = Collect(A, P) \<inter> Collect(A, Q)"
+lemma Collect_conj_eq: "{x\<in>A. P(x) \<and> Q(x)} = Collect(A, P) \<inter> Collect(A, Q)"
 by blast
 
 lemmas subset_SIs = subset_refl cons_subsetI subset_consI