src/ZF/AC/AC16_lemmas.ML

--- a/src/ZF/AC/AC16_lemmas.ML	Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/AC16_lemmas.ML	Mon Sep 29 11:48:48 1997 +0200
@@ -9,7 +9,7 @@
 
 goal thy "!!a. a~:A ==> cons(a,A)-{a}=A";
 by (Fast_tac 1);
-val cons_Diff_eq = result();
+qed "cons_Diff_eq";
 
 goalw thy [lepoll_def] "1 lepoll X <-> (EX x. x:X)";
 by (rtac iffI 1);
@@ -17,7 +17,7 @@
 by (etac exE 1);
 by (res_inst_tac [("x","lam a:1. x")] exI 1);
 by (fast_tac (!claset addSIs [lam_injective]) 1);
-val nat_1_lepoll_iff = result();
+qed "nat_1_lepoll_iff";
 
 goal thy "X eqpoll 1 <-> (EX x. X={x})";
 by (rtac iffI 1);
@@ -25,12 +25,12 @@
 by (dresolve_tac [nat_1_lepoll_iff RS iffD1] 1);
 by (fast_tac (!claset addSIs [lepoll_1_is_sing]) 1);
 by (fast_tac (!claset addSIs [singleton_eqpoll_1]) 1);
-val eqpoll_1_iff_singleton = result();
+qed "eqpoll_1_iff_singleton";
 
 goalw thy [succ_def] 
       "!!x. [| x eqpoll n; y~:x |] ==> cons(y,x) eqpoll succ(n)";
 by (fast_tac (!claset addSEs [cons_eqpoll_cong, mem_irrefl]) 1);
-val cons_eqpoll_succ = result();
+qed "cons_eqpoll_succ";
 
 goal thy "{Y:Pow(X). Y eqpoll 1} = {{x}. x:X}";
 by (rtac equalityI 1);
@@ -43,7 +43,7 @@
 by (rtac CollectI 1);
 by (Fast_tac 1);
 by (fast_tac (!claset addSIs [singleton_eqpoll_1]) 1);
-val subsets_eqpoll_1_eq = result();
+qed "subsets_eqpoll_1_eq";
 
 goalw thy [eqpoll_def, bij_def] "X eqpoll {{x}. x:X}";
 by (res_inst_tac [("x","lam x:X. {x}")] exI 1);
@@ -54,12 +54,12 @@
                 addIs [singleton_eq_iff RS iffD1]) 1);
 by (Asm_full_simp_tac 1);
 by (fast_tac (!claset addSIs [lam_type]) 1);
-val eqpoll_RepFun_sing = result();
+qed "eqpoll_RepFun_sing";
 
 goal thy "{Y:Pow(X). Y eqpoll 1} eqpoll X";
 by (resolve_tac [subsets_eqpoll_1_eq RS ssubst] 1);
 by (resolve_tac [eqpoll_RepFun_sing RS eqpoll_sym] 1);
-val subsets_eqpoll_1_eqpoll = result();
+qed "subsets_eqpoll_1_eqpoll";
 
 goal thy "!!x. [| InfCard(x); y:Pow(x); y eqpoll succ(z) |]  \
 \               ==> (LEAST i. i:y) : y";
@@ -68,7 +68,7 @@
 by (fast_tac (!claset addIs [LeastI]
         addSDs [InfCard_is_Card RS Card_is_Ord, PowD RS subsetD]
         addEs [Ord_in_Ord]) 1);
-val InfCard_Least_in = result();
+qed "InfCard_Least_in";
 
 goalw thy [lepoll_def] "!!i. [| InfCard(x); n:nat |] ==>  \
 \       {y:Pow(x). y eqpoll succ(succ(n))} lepoll  \
@@ -89,7 +89,7 @@
 by (resolve_tac [PowD RS subsetD] 1 THEN (assume_tac 1));
 by (REPEAT (fast_tac (!claset addSIs [Diff_sing_eqpoll]
                 addIs [InfCard_Least_in]) 1));
-val subsets_lepoll_lemma1 = result();
+qed "subsets_lepoll_lemma1";
 
 val prems = goal thy "(!!y. y:z ==> Ord(y)) ==> z <= succ(Union(z))";
 by (rtac subsetI 1);
@@ -102,28 +102,28 @@
 by (fast_tac (!claset addDs prems) 1);
 by (fast_tac (!claset addDs prems) 1);
 by (fast_tac (!claset addSEs [leE,ltE]) 1);
-val set_of_Ord_succ_Union = result();
+qed "set_of_Ord_succ_Union";
 
 goal thy "!!i. j<=i ==> i ~: j";
 by (fast_tac (!claset addSEs [mem_irrefl]) 1);
-val subset_not_mem = result();
+qed "subset_not_mem";
 
 val prems = goal thy "(!!y. y:z ==> Ord(y)) ==> succ(Union(z)) ~: z";
 by (resolve_tac [set_of_Ord_succ_Union RS subset_not_mem] 1);
 by (eresolve_tac prems 1);
-val succ_Union_not_mem = result();
+qed "succ_Union_not_mem";
 
 goal thy "Union(cons(succ(Union(z)),z)) = succ(Union(z))";
 by (Fast_tac 1);
-val Union_cons_eq_succ_Union = result();
+qed "Union_cons_eq_succ_Union";
 
 goal thy "!!i. [| Ord(i); Ord(j) |] ==> i Un j = i | i Un j = j";
 by (fast_tac (!claset addSDs [le_imp_subset] addEs [Ord_linear_le]) 1);
-val Un_Ord_disj = result();
+qed "Un_Ord_disj";
 
 goal thy "!!X. x:X ==> Union(X) = x Un Union(X-{x})";
 by (Fast_tac 1);
-val Union_eq_Un = result();
+qed "Union_eq_Un";
 
 goal thy "!!n. n:nat ==>  \
 \       ALL z. (ALL y:z. Ord(y)) & z eqpoll n & z~=0 --> Union(z) : z";
@@ -147,13 +147,13 @@
 by (etac disjE 1);
 by (etac subst_elem 1 THEN (assume_tac 1));
 by (rtac subst_elem 1 THEN (TRYALL assume_tac));
-val Union_in_lemma = result();
+qed "Union_in_lemma";
 
 goal thy "!!z. [| ALL x:z. Ord(x); z eqpoll n; z~=0; n:nat |]  \
 \               ==> Union(z) : z";
 by (dtac Union_in_lemma 1);
 by (fast_tac FOL_cs 1);
-val Union_in = result();
+qed "Union_in";
 
 goal thy "!!x. [| InfCard(x); z:Pow(x); z eqpoll n; n:nat |]  \
 \               ==> succ(Union(z)) : x";
@@ -168,7 +168,7 @@
 by (fast_tac (!claset addSIs [Union_in]
                       addSEs [PowD RS subsetD RSN 
 		 (2, InfCard_is_Card RS Card_is_Ord RS Ord_in_Ord)]) 1);
-val succ_Union_in_x = result();
+qed "succ_Union_in_x";
 
 goalw thy [lepoll_def] "!!X. [| InfCard(x); n:nat |] ==>  \
 \       {y:Pow(x). y eqpoll succ(n)} lepoll  \
@@ -186,7 +186,7 @@
                     addSDs [InfCard_is_Card RS Card_is_Ord] 
                     addEs  [Ord_in_Ord]) 2);
 by (fast_tac (!claset addSIs [succ_Union_in_x, nat_succI]) 1);
-val succ_lepoll_succ_succ = result();
+qed "succ_lepoll_succ_succ";
 
 goal thy "!!X. [| InfCard(X); n:nat |]  \
 \       ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X";
@@ -203,18 +203,18 @@
 by (eresolve_tac [eqpoll_refl RS prod_eqpoll_cong RS eqpoll_imp_lepoll] 1);
 by (fast_tac (!claset addEs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_trans]
         addSIs [succ_lepoll_succ_succ]) 1);
-val subsets_eqpoll_X = result();
+qed "subsets_eqpoll_X";
 
 goalw thy [surj_def] "!!f. [| f:surj(A,B); y<=B |]  \
 \       ==> f``(converse(f)``y) = y";
 by (fast_tac (!claset addDs [apply_equality2]
 	              addEs [apply_iff RS iffD2]) 1);
-val image_vimage_eq = result();
+qed "image_vimage_eq";
 
 goal thy "!!f. [| f:inj(A,B); y<=A |] ==> converse(f)``(f``y) = y";
 by (fast_tac (!claset addSEs [inj_is_fun RS apply_Pair]
                 addDs [inj_equality]) 1);
-val vimage_image_eq = result();
+qed "vimage_image_eq";
 
 goalw thy [eqpoll_def] "!!A B. A eqpoll B  \
 \       ==> {Y:Pow(A). Y eqpoll n} eqpoll {Y:Pow(B). Y eqpoll n}";
@@ -230,22 +230,22 @@
                         RS image_subset RS PowI]) 1);
 by (fast_tac (!claset addSEs [bij_is_inj RS vimage_image_eq]) 1);
 by (fast_tac (!claset addSEs [bij_is_surj RS image_vimage_eq]) 1);
-val subsets_eqpoll = result();
+qed "subsets_eqpoll";
 
 goalw thy [WO2_def] "!!X. WO2 ==> EX a. Card(a) & X eqpoll a";
 by (REPEAT (eresolve_tac [allE,exE,conjE] 1));
 by (fast_tac (!claset addSEs [well_ord_Memrel RS well_ord_cardinal_eqpoll RS
                 (eqpoll_sym RSN (2, eqpoll_trans)) RS eqpoll_sym]
                 addSIs [Card_cardinal]) 1);
-val WO2_imp_ex_Card = result();
+qed "WO2_imp_ex_Card";
 
 goal thy "!!X. [| X lepoll Y; ~Finite(X) |] ==> ~Finite(Y)";
 by (fast_tac (empty_cs addEs [notE, lepoll_Finite] addSIs [notI]) 1); 
-val lepoll_infinite = result();
+qed "lepoll_infinite";
 
 goalw thy [InfCard_def] "!!X. [| ~Finite(X); Card(X) |] ==> InfCard(X)";
 by (fast_tac (!claset addSEs [Card_is_Ord RS nat_le_infinite_Ord]) 1);
-val infinite_Card_is_InfCard = result();
+qed "infinite_Card_is_InfCard";
 
 goal thy "!!X n. [| WO2; n:nat; ~Finite(X) |]  \
 \       ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X";
@@ -257,12 +257,12 @@
 by (etac subsets_eqpoll 1);
 by (etac subsets_eqpoll_X 1 THEN (assume_tac 1));
 by (etac eqpoll_sym 1);
-val WO2_infinite_subsets_eqpoll_X = result();
+qed "WO2_infinite_subsets_eqpoll_X";
 
 goal thy "!!X. well_ord(X,R) ==> EX a. Card(a) & X eqpoll a";
 by (fast_tac (!claset addSEs [well_ord_cardinal_eqpoll RS eqpoll_sym]
                 addSIs [Card_cardinal]) 1);
-val well_ord_imp_ex_Card = result();
+qed "well_ord_imp_ex_Card";
 
 goal thy "!!X n. [| well_ord(X,R); n:nat; ~Finite(X) |]  \
 \               ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X";
@@ -274,5 +274,5 @@
 by (etac subsets_eqpoll 1);
 by (etac subsets_eqpoll_X 1 THEN (assume_tac 1));
 by (etac eqpoll_sym 1);
-val well_ord_infinite_subsets_eqpoll_X = result();
+qed "well_ord_infinite_subsets_eqpoll_X";