--- a/src/ZF/AC/AC0_AC1.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/AC0_AC1.ML Mon Sep 29 11:48:48 1997 +0200
@@ -8,7 +8,7 @@
goal thy "!!A. 0~:A ==> A <= Pow(Union(A))-{0}";
by (Fast_tac 1);
-val subset_Pow_Union = result();
+qed "subset_Pow_Union";
goal thy "!!f. [| f:(PROD X:A. X); D<=A |] ==> EX g. g:(PROD X:D. X)";
by (fast_tac (!claset addSIs [restrict_type, apply_type]) 1);
--- a/src/ZF/AC/AC10_AC15.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/AC10_AC15.ML Mon Sep 29 11:48:48 1997 +0200
@@ -31,7 +31,7 @@
by (etac not_emptyE 1);
by (res_inst_tac [("x","lam z:B. <x,z>")] exI 1);
by (fast_tac (!claset addSIs [snd_conv, lam_injective]) 1);
-val lepoll_Sigma = result();
+qed "lepoll_Sigma";
goal thy "!!A. 0~:A ==> ALL B:{cons(0,x*nat). x:A}. ~Finite(B)";
by (rtac ballI 1);
@@ -42,7 +42,7 @@
by (resolve_tac [lepoll_Sigma RS lepoll_Finite RS (nat_not_Finite RS notE)] 1
THEN (assume_tac 2));
by (Fast_tac 1);
-val cons_times_nat_not_Finite = result();
+qed "cons_times_nat_not_Finite";
goal thy "!!A. [| Union(C)=A; a:A |] ==> EX B:C. a:B & B <= A";
by (Fast_tac 1);
@@ -113,7 +113,7 @@
by (fast_tac (empty_cs addSDs [lemma3, theI] addDs [bspec]
addSEs [exE, conjE]
addIs [exI, ballI, lemma5]) 1);
-val ex_fun_AC13_AC15 = result();
+qed "ex_fun_AC13_AC15";
(* ********************************************************************** *)
(* The target proofs *)
@@ -232,7 +232,7 @@
goal thy "!!A. [| A~=0; A lepoll 1 |] ==> EX a. A={a}";
by (fast_tac (!claset addSEs [not_emptyE, lepoll_1_is_sing]) 1);
-val lemma_aux = result();
+qed "lemma_aux";
goal thy "!!f. ALL B:A. f(B)~=0 & f(B)<=B & f(B) lepoll 1 \
\ ==> (lam x:A. THE y. f(x)={y}) : (PROD X:A. X)";
--- a/src/ZF/AC/AC15_WO6.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/AC15_WO6.ML Mon Sep 29 11:48:48 1997 +0200
@@ -9,7 +9,7 @@
goal thy "!!x. Ord(x) ==> (UN a<x. F(a)) = (UN a:x. F(a))";
by (fast_tac (!claset addSIs [ltI] addSDs [ltD]) 1);
-val OUN_eq_UN = result();
+qed "OUN_eq_UN";
val [prem] = goal thy "ALL x:Pow(A)-{0}. f`x~=0 & f`x<=x & f`x lepoll m ==> \
\ (UN i<LEAST x. HH(f,A,x)={A}. HH(f,A,i)) = A";
--- a/src/ZF/AC/AC16_WO4.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/AC16_WO4.ML Mon Sep 29 11:48:48 1997 +0200
@@ -32,22 +32,22 @@
(* ********************************************************************** *)
(* well_ord(x,r) ==> well_ord({{y,z}. y:x}, Something(x,z)) **)
-val well_ord_paired = standard (paired_bij RS bij_is_inj RS well_ord_rvimage);
+bind_thm ("well_ord_paired", (paired_bij RS bij_is_inj RS well_ord_rvimage));
goal thy "!!A. [| A lepoll B; ~ A lepoll C |] ==> ~ B lepoll C";
by (fast_tac (!claset addEs [notE, lepoll_trans]) 1);
-val lepoll_trans1 = result();
+qed "lepoll_trans1";
goalw thy [lepoll_def]
"!!X.[| Y lepoll X; well_ord(X, R) |] ==> EX S. well_ord(Y, S)";
by (fast_tac (!claset addSEs [well_ord_rvimage]) 1);
-val well_ord_lepoll = result();
+qed "well_ord_lepoll";
goal thy "!!X. [| well_ord(X,R); well_ord(Y,S) \
\ |] ==> EX T. well_ord(X Un Y, T)";
by (eresolve_tac [well_ord_radd RS (Un_lepoll_sum RS well_ord_lepoll)] 1);
by (assume_tac 1);
-val well_ord_Un = result();
+qed "well_ord_Un";
(* ********************************************************************** *)
(* There exists a well ordered set y such that ... *)
@@ -70,7 +70,7 @@
val [prem] = goal thy "~Finite(B) ==> ~Finite(A Un B)";
by (fast_tac (!claset
addSIs [subset_imp_lepoll RS (prem RSN (2, lepoll_infinite))]) 1);
-val infinite_Un = result();
+qed "infinite_Un";
(* ********************************************************************** *)
(* There is a v : s_u such that k lepoll x Int y (in our case succ(k)) *)
@@ -92,12 +92,12 @@
(asm_simp_tac
(!simpset addsimps [inj_is_fun RS apply_type, left_inverse]
setloop (split_tac [expand_if] ORELSE' Step_tac))));
-val succ_not_lepoll_lemma = result();
+qed "succ_not_lepoll_lemma";
goalw thy [lepoll_def, eqpoll_def, bij_def, surj_def]
"!!A. [| ~A eqpoll B; A lepoll B |] ==> succ(A) lepoll B";
by (fast_tac (!claset addSEs [succ_not_lepoll_lemma, inj_is_fun]) 1);
-val succ_not_lepoll_imp_eqpoll = result();
+qed "succ_not_lepoll_imp_eqpoll";
val [prem] = goalw thy [s_u_def]
"(ALL v:s_u(u, t_n, k, y). k eqpoll v Int y ==> False) \
@@ -109,7 +109,7 @@
by (etac conjE 1);
by (etac swap 1);
by (fast_tac (!claset addSEs [succ_not_lepoll_imp_eqpoll]) 1);
-val suppose_not = result();
+qed "suppose_not";
(* ********************************************************************** *)
(* There is a k-2 element subset of y *)
@@ -120,7 +120,7 @@
by (fast_tac (FOL_cs addSDs [Ord_nat RSN (2, OrdmemD) RSN (2, restrict_inj)]
addSIs [subset_refl]
addSEs [restrict_bij, inj_is_fun RS fun_is_rel RS image_subset]) 1);
-val nat_lepoll_imp_ex_eqpoll_n = result();
+qed "nat_lepoll_imp_ex_eqpoll_n";
val ordertype_eqpoll =
ordermap_bij RS (exI RS (eqpoll_def RS def_imp_iff RS iffD2));
@@ -133,14 +133,14 @@
by (fast_tac (!claset addSIs [nat_le_infinite_Ord RS le_imp_lepoll]
addSEs [Ord_ordertype, ordertype_eqpoll RS eqpoll_imp_lepoll
RS lepoll_infinite]) 1);
-val ex_subset_eqpoll_n = result();
+qed "ex_subset_eqpoll_n";
goalw thy [lesspoll_def] "!!n. n: nat ==> n lesspoll nat";
by (fast_tac (!claset addSEs [Ord_nat RSN (2, ltI) RS leI RS le_imp_lepoll,
eqpoll_sym RS eqpoll_imp_lepoll]
addIs [Ord_nat RSN (2, nat_succI RS ltI) RS leI
RS le_imp_lepoll RS lepoll_trans RS succ_lepoll_natE]) 1);
-val n_lesspoll_nat = result();
+qed "n_lesspoll_nat";
goal thy "!!y. [| well_ord(y,R); ~Finite(y); k eqpoll a; a <= y; k: nat |] \
\ ==> y - a eqpoll y";
@@ -154,31 +154,31 @@
n_lesspoll_nat RS lesspoll_lepoll_lesspoll,
well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll
RS lepoll_infinite]) 1);
-val Diff_Finite_eqpoll = result();
+qed "Diff_Finite_eqpoll";
goal thy "!!x. [| a<=y; b:y-a; u:x |] ==> cons(b, cons(u, a)) : Pow(x Un y)";
by (Fast_tac 1);
-val cons_cons_subset = result();
+qed "cons_cons_subset";
goal thy "!!x. [| a eqpoll k; a<=y; b:y-a; u:x; x Int y = 0 \
\ |] ==> cons(b, cons(u, a)) eqpoll succ(succ(k))";
by (fast_tac (!claset addSIs [cons_eqpoll_succ] addEs [equals0D]) 1);
-val cons_cons_eqpoll = result();
+qed "cons_cons_eqpoll";
goalw thy [s_u_def] "s_u(u, t_n, k, y) <= t_n";
by (Fast_tac 1);
-val s_u_subset = result();
+qed "s_u_subset";
goalw thy [s_u_def, succ_def]
"!!w. [| w:t_n; cons(b,cons(u,a)) <= w; a <= y; b : y-a; k eqpoll a \
\ |] ==> w: s_u(u, t_n, succ(k), y)";
by (fast_tac (!claset addDs [eqpoll_imp_lepoll RS cons_lepoll_cong]
addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1);
-val s_uI = result();
+qed "s_uI";
goalw thy [s_u_def] "!!v. v : s_u(u, t_n, k, y) ==> u : v";
by (Fast_tac 1);
-val in_s_u_imp_u_in = result();
+qed "in_s_u_imp_u_in";
goal thy
"!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \
@@ -199,7 +199,7 @@
by (etac impE 1);
by (assume_tac 2);
by (fast_tac (!claset addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1);
-val ex1_superset_a = result();
+qed "ex1_superset_a";
goal thy
"!!A. [| succ(k) eqpoll A; k eqpoll B; B <= A; a : A-B; k:nat \
@@ -216,7 +216,7 @@
by (fast_tac (!claset addSIs [nat_succI]
addSEs [[eqpoll_sym RS eqpoll_imp_lepoll, subset_imp_lepoll] MRS
(lepoll_trans RS lepoll_trans) RS succ_lepoll_natE]) 1);
-val set_eq_cons = result();
+qed "set_eq_cons";
goal thy
"!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \
@@ -228,19 +228,19 @@
by (dresolve_tac [ex1_superset_a RS theI] 1 THEN REPEAT (assume_tac 1));
by (rtac set_eq_cons 1);
by (REPEAT (Fast_tac 1));
-val the_eq_cons = result();
+qed "the_eq_cons";
goal thy "!!a. [| cons(x,a) = cons(y,a); x~: a |] ==> x = y ";
by (fast_tac (!claset addSEs [equalityE]) 1);
-val cons_eqE = result();
+qed "cons_eqE";
goal thy "!!A. A = B ==> A Int C = B Int C";
by (Asm_simp_tac 1);
-val eq_imp_Int_eq = result();
+qed "eq_imp_Int_eq";
goal thy "!!a. [| a=b; a=c; b=d |] ==> c=d";
by (Asm_full_simp_tac 1);
-val msubst = result();
+qed "msubst";
(* ********************************************************************** *)
(* 1. y is less than or equipollent to {v:s_u. a <= v} *)
@@ -275,7 +275,7 @@
by (dres_inst_tac [("A","THE c. ?P(c)"), ("C","y")] eq_imp_Int_eq 1);
by (eresolve_tac [[asm_rl, the_eq_cons, the_eq_cons] MRS msubst] 1
THEN REPEAT (assume_tac 1));
-val y_lepoll_subset_s_u = result();
+qed "y_lepoll_subset_s_u";
(* ********************************************************************** *)
(* some arithmetic *)
@@ -298,7 +298,7 @@
by (fast_tac (!claset addSIs [Diff_sing_eqpoll, lepoll_Diff_sing]) 1);
by (res_inst_tac [("P","%z. z lepoll m")] subst 1 THEN (assume_tac 2));
by (Fast_tac 1);
-val eqpoll_sum_imp_Diff_lepoll_lemma = result();
+qed "eqpoll_sum_imp_Diff_lepoll_lemma";
goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) lepoll B; \
\ k:nat; m:nat |] \
@@ -307,7 +307,7 @@
by (dresolve_tac [nat_succI RS eqpoll_sum_imp_Diff_lepoll_lemma] 1
THEN (REPEAT (assume_tac 1)));
by (Fast_tac 1);
-val eqpoll_sum_imp_Diff_lepoll = result();
+qed "eqpoll_sum_imp_Diff_lepoll";
(* ********************************************************************** *)
(* similar properties for eqpoll *)
@@ -330,7 +330,7 @@
addss (!simpset addsimps [add_succ])) 1);
by (res_inst_tac [("P","%z. z eqpoll m")] subst 1 THEN (assume_tac 2));
by (Fast_tac 1);
-val eqpoll_sum_imp_Diff_eqpoll_lemma = result();
+qed "eqpoll_sum_imp_Diff_eqpoll_lemma";
goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) eqpoll B; \
\ k:nat; m:nat |] \
@@ -339,7 +339,7 @@
by (dresolve_tac [nat_succI RS eqpoll_sum_imp_Diff_eqpoll_lemma] 1
THEN (REPEAT (assume_tac 1)));
by (Fast_tac 1);
-val eqpoll_sum_imp_Diff_eqpoll = result();
+qed "eqpoll_sum_imp_Diff_eqpoll";
(* ********************************************************************** *)
(* back to the second part *)
@@ -348,7 +348,7 @@
goal thy "!!w. [| x Int y = 0; w <= x Un y |] \
\ ==> w Int (x - {u}) = w - cons(u, w Int y)";
by (fast_tac (!claset addEs [equals0D]) 1);
-val w_Int_eq_w_Diff = result();
+qed "w_Int_eq_w_Diff";
goal thy "!!w. [| w:{v:s_u(u, t_n, succ(l), y). a <= v}; \
\ l eqpoll a; t_n <= {v:Pow(x Un y). v eqpoll succ(succ(l) #+ m)}; \
@@ -362,18 +362,18 @@
addDs [s_u_subset RS subsetD]
addSEs [eqpoll_sym RS cons_eqpoll_succ RS eqpoll_sym, in_s_u_imp_u_in]
addSIs [nat_succI, eqpoll_sum_imp_Diff_eqpoll]) 1);
-val w_Int_eqpoll_m = result();
+qed "w_Int_eqpoll_m";
goal thy "!!m. [| 0<m; x eqpoll m; m:nat |] ==> x ~= 0";
by (fast_tac (empty_cs
addSEs [mem_irrefl, ltE, eqpoll_succ_imp_not_empty, natE]) 1);
-val eqpoll_m_not_empty = result();
+qed "eqpoll_m_not_empty";
goal thy
"!!z. [| z : xa Int (x - {u}); l eqpoll a; a <= y; x Int y = 0; u:x \
\ |] ==> cons(z, cons(u, a)) : {v: Pow(x Un y). v eqpoll succ(succ(l))}";
by (fast_tac (!claset addSIs [cons_eqpoll_succ] addEs [equals0D, eqpoll_sym]) 1);
-val cons_cons_in = result();
+qed "cons_cons_in";
(* ********************************************************************** *)
(* 2. {v:s_u. a <= v} is less than or equipollent *)
@@ -408,13 +408,13 @@
by (etac ex1_two_eq 1);
by (fast_tac (!claset addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1);
by (fast_tac (!claset addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1);
-val subset_s_u_lepoll_w = result();
+qed "subset_s_u_lepoll_w";
goal thy "!!k. [| 0<k; k:nat |] ==> EX l:nat. k = succ(l)";
by (etac natE 1);
by (fast_tac (empty_cs addSEs [ltE, mem_irrefl]) 1);
by (fast_tac (empty_cs addSIs [refl, bexI]) 1);
-val ex_eq_succ = result();
+qed "ex_eq_succ";
goal thy
"!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \
@@ -432,7 +432,7 @@
by (forward_tac [[y_lepoll_subset_s_u, subset_s_u_lepoll_w] MRS lepoll_trans] 1
THEN REPEAT (assume_tac 1));
by (contr_tac 1);
-val exists_proper_in_s_u = result();
+qed "exists_proper_in_s_u";
(* ********************************************************************** *)
(* LL can be well ordered *)
@@ -441,7 +441,7 @@
goal thy "{x:Pow(X). x lepoll 0} = {0}";
by (fast_tac (!claset addSDs [lepoll_0_is_0]
addSIs [lepoll_refl]) 1);
-val subsets_lepoll_0_eq_unit = result();
+qed "subsets_lepoll_0_eq_unit";
goal thy "!!X. [| well_ord(X, R); ~Finite(X); n:nat |] \
\ ==> EX S. well_ord({Y: Pow(X) . Y eqpoll succ(n)}, S)";
@@ -449,21 +449,21 @@
RS (eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1
THEN (REPEAT (assume_tac 1)));
by (fast_tac (!claset addSEs [bij_is_inj RS well_ord_rvimage]) 1);
-val well_ord_subsets_eqpoll_n = result();
+qed "well_ord_subsets_eqpoll_n";
goal thy "!!n. n:nat ==> {z:Pow(y). z lepoll succ(n)} = \
\ {z:Pow(y). z lepoll n} Un {z:Pow(y). z eqpoll succ(n)}";
by (fast_tac (!claset addIs [le_refl, leI, le_imp_lepoll]
addSDs [lepoll_succ_disj]
addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1);
-val subsets_lepoll_succ = result();
+qed "subsets_lepoll_succ";
goal thy "!!n. n:nat ==> \
\ {z:Pow(y). z lepoll n} Int {z:Pow(y). z eqpoll succ(n)} = 0";
by (fast_tac (!claset addSEs [eqpoll_sym RS eqpoll_imp_lepoll
RS lepoll_trans RS succ_lepoll_natE]
addSIs [equals0I]) 1);
-val Int_empty = result();
+qed "Int_empty";
(* ********************************************************************** *)
(* unit set is well-ordered by the empty relation *)
@@ -472,15 +472,15 @@
goalw thy [irrefl_def, trans_on_def, part_ord_def, linear_def, tot_ord_def]
"tot_ord({a},0)";
by (Simp_tac 1);
-val tot_ord_unit = result();
+qed "tot_ord_unit";
goalw thy [wf_on_def, wf_def] "wf[{a}](0)";
by (Fast_tac 1);
-val wf_on_unit = result();
+qed "wf_on_unit";
goalw thy [well_ord_def] "well_ord({a},0)";
by (simp_tac (!simpset addsimps [tot_ord_unit, wf_on_unit]) 1);
-val well_ord_unit = result();
+qed "well_ord_unit";
(* ********************************************************************** *)
(* well_ord_subsets_lepoll_n *)
@@ -499,7 +499,7 @@
by (eresolve_tac [Int_empty RS disj_Un_eqpoll_sum RS
(eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1);
by (fast_tac (!claset addSEs [bij_is_inj RS well_ord_rvimage]) 1);
-val well_ord_subsets_lepoll_n = result();
+qed "well_ord_subsets_lepoll_n";
goalw thy [LL_def, MM_def]
"!!x. t_n <= {v:Pow(x Un y). v eqpoll n} \
@@ -507,7 +507,7 @@
by (fast_tac (!claset addSEs [RepFunE]
addIs [subset_imp_lepoll RS (eqpoll_imp_lepoll
RSN (2, lepoll_trans))]) 1);
-val LL_subset = result();
+qed "LL_subset";
goal thy "!!x. [| t_n <= {v:Pow(x Un y). v eqpoll n}; \
\ well_ord(y, R); ~Finite(y); n:nat \
@@ -515,7 +515,7 @@
by (fast_tac (FOL_cs addIs [exI]
addSEs [LL_subset RSN (2, well_ord_subset)]
addEs [well_ord_subsets_lepoll_n RS exE]) 1);
-val well_ord_LL = result();
+qed "well_ord_LL";
(* ********************************************************************** *)
(* every element of LL is a contained in exactly one element of MM *)
@@ -526,7 +526,7 @@
\ t_n <= {v:Pow(x Un y). v eqpoll n}; \
\ v:LL(t_n, k, y) \
\ |] ==> EX! w. w:MM(t_n, k, y) & v<=w";
-by (step_tac (!claset addSEs [RepFunE]) 1);
+by (safe_tac (!claset addSEs [RepFunE]));
by (Fast_tac 1);
by (resolve_tac [lepoll_imp_eqpoll_subset RS exE] 1 THEN (assume_tac 1));
by (eres_inst_tac [("x","xa")] ballE 1);
@@ -536,7 +536,7 @@
by (dtac spec 1);
by (etac mp 1);
by (Fast_tac 1);
-val unique_superset_in_MM = result();
+qed "unique_superset_in_MM";
(* ********************************************************************** *)
(* The function GG satisfies the conditions of WO4 *)
@@ -557,15 +557,15 @@
THEN REPEAT (assume_tac 1));
by (rewrite_goals_tac [MM_def, s_u_def]);
by (Fast_tac 1);
-val exists_in_MM = result();
+qed "exists_in_MM";
goalw thy [LL_def] "!!w. w : MM(t_n, k, y) ==> w Int y : LL(t_n, k, y)";
by (Fast_tac 1);
-val Int_in_LL = result();
+qed "Int_in_LL";
goalw thy [MM_def] "MM(t_n, k, y) <= t_n";
by (Fast_tac 1);
-val MM_subset = result();
+qed "MM_subset";
goal thy
"!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \
@@ -583,7 +583,7 @@
by (eresolve_tac [unique_superset_in_MM RS the_equality2 RS ssubst] 1
THEN (assume_tac 1));
by (REPEAT (fast_tac (!claset addEs [equals0D] addSEs [Int_in_LL]) 1));
-val exists_in_LL = result();
+qed "exists_in_LL";
goalw thy [LL_def]
"!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \
@@ -592,7 +592,7 @@
\ ==> v = (THE x. x : MM(t_n, k, y) & v <= x) Int y";
by (fast_tac (!claset addSEs [Int_in_LL,
unique_superset_in_MM RS the_equality2 RS ssubst]) 1);
-val in_LL_eq_Int = result();
+qed "in_LL_eq_Int";
goal thy
"!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \
@@ -601,7 +601,7 @@
\ ==> (THE x. x : MM(t_n, k, y) & v <= x) <= x Un y";
by (fast_tac (!claset addSDs [unique_superset_in_MM RS theI RS conjunct1 RS
(MM_subset RS subsetD)]) 1);
-val the_in_MM_subset = result();
+qed "the_in_MM_subset";
goalw thy [GG_def]
"!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \
@@ -615,7 +615,7 @@
by (etac DiffE 1);
by (etac swap 1);
by (fast_tac (!claset addEs [ssubst]) 1);
-val GG_subset = result();
+qed "GG_subset";
goal thy
"!!x. [| well_ord(LL(t_n, succ(k), y), S); \
@@ -640,7 +640,7 @@
by (eresolve_tac [ordermap_type RS apply_type] 1);
by (eresolve_tac [ordermap_bij RS bij_is_inj RS left_inverse RS ssubst] 1
THEN REPEAT (assume_tac 1));
-val OUN_eq_x = result();
+qed "OUN_eq_x";
(* ********************************************************************** *)
(* Every element of the family is less than or equipollent to n-k (m) *)
@@ -650,12 +650,12 @@
"!!w. [| w : MM(t_n, k, y); t_n <= {v:Pow(x Un y). v eqpoll n} \
\ |] ==> w eqpoll n";
by (Fast_tac 1);
-val in_MM_eqpoll_n = result();
+qed "in_MM_eqpoll_n";
goalw thy [LL_def, MM_def]
"!!w. w : LL(t_n, k, y) ==> k lepoll w";
by (Fast_tac 1);
-val in_LL_eqpoll_n = result();
+qed "in_LL_eqpoll_n";
goalw thy [GG_def]
"!!x. [| \
@@ -678,7 +678,7 @@
addEs [unique_superset_in_MM RS theI RS conjunct1 RS in_MM_eqpoll_n,
in_LL_eq_Int RS equalityD1 RS (Int_lower1 RSN (2, subset_trans)),
ordermap_bij RS bij_converse_bij RS bij_is_fun RS apply_type]) 1));
-val all_in_lepoll_m = result();
+qed "all_in_lepoll_m";
(* ********************************************************************** *)
(* The main theorem AC16(n, k) ==> WO4(n-k) *)
--- 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";
--- a/src/ZF/AC/AC17_AC1.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/AC17_AC1.ML Mon Sep 29 11:48:48 1997 +0200
@@ -19,7 +19,7 @@
by (eresolve_tac [[bij_Least_HH_x RS bij_converse_bij RS bij_is_inj,
Ord_Least RS well_ord_Memrel] MRS well_ord_rvimage] 1);
by (assume_tac 1);
-val UN_eq_imp_well_ord = result();
+qed "UN_eq_imp_well_ord";
(* *********************************************************************** *)
(* theorems closer to the proof *)
@@ -35,7 +35,7 @@
by (etac swap 1);
by (rtac impI 1);
by (fast_tac (!claset addSIs [restrict_type]) 1);
-val not_AC1_imp_ex = result();
+qed "not_AC1_imp_ex";
goal thy "!!x. [| ALL f:Pow(x) - {0} -> x. EX u: Pow(x) - {0}. f`u~:u; \
\ EX f: Pow(x)-{0}->x. \
--- a/src/ZF/AC/AC18_AC19.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/AC18_AC19.ML Mon Sep 29 11:48:48 1997 +0200
@@ -18,7 +18,7 @@
by (rtac RepFunI 1 THEN (assume_tac 1));
by (dtac bspec 1 THEN (assume_tac 1));
by (etac subsetD 1 THEN (assume_tac 1));
-val PROD_subsets = result();
+qed "PROD_subsets";
goal thy "!!X. [| ALL A. 0 ~: A --> (EX f. f : (PROD X:A. X)); A ~= 0 |] ==> \
\ (INT a:A. UN b:B(a). X(a, b)) <= (UN f:PROD a:A. B(a). INT a:A. X(a, f`a))";
@@ -33,7 +33,7 @@
by (Simp_tac 1);
by (fast_tac (!claset addSEs [not_emptyE] addDs [RepFunI RSN (2, apply_type)]
addEs [CollectD2] addSIs [INT_I]) 1);
-val lemma_AC18 = result();
+qed "lemma_AC18";
val [prem] = goalw thy (AC18_def::AC_defs) "AC1 ==> AC18";
by (resolve_tac [prem RS revcut_rl] 1);
@@ -60,7 +60,7 @@
by (fast_tac (!claset addSIs [not_emptyI, RepFunI]
addSEs [not_emptyE, RepFunE]
addSDs [sym RS (RepFun_eq_0_iff RS iffD1)]) 1);
-val RepRep_conj = result();
+qed "RepRep_conj";
goal thy "!!c. [|c : a; x = c Un {0}; x ~: a |] ==> x - {0} : a";
by (hyp_subst_tac 1);
--- a/src/ZF/AC/AC7_AC9.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/AC7_AC9.ML Mon Sep 29 11:48:48 1997 +0200
@@ -15,26 +15,26 @@
goal ZF.thy "!!A. [| C~:A; B:A |] ==> B~=C";
by (Fast_tac 1);
-val mem_not_eq_not_mem = result();
+qed "mem_not_eq_not_mem";
goal thy "!!A. [| 0~:A; B:A |] ==> (nat->Union(A))*B ~= 0";
by (fast_tac (!claset addSDs [Sigma_empty_iff RS iffD1]
addDs [fun_space_emptyD, mem_not_eq_not_mem]
addEs [equals0D]
addSIs [equals0I,UnionI]) 1);
-val Sigma_fun_space_not0 = result();
+qed "Sigma_fun_space_not0";
goal thy "!!A C. (ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)";
by (REPEAT (rtac ballI 1));
by (resolve_tac [bspec RS (bspec RSN (2, eqpoll_sym RSN (2, eqpoll_trans)))] 1
THEN REPEAT (assume_tac 1));
-val all_eqpoll_imp_pair_eqpoll = result();
+qed "all_eqpoll_imp_pair_eqpoll";
goal thy "!!A. [| ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)); b:A \
\ |] ==> P(b)=R(b)";
by (dtac bspec 1 THEN (assume_tac 1));
by (Asm_full_simp_tac 1);
-val if_eqE1 = result();
+qed "if_eqE1";
goal thy "!!A. ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)) \
\ ==> ALL a:A. a~=b --> Q(a)=S(a)";
@@ -42,13 +42,13 @@
by (rtac impI 1);
by (dtac bspec 1 THEN (assume_tac 1));
by (Asm_full_simp_tac 1);
-val if_eqE2 = result();
+qed "if_eqE2";
goal thy "!!A. [| (lam x:A. f(x))=(lam x:A. g(x)); a:A |] ==> f(a)=g(a)";
by (fast_tac (!claset addDs [subsetD]
addSIs [lamI]
addEs [equalityE, lamE]) 1);
-val lam_eqE = result();
+qed "lam_eqE";
goalw thy [inj_def]
"!!A. C:A ==> (lam g:(nat->Union(A))*C. \
@@ -76,7 +76,7 @@
subst_elem] addEs [swap]) 2);
by (rewtac lepoll_def);
by (fast_tac (!claset addSIs [lemma]) 1);
-val Sigma_fun_space_eqpoll = result();
+qed "Sigma_fun_space_eqpoll";
(* ********************************************************************** *)
--- a/src/ZF/AC/AC_Equiv.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/AC_Equiv.ML Mon Sep 29 11:48:48 1997 +0200
@@ -29,7 +29,7 @@
by (eres_inst_tac [("n","n")] natE 1);
by (asm_simp_tac (!simpset addsimps [inj_def, succI1 RS Pi_empty2]) 1);
by (fast_tac (!claset addSIs [le_imp_subset RS id_subset_inj]) 1);
-val nat_le_imp_lepoll_lemma = result();
+qed "nat_le_imp_lepoll_lemma";
(* used in : AC10-AC15.ML WO1-WO6.ML WO6WO1.ML*)
val nat_le_imp_lepoll = nat_le_imp_lepoll_lemma RS bspec RS mp |> standard;
@@ -40,14 +40,14 @@
goal thy "!!X. (A->X)=0 ==> X=0";
by (fast_tac (!claset addSIs [equals0I] addEs [lam_type RSN (2, equals0D)]) 1);
-val fun_space_emptyD = result();
+qed "fun_space_emptyD";
(* used only in WO1_DC.ML *)
(*Note simpler proof*)
goal ZF.thy "!!A f g. [| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; \
\ A<=Df; A<=Dg |] ==> f``A=g``A";
by (asm_simp_tac (!simpset addsimps [image_fun]) 1);
-val images_eq = result();
+qed "images_eq";
(* used in : AC10-AC15.ML AC16WO4.ML WO6WO1.ML *)
(*I don't know where to put this one.*)
@@ -60,7 +60,7 @@
(Diff_sing_lepoll RSN (2, subset_imp_lepoll RS lepoll_trans)) 1
THEN (REPEAT (assume_tac 2)));
by (Fast_tac 1);
-val Diff_lepoll = result();
+qed "Diff_lepoll";
(* ********************************************************************** *)
(* lemmas concerning lepoll and eqpoll relations *)
@@ -73,13 +73,13 @@
(* lemma for ordertype_Int *)
goalw Cardinal.thy [rvimage_def] "rvimage(A,id(A),r) = r Int A*A";
by (rtac equalityI 1);
-by (Step_tac 1);
+by Safe_tac;
by (dres_inst_tac [("P","%a. <id(A)`xb,a>:r")] (id_conv RS subst) 1
THEN (assume_tac 1));
by (dres_inst_tac [("P","%a. <a,ya>:r")] (id_conv RS subst) 1
THEN (REPEAT (assume_tac 1)));
by (fast_tac (!claset addIs [id_conv RS ssubst]) 1);
-val rvimage_id = result();
+qed "rvimage_id";
(* used only in Hartog.ML *)
goal Cardinal.thy
@@ -87,49 +87,49 @@
by (res_inst_tac [("P","%a. ordertype(A,a)=ordertype(A,r)")]
(rvimage_id RS subst) 1);
by (eresolve_tac [id_bij RS bij_ordertype_vimage] 1);
-val ordertype_Int = result();
+qed "ordertype_Int";
(* used only in AC16_lemmas.ML *)
goalw CardinalArith.thy [InfCard_def]
"!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)";
by (asm_simp_tac (!simpset addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1);
-val Inf_Card_is_InfCard = result();
+qed "Inf_Card_is_InfCard";
goal thy "(THE z. {x}={z}) = x";
by (fast_tac (!claset addSIs [the_equality]
addSEs [singleton_eq_iff RS iffD1 RS sym]) 1);
-val the_element = result();
+qed "the_element";
goal thy "(lam x:A. {x}) : bij(A, {{x}. x:A})";
by (res_inst_tac [("d","%z. THE x. z={x}")] lam_bijective 1);
by (TRYALL (eresolve_tac [RepFunI, RepFunE]));
by (REPEAT (asm_full_simp_tac (!simpset addsimps [the_element]) 1));
-val lam_sing_bij = result();
+qed "lam_sing_bij";
val [major,minor] = goal thy
"[| f : Pi(A,B); (!!x. x:A ==> B(x)<=C(x)) |] ==> f : Pi(A,C)";
by (fast_tac (!claset addSIs [major RS Pi_type, minor RS subsetD,
major RS apply_type]) 1);
-val Pi_weaken_type = result();
+qed "Pi_weaken_type";
val [major, minor] = goalw thy [inj_def]
"[| f:inj(A, B); (!!a. a:A ==> f`a : C) |] ==> f:inj(A,C)";
by (fast_tac (!claset addSEs [minor]
addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1);
-val inj_strengthen_type = result();
+qed "inj_strengthen_type";
goal thy "A*B=0 <-> A=0 | B=0";
by (fast_tac (!claset addSIs [equals0I] addEs [equals0D]) 1);
-val Sigma_empty_iff = result();
+qed "Sigma_empty_iff";
goalw thy [Finite_def] "!!n. n:nat ==> Finite(n)";
by (fast_tac (!claset addSIs [eqpoll_refl]) 1);
-val nat_into_Finite = result();
+qed "nat_into_Finite";
goalw thy [Finite_def] "~Finite(nat)";
by (fast_tac (!claset addSDs [eqpoll_imp_lepoll]
addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1);
-val nat_not_Finite = result();
+qed "nat_not_Finite";
val le_imp_lepoll = le_imp_subset RS subset_imp_lepoll;
@@ -142,7 +142,7 @@
by (res_inst_tac [("b","xa")] (sym RSN (2, trans)) 1);
by (Fast_tac 1);
by (Fast_tac 1);
-val ex1_two_eq = result();
+qed "ex1_two_eq";
(* ********************************************************************** *)
(* image of a surjection *)
@@ -153,14 +153,14 @@
by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1
THEN (assume_tac 1));
by (fast_tac (!claset addSEs [apply_type] addIs [equalityI]) 1);
-val surj_image_eq = result();
+qed "surj_image_eq";
goal thy "!!y. succ(x) lepoll y ==> y ~= 0";
by (fast_tac (!claset addSDs [lepoll_0_is_0]) 1);
-val succ_lepoll_imp_not_empty = result();
+qed "succ_lepoll_imp_not_empty";
goal thy "!!x. x eqpoll succ(n) ==> x ~= 0";
by (fast_tac (!claset addSEs [eqpoll_sym RS eqpoll_0_is_0 RS succ_neq_0]) 1);
-val eqpoll_succ_imp_not_empty = result();
+qed "eqpoll_succ_imp_not_empty";
--- a/src/ZF/AC/Cardinal_aux.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/Cardinal_aux.ML Mon Sep 29 11:48:48 1997 +0200
@@ -33,7 +33,7 @@
by (resolve_tac [nat_le_infinite_Ord RS le_imp_lepoll
RSN (2, well_ord_Memrel RS well_ord_lepoll_imp_Card_le)] 1
THEN REPEAT (assume_tac 1));
-val Inf_Ord_imp_InfCard_cardinal = result();
+qed "Inf_Ord_imp_InfCard_cardinal";
val sum_lepoll_prod = [sum_eq_2_times RS equalityD1 RS subset_imp_lepoll,
asm_rl, lepoll_refl] MRS (prod_lepoll_mono RSN (2, lepoll_trans))
@@ -42,7 +42,7 @@
goal thy "!!A. [| A lepoll B; 2 lepoll A |] ==> A+B lepoll A*B";
by (REPEAT (ares_tac [[sum_lepoll_mono, sum_lepoll_prod]
MRS lepoll_trans, lepoll_refl] 1));
-val lepoll_imp_sum_lepoll_prod = result();
+qed "lepoll_imp_sum_lepoll_prod";
goal thy "!!A. [| A eqpoll i; B eqpoll i; ~Finite(i); Ord(i) |] \
\ ==> A Un B eqpoll i";
@@ -63,35 +63,35 @@
by (resolve_tac [Inf_Ord_imp_InfCard_cardinal RSN (2, well_ord_Memrel RS
well_ord_InfCard_square_eq) RS eqpoll_imp_lepoll] 1
THEN REPEAT (assume_tac 1));
-val Un_eqpoll_Inf_Ord = result();
+qed "Un_eqpoll_Inf_Ord";
val ss = (!simpset) addsimps [inj_is_fun RS apply_type, left_inverse]
setloop (split_tac [expand_if] ORELSE' etac UnE);
goal ZF.thy "{x, y} - {y} = {x} - {y}";
by (Fast_tac 1);
-val double_Diff_sing = result();
+qed "double_Diff_sing";
goal ZF.thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y";
by (split_tac [expand_if] 1);
by (asm_full_simp_tac (!simpset addsimps [double_Diff_sing, Diff_eq_0_iff]) 1);
by (fast_tac (!claset addSIs [the_equality] addEs [equalityE]) 1);
-val paired_bij_lemma = result();
+qed "paired_bij_lemma";
goal thy "(lam y:{{y,z}. y:x}. if(y-{z}=0, z, THE w. y-{z}={w})) \
\ : bij({{y,z}. y:x}, x)";
by (res_inst_tac [("d","%a. {a,z}")] lam_bijective 1);
by (TRYALL (fast_tac (!claset addSEs [RepFunE] addSIs [RepFunI]
addss (!simpset addsimps [paired_bij_lemma]))));
-val paired_bij = result();
+qed "paired_bij";
goalw thy [eqpoll_def] "{{y,z}. y:x} eqpoll x";
by (fast_tac (!claset addSIs [paired_bij]) 1);
-val paired_eqpoll = result();
+qed "paired_eqpoll";
goal thy "!!A. EX B. B eqpoll A & B Int C = 0";
by (fast_tac (!claset addSIs [paired_eqpoll, equals0I] addEs [mem_asym]) 1);
-val ex_eqpoll_disjoint = result();
+qed "ex_eqpoll_disjoint";
goal thy "!!A. [| A lepoll i; B lepoll i; ~Finite(i); Ord(i) |] \
\ ==> A Un B lepoll i";
@@ -103,7 +103,7 @@
by (eresolve_tac [eqpoll_refl RSN (2, Un_eqpoll_Inf_Ord) RS
eqpoll_imp_lepoll] 1
THEN (REPEAT (assume_tac 1)));
-val Un_lepoll_Inf_Ord = result();
+qed "Un_lepoll_Inf_Ord";
goal thy "!!P. [| P(i); i:j; Ord(j) |] ==> (LEAST i. P(i)) : j";
by (eresolve_tac [Least_le RS leE] 1);
@@ -111,7 +111,7 @@
by (etac ltE 1);
by (fast_tac (!claset addDs [OrdmemD]) 1);
by (etac subst_elem 1 THEN (assume_tac 1));
-val Least_in_Ord = result();
+qed "Least_in_Ord";
goal thy "!!x. [| well_ord(x,r); y<=x; y lepoll succ(n); n:nat |] \
\ ==> y-{THE b. first(b,y,r)} lepoll n";
@@ -120,18 +120,18 @@
by (res_inst_tac [("b","y-{THE b. first(b, y, r)}")] subst 1);
by (rtac empty_lepollI 2);
by (Fast_tac 1);
-val Diff_first_lepoll = result();
+qed "Diff_first_lepoll";
goal thy "(UN x:X. P(x)) <= (UN x:X. P(x)-Q(x)) Un (UN x:X. Q(x))";
by (Fast_tac 1);
-val UN_subset_split = result();
+qed "UN_subset_split";
goalw thy [lepoll_def] "!!a. Ord(a) ==> (UN x:a. {P(x)}) lepoll a";
by (res_inst_tac [("x","lam z:(UN x:a. {P(x)}). (LEAST i. P(i)=z)")] exI 1);
by (res_inst_tac [("d","%z. P(z)")] lam_injective 1);
by (fast_tac (!claset addSIs [Least_in_Ord]) 1);
by (fast_tac (!claset addIs [LeastI] addSEs [Ord_in_Ord]) 1);
-val UN_sing_lepoll = result();
+qed "UN_sing_lepoll";
goal thy "!!a T. [| well_ord(T, R); ~Finite(a); Ord(a); n:nat |] ==> \
\ ALL f. (ALL b:a. f`b lepoll n & f`b <= T) --> (UN b:a. f`b) lepoll a";
@@ -153,13 +153,13 @@
by (resolve_tac [UN_subset_split RS subset_imp_lepoll RS lepoll_trans] 1);
by (rtac Un_lepoll_Inf_Ord 1 THEN (REPEAT_FIRST assume_tac));
by (etac UN_sing_lepoll 1);
-val UN_fun_lepoll_lemma = result();
+qed "UN_fun_lepoll_lemma";
goal thy "!!a f. [| ALL b:a. f`b lepoll n & f`b <= T; well_ord(T, R); \
\ ~Finite(a); Ord(a); n:nat |] ==> (UN b:a. f`b) lepoll a";
by (eresolve_tac [UN_fun_lepoll_lemma RS allE] 1 THEN (REPEAT (assume_tac 1)));
by (Fast_tac 1);
-val UN_fun_lepoll = result();
+qed "UN_fun_lepoll";
goal thy "!!a f. [| ALL b:a. F(b) lepoll n & F(b) <= T; well_ord(T, R); \
\ ~Finite(a); Ord(a); n:nat |] ==> (UN b:a. F(b)) lepoll a";
@@ -168,7 +168,7 @@
THEN (TRYALL assume_tac));
by (Simp_tac 2);
by (Asm_full_simp_tac 1);
-val UN_lepoll = result();
+qed "UN_lepoll";
goal thy "!!a. Ord(a) ==> (UN b:a. F(b)) = (UN b:a. F(b) - (UN c:b. F(c)))";
by (rtac equalityI 1);
@@ -183,7 +183,7 @@
by (etac UN_E 1);
by (eres_inst_tac [("P","%z. x:F(z)"),("i","c")] less_LeastE 1);
by (eresolve_tac [Ord_Least RSN (2, ltI)] 1);
-val UN_eq_UN_Diffs = result();
+qed "UN_eq_UN_Diffs";
goalw thy [eqpoll_def] "!!A B. A Int B = 0 ==> A Un B eqpoll A + B";
by (res_inst_tac [("x","lam a:A Un B. if(a:A,Inl(a),Inr(a))")] exI 1);
@@ -193,7 +193,7 @@
by (TRYALL (split_tac [expand_if]));
by (TRYALL Asm_simp_tac);
by (fast_tac (!claset addDs [equals0D]) 1);
-val disj_Un_eqpoll_sum = result();
+qed "disj_Un_eqpoll_sum";
goalw thy [lepoll_def, eqpoll_def]
"!!X a. a lepoll X ==> EX Y. Y<=X & a eqpoll Y";
@@ -201,7 +201,7 @@
by (forward_tac [subset_refl RSN (2, restrict_bij)] 1);
by (res_inst_tac [("x","f``a")] exI 1);
by (fast_tac (!claset addSEs [inj_is_fun RS fun_is_rel RS image_subset]) 1);
-val lepoll_imp_eqpoll_subset = result();
+qed "lepoll_imp_eqpoll_subset";
(* ********************************************************************** *)
(* Diff_lesspoll_eqpoll_Card *)
@@ -235,7 +235,7 @@
(3, lt_Card_imp_lesspoll RS lepoll_lesspoll_lesspoll)] 1
THEN (TRYALL assume_tac));
by (fast_tac (!claset addSDs [lesspoll_def RS def_imp_iff RS iffD1]) 1);
-val Diff_lesspoll_eqpoll_Card_lemma = result();
+qed "Diff_lesspoll_eqpoll_Card_lemma";
goal thy "!!A. [| A eqpoll a; ~Finite(a); Card(a); B lesspoll a |] \
\ ==> A - B eqpoll a";
@@ -243,5 +243,5 @@
by (rtac Diff_lesspoll_eqpoll_Card_lemma 1 THEN (REPEAT (assume_tac 1)));
by (fast_tac (!claset addSIs [lesspoll_def RS def_imp_iff RS iffD2,
subset_imp_lepoll RS (eqpoll_imp_lepoll RSN (2, lepoll_trans))]) 1);
-val Diff_lesspoll_eqpoll_Card = result();
+qed "Diff_lesspoll_eqpoll_Card";
--- a/src/ZF/AC/DC.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/DC.ML Mon Sep 29 11:48:48 1997 +0200
@@ -112,7 +112,7 @@
by (dresolve_tac [nat_1I RSN (2, apply_type)] 1);
by (dresolve_tac [nat_0I RSN (2, bspec)] 1);
by (Asm_full_simp_tac 1);
-by (Step_tac 1);
+by Safe_tac;
by (rtac bexI 1 THEN (assume_tac 2));
by (best_tac (!claset addIs [ltD]
addSEs [nat_0_le RS leE]
@@ -124,7 +124,7 @@
by (dresolve_tac [nat_succI RS nat_succI RSN (2, apply_type)] 1
THEN (assume_tac 1));
by (Full_simp_tac 1);
-by (Step_tac 1);
+by Safe_tac;
by (forw_inst_tac [("a","succ(k)")] (domain_of_fun RS sym RS trans) 1 THEN
(assume_tac 1));
by (forw_inst_tac [("a","xa")] (domain_of_fun RS sym RS trans) 1 THEN
@@ -189,7 +189,7 @@
goal thy "!!f. [| f:A->B; B<=C |] ==> f:A->C";
by (rtac Pi_type 1 THEN (assume_tac 1));
by (fast_tac (!claset addSEs [apply_type]) 1);
-val fun_type_gen = result();
+qed "fun_type_gen";
goalw thy [DC_def, DC0_def] "!!Z. DC0 ==> DC(nat)";
by (REPEAT (resolve_tac [allI, impI] 1));
@@ -244,7 +244,7 @@
"!!A. A lesspoll nat ==> Finite(A)";
by (fast_tac (!claset addSDs [ltD, lepoll_imp_ex_le_eqpoll]
addSIs [Ord_nat]) 1);
-val lesspoll_nat_is_Finite = result();
+qed "lesspoll_nat_is_Finite";
goal thy "!!n. n:nat ==> ALL A. (A eqpoll n & A <= X) --> A : Fin(X)";
by (etac nat_induct 1);
@@ -263,7 +263,7 @@
by (dtac subsetD 1 THEN (assume_tac 1));
by (dresolve_tac [Fin.consI] 1 THEN (assume_tac 1));
by (asm_full_simp_tac (!simpset addsimps [cons_Diff]) 1);
-val Finite_Fin_lemma = result();
+qed "Finite_Fin_lemma";
goalw thy [Finite_def] "!!A. [| Finite(A); A <= X |] ==> A : Fin(X)";
by (etac bexE 1);
@@ -272,14 +272,14 @@
by (etac impE 1);
by (assume_tac 2);
by (Fast_tac 1);
-val Finite_Fin = result();
+qed "Finite_Fin";
goal thy "!!x. x: X \
\ ==> {<0,x>}: (UN n:nat. {f:succ(n)->X. ALL k:n. <f`k, f`succ(k)> : R})";
by (rtac (nat_0I RS UN_I) 1);
by (fast_tac (!claset addSIs [singleton_fun RS Pi_type]
addss (!simpset addsimps [singleton_0 RS sym])) 1);
-val singleton_in_funs = result();
+qed "singleton_in_funs";
goal thy
"!!X. [| XX = (UN n:nat. \
@@ -300,7 +300,7 @@
\ & (ALL f:Y. restrict(g, domain(f)) = f)" 1);
by (etac subst 2 THEN (*elimination equation for greater speed*)
fast_tac (!claset addss (!simpset)) 2);
-by (step_tac (!claset delrules [domainE]) 1);
+by (safe_tac (!claset delrules [domainE]));
by (swap_res_tac [bexI] 1 THEN etac singleton_in_funs 2);
by (asm_full_simp_tac (!simpset addsimps [nat_0I RSN (2, bexI),
cons_fun_type2, empty_fun]) 1);
@@ -311,24 +311,24 @@
by (asm_full_simp_tac (!simpset
addsimps [Ord_nat RSN (2, OrdmemD) RSN (2, image_fun),
[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1);
-val UN_image_succ_eq = result();
+qed "UN_image_succ_eq";
goal thy "!!f. [| (UN x:f``n. P(x)) = y; P(f`n) = succ(y); \
\ f:nat -> X; n:nat |] ==> (UN x:f``succ(n). P(x)) = succ(y)";
by (asm_full_simp_tac (!simpset addsimps [UN_image_succ_eq]) 1);
by (Fast_tac 1);
-val UN_image_succ_eq_succ = result();
+qed "UN_image_succ_eq_succ";
goal thy "!!f. [| f:succ(n) -> D; n:nat; \
\ domain(f)=succ(x); x=y |] ==> f`y : D";
by (fast_tac (!claset addEs [apply_type]
addSDs [[sym, domain_of_fun] MRS trans]) 1);
-val apply_domain_type = result();
+qed "apply_domain_type";
goal thy "!!f. [| f : nat -> X; n:nat |] ==> f``succ(n) = cons(f`n, f``n)";
by (asm_full_simp_tac (!simpset
addsimps [nat_succI, Ord_nat RSN (2, OrdmemD), image_fun]) 1);
-val image_fun_succ = result();
+qed "image_fun_succ";
goal thy "!!f. [| domain(f`n) = succ(u); f : nat -> (UN n:nat. \
\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \
@@ -336,7 +336,7 @@
\ |] ==> f`n : succ(k) -> domain(R)";
by (dtac apply_type 1 THEN (assume_tac 1));
by (fast_tac (!claset addEs [UN_E, domain_eq_imp_fun_type]) 1);
-val f_n_type = result();
+qed "f_n_type";
goal thy "!!f. [| f : nat -> (UN n:nat. \
\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \
@@ -347,7 +347,7 @@
by (etac CollectE 1);
by (dresolve_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1));
by (Asm_full_simp_tac 1);
-val f_n_pairs_in_R = result();
+qed "f_n_pairs_in_R";
goalw thy [restrict_def]
"!!f. [| restrict(f, domain(x))=x; f:n->X; domain(x) <= n \
@@ -357,7 +357,7 @@
by (fast_tac (!claset addSIs [lam_type]) 1);
by (fast_tac (!claset addSIs [lam_type]) 1);
by (asm_full_simp_tac (!simpset addsimps [subsetD RS cons_val_k]) 1);
-val restrict_cons_eq_restrict = result();
+qed "restrict_cons_eq_restrict";
goal thy "!!f. [| ALL x:f``n. restrict(f`n, domain(x))=x; \
\ f : nat -> (UN n:nat. \
@@ -372,7 +372,7 @@
by (asm_full_simp_tac (!simpset addsimps [domain_of_fun, restrict_cons_eq]) 1);
by (dtac bspec 1 THEN (assume_tac 1));
by (fast_tac (!claset addSEs [restrict_cons_eq_restrict]) 1);
-val all_in_image_restrict_eq = result();
+qed "all_in_image_restrict_eq";
goal thy
"!!X.[| ALL b<nat. <f``b, f`b> : \
@@ -429,7 +429,7 @@
by (asm_full_simp_tac (!simpset
addsimps [nat_into_Ord RS succ_in_succ, succI2, cons_val_k]) 2);
by (asm_full_simp_tac (!simpset addsimps [cons_val_n, cons_val_k]) 1);
-val simplify_recursion = result();
+qed "simplify_recursion";
goal thy "!!X. [| XX = (UN n:nat. \
@@ -510,11 +510,11 @@
THEN (assume_tac 1));
by (eres_inst_tac [("j","x")] (Ord_a RS Ord_in_Ord) 1);
by (REPEAT (fast_tac (!claset addDs [not_eq, not_eq RS not_sym]) 1));
-val fun_Ord_inj = result();
+qed "fun_Ord_inj";
goal thy "!!a. [| f:X->Y; A<=X; a:A |] ==> f`a : f``A";
by (fast_tac (!claset addSEs [image_fun RS ssubst]) 1);
-val value_in_image = result();
+qed "value_in_image";
goalw thy [DC_def, WO3_def]
"!!Z. ALL K. Card(K) --> DC(K) ==> WO3";
@@ -554,16 +554,16 @@
by (dresolve_tac [OrdmemD RS subsetD] 1
THEN REPEAT (assume_tac 1));
by (Asm_full_simp_tac 1);
-val lam_images_eq = result();
+qed "lam_images_eq";
goalw thy [lesspoll_def] "!!K. [| Card(K); b:K |] ==> b lesspoll K";
by (asm_full_simp_tac (!simpset addsimps [Card_iff_initial]) 1);
by (fast_tac (!claset addSIs [le_imp_lepoll, ltI, leI]) 1);
-val in_Card_imp_lesspoll = result();
+qed "in_Card_imp_lesspoll";
goal thy "(lam b:a. P(b)) : a -> {P(b). b:a}";
by (fast_tac (!claset addSIs [lam_type, RepFunI]) 1);
-val lam_type_RepFun = result();
+qed "lam_type_RepFun";
goal thy "!!Z. [| ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y, x> : R); \
\ b:a; Z:Pow(X); Z lesspoll a |] \
--- a/src/ZF/AC/DC_lemmas.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/DC_lemmas.ML Mon Sep 29 11:48:48 1997 +0200
@@ -12,7 +12,7 @@
by (res_inst_tac [("d","%z. P(z)")] (sym RSN (2, lam_injective)) 1);
by (fast_tac (!claset addSEs [RepFunE] addSIs [Least_in_Ord, prem]) 1);
by (REPEAT (eresolve_tac [RepFunE, LeastI, prem RS Ord_in_Ord] 1));
-val RepFun_lepoll = result();
+qed "RepFun_lepoll";
goalw thy [lesspoll_def] "!!n. n:nat ==> n lesspoll nat";
by (rtac conjI 1);
@@ -23,7 +23,7 @@
by (eresolve_tac [nat_succI RS (Ord_nat RSN (2, OrdmemD) RS
subset_imp_lepoll) RS lepoll_trans] 1
THEN (assume_tac 1));
-val n_lesspoll_nat = result();
+qed "n_lesspoll_nat";
goalw thy [lepoll_def]
"!!f. [| f:X->Y; Ord(X) |] ==> f``X lepoll X";
@@ -31,7 +31,7 @@
by (res_inst_tac [("d","%z. f`z")] lam_injective 1);
by (fast_tac (!claset addSIs [Least_in_Ord, apply_equality]) 1);
by (fast_tac (!claset addSEs [Ord_in_Ord] addSIs [LeastI, apply_equality]) 1);
-val image_Ord_lepoll = result();
+qed "image_Ord_lepoll";
val [major, minor] = goal thy
"[| (!!g. g:X ==> EX u. <g,u>:R); R<=X*X \
@@ -40,39 +40,39 @@
by (etac rangeE 1);
by (dresolve_tac [minor RS subsetD RS SigmaD2 RS major] 1);
by (Fast_tac 1);
-val range_subset_domain = result();
+qed "range_subset_domain";
val prems = goal thy "!!k. k:n ==> k~=n";
by (fast_tac (!claset addSEs [mem_irrefl]) 1);
-val mem_not_eq = result();
+qed "mem_not_eq";
goalw thy [succ_def] "!!g. g:n->X ==> cons(<n,x>, g) : succ(n) -> cons(x, X)";
by (fast_tac (!claset addSIs [fun_extend] addSEs [mem_irrefl]) 1);
-val cons_fun_type = result();
+qed "cons_fun_type";
goal thy "!!g. [| g:n->X; x:X |] ==> cons(<n,x>, g) : succ(n) -> X";
by (etac (cons_absorb RS subst) 1 THEN etac cons_fun_type 1);
-val cons_fun_type2 = result();
+qed "cons_fun_type2";
goal thy "!!n. n: nat ==> cons(<n,x>, g)``n = g``n";
by (fast_tac (!claset addSEs [mem_irrefl]) 1);
-val cons_image_n = result();
+qed "cons_image_n";
goal thy "!!n. g:n->X ==> cons(<n,x>, g)`n = x";
by (fast_tac (!claset addSIs [apply_equality] addSEs [cons_fun_type]) 1);
-val cons_val_n = result();
+qed "cons_val_n";
goal thy "!!k. k : n ==> cons(<n,x>, g)``k = g``k";
by (fast_tac (!claset addEs [mem_asym]) 1);
-val cons_image_k = result();
+qed "cons_image_k";
goal thy "!!k. [| k:n; g:n->X |] ==> cons(<n,x>, g)`k = g`k";
by (fast_tac (!claset addSIs [apply_equality, consI2] addSEs [cons_fun_type, apply_Pair]) 1);
-val cons_val_k = result();
+qed "cons_val_k";
goal thy "!!f. domain(f)=x ==> domain(cons(<x,y>, f)) = succ(x)";
by (asm_full_simp_tac (!simpset addsimps [domain_cons, succ_def]) 1);
-val domain_cons_eq_succ = result();
+qed "domain_cons_eq_succ";
goalw thy [restrict_def] "!!g. g:n->X ==> restrict(cons(<n,x>, g), n)=g";
by (rtac fun_extension 1);
@@ -81,27 +81,27 @@
by (etac succI2 1);
by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [cons_val_k]) 1);
-val restrict_cons_eq = result();
+qed "restrict_cons_eq";
goal thy "!!k. [| Ord(k); i:k |] ==> succ(i) : succ(k)";
by (resolve_tac [Ord_linear RS disjE] 1 THEN (assume_tac 3));
by (REPEAT (fast_tac (!claset addSIs [Ord_succ]
addEs [Ord_in_Ord, mem_irrefl, mem_asym]
addSDs [succ_inject]) 1));
-val succ_in_succ = result();
+qed "succ_in_succ";
goalw thy [restrict_def]
"!!f. [| restrict(f, domain(g)) = g; x: domain(g) |] ==> f`x = g`x";
by (etac subst 1);
by (Asm_full_simp_tac 1);
-val restrict_eq_imp_val_eq = result();
+qed "restrict_eq_imp_val_eq";
goal thy "!!f. [| domain(f)=A; f:B->C |] ==> f:A->C";
by (forward_tac [domain_of_fun] 1);
by (Fast_tac 1);
-val domain_eq_imp_fun_type = result();
+qed "domain_eq_imp_fun_type";
goal thy "!!R. [| R <= A * B; R ~= 0 |] ==> EX x. x:domain(R)";
by (fast_tac (!claset addSEs [not_emptyE]) 1);
-val ex_in_domain = result();
+qed "ex_in_domain";
--- a/src/ZF/AC/HH.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/HH.ML Mon Sep 29 11:48:48 1997 +0200
@@ -19,37 +19,37 @@
\ in if(f`z:Pow(z)-{0}, f`z, {x}))";
by (resolve_tac [HH_def RS def_transrec RS trans] 1);
by (Simp_tac 1);
-val HH_def_satisfies_eq = result();
+qed "HH_def_satisfies_eq";
goal thy "HH(f,x,a) : Pow(x)-{0} | HH(f,x,a)={x}";
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1);
by (simp_tac (!simpset addsimps [Let_def, Diff_subset RS PowI]
setloop split_tac [expand_if]) 1);
by (Fast_tac 1);
-val HH_values = result();
+qed "HH_values";
goal thy "!!A. B<=A ==> X-(UN a:A. P(a)) = X-(UN a:A-B. P(a))-(UN b:B. P(b))";
by (Fast_tac 1);
-val subset_imp_Diff_eq = result();
+qed "subset_imp_Diff_eq";
goal thy "!!c. [| c:a-b; b<a |] ==> c=b | b<c & c<a";
by (etac ltE 1);
-by (dres_inst_tac [("x","c")] Ord_linear 1);
+by (dtac Ord_linear 1);
+by (fast_tac (!claset addSIs [ltI] addIs [Ord_in_Ord]) 2);
by (fast_tac (!claset addEs [Ord_in_Ord]) 1);
-by (fast_tac (!claset addSIs [ltI] addIs [Ord_in_Ord]) 1);
-val Ord_DiffE = result();
+qed "Ord_DiffE";
val prems = goal thy "(!!y. y:A ==> P(y) = {x}) ==> x - (UN y:A. P(y)) = x";
by (asm_full_simp_tac (!simpset addsimps prems) 1);
by (fast_tac (!claset addSDs [prem] addSEs [mem_irrefl]) 1);
-val Diff_UN_eq_self = result();
+qed "Diff_UN_eq_self";
goal thy "!!a. x - (UN b:a. HH(f,x,b)) = x - (UN b:a1. HH(f,x,b)) \
\ ==> HH(f,x,a) = HH(f,x,a1)";
by (resolve_tac [HH_def_satisfies_eq RS
(HH_def_satisfies_eq RS sym RSN (3, trans RS trans))] 1);
by (etac subst_context 1);
-val HH_eq = result();
+qed "HH_eq";
goal thy "!!a. [| HH(f,x,b)={x}; b<a |] ==> HH(f,x,a)={x}";
by (res_inst_tac [("P","b<a")] impE 1 THEN REPEAT (assume_tac 2));
@@ -62,14 +62,14 @@
by (rtac Diff_UN_eq_self 1);
by (dtac Ord_DiffE 1 THEN (assume_tac 1));
by (fast_tac (!claset addEs [ltE]) 1);
-val HH_is_x_gt_too = result();
+qed "HH_is_x_gt_too";
goal thy "!!a. [| HH(f,x,a) : Pow(x)-{0}; b<a |] ==> HH(f,x,b) : Pow(x)-{0}";
by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1));
by (dtac HH_is_x_gt_too 1 THEN (assume_tac 1));
by (dtac subst 1 THEN (assume_tac 1));
by (fast_tac (!claset addSEs [mem_irrefl]) 1);
-val HH_subset_x_lt_too = result();
+qed "HH_subset_x_lt_too";
goal thy "!!a. HH(f,x,a) : Pow(x)-{0} \
\ ==> HH(f,x,a) : Pow(x - (UN b:a. HH(f,x,b)))-{0}";
@@ -79,14 +79,14 @@
by (dresolve_tac [expand_if RS iffD1] 1);
by (simp_tac (!simpset setloop split_tac [expand_if] ) 1);
by (fast_tac (subset_cs addSEs [mem_irrefl]) 1);
-val HH_subset_x_imp_subset_Diff_UN = result();
+qed "HH_subset_x_imp_subset_Diff_UN";
goal thy "!!x. [| HH(f,x,v)=HH(f,x,w); HH(f,x,v): Pow(x)-{0}; v:w |] ==> P";
by (forw_inst_tac [("P","%y. y: Pow(x)-{0}")] subst 1 THEN (assume_tac 1));
by (dres_inst_tac [("a","w")] HH_subset_x_imp_subset_Diff_UN 1);
by (dtac subst_elem 1 THEN (assume_tac 1));
by (fast_tac (!claset addSIs [singleton_iff RS iffD2, equals0I]) 1);
-val HH_eq_arg_lt = result();
+qed "HH_eq_arg_lt";
goal thy "!!x. [| HH(f,x,v)=HH(f,x,w); HH(f,x,w): Pow(x)-{0}; \
\ Ord(v); Ord(w) |] ==> v=w";
@@ -95,7 +95,7 @@
THEN REPEAT (assume_tac 2));
by (dtac subst_elem 1 THEN (assume_tac 1));
by (fast_tac (FOL_cs addDs [ltD] addSEs [HH_eq_arg_lt]) 1);
-val HH_eq_imp_arg_eq = result();
+qed "HH_eq_imp_arg_eq";
goalw thy [lepoll_def, inj_def]
"!!i. [| HH(f, x, i) : Pow(x)-{0}; Ord(i) |] ==> i lepoll Pow(x)-{0}";
@@ -103,24 +103,24 @@
by (Asm_simp_tac 1);
by (fast_tac (FOL_cs addSEs [HH_eq_imp_arg_eq, Ord_in_Ord, HH_subset_x_lt_too]
addSIs [lam_type, ballI, ltI] addIs [bexI]) 1);
-val HH_subset_x_imp_lepoll = result();
+qed "HH_subset_x_imp_lepoll";
goal thy "HH(f, x, Hartog(Pow(x)-{0})) = {x}";
by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 2));
by (fast_tac (FOL_cs addSDs [HH_subset_x_imp_lepoll]
addSIs [Ord_Hartog] addSEs [HartogE]) 1);
-val HH_Hartog_is_x = result();
+qed "HH_Hartog_is_x";
goal thy "HH(f, x, LEAST i. HH(f, x, i) = {x}) = {x}";
by (fast_tac (!claset addSIs [Ord_Hartog, HH_Hartog_is_x, LeastI]) 1);
-val HH_Least_eq_x = result();
+qed "HH_Least_eq_x";
goal thy "!!a. a:(LEAST i. HH(f,x,i)={x}) ==> HH(f,x,a) : Pow(x)-{0}";
by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1));
by (rtac less_LeastE 1);
by (eresolve_tac [Ord_Least RSN (2, ltI)] 2);
by (assume_tac 1);
-val less_Least_subset_x = result();
+qed "less_Least_subset_x";
(* ********************************************************************** *)
(* Lemmas used in the proofs of AC1 ==> WO2 and AC17 ==> AC1 *)
@@ -132,29 +132,29 @@
by (Asm_full_simp_tac 1);
by (fast_tac (!claset addSIs [lam_type] addDs [less_Least_subset_x]
addSEs [HH_eq_imp_arg_eq, Ord_Least RS Ord_in_Ord]) 1);
-val lam_Least_HH_inj_Pow = result();
+qed "lam_Least_HH_inj_Pow";
goal thy "!!x. ALL a:(LEAST i. HH(f,x,i)={x}). EX z:x. HH(f,x,a) = {z} \
\ ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \
\ : inj(LEAST i. HH(f,x,i)={x}, {{y}. y:x})";
by (resolve_tac [lam_Least_HH_inj_Pow RS inj_strengthen_type] 1);
by (Asm_full_simp_tac 1);
-val lam_Least_HH_inj = result();
+qed "lam_Least_HH_inj";
goalw thy [surj_def]
"!!x. [| x - (UN a:A. F(a)) = 0; \
\ ALL a:A. EX z:x. F(a) = {z} |] \
\ ==> (lam a:A. F(a)) : surj(A, {{y}. y:x})";
by (asm_full_simp_tac (!simpset addsimps [lam_type, Diff_eq_0_iff]) 1);
-by (Step_tac 1);
+by Safe_tac;
by (set_mp_tac 1);
by (deepen_tac (!claset addSIs [bexI] addSEs [equalityE]) 4 1);
-val lam_surj_sing = result();
+qed "lam_surj_sing";
goal thy "!!x. y:Pow(x)-{0} ==> x ~= 0";
by (fast_tac (!claset addSIs [equals0I, singletonI RS subst_elem]
addSDs [equals0D]) 1);
-val not_emptyI2 = result();
+qed "not_emptyI2";
goal thy "!!f. f`(x - (UN j:i. HH(f,x,j))): Pow(x - (UN j:i. HH(f,x,j)))-{0} \
\ ==> HH(f, x, i) : Pow(x) - {0}";
@@ -162,7 +162,7 @@
by (asm_full_simp_tac (!simpset addsimps [Let_def, Diff_subset RS PowI,
not_emptyI2 RS if_P]) 1);
by (Fast_tac 1);
-val f_subset_imp_HH_subset = result();
+qed "f_subset_imp_HH_subset";
val [prem] = goal thy "(!!z. z:Pow(x)-{0} ==> f`z : Pow(z)-{0}) ==> \
\ x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0";
@@ -172,20 +172,20 @@
f_subset_imp_HH_subset] 1);
by (fast_tac (!claset addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem)]
addSEs [mem_irrefl]) 1);
-val f_subsets_imp_UN_HH_eq_x = result();
+qed "f_subsets_imp_UN_HH_eq_x";
goal thy "HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j))) | HH(f,x,i)={x}";
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1);
by (simp_tac (!simpset addsimps [Let_def, Diff_subset RS PowI]
setloop split_tac [expand_if]) 1);
-val HH_values2 = result();
+qed "HH_values2";
goal thy
"!!f. HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j)))";
by (resolve_tac [HH_values2 RS disjE] 1 THEN (assume_tac 1));
by (fast_tac (!claset addSEs [equalityE, mem_irrefl]
addSDs [singleton_subsetD]) 1);
-val HH_subset_imp_eq = result();
+qed "HH_subset_imp_eq";
goal thy "!!f. [| f : (Pow(x)-{0}) -> {{z}. z:x}; \
\ a:(LEAST i. HH(f,x,i)={x}) |] ==> EX z:x. HH(f,x,a) = {z}";
@@ -196,7 +196,7 @@
by (fast_tac
(!claset addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1);
by (fast_tac (!claset addss (!simpset)) 1);
-val f_sing_imp_HH_sing = result();
+qed "f_sing_imp_HH_sing";
goalw thy [bij_def]
"!!f. [| x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0; \
@@ -205,13 +205,13 @@
\ : bij(LEAST i. HH(f,x,i)={x}, {{y}. y:x})";
by (fast_tac (!claset addSIs [lam_Least_HH_inj, lam_surj_sing,
f_sing_imp_HH_sing]) 1);
-val f_sing_lam_bij = result();
+qed "f_sing_lam_bij";
goal thy "!!f. f: (PROD X: Pow(x)-{0}. F(X)) \
\ ==> (lam X:Pow(x)-{0}. {f`X}) : (PROD X: Pow(x)-{0}. {{z}. z:F(X)})";
by (fast_tac (FOL_cs addSIs [lam_type, RepFun_eqI, singleton_eq_iff RS iffD2]
addDs [apply_type]) 1);
-val lam_singI = result();
+qed "lam_singI";
val bij_Least_HH_x =
(lam_singI RSN (2, [f_sing_lam_bij, lam_sing_bij RS bij_converse_bij]
--- a/src/ZF/AC/Hartog.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/Hartog.ML Mon Sep 29 11:48:48 1997 +0200
@@ -31,7 +31,7 @@
goal thy "!!X. [| Ord(a); a lepoll X |] ==> \
\ EX Y. Y<=X & (EX R. R<=X*X & ordertype(Y,R)=a)";
by (dtac Ord_lepoll_imp_ex_well_ord 1 THEN (assume_tac 1));
-by (Step_tac 1);
+by Safe_tac;
by (REPEAT (ares_tac [exI, conjI] 1));
by (etac ordertype_Int 2);
by (Fast_tac 1);
--- a/src/ZF/AC/WO1_WO6.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/WO1_WO6.ML Mon Sep 29 11:48:48 1997 +0200
@@ -34,16 +34,16 @@
goal thy "!!f. f: A->B ==> (lam x:A. {f`x}): A -> {{b}. b:B}";
by (fast_tac (!claset addSIs [lam_type, apply_type]) 1);
-val lam_sets = result();
+qed "lam_sets";
goalw thy [surj_def] "!!f. f:surj(A,B) ==> (UN a:A. {f`a}) = B";
by (fast_tac (!claset addSEs [apply_type]) 1);
-val surj_imp_eq_ = result();
+qed "surj_imp_eq_";
goal thy "!!f. [| f:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B";
by (fast_tac (!claset addSDs [surj_imp_eq_]
addSIs [ltI] addSEs [ltE]) 1);
-val surj_imp_eq = result();
+qed "surj_imp_eq";
goalw thy WO_defs "!!Z. WO1 ==> WO4(1)";
by (rtac allI 1);
--- a/src/ZF/AC/WO1_WO7.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/WO1_WO7.ML Mon Sep 29 11:48:48 1997 +0200
@@ -13,7 +13,7 @@
goalw thy [WO7_def] "WO7 <-> (ALL X. ~Finite(X) --> \
\ (EX R. well_ord(X,R) & ~well_ord(X,converse(R))))";
by (fast_tac (!claset addSEs [Finite_well_ord_converse]) 1);
-val WO7_iff_LEMMA = result();
+qed "WO7_iff_LEMMA";
(* ********************************************************************** *)
(* It is also easy to show that LEMMA implies WO1. *)
@@ -28,7 +28,7 @@
by (rewrite_goals_tac [Finite_def, eqpoll_def]);
by (fast_tac (!claset addSIs [[bij_is_inj, nat_implies_well_ord] MRS
well_ord_rvimage]) 1);
-val LEMMA_imp_WO1 = result();
+qed "LEMMA_imp_WO1";
(* ********************************************************************** *)
(* The Rubins' proof of the other implication is contained within the *)
@@ -55,12 +55,12 @@
by (eres_inst_tac [("x","succ(x)")] allE 1);
by (fast_tac (!claset addSIs [nat_succI, converseI, MemrelI,
nat_succI RSN (2, subsetD)]) 1);
-val converse_Memrel_not_wf_on = result();
+qed "converse_Memrel_not_wf_on";
goalw thy [well_ord_def]
"!!a. [| Ord(a); ~Finite(a) |] ==> ~well_ord(a,converse(Memrel(a)))";
by (fast_tac (!claset addSDs [converse_Memrel_not_wf_on]) 1);
-val converse_Memrel_not_well_ord = result();
+qed "converse_Memrel_not_well_ord";
goal thy "!!A. [| well_ord(A,r); well_ord(A,converse(r)) |] \
\ ==> well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r))))";
@@ -72,7 +72,7 @@
by (etac (ordertype_ord_iso RS ord_iso_sym RS ord_iso_is_bij RS
bij_is_inj RS well_ord_rvimage) 1
THEN (assume_tac 1));
-val well_ord_converse_Memrel = result();
+qed "well_ord_converse_Memrel";
goalw thy [WO1_def] "!!Z. WO1 ==> ALL X. ~Finite(X) --> \
\ (EX R. well_ord(X,R) & ~well_ord(X,converse(R)))";
@@ -86,5 +86,5 @@
bij_is_inj RS (exI RS (lepoll_def RS def_imp_iff RS iffD2))
RS lepoll_Finite]
addSIs [notI] addEs [notE]) 1);
-val WO1_imp_LEMMA = result();
+qed "WO1_imp_LEMMA";
--- a/src/ZF/AC/WO2_AC16.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/WO2_AC16.ML Mon Sep 29 11:48:48 1997 +0200
@@ -105,7 +105,7 @@
\ C lesspoll a |] ==> A - B - C eqpoll a";
by (rtac Diff_lesspoll_eqpoll_Card 1 THEN (REPEAT (assume_tac 1)));
by (rtac Diff_lesspoll_eqpoll_Card 1 THEN (REPEAT (assume_tac 1)));
-val dbl_Diff_eqpoll_Card = result();
+qed "dbl_Diff_eqpoll_Card";
(* ********************************************************************** *)
(* Case of finite ordinals *)
@@ -121,11 +121,11 @@
by (rtac lepoll_trans 1 THEN (assume_tac 2));
by (fast_tac (!claset addSEs [Ord_nat RSN (2, ltI) RS leI RS le_imp_subset RS
subset_imp_lepoll RSN (2, eqpoll_imp_lepoll RS lepoll_trans)]) 1);
-val Finite_lesspoll_infinite_Ord = result();
+qed "Finite_lesspoll_infinite_Ord";
goal thy "!!x. x:X ==> Union(X) = Union(X-{x}) Un x";
by (Fast_tac 1);
-val Union_eq_Un_Diff = result();
+qed "Union_eq_Un_Diff";
goal thy "!!n. n:nat ==> ALL X. X eqpoll n --> (ALL x:X. Finite(x)) \
\ --> Finite(Union(X))";
@@ -139,19 +139,19 @@
by (rtac Finite_Un 1);
by (Fast_tac 2);
by (fast_tac (!claset addSIs [Diff_sing_eqpoll]) 1);
-val Finite_Union_lemma = result();
+qed "Finite_Union_lemma";
goal thy "!!X. [| ALL x:X. Finite(x); Finite(X) |] ==> Finite(Union(X))";
by (eresolve_tac [Finite_def RS def_imp_iff RS iffD1 RS bexE] 1);
by (dtac Finite_Union_lemma 1);
by (Fast_tac 1);
-val Finite_Union = result();
+qed "Finite_Union";
goalw thy [Finite_def] "!!x. [| x lepoll n; n:nat |] ==> Finite(x)";
by (fast_tac (!claset
addEs [nat_into_Ord RSN (2, lepoll_imp_ex_le_eqpoll) RS exE,
Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD]) 1);
-val lepoll_nat_num_imp_Finite = result();
+qed "lepoll_nat_num_imp_Finite";
goal thy "!!X. [| ALL x:X. x lepoll n & x <= T; well_ord(T, R); X lepoll b; \
\ b<a; ~Finite(a); Card(a); n:nat |] \
@@ -175,7 +175,7 @@
THEN REPEAT (assume_tac 1));
by (rtac UN_lepoll 1
THEN (TRYALL (fast_tac (!claset addSEs [lt_Ord]))));
-val Union_lesspoll = result();
+qed "Union_lesspoll";
(* ********************************************************************** *)
(* recfunAC16_lepoll_index *)
@@ -183,20 +183,20 @@
goal thy "A Un {a} = cons(a, A)";
by (Fast_tac 1);
-val Un_sing_eq_cons = result();
+qed "Un_sing_eq_cons";
goal thy "!!A. A lepoll B ==> A Un {a} lepoll succ(B)";
by (asm_simp_tac (!simpset addsimps [Un_sing_eq_cons, succ_def]) 1);
by (eresolve_tac [mem_not_refl RSN (2, cons_lepoll_cong)] 1);
-val Un_lepoll_succ = result();
+qed "Un_lepoll_succ";
goal thy "!!a. Ord(a) ==> F(a) - (UN b<succ(a). F(b)) = 0";
by (fast_tac (!claset addSIs [OUN_I, le_refl]) 1);
-val Diff_UN_succ_empty = result();
+qed "Diff_UN_succ_empty";
goal thy "!!a. Ord(a) ==> F(a) Un X - (UN b<succ(a). F(b)) <= X";
by (fast_tac (!claset addSIs [OUN_I, le_refl]) 1);
-val Diff_UN_succ_subset = result();
+qed "Diff_UN_succ_subset";
goal thy "!!x. Ord(x) ==> \
\ recfunAC16(f, g, x, a) - (UN i<x. recfunAC16(f, g, i, a)) lepoll 1";
@@ -211,12 +211,12 @@
addSEs [Diff_UN_succ_empty RS ssubst]) 1);
by (fast_tac (!claset addSEs [Diff_UN_succ_subset RS subset_imp_lepoll RS
(singleton_eqpoll_1 RS eqpoll_imp_lepoll RSN (2, lepoll_trans))]) 1);
-val recfunAC16_Diff_lepoll_1 = result();
+qed "recfunAC16_Diff_lepoll_1";
goal thy "!!z. [| z : F(x); Ord(x) |] \
\ ==> z:F(LEAST i. z:F(i)) - (UN j<(LEAST i. z:F(i)). F(j))";
by (fast_tac (!claset addEs [less_LeastE] addSEs [OUN_E, LeastI]) 1);
-val in_Least_Diff = result();
+qed "in_Least_Diff";
goal thy "!!w. [| (LEAST i. w:F(i)) = (LEAST i. z:F(i)); \
\ w:(UN i<a. F(i)); z:(UN i<a. F(i)) |] \
@@ -229,11 +229,11 @@
by (etac subst 1 THEN (assume_tac 1));
by (eresolve_tac [lt_Ord RSN (2, Least_le) RS lt_trans1] 1
THEN (REPEAT (assume_tac 1)));
-val Least_eq_imp_ex = result();
+qed "Least_eq_imp_ex";
goal thy "!!A. [| A lepoll 1; a:A; b:A |] ==> a=b";
by (fast_tac (!claset addSDs [lepoll_1_is_sing]) 1);
-val two_in_lepoll_1 = result();
+qed "two_in_lepoll_1";
goal thy "!!a. [| ALL i<a. F(i)-(UN j<i. F(j)) lepoll 1; Limit(a) |] \
\ ==> (UN x<a. F(x)) lepoll a";
@@ -252,7 +252,7 @@
by (rtac impI 1);
by (dtac Least_eq_imp_ex 1 THEN (REPEAT (assume_tac 1)));
by (fast_tac (!claset addSEs [two_in_lepoll_1]) 1);
-val UN_lepoll_index = result();
+qed "UN_lepoll_index";
goal thy "!!y. Ord(y) ==> recfunAC16(f, fa, y, a) lepoll y";
by (etac trans_induct 1);
@@ -266,7 +266,7 @@
by (asm_simp_tac (!simpset addsimps [recfunAC16_Limit]) 1);
by (fast_tac (!claset addSEs [lt_Ord RS recfunAC16_Diff_lepoll_1]
addSIs [UN_lepoll_index]) 1);
-val recfunAC16_lepoll_index = result();
+qed "recfunAC16_lepoll_index";
goal thy "!!y. [| recfunAC16(f,g,y,a) <= {X: Pow(A). X eqpoll n}; \
\ A eqpoll a; y<a; ~Finite(a); Card(a); n:nat |] \
@@ -277,7 +277,7 @@
by (eresolve_tac [[bij_is_inj, Card_is_Ord RS well_ord_Memrel] MRS
well_ord_rvimage] 2 THEN (assume_tac 2));
by (fast_tac (!claset addSEs [eqpoll_imp_lepoll]) 1);
-val Union_recfunAC16_lesspoll = result();
+qed "Union_recfunAC16_lesspoll";
goal thy
"!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \
@@ -293,7 +293,7 @@
THEN (TRYALL assume_tac));
by (eresolve_tac [ltD RSN (2, bij_is_fun RS apply_type) RS CollectE] 1
THEN (TRYALL assume_tac));
-val dbl_Diff_eqpoll = result();
+qed "dbl_Diff_eqpoll";
(* back to the proof *)
@@ -313,7 +313,7 @@
by (fast_tac (!claset addSIs [equals0I]) 1);
by (eresolve_tac [ltD RSN (2, bij_is_fun RS apply_type RS CollectE)] 1
THEN (REPEAT (assume_tac 1)));
-val Un_in_Collect = result();
+qed "Un_in_Collect";
(* ********************************************************************** *)
(* Lemmas simplifying assumptions *)
@@ -346,15 +346,15 @@
lepoll_imp_eqpoll_subset RS exE] 1
THEN REPEAT (assume_tac 1));
by (fast_tac (!claset addSEs [eqpoll_sym]) 1);
-val ex_subset_eqpoll = result();
+qed "ex_subset_eqpoll";
goal thy "!!A. [| A <= B Un C; A Int C = 0 |] ==> A <= B";
by (fast_tac (!claset addDs [equals0D]) 1);
-val subset_Un_disjoint = result();
+qed "subset_Un_disjoint";
goal thy "!!F. [| X:Pow(A - Union(B) -C); T:B; F<=T |] ==> F Int X = 0";
by (fast_tac (!claset addSIs [equals0I]) 1);
-val Int_empty = result();
+qed "Int_empty";
(* ********************************************************************** *)
(* equipollent subset (and finite) is the whole set *)
@@ -362,7 +362,7 @@
goal thy "!!A. [| A <= B; a : A; A - {a} = B - {a} |] ==> A = B";
by (fast_tac (!claset addSEs [equalityE]) 1);
-val Diffs_eq_imp_eq = result();
+qed "Diffs_eq_imp_eq";
goal thy "!!A. m:nat ==> ALL A B. A <= B & m lepoll A & B lepoll m --> A=B";
by (etac nat_induct 1);
@@ -380,11 +380,11 @@
by (Fast_tac 1);
by (etac Diffs_eq_imp_eq 1
THEN REPEAT (assume_tac 1));
-val subset_imp_eq_lemma = result();
+qed "subset_imp_eq_lemma";
goal thy "!!A. [| A <= B; m lepoll A; B lepoll m; m:nat |] ==> A=B";
by (fast_tac (FOL_cs addSDs [subset_imp_eq_lemma]) 1);
-val subset_imp_eq = result();
+qed "subset_imp_eq";
goal thy "!!f. [| f:bij(a, {Y:X. Y eqpoll succ(k)}); k:nat; f`b<=f`y; b<a; \
\ y<a |] ==> b=y";
@@ -396,7 +396,7 @@
CollectE, eqpoll_imp_lepoll]) 1);
by (rewrite_goals_tac [bij_def, inj_def]);
by (fast_tac (!claset addSDs [ltD]) 1);
-val bij_imp_arg_eq = result();
+qed "bij_imp_arg_eq";
goal thy
"!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \
@@ -427,7 +427,7 @@
by (dtac bij_imp_arg_eq 1 THEN REPEAT (assume_tac 1));
by (hyp_subst_tac 1);
by (eresolve_tac [bexI RSN (2, notE)] 1 THEN TRYALL assume_tac);
-val ex_next_set = result();
+qed "ex_next_set";
(* ********************************************************************** *)
(* Lemma ex_next_Ord states that for any successor *)
@@ -450,11 +450,11 @@
(2, oexI)] 1);
by (resolve_tac [right_inverse_bij RS ssubst] 1
THEN REPEAT (ares_tac [Card_is_Ord] 1));
-val ex_next_Ord = result();
+qed "ex_next_Ord";
goal thy "!!Z. [| EX! Y. Y:Z & P(Y); ~P(W) |] ==> EX! Y. Y: (Z Un {W}) & P(Y)";
by (Fast_tac 1);
-val ex1_in_Un_sing = result();
+qed "ex1_in_Un_sing";
(* ********************************************************************** *)
(* Lemma simplifying assumptions *)
@@ -520,7 +520,7 @@
THEN REPEAT (ares_tac [lt_Ord, succ_leI] 1));
(*VERY SLOW! 24 secs??*)
by (eresolve_tac [lt_Ord RSN (2, LeastI)] 1 THEN (assume_tac 1));
-val main_induct = result();
+qed "main_induct";
(* ********************************************************************** *)
(* Lemma to simplify the inductive proof *)
@@ -568,7 +568,7 @@
by (dresolve_tac [disjI1 RSN (2, mp)] 1 THEN (assume_tac 1));
by (etac ex1_two_eq 1);
by (REPEAT (Fast_tac 1));
-val lemma_simp_induct = result();
+qed "lemma_simp_induct";
(* ********************************************************************** *)
(* The target theorem *)
--- a/src/ZF/AC/WO6_WO1.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/WO6_WO1.ML Mon Sep 29 11:48:48 1997 +0200
@@ -18,7 +18,7 @@
by (asm_full_simp_tac
(!simpset addsimps [oadd_odiff_inverse, odiff_oadd_inverse]) 4);
by (safe_tac (!claset addSEs [lt_Ord]));
-val lt_oadd_odiff_disj = result();
+qed "lt_oadd_odiff_disj";
(*The corresponding elimination rule*)
val lt_oadd_odiff_cases = rule_by_tactic (safe_tac (!claset))
@@ -33,27 +33,27 @@
(* ********************************************************************** *)
goalw thy [uu_def] "domain(uu(f,b,g,d)) <= f`b";
-by (Fast_tac 1);
-val domain_uu_subset = result();
+by (Blast_tac 1);
+qed "domain_uu_subset";
goal thy "!! a. ALL b<a. f`b lepoll m ==> \
\ ALL b<a. ALL g<a. ALL d<a. domain(uu(f,b,g,d)) lepoll m";
by (fast_tac (!claset addSEs
[domain_uu_subset RS subset_imp_lepoll RS lepoll_trans]) 1);
-val quant_domain_uu_lepoll_m = result();
+qed "quant_domain_uu_lepoll_m";
goalw thy [uu_def] "uu(f,b,g,d) <= f`b * f`g";
-by (Fast_tac 1);
-val uu_subset1 = result();
+by (Blast_tac 1);
+qed "uu_subset1";
goalw thy [uu_def] "uu(f,b,g,d) <= f`d";
-by (Fast_tac 1);
-val uu_subset2 = result();
+by (Blast_tac 1);
+qed "uu_subset2";
goal thy "!! a. [| ALL b<a. f`b lepoll m; d<a |] ==> uu(f,b,g,d) lepoll m";
by (fast_tac (!claset
addSEs [uu_subset2 RS subset_imp_lepoll RS lepoll_trans]) 1);
-val uu_lepoll_m = result();
+qed "uu_lepoll_m";
(* ********************************************************************** *)
(* Two cases for lemma ii *)
@@ -65,8 +65,8 @@
\ (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 --> \
\ u(f,b,g,d) eqpoll m))";
by (Asm_simp_tac 1);
-by (fast_tac (!claset delrules [equalityI]) 1);
-val cases = result();
+by (blast_tac (!claset delrules [equalityI]) 1);
+qed "cases";
(* ********************************************************************** *)
(* Lemmas used in both cases *)
@@ -75,7 +75,7 @@
by (fast_tac (!claset addSIs [equalityI] addIs [ltI]
addSDs [lt_oadd_disj]
addSEs [lt_oadd1, oadd_lt_mono2]) 1);
-val UN_oadd = result();
+qed "UN_oadd";
(* ********************************************************************** *)
@@ -86,7 +86,7 @@
by (rtac (LetI RS LetI) 1);
by (split_tac [expand_if] 1);
by (simp_tac (!simpset addsimps [domain_uu_subset]) 1);
-val vv1_subset = result();
+qed "vv1_subset";
(* ********************************************************************** *)
(* Case 1 : Union of images is the whole "y" *)
@@ -99,11 +99,11 @@
oadd_le_self RS le_imp_not_lt, lt_Ord,
odiff_oadd_inverse, ltD,
vv1_subset RS Diff_partition, ww1_def]) 1);
-val UN_gg1_eq = result();
+qed "UN_gg1_eq";
goal thy "domain(gg1(f,a,m)) = a++a";
by (simp_tac (!simpset addsimps [lam_funtype RS domain_of_fun, gg1_def]) 1);
-val domain_gg1 = result();
+qed "domain_gg1";
(* ********************************************************************** *)
(* every value of defined function is less than or equipollent to m *)
@@ -114,7 +114,7 @@
by (etac ssubst 1);
by (res_inst_tac [("Q","%z. P(z, LEAST b. P(z, b))")] LeastI2 1);
by (REPEAT (fast_tac (!claset addSEs [LeastI]) 1));
-val nested_LeastI = result();
+qed "nested_LeastI";
val nested_Least_instance =
standard
@@ -142,14 +142,14 @@
by (excluded_middle_tac "f`(b--a) = 0" 1);
by (asm_simp_tac (!simpset addsimps [empty_lepollI]) 2);
by (rtac Diff_lepoll 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
by (rtac vv1_subset 1);
by (dtac (ospec RS mp) 1);
by (REPEAT (eresolve_tac [asm_rl, oexE] 1));
by (asm_simp_tac (!simpset
addsimps [vv1_def, Let_def, lt_Ord,
nested_Least_instance RS conjunct1]) 1);
-val gg1_lepoll_m = result();
+qed "gg1_lepoll_m";
(* ********************************************************************** *)
(* Case 2 : lemmas *)
@@ -165,19 +165,19 @@
by (fast_tac (!claset addSIs [not_emptyI]
addSDs [SigmaI RSN (2, subsetD)]
addSEs [not_emptyE]) 1);
-val ex_d_uu_not_empty = result();
+qed "ex_d_uu_not_empty";
goal thy "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \
\ y*y<=y; (UN b<a. f`b)=y |] \
\ ==> uu(f,b,g,LEAST d. (uu(f,b,g,d) ~= 0)) ~= 0";
by (dtac ex_d_uu_not_empty 1 THEN REPEAT (assume_tac 1));
by (fast_tac (!claset addSEs [LeastI, lt_Ord]) 1);
-val uu_not_empty = result();
+qed "uu_not_empty";
goal ZF.thy "!!r. [| r<=A*B; r~=0 |] ==> domain(r)~=0";
by (REPEAT (eresolve_tac [asm_rl, not_emptyE, subsetD RS SigmaE,
sym RSN (2, subst_elem) RS domainI RS not_emptyI] 1));
-val not_empty_rel_imp_domain = result();
+qed "not_empty_rel_imp_domain";
goal thy "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \
\ y*y <= y; (UN b<a. f`b)=y |] \
@@ -186,11 +186,11 @@
THEN REPEAT (assume_tac 1));
by (resolve_tac [Least_le RS lt_trans1] 1
THEN (REPEAT (ares_tac [lt_Ord] 1)));
-val Least_uu_not_empty_lt_a = result();
+qed "Least_uu_not_empty_lt_a";
goal ZF.thy "!!B. [| B<=A; a~:B |] ==> B <= A-{a}";
-by (Fast_tac 1);
-val subset_Diff_sing = result();
+by (Blast_tac 1);
+qed "subset_Diff_sing";
(*Could this be proved more directly?*)
goal thy "!!A B. [| A lepoll m; m lepoll B; B <= A; m:nat |] ==> A=B";
@@ -205,7 +205,7 @@
Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS
succ_lepoll_natE] 1
THEN REPEAT (assume_tac 1));
-val supset_lepoll_imp_eq = result();
+qed "supset_lepoll_imp_eq";
goal thy
"!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \
@@ -223,7 +223,7 @@
THEN TRYALL assume_tac);
by (rtac (eqpoll_sym RS eqpoll_imp_lepoll RSN (2, supset_lepoll_imp_eq)) 1);
by (REPEAT (fast_tac (!claset addSIs [domain_uu_subset, nat_succI]) 1));
-val uu_Least_is_fun = result();
+qed "uu_Least_is_fun";
goalw thy [vv2_def]
"!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \
@@ -232,10 +232,10 @@
\ (UN b<a. f`b)=y; b<a; g<a; m:nat; s:f`b \
\ |] ==> vv2(f,b,g,s) <= f`g";
by (split_tac [expand_if] 1);
-by (Step_tac 1);
+by Safe_tac;
by (etac (uu_Least_is_fun RS apply_type) 1);
by (REPEAT_SOME (fast_tac (!claset addSIs [not_emptyI, singleton_subsetI])));
-val vv2_subset = result();
+qed "vv2_subset";
(* ********************************************************************** *)
(* Case 2 : Union of images is the whole "y" *)
@@ -252,11 +252,11 @@
oadd_le_self RS le_imp_not_lt, lt_Ord,
odiff_oadd_inverse, ww2_def,
vv2_subset RS Diff_partition]) 1);
-val UN_gg2_eq = result();
+qed "UN_gg2_eq";
goal thy "domain(gg2(f,a,b,s)) = a++a";
by (simp_tac (!simpset addsimps [lam_funtype RS domain_of_fun, gg2_def]) 1);
-val domain_gg2 = result();
+qed "domain_gg2";
(* ********************************************************************** *)
(* every value of defined function is less than or equipollent to m *)
@@ -271,7 +271,7 @@
addSIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans,
not_lt_imp_le RS le_imp_subset RS subset_imp_lepoll,
nat_into_Ord, nat_1I]) 1);
-val vv2_lepoll = result();
+qed "vv2_lepoll";
goalw thy [ww2_def]
"!!m. [| ALL b<a. f`b lepoll succ(m); g<a; m:nat; vv2(f,b,g,d) <= f`g \
@@ -282,7 +282,7 @@
by (rtac Diff_lepoll 1
THEN (TRYALL assume_tac));
by (asm_simp_tac (!simpset addsimps [vv2_def, expand_if, not_emptyI]) 1);
-val ww2_lepoll = result();
+qed "ww2_lepoll";
goalw thy [gg2_def]
"!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 --> \
@@ -294,7 +294,7 @@
by (safe_tac (!claset addSEs [lt_oadd_odiff_cases, lt_Ord2]));
by (asm_simp_tac (!simpset addsimps [vv2_lepoll]) 1);
by (asm_simp_tac (!simpset addsimps [ww2_lepoll, vv2_subset]) 1);
-val gg2_lepoll_m = result();
+qed "gg2_lepoll_m";
(* ********************************************************************** *)
(* lemma ii *)
@@ -320,7 +320,7 @@
is just too slow.*)
by (asm_simp_tac (!simpset addsimps
[Ord_oadd, domain_gg2, UN_gg2_eq, gg2_lepoll_m]) 1);
-val lemma_ii = result();
+qed "lemma_ii";
(* ********************************************************************** *)
@@ -334,14 +334,14 @@
goal thy "ALL n:nat. rec(n, x, %k r. r Un r*r) <= \
\ rec(succ(n), x, %k r. r Un r*r)";
by (fast_tac (!claset addIs [rec_succ RS ssubst]) 1);
-val z_n_subset_z_succ_n = result();
+qed "z_n_subset_z_succ_n";
goal thy "!!n. [| ALL n:nat. f(n)<=f(succ(n)); n le m; n : nat; m: nat |] \
\ ==> f(n)<=f(m)";
by (eres_inst_tac [("P","n le m")] rev_mp 1);
by (res_inst_tac [("P","%z. n le z --> f(n) <= f(z)")] nat_induct 1);
by (REPEAT (fast_tac le_cs 1));
-val le_subsets = result();
+qed "le_subsets";
goal thy "!!n m. [| n le m; m:nat |] ==> \
\ rec(n, x, %k r. r Un r*r) <= rec(m, x, %k r. r Un r*r)";
@@ -349,7 +349,7 @@
THEN (TRYALL assume_tac));
by (eresolve_tac [Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD] 1
THEN (assume_tac 1));
-val le_imp_rec_subset = result();
+qed "le_imp_rec_subset";
goal thy "EX y. x Un y*y <= y";
by (res_inst_tac [("x","UN n:nat. rec(n, x, %k r. r Un r*r)")] exI 1);
@@ -361,7 +361,7 @@
by (fast_tac (ZF_cs addIs [le_imp_rec_subset RS subsetD]
addSIs [Un_upper1_le, Un_upper2_le, Un_nat_type]
addSEs [nat_into_Ord] addss (!simpset)) 1);
-val lemma_iv = result();
+qed "lemma_iv";
(* ********************************************************************** *)
(* Rubin & Rubin wrote : *)
@@ -380,7 +380,7 @@
goalw thy [WO6_def, NN_def] "!!y. WO6 ==> NN(y) ~= 0";
by (fast_tac (ZF_cs addEs [equals0D]) 1);
-val WO6_imp_NN_not_empty = result();
+qed "WO6_imp_NN_not_empty";
(* ********************************************************************** *)
(* 1 : NN(y) ==> y can be well-ordered *)
@@ -408,12 +408,12 @@
by (fast_tac (!claset addSEs [Least_le RS lt_trans1 RS ltD, lt_Ord]) 1);
by (resolve_tac [lemma2 RS ssubst] 1 THEN REPEAT (assume_tac 1));
by (fast_tac (!claset addSIs [the_equality]) 1);
-val NN_imp_ex_inj = result();
+qed "NN_imp_ex_inj";
goal thy "!!y. [| y*y <= y; 1 : NN(y) |] ==> EX r. well_ord(y, r)";
by (dtac NN_imp_ex_inj 1);
by (fast_tac (!claset addSEs [well_ord_Memrel RSN (2, well_ord_rvimage)]) 1);
-val y_well_ord = result();
+qed "y_well_ord";
(* ********************************************************************** *)
(* reverse induction which lets us infer that 1 : NN(y) *)
@@ -424,11 +424,11 @@
\ ==> n~=0 --> P(n) --> P(1)";
by (res_inst_tac [("n","n")] nat_induct 1);
by (rtac prem1 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
by (excluded_middle_tac "x=0" 1);
-by (Fast_tac 2);
+by (Blast_tac 2);
by (fast_tac (!claset addSIs [prem2]) 1);
-val rev_induct_lemma = result();
+qed "rev_induct_lemma";
val prems = goal thy
"[| P(n); n:nat; n~=0; \
@@ -437,11 +437,11 @@
by (resolve_tac [rev_induct_lemma RS impE] 1);
by (etac impE 4 THEN (assume_tac 5));
by (REPEAT (ares_tac prems 1));
-val rev_induct = result();
+qed "rev_induct";
goalw thy [NN_def] "!!n. n:NN(y) ==> n:nat";
by (etac CollectD1 1);
-val NN_into_nat = result();
+qed "NN_into_nat";
goal thy "!!n. [| n:NN(y); y*y <= y; n~=0 |] ==> 1:NN(y)";
by (rtac rev_induct 1 THEN REPEAT (ares_tac [NN_into_nat] 1));
@@ -456,7 +456,7 @@
goalw thy [NN_def] "!!y. 0:NN(y) ==> y=0";
by (fast_tac (!claset addSIs [equalityI]
addSDs [lepoll_0_is_0] addEs [subst]) 1);
-val NN_y_0 = result();
+qed "NN_y_0";
goalw thy [WO1_def] "!!Z. WO6 ==> WO1";
by (rtac allI 1);
--- a/src/ZF/AC/WO_AC.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/WO_AC.ML Mon Sep 29 11:48:48 1997 +0200
@@ -11,12 +11,12 @@
\ ==> (THE b. first(b,B,r)) : B";
by (fast_tac (!claset addSEs [well_ord_imp_ex1_first RS theI RS
(first_def RS def_imp_iff RS iffD1 RS conjunct1)]) 1);
-val first_in_B = result();
+qed "first_in_B";
goal thy "!!A. [| well_ord(Union(A), R); 0~:A |] ==> EX f. f:(PROD X:A. X)";
by (fast_tac (!claset addSEs [first_in_B] addSIs [lam_type]) 1);
-val ex_choice_fun = result();
+qed "ex_choice_fun";
goal thy "!!A. well_ord(A, R) ==> EX f. f:(PROD X: Pow(A)-{0}. X)";
by (fast_tac (!claset addSEs [well_ord_subset RS ex_choice_fun]) 1);
-val ex_choice_fun_Pow = result();
+qed "ex_choice_fun_Pow";
--- a/src/ZF/AC/recfunAC16.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/recfunAC16.ML Mon Sep 29 11:48:48 1997 +0200
@@ -13,7 +13,7 @@
goalw thy [recfunAC16_def] "recfunAC16(f,fa,0,a) = 0";
by (rtac transrec2_0 1);
-val recfunAC16_0 = result();
+qed "recfunAC16_0";
goalw thy [recfunAC16_def] "recfunAC16(f,fa,succ(i),a) = \
\ if (EX y:recfunAC16(f,fa,i,a). fa ` i <= y, recfunAC16(f,fa,i,a), \
@@ -21,12 +21,12 @@
\ (ALL b<a. (fa`b <= f`j \
\ --> (ALL t:recfunAC16(f,fa,i,a). ~ fa`b <= t))))})";
by (rtac transrec2_succ 1);
-val recfunAC16_succ = result();
+qed "recfunAC16_succ";
goalw thy [recfunAC16_def] "!!i. Limit(i) \
\ ==> recfunAC16(f,fa,i,a) = (UN j<i. recfunAC16(f,fa,j,a))";
by (etac transrec2_Limit 1);
-val recfunAC16_Limit = result();
+qed "recfunAC16_Limit";
(* ********************************************************************** *)
(* Monotonicity of transrec2 *)
@@ -44,14 +44,14 @@
by (fast_tac (!claset addIs [OUN_I, ltI]
addSEs [Limit_has_succ RS ltE, succI1 RSN (2, Ord_in_Ord) RS le_refl,
transrec2_Limit RS ssubst]) 1);
-val transrec2_mono_lemma = result();
+qed "transrec2_mono_lemma";
val [prem1, prem2] = goal thy "[| !!g r. r <= B(g,r); j le i |] \
\ ==> transrec2(j, 0, B) <= transrec2(i, 0, B)";
by (resolve_tac [prem2 RS leE] 1);
by (resolve_tac [transrec2_mono_lemma RS impE] 1);
by (TRYALL (fast_tac (!claset addSIs [prem1, prem2, lt_Ord2])));
-val transrec2_mono = result();
+qed "transrec2_mono";
(* ********************************************************************** *)
(* Monotonicity of recfunAC16 *)
@@ -61,5 +61,5 @@
"!!i. i le j ==> recfunAC16(f, g, i, a) <= recfunAC16(f, g, j, a)";
by (rtac transrec2_mono 1);
by (REPEAT (fast_tac (!claset addIs [expand_if RS iffD2]) 1));
-val recfunAC16_mono = result();
+qed "recfunAC16_mono";
--- a/src/ZF/AC/rel_is_fun.ML Mon Sep 29 11:47:01 1997 +0200
+++ b/src/ZF/AC/rel_is_fun.ML Mon Sep 29 11:48:48 1997 +0200
@@ -22,7 +22,7 @@
by (rtac LeastI2 1);
by (REPEAT (fast_tac (!claset addSEs [nat_into_Ord RS Ord_in_Ord]
addss (!simpset addsimps [left_inverse])) 1));
-val lepoll_m_imp_domain_lepoll_m = result();
+qed "lepoll_m_imp_domain_lepoll_m";
goalw Cardinal.thy [function_def]
"!!r. [| succ(m) lepoll domain(r); r lepoll succ(m); m:nat |] ==> \
@@ -32,11 +32,11 @@
by (fast_tac (!claset addSEs [lepoll_trans RS succ_lepoll_natE,
Diff_sing_lepoll RSN (2, lepoll_m_imp_domain_lepoll_m)]
addEs [not_sym RSN (2, domain_Diff_eq) RS subst]) 1);
-val rel_domain_ex1 = result();
+qed "rel_domain_ex1";
goal Cardinal.thy
"!!r. [| succ(m) lepoll domain(r); r lepoll succ(m); m:nat; \
\ r<=A*B; A=domain(r) |] ==> r: A->B";
by (hyp_subst_tac 1);
by (asm_simp_tac (!simpset addsimps [Pi_iff, rel_domain_ex1]) 1);
-val rel_is_fun = result();
+qed "rel_is_fun";