author paulson Fri, 09 Mar 2012 17:24:00 +0000 changeset 46847 8740cea39a4a parent 46842 52e9770e0107 child 46848 13eeb06847cb
More calculation-based cardinality proofs
 src/ZF/Cardinal.thy file | annotate | diff | comparison | revisions
```--- a/src/ZF/Cardinal.thy	Thu Mar 08 16:49:24 2012 +0000
+++ b/src/ZF/Cardinal.thy	Fri Mar 09 17:24:00 2012 +0000
@@ -26,7 +26,7 @@

definition
cardinal :: "i=>i"           ("|_|")  where
-    "|A| == LEAST i. i eqpoll A"
+    "|A| == (LEAST i. i eqpoll A)"

definition
Finite   :: "i=>o"  where
@@ -42,7 +42,7 @@
lesspoll  (infixl "\<prec>" 50) and
Least     (binder "\<mu>" 10)

-notation (HTML output)
+notation (HTML)
eqpoll    (infixl "\<approx>" 50) and
Least     (binder "\<mu>" 10)

@@ -244,14 +244,14 @@
(** LEAST -- the least number operator [from HOL/Univ.ML] **)

lemma Least_equality:
-    "[| P(i);  Ord(i);  !!x. x<i ==> ~P(x) |] ==> (LEAST x. P(x)) = i"
+    "[| P(i);  Ord(i);  !!x. x<i ==> ~P(x) |] ==> (\<mu> x. P(x)) = i"
apply (unfold Least_def)
apply (rule the_equality, blast)
apply (elim conjE)
apply (erule Ord_linear_lt, assumption, blast+)
done

-lemma LeastI: "[| P(i);  Ord(i) |] ==> P(LEAST x. P(x))"
+lemma LeastI: "[| P(i);  Ord(i) |] ==> P(\<mu> x. P(x))"
apply (erule rev_mp)
apply (erule_tac i=i in trans_induct)
apply (rule impI)
@@ -260,7 +260,7 @@
done

(*Proof is almost identical to the one above!*)
-lemma Least_le: "[| P(i);  Ord(i) |] ==> (LEAST x. P(x)) \<le> i"
+lemma Least_le: "[| P(i);  Ord(i) |] ==> (\<mu> x. P(x)) \<le> i"
apply (erule rev_mp)
apply (erule_tac i=i in trans_induct)
apply (rule impI)
@@ -271,24 +271,24 @@
done

(*LEAST really is the smallest*)
-lemma less_LeastE: "[| P(i);  i < (LEAST x. P(x)) |] ==> Q"
+lemma less_LeastE: "[| P(i);  i < (\<mu> x. P(x)) |] ==> Q"
apply (rule Least_le [THEN  lt_trans2, THEN lt_irrefl], assumption+)
done

(*Easier to apply than LeastI: conclusion has only one occurrence of P*)
lemma LeastI2:
-    "[| P(i);  Ord(i);  !!j. P(j) ==> Q(j) |] ==> Q(LEAST j. P(j))"
+    "[| P(i);  Ord(i);  !!j. P(j) ==> Q(j) |] ==> Q(\<mu> j. P(j))"
by (blast intro: LeastI )

(*If there is no such P then LEAST is vacuously 0*)
lemma Least_0:
-    "[| ~ (\<exists>i. Ord(i) & P(i)) |] ==> (LEAST x. P(x)) = 0"
+    "[| ~ (\<exists>i. Ord(i) & P(i)) |] ==> (\<mu> x. P(x)) = 0"
apply (unfold Least_def)
apply (rule the_0, blast)
done

-lemma Ord_Least [intro,simp,TC]: "Ord(LEAST x. P(x))"
+lemma Ord_Least [intro,simp,TC]: "Ord(\<mu> x. P(x))"
apply (case_tac "\<exists>i. Ord(i) & P(i)")
apply safe
apply (rule Least_le [THEN ltE])
@@ -301,8 +301,7 @@
(** Basic properties of cardinals **)

(*Not needed for simplification, but helpful below*)
-lemma Least_cong:
-     "(!!y. P(y) \<longleftrightarrow> Q(y)) ==> (LEAST x. P(x)) = (LEAST x. Q(x))"
+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
@@ -329,11 +328,14 @@
by (rule Ord_cardinal_eqpoll [THEN cardinal_cong])

lemma well_ord_cardinal_eqE:
-     "[| well_ord(X,r);  well_ord(Y,s);  |X| = |Y| |] ==> X \<approx> Y"
-apply (rule eqpoll_sym [THEN eqpoll_trans])
-apply (erule well_ord_cardinal_eqpoll)
-done
+  assumes woX: "well_ord(X,r)" and woY: "well_ord(Y,s)" and eq: "|X| = |Y|"
+shows "X \<approx> Y"
+proof -
+  have "X \<approx> |X|" by (blast intro: well_ord_cardinal_eqpoll [OF woX] eqpoll_sym)
+  also have "... = |Y|" by (rule eq)
+  also have "... \<approx> Y" by (rule well_ord_cardinal_eqpoll [OF woY])
+  finally show ?thesis .
+qed

lemma well_ord_cardinal_eqpoll_iff:
"[| well_ord(X,r);  well_ord(Y,s) |] ==> |X| = |Y| \<longleftrightarrow> X \<approx> Y"
@@ -403,17 +405,26 @@
(*Infinite unions of cardinals?  See Devlin, Lemma 6.7, page 98*)

lemma Card_cardinal: "Card(|A|)"
-apply (unfold cardinal_def)
-apply (case_tac "\<exists>i. Ord (i) & i \<approx> A")
- txt{*degenerate case*}
- prefer 2 apply (erule Least_0 [THEN ssubst], rule Card_0)
-txt{*real case: A is isomorphic to some ordinal*}
-apply (rule Ord_Least [THEN CardI], safe)
-apply (rule less_LeastE)
-prefer 2 apply assumption
-apply (erule eqpoll_trans)
-apply (best intro: LeastI )
-done
+proof (unfold cardinal_def)
+  show "Card(\<mu> i. i \<approx> A)"
+    proof (cases "\<exists>i. Ord (i) & i \<approx> A")
+      case False thus ?thesis           --{*degenerate case*}
+        by (simp add: Least_0 Card_0)
+    next
+      case True                         --{*real case: @{term A} is isomorphic to some ordinal*}
+      then obtain i where i: "Ord(i)" "i \<approx> A" by blast
+      show ?thesis
+        proof (rule CardI [OF Ord_Least], rule notI)
+          fix j
+          assume j: "j < (\<mu> i. i \<approx> A)"
+          assume "j \<approx> (\<mu> i. i \<approx> A)"
+          also have "... \<approx> A" using i by (auto intro: LeastI)
+          finally have "j \<approx> A" .
+          thus False
+            by (rule less_LeastE [OF _ j])
+        qed
+    qed
+qed

(*Kunen's Lemma 10.5*)
lemma cardinal_eq_lemma: ```