--- a/src/ZF/Cardinal.thy Mon Nov 30 19:33:07 2020 +0000
+++ b/src/ZF/Cardinal.thy Mon Nov 30 22:00:23 2020 +0000
@@ -329,7 +329,7 @@
lemma Least_cong: "(!!y. P(y) \<longleftrightarrow> Q(y)) ==> (\<mu> x. P(x)) = (\<mu> x. Q(x))"
by simp
-(*Need AC to get @{term"X \<lesssim> Y ==> |X| \<le> |Y|"}; see well_ord_lepoll_imp_Card_le
+(*Need AC to get @{term"X \<lesssim> Y ==> |X| \<le> |Y|"}; see well_ord_lepoll_imp_cardinal_le
Converse also requires AC, but see well_ord_cardinal_eqE*)
lemma cardinal_cong: "X \<approx> Y ==> |X| = |Y|"
apply (unfold eqpoll_def cardinal_def)
@@ -507,7 +507,7 @@
by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
(*Can use AC or finiteness to discharge first premise*)
-lemma well_ord_lepoll_imp_Card_le:
+lemma well_ord_lepoll_imp_cardinal_le:
assumes wB: "well_ord(B,r)" and AB: "A \<lesssim> B"
shows "|A| \<le> |B|"
using Ord_cardinal [of A] Ord_cardinal [of B]
@@ -528,7 +528,7 @@
lemma lepoll_cardinal_le: "[| A \<lesssim> i; Ord(i) |] ==> |A| \<le> i"
apply (rule le_trans)
-apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption)
+apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_cardinal_le], assumption)
apply (erule Ord_cardinal_le)
done
--- a/src/ZF/CardinalArith.thy Mon Nov 30 19:33:07 2020 +0000
+++ b/src/ZF/CardinalArith.thy Mon Nov 30 22:00:23 2020 +0000
@@ -151,7 +151,7 @@
have "K \<le> |K|"
by (rule Card_cardinal_le [OF K])
moreover have "|K| \<le> |K + L|" using K L
- by (blast intro: well_ord_lepoll_imp_Card_le sum_lepoll_self
+ by (blast intro: well_ord_lepoll_imp_cardinal_le sum_lepoll_self
well_ord_radd well_ord_Memrel Card_is_Ord)
ultimately show "K \<le> |K + L|"
by (blast intro: le_trans)
@@ -173,7 +173,7 @@
"[| K' \<le> K; L' \<le> L |] ==> (K' \<oplus> L') \<le> (K \<oplus> L)"
apply (unfold cadd_def)
apply (safe dest!: le_subset_iff [THEN iffD1])
-apply (rule well_ord_lepoll_imp_Card_le)
+apply (rule well_ord_lepoll_imp_cardinal_le)
apply (blast intro: well_ord_radd well_ord_Memrel)
apply (blast intro: sum_lepoll_mono subset_imp_lepoll)
done
@@ -308,7 +308,7 @@
lemma cmult_square_le: "Card(K) ==> K \<le> K \<otimes> K"
apply (unfold cmult_def)
apply (rule le_trans)
-apply (rule_tac [2] well_ord_lepoll_imp_Card_le)
+apply (rule_tac [2] well_ord_lepoll_imp_cardinal_le)
apply (rule_tac [3] prod_square_lepoll)
apply (simp add: le_refl Card_is_Ord Card_cardinal_eq)
apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord)
@@ -325,7 +325,7 @@
lemma cmult_le_self:
"[| Card(K); Ord(L); 0<L |] ==> K \<le> (K \<otimes> L)"
apply (unfold cmult_def)
-apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le])
+apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_cardinal_le])
apply assumption
apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord)
apply (blast intro: prod_lepoll_self ltD)
@@ -347,7 +347,7 @@
"[| K' \<le> K; L' \<le> L |] ==> (K' \<otimes> L') \<le> (K \<otimes> L)"
apply (unfold cmult_def)
apply (safe dest!: le_subset_iff [THEN iffD1])
-apply (rule well_ord_lepoll_imp_Card_le)
+apply (rule well_ord_lepoll_imp_cardinal_le)
apply (blast intro: well_ord_rmult well_ord_Memrel)
apply (blast intro: prod_lepoll_mono subset_imp_lepoll)
done
@@ -548,7 +548,7 @@
assumes K: "Limit(K)" and x: "x<K" and y: " y<K"
defines "z \<equiv> succ(x \<union> y)"
shows "|ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle>| \<le> |succ(z)| \<otimes> |succ(z)|"
-proof (unfold cmult_def, rule well_ord_lepoll_imp_Card_le)
+proof (unfold cmult_def, rule well_ord_lepoll_imp_cardinal_le)
show "well_ord(|succ(z)| \<times> |succ(z)|,
rmult(|succ(z)|, Memrel(|succ(z)|), |succ(z)|, Memrel(|succ(z)|)))"
by (blast intro: Ord_cardinal well_ord_Memrel well_ord_rmult)
@@ -627,10 +627,10 @@
(*Main result: Kunen's Theorem 10.12*)
lemma InfCard_csquare_eq:
- assumes IK: "InfCard(K)" shows "InfCard(K) ==> K \<otimes> K = K"
+ assumes IK: "InfCard(K)" shows "K \<otimes> K = K"
proof -
have OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card)
- show "InfCard(K) ==> K \<otimes> K = K" using OK
+ show "K \<otimes> K = K" using OK IK
proof (induct rule: trans_induct)
case (step i)
show "i \<otimes> i = i"
@@ -935,6 +935,6 @@
qed
lemma Ord_nat_subset_into_Card: "[| Ord(i); i \<subseteq> nat |] ==> Card(i)"
-by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card)
+ by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card)
end
--- a/src/ZF/Cardinal_AC.thy Mon Nov 30 19:33:07 2020 +0000
+++ b/src/ZF/Cardinal_AC.thy Mon Nov 30 22:00:23 2020 +0000
@@ -33,9 +33,9 @@
==> |A \<union> C| = |B \<union> D|"
by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
-lemma lepoll_imp_Card_le: "A \<lesssim> B ==> |A| \<le> |B|"
+lemma lepoll_imp_cardinal_le: "A \<lesssim> B ==> |A| \<le> |B|"
apply (rule AC_well_ord [THEN exE])
-apply (erule well_ord_lepoll_imp_Card_le, assumption)
+apply (erule well_ord_lepoll_imp_cardinal_le, assumption)
done
lemma cadd_assoc: "(i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
@@ -82,7 +82,7 @@
lemma le_Card_iff: "Card(K) ==> |A| \<le> K \<longleftrightarrow> A \<lesssim> K"
apply (erule Card_cardinal_eq [THEN subst], rule iffI,
erule Card_le_imp_lepoll)
-apply (erule lepoll_imp_Card_le)
+apply (erule lepoll_imp_cardinal_le)
done
lemma cardinal_0_iff_0 [simp]: "|A| = 0 \<longleftrightarrow> A = 0"
@@ -132,7 +132,7 @@
text\<open>Kunen's Lemma 10.20\<close>
lemma surj_implies_cardinal_le:
assumes f: "f \<in> surj(X,Y)" shows "|Y| \<le> |X|"
-proof (rule lepoll_imp_Card_le)
+proof (rule lepoll_imp_cardinal_le)
from f [THEN surj_implies_inj] obtain g where "g \<in> inj(Y,X)" ..
thus "Y \<lesssim> X"
by (auto simp add: lepoll_def)
--- a/src/ZF/Constructible/Formula.thy Mon Nov 30 19:33:07 2020 +0000
+++ b/src/ZF/Constructible/Formula.thy Mon Nov 30 22:00:23 2020 +0000
@@ -80,21 +80,19 @@
(\<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. satisfies(A,p) ` (Cons(x,env)) = 1))"
-lemma "p \<in> formula ==> satisfies(A,p) \<in> list(A) -> bool"
+lemma satisfies_type: "p \<in> formula \<Longrightarrow> satisfies(A,p) \<in> list(A) -> bool"
by (induct set: formula) simp_all
abbreviation
sats :: "[i,i,i] => o" where
"sats(A,p,env) == satisfies(A,p)`env = 1"
-lemma [simp]:
- "env \<in> list(A)
- ==> sats(A, Member(x,y), env) \<longleftrightarrow> nth(x,env) \<in> nth(y,env)"
+lemma sats_Member_iff [simp]:
+ "env \<in> list(A) \<Longrightarrow> sats(A, Member(x,y), env) \<longleftrightarrow> nth(x,env) \<in> nth(y,env)"
by simp
-lemma [simp]:
- "env \<in> list(A)
- ==> sats(A, Equal(x,y), env) \<longleftrightarrow> nth(x,env) = nth(y,env)"
+lemma sats_Equal_iff [simp]:
+ "env \<in> list(A) \<Longrightarrow> sats(A, Equal(x,y), env) \<longleftrightarrow> nth(x,env) = nth(y,env)"
by simp
lemma sats_Nand_iff [simp]:
--- a/src/ZF/Constructible/Rank.thy Mon Nov 30 19:33:07 2020 +0000
+++ b/src/ZF/Constructible/Rank.thy Mon Nov 30 22:00:23 2020 +0000
@@ -397,7 +397,7 @@
text\<open>(b) Order types are absolute\<close>
-theorem (in M_ordertype)
+theorem (in M_ordertype) ordertypes_are_absolute:
"[| wellordered(M,A,r); f \<in> ord_iso(A, r, i, Memrel(i));
M(A); M(r); M(f); M(i); Ord(i) |] ==> i = ordertype(A,r)"
by (blast intro: Ord_ordertype relativized_imp_well_ord ordertype_ord_iso
--- a/src/ZF/Constructible/Wellorderings.thy Mon Nov 30 19:33:07 2020 +0000
+++ b/src/ZF/Constructible/Wellorderings.thy Mon Nov 30 22:00:23 2020 +0000
@@ -137,8 +137,8 @@
by (unfold transitive_rel_def trans_on_def, blast)
lemma (in M_basic) wf_on_imp_relativized:
- "wf[A](r) ==> wellfounded_on(M,A,r)"
-apply (simp add: wellfounded_on_def wf_def wf_on_def, clarify)
+ "wf[A](r) \<Longrightarrow> wellfounded_on(M,A,r)"
+apply (clarsimp simp: wellfounded_on_def wf_def wf_on_def)
apply (drule_tac x=x in spec, blast)
done
@@ -164,17 +164,15 @@
==> order_isomorphism(M,A,r,B,s,f) \<longleftrightarrow> f \<in> ord_iso(A,r,B,s)"
by (simp add: order_isomorphism_def ord_iso_def)
-lemma (in M_basic) pred_set_abs [simp]:
+lemma (in M_trans) pred_set_abs [simp]:
"[| M(r); M(B) |] ==> pred_set(M,A,x,r,B) \<longleftrightarrow> B = Order.pred(A,x,r)"
apply (simp add: pred_set_def Order.pred_def)
apply (blast dest: transM)
done
lemma (in M_basic) pred_closed [intro,simp]:
- "[| M(A); M(r); M(x) |] ==> M(Order.pred(A,x,r))"
-apply (simp add: Order.pred_def)
-apply (insert pred_separation [of r x], simp)
-done
+ "\<lbrakk>M(A); M(r); M(x)\<rbrakk> \<Longrightarrow> M(Order.pred(A, x, r))"
+ using pred_separation [of r x] by (simp add: Order.pred_def)
lemma (in M_basic) membership_abs [simp]:
"[| M(r); M(A) |] ==> membership(M,A,r) \<longleftrightarrow> r = Memrel(A)"
@@ -190,17 +188,12 @@
done
lemma (in M_basic) M_Memrel_iff:
- "M(A) ==>
- Memrel(A) = {z \<in> A*A. \<exists>x[M]. \<exists>y[M]. z = \<langle>x,y\<rangle> & x \<in> y}"
-apply (simp add: Memrel_def)
-apply (blast dest: transM)
-done
+ "M(A) \<Longrightarrow> Memrel(A) = {z \<in> A*A. \<exists>x[M]. \<exists>y[M]. z = \<langle>x,y\<rangle> & x \<in> y}"
+unfolding Memrel_def by (blast dest: transM)
lemma (in M_basic) Memrel_closed [intro,simp]:
- "M(A) ==> M(Memrel(A))"
-apply (simp add: M_Memrel_iff)
-apply (insert Memrel_separation, simp)
-done
+ "M(A) \<Longrightarrow> M(Memrel(A))"
+ using Memrel_separation by (simp add: M_Memrel_iff)
subsection \<open>Main results of Kunen, Chapter 1 section 6\<close>
@@ -208,19 +201,19 @@
text\<open>Subset properties-- proved outside the locale\<close>
lemma linear_rel_subset:
- "[| linear_rel(M,A,r); B<=A |] ==> linear_rel(M,B,r)"
+ "\<lbrakk>linear_rel(M, A, r); B \<subseteq> A\<rbrakk> \<Longrightarrow> linear_rel(M, B, r)"
by (unfold linear_rel_def, blast)
lemma transitive_rel_subset:
- "[| transitive_rel(M,A,r); B<=A |] ==> transitive_rel(M,B,r)"
+ "\<lbrakk>transitive_rel(M, A, r); B \<subseteq> A\<rbrakk> \<Longrightarrow> transitive_rel(M, B, r)"
by (unfold transitive_rel_def, blast)
lemma wellfounded_on_subset:
- "[| wellfounded_on(M,A,r); B<=A |] ==> wellfounded_on(M,B,r)"
+ "\<lbrakk>wellfounded_on(M, A, r); B \<subseteq> A\<rbrakk> \<Longrightarrow> wellfounded_on(M, B, r)"
by (unfold wellfounded_on_def subset_def, blast)
lemma wellordered_subset:
- "[| wellordered(M,A,r); B<=A |] ==> wellordered(M,B,r)"
+ "\<lbrakk>wellordered(M, A, r); B \<subseteq> A\<rbrakk> \<Longrightarrow> wellordered(M, B, r)"
apply (unfold wellordered_def)
apply (blast intro: linear_rel_subset transitive_rel_subset
wellfounded_on_subset)
--- a/src/ZF/InfDatatype.thy Mon Nov 30 19:33:07 2020 +0000
+++ b/src/ZF/InfDatatype.thy Mon Nov 30 22:00:23 2020 +0000
@@ -103,7 +103,7 @@
lemmas le_nat_Un_cardinal =
Un_upper2_le [OF Ord_nat Card_cardinal [THEN Card_is_Ord]]
-lemmas UN_upper_cardinal = UN_upper [THEN subset_imp_lepoll, THEN lepoll_imp_Card_le]
+lemmas UN_upper_cardinal = UN_upper [THEN subset_imp_lepoll, THEN lepoll_imp_cardinal_le]
(*The new version of Data_Arg.intrs, declared in Datatype.ML*)
lemmas Data_Arg_intros =