# HG changeset patch # User paulson # Date 902399044 -7200 # Node ID 59ef39008514b01fba4e755f2bf6fc5d2e887b93 # Parent 41a01176b9de492bde9fcc3d89250a01eba61c4d even more tidying of Goal commands diff -r 41a01176b9de -r 59ef39008514 src/ZF/AC/DC.ML --- 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. : R}); \ +Goal "[| XX = (UN n:nat. {f:n->X. ALL k:n. : R}); \ \ ALL n:nat. : \ \ {: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. : R}); \ +Goal "[| XX = (UN n:nat. {f:n->X. ALL k:n. : R}); \ \ ALL n:nat. : \ \ {: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. : R}); \ \ RR = {: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 : \ +Goal "[| ALL b : \ \ {: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. : R}); \ \ ALL b : \ \ {: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)); diff -r 41a01176b9de -r 59ef39008514 src/ZF/AC/HH.ML --- 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); diff -r 41a01176b9de -r 59ef39008514 src/ZF/AC/WO2_AC16.ML --- 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 \ +Goal "[| ALL g \ \ domain(uu(f, b, g, d)) eqpoll succ(m); \ \ ALL b 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"; diff -r 41a01176b9de -r 59ef39008514 src/ZF/Cardinal.ML --- 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 ~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 ~(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); diff -r 41a01176b9de -r 59ef39008514 src/ZF/Coind/ECR.ML --- 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; \ \ :ElabRel; ve_dom(ve) = te_dom(te); \ \ {.y:ve_dom(ve)}: \ \ Pow({} Un HasTyRel) |] ==> \ diff -r 41a01176b9de -r 59ef39008514 src/ZF/Coind/Types.ML --- 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); diff -r 41a01176b9de -r 59ef39008514 src/ZF/Epsilon.ML --- 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"; diff -r 41a01176b9de -r 59ef39008514 src/ZF/EquivClass.ML --- 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 |] ==> : r"; -by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1)); +Goal "[| r``{a} = r``{b}; equiv(A,r); b: A |] ==> : 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) ==> : r <-> r``{x} = r``{y} & x:A & y:A"; +Goal "equiv(A,r) ==> : 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} <-> : r"; +Goal "[| equiv(A,r); x: A; y: A |] ==> r``{x} = r``{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) |] ==> :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; : r |] ==> b(y,w) = b(z,w); \ \ !! y z w. [| w: A; : 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; : 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) \ diff -r 41a01176b9de -r 59ef39008514 src/ZF/Finite.ML --- 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"; diff -r 41a01176b9de -r 59ef39008514 src/ZF/IMP/Equiv.ML --- 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-> 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-> 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-> snd(io)}"; +Goal "ALL c:com. C(c) = {io:(loc->nat)*(loc->nat). -c-> snd(io)}"; by (fast_tac (claset() addIs [C_subset RS subsetD] addEs [com2 RS bspec] addDs [com1] diff -r 41a01176b9de -r 59ef39008514 src/ZF/Order.ML --- 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; \ \ :r ==> P; x=y ==> P; :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; :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 |] ==> : r <-> : 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); : r; \ +Goal "[| well_ord(A,r); well_ord(B,s); : 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 |] ==> : 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 |] \ \ ==> ~ : 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))"; diff -r 41a01176b9de -r 59ef39008514 src/ZF/OrderArith.ML --- 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] "[| : 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); : 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 "[| <, > : rmult(A,r,B,s); \ \ [| : r; a':A; a:A; b':B; b:B |] ==> Q; \ \ [| : 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 :A*B. ) : bij(A*B, C*D)"; by (res_inst_tac [("d", "%. ")] 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. ) : 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., 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., 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 :(A+B)*C. case(%y. Inl(), %y. Inr(), x)) \ +Goal "(lam :(A+B)*C. case(%y. Inl(), %y. Inr(), x)) \ \ : bij((A+B)*C, (A*C)+(B*C))"; by (res_inst_tac [("d", "case(%., %.)")] lam_bijective 1); @@ -322,8 +307,7 @@ by (ALLGOALS Asm_simp_tac); qed "sum_prod_distrib_bij"; -Goal - "(lam :(A+B)*C. case(%y. Inl(), %y. Inr(), x)) \ +Goal "(lam :(A+B)*C. case(%y. Inl(), %y. Inr(), 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 <, z>:(A*B)*C. >) : bij((A*B)*C, A*(B*C))"; +Goal "(lam <, z>:(A*B)*C. >) : bij((A*B)*C, A*(B*C))"; by (res_inst_tac [("d", "%>. <, z>")] lam_bijective 1); by (ALLGOALS (asm_simp_tac (simpset() setloop etac SigmaE))); qed "prod_assoc_bij"; -Goal - "(lam <, z>:(A*B)*C. >) \ +Goal "(lam <, z>:(A*B)*C. >) \ \ : 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); diff -r 41a01176b9de -r 59ef39008514 src/ZF/OrderType.ML --- 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 R"; +Goal "[| 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 - "[| : r; wf[A](r); w: A; x: A |] ==> \ +Goal "[| : 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 \ +Goal "[| well_ord(A,r); k \ \ 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 j i++j < i++k <-> j i++j < i++k <-> j 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, , 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); diff -r 41a01176b9de -r 59ef39008514 src/ZF/Perm.ML --- 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); diff -r 41a01176b9de -r 59ef39008514 src/ZF/QPair.ML --- 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"; diff -r 41a01176b9de -r 59ef39008514 src/ZF/QUniv.ML --- 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) \ -\ |] ==> Int Vset(i) <= (UN j:i. )"; +Goal "Ord(i) ==> Int Vset(i) <= (UN j:i. )"; 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"; diff -r 41a01176b9de -r 59ef39008514 src/ZF/Resid/Conversion.ML --- 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); diff -r 41a01176b9de -r 59ef39008514 src/ZF/Resid/Residuals.ML --- 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] diff -r 41a01176b9de -r 59ef39008514 src/ZF/Resid/Substitution.ML --- 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)"; diff -r 41a01176b9de -r 59ef39008514 src/ZF/Sum.ML --- 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))))"; diff -r 41a01176b9de -r 59ef39008514 src/ZF/Univ.ML --- 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); diff -r 41a01176b9de -r 59ef39008514 src/ZF/Zorn.ML --- 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 = \ diff -r 41a01176b9de -r 59ef39008514 src/ZF/ex/BT.ML --- 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"; diff -r 41a01176b9de -r 59ef39008514 src/ZF/ex/Comb.ML --- 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"; diff -r 41a01176b9de -r 59ef39008514 src/ZF/ex/Integ.ML --- 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``{}, p2), p1))"; by (rtac (equiv_intrel RS congruent2_commuteI) 1); diff -r 41a01176b9de -r 59ef39008514 src/ZF/ex/LList.ML --- 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'. : lleq(A) --> l Int Vset(i) <= l'"; +Goal "Ord(i) ==> ALL 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); diff -r 41a01176b9de -r 59ef39008514 src/ZF/ex/Limit.ML --- 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"; diff -r 41a01176b9de -r 59ef39008514 src/ZF/ex/ListN.ML --- 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 - "[| : listn(A); : listn(A) |] ==> : listn(A)"; +Goal "[| : listn(A); : listn(A) |] ==> : listn(A)"; by (etac listn.induct 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps listn.intrs))); qed "listn_append"; diff -r 41a01176b9de -r 59ef39008514 src/ZF/ex/Primrec.ML --- 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). \