author lcp Fri, 23 Dec 1994 16:33:37 +0100 changeset 833 ba386650df2c parent 832 ad50a9e74eaf child 834 ad1d0eb0ee82
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, succ_eqpoll_succD, cons_lepoll_cons_iff, cons_eqpoll_cons_iff. Deleted inj_succ_succD. Streamlined proof of nat_lepoll_imp_le_lemma. Added Krzysztof's theorems diff_sing_lepoll, lepoll_diff_sing, diff_sing_eqpoll, lepoll_1_is_sing, inj_not_surj_succ, lesspoll_trans, lesspoll_lepoll_lesspoll, lepoll_lesspoll_lesspoll, lepoll_imp_lesspoll_succ, lesspoll_succ_imp_lepoll, lepoll_succ_disj, lepoll_nat_imp_Finite, lepoll_Finite, Finite_imp_cons_Finite, Finite_imp_succ_Finite, nat_le_infinite_Ord, nat_wf_on_converse_Memrel, nat_well_ord_converse_Memrel, well_ord_converse, ordertype_eq_n, Finite_well_ord_converse
 src/ZF/Cardinal.ML file | annotate | diff | comparison | revisions
```--- a/src/ZF/Cardinal.ML	Fri Dec 23 16:32:39 1994 +0100
+++ b/src/ZF/Cardinal.ML	Fri Dec 23 16:33:37 1994 +0100
@@ -105,6 +105,48 @@
qed "eqpoll_iff";

+goalw Cardinal.thy [lepoll_def, inj_def] "!!A. A lepoll 0 ==> A = 0";
+by (fast_tac (eq_cs addDs [apply_type]) 1);
+qed "lepoll_0_is_0";
+
+(*0 lepoll Y*)
+bind_thm ("empty_lepollI", empty_subsetI RS subset_imp_lepoll);
+
+(*A eqpoll 0 ==> A=0*)
+bind_thm ("eqpoll_0_is_0",  eqpoll_imp_lepoll RS lepoll_0_is_0);
+
+
+(*** lesspoll: contributions by Krzysztof Grabczewski ***)
+
+goalw Cardinal.thy [inj_def, surj_def]
+  "!!f. [| f : inj(A, succ(m)); f ~: surj(A, succ(m)) |] ==> EX f. f:inj(A,m)";
+by (safe_tac lemmas_cs);
+by (swap_res_tac [exI] 1);
+by (res_inst_tac [("a", "lam z:A. if(f`z=m, y, f`z)")] CollectI 1);
+by (fast_tac (ZF_cs addSIs [if_type RS lam_type]
+                    addEs [apply_funtype RS succE]) 1);
+(*Proving it's injective*)
+by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1);
+by (fast_tac ZF_cs 1);
+qed "inj_not_surj_succ";
+
+(** Variations on transitivity **)
+
+goalw Cardinal.thy [lesspoll_def]
+      "!!X. [| X lesspoll Y; Y lesspoll Z |] ==> X lesspoll Z";
+qed "lesspoll_trans";
+
+goalw Cardinal.thy [lesspoll_def]
+      "!!X. [| X lesspoll Y; Y lepoll Z |] ==> X lesspoll Z";
+qed "lesspoll_lepoll_lesspoll";
+
+goalw Cardinal.thy [lesspoll_def]
+      "!!X. [| X lesspoll Y; Z lepoll X |] ==> Z lesspoll Y";
+qed "lepoll_lesspoll_lesspoll";
+

(** LEAST -- the least number operator [from HOL/Univ.ML] **)

@@ -296,50 +338,43 @@
qed "Card_le_iff";

-(** The swap operator [NOT USED] **)
-
-goalw Cardinal.thy [swap_def]
-    "!!A. [| x:A;  y:A |] ==> swap(A,x,y) : A->A";
-by (REPEAT (ares_tac [lam_type,if_type] 1));
-qed "swap_type";
-
-goalw Cardinal.thy [swap_def]
-    "!!A. [| x:A;  y:A;  z:A |] ==> swap(A,x,y)`(swap(A,x,y)`z) = z";
-by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1);
-qed "swap_swap_identity";
-
-goal Cardinal.thy "!!A. [| x:A;  y:A |] ==> swap(A,x,y) : bij(A,A)";
-by (rtac nilpotent_imp_bijective 1);
-by (REPEAT (ares_tac [swap_type, comp_eq_id_iff RS iffD2,
-		      ballI, swap_swap_identity] 1));
-qed "swap_bij";
-
(*** The finite cardinals ***)

-(*Lemma suggested by Mike Fourman*)
-val [prem] = goalw Cardinal.thy [inj_def]
- "f: inj(succ(m), succ(n)) ==> (lam x:m. if(f`x=n, f`m, f`x)) : inj(m,n)";
+goalw Cardinal.thy [lepoll_def, inj_def]
+ "!!A B. [| cons(u,A) lepoll cons(v,B);  u~:A;  v~:B |] ==> A lepoll B";
+by (safe_tac ZF_cs);
+by (res_inst_tac [("x", "lam x:A. if(f`x=v, f`u, f`x)")] exI 1);
by (rtac CollectI 1);
-(*Proving it's in the function space m->n*)
-by (cut_facts_tac [prem] 1);
+(*Proving it's in the function space A->B*)
by (rtac (if_type RS lam_type) 1);
+by (fast_tac (ZF_cs addEs [apply_funtype RS consE]) 1);
(*Proving it's injective*)
by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1);
-(*Adding  prem  earlier would cause the simplifier to loop*)
-by (cut_facts_tac [prem] 1);
-by (fast_tac (ZF_cs addSEs [mem_irrefl]) 1);
-qed "inj_succ_succD";
+by (fast_tac ZF_cs 1);
+qed "cons_lepoll_consD";

-val [prem] = goalw Cardinal.thy [lepoll_def]
+goal Cardinal.thy
+ "!!A B. [| cons(u,A) eqpoll cons(v,B);  u~:A;  v~:B |] ==> A eqpoll B";
+by (asm_full_simp_tac (ZF_ss addsimps [eqpoll_iff]) 1);
+by (fast_tac (ZF_cs addIs [cons_lepoll_consD]) 1);
+qed "cons_eqpoll_consD";
+
+(*Lemma suggested by Mike Fourman*)
+goalw Cardinal.thy [succ_def] "!!m n. succ(m) lepoll succ(n) ==> m lepoll n";
+by (etac cons_lepoll_consD 1);
+by (REPEAT (rtac mem_not_refl 1));
+qed "succ_lepoll_succD";
+
+val [prem] = goal Cardinal.thy
"m:nat ==> ALL n: nat. m lepoll n --> m le n";
by (nat_ind_tac "m" [prem] 1);
by (fast_tac (ZF_cs addSIs [nat_0_le]) 1);
by (rtac ballI 1);
by (eres_inst_tac [("n","n")] natE 1);
-by (asm_simp_tac (ZF_ss addsimps [inj_def, succI1 RS Pi_empty2]) 1);
+by (asm_simp_tac (ZF_ss addsimps [lepoll_def, inj_def,
+				  succI1 RS Pi_empty2]) 1);
val nat_lepoll_imp_le_lemma = result();

bind_thm ("nat_lepoll_imp_le", nat_lepoll_imp_le_lemma RS bspec RS mp);
@@ -367,6 +402,33 @@
qed "succ_lepoll_natE";

+(** lepoll, lesspoll and natural numbers **)
+
+goalw Cardinal.thy [lesspoll_def]
+      "!!m. [| A lepoll m; m:nat |] ==> A lesspoll succ(m)";
+by (rtac conjI 1);
+by (fast_tac (ZF_cs addIs [subset_imp_lepoll RSN (2,lepoll_trans)]) 1);
+by (rtac notI 1);
+by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll] 1);
+by (dtac lepoll_trans 1 THEN assume_tac 1);
+by (etac succ_lepoll_natE 1 THEN assume_tac 1);
+qed "lepoll_imp_lesspoll_succ";
+
+goalw Cardinal.thy [lesspoll_def, lepoll_def, eqpoll_def, bij_def]
+      "!!m. [| A lesspoll succ(m); m:nat |] ==> A lepoll m";
+by (step_tac ZF_cs 1);
+by (fast_tac (ZF_cs addSIs [inj_not_surj_succ]) 1);
+qed "lesspoll_succ_imp_lepoll";
+
+goal Cardinal.thy "!!A m. [| A lepoll succ(m);  m:nat |] ==>  \
+\                         A lepoll m | A eqpoll succ(m)";
+by (rtac disjCI 1);
+by (rtac lesspoll_succ_imp_lepoll 1);
+by (assume_tac 2);
+by (asm_simp_tac (ZF_ss addsimps [lesspoll_def]) 1);
+qed "lepoll_succ_disj";
+
+
(*** The first infinite cardinal: Omega, or nat ***)

(*This implies Kunen's Lemma 10.6*)
@@ -428,6 +490,22 @@
by (asm_full_simp_tac (ZF_ss addsimps [eqpoll_iff, cons_lepoll_cong]) 1);
qed "cons_eqpoll_cong";

+goal Cardinal.thy
+    "!!A B. [| a ~: A;  b ~: B |] ==> \
+\           cons(a,A) lepoll cons(b,B)  <->  A lepoll B";
+by (fast_tac (ZF_cs addIs [cons_lepoll_cong, cons_lepoll_consD]) 1);
+qed "cons_lepoll_cons_iff";
+
+goal Cardinal.thy
+    "!!A B. [| a ~: A;  b ~: B |] ==> \
+\           cons(a,A) eqpoll cons(b,B)  <->  A eqpoll B";
+by (fast_tac (ZF_cs addIs [cons_eqpoll_cong, cons_eqpoll_consD]) 1);
+qed "cons_eqpoll_cons_iff";
+
+goalw Cardinal.thy [succ_def] "{a} eqpoll 1";
+by (fast_tac (ZF_cs addSIs [eqpoll_refl RS cons_eqpoll_cong]) 1);
+qed "singleton_eqpoll_1";
+
(*Congruence law for  succ  under equipollence*)
goalw Cardinal.thy [succ_def]
"!!A B. A eqpoll B ==> succ(A) eqpoll succ(B)";
@@ -475,3 +553,127 @@
setloop split_tac [expand_if]) 1);
by (fast_tac (ZF_cs addEs [equals0D]) 1);
qed "inj_disjoint_eqpoll";
+
+
+(*** Lemmas by Krzysztof Grabczewski.  New proofs using cons_lepoll_cons.
+     Could easily generalise from succ to cons. ***)
+
+goalw Cardinal.thy [succ_def]
+      "!!A a n. [| a:A;  A lepoll succ(n) |] ==> A - {a} lepoll n";
+by (rtac cons_lepoll_consD 1);
+by (rtac mem_not_refl 3);
+by (eresolve_tac [cons_Diff RS ssubst] 1);
+by (safe_tac ZF_cs);
+qed "diff_sing_lepoll";
+
+goalw Cardinal.thy [succ_def]
+      "!!A a n. [| a:A; succ(n) lepoll A |] ==> n lepoll A - {a}";
+by (rtac cons_lepoll_consD 1);
+by (rtac mem_not_refl 2);
+by (eresolve_tac [cons_Diff RS ssubst] 1);
+by (safe_tac ZF_cs);
+qed "lepoll_diff_sing";
+
+goal Cardinal.thy "!!A a n. [| a:A; A eqpoll succ(n) |] ==> A - {a} eqpoll n";
+qed "diff_sing_eqpoll";
+
+goal Cardinal.thy "!!A. [| A lepoll 1; a:A |] ==> A = {a}";
+by (forward_tac [diff_sing_lepoll] 1);
+by (assume_tac 1);
+by (dtac lepoll_0_is_0 1);
+by (fast_tac (eq_cs addEs [equalityE]) 1);
+qed "lepoll_1_is_sing";
+
+
+(*** Finite and infinite sets ***)
+
+goalw Cardinal.thy [Finite_def]
+    "!!A. [| A lepoll n;  n:nat |] ==> Finite(A)";
+by (etac rev_mp 1);
+by (etac nat_induct 1);
+qed "lepoll_nat_imp_Finite";
+
+goalw Cardinal.thy [Finite_def]
+     "!!X. [| Y lepoll X;  Finite(X) |] ==> Finite(Y)";
+		     rewrite_rule [Finite_def] lepoll_nat_imp_Finite]) 1);
+qed "lepoll_Finite";
+
+goalw Cardinal.thy [Finite_def] "!!x. Finite(x) ==> Finite(cons(y,x))";
+by (excluded_middle_tac "y:x" 1);
+by (asm_simp_tac (ZF_ss addsimps [cons_absorb]) 2);
+by (etac bexE 1);
+by (rtac bexI 1);
+by (etac nat_succI 2);
+by (asm_simp_tac
+    (ZF_ss addsimps [succ_def, cons_eqpoll_cong, mem_not_refl]) 1);
+qed "Finite_imp_cons_Finite";
+
+goalw Cardinal.thy [succ_def] "!!x. Finite(x) ==> Finite(succ(x))";
+by (etac Finite_imp_cons_Finite 1);
+qed "Finite_imp_succ_Finite";
+
+goalw Cardinal.thy [Finite_def]
+      "!!i. [| Ord(i);  ~ Finite(i) |] ==> nat le i";
+by (eresolve_tac [Ord_nat RSN (2,Ord_linear2)] 1);
+by (assume_tac 2);
+qed "nat_le_infinite_Ord";
+
+
+(*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
+  set is well-ordered.  Proofs simplified by lcp. *)
+
+goal Nat.thy "!!n. n:nat ==> wf[n](converse(Memrel(n)))";
+by (etac nat_induct 1);
+by (fast_tac (ZF_cs addIs [wf_onI]) 1);
+by (rtac wf_onI 1);
+by (asm_full_simp_tac
+    (ZF_ss addsimps [wf_on_def, wf_def, converse_iff, Memrel_iff]) 1);
+by (excluded_middle_tac "x:Z" 1);
+by (dres_inst_tac [("x", "x")] bspec 2 THEN assume_tac 2);
+by (dres_inst_tac [("x", "Z")] spec 1);
+by (safe_tac ZF_cs);
+by (dres_inst_tac [("x", "xa")] bspec 1 THEN assume_tac 1);
+by (fast_tac ZF_cs 1);
+qed "nat_wf_on_converse_Memrel";
+
+goal Cardinal.thy "!!n. n:nat ==> well_ord(n,converse(Memrel(n)))";
+by (forward_tac [Ord_nat RS Ord_in_Ord RS well_ord_Memrel] 1);
+by (rewtac well_ord_def);
+by (fast_tac (ZF_cs addSIs [tot_ord_converse, nat_wf_on_converse_Memrel]) 1);
+qed "nat_well_ord_converse_Memrel";
+
+goal Cardinal.thy
+    "!!A. [| well_ord(A,r); 	\
+\            well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r)))) \
+\         |] ==> well_ord(A,converse(r))";
+by (resolve_tac [well_ord_Int_iff RS iffD1] 1);
+by (forward_tac [ordermap_bij RS bij_is_inj RS well_ord_rvimage] 1);
+by (assume_tac 1);
+by (asm_full_simp_tac
+    (ZF_ss addsimps [rvimage_converse, converse_Int, converse_prod,
+		     ordertype_ord_iso RS ord_iso_rvimage_eq]) 1);
+qed "well_ord_converse";
+
+goal Cardinal.thy
+    "!!A. [| well_ord(A,r);  A eqpoll n;  n:nat |] ==> ordertype(A,r)=n";
+by (rtac (Ord_ordertype RS Ord_nat_eqpoll_iff RS iffD1) 1 THEN
+    REPEAT (assume_tac 1));
+by (rtac eqpoll_trans 1 THEN assume_tac 2);
+by (rewtac eqpoll_def);
+by (fast_tac (ZF_cs addSIs [ordermap_bij RS bij_converse_bij]) 1);
+qed "ordertype_eq_n";
+
+goalw Cardinal.thy [Finite_def]
+    "!!A. [| Finite(A);  well_ord(A,r) |] ==> well_ord(A,converse(r))";
+by (rtac well_ord_converse 1 THEN assume_tac 1);