# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1666105141 -3600
# Node ID 332b76850f0e5a2f0cee381aecd892378f16d46b
# Parent  e5162a8baa2458d3e70d0b994491746bfb19fba6
Slight tidying of legacy proofs

diff -r e5162a8baa24 -r 332b76850f0e src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Mon Oct 17 16:00:41 2022 +0100
+++ b/src/ZF/ZF_Base.thy	Tue Oct 18 15:59:01 2022 +0100
@@ -313,13 +313,13 @@
 lemma rev_bspec: "\<lbrakk>x: A;  \<forall>x\<in>A. P(x)\<rbrakk> \<Longrightarrow> P(x)"
 by (simp add: Ball_def)
 
-(*Trival rewrite rule;   @{term"(\<forall>x\<in>A.P)<->P"} holds only if A is nonempty!*)
-lemma ball_triv [simp]: "(\<forall>x\<in>A. P) <-> ((\<exists>x. x\<in>A) \<longrightarrow> P)"
+(*Trival rewrite rule;   @{term"(\<forall>x\<in>A.P)\<longleftrightarrow>P"} holds only if A is nonempty!*)
+lemma ball_triv [simp]: "(\<forall>x\<in>A. P) \<longleftrightarrow> ((\<exists>x. x\<in>A) \<longrightarrow> P)"
 by (simp add: Ball_def)
 
 (*Congruence rule for rewriting*)
 lemma ball_cong [cong]:
-    "\<lbrakk>A=A';  \<And>x. x\<in>A' \<Longrightarrow> P(x) <-> P'(x)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>A. P(x)) <-> (\<forall>x\<in>A'. P'(x))"
+    "\<lbrakk>A=A';  \<And>x. x\<in>A' \<Longrightarrow> P(x) \<longleftrightarrow> P'(x)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>A. P(x)) \<longleftrightarrow> (\<forall>x\<in>A'. P'(x))"
 by (simp add: Ball_def)
 
 lemma atomize_ball:
@@ -346,13 +346,13 @@
 lemma bexE [elim!]: "\<lbrakk>\<exists>x\<in>A. P(x);  \<And>x. \<lbrakk>x\<in>A; P(x)\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
 by (simp add: Bex_def, blast)
 
-(*We do not even have @{term"(\<exists>x\<in>A. True) <-> True"} unless @{term"A" is nonempty\<And>*)
-lemma bex_triv [simp]: "(\<exists>x\<in>A. P) <-> ((\<exists>x. x\<in>A) \<and> P)"
+(*We do not even have @{term"(\<exists>x\<in>A. True) \<longleftrightarrow> True"} unless @{term"A" is nonempty\<And>*)
+lemma bex_triv [simp]: "(\<exists>x\<in>A. P) \<longleftrightarrow> ((\<exists>x. x\<in>A) \<and> P)"
 by (simp add: Bex_def)
 
 lemma bex_cong [cong]:
-    "\<lbrakk>A=A';  \<And>x. x\<in>A' \<Longrightarrow> P(x) <-> P'(x)\<rbrakk>
-     \<Longrightarrow> (\<exists>x\<in>A. P(x)) <-> (\<exists>x\<in>A'. P'(x))"
+    "\<lbrakk>A=A';  \<And>x. x\<in>A' \<Longrightarrow> P(x) \<longleftrightarrow> P'(x)\<rbrakk>
+     \<Longrightarrow> (\<exists>x\<in>A. P(x)) \<longleftrightarrow> (\<exists>x\<in>A'. P'(x))"
 by (simp add: Bex_def cong: conj_cong)
 
 
@@ -375,27 +375,25 @@
 by (simp add: subset_def, blast)
 
 (*Sometimes useful with premises in this order*)
-lemma rev_subsetD: "\<lbrakk>c\<in>A; A<=B\<rbrakk> \<Longrightarrow> c\<in>B"
+lemma rev_subsetD: "\<lbrakk>c\<in>A; A\<subseteq>B\<rbrakk> \<Longrightarrow> c\<in>B"
 by blast
 
 lemma contra_subsetD: "\<lbrakk>A \<subseteq> B; c \<notin> B\<rbrakk> \<Longrightarrow> c \<notin> A"
-by blast
+  by blast
 
 lemma rev_contra_subsetD: "\<lbrakk>c \<notin> B;  A \<subseteq> B\<rbrakk> \<Longrightarrow> c \<notin> A"
-by blast
+  by blast
 
 lemma subset_refl [simp]: "A \<subseteq> A"
-by blast
+  by blast
 
-lemma subset_trans: "\<lbrakk>A<=B;  B<=C\<rbrakk> \<Longrightarrow> A<=C"
-by blast
+lemma subset_trans: "\<lbrakk>A\<subseteq>B;  B\<subseteq>C\<rbrakk> \<Longrightarrow> A\<subseteq>C"
+  by blast
 
-(*Useful for proving A<=B by rewriting in some cases*)
+(*Useful for proving A\<subseteq>B by rewriting in some cases*)
 lemma subset_iff:
-     "A<=B <-> (\<forall>x. x\<in>A \<longrightarrow> x\<in>B)"
-  unfolding subset_def Ball_def
-apply (rule iff_refl)
-done
+     "A\<subseteq>B \<longleftrightarrow> (\<forall>x. x\<in>A \<longrightarrow> x\<in>B)"
+  by auto
 
 text\<open>For calculations\<close>
 declare subsetD [trans] rev_subsetD [trans] subset_trans [trans]
@@ -405,34 +403,33 @@
 
 (*Anti-symmetry of the subset relation*)
 lemma equalityI [intro]: "\<lbrakk>A \<subseteq> B;  B \<subseteq> A\<rbrakk> \<Longrightarrow> A = B"
-by (rule extension [THEN iffD2], rule conjI)
+  by (rule extension [THEN iffD2], rule conjI)
 
 
-lemma equality_iffI: "(\<And>x. x\<in>A <-> x\<in>B) \<Longrightarrow> A = B"
-by (rule equalityI, blast+)
+lemma equality_iffI: "(\<And>x. x\<in>A \<longleftrightarrow> x\<in>B) \<Longrightarrow> A = B"
+  by (rule equalityI, blast+)
 
 lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1]
 lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2]
 
-lemma equalityE: "\<lbrakk>A = B;  \<lbrakk>A<=B; B<=A\<rbrakk> \<Longrightarrow> P\<rbrakk>  \<Longrightarrow>  P"
-by (blast dest: equalityD1 equalityD2)
+lemma equalityE: "\<lbrakk>A = B;  \<lbrakk>A\<subseteq>B; B\<subseteq>A\<rbrakk> \<Longrightarrow> P\<rbrakk>  \<Longrightarrow>  P"
+  by (blast dest: equalityD1 equalityD2)
 
 lemma equalityCE:
-    "\<lbrakk>A = B;  \<lbrakk>c\<in>A; c\<in>B\<rbrakk> \<Longrightarrow> P;  \<lbrakk>c\<notin>A; c\<notin>B\<rbrakk> \<Longrightarrow> P\<rbrakk>  \<Longrightarrow>  P"
-by (erule equalityE, blast)
+  "\<lbrakk>A = B;  \<lbrakk>c\<in>A; c\<in>B\<rbrakk> \<Longrightarrow> P;  \<lbrakk>c\<notin>A; c\<notin>B\<rbrakk> \<Longrightarrow> P\<rbrakk>  \<Longrightarrow>  P"
+  by (erule equalityE, blast)
 
 lemma equality_iffD:
-  "A = B \<Longrightarrow> (\<And>x. x \<in> A <-> x \<in> B)"
+  "A = B \<Longrightarrow> (\<And>x. x \<in> A \<longleftrightarrow> x \<in> B)"
   by auto
 
 
 subsection\<open>Rules for Replace -- the derived form of replacement\<close>
 
 lemma Replace_iff:
-    "b \<in> {y. x\<in>A, P(x,y)}  <->  (\<exists>x\<in>A. P(x,b) \<and> (\<forall>y. P(x,y) \<longrightarrow> y=b))"
+    "b \<in> {y. x\<in>A, P(x,y)}  \<longleftrightarrow>  (\<exists>x\<in>A. P(x,b) \<and> (\<forall>y. P(x,y) \<longrightarrow> y=b))"
   unfolding Replace_def
-apply (rule replacement [THEN iff_trans], blast+)
-done
+  by (rule replacement [THEN iff_trans], blast+)
 
 (*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
 lemma ReplaceI [intro]:
@@ -449,17 +446,16 @@
 
 (*As above but without the (generally useless) 3rd assumption*)
 lemma ReplaceE2 [elim!]:
-    "\<lbrakk>b \<in> {y. x\<in>A, P(x,y)};
+  "\<lbrakk>b \<in> {y. x\<in>A, P(x,y)};
         \<And>x. \<lbrakk>x: A;  P(x,b)\<rbrakk> \<Longrightarrow> R
-\<rbrakk> \<Longrightarrow> R"
-by (erule ReplaceE, blast)
+   \<rbrakk> \<Longrightarrow> R"
+  by (erule ReplaceE, blast)
 
 lemma Replace_cong [cong]:
-    "\<lbrakk>A=B;  \<And>x y. x\<in>B \<Longrightarrow> P(x,y) <-> Q(x,y)\<rbrakk> \<Longrightarrow>
-     Replace(A,P) = Replace(B,Q)"
-apply (rule equality_iffI)
-apply (simp add: Replace_iff)
-done
+  "\<lbrakk>A=B;  \<And>x y. x\<in>B \<Longrightarrow> P(x,y) \<longleftrightarrow> Q(x,y)\<rbrakk> \<Longrightarrow> Replace(A,P) = Replace(B,Q)"
+  apply (rule equality_iffI)
+  apply (simp add: Replace_iff)
+  done
 
 
 subsection\<open>Rules for RepFun\<close>
@@ -469,49 +465,44 @@
 
 (*Useful for coinduction proofs*)
 lemma RepFun_eqI [intro]: "\<lbrakk>b=f(a);  a \<in> A\<rbrakk> \<Longrightarrow> b \<in> {f(x). x\<in>A}"
-apply (erule ssubst)
-apply (erule RepFunI)
-done
+  by (blast intro: RepFunI)
 
 lemma RepFunE [elim!]:
-    "\<lbrakk>b \<in> {f(x). x\<in>A};
+  "\<lbrakk>b \<in> {f(x). x\<in>A};
         \<And>x.\<lbrakk>x\<in>A;  b=f(x)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow>
      P"
-by (simp add: RepFun_def Replace_iff, blast)
+  by (simp add: RepFun_def Replace_iff, blast)
 
 lemma RepFun_cong [cong]:
-    "\<lbrakk>A=B;  \<And>x. x\<in>B \<Longrightarrow> f(x)=g(x)\<rbrakk> \<Longrightarrow> RepFun(A,f) = RepFun(B,g)"
-by (simp add: RepFun_def)
+  "\<lbrakk>A=B;  \<And>x. x\<in>B \<Longrightarrow> f(x)=g(x)\<rbrakk> \<Longrightarrow> RepFun(A,f) = RepFun(B,g)"
+  by (simp add: RepFun_def)
 
-lemma RepFun_iff [simp]: "b \<in> {f(x). x\<in>A} <-> (\<exists>x\<in>A. b=f(x))"
-by (unfold Bex_def, blast)
+lemma RepFun_iff [simp]: "b \<in> {f(x). x\<in>A} \<longleftrightarrow> (\<exists>x\<in>A. b=f(x))"
+  by (unfold Bex_def, blast)
 
 lemma triv_RepFun [simp]: "{x. x\<in>A} = A"
-by blast
+  by blast
 
 
 subsection\<open>Rules for Collect -- forming a subset by separation\<close>
 
 (*Separation is derivable from Replacement*)
-lemma separation [simp]: "a \<in> {x\<in>A. P(x)} <-> a\<in>A \<and> P(a)"
-by (unfold Collect_def, blast)
+lemma separation [simp]: "a \<in> {x\<in>A. P(x)} \<longleftrightarrow> a\<in>A \<and> P(a)"
+  by (auto simp: Collect_def)
 
 lemma CollectI [intro!]: "\<lbrakk>a\<in>A;  P(a)\<rbrakk> \<Longrightarrow> a \<in> {x\<in>A. P(x)}"
-by simp
+  by simp
 
 lemma CollectE [elim!]: "\<lbrakk>a \<in> {x\<in>A. P(x)};  \<lbrakk>a\<in>A; P(a)\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
-by simp
+  by simp
 
-lemma CollectD1: "a \<in> {x\<in>A. P(x)} \<Longrightarrow> a\<in>A"
-by (erule CollectE, assumption)
-
-lemma CollectD2: "a \<in> {x\<in>A. P(x)} \<Longrightarrow> P(a)"
-by (erule CollectE, assumption)
+lemma CollectD1: "a \<in> {x\<in>A. P(x)} \<Longrightarrow> a\<in>A" and CollectD2: "a \<in> {x\<in>A. P(x)} \<Longrightarrow> P(a)"
+  by auto
 
 lemma Collect_cong [cong]:
-    "\<lbrakk>A=B;  \<And>x. x\<in>B \<Longrightarrow> P(x) <-> Q(x)\<rbrakk>
+  "\<lbrakk>A=B;  \<And>x. x\<in>B \<Longrightarrow> P(x) \<longleftrightarrow> Q(x)\<rbrakk>
      \<Longrightarrow> Collect(A, \<lambda>x. P(x)) = Collect(B, \<lambda>x. Q(x))"
-by (simp add: Collect_def)
+  by (simp add: Collect_def)
 
 
 subsection\<open>Rules for Unions\<close>
@@ -520,30 +511,30 @@
 
 (*The order of the premises presupposes that C is rigid; A may be flexible*)
 lemma UnionI [intro]: "\<lbrakk>B: C;  A: B\<rbrakk> \<Longrightarrow> A: \<Union>(C)"
-by (simp, blast)
+  by auto
 
 lemma UnionE [elim!]: "\<lbrakk>A \<in> \<Union>(C);  \<And>B.\<lbrakk>A: B;  B: C\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
-by (simp, blast)
+  by auto
 
 
 subsection\<open>Rules for Unions of families\<close>
 (* @{term"\<Union>x\<in>A. B(x)"} abbreviates @{term"\<Union>({B(x). x\<in>A})"} *)
 
-lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B(x)) <-> (\<exists>x\<in>A. b \<in> B(x))"
-by (simp add: Bex_def, blast)
+lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B(x)) \<longleftrightarrow> (\<exists>x\<in>A. b \<in> B(x))"
+  by blast
 
 (*The order of the premises presupposes that A is rigid; b may be flexible*)
 lemma UN_I: "\<lbrakk>a: A;  b: B(a)\<rbrakk> \<Longrightarrow> b: (\<Union>x\<in>A. B(x))"
-by (simp, blast)
+  by force
 
 
 lemma UN_E [elim!]:
-    "\<lbrakk>b \<in> (\<Union>x\<in>A. B(x));  \<And>x.\<lbrakk>x: A;  b: B(x)\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
-by blast
+  "\<lbrakk>b \<in> (\<Union>x\<in>A. B(x));  \<And>x.\<lbrakk>x: A;  b: B(x)\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+  by blast
 
 lemma UN_cong:
-    "\<lbrakk>A=B;  \<And>x. x\<in>B \<Longrightarrow> C(x)=D(x)\<rbrakk> \<Longrightarrow> (\<Union>x\<in>A. C(x)) = (\<Union>x\<in>B. D(x))"
-by simp
+  "\<lbrakk>A=B;  \<And>x. x\<in>B \<Longrightarrow> C(x)=D(x)\<rbrakk> \<Longrightarrow> (\<Union>x\<in>A. C(x)) = (\<Union>x\<in>B. D(x))"
+  by simp
 
 
 (*No "Addcongs [UN_cong]" because @{term\<Union>} is a combination of constants*)
@@ -558,69 +549,67 @@
 (*The set @{term"{x\<in>0. False}"} is empty; by foundation it equals 0
   See Suppes, page 21.*)
 lemma not_mem_empty [simp]: "a \<notin> 0"
-apply (cut_tac foundation)
-apply (best dest: equalityD2)
-done
+  using foundation by (best dest: equalityD2)
 
 lemmas emptyE [elim!] = not_mem_empty [THEN notE]
 
 
 lemma empty_subsetI [simp]: "0 \<subseteq> A"
-by blast
+  by blast
 
 lemma equals0I: "\<lbrakk>\<And>y. y\<in>A \<Longrightarrow> False\<rbrakk> \<Longrightarrow> A=0"
-by blast
+  by blast
 
 lemma equals0D [dest]: "A=0 \<Longrightarrow> a \<notin> A"
-by blast
+  by blast
 
 declare sym [THEN equals0D, dest]
 
 lemma not_emptyI: "a\<in>A \<Longrightarrow> A \<noteq> 0"
-by blast
+  by blast
 
 lemma not_emptyE:  "\<lbrakk>A \<noteq> 0;  \<And>x. x\<in>A \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
-by blast
+  by blast
 
 
 subsection\<open>Rules for Inter\<close>
 
 (*Not obviously useful for proving InterI, InterD, InterE*)
-lemma Inter_iff: "A \<in> \<Inter>(C) <-> (\<forall>x\<in>C. A: x) \<and> C\<noteq>0"
-by (simp add: Inter_def Ball_def, blast)
+lemma Inter_iff: "A \<in> \<Inter>(C) \<longleftrightarrow> (\<forall>x\<in>C. A: x) \<and> C\<noteq>0"
+  by (force simp: Inter_def)
 
 (* Intersection is well-behaved only if the family is non-empty! *)
 lemma InterI [intro!]:
-    "\<lbrakk>\<And>x. x: C \<Longrightarrow> A: x;  C\<noteq>0\<rbrakk> \<Longrightarrow> A \<in> \<Inter>(C)"
-by (simp add: Inter_iff)
+  "\<lbrakk>\<And>x. x: C \<Longrightarrow> A: x;  C\<noteq>0\<rbrakk> \<Longrightarrow> A \<in> \<Inter>(C)"
+  by (simp add: Inter_iff)
 
 (*A "destruct" rule -- every B in C contains A as an element, but
   A\<in>B can hold when B\<in>C does not!  This rule is analogous to "spec". *)
 lemma InterD [elim, Pure.elim]: "\<lbrakk>A \<in> \<Inter>(C);  B \<in> C\<rbrakk> \<Longrightarrow> A \<in> B"
-by (unfold Inter_def, blast)
+  by (force simp: Inter_def)
 
 (*"Classical" elimination rule -- does not require exhibiting @{term"B\<in>C"} *)
 lemma InterE [elim]:
-    "\<lbrakk>A \<in> \<Inter>(C);  B\<notin>C \<Longrightarrow> R;  A\<in>B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
-by (simp add: Inter_def, blast)
+  "\<lbrakk>A \<in> \<Inter>(C);  B\<notin>C \<Longrightarrow> R;  A\<in>B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+  by (auto simp: Inter_def)
 
 
 subsection\<open>Rules for Intersections of families\<close>
 
 (* @{term"\<Inter>x\<in>A. B(x)"} abbreviates @{term"\<Inter>({B(x). x\<in>A})"} *)
 
-lemma INT_iff: "b \<in> (\<Inter>x\<in>A. B(x)) <-> (\<forall>x\<in>A. b \<in> B(x)) \<and> A\<noteq>0"
-by (force simp add: Inter_def)
+lemma INT_iff: "b \<in> (\<Inter>x\<in>A. B(x)) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B(x)) \<and> A\<noteq>0"
+  by (force simp add: Inter_def)
 
 lemma INT_I: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b: B(x);  A\<noteq>0\<rbrakk> \<Longrightarrow> b: (\<Inter>x\<in>A. B(x))"
-by blast
+  by blast
 
 lemma INT_E: "\<lbrakk>b \<in> (\<Inter>x\<in>A. B(x));  a: A\<rbrakk> \<Longrightarrow> b \<in> B(a)"
-by blast
+  by blast
 
 lemma INT_cong:
-    "\<lbrakk>A=B;  \<And>x. x\<in>B \<Longrightarrow> C(x)=D(x)\<rbrakk> \<Longrightarrow> (\<Inter>x\<in>A. C(x)) = (\<Inter>x\<in>B. D(x))"
-by simp
+  "\<lbrakk>A=B;  \<And>x. x\<in>B \<Longrightarrow> C(x)=D(x)\<rbrakk> \<Longrightarrow> (\<Inter>x\<in>A. C(x)) = (\<Inter>x\<in>B. D(x))"
+  by simp
 
 (*No "Addcongs [INT_cong]" because @{term\<Inter>} is a combination of constants*)
 
@@ -628,10 +617,10 @@
 subsection\<open>Rules for Powersets\<close>
 
 lemma PowI: "A \<subseteq> B \<Longrightarrow> A \<in> Pow(B)"
-by (erule Pow_iff [THEN iffD2])
+  by (erule Pow_iff [THEN iffD2])
 
-lemma PowD: "A \<in> Pow(B)  \<Longrightarrow>  A<=B"
-by (erule Pow_iff [THEN iffD1])
+lemma PowD: "A \<in> Pow(B)  \<Longrightarrow>  A\<subseteq>B"
+  by (erule Pow_iff [THEN iffD1])
 
 declare Pow_iff [iff]
 
@@ -645,6 +634,6 @@
   make it diverge.  Variable b represents ANY map, such as
   (lam x\<in>A.b(x)): A->Pow(A). *)
 lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) \<noteq> S"
-by (best elim!: equalityCE del: ReplaceI RepFun_eqI)
+  by (best elim!: equalityCE del: ReplaceI RepFun_eqI)
 
 end