--- a/src/ZF/AC/DC.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/AC/DC.ML Thu Aug 06 12:24:04 1998 +0200
@@ -100,8 +100,7 @@
by (fast_tac (claset() addSIs [lemma1_1] addSEs [lemma1_2, lemma1_3]) 1);
val lemma1 = result();
-Goal
-"[| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \
+Goal "[| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \
\ ALL n:nat. <f`n, f`succ(n)> : \
\ {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1)) \
\ & restrict(z2, domain(z1)) = z1}; \
@@ -136,8 +135,7 @@
by (deepen_tac (claset() addDs [domain_of_fun RS sym RS trans]) 0 1);
val lemma2 = result();
-Goal
-"[| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \
+Goal "[| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \
\ ALL n:nat. <f`n, f`succ(n)> : \
\ {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1)) \
\ & restrict(z2, domain(z1)) = z1}; \
@@ -282,8 +280,7 @@
addss (simpset() addsimps [singleton_0 RS sym])) 1);
qed "singleton_in_funs";
-Goal
- "[| XX = (UN n:nat. \
+Goal "[| XX = (UN n:nat. \
\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \
\ RR = {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f)) \
\ & (ALL f:z1. restrict(z2, domain(f)) = f)) | \
@@ -375,8 +372,7 @@
by (fast_tac (claset() addSEs [restrict_cons_eq_restrict]) 1);
qed "all_in_image_restrict_eq";
-Goal
-"[| ALL b<nat. <f``b, f`b> : \
+Goal "[| ALL b<nat. <f``b, f`b> : \
\ {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f)) & \
\ (ALL f:z1. restrict(z2, domain(f)) = f)) | \
\ (~ (EX g:XX. domain(g)=succ(UN f:z1. domain(f)) & \
@@ -455,8 +451,7 @@
by (fast_tac (FOL_cs addSEs [conjE, f_n_pairs_in_R, trans, subst_context]) 1);
val lemma2 = result();
-Goal
-"[| XX = (UN n:nat. \
+Goal "[| XX = (UN n:nat. \
\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \
\ ALL b<nat. <f``b, f`b> : \
\ {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f)) \
@@ -551,8 +546,7 @@
(* WO1 ==> ALL K. Card(K) --> DC(K) *)
(* ********************************************************************** *)
-Goal
- "[| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b";
+Goal "[| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b";
by (rtac images_eq 1);
by (REPEAT (fast_tac (claset() addSEs [RepFunI, OrdmemD]
addSIs [lam_type]) 2));
--- a/src/ZF/AC/HH.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/AC/HH.ML Thu Aug 06 12:24:04 1998 +0200
@@ -177,8 +177,7 @@
by (simp_tac (simpset() addsimps [Let_def, Diff_subset RS PowI]) 1);
qed "HH_values2";
-Goal
- "HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j)))";
+Goal "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);
--- a/src/ZF/AC/WO2_AC16.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/AC/WO2_AC16.ML Thu Aug 06 12:24:04 1998 +0200
@@ -303,8 +303,7 @@
qed "Union_recfunAC16_lesspoll";
-Goal
- "!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \
+Goal "[| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \
\ Card(a); ~ Finite(a); A eqpoll a; \
\ k : nat; m : nat; y<a; \
\ fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}) |] \
@@ -433,8 +432,7 @@
qed "bij_imp_arg_eq";
-Goal
- "!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \
+Goal "[| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \
\ Card(a); ~ Finite(a); A eqpoll a; \
\ k : nat; m : nat; y<a; \
\ fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}); \
@@ -470,8 +468,7 @@
(* ********************************************************************** *)
-Goal
- "!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \
+Goal "[| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \
\ Card(a); ~ Finite(a); A eqpoll a; \
\ k : nat; m : nat; y<a; \
\ fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}); \
--- a/src/ZF/AC/WO6_WO1.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/AC/WO6_WO1.ML Thu Aug 06 12:24:04 1998 +0200
@@ -205,8 +205,7 @@
THEN REPEAT (assume_tac 1));
qed "supset_lepoll_imp_eq";
-Goal
- "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \
+Goal "[| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \
\ domain(uu(f, b, g, d)) eqpoll succ(m); \
\ ALL b<a. f`b lepoll succ(m); y*y <= y; \
\ (UN b<a. f`b)=y; b<a; g<a; d<a; \
--- a/src/ZF/Bool.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/Bool.ML Thu Aug 06 12:24:04 1998 +0200
@@ -3,7 +3,7 @@
Author: Martin D Coen, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-For ZF/bool.thy. Booleans in Zermelo-Fraenkel Set Theory
+Booleans in Zermelo-Fraenkel Set Theory
*)
open Bool;
@@ -31,7 +31,7 @@
(** 1=0 ==> R **)
val one_neq_0 = one_not_0 RS notE;
-val major::prems = goalw Bool.thy bool_defs
+val major::prems = Goalw bool_defs
"[| c: bool; c=1 ==> P; c=0 ==> P |] ==> P";
by (rtac (major RS consE) 1);
by (REPEAT (eresolve_tac (singletonE::prems) 1));
@@ -54,17 +54,16 @@
fun bool_tac i = fast_tac (claset() addSEs [boolE] addss (simpset())) i;
-Goal
- "[| b: bool; c: A(1); d: A(0) |] ==> cond(b,c,d): A(b)";
+Goal "[| b: bool; c: A(1); d: A(0) |] ==> cond(b,c,d): A(b)";
by (bool_tac 1);
qed "cond_type";
-val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
+val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
by (rewtac rew);
by (rtac cond_1 1);
qed "def_cond_1";
-val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d";
+val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d";
by (rewtac rew);
by (rtac cond_0 1);
qed "def_cond_0";
@@ -129,8 +128,7 @@
by (bool_tac 1);
qed "and_assoc";
-Goal
- "[| a: bool; b:bool; c:bool |] ==> \
+Goal "[| a: bool; b:bool; c:bool |] ==> \
\ (a or b) and c = (a and c) or (b and c)";
by (bool_tac 1);
qed "and_or_distrib";
@@ -151,8 +149,7 @@
by (bool_tac 1);
qed "or_assoc";
-Goal
- "[| a: bool; b: bool; c: bool |] ==> \
+Goal "[| a: bool; b: bool; c: bool |] ==> \
\ (a and b) or c = (a or c) and (b or c)";
by (bool_tac 1);
qed "or_and_distrib";
--- a/src/ZF/Cardinal.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/Cardinal.ML Thu Aug 06 12:24:04 1998 +0200
@@ -99,7 +99,7 @@
by (REPEAT (assume_tac 1));
qed "eqpollI";
-val [major,minor] = goal Cardinal.thy
+val [major,minor] = Goal
"[| X eqpoll Y; [| X lepoll Y; Y lepoll X |] ==> P |] ==> P";
by (rtac minor 1);
by (REPEAT (resolve_tac [major, eqpoll_imp_lepoll, eqpoll_sym] 1));
@@ -186,7 +186,7 @@
(** LEAST -- the least number operator [from HOL/Univ.ML] **)
-val [premP,premOrd,premNot] = goalw Cardinal.thy [Least_def]
+val [premP,premOrd,premNot] = Goalw [Least_def]
"[| P(i); Ord(i); !!x. x<i ==> ~P(x) |] ==> (LEAST x. P(x)) = i";
by (rtac the_equality 1);
by (blast_tac (claset() addSIs [premP,premOrd,premNot]) 1);
@@ -250,8 +250,7 @@
(** Basic properties of cardinals **)
(*Not needed for simplification, but helpful below*)
-val prems = goal Cardinal.thy
- "[| !!y. P(y) <-> Q(y) |] ==> (LEAST x. P(x)) = (LEAST x. Q(x))";
+val prems = Goal "(!!y. P(y) <-> Q(y)) ==> (LEAST x. P(x)) = (LEAST x. Q(x))";
by (simp_tac (simpset() addsimps prems) 1);
qed "Least_cong";
@@ -273,15 +272,13 @@
(* Ord(A) ==> |A| eqpoll A *)
bind_thm ("Ord_cardinal_eqpoll", well_ord_Memrel RS well_ord_cardinal_eqpoll);
-Goal
- "[| well_ord(X,r); well_ord(Y,s); |X| = |Y| |] ==> X eqpoll Y";
+Goal "[| well_ord(X,r); well_ord(Y,s); |X| = |Y| |] ==> X eqpoll Y";
by (rtac (eqpoll_sym RS eqpoll_trans) 1);
by (etac well_ord_cardinal_eqpoll 1);
by (asm_simp_tac (simpset() addsimps [well_ord_cardinal_eqpoll]) 1);
qed "well_ord_cardinal_eqE";
-Goal
- "[| well_ord(X,r); well_ord(Y,s) |] ==> |X| = |Y| <-> X eqpoll Y";
+Goal "[| well_ord(X,r); well_ord(Y,s) |] ==> |X| = |Y| <-> X eqpoll Y";
by (blast_tac (claset() addIs [cardinal_cong, well_ord_cardinal_eqE]) 1);
qed "well_ord_cardinal_eqpoll_iff";
@@ -297,7 +294,7 @@
qed "Card_cardinal_eq";
(* Could replace the ~(j eqpoll i) by ~(i lepoll j) *)
-val prems = goalw Cardinal.thy [Card_def,cardinal_def]
+val prems = Goalw [Card_def,cardinal_def]
"[| Ord(i); !!j. j<i ==> ~(j eqpoll i) |] ==> Card(i)";
by (stac Least_equality 1);
by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1));
@@ -403,8 +400,7 @@
qed "Card_le_iff";
(*Can use AC or finiteness to discharge first premise*)
-Goal
- "[| well_ord(B,r); A lepoll B |] ==> |A| le |B|";
+Goal "[| well_ord(B,r); A lepoll B |] ==> |A| le |B|";
by (res_inst_tac [("i","|A|"),("j","|B|")] Ord_linear_le 1);
by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI]));
by (rtac (eqpollI RS cardinal_cong) 1 THEN assume_tac 1);
@@ -445,8 +441,7 @@
by (Blast_tac 1);
qed "cons_lepoll_consD";
-Goal
- "[| cons(u,A) eqpoll cons(v,B); u~:A; v~:B |] ==> A eqpoll B";
+Goal "[| cons(u,A) eqpoll cons(v,B); u~:A; v~:B |] ==> A eqpoll B";
by (asm_full_simp_tac (simpset() addsimps [eqpoll_iff]) 1);
by (blast_tac (claset() addIs [cons_lepoll_consD]) 1);
qed "cons_eqpoll_consD";
@@ -457,9 +452,8 @@
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);
+Goal "m:nat ==> ALL n: nat. m lepoll n --> m le n";
+by (nat_ind_tac "m" [] 1);
by (blast_tac (claset() addSIs [nat_0_le]) 1);
by (rtac ballI 1);
by (eres_inst_tac [("n","n")] natE 1);
@@ -470,8 +464,7 @@
bind_thm ("nat_lepoll_imp_le", nat_lepoll_imp_le_lemma RS bspec RS mp);
-Goal
- "[| m:nat; n: nat |] ==> m eqpoll n <-> m = n";
+Goal "[| m:nat; n: nat |] ==> m eqpoll n <-> m = n";
by (rtac iffI 1);
by (asm_simp_tac (simpset() addsimps [eqpoll_refl]) 2);
by (blast_tac (claset() addIs [nat_lepoll_imp_le, le_anti_sym]
@@ -578,19 +571,16 @@
setloop etac consE') 1);
qed "cons_lepoll_cong";
-Goal
- "[| A eqpoll B; a ~: A; b ~: B |] ==> cons(a,A) eqpoll cons(b,B)";
+Goal "[| A eqpoll B; a ~: A; b ~: B |] ==> cons(a,A) eqpoll cons(b,B)";
by (asm_full_simp_tac (simpset() addsimps [eqpoll_iff, cons_lepoll_cong]) 1);
qed "cons_eqpoll_cong";
-Goal
- "[| a ~: A; b ~: B |] ==> \
+Goal "[| a ~: A; b ~: B |] ==> \
\ cons(a,A) lepoll cons(b,B) <-> A lepoll B";
by (blast_tac (claset() addIs [cons_lepoll_cong, cons_lepoll_consD]) 1);
qed "cons_lepoll_cons_iff";
-Goal
- "[| a ~: A; b ~: B |] ==> \
+Goal "[| a ~: A; b ~: B |] ==> \
\ cons(a,A) eqpoll cons(b,B) <-> A eqpoll B";
by (blast_tac (claset() addIs [cons_eqpoll_cong, cons_eqpoll_consD]) 1);
qed "cons_eqpoll_cons_iff";
@@ -764,8 +754,7 @@
nat_wf_on_converse_Memrel]) 1);
qed "nat_well_ord_converse_Memrel";
-Goal
- "[| well_ord(A,r); \
+Goal "[| 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);
@@ -776,8 +765,7 @@
ordertype_ord_iso RS ord_iso_rvimage_eq]) 1);
qed "well_ord_converse";
-Goal
- "[| well_ord(A,r); A eqpoll n; n:nat |] ==> ordertype(A,r)=n";
+Goal "[| 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);
--- a/src/ZF/Coind/ECR.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/Coind/ECR.ML Thu Aug 06 12:24:04 1998 +0200
@@ -8,8 +8,7 @@
(* Specialised co-induction rule *)
-Goal
- "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \
+Goal "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \
\ <te, e_fn(x, e), t>:ElabRel; ve_dom(ve) = te_dom(te); \
\ {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}: \
\ Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |] ==> \
--- a/src/ZF/Coind/Types.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/Coind/Types.ML Thu Aug 06 12:24:04 1998 +0200
@@ -18,8 +18,7 @@
by (simp_tac (simpset() addsimps (rank_te_owr1::TyEnv.case_eqns)) 1);
qed "te_rec_emp";
-Goal
- " te_rec(te_owr(te,x,t),c_te_emp,f_te_owr) = \
+Goal " te_rec(te_owr(te,x,t),c_te_emp,f_te_owr) = \
\ f_te_owr(te,x,t,te_rec(te,c_te_emp,f_te_owr))";
by (rtac (te_rec_def RS def_Vrec RS trans) 1);
by (simp_tac (rank_ss addsimps (rank_te_owr1::TyEnv.case_eqns)) 1);
--- a/src/ZF/Epsilon.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/Epsilon.ML Thu Aug 06 12:24:04 1998 +0200
@@ -104,8 +104,7 @@
qed "mem_eclose_trans";
(*Variant of the previous lemma in a useable form for the sequel*)
-Goal
- "[| A: eclose({B}); B: eclose({C}) |] ==> A: eclose({C})";
+Goal "[| A: eclose({B}); B: eclose({C}) |] ==> A: eclose({C})";
by (rtac ([Transset_eclose, singleton_subsetI] MRS eclose_least RS subsetD) 1);
by (REPEAT (assume_tac 1));
qed "mem_eclose_sing_trans";
--- a/src/ZF/EquivClass.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/EquivClass.ML Thu Aug 06 12:24:04 1998 +0200
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-For EquivClass.thy. Equivalence relations in Zermelo-Fraenkel Set Theory
+Equivalence relations in Zermelo-Fraenkel Set Theory
*)
val RSLIST = curry (op MRS);
@@ -63,9 +63,8 @@
by (Blast_tac 1);
qed "subset_equiv_class";
-val prems = goal EquivClass.thy
- "[| r``{a} = r``{b}; equiv(A,r); b: A |] ==> <a,b>: r";
-by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1));
+Goal "[| r``{a} = r``{b}; equiv(A,r); b: A |] ==> <a,b>: r";
+by (REPEAT (ares_tac[equalityD2, subset_equiv_class] 1));
qed "eq_equiv_class";
(*thus r``{a} = r``{b} as well*)
@@ -78,14 +77,12 @@
by (safe_tac subset_cs);
qed "equiv_type";
-Goal
- "equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A";
+Goal "equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A";
by (blast_tac (claset() addIs [eq_equiv_class, equiv_class_eq]
addDs [equiv_type]) 1);
qed "equiv_class_eq_iff";
-Goal
- "[| equiv(A,r); x: A; y: A |] ==> r``{x} = r``{y} <-> <x,y>: r";
+Goal "[| equiv(A,r); x: A; y: A |] ==> r``{x} = r``{y} <-> <x,y>: r";
by (blast_tac (claset() addIs [eq_equiv_class, equiv_class_eq]
addDs [equiv_type]) 1);
qed "eq_equiv_class_iff";
@@ -94,12 +91,11 @@
(** Introduction/elimination rules -- needed? **)
-val prems = goalw EquivClass.thy [quotient_def] "x:A ==> r``{x}: A/r";
-by (rtac RepFunI 1);
-by (resolve_tac prems 1);
+Goalw [quotient_def] "x:A ==> r``{x}: A/r";
+by (etac RepFunI 1);
qed "quotientI";
-val major::prems = goalw EquivClass.thy [quotient_def]
+val major::prems = Goalw [quotient_def]
"[| X: A/r; !!x. [| X = r``{x}; x:A |] ==> P |] \
\ ==> P";
by (rtac (major RS RepFunE) 1);
@@ -138,7 +134,7 @@
qed "UN_equiv_class";
(*type checking of UN x:r``{a}. b(x) *)
-val prems = goalw EquivClass.thy [quotient_def]
+val prems = Goalw [quotient_def]
"[| equiv(A,r); congruent(r,b); X: A/r; \
\ !!x. x : A ==> b(x) : B |] \
\ ==> (UN x:X. b(x)) : B";
@@ -150,7 +146,7 @@
(*Sufficient conditions for injectiveness. Could weaken premises!
major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
*)
-val prems = goalw EquivClass.thy [quotient_def]
+val prems = Goalw [quotient_def]
"[| equiv(A,r); congruent(r,b); \
\ (UN x:X. b(x))=(UN y:Y. b(y)); X: A/r; Y: A/r; \
\ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |] \
@@ -195,7 +191,7 @@
qed "UN_equiv_class2";
(*type checking*)
-val prems = goalw EquivClass.thy [quotient_def]
+val prems = Goalw [quotient_def]
"[| equiv(A,r); congruent2(r,b); \
\ X1: A/r; X2: A/r; \
\ !!x1 x2. [| x1: A; x2: A |] ==> b(x1,x2) : B \
@@ -210,7 +206,7 @@
(*Suggested by John Harrison -- the two subproofs may be MUCH simpler
than the direct proof*)
-val prems = goalw EquivClass.thy [congruent2_def,equiv_def,refl_def]
+val prems = Goalw [congruent2_def,equiv_def,refl_def]
"[| equiv(A,r); \
\ !! y z w. [| w: A; <y,z> : r |] ==> b(y,w) = b(z,w); \
\ !! y z w. [| w: A; <y,z> : r |] ==> b(w,y) = b(w,z) \
@@ -222,7 +218,7 @@
ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));
qed "congruent2I";
-val [equivA,commute,congt] = goal EquivClass.thy
+val [equivA,commute,congt] = Goal
"[| equiv(A,r); \
\ !! y z. [| y: A; z: A |] ==> b(y,z) = b(z,y); \
\ !! y z w. [| w: A; <y,z>: r |] ==> b(w,y) = b(w,z) \
@@ -236,7 +232,7 @@
qed "congruent2_commuteI";
(*Obsolete?*)
-val [equivA,ZinA,congt,commute] = goalw EquivClass.thy [quotient_def]
+val [equivA,ZinA,congt,commute] = Goalw [quotient_def]
"[| equiv(A,r); Z: A/r; \
\ !!w. [| w: A |] ==> congruent(r, %z. b(w,z)); \
\ !!x y. [| x: A; y: A |] ==> b(y,x) = b(x,y) \
--- a/src/ZF/Finite.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/Finite.ML Thu Aug 06 12:24:04 1998 +0200
@@ -26,7 +26,7 @@
(** Induction on finite sets **)
(*Discharging x~:y entails extra work*)
-val major::prems = goal Finite.thy
+val major::prems = Goal
"[| b: Fin(A); \
\ P(0); \
\ !!x y. [| x: A; y: Fin(A); x~:y; P(y) |] ==> P(cons(x,y)) \
@@ -41,8 +41,7 @@
Addsimps Fin.intrs;
(*The union of two finite sets is finite.*)
-Goal
- "!!b c. [| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)";
+Goal "[| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)";
by (etac Fin_induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_cons])));
qed "Fin_UnI";
@@ -69,7 +68,7 @@
by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
qed "Fin_subset";
-val major::prems = goal Finite.thy
+val major::prems = Goal
"[| c: Fin(A); b: Fin(A); \
\ P(b); \
\ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \
@@ -80,7 +79,7 @@
Diff_subset RS Fin_subset]))));
qed "Fin_0_induct_lemma";
-val prems = goal Finite.thy
+val prems = Goal
"[| b: Fin(A); \
\ P(b); \
\ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \
@@ -91,10 +90,11 @@
qed "Fin_0_induct";
(*Functions from a finite ordinal*)
-val prems = goal Finite.thy "n: nat ==> n->A <= Fin(nat*A)";
-by (nat_ind_tac "n" prems 1);
+Goal "n: nat ==> n->A <= Fin(nat*A)";
+by (nat_ind_tac "n" [] 1);
by (simp_tac (simpset() addsimps [Pi_empty1, subset_iff, cons_iff]) 1);
-by (asm_simp_tac (simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
+by (asm_simp_tac
+ (simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
by (fast_tac (claset() addSIs [Fin.consI]) 1);
qed "nat_fun_subset_Fin";
--- a/src/ZF/IMP/Equiv.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/IMP/Equiv.ML Thu Aug 06 12:24:04 1998 +0200
@@ -4,8 +4,7 @@
Copyright 1994 TUM
*)
-val prems = goal Equiv.thy
- "!!a. [| a: aexp; sigma: loc -> nat |] ==> \
+Goal "[| a: aexp; sigma: loc -> nat |] ==> \
\ <a,sigma> -a-> n <-> A(a,sigma) = n";
by (res_inst_tac [("x","n")] spec 1); (* quantify n *)
by (etac aexp.induct 1);
@@ -30,8 +29,7 @@
];
-val prems = goal Equiv.thy
- "!!b. [| b: bexp; sigma: loc -> nat |] ==> \
+Goal "[| b: bexp; sigma: loc -> nat |] ==> \
\ <b,sigma> -b-> w <-> B(b,sigma) = w";
by (res_inst_tac [("x","w")] spec 1);
by (etac bexp.induct 1);
@@ -93,8 +91,7 @@
(**** Proof of Equivalence ****)
-Goal
- "ALL c:com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
+Goal "ALL c:com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
by (fast_tac (claset() addIs [C_subset RS subsetD]
addEs [com2 RS bspec]
addDs [com1]
--- a/src/ZF/Order.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/Order.ML Thu Aug 06 12:24:04 1998 +0200
@@ -19,7 +19,7 @@
by (Blast_tac 1);
qed "part_ord_Imp_asym";
-val major::premx::premy::prems = goalw Order.thy [linear_def]
+val major::premx::premy::prems = Goalw [linear_def]
"[| linear(A,r); x:A; y:A; \
\ <x,y>:r ==> P; x=y ==> P; <y,x>:r ==> P |] ==> P";
by (cut_facts_tac [major,premx,premy] 1);
@@ -66,7 +66,7 @@
bind_thm ("predI", conjI RS (pred_iff RS iffD2));
-val [major,minor] = goalw Order.thy [pred_def]
+val [major,minor] = Goalw [pred_def]
"[| y: pred(A,x,r); [| y:A; <y,x>:r |] ==> P |] ==> P";
by (rtac (major RS CollectE) 1);
by (REPEAT (ares_tac [minor] 1));
@@ -216,7 +216,7 @@
(** Order-isomorphisms -- or similarities, as Suppes calls them **)
-val prems = goalw Order.thy [ord_iso_def]
+val prems = Goalw [ord_iso_def]
"[| f: bij(A, B); \
\ !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s \
\ |] ==> f: ord_iso(A,r,B,s)";
@@ -298,8 +298,7 @@
by (asm_full_simp_tac (simpset() addsimps [comp_eq_id_iff RS iffD1]) 1);
qed "mono_ord_isoI";
-Goal
- "[| well_ord(A,r); well_ord(B,s); \
+Goal "[| well_ord(A,r); well_ord(B,s); \
\ f: mono_map(A,r,B,s); converse(f): mono_map(B,s,A,r) \
\ |] ==> f: ord_iso(A,r,B,s)";
by (REPEAT (ares_tac [mono_ord_isoI] 1));
@@ -362,8 +361,7 @@
(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
of a well-ordering*)
-Goal
- "[| well_ord(A,r); f : ord_iso(A, r, pred(A,x,r), r); x:A |] ==> P";
+Goal "[| well_ord(A,r); f : ord_iso(A, r, pred(A,x,r), r); x:A |] ==> P";
by (metacut_tac well_ord_iso_subset_lemma 1);
by (REPEAT_FIRST (ares_tac [pred_subset]));
(*Now we know f`x < x *)
@@ -374,8 +372,7 @@
qed "well_ord_iso_predE";
(*Simple consequence of Lemma 6.1*)
-Goal
- "[| well_ord(A,r); f : ord_iso(pred(A,a,r), r, pred(A,c,r), r); \
+Goal "[| well_ord(A,r); f : ord_iso(pred(A,a,r), r, pred(A,c,r), r); \
\ a:A; c:A |] ==> a=c";
by (forward_tac [well_ord_is_trans_on] 1);
by (forward_tac [well_ord_is_linear] 1);
@@ -404,8 +401,7 @@
(*But in use, A and B may themselves be initial segments. Then use
trans_pred_pred_eq to simplify the pred(pred...) terms. See just below.*)
-Goal
- "[| f : ord_iso(A,r,B,s); a:A |] ==> \
+Goal "[| f : ord_iso(A,r,B,s); a:A |] ==> \
\ restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)";
by (asm_simp_tac (simpset() addsimps [ord_iso_image_pred RS sym]) 1);
by (rewtac ord_iso_def);
@@ -416,8 +412,7 @@
qed "ord_iso_restrict_pred";
(*Tricky; a lot of forward proof!*)
-Goal
- "[| well_ord(A,r); well_ord(B,s); <a,c>: r; \
+Goal "[| well_ord(A,r); well_ord(B,s); <a,c>: r; \
\ f : ord_iso(pred(A,a,r), r, pred(B,b,s), s); \
\ g : ord_iso(pred(A,c,r), r, pred(B,d,s), s); \
\ a:A; c:A; b:B; d:B |] ==> <b,d>: s";
@@ -439,8 +434,7 @@
addIs [ord_iso_is_bij, bij_is_fun, apply_funtype];
(*See Halmos, page 72*)
-Goal
- "[| well_ord(A,r); \
+Goal "[| well_ord(A,r); \
\ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s); y: A |] \
\ ==> ~ <g`y, f`y> : s";
by (forward_tac [well_ord_iso_subset_lemma] 1);
@@ -453,8 +447,7 @@
qed "well_ord_iso_unique_lemma";
(*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*)
-Goal
- "[| well_ord(A,r); \
+Goal "[| well_ord(A,r); \
\ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s) |] ==> f = g";
by (rtac fun_extension 1);
by (REPEAT (etac (ord_iso_is_bij RS bij_is_fun) 1));
@@ -492,8 +485,7 @@
ord_iso_sym, ord_iso_trans]) 1);
qed "function_ord_iso_map";
-Goal
- "well_ord(B,s) ==> ord_iso_map(A,r,B,s) \
+Goal "well_ord(B,s) ==> ord_iso_map(A,r,B,s) \
\ : domain(ord_iso_map(A,r,B,s)) -> range(ord_iso_map(A,r,B,s))";
by (asm_simp_tac
(simpset() addsimps [Pi_iff, function_ord_iso_map,
@@ -551,8 +543,7 @@
qed "domain_ord_iso_map_subset";
(*For the 4-way case analysis in the main result*)
-Goal
- "[| well_ord(A,r); well_ord(B,s) |] ==> \
+Goal "[| well_ord(A,r); well_ord(B,s) |] ==> \
\ domain(ord_iso_map(A,r,B,s)) = A | \
\ (EX x:A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))";
by (forward_tac [well_ord_is_wf] 1);
@@ -572,8 +563,7 @@
qed "domain_ord_iso_map_cases";
(*As above, by duality*)
-Goal
- "[| well_ord(A,r); well_ord(B,s) |] ==> \
+Goal "[| well_ord(A,r); well_ord(B,s) |] ==> \
\ range(ord_iso_map(A,r,B,s)) = B | \
\ (EX y:B. range(ord_iso_map(A,r,B,s))= pred(B,y,s))";
by (resolve_tac [converse_ord_iso_map RS subst] 1);
@@ -582,8 +572,7 @@
qed "range_ord_iso_map_cases";
(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*)
-Goal
- "[| well_ord(A,r); well_ord(B,s) |] ==> \
+Goal "[| well_ord(A,r); well_ord(B,s) |] ==> \
\ ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) | \
\ (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) | \
\ (EX y:B. ord_iso_map(A,r,B,s) : ord_iso(A, r, pred(B,y,s), s))";
--- a/src/ZF/OrderArith.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/OrderArith.ML Thu Aug 06 12:24:04 1998 +0200
@@ -35,7 +35,7 @@
(** Elimination Rule **)
-val major::prems = goalw OrderArith.thy [radd_def]
+val major::prems = Goalw [radd_def]
"[| <p',p> : radd(A,r,B,s); \
\ !!x y. [| p'=Inl(x); x:A; p=Inr(y); y:B |] ==> Q; \
\ !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q; \
@@ -74,8 +74,7 @@
(** Well-foundedness **)
-Goal
- "[| wf[A](r); wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))";
+Goal "[| wf[A](r); wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))";
by (rtac wf_onI2 1);
by (subgoal_tac "ALL x:A. Inl(x): Ba" 1);
(*Proving the lemma, which is needed twice!*)
@@ -90,15 +89,13 @@
by (best_tac (claset() addSEs [raddE, bspec RS mp]) 1);
qed "wf_on_radd";
-Goal
- "[| wf(r); wf(s) |] ==> wf(radd(field(r),r,field(s),s))";
+Goal "[| wf(r); wf(s) |] ==> wf(radd(field(r),r,field(s),s))";
by (asm_full_simp_tac (simpset() addsimps [wf_iff_wf_on_field]) 1);
by (rtac (field_radd RSN (2, wf_on_subset_A)) 1);
by (REPEAT (ares_tac [wf_on_radd] 1));
qed "wf_radd";
-Goal
- "[| well_ord(A,r); well_ord(B,s) |] ==> \
+Goal "[| well_ord(A,r); well_ord(B,s) |] ==> \
\ well_ord(A+B, radd(A,r,B,s))";
by (rtac well_ordI 1);
by (asm_full_simp_tac (simpset() addsimps [well_ord_def, wf_on_radd]) 1);
@@ -108,8 +105,7 @@
(** An ord_iso congruence law **)
-Goal
- "[| f: bij(A,C); g: bij(B,D) |] ==> \
+Goal "[| f: bij(A,C); g: bij(B,D) |] ==> \
\ (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)";
by (res_inst_tac
[("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(g)`y))")]
@@ -134,8 +130,7 @@
(*Could we prove an ord_iso result? Perhaps
ord_iso(A+B, radd(A,r,B,s), A Un B, r Un s) *)
-Goal
- "A Int B = 0 ==> \
+Goal "A Int B = 0 ==> \
\ (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)";
by (res_inst_tac [("d", "%z. if(z:A, Inl(z), Inr(z))")]
lam_bijective 1);
@@ -148,16 +143,14 @@
(** Associativity **)
-Goal
- "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
+Goal "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
\ : bij((A+B)+C, A+(B+C))";
by (res_inst_tac [("d", "case(%x. Inl(Inl(x)), case(%x. Inl(Inr(x)), Inr))")]
lam_bijective 1);
by (ALLGOALS (asm_simp_tac (simpset() setloop etac sumE)));
qed "sum_assoc_bij";
-Goal
- "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
+Goal "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
\ : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t), \
\ A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))";
by (resolve_tac [sum_assoc_bij RS ord_isoI] 1);
@@ -179,7 +172,7 @@
Addsimps [rmult_iff];
-val major::prems = goal OrderArith.thy
+val major::prems = Goal
"[| <<a',b'>, <a,b>> : rmult(A,r,B,s); \
\ [| <a',a>: r; a':A; a:A; b':B; b:B |] ==> Q; \
\ [| <b',b>: s; a:A; a'=a; b':B; b:B |] ==> Q \
@@ -211,8 +204,7 @@
(** Well-foundedness **)
-Goal
- "[| wf[A](r); wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))";
+Goal "[| wf[A](r); wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))";
by (rtac wf_onI2 1);
by (etac SigmaE 1);
by (etac ssubst 1);
@@ -225,15 +217,13 @@
qed "wf_on_rmult";
-Goal
- "[| wf(r); wf(s) |] ==> wf(rmult(field(r),r,field(s),s))";
+Goal "[| wf(r); wf(s) |] ==> wf(rmult(field(r),r,field(s),s))";
by (asm_full_simp_tac (simpset() addsimps [wf_iff_wf_on_field]) 1);
by (rtac (field_rmult RSN (2, wf_on_subset_A)) 1);
by (REPEAT (ares_tac [wf_on_rmult] 1));
qed "wf_rmult";
-Goal
- "[| well_ord(A,r); well_ord(B,s) |] ==> \
+Goal "[| well_ord(A,r); well_ord(B,s) |] ==> \
\ well_ord(A*B, rmult(A,r,B,s))";
by (rtac well_ordI 1);
by (asm_full_simp_tac (simpset() addsimps [well_ord_def, wf_on_rmult]) 1);
@@ -244,8 +234,7 @@
(** An ord_iso congruence law **)
-Goal
- "[| f: bij(A,C); g: bij(B,D) |] ==> \
+Goal "[| f: bij(A,C); g: bij(B,D) |] ==> \
\ (lam <x,y>:A*B. <f`x, g`y>) : bij(A*B, C*D)";
by (res_inst_tac [("d", "%<x,y>. <converse(f)`x, converse(g)`y>")]
lam_bijective 1);
@@ -271,8 +260,7 @@
qed "singleton_prod_bij";
(*Used??*)
-Goal
- "well_ord({x},xr) ==> \
+Goal "well_ord({x},xr) ==> \
\ (lam z:A. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))";
by (resolve_tac [singleton_prod_bij RS ord_isoI] 1);
by (Asm_simp_tac 1);
@@ -281,8 +269,7 @@
(*Here we build a complicated function term, then simplify it using
case_cong, id_conv, comp_lam, case_case.*)
-Goal
- "a~:C ==> \
+Goal "a~:C ==> \
\ (lam x:C*B + D. case(%x. x, %y.<a,y>, x)) \
\ : bij(C*B + D, C*B Un {a}*D)";
by (rtac subst_elem 1);
@@ -296,8 +283,7 @@
by (asm_simp_tac (simpset() addsimps [case_case]) 1);
qed "prod_sum_singleton_bij";
-Goal
- "[| a:A; well_ord(A,r) |] ==> \
+Goal "[| a:A; well_ord(A,r) |] ==> \
\ (lam x:pred(A,a,r)*B + pred(B,b,s). case(%x. x, %y.<a,y>, x)) \
\ : ord_iso(pred(A,a,r)*B + pred(B,b,s), \
\ radd(A*B, rmult(A,r,B,s), B, s), \
@@ -313,8 +299,7 @@
(** Distributive law **)
-Goal
- "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
+Goal "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
\ : bij((A+B)*C, (A*C)+(B*C))";
by (res_inst_tac
[("d", "case(%<x,y>.<Inl(x),y>, %<x,y>.<Inr(x),y>)")] lam_bijective 1);
@@ -322,8 +307,7 @@
by (ALLGOALS Asm_simp_tac);
qed "sum_prod_distrib_bij";
-Goal
- "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
+Goal "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
\ : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), \
\ (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))";
by (resolve_tac [sum_prod_distrib_bij RS ord_isoI] 1);
@@ -333,14 +317,12 @@
(** Associativity **)
-Goal
- "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))";
+Goal "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))";
by (res_inst_tac [("d", "%<x, <y,z>>. <<x,y>, z>")] lam_bijective 1);
by (ALLGOALS (asm_simp_tac (simpset() setloop etac SigmaE)));
qed "prod_assoc_bij";
-Goal
- "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) \
+Goal "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) \
\ : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t), \
\ A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))";
by (resolve_tac [prod_assoc_bij RS ord_isoI] 1);
@@ -409,8 +391,7 @@
(** Well-foundedness **)
-Goal
- "[| f: A->B; wf[B](r) |] ==> wf[A](rvimage(A,f,r))";
+Goal "[| f: A->B; wf[B](r) |] ==> wf[A](rvimage(A,f,r))";
by (rtac wf_onI2 1);
by (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba" 1);
by (Blast_tac 1);
@@ -421,8 +402,7 @@
qed "wf_on_rvimage";
(*Note that we need only wf[A](...) and linear(A,...) to get the result!*)
-Goal
- "[| f: inj(A,B); well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))";
+Goal "[| f: inj(A,B); well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))";
by (rtac well_ordI 1);
by (rewrite_goals_tac [well_ord_def, tot_ord_def]);
by (blast_tac (claset() addSIs [wf_on_rvimage, inj_is_fun]) 1);
--- a/src/ZF/OrderType.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/OrderType.ML Thu Aug 06 12:24:04 1998 +0200
@@ -19,7 +19,7 @@
by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
by (resolve_tac [prem RS ltE] 1);
by (asm_simp_tac (simpset() addsimps [linear_def, Memrel_iff,
- [ltI, prem] MRS lt_trans2 RS ltD]) 1);
+ [ltI, prem] MRS lt_trans2 RS ltD]) 1);
by (REPEAT (resolve_tac [ballI, Ord_linear] 1));
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
qed "le_well_ord_Memrel";
@@ -40,8 +40,7 @@
by (Blast_tac 1);
qed "pred_Memrel";
-Goal
- "[| j<i; f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R";
+Goal "[| j<i; f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R";
by (forward_tac [lt_pred_Memrel] 1);
by (etac ltE 1);
by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN
@@ -53,8 +52,7 @@
qed "Ord_iso_implies_eq_lemma";
(*Kunen's Theorem 7.3 (ii), page 16. Isomorphic ordinals are equal*)
-Goal
- "[| Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) \
+Goal "[| Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) \
\ |] ==> i=j";
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
by (REPEAT (eresolve_tac [asm_rl, ord_iso_sym, Ord_iso_implies_eq_lemma] 1));
@@ -84,8 +82,7 @@
qed "ordermap_eq_image";
(*Useful for rewriting PROVIDED pred is not unfolded until later!*)
-Goal
- "[| wf[A](r); x:A |] ==> \
+Goal "[| wf[A](r); x:A |] ==> \
\ ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
by (asm_simp_tac (simpset() addsimps [ordermap_eq_image, pred_subset,
ordermap_type RS image_fun]) 1);
@@ -127,8 +124,7 @@
(*** ordermap preserves the orderings in both directions ***)
-Goal
- "[| <w,x>: r; wf[A](r); w: A; x: A |] ==> \
+Goal "[| <w,x>: r; wf[A](r); w: A; x: A |] ==> \
\ ordermap(A,r)`w : ordermap(A,r)`x";
by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
by (assume_tac 1);
@@ -171,8 +167,7 @@
by (blast_tac (claset() addSDs [converse_ordermap_mono]) 1);
qed "ordertype_ord_iso";
-Goal
- "[| f: ord_iso(A,r,B,s); well_ord(B,s) |] ==> \
+Goal "[| f: ord_iso(A,r,B,s); well_ord(B,s) |] ==> \
\ ordertype(A,r) = ordertype(B,s)";
by (forward_tac [well_ord_ord_iso] 1 THEN assume_tac 1);
by (rtac Ord_iso_implies_eq 1
@@ -181,8 +176,7 @@
addSEs [ordertype_ord_iso]) 0 1);
qed "ordertype_eq";
-Goal
- "[| ordertype(A,r) = ordertype(B,s); \
+Goal "[| ordertype(A,r) = ordertype(B,s); \
\ well_ord(A,r); well_ord(B,s) \
\ |] ==> EX f. f: ord_iso(A,r,B,s)";
by (rtac exI 1);
@@ -225,8 +219,7 @@
(*** A fundamental unfolding law for ordertype. ***)
(*Ordermap returns the same result if applied to an initial segment*)
-Goal
- "[| well_ord(A,r); y:A; z: pred(A,y,r) |] ==> \
+Goal "[| well_ord(A,r); y:A; z: pred(A,y,r) |] ==> \
\ ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z";
by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1);
by (wf_on_ind_tac "z" [] 1);
@@ -248,8 +241,7 @@
(** Theorems by Krzysztof Grabczewski; proofs simplified by lcp **)
-Goal
- "[| well_ord(A,r); x:A |] ==> \
+Goal "[| well_ord(A,r); x:A |] ==> \
\ ordertype(pred(A,x,r),r) <= ordertype(A,r)";
by (asm_simp_tac (simpset() addsimps [ordertype_unfold,
pred_subset RSN (2, well_ord_subset)]) 1);
@@ -257,8 +249,7 @@
addEs [predE]) 1);
qed "ordertype_pred_subset";
-Goal
- "[| well_ord(A,r); x:A |] ==> \
+Goal "[| well_ord(A,r); x:A |] ==> \
\ ordertype(pred(A,x,r),r) < ordertype(A,r)";
by (resolve_tac [ordertype_pred_subset RS subset_imp_le RS leE] 1);
by (REPEAT (ares_tac [Ord_ordertype, well_ord_subset, pred_subset] 1));
@@ -269,8 +260,7 @@
(*May rewrite with this -- provided no rules are supplied for proving that
well_ord(pred(A,x,r), r) *)
-Goal
- "well_ord(A,r) ==> \
+Goal "well_ord(A,r) ==> \
\ ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}";
by (rtac equalityI 1);
by (safe_tac (claset() addSIs [ordertype_pred_lt RS ltD]));
@@ -316,8 +306,7 @@
by (ALLGOALS Asm_simp_tac);
qed "bij_sum_0";
-Goal
- "well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)";
+Goal "well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)";
by (resolve_tac [bij_sum_0 RS ord_isoI RS ordertype_eq] 1);
by (assume_tac 2);
by (fast_tac (claset() addss (simpset() addsimps [radd_Inl_iff, Memrel_iff])) 1);
@@ -329,8 +318,7 @@
by (ALLGOALS Asm_simp_tac);
qed "bij_0_sum";
-Goal
- "well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)";
+Goal "well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)";
by (resolve_tac [bij_0_sum RS ord_isoI RS ordertype_eq] 1);
by (assume_tac 2);
by (fast_tac (claset() addss (simpset() addsimps [radd_Inr_iff, Memrel_iff])) 1);
@@ -350,8 +338,7 @@
(simpset() addsimps [radd_Inl_iff, radd_Inr_Inl_iff])));
qed "pred_Inl_bij";
-Goal
- "[| a:A; well_ord(A,r) |] ==> \
+Goal "[| a:A; well_ord(A,r) |] ==> \
\ ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) = \
\ ordertype(pred(A,a,r), r)";
by (resolve_tac [pred_Inl_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
@@ -368,8 +355,7 @@
by (ALLGOALS (Asm_full_simp_tac));
qed "pred_Inr_bij";
-Goal
- "[| b:B; well_ord(A,r); well_ord(B,s) |] ==> \
+Goal "[| b:B; well_ord(A,r); well_ord(B,s) |] ==> \
\ ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) = \
\ ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))";
by (resolve_tac [pred_Inr_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
@@ -421,15 +407,13 @@
(** A couple of strange but necessary results! **)
-Goal
- "A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))";
+Goal "A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))";
by (resolve_tac [id_bij RS ord_isoI] 1);
by (asm_simp_tac (simpset() addsimps [id_conv, Memrel_iff]) 1);
by (Blast_tac 1);
qed "id_ord_iso_Memrel";
-Goal
- "[| well_ord(A,r); k<j |] ==> \
+Goal "[| well_ord(A,r); k<j |] ==> \
\ ordertype(A+k, radd(A, r, k, Memrel(j))) = \
\ ordertype(A+k, radd(A, r, k, Memrel(k)))";
by (etac ltE 1);
@@ -450,21 +434,18 @@
ordertype_sum_Memrel]) 1);
qed "oadd_lt_mono2";
-Goal
- "[| i++j < i++k; Ord(i); Ord(j); Ord(k) |] ==> j<k";
+Goal "[| i++j < i++k; Ord(i); Ord(j); Ord(k) |] ==> j<k";
by (rtac Ord_linear_lt 1);
by (REPEAT_SOME assume_tac);
by (ALLGOALS
(blast_tac (claset() addDs [oadd_lt_mono2] addEs [lt_irrefl, lt_asym])));
qed "oadd_lt_cancel2";
-Goal
- "[| Ord(i); Ord(j); Ord(k) |] ==> i++j < i++k <-> j<k";
+Goal "[| Ord(i); Ord(j); Ord(k) |] ==> i++j < i++k <-> j<k";
by (blast_tac (claset() addSIs [oadd_lt_mono2] addSDs [oadd_lt_cancel2]) 1);
qed "oadd_lt_iff2";
-Goal
- "[| i++j = i++k; Ord(i); Ord(j); Ord(k) |] ==> j=k";
+Goal "[| i++j = i++k; Ord(i); Ord(j); Ord(k) |] ==> j=k";
by (rtac Ord_linear_lt 1);
by (REPEAT_SOME assume_tac);
by (ALLGOALS
@@ -502,8 +483,7 @@
by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1));
qed "oadd_assoc";
-Goal
- "[| Ord(i); Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})";
+Goal "[| Ord(i); Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})";
by (rtac (subsetI RS equalityI) 1);
by (eresolve_tac [ltI RS lt_oadd_disj RS disjE] 1);
by (REPEAT (ares_tac [Ord_oadd] 1));
@@ -518,8 +498,7 @@
by (Blast_tac 1);
qed "oadd_1";
-Goal
- "[| Ord(i); Ord(j) |] ==> i++succ(j) = succ(i++j)";
+Goal "[| Ord(i); Ord(j) |] ==> i++succ(j) = succ(i++j)";
(*ZF_ss prevents looping*)
by (asm_simp_tac (ZF_ss addsimps [Ord_oadd, oadd_1 RS sym]) 1);
by (asm_simp_tac (simpset() addsimps [oadd_1, oadd_assoc, Ord_1]) 1);
@@ -528,16 +507,15 @@
(** Ordinal addition with limit ordinals **)
-val prems = goal OrderType.thy
- "[| Ord(i); !!x. x:A ==> Ord(j(x)); a:A |] ==> \
-\ i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
+val prems =
+Goal "[| Ord(i); !!x. x:A ==> Ord(j(x)); a:A |] ==> \
+\ i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
by (blast_tac (claset() addIs (prems @ [ltI, Ord_UN, Ord_oadd,
lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD])
addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1);
qed "oadd_UN";
-Goal
- "[| Ord(i); Limit(j) |] ==> i++j = (UN k:j. i++k)";
+Goal "[| Ord(i); Limit(j) |] ==> i++j = (UN k:j. i++k)";
by (forward_tac [Limit_has_0 RS ltD] 1);
by (asm_simp_tac (simpset() addsimps [Limit_is_Ord RS Ord_in_Ord,
oadd_UN RS sym, Union_eq_UN RS sym,
@@ -579,8 +557,7 @@
by (asm_simp_tac (simpset() addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1);
qed "oadd_le_mono";
-Goal
- "[| Ord(i); Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k";
+Goal "[| Ord(i); Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k";
by (asm_simp_tac (simpset() addsimps [oadd_lt_iff2, oadd_succ RS sym,
Ord_succ]) 1);
qed "oadd_le_iff2";
@@ -590,8 +567,7 @@
Probably simpler to define the difference recursively!
**)
-Goal
- "A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
+Goal "A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1);
by (blast_tac (claset() addSIs [if_type]) 1);
by (fast_tac (claset() addSIs [case_type]) 1);
@@ -599,8 +575,7 @@
by (ALLGOALS Asm_simp_tac);
qed "bij_sum_Diff";
-Goal
- "i le j ==> \
+Goal "i le j ==> \
\ ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) = \
\ ordertype(j, Memrel(j))";
by (safe_tac (claset() addSDs [le_subset_iff RS iffD1]));
@@ -615,8 +590,8 @@
qed "ordertype_sum_Diff";
Goalw [oadd_def, odiff_def]
- "i le j ==> \
-\ i ++ (j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))";
+ "i le j \
+\ ==> i ++ (j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))";
by (safe_tac (claset() addSDs [le_subset_iff RS iffD1]));
by (resolve_tac [sum_ord_iso_cong RS ordertype_eq] 1);
by (etac id_ord_iso_Memrel 1);
@@ -638,8 +613,7 @@
(*By oadd_inject, the difference between i and j is unique. Note that we get
i++j = k ==> j = k--i. *)
-Goal
- "[| Ord(i); Ord(j) |] ==> (i++j) -- i = j";
+Goal "[| Ord(i); Ord(j) |] ==> (i++j) -- i = j";
by (rtac oadd_inject 1);
by (REPEAT (ares_tac [Ord_ordertype, Ord_oadd, Ord_odiff] 2));
by (asm_simp_tac (simpset() addsimps [oadd_odiff_inverse, oadd_le_self]) 1);
@@ -650,7 +624,7 @@
by (rtac (k_le_i RS lt_Ord RSN (2,oadd_lt_cancel2)) 1);
by (simp_tac
(simpset() addsimps [i_lt_j, k_le_i, [k_le_i, leI] MRS le_trans,
- oadd_odiff_inverse]) 1);
+ oadd_odiff_inverse]) 1);
by (REPEAT (resolve_tac (Ord_odiff ::
([i_lt_j, k_le_i] RL [lt_Ord, lt_Ord2])) 1));
qed "odiff_lt_mono2";
@@ -675,8 +649,7 @@
by (ALLGOALS (Blast_tac));
qed "pred_Pair_eq";
-Goal
- "[| a:A; b:B; well_ord(A,r); well_ord(B,s) |] ==> \
+Goal "[| a:A; b:B; well_ord(A,r); well_ord(B,s) |] ==> \
\ ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) = \
\ ordertype(pred(A,a,r)*B + pred(B,b,s), \
\ radd(A*B, rmult(A,r,B,s), B, s))";
@@ -733,8 +706,7 @@
symmetric omult_def]) 1);
qed "omult_oadd_lt";
-Goal
- "[| Ord(i); Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})";
+Goal "[| Ord(i); Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})";
by (rtac (subsetI RS equalityI) 1);
by (resolve_tac [lt_omult RS exE] 1);
by (etac ltI 3);
@@ -818,15 +790,14 @@
(** Ordinal multiplication with limit ordinals **)
-val prems = goal OrderType.thy
- "[| Ord(i); !!x. x:A ==> Ord(j(x)) |] ==> \
-\ i ** (UN x:A. j(x)) = (UN x:A. i**j(x))";
+val prems =
+Goal "[| Ord(i); !!x. x:A ==> Ord(j(x)) |] ==> \
+\ i ** (UN x:A. j(x)) = (UN x:A. i**j(x))";
by (asm_simp_tac (simpset() addsimps (prems@[Ord_UN, omult_unfold])) 1);
by (Blast_tac 1);
qed "omult_UN";
-Goal
- "[| Ord(i); Limit(j) |] ==> i**j = (UN k:j. i**k)";
+Goal "[| Ord(i); Limit(j) |] ==> i**j = (UN k:j. i**k)";
by (asm_simp_tac
(simpset() addsimps [Limit_is_Ord RS Ord_in_Ord, omult_UN RS sym,
Union_eq_UN RS sym, Limit_Union_eq]) 1);
--- a/src/ZF/Perm.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/Perm.ML Thu Aug 06 12:24:04 1998 +0200
@@ -167,13 +167,11 @@
(** Equations for converse(f) **)
(*The premises are equivalent to saying that f is injective...*)
-Goal
- "[| f: A->B; converse(f): C->A; a: A |] ==> converse(f)`(f`a) = a";
+Goal "[| f: A->B; converse(f): C->A; a: A |] ==> converse(f)`(f`a) = a";
by (blast_tac (claset() addIs [apply_Pair, apply_equality, converseI]) 1);
qed "left_inverse_lemma";
-Goal
- "[| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a";
+Goal "[| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a";
by (blast_tac (claset() addIs [left_inverse_lemma, inj_converse_fun,
inj_is_fun]) 1);
qed "left_inverse";
@@ -390,8 +388,7 @@
by (blast_tac (claset() addSIs [comp_fun_apply RS sym, apply_funtype]) 1);
qed "comp_mem_surjD1";
-Goal
- "[| (f O g)`a = c; g: A->B; f: B->C; a:A |] ==> f`(g`a) = c";
+Goal "[| (f O g)`a = c; g: A->B; f: B->C; a:A |] ==> f`(g`a) = c";
by (REPEAT (ares_tac [comp_fun_apply RS sym RS trans] 1));
qed "comp_fun_applyD";
@@ -459,8 +456,7 @@
(** Unions of functions -- cf similar theorems on func.ML **)
(*Theorem by KG, proof by LCP*)
-Goal
- "[| f: inj(A,B); g: inj(C,D); B Int D = 0 |] ==> \
+Goal "[| f: inj(A,B); g: inj(C,D); B Int D = 0 |] ==> \
\ (lam a: A Un C. if(a:A, f`a, g`a)) : inj(A Un C, B Un D)";
by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, converse(g)`z)")]
lam_injective 1);
@@ -479,8 +475,7 @@
(*A simple, high-level proof; the version for injections follows from it,
using f:inj(A,B) <-> f:bij(A,range(f)) *)
-Goal
- "[| f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 |] ==> \
+Goal "[| f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 |] ==> \
\ (f Un g) : bij(A Un C, B Un D)";
by (rtac invertible_imp_bijective 1);
by (stac converse_Un 1);
--- a/src/ZF/QPair.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/QPair.ML Thu Aug 06 12:24:04 1998 +0200
@@ -273,8 +273,7 @@
(** <+> is itself injective... who cares?? **)
-Goal
- "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))";
+Goal "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))";
by (Blast_tac 1);
qed "qsum_iff";
--- a/src/ZF/QUniv.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/QUniv.ML Thu Aug 06 12:24:04 1998 +0200
@@ -221,9 +221,7 @@
bind_thm ("QPair_Int_Vset_subset_trans",
[Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] MRS subset_trans);
-Goal
- "[| Ord(i) \
-\ |] ==> <a;b> Int Vset(i) <= (UN j:i. <a Int Vset(j); b Int Vset(j)>)";
+Goal "Ord(i) ==> <a;b> Int Vset(i) <= (UN j:i. <a Int Vset(j); b Int Vset(j)>)";
by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
(*0 case*)
by (stac Vfrom_0 1);
@@ -232,6 +230,7 @@
by (rtac (Transset_0 RS QPair_Int_Vfrom_succ_subset RS subset_trans) 1);
by (rtac (succI1 RS UN_upper) 1);
(*Limit(i) case*)
-by (asm_simp_tac (simpset() addsimps [Limit_Vfrom_eq, Int_UN_distrib, subset_refl,
- UN_mono, QPair_Int_Vset_subset_trans]) 1);
+by (asm_simp_tac
+ (simpset() addsimps [Limit_Vfrom_eq, Int_UN_distrib, subset_refl,
+ UN_mono, QPair_Int_Vset_subset_trans]) 1);
qed "QPair_Int_Vset_subset_UN";
--- a/src/ZF/Resid/Conversion.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/Resid/Conversion.ML Thu Aug 06 12:24:04 1998 +0200
@@ -9,8 +9,7 @@
AddIs (Sconv.intrs @ Sconv1.intrs);
-Goal
- "!!u. m<--->n ==> n<--->m";
+Goal "m<--->n ==> n<--->m";
by (etac Sconv.induct 1);
by (etac Sconv1.induct 1);
by (ALLGOALS Blast_tac);
@@ -20,8 +19,7 @@
(* Church_Rosser Theorem *)
(* ------------------------------------------------------------------------- *)
-Goal
- "!!u. m<--->n ==> EX p.(m --->p) & (n ---> p)";
+Goal "m<--->n ==> EX p.(m --->p) & (n ---> p)";
by (etac Sconv.induct 1);
by (etac Sconv1.induct 1);
by (blast_tac (claset() addIs [red1D1,redD2]) 1);
--- a/src/ZF/Resid/Residuals.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/Resid/Residuals.ML Thu Aug 06 12:24:04 1998 +0200
@@ -93,8 +93,7 @@
by (fast_tac resfunc_cs 1);
qed "res_redex";
-Goal
- "[|s~t; regular(t)|]==> regular(t) --> s |> t:redexes";
+Goal "[|s~t; regular(t)|]==> regular(t) --> s |> t:redexes";
by (etac Scomp.induct 1);
by (ALLGOALS (asm_full_simp_tac
(simpset() addsimps [res_Var,res_Fun,res_App,res_redex]
--- a/src/ZF/Resid/Substitution.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/Resid/Substitution.ML Thu Aug 06 12:24:04 1998 +0200
@@ -112,8 +112,7 @@
addsimps [lift_rec_Var,subst_Var]);
-Goal
- "u:redexes ==> ALL k:nat. lift_rec(u,k):redexes";
+Goal "u:redexes ==> ALL k:nat. lift_rec(u,k):redexes";
by (eresolve_tac [redexes.induct] 1);
by (ALLGOALS(asm_full_simp_tac
((addsplit (simpset())) addsimps [lift_rec_Fun,lift_rec_App])));
@@ -209,8 +208,7 @@
by (asm_full_simp_tac (simpset()) 1);
qed "subst_rec_lift_rec";
-Goal
- "v:redexes ==> \
+Goal "v:redexes ==> \
\ ALL m:nat. ALL n:nat. ALL u:redexes. ALL w:redexes. m le n --> \
\ subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m)=\
\ subst_rec(w,subst_rec(u,v,m),n)";
--- a/src/ZF/Sum.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/Sum.ML Thu Aug 06 12:24:04 1998 +0200
@@ -151,8 +151,7 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
qed "case_type";
-Goal
- "u: A+B ==> \
+Goal "u: A+B ==> \
\ R(case(c,d,u)) <-> \
\ ((ALL x:A. u = Inl(x) --> R(c(x))) & \
\ (ALL y:B. u = Inr(y) --> R(d(y))))";
--- a/src/ZF/Univ.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/Univ.ML Thu Aug 06 12:24:04 1998 +0200
@@ -386,8 +386,7 @@
by (Blast_tac 1);
qed "Pow_in_Vfrom";
-Goal
- "[| a: Vfrom(A,i); Limit(i); Transset(A) |] ==> Pow(a) : Vfrom(A,i)";
+Goal "[| a: Vfrom(A,i); Limit(i); Transset(A) |] ==> Pow(a) : Vfrom(A,i)";
(*Blast_tac: PROOF FAILED*)
by (fast_tac (claset() addEs [Limit_VfromE]
addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1);
--- a/src/ZF/Zorn.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/Zorn.ML Thu Aug 06 12:24:04 1998 +0200
@@ -207,8 +207,7 @@
qed "Hausdorff_next_exists";
(*Lemma 4*)
-Goal
- "[| c: TFin(S,next); \
+Goal " [| c: TFin(S,next); \
\ ch: (PROD X: Pow(chain(S))-{0}. X); \
\ next: increasing(S); \
\ ALL X: Pow(S). next`X = \
--- a/src/ZF/ex/BT.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/ex/BT.ML Thu Aug 06 12:24:04 1998 +0200
@@ -50,8 +50,7 @@
by (Simp_tac 1);
qed "bt_rec_Lf";
-Goal
- "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
+Goal "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
by (simp_tac (rank_ss addsimps (bt.case_eqns @ [rank_Br1, rank_Br2])) 1);
qed "bt_rec_Br";
--- a/src/ZF/ex/Comb.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/ex/Comb.ML Thu Aug 06 12:24:04 1998 +0200
@@ -165,8 +165,7 @@
by (Blast_tac 1);
qed "S1_parcontractD";
-Goal
- "!!p q r. S#p#q =1=> r ==> (EX p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
+Goal "S#p#q =1=> r ==> (EX p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
by (blast_tac (claset() addSDs [S1_parcontractD]) 1);
qed "S2_parcontractD";
--- a/src/ZF/ex/Integ.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/ex/Integ.ML Thu Aug 06 12:24:04 1998 +0200
@@ -286,8 +286,7 @@
(** Congruence property for multiplication **)
-Goal
- "congruent2(intrel, %p1 p2. \
+Goal "congruent2(intrel, %p1 p2. \
\ split(%x1 y1. split(%x2 y2. \
\ intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
by (rtac (equiv_intrel RS congruent2_commuteI) 1);
--- a/src/ZF/ex/LList.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/ex/LList.ML Thu Aug 06 12:24:04 1998 +0200
@@ -43,8 +43,7 @@
AddSDs [qunivD];
AddSEs [Ord_in_Ord];
-Goal
- "Ord(i) ==> ALL l: llist(quniv(A)). l Int Vset(i) <= univ(eclose(A))";
+Goal "Ord(i) ==> ALL l: llist(quniv(A)). l Int Vset(i) <= univ(eclose(A))";
by (etac trans_induct 1);
by (rtac ballI 1);
by (etac llist.elim 1);
@@ -71,8 +70,7 @@
AddSEs [Ord_in_Ord, Pair_inject];
(*Lemma for proving finality. Unfold the lazy list; use induction hypothesis*)
-Goal
- "Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
+Goal "Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
by (etac trans_induct 1);
by (REPEAT (resolve_tac [allI, impI] 1));
by (etac lleq.elim 1);
@@ -155,8 +153,7 @@
(*Reasoning borrowed from lleq.ML; a similar proof works for all
"productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
-Goal
- "Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \
+Goal "Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \
\ univ(eclose(bool))";
by (etac trans_induct 1);
by (rtac ballI 1);
--- a/src/ZF/ex/Limit.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/ex/Limit.ML Thu Aug 06 12:24:04 1998 +0200
@@ -331,8 +331,7 @@
by (Asm_simp_tac 1);
qed "subchain_isub";
-Goal
- "[|dominate(D,X,Y); subchain(Y,X); islub(D,X,x); islub(D,Y,y); cpo(D); \
+Goal "[|dominate(D,X,Y); subchain(Y,X); islub(D,X,x); islub(D,Y,y); cpo(D); \
\ X:nat->set(D); Y:nat->set(D)|] ==> x = y";
by (blast_tac (claset() addIs [cpo_antisym, dominate_islub, islub_least,
subchain_isub, islub_isub, islub_in]) 1);
@@ -2156,8 +2155,7 @@
by (auto_tac (claset() addIs [exI,rho_projpair], simpset()));
qed "emb_rho_emb";
-Goal
- "[| emb_chain(DD,ee); n:nat |] ==> \
+Goal "[| emb_chain(DD,ee); n:nat |] ==> \
\ rho_proj(DD,ee,n) : cont(Dinf(DD,ee),DD`n)";
by (auto_tac (claset() addIs [rho_projpair,projpair_p_cont], simpset()));
qed "rho_proj_cont";
--- a/src/ZF/ex/ListN.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/ex/ListN.ML Thu Aug 06 12:24:04 1998 +0200
@@ -35,8 +35,7 @@
by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
qed "listn_mono";
-Goal
- "[| <n,l> : listn(A); <n',l'> : listn(A) |] ==> <n#+n', l@l'> : listn(A)";
+Goal "[| <n,l> : listn(A); <n',l'> : listn(A) |] ==> <n#+n', l@l'> : listn(A)";
by (etac listn.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps listn.intrs)));
qed "listn_append";
--- a/src/ZF/ex/Primrec.ML Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/ex/Primrec.ML Thu Aug 06 12:24:04 1998 +0200
@@ -257,8 +257,7 @@
(** COMP case **)
-Goal
- "fs : list({f: primrec . \
+Goal "fs : list({f: primrec . \
\ EX kf:nat. ALL l:list(nat). \
\ f`l < ack(kf, list_add(l))}) \
\ ==> EX k:nat. ALL l: list(nat). \