# HG changeset patch # User paulson # Date 900504798 -7200 # Node ID 8258771906189b6a37520fb11806137fd97a4cea # Parent 1ea751ae62b2116dcde715fb501bf6cea1c0bd83 More tidying and removal of "\!\!... from Goal commands diff -r 1ea751ae62b2 -r 825877190618 src/ZF/AC/AC10_AC15.ML --- a/src/ZF/AC/AC10_AC15.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/AC/AC10_AC15.ML Wed Jul 15 14:13:18 1998 +0200 @@ -49,14 +49,14 @@ val lemma1 = result(); Goalw [pairwise_disjoint_def] - "!!A. [| pairwise_disjoint(A); B:A; C:A; a:B; a:C |] ==> B=C"; + "[| pairwise_disjoint(A); B:A; C:A; a:B; a:C |] ==> B=C"; by (dtac IntI 1 THEN (assume_tac 1)); by (dres_inst_tac [("A","B Int C")] not_emptyI 1); by (Fast_tac 1); val lemma2 = result(); Goalw [sets_of_size_between_def] - "!!A. ALL B:{cons(0, x*nat). x:A}. pairwise_disjoint(f`B) & \ + "ALL B:{cons(0, x*nat). x:A}. pairwise_disjoint(f`B) & \ \ sets_of_size_between(f`B, 2, n) & Union(f`B)=B \ \ ==> ALL B:A. EX! u. u:f`cons(0, B*nat) & u <= cons(0, B*nat) & \ \ 0:u & 2 lepoll u & u lepoll n"; @@ -252,6 +252,6 @@ (* AC11 ==> AC14 *) (* ********************************************************************** *) -Goalw [AC11_def, AC14_def] "!!Z. AC11 ==> AC14"; +Goalw [AC11_def, AC14_def] "AC11 ==> AC14"; by (fast_tac (claset() addSIs [AC10_AC13]) 1); qed "AC11_AC14"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/AC/AC15_WO6.ML --- a/src/ZF/AC/AC15_WO6.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/AC/AC15_WO6.ML Wed Jul 15 14:13:18 1998 +0200 @@ -30,7 +30,7 @@ addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1); val lemma2 = result(); -Goalw [AC15_def, WO6_def] "!!Z. AC15 ==> WO6"; +Goalw [AC15_def, WO6_def] "AC15 ==> WO6"; by (rtac allI 1); by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1); by (etac impE 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/AC/AC16_WO4.ML --- a/src/ZF/AC/AC16_WO4.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/AC/AC16_WO4.ML Wed Jul 15 14:13:18 1998 +0200 @@ -39,7 +39,7 @@ qed "lepoll_trans1"; Goalw [lepoll_def] - "!!X.[| Y lepoll X; well_ord(X, R) |] ==> EX S. well_ord(Y, S)"; + "[| Y lepoll X; well_ord(X, R) |] ==> EX S. well_ord(Y, S)"; by (fast_tac (claset() addSEs [well_ord_rvimage]) 1); qed "well_ord_lepoll"; @@ -95,7 +95,7 @@ qed "succ_not_lepoll_lemma"; Goalw [lepoll_def, eqpoll_def, bij_def, surj_def] - "!!A. [| ~A eqpoll B; A lepoll B |] ==> succ(A) lepoll B"; + "[| ~A eqpoll B; A lepoll B |] ==> succ(A) lepoll B"; by (fast_tac (claset() addSEs [succ_not_lepoll_lemma, inj_is_fun]) 1); qed "succ_not_lepoll_imp_eqpoll"; @@ -116,7 +116,7 @@ (* ********************************************************************** *) Goalw [lepoll_def, eqpoll_def] - "!!X. [| n:nat; nat lepoll X |] ==> EX Y. Y<=X & n eqpoll Y"; + "[| n:nat; nat lepoll X |] ==> EX Y. Y<=X & n eqpoll Y"; by (fast_tac (FOL_cs addSDs [Ord_nat RSN (2, OrdmemD) RSN (2, restrict_inj)] addSIs [subset_refl] addSEs [restrict_bij, inj_is_fun RS fun_is_rel RS image_subset]) 1); @@ -170,7 +170,7 @@ qed "s_u_subset"; Goalw [s_u_def, succ_def] - "!!w. [| w:t_n; cons(b,cons(u,a)) <= w; a <= y; b : y-a; k eqpoll a \ + "[| w:t_n; cons(b,cons(u,a)) <= w; a <= y; b : y-a; k eqpoll a \ \ |] ==> w: s_u(u, t_n, succ(k), y)"; by (fast_tac (claset() addDs [eqpoll_imp_lepoll RS cons_lepoll_cong] addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1); @@ -181,7 +181,7 @@ qed "in_s_u_imp_u_in"; Goal - "!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \ + "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \ \ EX! w. w:t_n & z <= w; \ \ k eqpoll a; a <= y; b : y - a; u : x; x Int y = 0 |] \ \ ==> EX! c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c"; @@ -202,7 +202,7 @@ qed "ex1_superset_a"; Goal - "!!A. [| succ(k) eqpoll A; k eqpoll B; B <= A; a : A-B; k:nat \ + "[| succ(k) eqpoll A; k eqpoll B; B <= A; a : A-B; k:nat \ \ |] ==> A = cons(a, B)"; by (rtac equalityI 1); by (Fast_tac 2); @@ -220,7 +220,7 @@ qed "set_eq_cons"; Goal - "!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \ + "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \ \ EX! w. w:t_n & z <= w; \ \ ALL v:s_u(u, t_n, succ(k), y). succ(k) eqpoll v Int y; \ \ k eqpoll a; a <= y; b : y - a; u : x; x Int y = 0; k:nat \ @@ -249,7 +249,7 @@ (* ********************************************************************** *) Goal - "!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \ + "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \ \ EX! w. w:t_n & z <= w; \ \ ALL v:s_u(u, t_n, succ(k), y). succ(k) eqpoll v Int y; \ \ well_ord(y,R); ~Finite(y); k eqpoll a; a <= y; \ @@ -283,7 +283,7 @@ (* ********************************************************************** *) Goal - "!!k. [| k:nat; m:nat |] ==> \ + "[| k:nat; m:nat |] ==> \ \ ALL A B. A eqpoll k #+ m & k lepoll B & B<=A --> A-B lepoll m"; by (eres_inst_tac [("n","k")] nat_induct 1); by (simp_tac (simpset() addsimps [add_0]) 1); @@ -315,7 +315,7 @@ (* ********************************************************************** *) Goal - "!!k. [| k:nat; m:nat |] ==> \ + "[| k:nat; m:nat |] ==> \ \ ALL A B. A eqpoll k #+ m & k eqpoll B & B<=A --> A-B eqpoll m"; by (eres_inst_tac [("n","k")] nat_induct 1); by (fast_tac (claset() addSDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_0_is_0] @@ -371,7 +371,7 @@ qed "eqpoll_m_not_empty"; Goal - "!!z. [| z : xa Int (x - {u}); l eqpoll a; a <= y; x Int y = 0; u:x \ + "[| z : xa Int (x - {u}); l eqpoll a; a <= y; x Int y = 0; u:x \ \ |] ==> cons(z, cons(u, a)) : {v: Pow(x Un y). v eqpoll succ(succ(l))}"; by (fast_tac (claset() addSIs [cons_eqpoll_succ] addEs [equals0D, eqpoll_sym]) 1); qed "cons_cons_in"; @@ -382,7 +382,7 @@ (* ********************************************************************** *) Goal - "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(l))}. \ + "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(l))}. \ \ EX! w. w:t_n & z <= w; \ \ t_n <= {v:Pow(x Un y). v eqpoll succ(succ(l) #+ m)}; \ \ 0 LL(t_n, k, y) <= {z:Pow(y). z lepoll n}"; by (fast_tac (claset() addSEs [RepFunE] addIs [subset_imp_lepoll RS (eqpoll_imp_lepoll @@ -523,7 +523,7 @@ (* ********************************************************************** *) Goalw [MM_def, LL_def] - "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ + "[| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ \ v:LL(t_n, k, y) \ \ |] ==> EX! w. w:MM(t_n, k, y) & v<=w"; @@ -548,7 +548,7 @@ (* ********************************************************************** *) Goal - "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \ + "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \ \ EX! w. w:t_n & z <= w; \ \ well_ord(y,R); ~Finite(y); u:x; x Int y = 0; \ \ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ @@ -569,7 +569,7 @@ qed "MM_subset"; Goal - "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \ + "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \ \ EX! w. w:t_n & z <= w; \ \ well_ord(y,R); ~Finite(y); u:x; x Int y = 0; \ \ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ @@ -587,7 +587,7 @@ qed "exists_in_LL"; Goalw [LL_def] - "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ + "[| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ \ v : LL(t_n, k, y) |] \ \ ==> v = (THE x. x : MM(t_n, k, y) & v <= x) Int y"; @@ -596,7 +596,7 @@ qed "in_LL_eq_Int"; Goal - "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ + "[| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ \ v : LL(t_n, k, y) |] \ \ ==> (THE x. x : MM(t_n, k, y) & v <= x) <= x Un y"; @@ -605,7 +605,7 @@ qed "the_in_MM_subset"; Goalw [GG_def] - "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ + "[| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ \ t_n <= {v:Pow(x Un y). v eqpoll n}; \ \ v : LL(t_n, k, y) |] \ \ ==> GG(t_n, k, y) ` v <= x"; @@ -619,7 +619,7 @@ qed "GG_subset"; Goal - "!!x. [| well_ord(LL(t_n, succ(k), y), S); \ + "[| well_ord(LL(t_n, succ(k), y), S); \ \ ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. EX! w. w:t_n & z <= w; \ \ well_ord(y,R); ~Finite(y); x Int y = 0; \ \ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ @@ -648,18 +648,18 @@ (* ********************************************************************** *) Goalw [MM_def] - "!!w. [| w : MM(t_n, k, y); t_n <= {v:Pow(x Un y). v eqpoll n} \ + "[| w : MM(t_n, k, y); t_n <= {v:Pow(x Un y). v eqpoll n} \ \ |] ==> w eqpoll n"; by (Fast_tac 1); qed "in_MM_eqpoll_n"; Goalw [LL_def, MM_def] - "!!w. w : LL(t_n, k, y) ==> k lepoll w"; + "w : LL(t_n, k, y) ==> k lepoll w"; by (Fast_tac 1); qed "in_LL_eqpoll_n"; Goalw [GG_def] - "!!x. [| \ + "[| \ \ ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. EX! w. w:t_n & z <= w; \ \ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ \ well_ord(LL(t_n, succ(k), y), S); k:nat; m:nat |] \ @@ -686,7 +686,7 @@ (* ********************************************************************** *) Goalw [AC16_def,WO4_def] - "!!n k. [| AC16(k #+ m, k); 0 < k; 0 < m; k:nat; m:nat |] ==> WO4(m)"; + "[| AC16(k #+ m, k); 0 < k; 0 < m; k:nat; m:nat |] ==> WO4(m)"; by (rtac allI 1); by (excluded_middle_tac "Finite(A)" 1); by (rtac lemma1 2 THEN REPEAT (assume_tac 2)); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/AC/AC16_lemmas.ML --- a/src/ZF/AC/AC16_lemmas.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/AC/AC16_lemmas.ML Wed Jul 15 14:13:18 1998 +0200 @@ -27,8 +27,7 @@ by (fast_tac (claset() addSIs [singleton_eqpoll_1]) 1); qed "eqpoll_1_iff_singleton"; -Goalw [succ_def] - "!!x. [| x eqpoll n; y~:x |] ==> cons(y,x) eqpoll succ(n)"; +Goalw [succ_def] "[| x eqpoll n; y~:x |] ==> cons(y,x) eqpoll succ(n)"; by (fast_tac (claset() addSEs [cons_eqpoll_cong, mem_irrefl]) 1); qed "cons_eqpoll_succ"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/AC/AC18_AC19.ML --- a/src/ZF/AC/AC18_AC19.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/AC/AC18_AC19.ML Wed Jul 15 14:13:18 1998 +0200 @@ -56,7 +56,7 @@ (* ********************************************************************** *) Goalw [u_def] - "!!A. [| A ~= 0; 0 ~: A |] ==> {u_(a). a:A} ~= 0 & 0 ~: {u_(a). a:A}"; + "[| A ~= 0; 0 ~: A |] ==> {u_(a). a:A} ~= 0 & 0 ~: {u_(a). a:A}"; by (fast_tac (claset() addSIs [not_emptyI, RepFunI] addSEs [not_emptyE, RepFunE] addSDs [sym RS (RepFun_eq_0_iff RS iffD1)]) 1); @@ -74,7 +74,7 @@ val lemma1_1 = result(); Goalw [u_def] - "!!a. [| f`(u_(a)) ~: a; f: (PROD B:{u_(a). a:A}. B); a:A |] \ + "[| f`(u_(a)) ~: a; f: (PROD B:{u_(a). a:A}. B); a:A |] \ \ ==> f`(u_(a))-{0} : a"; by (fast_tac (claset() addSEs [RepFunI, RepFunE, lemma1_1] addSDs [apply_type]) 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/AC/AC1_WO2.ML --- a/src/ZF/AC/AC1_WO2.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/AC/AC1_WO2.ML Wed Jul 15 14:13:18 1998 +0200 @@ -17,7 +17,7 @@ by (fast_tac (claset() addSIs [prem RS Pi_weaken_type]) 1); val lemma1 = uresult() |> standard; -Goalw [AC1_def, WO2_def, eqpoll_def] "!!Z. AC1 ==> WO2"; +Goalw [AC1_def, WO2_def, eqpoll_def] "AC1 ==> WO2"; by (rtac allI 1); by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1); by (fast_tac (claset() addSDs [lemma1] addSIs [Ord_Least]) 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/AC/AC2_AC6.ML --- a/src/ZF/AC/AC2_AC6.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/AC/AC2_AC6.ML Wed Jul 15 14:13:18 1998 +0200 @@ -20,7 +20,7 @@ val lemma1 = result(); Goalw [pairwise_disjoint_def] - "!!A. [| pairwise_disjoint(A); B:A; C:A; D:B; D:C |] ==> f`B = f`C"; + "[| pairwise_disjoint(A); B:A; C:A; D:B; D:C |] ==> f`B = f`C"; by (fast_tac (claset() addSEs [equals0D]) 1); val lemma2 = result(); @@ -59,7 +59,7 @@ addSDs [bspec]) 1); val lemma3 = result(); -Goalw (AC_defs@AC_aux_defs) "!!Z. AC2 ==> AC1"; +Goalw (AC_defs@AC_aux_defs) "AC2 ==> AC1"; by (REPEAT (resolve_tac [allI, impI] 1)); by (REPEAT (eresolve_tac [allE, impE] 1)); by (fast_tac (claset() addSEs [lemma3]) 2); @@ -127,7 +127,7 @@ (* AC4 ==> AC5 *) (* ********************************************************************** *) -Goalw (range_def::AC_defs) "!!Z. AC4 ==> AC5"; +Goalw (range_def::AC_defs) "AC4 ==> AC5"; by (REPEAT (resolve_tac [allI,ballI] 1)); by (REPEAT (eresolve_tac [allE,impE] 1)); by (eresolve_tac [fun_is_rel RS converse_type] 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/AC/AC7_AC9.ML --- a/src/ZF/AC/AC7_AC9.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/AC/AC7_AC9.ML Wed Jul 15 14:13:18 1998 +0200 @@ -51,7 +51,7 @@ qed "lam_eqE"; Goalw [inj_def] - "!!A. C:A ==> (lam g:(nat->Union(A))*C. \ + "C:A ==> (lam g:(nat->Union(A))*C. \ \ (lam n:nat. if(n=0, snd(g), fst(g)`(n #- 1)))) \ \ : inj((nat->Union(A))*C, (nat->Union(A)) ) "; by (rtac CollectI 1); @@ -132,7 +132,7 @@ (* ********************************************************************** *) Goalw [eqpoll_def] - "!!A. ALL B:A. EX B1 B2. B= & B1 eqpoll B2 \ + "ALL B:A. EX B1 B2. B= & B1 eqpoll B2 \ \ ==> 0 ~: { bij(fst(B),snd(B)). B:A }"; by (rtac notI 1); by (etac RepFunE 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/AC/Cardinal_aux.ML --- a/src/ZF/AC/Cardinal_aux.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/AC/Cardinal_aux.ML Wed Jul 15 14:13:18 1998 +0200 @@ -196,7 +196,7 @@ qed "disj_Un_eqpoll_sum"; Goalw [lepoll_def, eqpoll_def] - "!!X a. a lepoll X ==> EX Y. Y<=X & a eqpoll Y"; + "a lepoll X ==> EX Y. Y<=X & a eqpoll Y"; by (etac exE 1); by (forward_tac [subset_refl RSN (2, restrict_bij)] 1); by (res_inst_tac [("x","f``a")] exI 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/AC/DC.ML --- a/src/ZF/AC/DC.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/AC/DC.ML Wed Jul 15 14:13:18 1998 +0200 @@ -101,7 +101,7 @@ val lemma1 = result(); Goal -"!!X.[| XX = (UN n:nat. {f:n->X. ALL k:n. : R}); \ +"[| 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}; \ @@ -137,7 +137,7 @@ val lemma2 = result(); Goal -"!!X.[| XX = (UN n:nat. {f:n->X. ALL k:n. : R}); \ +"[| 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}; \ @@ -191,7 +191,7 @@ by (fast_tac (claset() addSEs [apply_type]) 1); qed "fun_type_gen"; -Goalw [DC_def, DC0_def] "!!Z. DC0 ==> DC(nat)"; +Goalw [DC_def, DC0_def] "DC0 ==> DC(nat)"; by (REPEAT (resolve_tac [allI, impI] 1)); by (REPEAT (eresolve_tac [conjE, allE] 1)); by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1 @@ -242,7 +242,7 @@ ************************************************************************* *) Goalw [lesspoll_def, Finite_def] - "!!A. A lesspoll nat ==> Finite(A)"; + "A lesspoll nat ==> Finite(A)"; by (fast_tac (claset() addSDs [ltD, lepoll_imp_ex_le_eqpoll] addSIs [Ord_nat]) 1); qed "lesspoll_nat_is_Finite"; @@ -283,7 +283,7 @@ qed "singleton_in_funs"; Goal - "!!X. [| XX = (UN n:nat. \ + "[| 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)) | \ @@ -351,7 +351,7 @@ qed "f_n_pairs_in_R"; Goalw [restrict_def] - "!!f. [| restrict(f, domain(x))=x; f:n->X; domain(x) <= n \ + "[| restrict(f, domain(x))=x; f:n->X; domain(x) <= n \ \ |] ==> restrict(cons(, f), domain(x)) = x"; by (eresolve_tac [sym RS trans RS sym] 1); by (rtac fun_extension 1); @@ -376,7 +376,7 @@ qed "all_in_image_restrict_eq"; Goal -"!!X.[| ALL b : \ +"[| 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)) & \ @@ -456,7 +456,7 @@ val lemma2 = result(); Goal -"!!n. [| XX = (UN n:nat. \ +"[| 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)) \ @@ -478,7 +478,7 @@ val lemma3 = result(); -Goalw [DC_def, DC0_def] "!!Z. DC(nat) ==> DC0"; +Goalw [DC_def, DC0_def] "DC(nat) ==> DC0"; by (REPEAT (resolve_tac [allI, impI] 1)); by (REPEAT (eresolve_tac [asm_rl, conjE, ex_in_domain RS exE, allE] 1)); by (eresolve_tac [[refl, refl] MRS lemma4 RSN (2, impE)] 1 @@ -502,7 +502,7 @@ (* ********************************************************************** *) Goalw [lesspoll_def] - "!!A. [| ~ A lesspoll B; C lesspoll B |] ==> A - C ~= 0"; + "[| ~ A lesspoll B; C lesspoll B |] ==> A - C ~= 0"; by (fast_tac (claset() addSDs [Diff_eq_0_iff RS iffD1 RS subset_imp_lepoll] addSIs [eqpollI] addEs [notE] addSEs [eqpollE, lepoll_trans]) 1); val lesspoll_lemma = result(); @@ -523,7 +523,7 @@ qed "value_in_image"; Goalw [DC_def, WO3_def] - "!!Z. ALL K. Card(K) --> DC(K) ==> WO3"; + "ALL K. Card(K) --> DC(K) ==> WO3"; by (rtac allI 1); by (excluded_middle_tac "A lesspoll Hartog(A)" 1); by (fast_tac (claset() addSDs [lesspoll_imp_ex_lt_eqpoll] @@ -552,7 +552,7 @@ (* ********************************************************************** *) Goal - "!!a. [| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b"; + "[| 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)); @@ -598,7 +598,7 @@ val lemma = result(); Goalw [DC_def, WO1_def] - "!!Z. WO1 ==> ALL K. Card(K) --> DC(K)"; + "WO1 ==> ALL K. Card(K) --> DC(K)"; by (REPEAT (resolve_tac [allI,impI] 1)); by (REPEAT (eresolve_tac [allE,exE,conjE] 1)); by (res_inst_tac [("x","lam b:K. ff(b, X, Ra, R)")] bexI 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/AC/DC_lemmas.ML --- a/src/ZF/AC/DC_lemmas.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/AC/DC_lemmas.ML Wed Jul 15 14:13:18 1998 +0200 @@ -26,7 +26,7 @@ qed "n_lesspoll_nat"; Goalw [lepoll_def] - "!!f. [| f:X->Y; Ord(X) |] ==> f``X lepoll X"; + "[| f:X->Y; Ord(X) |] ==> f``X lepoll X"; by (res_inst_tac [("x","lam x:f``X. LEAST y. f`y = x")] exI 1); by (res_inst_tac [("d","%z. f`z")] lam_injective 1); by (fast_tac (claset() addSIs [Least_in_Ord, apply_equality]) 1); @@ -91,7 +91,7 @@ qed "succ_in_succ"; Goalw [restrict_def] - "!!f. [| restrict(f, domain(g)) = g; x: domain(g) |] ==> f`x = g`x"; + "[| restrict(f, domain(g)) = g; x: domain(g) |] ==> f`x = g`x"; by (etac subst 1); by (Asm_full_simp_tac 1); qed "restrict_eq_imp_val_eq"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/AC/HH.ML --- a/src/ZF/AC/HH.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/AC/HH.ML Wed Jul 15 14:13:18 1998 +0200 @@ -97,7 +97,7 @@ qed "HH_eq_imp_arg_eq"; Goalw [lepoll_def, inj_def] - "!!i. [| HH(f, x, i) : Pow(x)-{0}; Ord(i) |] ==> i lepoll Pow(x)-{0}"; + "[| HH(f, x, i) : Pow(x)-{0}; Ord(i) |] ==> i lepoll Pow(x)-{0}"; by (res_inst_tac [("x","lam j:i. HH(f, x, j)")] exI 1); by (Asm_simp_tac 1); by (fast_tac (FOL_cs addSEs [HH_eq_imp_arg_eq, Ord_in_Ord, HH_subset_x_lt_too] @@ -141,7 +141,7 @@ qed "lam_Least_HH_inj"; Goalw [surj_def] - "!!x. [| x - (UN a:A. F(a)) = 0; \ + "[| x - (UN a:A. F(a)) = 0; \ \ ALL a:A. EX z:x. F(a) = {z} |] \ \ ==> (lam a:A. F(a)) : surj(A, {{y}. y:x})"; by (asm_full_simp_tac (simpset() addsimps [lam_type, Diff_eq_0_iff]) 1); @@ -179,7 +179,7 @@ qed "HH_values2"; Goal - "!!f. HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j)))"; + "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); @@ -197,7 +197,7 @@ qed "f_sing_imp_HH_sing"; Goalw [bij_def] - "!!f. [| x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0; \ + "[| x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0; \ \ f : (Pow(x)-{0}) -> {{z}. z:x} |] \ \ ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \ \ : bij(LEAST i. HH(f,x,i)={x}, {{y}. y:x})"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/AC/WO1_AC.ML --- a/src/ZF/AC/WO1_AC.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/AC/WO1_AC.ML Wed Jul 15 14:13:18 1998 +0200 @@ -31,7 +31,7 @@ (* WO1 ==> AC1 *) (* ********************************************************************** *) -Goalw [AC1_def, WO1_def] "!!Z. WO1 ==> AC1"; +Goalw [AC1_def, WO1_def] "WO1 ==> AC1"; by (fast_tac (claset() addSEs [ex_choice_fun]) 1); qed "WO1_AC1"; @@ -79,7 +79,7 @@ val lemma = result(); Goalw AC_aux_defs - "!!f. f : bij(D+D, B) ==> \ + "f : bij(D+D, B) ==> \ \ pairwise_disjoint({{f`Inl(i), f`Inr(i)}. i:D})"; by (fast_tac (claset() addSEs [RepFunE, not_emptyE] addDs [bij_is_inj RS lemma, Inl_iff RS iffD1, @@ -92,7 +92,8 @@ "[| f : bij(D+D, B); 1 le n |] ==> \ \ sets_of_size_between({{f`Inl(i), f`Inr(i)}. i:D}, 2, succ(n))"; by (rewtac succ_def); -by (fast_tac (claset() addSIs [cons_lepoll_cong, minor, lepoll_refl, InlI, InrI] +by (fast_tac (claset() + addSIs [cons_lepoll_cong, minor, lepoll_refl, InlI, InrI] addIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans, le_imp_subset RS subset_imp_lepoll] addDs [major RS bij_is_inj RS lemma, Inl_Inr_iff RS iffD1 RS FalseE] @@ -100,7 +101,7 @@ val lemma2_4 = result(); Goalw [bij_def, surj_def] - "!!f. f : bij(D+D, B) ==> Union({{f`Inl(i), f`Inr(i)}. i:D})=B"; + "f : bij(D+D, B) ==> Union({{f`Inl(i), f`Inr(i)}. i:D})=B"; by (fast_tac (claset() addSEs [inj_is_fun RS apply_type]) 1); val lemma2_5 = result(); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/AC/WO1_WO6.ML --- a/src/ZF/AC/WO1_WO6.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/AC/WO1_WO6.ML Wed Jul 15 14:13:18 1998 +0200 @@ -19,14 +19,14 @@ (* ********************************************************************** *) -Goalw (eqpoll_def::WO_defs) "!!Z. WO3 ==> WO1"; +Goalw (eqpoll_def::WO_defs) "WO3 ==> WO1"; by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage, well_ord_Memrel RS well_ord_subset]) 1); qed "WO3_WO1"; (* ********************************************************************** *) -Goalw (eqpoll_def::WO_defs) "!!Z. WO1 ==> WO2"; +Goalw (eqpoll_def::WO_defs) "WO1 ==> WO2"; by (fast_tac (claset() addSIs [Ord_ordertype, ordermap_bij]) 1); qed "WO1_WO2"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Arith.ML --- a/src/ZF/Arith.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Arith.ML Wed Jul 15 14:13:18 1998 +0200 @@ -354,7 +354,7 @@ (*Type checking depends upon termination!*) Goalw [div_def] - "!!m n. [| 0 m div n : nat"; + "[| 0 m div n : nat"; by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1)); qed "div_type"; @@ -573,7 +573,7 @@ (*Thanks to Sten Agerholm*) Goal (* add_le_elim1 *) - "!!m n k. [|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k"; + "[|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k"; by (etac rev_mp 1); by (eres_inst_tac [("n","n")] nat_induct 1); by (Asm_simp_tac 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Cardinal.ML --- a/src/ZF/Cardinal.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Cardinal.ML Wed Jul 15 14:13:18 1998 +0200 @@ -109,7 +109,7 @@ by (blast_tac (claset() addIs [eqpollI] addSEs [eqpollE]) 1); qed "eqpoll_iff"; -Goalw [lepoll_def, inj_def] "!!A. A lepoll 0 ==> A = 0"; +Goalw [lepoll_def, inj_def] "A lepoll 0 ==> A = 0"; by (blast_tac (claset() addDs [apply_type]) 1); qed "lepoll_0_is_0"; @@ -303,7 +303,7 @@ by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1)); qed "CardI"; -Goalw [Card_def, cardinal_def] "!!i. Card(i) ==> Ord(i)"; +Goalw [Card_def, cardinal_def] "Card(i) ==> Ord(i)"; by (etac ssubst 1); by (rtac Ord_Least 1); qed "Card_is_Ord"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/CardinalArith.ML --- a/src/ZF/CardinalArith.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/CardinalArith.ML Wed Jul 15 14:13:18 1998 +0200 @@ -38,7 +38,7 @@ (*Unconditional version requires AC*) Goalw [cadd_def] - "!!i j k. [| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ==> \ + "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ==> \ \ (i |+| j) |+| k = i |+| (j |+| k)"; by (rtac cardinal_cong 1); by (rtac ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS sum_eqpoll_cong RS @@ -70,7 +70,7 @@ (*Could probably weaken the premises to well_ord(K,r), or removing using AC*) Goalw [cadd_def] - "!!K. [| Card(K); Ord(L) |] ==> K le (K |+| L)"; + "[| Card(K); Ord(L) |] ==> K le (K |+| L)"; by (rtac ([Card_cardinal_le, well_ord_lepoll_imp_Card_le] MRS le_trans) 1); by (rtac sum_lepoll_self 3); by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Card_is_Ord] 1)); @@ -79,7 +79,7 @@ (** Monotonicity of addition **) Goalw [lepoll_def] - "!!A B C D. [| A lepoll C; B lepoll D |] ==> A + B lepoll C + D"; + "[| A lepoll C; B lepoll D |] ==> A + B lepoll C + D"; by (REPEAT (etac exE 1)); by (res_inst_tac [("x", "lam z:A+B. case(%w. Inl(f`w), %y. Inr(fa`y), z)")] exI 1); @@ -92,7 +92,7 @@ qed "sum_lepoll_mono"; Goalw [cadd_def] - "!!K. [| K' le K; L' le L |] ==> (K' |+| L') le (K |+| L)"; + "[| K' le K; L' le L |] ==> (K' |+| L') le (K |+| L)"; by (safe_tac (claset() addSDs [le_subset_iff RS iffD1])); by (rtac well_ord_lepoll_imp_Card_le 1); by (REPEAT (ares_tac [sum_lepoll_mono, subset_imp_lepoll] 2)); @@ -114,7 +114,7 @@ (*Pulling the succ(...) outside the |...| requires m, n: nat *) (*Unconditional version requires AC*) Goalw [cadd_def] - "!!m n. [| Ord(m); Ord(n) |] ==> succ(m) |+| n = |succ(m |+| n)|"; + "[| Ord(m); Ord(n) |] ==> succ(m) |+| n = |succ(m |+| n)|"; by (rtac (sum_succ_eqpoll RS cardinal_cong RS trans) 1); by (rtac (succ_eqpoll_cong RS cardinal_cong) 1); by (rtac (well_ord_cardinal_eqpoll RS eqpoll_sym) 1); @@ -157,7 +157,7 @@ (*Unconditional version requires AC*) Goalw [cmult_def] - "!!i j k. [| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ==> \ + "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ==> \ \ (i |*| j) |*| k = i |*| (j |*| k)"; by (rtac cardinal_cong 1); by (rtac ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS prod_eqpoll_cong RS @@ -176,7 +176,7 @@ qed "sum_prod_distrib_eqpoll"; Goalw [cadd_def, cmult_def] - "!!i j k. [| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ==> \ + "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ==> \ \ (i |+| j) |*| k = (i |*| k) |+| (j |*| k)"; by (rtac cardinal_cong 1); by (rtac ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS prod_eqpoll_cong RS @@ -207,7 +207,7 @@ by (resolve_tac [singleton_prod_bij RS bij_converse_bij] 1); qed "prod_singleton_eqpoll"; -Goalw [cmult_def, succ_def] "!!K. Card(K) ==> 1 |*| K = K"; +Goalw [cmult_def, succ_def] "Card(K) ==> 1 |*| K = K"; by (asm_simp_tac (simpset() addsimps [prod_singleton_eqpoll RS cardinal_cong, Card_cardinal_eq]) 1); qed "cmult_1"; @@ -231,14 +231,14 @@ (** Multiplication by a non-zero cardinal **) -Goalw [lepoll_def, inj_def] "!!b. b: B ==> A lepoll A*B"; +Goalw [lepoll_def, inj_def] "b: B ==> A lepoll A*B"; by (res_inst_tac [("x", "lam x:A. ")] exI 1); by (asm_simp_tac (simpset() addsimps [lam_type]) 1); qed "prod_lepoll_self"; (*Could probably weaken the premises to well_ord(K,r), or removing using AC*) Goalw [cmult_def] - "!!K. [| Card(K); Ord(L); 0 K le (K |*| L)"; + "[| Card(K); Ord(L); 0 K le (K |*| L)"; by (rtac ([Card_cardinal_le, well_ord_lepoll_imp_Card_le] MRS le_trans) 1); by (rtac prod_lepoll_self 3); by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Card_is_Ord, ltD] 1)); @@ -247,7 +247,7 @@ (** Monotonicity of multiplication **) Goalw [lepoll_def] - "!!A B C D. [| A lepoll C; B lepoll D |] ==> A * B lepoll C * D"; + "[| A lepoll C; B lepoll D |] ==> A * B lepoll C * D"; by (REPEAT (etac exE 1)); by (res_inst_tac [("x", "lam :A*B. ")] exI 1); by (res_inst_tac [("d", "%.")] @@ -258,7 +258,7 @@ qed "prod_lepoll_mono"; Goalw [cmult_def] - "!!K. [| K' le K; L' le L |] ==> (K' |*| L') le (K |*| L)"; + "[| K' le K; L' le L |] ==> (K' |*| L') le (K |*| L)"; by (safe_tac (claset() addSDs [le_subset_iff RS iffD1])); by (rtac well_ord_lepoll_imp_Card_le 1); by (REPEAT (ares_tac [prod_lepoll_mono, subset_imp_lepoll] 2)); @@ -279,7 +279,7 @@ (*Unconditional version requires AC*) Goalw [cmult_def, cadd_def] - "!!m n. [| Ord(m); Ord(n) |] ==> succ(m) |*| n = n |+| (m |*| n)"; + "[| Ord(m); Ord(n) |] ==> succ(m) |*| n = n |+| (m |*| n)"; by (rtac (prod_succ_eqpoll RS cardinal_cong RS trans) 1); by (rtac (cardinal_cong RS sym) 1); by (rtac ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS sum_eqpoll_cong) 1); @@ -310,7 +310,7 @@ %y. if(y:nat, nat_case(u,%z.z,y), y). If f: inj(nat,A) then range(f) behaves like the natural numbers.*) Goalw [lepoll_def] - "!!i. nat lepoll A ==> cons(u,A) lepoll A"; + "nat lepoll A ==> cons(u,A) lepoll A"; by (etac exE 1); by (res_inst_tac [("x", "lam z:cons(u,A). if(z=u, f`0, \ @@ -347,7 +347,7 @@ qed "InfCard_is_Card"; Goalw [InfCard_def] - "!!K L. [| InfCard(K); Card(L) |] ==> InfCard(K Un L)"; + "[| InfCard(K); Card(L) |] ==> InfCard(K Un L)"; by (asm_simp_tac (simpset() addsimps [Card_Un, Un_upper1_le RSN (2,le_trans), Card_is_Ord]) 1); qed "InfCard_Un"; @@ -381,13 +381,13 @@ (** Establishing the well-ordering **) Goalw [inj_def] - "!!K. Ord(K) ==> (lam :K*K. ) : inj(K*K, K*K*K)"; + "Ord(K) ==> (lam :K*K. ) : inj(K*K, K*K*K)"; by (fast_tac (claset() addss (simpset()) addIs [lam_type, Un_least_lt RS ltD, ltI]) 1); qed "csquare_lam_inj"; Goalw [csquare_rel_def] - "!!K. Ord(K) ==> well_ord(K*K, csquare_rel(K))"; + "Ord(K) ==> well_ord(K*K, csquare_rel(K))"; by (rtac (csquare_lam_inj RS well_ord_rvimage) 1); by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1)); qed "well_ord_csquare"; @@ -395,7 +395,7 @@ (** Characterising initial segments of the well-ordering **) Goalw [csquare_rel_def] - "!!K. [| x \ + "[| x \ \ <, > : csquare_rel(K) --> x le z & y le z"; by (REPEAT (etac ltE 1)); by (asm_simp_tac (simpset() addsimps [rvimage_iff, rmult_iff, Memrel_iff, @@ -406,7 +406,7 @@ qed_spec_mp "csquareD"; Goalw [pred_def] - "!!K. z pred(K*K, , csquare_rel(K)) <= succ(z)*succ(z)"; + "z pred(K*K, , csquare_rel(K)) <= succ(z)*succ(z)"; by (safe_tac (claset_of ZF.thy addSEs [SigmaE])); (*avoids using succCI,...*) by (rtac (csquareD RS conjE) 1); by (rewtac lt_def); @@ -415,7 +415,7 @@ qed "pred_csquare_subset"; Goalw [csquare_rel_def] - "!!K. [| x <, > : csquare_rel(K)"; + "[| x <, > : csquare_rel(K)"; by (subgoals_tac ["x \ + "[| x le z; y le z; z \ \ <, > : csquare_rel(K) | x=z & y=z"; by (subgoals_tac ["x \ +Goal "[| Limit(K); x \ \ ordermap(K*K, csquare_rel(K)) ` < \ \ ordermap(K*K, csquare_rel(K)) ` "; by (subgoals_tac ["z: K*K has no more than z*z predecessors..." (page 29) *) Goalw [cmult_def] - "!!K. [| Limit(K); x \ + "[| Limit(K); x \ \ | ordermap(K*K, csquare_rel(K)) ` | le |succ(z)| |*| |succ(z)|"; by (rtac (well_ord_rmult RS well_ord_lepoll_imp_Card_le) 1); by (REPEAT (ares_tac [Ord_cardinal, well_ord_Memrel] 1)); @@ -475,8 +474,7 @@ qed "ordermap_csquare_le"; (*Kunen: "... so the order type <= K" *) -Goal - "!!K. [| InfCard(K); ALL y:K. InfCard(y) --> y |*| y = y |] ==> \ +Goal "[| InfCard(K); ALL y:K. InfCard(y) --> y |*| y = y |] ==> \ \ ordertype(K*K, csquare_rel(K)) le K"; by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1); by (rtac all_lt_imp_le 1); @@ -526,8 +524,7 @@ qed "InfCard_csquare_eq"; (*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*) -Goal - "!!A. [| well_ord(A,r); InfCard(|A|) |] ==> A*A eqpoll A"; +Goal "[| well_ord(A,r); InfCard(|A|) |] ==> A*A eqpoll A"; by (resolve_tac [prod_eqpoll_cong RS eqpoll_trans] 1); by (REPEAT (etac (well_ord_cardinal_eqpoll RS eqpoll_sym) 1)); by (rtac well_ord_cardinal_eqE 1); @@ -548,8 +545,7 @@ qed "InfCard_le_cmult_eq"; (*Corollary 10.13 (1), for cardinal multiplication*) -Goal - "!!K. [| InfCard(K); InfCard(L) |] ==> K |*| L = K Un L"; +Goal "[| InfCard(K); InfCard(L) |] ==> K |*| L = K Un L"; by (res_inst_tac [("i","K"),("j","L")] Ord_linear_le 1); by (typechk_tac [InfCard_is_Card, Card_is_Ord]); by (resolve_tac [cmult_commute RS ssubst] 1); @@ -579,8 +575,7 @@ by (asm_simp_tac (simpset() addsimps [InfCard_cdouble_eq]) 1); qed "InfCard_le_cadd_eq"; -Goal - "!!K. [| InfCard(K); InfCard(L) |] ==> K |+| L = K Un L"; +Goal "[| InfCard(K); InfCard(L) |] ==> K |+| L = K Un L"; by (res_inst_tac [("i","K"),("j","L")] Ord_linear_le 1); by (typechk_tac [InfCard_is_Card, Card_is_Ord]); by (resolve_tac [cadd_commute RS ssubst] 1); @@ -630,8 +625,7 @@ (*The proof by contradiction: the bijection f yields a wellordering of X whose ordertype is jump_cardinal(K). *) -Goal - "!!K. [| well_ord(X,r); r <= K * K; X <= K; \ +Goal "[| well_ord(X,r); r <= K * K; X <= K; \ \ f : bij(ordertype(X,r), jump_cardinal(K)) \ \ |] ==> jump_cardinal(K) : jump_cardinal(K)"; by (subgoal_tac "f O ordermap(X,r): bij(X, jump_cardinal(K))" 1); @@ -658,7 +652,7 @@ (*** Basic properties of successor cardinals ***) Goalw [csucc_def] - "!!K. Ord(K) ==> Card(csucc(K)) & K < csucc(K)"; + "Ord(K) ==> Card(csucc(K)) & K < csucc(K)"; by (rtac LeastI 1); by (REPEAT (ares_tac [conjI, Card_jump_cardinal, K_lt_jump_cardinal, Ord_jump_cardinal] 1)); @@ -674,13 +668,12 @@ qed "Ord_0_lt_csucc"; Goalw [csucc_def] - "!!K L. [| Card(L); K csucc(K) le L"; + "[| Card(L); K csucc(K) le L"; by (rtac Least_le 1); by (REPEAT (ares_tac [conjI, Card_is_Ord] 1)); qed "csucc_le"; -Goal - "!!K. [| Ord(i); Card(K) |] ==> i < csucc(K) <-> |i| le K"; +Goal "[| Ord(i); Card(K) |] ==> i < csucc(K) <-> |i| le K"; by (rtac iffI 1); by (rtac Card_lt_imp_lt 2); by (etac lt_trans1 2); @@ -693,14 +686,13 @@ ORELSE eresolve_tac [ltE, Card_is_Ord] 1)); qed "lt_csucc_iff"; -Goal - "!!K' K. [| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' le K"; +Goal "!!K' K. [| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' le K"; by (asm_simp_tac (simpset() addsimps [lt_csucc_iff, Card_cardinal_eq, Card_is_Ord]) 1); qed "Card_lt_csucc_iff"; Goalw [InfCard_def] - "!!K. InfCard(K) ==> InfCard(csucc(K))"; + "InfCard(K) ==> InfCard(csucc(K))"; by (asm_simp_tac (simpset() addsimps [Card_csucc, Card_is_Ord, lt_csucc RS leI RSN (2,le_trans)]) 1); qed "InfCard_csucc"; @@ -708,8 +700,7 @@ (*** Finite sets ***) -Goal - "!!n. n: nat ==> ALL A. A eqpoll n --> A : Fin(A)"; +Goal "n: nat ==> ALL A. A eqpoll n --> A : Fin(A)"; by (etac nat_induct 1); by (simp_tac (simpset() addsimps (eqpoll_0_iff::Fin.intrs)) 1); by (Clarify_tac 1); @@ -740,8 +731,7 @@ by (blast_tac (claset() addIs [Finite_into_Fin, Fin_into_Finite]) 1); qed "Finite_Fin_iff"; -Goal - "!!A. [| Finite(A); Finite(B) |] ==> Finite(A Un B)"; +Goal "[| Finite(A); Finite(B) |] ==> Finite(A Un B)"; by (blast_tac (claset() addSIs [Fin_into_Finite, Fin_UnI] addSDs [Finite_into_Fin] addIs [Un_upper1 RS Fin_mono RS subsetD, @@ -751,8 +741,7 @@ (** Removing elements from a finite set decreases its cardinality **) -Goal - "!!A. A: Fin(U) ==> x~:A --> ~ cons(x,A) lepoll A"; +Goal "A: Fin(U) ==> x~:A --> ~ cons(x,A) lepoll A"; by (etac Fin_induct 1); by (simp_tac (simpset() addsimps [lepoll_0_iff]) 1); by (subgoal_tac "cons(x,cons(xa,y)) = cons(xa,cons(x,y))" 1); @@ -761,8 +750,7 @@ by (Blast_tac 1); qed "Fin_imp_not_cons_lepoll"; -Goal - "!!a A. [| Finite(A); a~:A |] ==> |cons(a,A)| = succ(|A|)"; +Goal "[| Finite(A); a~:A |] ==> |cons(a,A)| = succ(|A|)"; by (rewtac cardinal_def); by (rtac Least_equality 1); by (fold_tac [cardinal_def]); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Cardinal_AC.ML --- a/src/ZF/Cardinal_AC.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Cardinal_AC.ML Wed Jul 15 14:13:18 1998 +0200 @@ -30,8 +30,7 @@ by (blast_tac (claset() addIs [cardinal_cong, cardinal_eqE]) 1); qed "cardinal_eqpoll_iff"; -Goal - "!!A. [| |A|=|B|; |C|=|D|; A Int C = 0; B Int D = 0 |] ==> \ +Goal "[| |A|=|B|; |C|=|D|; A Int C = 0; B Int D = 0 |] ==> \ \ |A Un C| = |B Un D|"; by (asm_full_simp_tac (simpset() addsimps [cardinal_eqpoll_iff, eqpoll_disjoint_Un]) 1); @@ -106,8 +105,7 @@ qed "surj_implies_cardinal_le"; (*Kunen's Lemma 10.21*) -Goal - "!!K. [| InfCard(K); ALL i:K. |X(i)| le K |] ==> |UN i:K. X(i)| le K"; +Goal "[| InfCard(K); ALL i:K. |X(i)| le K |] ==> |UN i:K. X(i)| le K"; by (asm_full_simp_tac (simpset() addsimps [InfCard_is_Card, le_Card_iff]) 1); by (rtac lepoll_trans 1); by (resolve_tac [InfCard_square_eq RS eqpoll_imp_lepoll] 2); @@ -134,8 +132,7 @@ qed "cardinal_UN_le"; (*The same again, using csucc*) -Goal - "!!K. [| InfCard(K); ALL i:K. |X(i)| < csucc(K) |] ==> \ +Goal "[| InfCard(K); ALL i:K. |X(i)| < csucc(K) |] ==> \ \ |UN i:K. X(i)| < csucc(K)"; by (asm_full_simp_tac (simpset() addsimps [Card_lt_csucc_iff, cardinal_UN_le, @@ -144,8 +141,7 @@ (*The same again, for a union of ordinals. In use, j(i) is a bit like rank(i), the least ordinal j such that i:Vfrom(A,j). *) -Goal - "!!K. [| InfCard(K); ALL i:K. j(i) < csucc(K) |] ==> \ +Goal "[| InfCard(K); ALL i:K. j(i) < csucc(K) |] ==> \ \ (UN i:K. j(i)) < csucc(K)"; by (resolve_tac [cardinal_UN_lt_csucc RS Card_lt_imp_lt] 1); by (assume_tac 1); @@ -178,8 +174,7 @@ (*Simpler to require |W|=K; we'd have a bijection; but the theorem would be weaker.*) -Goal - "!!K. [| InfCard(K); |W| le K; ALL w:W. j(w) < csucc(K) |] ==> \ +Goal "[| InfCard(K); |W| le K; ALL w:W. j(w) < csucc(K) |] ==> \ \ (UN w:W. j(w)) < csucc(K)"; by (excluded_middle_tac "W=0" 1); by (asm_simp_tac (*solve the easy 0 case*) diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Coind/ECR.ML --- a/src/ZF/Coind/ECR.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Coind/ECR.ML Wed Jul 15 14:13:18 1998 +0200 @@ -9,7 +9,7 @@ (* Specialised co-induction rule *) Goal - "!!x.[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \ + "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \ \ :ElabRel; ve_dom(ve) = te_dom(te); \ \ {.y:ve_dom(ve)}: \ \ Pow({} Un HasTyRel) |] ==> \ @@ -47,7 +47,7 @@ (* Properties of the pointwise extension to environments *) Goalw [hastyenv_def] - "!!ve.[| ve:ValEnv; te:TyEnv; hastyenv(ve,te); :HasTyRel |] ==> \ + "[| ve:ValEnv; te:TyEnv; hastyenv(ve,te); :HasTyRel |] ==> \ \ hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))"; by Safe_tac; by (stac ve_dom_owr 1); @@ -68,7 +68,7 @@ qed "hastyenv_owr"; Goalw [isofenv_def,hastyenv_def] - "!!ve.[| ve:ValEnv; te:TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)"; + "[| ve:ValEnv; te:TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)"; by Safe_tac; by (dtac bspec 1); by (assume_tac 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Coind/MT.ML --- a/src/ZF/Coind/MT.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Coind/MT.ML Wed Jul 15 14:13:18 1998 +0200 @@ -11,22 +11,21 @@ (* The Consistency theorem *) (* ############################################################ *) -Goal - "!!t. [| c:Const; hastyenv(ve,te);:ElabRel |] ==> \ +Goal "[| c:Const; hastyenv(ve,te);:ElabRel |] ==> \ \ : HasTyRel"; by (Fast_tac 1); qed "consistency_const"; Goalw [hastyenv_def] - "!!t. [| x:ve_dom(ve); hastyenv(ve,te); :ElabRel |] ==> \ + "[| x:ve_dom(ve); hastyenv(ve,te); :ElabRel |] ==> \ \ :HasTyRel"; by (Fast_tac 1); qed "consistency_var"; Goalw [hastyenv_def] - "!!t. [| ve:ValEnv; x:ExVar; e:Exp; hastyenv(ve,te); \ + "[| ve:ValEnv; x:ExVar; e:Exp; hastyenv(ve,te); \ \ :ElabRel \ \ |] ==> : HasTyRel"; by (Best_tac 1); @@ -143,8 +142,7 @@ fun mt_cases_tac t = ((rtac t 1) THEN (TRYALL assume_tac)); -Goal - "!!e. :EvalRel ==> \ +Goal ":EvalRel ==> \ \ (ALL t te. hastyenv(ve,te) --> :ElabRel --> :HasTyRel)"; by (etac EvalRel.induct 1); by (safe_tac ZF_cs); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Coind/Map.ML --- a/src/ZF/Coind/Map.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Coind/Map.ML Wed Jul 15 14:13:18 1998 +0200 @@ -59,7 +59,7 @@ (* Lemmas *) Goalw [quniv_def] - "!!A. A <= univ(X) ==> Pow(A * Union(quniv(X))) <= quniv(X)"; + "A <= univ(X) ==> Pow(A * Union(quniv(X))) <= quniv(X)"; by (rtac Pow_mono 1); by (rtac ([Sigma_mono, product_univ] MRS subset_trans) 1); by (etac subset_trans 1); @@ -103,7 +103,7 @@ Goalw [map_owr_def,PMap_def,TMap_def] - "!! A.[| m:PMap(A,B); a:A; b:B |] ==> map_owr(m,a,b):PMap(A,B)"; + "[| m:PMap(A,B); a:A; b:B |] ==> map_owr(m,a,b):PMap(A,B)"; by Safe_tac; by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [if_iff]))); by (Fast_tac 1); @@ -123,7 +123,7 @@ (** map_app **) Goalw [TMap_def,map_app_def] - "!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a) ~=0"; + "[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a) ~=0"; by (etac domainE 1); by (dtac imageI 1); by (Fast_tac 1); @@ -131,12 +131,12 @@ qed "tmap_app_notempty"; Goalw [TMap_def,map_app_def,domain_def] - "!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a):B"; + "[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a):B"; by (Fast_tac 1); qed "tmap_appI"; Goalw [PMap_def] - "!!m.[| m:PMap(A,B); a:domain(m) |] ==> map_app(m,a):B"; + "[| m:PMap(A,B); a:domain(m) |] ==> map_app(m,a):B"; by (forward_tac [tmap_app_notempty] 1); by (assume_tac 1); by (dtac tmap_appI 1); @@ -147,12 +147,12 @@ (** domain **) Goalw [TMap_def] - "!!m.[| m:TMap(A,B); a:domain(m) |] ==> a:A"; + "[| m:TMap(A,B); a:domain(m) |] ==> a:A"; by (Fast_tac 1); qed "tmap_domainD"; Goalw [PMap_def,TMap_def] - "!!m.[| m:PMap(A,B); a:domain(m) |] ==> a:A"; + "[| m:PMap(A,B); a:domain(m) |] ==> a:A"; by (Fast_tac 1); qed "pmap_domainD"; @@ -180,7 +180,7 @@ qed "map_domain_emp"; Goalw [map_owr_def] - "!!a. b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)"; + "b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)"; by (simp_tac (simpset() addsimps [domain_Sigma]) 1); by (rtac equalityI 1); by (Fast_tac 1); @@ -204,7 +204,7 @@ qed "map_app_owr1"; Goalw [map_app_def,map_owr_def] - "!!a. c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)"; + "c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)"; by (rtac (excluded_middle RS disjE) 1); by (stac qbeta_emp 1); by (assume_tac 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Coind/Types.ML --- a/src/ZF/Coind/Types.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Coind/Types.ML Wed Jul 15 14:13:18 1998 +0200 @@ -38,12 +38,11 @@ qed "te_app_owr1"; Goalw [te_app_def] - "!!x y. x ~= y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)"; + "x ~= y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)"; by (asm_simp_tac (simpset() addsimps [te_rec_owr,(not_sym RS if_not_P)]) 1); qed "te_app_owr2"; -Goal - "!!te. [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==> te_app(te,x):Ty"; +Goal "[| te:TyEnv; x:ExVar; x:te_dom(te) |] ==> te_app(te,x):Ty"; by (res_inst_tac [("P","x:te_dom(te)")] impE 1); by (assume_tac 2); by (assume_tac 2); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Coind/Values.ML --- a/src/ZF/Coind/Values.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Coind/Values.ML Wed Jul 15 14:13:18 1998 +0200 @@ -60,7 +60,7 @@ qed "v_closNE"; Goalw (sum_def::QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs) - "!!c. c:Const ==> v_const(c) ~= 0"; + "c:Const ==> v_const(c) ~= 0"; by (dtac constNEE 1); by (etac not_emptyE 1); by (rtac not_emptyI 1); @@ -95,14 +95,14 @@ qed "ve_dom_owr"; Goalw [ve_app_def,ve_owr_def] -"!!ve. ve:ValEnv ==> ve_app(ve_owr(ve,x,v),x) = v"; +"ve:ValEnv ==> ve_app(ve_owr(ve,x,v),x) = v"; by (etac ValEnvE 1); by (asm_full_simp_tac (simpset() addsimps Val_ValEnv.case_eqns) 1); by (rtac map_app_owr1 1); qed "ve_app_owr1"; Goalw [ve_app_def,ve_owr_def] - "!!ve. ve:ValEnv ==> x ~= y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)"; + "ve:ValEnv ==> x ~= y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)"; by (etac ValEnvE 1); by (asm_full_simp_tac (simpset() addsimps Val_ValEnv.case_eqns) 1); by (rtac map_app_owr2 1); @@ -112,7 +112,7 @@ (* Introduction rules for operators on value environments *) Goalw [ve_app_def,ve_owr_def,ve_dom_def] - "!!ve.[| ve:ValEnv; x:ve_dom(ve) |] ==> ve_app(ve,x):Val"; + "[| ve:ValEnv; x:ve_dom(ve) |] ==> ve_app(ve,x):Val"; by (etac ValEnvE 1); by (hyp_subst_tac 1); by (asm_full_simp_tac (simpset() addsimps Val_ValEnv.case_eqns) 1); @@ -122,7 +122,7 @@ qed "ve_appI"; Goalw [ve_dom_def] - "!!ve.[| ve:ValEnv; x:ve_dom(ve) |] ==> x:ExVar"; + "[| ve:ValEnv; x:ve_dom(ve) |] ==> x:ExVar"; by (etac ValEnvE 1); by (hyp_subst_tac 1); by (asm_full_simp_tac (simpset() addsimps Val_ValEnv.case_eqns) 1); @@ -136,8 +136,7 @@ by (rtac pmap_empI 1); qed "ve_empI"; -Goalw [ve_owr_def] - "!!ve.[|ve:ValEnv; x:ExVar; v:Val |] ==> ve_owr(ve,x,v):ValEnv"; +Goalw [ve_owr_def] "[|ve:ValEnv; x:ExVar; v:Val |] ==> ve_owr(ve,x,v):ValEnv"; by (etac ValEnvE 1); by (hyp_subst_tac 1); by (asm_full_simp_tac (simpset() addsimps Val_ValEnv.case_eqns) 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Epsilon.ML --- a/src/ZF/Epsilon.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Epsilon.ML Wed Jul 15 14:13:18 1998 +0200 @@ -61,7 +61,7 @@ (** eclose(A) is the least transitive set including A as a subset. **) Goalw [Transset_def] - "!!X A n. [| Transset(X); A<=X; n: nat |] ==> \ + "[| Transset(X); A<=X; n: nat |] ==> \ \ nat_rec(n, A, %m r. Union(r)) <= X"; by (etac nat_induct 1); by (asm_simp_tac (simpset() addsimps [nat_rec_0]) 1); @@ -70,7 +70,7 @@ qed "eclose_least_lemma"; Goalw [eclose_def] - "!!X A. [| Transset(X); A<=X |] ==> eclose(A) <= X"; + "[| Transset(X); A<=X |] ==> eclose(A) <= X"; by (rtac (eclose_least_lemma RS UN_least) 1); by (REPEAT (assume_tac 1)); qed "eclose_least"; @@ -105,13 +105,13 @@ (*Variant of the previous lemma in a useable form for the sequel*) Goal - "!!A B C. [| A: eclose({B}); B: eclose({C}) |] ==> A: eclose({C})"; + "[| 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"; Goalw [Transset_def] - "!!i j. [| Transset(i); j:i |] ==> Memrel(i)-``{j} = j"; + "[| Transset(i); j:i |] ==> Memrel(i)-``{j} = j"; by (blast_tac (claset() addSIs [MemrelI] addSEs [MemrelE]) 1); qed "under_Memrel"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/EquivClass.ML --- a/src/ZF/EquivClass.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/EquivClass.ML Wed Jul 15 14:13:18 1998 +0200 @@ -15,23 +15,23 @@ (** first half: equiv(A,r) ==> converse(r) O r = r **) Goalw [trans_def,sym_def] - "!!r. [| sym(r); trans(r) |] ==> converse(r) O r <= r"; + "[| sym(r); trans(r) |] ==> converse(r) O r <= r"; by (Blast_tac 1); qed "sym_trans_comp_subset"; Goalw [refl_def] - "!!A r. [| refl(A,r); r <= A*A |] ==> r <= converse(r) O r"; + "[| refl(A,r); r <= A*A |] ==> r <= converse(r) O r"; by (Blast_tac 1); qed "refl_comp_subset"; Goalw [equiv_def] - "!!A r. equiv(A,r) ==> converse(r) O r = r"; + "equiv(A,r) ==> converse(r) O r = r"; by (blast_tac (subset_cs addSIs [sym_trans_comp_subset, refl_comp_subset]) 1); qed "equiv_comp_eq"; (*second half*) Goalw [equiv_def,refl_def,sym_def,trans_def] - "!!A r. [| converse(r) O r = r; domain(r) = A |] ==> equiv(A,r)"; + "[| converse(r) O r = r; domain(r) = A |] ==> equiv(A,r)"; by (etac equalityE 1); by (subgoal_tac "ALL x y. : r --> : r" 1); by (ALLGOALS Fast_tac); @@ -41,25 +41,25 @@ (*Lemma for the next result*) Goalw [trans_def,sym_def] - "!!A r. [| sym(r); trans(r); : r |] ==> r``{a} <= r``{b}"; + "[| sym(r); trans(r); : r |] ==> r``{a} <= r``{b}"; by (Blast_tac 1); qed "equiv_class_subset"; Goalw [equiv_def] - "!!A r. [| equiv(A,r); : r |] ==> r``{a} = r``{b}"; + "[| equiv(A,r); : r |] ==> r``{a} = r``{b}"; by (safe_tac (subset_cs addSIs [equalityI, equiv_class_subset])); by (rewtac sym_def); by (Blast_tac 1); qed "equiv_class_eq"; Goalw [equiv_def,refl_def] - "!!A r. [| equiv(A,r); a: A |] ==> a: r``{a}"; + "[| equiv(A,r); a: A |] ==> a: r``{a}"; by (Blast_tac 1); qed "equiv_class_self"; (*Lemma for the next result*) Goalw [equiv_def,refl_def] - "!!A r. [| equiv(A,r); r``{b} <= r``{a}; b: A |] ==> : r"; + "[| equiv(A,r); r``{b} <= r``{a}; b: A |] ==> : r"; by (Blast_tac 1); qed "subset_equiv_class"; @@ -70,7 +70,7 @@ (*thus r``{a} = r``{b} as well*) Goalw [equiv_def,trans_def,sym_def] - "!!A r. [| equiv(A,r); x: (r``{a} Int r``{b}) |] ==> : r"; + "[| equiv(A,r); x: (r``{a} Int r``{b}) |] ==> : r"; by (Blast_tac 1); qed "equiv_class_nondisjoint"; @@ -79,13 +79,13 @@ qed "equiv_type"; Goal - "!!A r. equiv(A,r) ==> : r <-> r``{x} = r``{y} & x:A & y:A"; + "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 - "!!A r. [| equiv(A,r); x: A; y: A |] ==> r``{x} = r``{y} <-> : r"; + "[| 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"; @@ -108,12 +108,12 @@ qed "quotientE"; Goalw [equiv_def,refl_def,quotient_def] - "!!A r. equiv(A,r) ==> Union(A/r) = A"; + "equiv(A,r) ==> Union(A/r) = A"; by (Blast_tac 1); qed "Union_quotient"; Goalw [quotient_def] - "!!A r. [| equiv(A,r); X: A/r; Y: A/r |] ==> X=Y | (X Int Y <= 0)"; + "[| equiv(A,r); X: A/r; Y: A/r |] ==> X=Y | (X Int Y <= 0)"; by (safe_tac (claset() addSIs [equiv_class_eq])); by (assume_tac 1); by (rewrite_goals_tac [equiv_def,trans_def,sym_def]); @@ -168,7 +168,7 @@ Goalw [congruent_def,congruent2_def,equiv_def,refl_def] - "!!A r. [| equiv(A,r); congruent2(r,b); a: A |] ==> congruent(r,b(a))"; + "[| equiv(A,r); congruent2(r,b); a: A |] ==> congruent(r,b(a))"; by (Blast_tac 1); qed "congruent2_implies_congruent"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Fixedpt.ML --- a/src/ZF/Fixedpt.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Fixedpt.ML Wed Jul 15 14:13:18 1998 +0200 @@ -55,7 +55,7 @@ (*lfp is contained in each pre-fixedpoint*) Goalw [lfp_def] - "!!A. [| h(A) <= A; A<=D |] ==> lfp(D,h) <= A"; + "[| h(A) <= A; A<=D |] ==> lfp(D,h) <= A"; by (Blast_tac 1); (*or by (rtac (PowI RS CollectI RS Inter_lower) 1); *) qed "lfp_lowerbound"; @@ -258,8 +258,7 @@ qed "coinduct_lemma"; (*strong version*) -Goal - "!!X D. [| bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D |] ==> \ +Goal "[| bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D |] ==> \ \ a : gfp(D,h)"; by (rtac weak_coinduct 1); by (etac coinduct_lemma 2); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/InfDatatype.ML --- a/src/ZF/InfDatatype.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/InfDatatype.ML Wed Jul 15 14:13:18 1998 +0200 @@ -11,8 +11,7 @@ transfer InfDatatype.thy Limit_VfromE |> standard; -Goal - "!!K. [| f: W -> Vfrom(A,csucc(K)); |W| le K; InfCard(K) \ +Goal "[| f: W -> Vfrom(A,csucc(K)); |W| le K; InfCard(K) \ \ |] ==> EX j. f: W -> Vfrom(A,j) & j < csucc(K)"; by (res_inst_tac [("x", "UN w:W. LEAST i. f`w : Vfrom(A,i)")] exI 1); by (rtac conjI 1); @@ -29,15 +28,13 @@ by (assume_tac 1); qed "fun_Vcsucc_lemma"; -Goal - "!!K. [| W <= Vfrom(A,csucc(K)); |W| le K; InfCard(K) \ +Goal "[| W <= Vfrom(A,csucc(K)); |W| le K; InfCard(K) \ \ |] ==> EX j. W <= Vfrom(A,j) & j < csucc(K)"; by (asm_full_simp_tac (simpset() addsimps [subset_iff_id, fun_Vcsucc_lemma]) 1); qed "subset_Vcsucc"; (*Version for arbitrary index sets*) -Goal - "!!K. [| |W| le K; InfCard(K); W <= Vfrom(A,csucc(K)) |] ==> \ +Goal "[| |W| le K; InfCard(K); W <= Vfrom(A,csucc(K)) |] ==> \ \ W -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"; by (safe_tac (claset() addSDs [fun_Vcsucc_lemma, subset_Vcsucc])); by (resolve_tac [Vfrom RS ssubst] 1); @@ -50,8 +47,7 @@ Limit_has_succ, Un_least_lt] 1)); qed "fun_Vcsucc"; -Goal - "!!K. [| f: W -> Vfrom(A, csucc(K)); |W| le K; InfCard(K); \ +Goal "[| f: W -> Vfrom(A, csucc(K)); |W| le K; InfCard(K); \ \ W <= Vfrom(A,csucc(K)) \ \ |] ==> f: Vfrom(A,csucc(K))"; by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1)); @@ -62,16 +58,14 @@ (** Version where K itself is the index set **) -Goal - "!!K. InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"; +Goal "InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"; by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1); by (REPEAT (ares_tac [fun_Vcsucc, Ord_cardinal_le, i_subset_Vfrom, lt_csucc RS leI RS le_imp_subset RS subset_trans] 1)); qed "Card_fun_Vcsucc"; -Goal - "!!K. [| f: K -> Vfrom(A, csucc(K)); InfCard(K) \ +Goal "[| f: K -> Vfrom(A, csucc(K)); InfCard(K) \ \ |] ==> f: Vfrom(A,csucc(K))"; by (REPEAT (ares_tac [Card_fun_Vcsucc RS subsetD] 1)); qed "Card_fun_in_Vcsucc"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/List.ML --- a/src/ZF/List.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/List.ML Wed Jul 15 14:13:18 1998 +0200 @@ -111,7 +111,7 @@ qed "drop_Nil"; Goalw [drop_def] - "!!i. i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)"; + "i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)"; by (rtac sym 1); by (etac nat_induct 1); by (Simp_tac 1); @@ -121,7 +121,7 @@ Addsimps [drop_0, drop_Nil, drop_succ_Cons]; Goalw [drop_def] - "!!i l. [| i:nat; l: list(A) |] ==> drop(i,l) : list(A)"; + "[| i:nat; l: list(A) |] ==> drop(i,l) : list(A)"; by (etac nat_induct 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [tl_type]))); qed "drop_type"; @@ -189,7 +189,7 @@ Addsimps [length_Nil,length_Cons]; Goalw [length_def] - "!!l. l: list(A) ==> length(l) : nat"; + "l: list(A) ==> length(l) : nat"; by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1)); qed "length_type"; @@ -199,7 +199,7 @@ Addsimps [app_Nil, app_Cons]; Goalw [app_def] - "!!xs ys. [| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)"; + "[| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)"; by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1)); qed "app_type"; @@ -209,7 +209,7 @@ Addsimps [rev_Nil,rev_Cons] ; Goalw [rev_def] - "!!xs. xs: list(A) ==> rev(xs) : list(A)"; + "xs: list(A) ==> rev(xs) : list(A)"; by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1)); qed "rev_type"; @@ -220,7 +220,7 @@ Addsimps [flat_Nil,flat_Cons]; Goalw [flat_def] - "!!ls. ls: list(list(A)) ==> flat(ls) : list(A)"; + "ls: list(list(A)) ==> flat(ls) : list(A)"; by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1)); qed "flat_type"; @@ -231,13 +231,12 @@ Addsimps [set_of_list_Nil,set_of_list_Cons]; Goalw [set_of_list_def] - "!!l. l: list(A) ==> set_of_list(l) : Pow(A)"; + "l: list(A) ==> set_of_list(l) : Pow(A)"; by (etac list_rec_type 1); by (ALLGOALS (Blast_tac)); qed "set_of_list_type"; -Goal - "!!l. xs: list(A) ==> \ +Goal "xs: list(A) ==> \ \ set_of_list (xs@ys) = set_of_list(xs) Un set_of_list(ys)"; by (etac list.induct 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_cons]))); @@ -250,7 +249,7 @@ Addsimps [list_add_Nil,list_add_Cons]; Goalw [list_add_def] - "!!xs. xs: list(nat) ==> list_add(xs) : nat"; + "xs: list(nat) ==> list_add(xs) : nat"; by (REPEAT (ares_tac [list_rec_type, nat_0I, add_type] 1)); qed "list_add_type"; @@ -340,8 +339,7 @@ (** Length and drop **) (*Lemma for the inductive step of drop_length*) -Goal - "!!xs. xs: list(A) ==> \ +Goal "xs: list(A) ==> \ \ ALL x. EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"; by (etac list.induct 1); by (ALLGOALS Asm_simp_tac); @@ -349,8 +347,7 @@ qed "drop_length_Cons_lemma"; bind_thm ("drop_length_Cons", (drop_length_Cons_lemma RS spec)); -Goal - "!!l. l: list(A) ==> ALL i: length(l). EX z zs. drop(i,l) = Cons(z,zs)"; +Goal "l: list(A) ==> ALL i: length(l). EX z zs. drop(i,l) = Cons(z,zs)"; by (etac list.induct 1); by (ALLGOALS Asm_simp_tac); by (rtac conjI 1); @@ -394,8 +391,7 @@ instantiate the variable ?A in the rules' typing conditions; note that rev_type does not instantiate ?A. Only the premises do. *) -Goal - "!!xs. [| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)"; +Goal "[| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)"; by (etac list.induct 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_right_Nil,app_assoc]))); qed "rev_app_distrib"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Nat.ML --- a/src/ZF/Nat.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Nat.ML Wed Jul 15 14:13:18 1998 +0200 @@ -168,8 +168,7 @@ (** Induction principle analogous to trancl_induct **) -Goal - "!!m. m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> \ +Goal "m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> \ \ (ALL n:nat. m P(m,n))"; by (etac nat_induct 1); by (ALLGOALS (*blast_tac gives PROOF FAILED*) diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Order.ML --- a/src/ZF/Order.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Order.ML Wed Jul 15 14:13:18 1998 +0200 @@ -15,7 +15,7 @@ (*needed?*) Goalw [part_ord_def, irrefl_def, trans_on_def, asym_def] - "!!r. part_ord(A,r) ==> asym(r Int A*A)"; + "part_ord(A,r) ==> asym(r Int A*A)"; by (Blast_tac 1); qed "part_ord_Imp_asym"; @@ -37,23 +37,23 @@ Goalw [irrefl_def, part_ord_def, tot_ord_def, trans_on_def, well_ord_def] - "!!r. [| wf[A](r); linear(A,r) |] ==> well_ord(A,r)"; + "[| wf[A](r); linear(A,r) |] ==> well_ord(A,r)"; by (asm_simp_tac (simpset() addsimps [wf_on_not_refl]) 1); by (fast_tac (claset() addEs [linearE, wf_on_asym, wf_on_chain3]) 1); qed "well_ordI"; Goalw [well_ord_def] - "!!r. well_ord(A,r) ==> wf[A](r)"; + "well_ord(A,r) ==> wf[A](r)"; by Safe_tac; qed "well_ord_is_wf"; Goalw [well_ord_def, tot_ord_def, part_ord_def] - "!!r. well_ord(A,r) ==> trans[A](r)"; + "well_ord(A,r) ==> trans[A](r)"; by Safe_tac; qed "well_ord_is_trans_on"; Goalw [well_ord_def, tot_ord_def] - "!!r. well_ord(A,r) ==> linear(A,r)"; + "well_ord(A,r) ==> linear(A,r)"; by (Blast_tac 1); qed "well_ord_is_linear"; @@ -86,7 +86,7 @@ qed "pred_pred_eq"; Goalw [trans_on_def, pred_def] - "!!r. [| trans[A](r); :r; x:A; y:A \ + "[| trans[A](r); :r; x:A; y:A \ \ |] ==> pred(pred(A,x,r), y, r) = pred(A,y,r)"; by (Blast_tac 1); qed "trans_pred_pred_eq"; @@ -97,22 +97,22 @@ (*Note: a relation s such that s<=r need not be a partial ordering*) Goalw [part_ord_def, irrefl_def, trans_on_def] - "!!A B r. [| part_ord(A,r); B<=A |] ==> part_ord(B,r)"; + "[| part_ord(A,r); B<=A |] ==> part_ord(B,r)"; by (Blast_tac 1); qed "part_ord_subset"; Goalw [linear_def] - "!!A B r. [| linear(A,r); B<=A |] ==> linear(B,r)"; + "[| linear(A,r); B<=A |] ==> linear(B,r)"; by (Blast_tac 1); qed "linear_subset"; Goalw [tot_ord_def] - "!!A B r. [| tot_ord(A,r); B<=A |] ==> tot_ord(B,r)"; + "[| tot_ord(A,r); B<=A |] ==> tot_ord(B,r)"; by (fast_tac (claset() addSEs [part_ord_subset, linear_subset]) 1); qed "tot_ord_subset"; Goalw [well_ord_def] - "!!A B r. [| well_ord(A,r); B<=A |] ==> well_ord(B,r)"; + "[| well_ord(A,r); B<=A |] ==> well_ord(B,r)"; by (fast_tac (claset() addSEs [tot_ord_subset, wf_on_subset_A]) 1); qed "well_ord_subset"; @@ -182,12 +182,12 @@ (** Order-preserving (monotone) maps **) Goalw [mono_map_def] - "!!f. f: mono_map(A,r,B,s) ==> f: A->B"; + "f: mono_map(A,r,B,s) ==> f: A->B"; by (etac CollectD1 1); qed "mono_map_is_fun"; Goalw [mono_map_def, inj_def] - "!!f. [| linear(A,r); wf[B](s); f: mono_map(A,r,B,s) |] ==> f: inj(A,B)"; + "[| linear(A,r); wf[B](s); f: mono_map(A,r,B,s) |] ==> f: inj(A,B)"; by (Clarify_tac 1); by (linear_case_tac 1); by (REPEAT @@ -208,24 +208,24 @@ qed "ord_isoI"; Goalw [ord_iso_def, mono_map_def] - "!!f. f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)"; + "f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)"; by (blast_tac (claset() addSDs [bij_is_fun]) 1); qed "ord_iso_is_mono_map"; Goalw [ord_iso_def] - "!!f. f: ord_iso(A,r,B,s) ==> f: bij(A,B)"; + "f: ord_iso(A,r,B,s) ==> f: bij(A,B)"; by (etac CollectD1 1); qed "ord_iso_is_bij"; (*Needed? But ord_iso_converse is!*) Goalw [ord_iso_def] - "!!f. [| f: ord_iso(A,r,B,s); : r; x:A; y:A |] ==> \ + "[| f: ord_iso(A,r,B,s); : r; x:A; y:A |] ==> \ \ : s"; by (Blast_tac 1); qed "ord_iso_apply"; Goalw [ord_iso_def] - "!!f. [| f: ord_iso(A,r,B,s); : s; x:B; y:B |] ==> \ + "[| f: ord_iso(A,r,B,s); : s; x:B; y:B |] ==> \ \ : r"; by (etac CollectE 1); by (etac (bspec RS bspec RS iffD2) 1); @@ -251,20 +251,20 @@ (*Symmetry of similarity*) Goalw [ord_iso_def] - "!!f. f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)"; + "f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)"; by (fast_tac (claset() addss bij_inverse_ss) 1); qed "ord_iso_sym"; (*Transitivity of similarity*) Goalw [mono_map_def] - "!!f. [| g: mono_map(A,r,B,s); f: mono_map(B,s,C,t) |] ==> \ + "[| g: mono_map(A,r,B,s); f: mono_map(B,s,C,t) |] ==> \ \ (f O g): mono_map(A,r,C,t)"; by (fast_tac (claset() addss bij_inverse_ss) 1); qed "mono_map_trans"; (*Transitivity of similarity: the order-isomorphism relation*) Goalw [ord_iso_def] - "!!f. [| g: ord_iso(A,r,B,s); f: ord_iso(B,s,C,t) |] ==> \ + "[| g: ord_iso(A,r,B,s); f: ord_iso(B,s,C,t) |] ==> \ \ (f O g): ord_iso(A,r,C,t)"; by (fast_tac (claset() addss bij_inverse_ss) 1); qed "ord_iso_trans"; @@ -272,7 +272,7 @@ (** Two monotone maps can make an order-isomorphism **) Goalw [ord_iso_def, mono_map_def] - "!!f g. [| f: mono_map(A,r,B,s); g: mono_map(B,s,A,r); \ + "[| f: mono_map(A,r,B,s); g: mono_map(B,s,A,r); \ \ f O g = id(B); g O f = id(A) |] ==> f: ord_iso(A,r,B,s)"; by Safe_tac; by (REPEAT_FIRST (ares_tac [fg_imp_bijective])); @@ -283,7 +283,7 @@ qed "mono_ord_isoI"; Goal - "!!B. [| well_ord(A,r); well_ord(B,s); \ + "[| 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)); @@ -297,13 +297,13 @@ (** Order-isomorphisms preserve the ordering's properties **) Goalw [part_ord_def, irrefl_def, trans_on_def, ord_iso_def] - "!!A B r. [| part_ord(B,s); f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)"; + "[| part_ord(B,s); f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)"; by (Asm_simp_tac 1); by (fast_tac (claset() addIs [bij_is_fun RS apply_type]) 1); qed "part_ord_ord_iso"; Goalw [linear_def, ord_iso_def] - "!!A B r. [| linear(B,s); f: ord_iso(A,r,B,s) |] ==> linear(A,r)"; + "[| linear(B,s); f: ord_iso(A,r,B,s) |] ==> linear(A,r)"; by (Asm_simp_tac 1); by Safe_tac; by (dres_inst_tac [("x1", "f`x"), ("x", "f`xa")] (bspec RS bspec) 1); @@ -313,7 +313,7 @@ qed "linear_ord_iso"; Goalw [wf_on_def, wf_def, ord_iso_def] - "!!A B r. [| wf[B](s); f: ord_iso(A,r,B,s) |] ==> wf[A](r)"; + "[| wf[B](s); f: ord_iso(A,r,B,s) |] ==> wf[A](r)"; (*reversed &-congruence rule handles context of membership in A*) by (asm_full_simp_tac (simpset() addcongs [conj_cong2]) 1); by Safe_tac; @@ -324,7 +324,7 @@ qed "wf_on_ord_iso"; Goalw [well_ord_def, tot_ord_def] - "!!A B r. [| well_ord(B,s); f: ord_iso(A,r,B,s) |] ==> well_ord(A,r)"; + "[| well_ord(B,s); f: ord_iso(A,r,B,s) |] ==> well_ord(A,r)"; by (fast_tac (claset() addSEs [part_ord_ord_iso, linear_ord_iso, wf_on_ord_iso]) 1); qed "well_ord_ord_iso"; @@ -335,7 +335,7 @@ (*Inductive argument for Kunen's Lemma 6.1, etc. Simple proof from Halmos, page 72*) Goalw [well_ord_def, ord_iso_def] - "!!r. [| well_ord(A,r); f: ord_iso(A,r, A',r); A'<= A; y: A |] \ + "[| well_ord(A,r); f: ord_iso(A,r, A',r); A'<= A; y: A |] \ \ ==> ~ : r"; by (REPEAT (eresolve_tac [conjE, CollectE] 1)); by (wf_on_ind_tac "y" [] 1); @@ -347,7 +347,7 @@ (*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment of a well-ordering*) Goal - "!!r. [| well_ord(A,r); f : ord_iso(A, r, pred(A,x,r), r); x:A |] ==> P"; + "[| 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 *) @@ -359,7 +359,7 @@ (*Simple consequence of Lemma 6.1*) Goal - "!!r. [| well_ord(A,r); f : ord_iso(pred(A,a,r), r, pred(A,c,r), r); \ + "[| 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); @@ -374,7 +374,7 @@ (*Does not assume r is a wellordering!*) Goalw [ord_iso_def, pred_def] - "!!r. [| f : ord_iso(A,r,B,s); a:A |] ==> \ + "[| f : ord_iso(A,r,B,s); a:A |] ==> \ \ f `` pred(A,a,r) = pred(B, f`a, s)"; by (etac CollectE 1); by (asm_simp_tac @@ -389,7 +389,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 - "!!r. [| f : ord_iso(A,r,B,s); a:A |] ==> \ + "[| 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); @@ -401,7 +401,7 @@ (*Tricky; a lot of forward proof!*) Goal - "!!r. [| well_ord(A,r); well_ord(B,s); : r; \ + "[| 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"; @@ -424,7 +424,7 @@ (*See Halmos, page 72*) Goal - "!!r. [| well_ord(A,r); \ + "[| 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); @@ -438,7 +438,7 @@ (*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*) Goal - "!!r. [| well_ord(A,r); \ + "[| 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)); @@ -471,13 +471,13 @@ qed "converse_ord_iso_map"; Goalw [ord_iso_map_def, function_def] - "!!B. well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))"; + "well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))"; by (blast_tac (claset() addIs [well_ord_iso_pred_eq, ord_iso_sym, ord_iso_trans]) 1); qed "function_ord_iso_map"; Goal - "!!B. well_ord(B,s) ==> ord_iso_map(A,r,B,s) \ + "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, @@ -485,7 +485,7 @@ qed "ord_iso_map_fun"; Goalw [mono_map_def] - "!!B. [| well_ord(A,r); well_ord(B,s) |] ==> ord_iso_map(A,r,B,s) \ + "[| well_ord(A,r); well_ord(B,s) |] ==> ord_iso_map(A,r,B,s) \ \ : mono_map(domain(ord_iso_map(A,r,B,s)), r, \ \ range(ord_iso_map(A,r,B,s)), s)"; by (asm_simp_tac (simpset() addsimps [ord_iso_map_fun]) 1); @@ -501,7 +501,7 @@ qed "ord_iso_map_mono_map"; Goalw [mono_map_def] - "!!B. [| well_ord(A,r); well_ord(B,s) |] ==> ord_iso_map(A,r,B,s) \ + "[| well_ord(A,r); well_ord(B,s) |] ==> ord_iso_map(A,r,B,s) \ \ : ord_iso(domain(ord_iso_map(A,r,B,s)), r, \ \ range(ord_iso_map(A,r,B,s)), s)"; by (rtac well_ord_mono_ord_isoI 1); @@ -515,7 +515,7 @@ (*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*) Goalw [ord_iso_map_def] - "!!B. [| well_ord(A,r); well_ord(B,s); \ + "[| well_ord(A,r); well_ord(B,s); \ \ a: A; a ~: domain(ord_iso_map(A,r,B,s)) \ \ |] ==> domain(ord_iso_map(A,r,B,s)) <= pred(A, a, r)"; by (safe_tac (claset() addSIs [predI])); @@ -536,7 +536,7 @@ (*For the 4-way case analysis in the main result*) Goal - "!!B. [| well_ord(A,r); well_ord(B,s) |] ==> \ + "[| 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); @@ -557,7 +557,7 @@ (*As above, by duality*) Goal - "!!B. [| well_ord(A,r); well_ord(B,s) |] ==> \ + "[| 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); @@ -567,7 +567,7 @@ (*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*) Goal - "!!B. [| well_ord(A,r); well_ord(B,s) |] ==> \ + "[| 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))"; @@ -590,27 +590,27 @@ (*** Properties of converse(r), by Krzysztof Grabczewski ***) Goalw [irrefl_def] - "!!A. irrefl(A,r) ==> irrefl(A,converse(r))"; + "irrefl(A,r) ==> irrefl(A,converse(r))"; by (Blast_tac 1); qed "irrefl_converse"; Goalw [trans_on_def] - "!!A. trans[A](r) ==> trans[A](converse(r))"; + "trans[A](r) ==> trans[A](converse(r))"; by (Blast_tac 1); qed "trans_on_converse"; Goalw [part_ord_def] - "!!A. part_ord(A,r) ==> part_ord(A,converse(r))"; + "part_ord(A,r) ==> part_ord(A,converse(r))"; by (blast_tac (claset() addSIs [irrefl_converse, trans_on_converse]) 1); qed "part_ord_converse"; Goalw [linear_def] - "!!A. linear(A,r) ==> linear(A,converse(r))"; + "linear(A,r) ==> linear(A,converse(r))"; by (Blast_tac 1); qed "linear_converse"; Goalw [tot_ord_def] - "!!A. tot_ord(A,r) ==> tot_ord(A,converse(r))"; + "tot_ord(A,r) ==> tot_ord(A,converse(r))"; by (blast_tac (claset() addSIs [part_ord_converse, linear_converse]) 1); qed "tot_ord_converse"; @@ -623,7 +623,7 @@ qed "first_is_elem"; Goalw [well_ord_def, wf_on_def, wf_def, first_def] - "!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))"; + "[| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))"; by (REPEAT (eresolve_tac [conjE,allE,disjE] 1)); by (contr_tac 1); by (etac bexE 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/OrderArith.ML --- a/src/ZF/OrderArith.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/OrderArith.ML Wed Jul 15 14:13:18 1998 +0200 @@ -66,7 +66,7 @@ radd_Inl_Inr_iff, radd_Inr_Inl_iff]; Goalw [linear_def] - "!!r s. [| linear(A,r); linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"; + "[| linear(A,r); linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"; by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac sumE)); by (ALLGOALS Asm_simp_tac); qed "linear_radd"; @@ -75,7 +75,7 @@ (** Well-foundedness **) Goal - "!!r s. [| wf[A](r); wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))"; + "[| 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!*) @@ -91,14 +91,14 @@ qed "wf_on_radd"; Goal - "!!r s. [| wf(r); wf(s) |] ==> wf(radd(field(r),r,field(s),s))"; + "[| 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 - "!!r s. [| well_ord(A,r); well_ord(B,s) |] ==> \ + "[| 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); @@ -109,7 +109,7 @@ (** An ord_iso congruence law **) Goal - "!!f g. [| f: bij(A,C); g: bij(B,D) |] ==> \ + "[| 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))")] @@ -119,7 +119,7 @@ qed "sum_bij"; Goalw [ord_iso_def] - "!!r s. [| f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') |] ==> \ + "[| f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') |] ==> \ \ (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) \ \ : ord_iso(A+B, radd(A,r,B,s), A'+B', radd(A',r',B',s'))"; by (safe_tac (claset() addSIs [sum_bij])); @@ -135,7 +135,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 B. A Int B = 0 ==> \ + "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); @@ -171,7 +171,7 @@ (** Rewrite rule. Can be used to obtain introduction rules **) Goalw [rmult_def] - "!!r s. <, > : rmult(A,r,B,s) <-> \ + "<, > : rmult(A,r,B,s) <-> \ \ (: r & a':A & a:A & b': B & b: B) | \ \ (: s & a'=a & a:A & b': B & b: B)"; by (Blast_tac 1); @@ -212,7 +212,7 @@ (** Well-foundedness **) Goal - "!!r s. [| wf[A](r); wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))"; + "[| 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); @@ -226,14 +226,14 @@ Goal - "!!r s. [| wf(r); wf(s) |] ==> wf(rmult(field(r),r,field(s),s))"; + "[| 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 - "!!r s. [| well_ord(A,r); well_ord(B,s) |] ==> \ + "[| 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); @@ -245,7 +245,7 @@ (** An ord_iso congruence law **) Goal - "!!f g. [| f: bij(A,C); g: bij(B,D) |] ==> \ + "[| f: bij(A,C); g: bij(B,D) |] ==> \ \ (lam :A*B. ) : bij(A*B, C*D)"; by (res_inst_tac [("d", "%. ")] lam_bijective 1); @@ -254,7 +254,7 @@ qed "prod_bij"; Goalw [ord_iso_def] - "!!r s. [| f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') |] ==> \ + "[| f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') |] ==> \ \ (lam :A*B. ) \ \ : ord_iso(A*B, rmult(A,r,B,s), A'*B', rmult(A',r',B',s'))"; by (safe_tac (claset() addSIs [prod_bij])); @@ -272,7 +272,7 @@ (*Used??*) Goal - "!!x xr. well_ord({x},xr) ==> \ + "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); @@ -282,7 +282,7 @@ (*Here we build a complicated function term, then simplify it using case_cong, id_conv, comp_lam, case_case.*) Goal - "!!a. a~:C ==> \ + "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); @@ -297,7 +297,7 @@ qed "prod_sum_singleton_bij"; Goal - "!!A. [| a:A; well_ord(A,r) |] ==> \ + "[| 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), \ @@ -375,17 +375,17 @@ (** Partial Ordering Properties **) Goalw [irrefl_def, rvimage_def] - "!!A B. [| f: inj(A,B); irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))"; + "[| f: inj(A,B); irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))"; by (blast_tac (claset() addIs [inj_is_fun RS apply_type]) 1); qed "irrefl_rvimage"; Goalw [trans_on_def, rvimage_def] - "!!A B. [| f: inj(A,B); trans[B](r) |] ==> trans[A](rvimage(A,f,r))"; + "[| f: inj(A,B); trans[B](r) |] ==> trans[A](rvimage(A,f,r))"; by (blast_tac (claset() addIs [inj_is_fun RS apply_type]) 1); qed "trans_on_rvimage"; Goalw [part_ord_def] - "!!A B. [| f: inj(A,B); part_ord(B,r) |] ==> part_ord(A, rvimage(A,f,r))"; + "[| f: inj(A,B); part_ord(B,r) |] ==> part_ord(A, rvimage(A,f,r))"; by (blast_tac (claset() addSIs [irrefl_rvimage, trans_on_rvimage]) 1); qed "part_ord_rvimage"; @@ -402,7 +402,7 @@ qed "linear_rvimage"; Goalw [tot_ord_def] - "!!A B. [| f: inj(A,B); tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))"; + "[| f: inj(A,B); tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))"; by (blast_tac (claset() addSIs [part_ord_rvimage, linear_rvimage]) 1); qed "tot_ord_rvimage"; @@ -410,7 +410,7 @@ (** Well-foundedness **) Goal - "!!r. [| f: A->B; wf[B](r) |] ==> wf[A](rvimage(A,f,r))"; + "[| 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); @@ -422,7 +422,7 @@ (*Note that we need only wf[A](...) and linear(A,...) to get the result!*) Goal - "!!r. [| f: inj(A,B); well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))"; + "[| 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); @@ -430,11 +430,11 @@ qed "well_ord_rvimage"; Goalw [ord_iso_def] - "!!A B. f: bij(A,B) ==> f: ord_iso(A, rvimage(A,f,s), B, s)"; + "f: bij(A,B) ==> f: ord_iso(A, rvimage(A,f,s), B, s)"; by (asm_full_simp_tac (simpset() addsimps [rvimage_iff]) 1); qed "ord_iso_rvimage"; Goalw [ord_iso_def, rvimage_def] - "!!A B. f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A"; + "f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A"; by (Blast_tac 1); qed "ord_iso_rvimage_eq"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/OrderType.ML --- a/src/ZF/OrderType.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/OrderType.ML Wed Jul 15 14:13:18 1998 +0200 @@ -30,18 +30,18 @@ (*Kunen's Theorem 7.3 (i), page 16; see also Ordinal/Ord_in_Ord The smaller ordinal is an initial segment of the larger *) Goalw [pred_def, lt_def] - "!!i j. j pred(i, j, Memrel(i)) = j"; + "j pred(i, j, Memrel(i)) = j"; by (asm_simp_tac (simpset() addsimps [Memrel_iff]) 1); by (blast_tac (claset() addIs [Ord_trans]) 1); qed "lt_pred_Memrel"; Goalw [pred_def,Memrel_def] - "!!A x. x:A ==> pred(A, x, Memrel(A)) = A Int x"; + "x:A ==> pred(A, x, Memrel(A)) = A Int x"; by (Blast_tac 1); qed "pred_Memrel"; Goal - "!!i. [| j R"; + "[| 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 @@ -54,7 +54,7 @@ (*Kunen's Theorem 7.3 (ii), page 16. Isomorphic ordinals are equal*) Goal - "!!i. [| Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) \ + "[| 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)); @@ -74,7 +74,7 @@ (*Useful for cardinality reasoning; see CardinalArith.ML*) Goalw [ordermap_def, pred_def] - "!!r. [| wf[A](r); x:A |] ==> \ + "[| wf[A](r); x:A |] ==> \ \ ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"; by (Asm_simp_tac 1); by (etac (wfrec_on RS trans) 1); @@ -85,7 +85,7 @@ (*Useful for rewriting PROVIDED pred is not unfolded until later!*) Goal - "!!r. [| wf[A](r); x:A |] ==> \ + "[| 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); @@ -102,7 +102,7 @@ assume_tac i]; Goalw [well_ord_def, tot_ord_def, part_ord_def] - "!!r. [| well_ord(A,r); x:A |] ==> Ord(ordermap(A,r) ` x)"; + "[| well_ord(A,r); x:A |] ==> Ord(ordermap(A,r) ` x)"; by Safe_tac; by (wf_on_ind_tac "x" [] 1); by (asm_simp_tac (simpset() addsimps [ordermap_pred_unfold]) 1); @@ -115,7 +115,7 @@ qed "Ord_ordermap"; Goalw [ordertype_def] - "!!r. well_ord(A,r) ==> Ord(ordertype(A,r))"; + "well_ord(A,r) ==> Ord(ordertype(A,r))"; by (stac ([ordermap_type, subset_refl] MRS image_fun) 1); by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); by (blast_tac (claset() addIs [Ord_ordermap]) 2); @@ -128,7 +128,7 @@ (*** ordermap preserves the orderings in both directions ***) Goal - "!!r. [| : r; wf[A](r); w: A; x: A |] ==> \ + "[| : 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); @@ -137,7 +137,7 @@ (*linearity of r is crucial here*) Goalw [well_ord_def, tot_ord_def] - "!!r. [| ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); \ + "[| ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); \ \ w: A; x: A |] ==> : r"; by Safe_tac; by (linear_case_tac 1); @@ -153,7 +153,7 @@ (ordermap_type RS surj_image)); Goalw [well_ord_def, tot_ord_def, bij_def, inj_def] - "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"; + "well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"; by (fast_tac (claset() addSIs [ordermap_type, ordermap_surj] addEs [linearE] addDs [ordermap_mono] @@ -163,7 +163,7 @@ (*** Isomorphisms involving ordertype ***) Goalw [ord_iso_def] - "!!r. well_ord(A,r) ==> \ + "well_ord(A,r) ==> \ \ ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"; by (safe_tac (claset() addSEs [well_ord_is_wf] addSIs [ordermap_type RS apply_type, @@ -172,7 +172,7 @@ qed "ordertype_ord_iso"; Goal - "!!f. [| f: ord_iso(A,r,B,s); well_ord(B,s) |] ==> \ + "[| 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 @@ -182,7 +182,7 @@ qed "ordertype_eq"; Goal - "!!A B. [| ordertype(A,r) = ordertype(B,s); \ + "[| 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); @@ -226,7 +226,7 @@ (*Ordermap returns the same result if applied to an initial segment*) Goal - "!!r. [| well_ord(A,r); y:A; z: pred(A,y,r) |] ==> \ + "[| 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); @@ -249,7 +249,7 @@ (** Theorems by Krzysztof Grabczewski; proofs simplified by lcp **) Goal - "!!r. [| well_ord(A,r); x:A |] ==> \ + "[| 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); @@ -258,7 +258,7 @@ qed "ordertype_pred_subset"; Goal - "!!r. [| well_ord(A,r); x:A |] ==> \ + "[| 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)); @@ -270,7 +270,7 @@ (*May rewrite with this -- provided no rules are supplied for proving that well_ord(pred(A,x,r), r) *) Goal - "!!A r. well_ord(A,r) ==> \ + "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])); @@ -298,7 +298,7 @@ (*proof by lcp*) Goalw [Ord_alt_def, Ord_def, Transset_def, well_ord_def, tot_ord_def, part_ord_def, trans_on_def] - "!!i. Ord_alt(i) ==> Ord(i)"; + "Ord_alt(i) ==> Ord(i)"; by (asm_full_simp_tac (simpset() addsimps [Memrel_iff, pred_Memrel]) 1); by (blast_tac (claset() addSEs [equalityE]) 1); qed "Ord_alt_is_Ord"; @@ -317,7 +317,7 @@ qed "bij_sum_0"; Goal - "!!A r. well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)"; + "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); @@ -330,7 +330,7 @@ qed "bij_0_sum"; Goal - "!!A r. well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)"; + "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); @@ -340,7 +340,7 @@ (*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *) Goalw [pred_def] - "!!A B. a:A ==> \ + "a:A ==> \ \ (lam x:pred(A,a,r). Inl(x)) \ \ : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))"; by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1); @@ -351,7 +351,7 @@ qed "pred_Inl_bij"; Goal - "!!A B. [| a:A; well_ord(A,r) |] ==> \ + "[| 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); @@ -360,7 +360,7 @@ qed "ordertype_pred_Inl_eq"; Goalw [pred_def, id_def] - "!!A B. b:B ==> \ + "b:B ==> \ \ id(A+pred(B,b,s)) \ \ : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))"; by (res_inst_tac [("d", "%z. z")] lam_bijective 1); @@ -369,7 +369,7 @@ qed "pred_Inr_bij"; Goal - "!!A B. [| b:B; well_ord(A,r); well_ord(B,s) |] ==> \ + "[| 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); @@ -380,7 +380,7 @@ (*** Basic laws for ordinal addition ***) Goalw [oadd_def] - "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i++j)"; + "[| Ord(i); Ord(j) |] ==> Ord(i++j)"; by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 1)); qed "Ord_oadd"; @@ -422,14 +422,14 @@ (** A couple of strange but necessary results! **) Goal - "!!A B. A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))"; + "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 - "!!k. [| well_ord(A,r); k \ + "[| 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); @@ -451,7 +451,7 @@ qed "oadd_lt_mono2"; Goal - "!!i j k. [| i++j < i++k; Ord(i); Ord(j); Ord(k) |] ==> j j i++j < i++k <-> j i++j < i++k <-> j j=k"; + "[| 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 @@ -473,7 +473,7 @@ qed "oadd_inject"; Goalw [oadd_def] - "!!i j k. [| k < i++j; Ord(i); Ord(j) |] ==> k k (i++j)++k = i++(j++k)"; + "[| Ord(i); Ord(j); Ord(k) |] ==> (i++j)++k = i++(j++k)"; by (resolve_tac [ordertype_eq RS trans] 1); by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS sum_ord_iso_cong) 1); @@ -503,7 +503,7 @@ qed "oadd_assoc"; Goal - "!!i j. [| Ord(i); Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})"; + "[| 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)); @@ -519,7 +519,7 @@ qed "oadd_1"; Goal - "!!i. [| Ord(i); Ord(j) |] ==> i++succ(j) = succ(i++j)"; + "[| 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); @@ -537,7 +537,7 @@ qed "oadd_UN"; Goal - "!!i j. [| Ord(i); Limit(j) |] ==> i++j = (UN k:j. i++k)"; + "[| 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, @@ -580,7 +580,7 @@ qed "oadd_le_mono"; Goal - "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k"; + "[| 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"; @@ -591,7 +591,7 @@ **) Goal - "!!A B. A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))"; + "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); @@ -600,7 +600,7 @@ qed "bij_sum_Diff"; Goal - "!!i j. i le j ==> \ + "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,7 +615,7 @@ qed "ordertype_sum_Diff"; Goalw [oadd_def, odiff_def] - "!!i j. i le 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); @@ -631,7 +631,7 @@ qed "oadd_odiff_inverse"; Goalw [odiff_def] - "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i--j)"; + "[| Ord(i); Ord(j) |] ==> Ord(i--j)"; by (REPEAT (ares_tac [Ord_ordertype, well_ord_Memrel RS well_ord_subset, Diff_subset] 1)); qed "Ord_odiff"; @@ -639,7 +639,7 @@ (*By oadd_inject, the difference between i and j is unique. Note that we get i++j = k ==> j = k--i. *) Goal - "!!i j. [| Ord(i); Ord(j) |] ==> (i++j) -- i = j"; + "[| 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); @@ -659,14 +659,14 @@ (**** Ordinal Multiplication ****) Goalw [omult_def] - "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i**j)"; + "[| Ord(i); Ord(j) |] ==> Ord(i**j)"; by (REPEAT (ares_tac [Ord_ordertype, well_ord_rmult, well_ord_Memrel] 1)); qed "Ord_omult"; (*** A useful unfolding law ***) Goalw [pred_def] - "!!A B. [| a:A; b:B |] ==> \ + "[| a:A; b:B |] ==> \ \ pred(A*B, , rmult(A,r,B,s)) = \ \ pred(A,a,r)*B Un ({a} * pred(B,b,s))"; by (rtac equalityI 1); @@ -676,7 +676,7 @@ qed "pred_Pair_eq"; Goal - "!!A B. [| a:A; b:B; well_ord(A,r); well_ord(B,s) |] ==> \ + "[| 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))"; @@ -688,7 +688,7 @@ qed "ordertype_pred_Pair_eq"; Goalw [oadd_def, omult_def] - "!!i j. [| i' \ + "[| i' \ \ ordertype(pred(i*j, , rmult(i,Memrel(i),j,Memrel(j))), \ \ rmult(i,Memrel(i),j,Memrel(j))) = \ \ j**i' ++ j'"; @@ -707,7 +707,7 @@ qed "ordertype_pred_Pair_lemma"; Goalw [omult_def] - "!!i j. [| Ord(i); Ord(j); k \ + "[| Ord(i); Ord(j); k \ \ EX j' i'. k = j**i' ++ j' & j' j**i' ++ j' < j**i"; + "[| j' j**i' ++ j' < j**i"; by (rtac ltI 1); by (asm_simp_tac (simpset() addsimps [Ord_ordertype, well_ord_rmult, well_ord_Memrel, @@ -734,7 +734,7 @@ qed "omult_oadd_lt"; Goal - "!!i j. [| Ord(i); Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})"; + "[| 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); @@ -780,7 +780,7 @@ (** Distributive law for ordinal multiplication and addition **) Goalw [omult_def, oadd_def] - "!!i. [| Ord(i); Ord(j); Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)"; + "[| Ord(i); Ord(j); Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)"; by (resolve_tac [ordertype_eq RS trans] 1); by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS prod_ord_iso_cong) 1); @@ -803,7 +803,7 @@ (** Associative law **) Goalw [omult_def] - "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> (i**j)**k = i**(j**k)"; + "[| Ord(i); Ord(j); Ord(k) |] ==> (i**j)**k = i**(j**k)"; by (resolve_tac [ordertype_eq RS trans] 1); by (rtac ([ord_iso_refl, ordertype_ord_iso RS ord_iso_sym] MRS prod_ord_iso_cong) 1); @@ -826,7 +826,7 @@ qed "omult_UN"; Goal - "!!i j. [| Ord(i); Limit(j) |] ==> i**j = (UN k:j. i**k)"; + "[| 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); @@ -880,8 +880,7 @@ Ord_succD] 1)); qed "omult_le_mono"; -Goal - "!!i j. [| i' le i; j' i'**j' < i**j"; +Goal "[| i' le i; j' i'**j' < i**j"; by (rtac lt_trans1 1); by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_lt_mono2, ltE, Ord_succD] 1)); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Ordinal.ML --- a/src/ZF/Ordinal.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Ordinal.ML Wed Jul 15 14:13:18 1998 +0200 @@ -23,7 +23,7 @@ (** Consequences of downwards closure **) Goalw [Transset_def] - "!!C a b. [| Transset(C); {a,b}: C |] ==> a:C & b: C"; + "[| Transset(C); {a,b}: C |] ==> a:C & b: C"; by (Blast_tac 1); qed "Transset_doubleton_D"; @@ -52,12 +52,12 @@ qed "Transset_0"; Goalw [Transset_def] - "!!i j. [| Transset(i); Transset(j) |] ==> Transset(i Un j)"; + "[| Transset(i); Transset(j) |] ==> Transset(i Un j)"; by (Blast_tac 1); qed "Transset_Un"; Goalw [Transset_def] - "!!i j. [| Transset(i); Transset(j) |] ==> Transset(i Int j)"; + "[| Transset(i); Transset(j) |] ==> Transset(i Int j)"; by (Blast_tac 1); qed "Transset_Int"; @@ -343,13 +343,13 @@ (*Transset(i) does not suffice, though ALL j:i.Transset(j) does*) Goalw [Ord_def, Transset_def, trans_def] - "!!i. Ord(i) ==> trans(Memrel(i))"; + "Ord(i) ==> trans(Memrel(i))"; by (Blast_tac 1); qed "trans_Memrel"; (*If Transset(A) then Memrel(A) internalizes the membership relation below A*) Goalw [Transset_def] - "!!A. Transset(A) ==> : Memrel(A) <-> a:b & b:A"; + "Transset(A) ==> : Memrel(A) <-> a:b & b:A"; by (Blast_tac 1); qed "Transset_Memrel_iff"; @@ -654,7 +654,7 @@ qed "Limit_has_succ"; Goalw [Limit_def] - "!!i. [| 0 Limit(i)"; + "[| 0 Limit(i)"; by (safe_tac subset_cs); by (rtac (not_le_iff_lt RS iffD1) 2); by (blast_tac le_cs 4); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Perm.ML --- a/src/ZF/Perm.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Perm.ML Wed Jul 15 14:13:18 1998 +0200 @@ -58,7 +58,7 @@ (*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*) Goalw [inj_def] - "!!f A B. [| :f; :f; f: inj(A,B) |] ==> a=c"; + "[| :f; :f; f: inj(A,B) |] ==> a=c"; by (REPEAT (eresolve_tac [asm_rl, Pair_mem_PiE, CollectE] 1)); by (Blast_tac 1); qed "inj_equality"; @@ -168,12 +168,12 @@ (*The premises are equivalent to saying that f is injective...*) Goal - "!!f. [| f: A->B; converse(f): C->A; a: A |] ==> converse(f)`(f`a) = a"; + "[| 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. [| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a"; + "[| 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"; @@ -307,7 +307,7 @@ (** Composition preserves functions, injections, and surjections **) Goalw [function_def] - "!!f g. [| function(g); function(f) |] ==> function(f O g)"; + "[| function(g); function(f) |] ==> function(f O g)"; by (Blast_tac 1); qed "comp_function"; @@ -347,12 +347,12 @@ qed "comp_inj"; Goalw [surj_def] - "!!f g. [| g: surj(A,B); f: surj(B,C) |] ==> (f O g) : surj(A,C)"; + "[| g: surj(A,B); f: surj(B,C) |] ==> (f O g) : surj(A,C)"; by (blast_tac (claset() addSIs [comp_fun,comp_fun_apply]) 1); qed "comp_surj"; Goalw [bij_def] - "!!f g. [| g: bij(A,B); f: bij(B,C) |] ==> (f O g) : bij(A,C)"; + "[| g: bij(A,B); f: bij(B,C) |] ==> (f O g) : bij(A,C)"; by (blast_tac (claset() addIs [comp_inj,comp_surj]) 1); qed "comp_bij"; @@ -362,14 +362,14 @@ Artificial Intelligence, 10:1--27, 1978. **) Goalw [inj_def] - "!!f g. [| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)"; + "[| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)"; by Safe_tac; by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1)); by (asm_simp_tac (simpset() ) 1); qed "comp_mem_injD1"; Goalw [inj_def,surj_def] - "!!f g. [| (f O g): inj(A,C); g: surj(A,B); f: B->C |] ==> f: inj(B,C)"; + "[| (f O g): inj(A,C); g: surj(A,B); f: B->C |] ==> f: inj(B,C)"; by Safe_tac; by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1); by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3); @@ -381,17 +381,17 @@ qed "comp_mem_injD2"; Goalw [surj_def] - "!!f g. [| (f O g): surj(A,C); g: A->B; f: B->C |] ==> f: surj(B,C)"; + "[| (f O g): surj(A,C); g: A->B; f: B->C |] ==> f: surj(B,C)"; by (blast_tac (claset() addSIs [comp_fun_apply RS sym, apply_funtype]) 1); qed "comp_mem_surjD1"; Goal - "!!f g. [| (f O g)`a = c; g: A->B; f: B->C; a:A |] ==> f`(g`a) = c"; + "[| (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"; Goalw [inj_def,surj_def] - "!!f g. [| (f O g): surj(A,C); g: A->B; f: inj(B,C) |] ==> g: surj(A,B)"; + "[| (f O g): surj(A,C); g: A->B; f: inj(B,C) |] ==> g: surj(A,B)"; by Safe_tac; by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1); by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_fun_applyD 1)); @@ -424,7 +424,7 @@ (** Proving that a function is a bijection **) Goalw [id_def] - "!!f A B. [| f: A->B; g: B->A |] ==> \ + "[| f: A->B; g: B->A |] ==> \ \ f O g = id(B) <-> (ALL y:B. f`(g`y)=y)"; by Safe_tac; by (dres_inst_tac [("t", "%h. h`y ")] subst_context 1); @@ -435,7 +435,7 @@ qed "comp_eq_id_iff"; Goalw [bij_def] - "!!f A B. [| f: A->B; g: B->A; f O g = id(B); g O f = id(A) \ + "[| f: A->B; g: B->A; f O g = id(B); g O f = id(A) \ \ |] ==> f : bij(A,B)"; by (asm_full_simp_tac (simpset() addsimps [comp_eq_id_iff]) 1); by (REPEAT (ares_tac [conjI, f_imp_injective, f_imp_surjective] 1 @@ -455,7 +455,7 @@ (*Theorem by KG, proof by LCP*) Goal - "!!f g. [| f: inj(A,B); g: inj(C,D); B Int D = 0 |] ==> \ + "[| 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); @@ -466,7 +466,7 @@ qed "inj_disjoint_Un"; Goalw [surj_def] - "!!f g. [| f: surj(A,B); g: surj(C,D); A Int C = 0 |] ==> \ + "[| f: surj(A,B); g: surj(C,D); A Int C = 0 |] ==> \ \ (f Un g) : surj(A Un C, B Un D)"; by (blast_tac (claset() addIs [fun_disjoint_apply1, fun_disjoint_apply2, fun_disjoint_Un, trans]) 1); @@ -475,7 +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 g. [| f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 |] ==> \ + "[| 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); @@ -500,7 +500,7 @@ qed "restrict_image"; Goalw [inj_def] - "!!f. [| f: inj(A,B); C<=A |] ==> restrict(f,C): inj(C,B)"; + "[| f: inj(A,B); C<=A |] ==> restrict(f,C): inj(C,B)"; by (safe_tac (claset() addSEs [restrict_type2])); by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp, subsetD, box_equals, restrict] 1)); @@ -514,7 +514,7 @@ qed "restrict_surj"; Goalw [inj_def,bij_def] - "!!f. [| f: inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C)"; + "[| f: inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C)"; by (blast_tac (claset() addSIs [restrict, restrict_surj] addIs [box_equals, surj_is_fun]) 1); qed "restrict_bij"; @@ -537,7 +537,7 @@ qed "inj_succ_restrict"; Goalw [inj_def] - "!!f. [| f: inj(A,B); a~:A; b~:B |] ==> \ + "[| f: inj(A,B); a~:A; b~:B |] ==> \ \ cons(,f) : inj(cons(a,A), cons(b,B))"; by (fast_tac (claset() addIs [apply_type] addss (simpset() addsimps [fun_extend, fun_extend_apply2, diff -r 1ea751ae62b2 -r 825877190618 src/ZF/QPair.ML --- a/src/ZF/QPair.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/QPair.ML Wed Jul 15 14:13:18 1998 +0200 @@ -3,8 +3,6 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -For QPair.thy. - Quine-inspired ordered pairs and disjoint sums, for non-well-founded data structures in ZF. Does not precisely follow Quine's construction. Thanks to Thomas Forster for suggesting this approach! @@ -140,8 +138,7 @@ (asm_simp_tac (simpset() addsimps prems) 1) ]); Goalw [qsplit_def] - "!!u. u: A<*>B ==> \ -\ R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = --> R(c(x,y)))"; + "u: A<*>B ==> R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = --> R(c(x,y)))"; by Auto_tac; qed "expand_qsplit"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/QUniv.ML --- a/src/ZF/QUniv.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/QUniv.ML Wed Jul 15 14:13:18 1998 +0200 @@ -26,12 +26,12 @@ (** Introduction and elimination rules avoid tiresome folding/unfolding **) Goalw [quniv_def] - "!!X A. X <= univ(eclose(A)) ==> X : quniv(A)"; + "X <= univ(eclose(A)) ==> X : quniv(A)"; by (etac PowI 1); qed "qunivI"; Goalw [quniv_def] - "!!X A. X : quniv(A) ==> X <= univ(eclose(A))"; + "X : quniv(A) ==> X <= univ(eclose(A))"; by (etac PowD 1); qed "qunivD"; @@ -74,7 +74,7 @@ (*Quine ordered pairs*) Goalw [QPair_def] - "!!A a. [| a <= univ(A); b <= univ(A) |] ==> <= univ(A)"; + "[| a <= univ(A); b <= univ(A) |] ==> <= univ(A)"; by (REPEAT (ares_tac [sum_subset_univ] 1)); qed "QPair_subset_univ"; @@ -99,7 +99,7 @@ (*Quine ordered pairs*) Goalw [quniv_def,QPair_def] - "!!A a. [| a: quniv(A); b: quniv(A) |] ==> : quniv(A)"; + "[| a: quniv(A); b: quniv(A) |] ==> : quniv(A)"; by (REPEAT (dtac PowD 1)); by (REPEAT (ares_tac [PowI, sum_subset_univ] 1)); qed "QPair_in_quniv"; @@ -114,7 +114,7 @@ (*The opposite inclusion*) Goalw [quniv_def,QPair_def] - "!!A a b. : quniv(A) ==> a: quniv(A) & b: quniv(A)"; + " : quniv(A) ==> a: quniv(A) & b: quniv(A)"; by (etac ([Transset_eclose RS Transset_univ, PowD] MRS Transset_includes_summands RS conjE) 1); by (REPEAT (ares_tac [conjI,PowI] 1)); @@ -199,7 +199,7 @@ (*** Intersecting with Vfrom... ***) Goalw [QPair_def,sum_def] - "!!X. Transset(X) ==> \ + "Transset(X) ==> \ \ Int Vfrom(X, succ(i)) <= "; by (stac Int_Un_distrib 1); by (rtac Un_mono 1); @@ -212,7 +212,7 @@ (*Rule for level i -- preserving the level, not decreasing it*) Goalw [QPair_def] - "!!X. Transset(X) ==> \ + "Transset(X) ==> \ \ Int Vfrom(X,i) <= "; by (etac (Transset_Vfrom RS Transset_sum_Int_subset) 1); qed "QPair_Int_Vfrom_subset"; @@ -222,7 +222,7 @@ [Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] MRS subset_trans); Goal - "!!i. [| Ord(i) \ + "[| Ord(i) \ \ |] ==> Int Vset(i) <= (UN j:i. )"; by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac); (*0 case*) diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Rel.ML --- a/src/ZF/Rel.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Rel.ML Wed Jul 15 14:13:18 1998 +0200 @@ -3,7 +3,7 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge -For Rel.thy. Relations in Zermelo-Fraenkel Set Theory +Relations in Zermelo-Fraenkel Set Theory *) open Rel; @@ -49,12 +49,12 @@ (* transitivity *) Goalw [trans_def] - "!!r. [| trans(r); :r; :r |] ==> :r"; + "[| trans(r); :r; :r |] ==> :r"; by (Blast_tac 1); qed "transD"; Goalw [trans_on_def] - "!!r. [| trans[A](r); :r; :r; a:A; b:A; c:A |] ==> :r"; + "[| trans[A](r); :r; :r; a:A; b:A; c:A |] ==> :r"; by (Blast_tac 1); qed "trans_onD"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Resid/Confluence.ML --- a/src/ZF/Resid/Confluence.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Resid/Confluence.ML Wed Jul 15 14:13:18 1998 +0200 @@ -12,7 +12,7 @@ (* ------------------------------------------------------------------------- *) Goalw [confluence_def,strip_def] - "!!u.[|confluence(Spar_red1)|]==> strip"; + "[|confluence(Spar_red1)|]==> strip"; by (resolve_tac [impI RS allI RS allI] 1); by (etac Spar_red.induct 1); by (Fast_tac 1); @@ -21,16 +21,14 @@ Goalw [confluence_def,strip_def] - "!!u. strip==> confluence(Spar_red)"; + "strip==> confluence(Spar_red)"; by (resolve_tac [impI RS allI RS allI] 1); by (etac Spar_red.induct 1); -by (Fast_tac 1); +by (Blast_tac 1); by (Clarify_tac 1); by (dres_inst_tac [("x1","z")] (spec RS mp) 1); -by (REPEAT(eresolve_tac [exE,conjE] 2)); -by (dres_inst_tac [("x1","ua")] (spec RS mp) 2); -by (fast_tac (claset() addIs [Spar_red.trans]) 3); -by (TRYALL assume_tac ); +by (blast_tac (claset() addIs [Spar_red.trans]) 2); +by (assume_tac 1); qed "strip_lemma_l"; (* ------------------------------------------------------------------------- *) @@ -52,7 +50,7 @@ parallel_moves RS strip_lemma_r RS strip_lemma_l); Goalw [confluence_def] - "!!u.[|confluence(Spar_red)|]==> confluence(Sred)"; + "[|confluence(Spar_red)|]==> confluence(Sred)"; by (blast_tac (claset() addIs [par_red_red, red_par_red]) 1); val lemma1 = result(); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Resid/Cube.ML --- a/src/ZF/Resid/Cube.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Resid/Cube.ML Wed Jul 15 14:13:18 1998 +0200 @@ -17,8 +17,7 @@ (* ------------------------------------------------------------------------- *) (* Having more assumptions than needed -- removed below *) -Goal - "!!u. v<==u ==> \ +Goal "v<==u ==> \ \ regular(u)-->(ALL w. w~v-->w~u--> \ \ w |> u = (w|>v) |> (u|>v))"; by (etac Ssub.induct 1); @@ -31,8 +30,7 @@ by (asm_full_simp_tac prism_ss 1); qed_spec_mp "prism_l"; -Goal - "!!u.[|v <== u; regular(u); w~v|]==> \ +Goal "[|v <== u; regular(u); w~v|]==> \ \ w |> u = (w|>v) |> (u|>v)"; by (rtac prism_l 1); by (rtac comp_trans 4); @@ -45,8 +43,7 @@ (* Levy's Cube Lemma *) (* ------------------------------------------------------------------------- *) -Goal - "!!u.[|u~v; regular(v); regular(u); w~u|]==> \ +Goal "[|u~v; regular(v); regular(u); w~u|]==> \ \ (w|>u) |> (v|>u) = (w|>v) |> (u|>v)"; by (stac preservation 1 THEN assume_tac 1 THEN assume_tac 1); @@ -68,8 +65,7 @@ (* paving theorem *) (* ------------------------------------------------------------------------- *) -Goal - "!!u.[|w~u; w~v; regular(u); regular(v)|]==> \ +Goal "[|w~u; w~v; regular(u); regular(v)|]==> \ \ EX uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\ \ regular(vu) & (w|>v)~uv & regular(uv) "; by (subgoal_tac "u~v" 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Resid/Reduction.ML --- a/src/ZF/Resid/Reduction.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Resid/Reduction.ML Wed Jul 15 14:13:18 1998 +0200 @@ -43,28 +43,24 @@ by (ALLGOALS (Asm_simp_tac )); qed "red_Fun"; -Goal - "!!u.[|n:lambda; m ---> m'|]==> Apl(m,n)--->Apl(m',n)"; +Goal "[|n:lambda; m ---> m'|]==> Apl(m,n)--->Apl(m',n)"; by (etac Sred.induct 1); by (resolve_tac [Sred.trans] 3); by (ALLGOALS (Asm_simp_tac )); qed "red_Apll"; -Goal - "!!u.[|n:lambda; m ---> m'|]==> Apl(n,m)--->Apl(n,m')"; +Goal "[|n:lambda; m ---> m'|]==> Apl(n,m)--->Apl(n,m')"; by (etac Sred.induct 1); by (resolve_tac [Sred.trans] 3); by (ALLGOALS (Asm_simp_tac )); qed "red_Aplr"; -Goal - "!!u.[|m ---> m'; n--->n'|]==> Apl(m,n)--->Apl(m',n')"; +Goal "[|m ---> m'; n--->n'|]==> Apl(m,n)--->Apl(m',n')"; by (res_inst_tac [("n","Apl(m',n)")] Sred.trans 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [red_Apll,red_Aplr]) )); qed "red_Apl"; -Goal - "!!u.[|m:lambda; m':lambda; n:lambda; n':lambda; m ---> m'; n--->n'|]==> \ +Goal "[|m:lambda; m':lambda; n:lambda; n':lambda; m ---> m'; n--->n'|]==> \ \ Apl(Fun(m),n)---> n'/m'"; by (res_inst_tac [("n","Apl(Fun(m'),n')")] Sred.trans 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [red_Apl,red_Fun]) )); @@ -104,8 +100,7 @@ (* Simulation *) (* ------------------------------------------------------------------------- *) -Goal - "!!u. m=1=>n ==> EX v. m|>v = n & m~v & regular(v)"; +Goal "m=1=>n ==> EX v. m|>v = n & m~v & regular(v)"; by (etac Spar_red1.induct 1); by Safe_tac; by (ALLGOALS (REPEAT o (resolve_tac [exI,conjI]))); @@ -118,15 +113,13 @@ (* commuting of unmark and subst *) (* ------------------------------------------------------------------------- *) -Goal - "!!u. u:redexes ==> \ +Goal "u:redexes ==> \ \ ALL k:nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)"; by (eresolve_tac [redexes.induct] 1); by (ALLGOALS (asm_full_simp_tac (addsplit (simpset())))); qed "unmmark_lift_rec"; -Goal - "!!u. v:redexes ==> ALL k:nat. ALL u:redexes. \ +Goal "v:redexes ==> ALL k:nat. ALL u:redexes. \ \ unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)"; by (eresolve_tac [redexes.induct] 1); by (ALLGOALS (asm_full_simp_tac @@ -138,16 +131,14 @@ (* Completeness *) (* ------------------------------------------------------------------------- *) -Goal - "!!u. u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)"; +Goal "u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)"; by (etac Scomp.induct 1); by (ALLGOALS (asm_full_simp_tac (reducL_ss addsimps [unmmark_subst_rec]) )); by (dres_inst_tac [("psi", "Fun(?u) =1=> ?w")] asm_rl 1); by (asm_full_simp_tac reducL_ss 1); qed_spec_mp "completeness_l"; -Goal - "!!u.[|u:lambda; u~v; regular(v)|]==> u =1=> unmark(u|>v)"; +Goal "[|u:lambda; u~v; regular(v)|]==> u =1=> unmark(u|>v)"; by (dtac completeness_l 1); by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lambda_unmark]) )); qed "completeness"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Resid/Residuals.ML --- a/src/ZF/Resid/Residuals.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Resid/Residuals.ML Wed Jul 15 14:13:18 1998 +0200 @@ -43,14 +43,12 @@ (* residuals is a partial function *) (* ------------------------------------------------------------------------- *) -Goal - "!!u. residuals(u,v,w) ==> ALL w1. residuals(u,v,w1) --> w1 = w"; +Goal "residuals(u,v,w) ==> ALL w1. residuals(u,v,w1) --> w1 = w"; by (etac Sres.induct 1); by (ALLGOALS Fast_tac); qed_spec_mp "residuals_function"; -Goal - "!!u. u~v ==> regular(v) --> (EX w. residuals(u,v,w))"; +Goal "u~v ==> regular(v) --> (EX w. residuals(u,v,w))"; by (etac Scomp.induct 1); by (ALLGOALS Fast_tac); qed "residuals_intro"; @@ -74,29 +72,29 @@ addSEs [comp_resfuncE]); Goalw [res_func_def] - "!!n. n:nat ==> Var(n) |> Var(n) = Var(n)"; + "n:nat ==> Var(n) |> Var(n) = Var(n)"; by (fast_tac resfunc_cs 1); qed "res_Var"; Goalw [res_func_def] - "!!n.[|s~t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)"; + "[|s~t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)"; by (fast_tac resfunc_cs 1); qed "res_Fun"; Goalw [res_func_def] - "!!n.[|s~u; regular(u); t~v; regular(v); b:bool|]==> \ + "[|s~u; regular(u); t~v; regular(v); b:bool|]==> \ \ App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)"; by (fast_tac resfunc_cs 1); qed "res_App"; Goalw [res_func_def] - "!!n.[|s~u; regular(u); t~v; regular(v); b:bool|]==> \ + "[|s~u; regular(u); t~v; regular(v); b:bool|]==> \ \ App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)"; by (fast_tac resfunc_cs 1); qed "res_redex"; Goal - "!!n.[|s~t; regular(t)|]==> regular(t) --> s |> t:redexes"; + "[|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] @@ -118,20 +116,17 @@ (* Commutation theorem *) (* ------------------------------------------------------------------------- *) -Goal - "!!u. u<==v ==> u~v"; +Goal "u<==v ==> u~v"; by (etac Ssub.induct 1); by (ALLGOALS Asm_simp_tac); qed "sub_comp"; -Goal - "!!u. u<==v ==> regular(v) --> regular(u)"; +Goal "u<==v ==> regular(v) --> regular(u)"; by (etac Ssub.induct 1); by (ALLGOALS (asm_simp_tac res1L_ss)); qed "sub_preserve_reg"; -Goal - "!!u.[|u~v; k:nat|]==> regular(v)--> (ALL n:nat. \ +Goal "[|u~v; k:nat|]==> regular(v)--> (ALL n:nat. \ \ lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))"; by (etac Scomp.induct 1); by Safe_tac; @@ -140,8 +135,7 @@ by (Asm_full_simp_tac 1); qed "residuals_lift_rec"; -Goal - "!!u. u1~u2 ==> ALL v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->\ +Goal "u1~u2 ==> ALL v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->\ \ (ALL n:nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \ \ subst_rec(v1 |> v2, u1 |> u2,n))"; by (etac Scomp.induct 1); @@ -153,8 +147,7 @@ qed "residuals_subst_rec"; -Goal - "!!u.[|u1~u2; v1~v2; regular(u2); regular(v2)|]==>\ +Goal "[|u1~u2; v1~v2; regular(u2); regular(v2)|]==>\ \ (v1/u1) |> (v2/u2) = (v1 |> v2)/(u1 |> u2)"; by (asm_simp_tac (simpset() addsimps ([residuals_subst_rec])) 1); qed "commutation"; @@ -163,8 +156,7 @@ (* Residuals are comp and regular *) (* ------------------------------------------------------------------------- *) -Goal - "!!u. u~v ==> ALL w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)"; +Goal "u~v ==> ALL w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)"; by (etac Scomp.induct 1); by (ALLGOALS (asm_simp_tac res1L_ss)); by (dresolve_tac [spec RS mp RS mp RS mp] 1 @@ -175,8 +167,7 @@ qed_spec_mp "residuals_preserve_comp"; -Goal - "!!u. u~v ==> regular(u) --> regular(v) --> regular(u|>v)"; +Goal "u~v ==> regular(u) --> regular(v) --> regular(u|>v)"; by (etac Scomp.induct 1); by Safe_tac; by (TRYALL (dres_inst_tac [("psi", "regular(Fun(?u) |> ?v)")] asm_rl)); @@ -187,14 +178,12 @@ (* Preservation lemma *) (* ------------------------------------------------------------------------- *) -Goal - "!!u. u~v ==> v ~ (u un v)"; +Goal "u~v ==> v ~ (u un v)"; by (etac Scomp.induct 1); by (ALLGOALS Asm_full_simp_tac); qed "union_preserve_comp"; -Goal - "!!u. u ~ v ==> regular(v) --> u|>v = (u un v)|>v"; +Goal "u ~ v ==> regular(v) --> u|>v = (u un v)|>v"; by (etac Scomp.induct 1); by Safe_tac; by (dres_inst_tac [("psi", "Fun(?u) |> ?v = ?w")] asm_rl 3); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Resid/SubUnion.ML --- a/src/ZF/Resid/SubUnion.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Resid/SubUnion.ML Wed Jul 15 14:13:18 1998 +0200 @@ -22,19 +22,19 @@ (* ------------------------------------------------------------------------- *) Goalw [union_def] - "!!u. n:nat==>Var(n) un Var(n)=Var(n)"; + "n:nat==>Var(n) un Var(n)=Var(n)"; by (Asm_simp_tac 1); by (simp_tac (rank_ss addsimps redexes.con_defs) 1); qed "union_Var"; Goalw [union_def] - "!!u.[|u:redexes; v:redexes|]==>Fun(u) un Fun(v)=Fun(u un v)"; + "[|u:redexes; v:redexes|]==>Fun(u) un Fun(v)=Fun(u un v)"; by (Asm_simp_tac 1); by (simp_tac (rank_ss addsimps redexes.con_defs) 1); qed "union_Fun"; Goalw [union_def] - "!!u.[|b1:bool; b2:bool; u1:redexes; v1:redexes; u2:redexes; v2:redexes|]==> \ + "[|b1:bool; b2:bool; u1:redexes; v1:redexes; u2:redexes; v2:redexes|]==> \ \ App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)"; by (Asm_simp_tac 1); by (simp_tac (rank_ss addsimps redexes.con_defs) 1); @@ -70,20 +70,17 @@ by (ALLGOALS Fast_tac); qed "comp_refl"; -Goal - "!!u. u ~ v ==> v ~ u"; +Goal "u ~ v ==> v ~ u"; by (etac Scomp.induct 1); by (ALLGOALS Fast_tac); qed "comp_sym"; -Goal - "u ~ v <-> v ~ u"; +Goal "u ~ v <-> v ~ u"; by (fast_tac (claset() addIs [comp_sym]) 1); qed "comp_sym_iff"; -Goal - "!!u. u ~ v ==> ALL w. v ~ w-->u ~ w"; +Goal "u ~ v ==> ALL w. v ~ w-->u ~ w"; by (etac Scomp.induct 1); by (ALLGOALS Fast_tac); qed_spec_mp "comp_trans"; @@ -92,22 +89,19 @@ (* union proofs *) (* ------------------------------------------------------------------------- *) -Goal - "!!u. u ~ v ==> u <== (u un v)"; +Goal "u ~ v ==> u <== (u un v)"; by (etac Scomp.induct 1); by (etac boolE 3); by (ALLGOALS Asm_full_simp_tac); qed "union_l"; -Goal - "!!u. u ~ v ==> v <== (u un v)"; +Goal "u ~ v ==> v <== (u un v)"; by (etac Scomp.induct 1); by (eres_inst_tac [("c","b2")] boolE 3); by (ALLGOALS Asm_full_simp_tac); qed "union_r"; -Goal - "!!u. u ~ v ==> u un v = v un u"; +Goal "u ~ v ==> u un v = v un u"; by (etac Scomp.induct 1); by (ALLGOALS(asm_simp_tac (simpset() addsimps [or_commute]))); qed "union_sym"; @@ -116,8 +110,7 @@ (* regular proofs *) (* ------------------------------------------------------------------------- *) -Goal - "!!u. u ~ v ==> regular(u)-->regular(v)-->regular(u un v)"; +Goal "u ~ v ==> regular(u)-->regular(v)-->regular(u un v)"; by (etac Scomp.induct 1); by (ALLGOALS(asm_full_simp_tac (simpset() setloop(SELECT_GOAL Safe_tac)))); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Resid/Substitution.ML --- a/src/ZF/Resid/Substitution.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Resid/Substitution.ML Wed Jul 15 14:13:18 1998 +0200 @@ -43,28 +43,28 @@ (* lift_rec equality rules *) (* ------------------------------------------------------------------------- *) Goalw [lift_rec_def] - "!!n.[|n:nat; i:nat|]==> lift_rec(Var(i),n) =if(i lift_rec(Var(i),n) =if(i lift_rec(Var(i),k) = Var(succ(i))"; + "[|n:nat; i:nat; k:nat; k le i|]==> lift_rec(Var(i),k) = Var(succ(i))"; by (Asm_full_simp_tac 1); qed "lift_rec_le"; Goalw [lift_rec_def] - "!!n.[|i:nat; k:nat; i lift_rec(Var(i),k) = Var(i)"; + "[|i:nat; k:nat; i lift_rec(Var(i),k) = Var(i)"; by (Asm_full_simp_tac 1); qed "lift_rec_gt"; Goalw [lift_rec_def] - "!!n.[|n:nat; k:nat|]==> \ + "[|n:nat; k:nat|]==> \ \ lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))"; by (Asm_full_simp_tac 1); qed "lift_rec_Fun"; Goalw [lift_rec_def] - "!!n.[|n:nat; k:nat|]==> \ + "[|n:nat; k:nat|]==> \ \ lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))"; by (Asm_full_simp_tac 1); qed "lift_rec_App"; @@ -74,36 +74,36 @@ (* ------------------------------------------------------------------------- *) Goalw [subst_rec_def] - "!!n.[|i:nat; k:nat; u:redexes|]==> \ + "[|i:nat; k:nat; u:redexes|]==> \ \ subst_rec(u,Var(i),k) = if(k subst_rec(u,Var(n),n) = u"; + "[|n:nat; u:redexes|]==> subst_rec(u,Var(n),n) = u"; by (asm_full_simp_tac (simpset()) 1); qed "subst_eq"; Goalw [subst_rec_def] - "!!n.[|n:nat; u:redexes; p:nat; p \ + "[|n:nat; u:redexes; p:nat; p \ \ subst_rec(u,Var(n),p) = Var(n#-1)"; by (asm_full_simp_tac (simpset()) 1); qed "subst_gt"; Goalw [subst_rec_def] - "!!n.[|n:nat; u:redexes; p:nat; n \ + "[|n:nat; u:redexes; p:nat; n \ \ subst_rec(u,Var(n),p) = Var(n)"; by (asm_full_simp_tac (simpset() addsimps [gt_not_eq,leI]) 1); qed "subst_lt"; Goalw [subst_rec_def] - "!!n.[|p:nat; u:redexes|]==> \ + "[|p:nat; u:redexes|]==> \ \ subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) "; by (asm_full_simp_tac (simpset()) 1); qed "subst_Fun"; Goalw [subst_rec_def] - "!!n.[|p:nat; u:redexes|]==> \ + "[|p:nat; u:redexes|]==> \ \ subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))"; by (asm_full_simp_tac (simpset()) 1); qed "subst_App"; @@ -113,15 +113,14 @@ Goal - "!!n. u:redexes ==> ALL k:nat. lift_rec(u,k):redexes"; + "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]))); qed "lift_rec_type_a"; val lift_rec_type = lift_rec_type_a RS bspec; -Goalw [] - "!!n. v:redexes ==> ALL n:nat. ALL u:redexes. subst_rec(u,v,n):redexes"; +Goal "v:redexes ==> ALL n:nat. ALL u:redexes. subst_rec(u,v,n):redexes"; by (eresolve_tac [redexes.induct] 1); by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps [subst_Fun,subst_App, @@ -139,36 +138,31 @@ (* lift and substitution proofs *) (* ------------------------------------------------------------------------- *) -Goalw [] - "!!n. u:redexes ==> ALL n:nat. ALL i:nat. i le n --> \ +Goal "u:redexes ==> ALL n:nat. ALL i:nat. i le n --> \ \ (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))"; -by ((eresolve_tac [redexes.induct] 1) - THEN (ALLGOALS Asm_simp_tac)); +by ((eresolve_tac [redexes.induct] 1) THEN (ALLGOALS Asm_simp_tac)); by Safe_tac; -by (excluded_middle_tac "na < xa" 1); +by (excluded_middle_tac "n < xa" 1); by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2)); -by (ALLGOALS(asm_full_simp_tac - ((addsplit (simpset())) addsimps [leI]))); +by (ALLGOALS (asm_full_simp_tac (addsplit (simpset()) addsimps [leI]))); qed "lift_lift_rec"; -Goalw [] - "!!n.[|u:redexes; n:nat|]==> \ +Goal "[|u:redexes; n:nat|]==> \ \ lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))"; by (asm_simp_tac (simpset() addsimps [lift_lift_rec]) 1); qed "lift_lift"; -Goal - "!!n. v:redexes ==> \ +Goal "v:redexes ==> \ \ ALL n:nat. ALL m:nat. ALL u:redexes. n le m-->\ \ lift_rec(subst_rec(u,v,n),m) = \ \ subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)"; by ((eresolve_tac [redexes.induct] 1) THEN (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift])))); by Safe_tac; -by (excluded_middle_tac "na < x" 1); +by (excluded_middle_tac "n < x" 1); by (asm_full_simp_tac (simpset()) 1); -by (eres_inst_tac [("j","na")] leE 1); +by (eres_inst_tac [("j","n")] leE 1); by (asm_full_simp_tac ((addsplit (simpset())) addsimps [leI,gt_pred,succ_pred]) 1); by (hyp_subst_tac 1); @@ -178,48 +172,45 @@ by (asm_full_simp_tac (simpset() addsimps [leI]) 1); qed "lift_rec_subst_rec"; -Goalw [] - "!!n.[|v:redexes; u:redexes; n:nat|]==> \ +Goal "[|v:redexes; u:redexes; n:nat|]==> \ \ lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))"; by (asm_full_simp_tac (simpset() addsimps [lift_rec_subst_rec]) 1); qed "lift_subst"; -Goalw [] - "!!n. v:redexes ==> \ +Goal "v:redexes ==> \ \ ALL n:nat. ALL m:nat. ALL u:redexes. m le n-->\ \ lift_rec(subst_rec(u,v,n),m) = \ \ subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))"; by ((eresolve_tac [redexes.induct] 1) THEN (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift])))); by Safe_tac; -by (excluded_middle_tac "na < x" 1); +by (excluded_middle_tac "n < x" 1); by (asm_full_simp_tac (simpset()) 1); by (eres_inst_tac [("i","x")] leE 1); by (forward_tac [lt_trans1] 1 THEN assume_tac 1); by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [succ_pred,leI,gt_pred]))); by (asm_full_simp_tac (simpset() addsimps [leI]) 1); -by (excluded_middle_tac "na < xa" 1); +by (excluded_middle_tac "n < xa" 1); by (asm_full_simp_tac (simpset()) 1); by (asm_full_simp_tac (simpset() addsimps [leI]) 1); qed "lift_rec_subst_rec_lt"; -Goalw [] - "!!n. u:redexes ==> \ +Goal "u:redexes ==> \ \ ALL n:nat. ALL v:redexes. subst_rec(v,lift_rec(u,n),n) = u"; by ((eresolve_tac [redexes.induct] 1) THEN (ALLGOALS Asm_simp_tac)); by Safe_tac; -by (excluded_middle_tac "na < x" 1); -(* x <= na *) +by (excluded_middle_tac "n < x" 1); +(* x <= n *) by (asm_full_simp_tac (simpset()) 1); by (asm_full_simp_tac (simpset()) 1); qed "subst_rec_lift_rec"; Goal - "!!n. v:redexes ==> \ + "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)"; @@ -227,7 +218,7 @@ (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift RS sym,lift_rec_subst_rec_lt])))); by Safe_tac; -by (excluded_middle_tac "na le succ(xa)" 1); +by (excluded_middle_tac "n le succ(xa)" 1); by (asm_full_simp_tac (simpset()) 1); by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1); by (etac leE 1); @@ -236,12 +227,12 @@ by (forw_inst_tac [("i","x")] (nat_into_Ord RS le_refl RS lt_trans) 1 THEN assume_tac 1); by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 1); -by (eres_inst_tac [("i","na")] leE 1); +by (eres_inst_tac [("i","n")] leE 1); by (asm_full_simp_tac (simpset() addsimps [succ_pred,subst_rec_lift_rec,leI]) 2); -by (excluded_middle_tac "na < x" 1); +by (excluded_middle_tac "n < x" 1); by (asm_full_simp_tac (simpset()) 1); -by (eres_inst_tac [("j","na")] leE 1); +by (eres_inst_tac [("j","n")] leE 1); by (asm_simp_tac (simpset() addsimps [gt_pred]) 1); by (asm_simp_tac (simpset() addsimps [subst_rec_lift_rec]) 1); by (forward_tac [lt_trans2] 1 THEN assume_tac 1); @@ -249,8 +240,7 @@ qed "subst_rec_subst_rec"; -Goalw [] - "!!n.[|v:redexes; u:redexes; w:redexes; n:nat|]==> \ +Goal "[|v:redexes; u:redexes; w:redexes; n:nat|]==> \ \ subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)"; by (asm_simp_tac (simpset() addsimps [subst_rec_subst_rec]) 1); qed "substitution"; @@ -261,28 +251,24 @@ (* ------------------------------------------------------------------------- *) -Goal - "!!n.[|n:nat; u ~ v|]==> ALL m:nat. lift_rec(u,m) ~ lift_rec(v,m)"; +Goal "[|n:nat; u ~ v|]==> ALL m:nat. lift_rec(u,m) ~ lift_rec(v,m)"; by (etac Scomp.induct 1); by (ALLGOALS(asm_simp_tac (simpset() addsimps [comp_refl]))); qed "lift_rec_preserve_comp"; -Goal - "!!n. u2 ~ v2 ==> ALL m:nat. ALL u1:redexes. ALL v1:redexes.\ +Goal "u2 ~ v2 ==> ALL m:nat. ALL u1:redexes. ALL v1:redexes.\ \ u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)"; by (etac Scomp.induct 1); by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps ([lift_rec_preserve_comp,comp_refl])))); qed "subst_rec_preserve_comp"; -Goal - "!!n. regular(u) ==> ALL m:nat. regular(lift_rec(u,m))"; +Goal "regular(u) ==> ALL m:nat. regular(lift_rec(u,m))"; by (eresolve_tac [Sreg.induct] 1); by (ALLGOALS(asm_full_simp_tac (addsplit (simpset())))); qed "lift_rec_preserve_reg"; -Goal - "!!n. regular(v) ==> \ +Goal "regular(v) ==> \ \ ALL m:nat. ALL u:redexes. regular(u)-->regular(subst_rec(u,v,m))"; by (eresolve_tac [Sreg.induct] 1); by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Resid/Terms.ML --- a/src/ZF/Resid/Terms.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Resid/Terms.ML Wed Jul 15 14:13:18 1998 +0200 @@ -11,18 +11,15 @@ (* unmark simplifications *) (* ------------------------------------------------------------------------- *) -Goalw [unmark_def] - "unmark(Var(n)) = Var(n)"; +Goalw [unmark_def] "unmark(Var(n)) = Var(n)"; by (Asm_simp_tac 1); qed "unmark_Var"; -Goalw [unmark_def] - "unmark(Fun(t)) = Fun(unmark(t))"; +Goalw [unmark_def] "unmark(Fun(t)) = Fun(unmark(t))"; by (Asm_simp_tac 1); qed "unmark_Fun"; -Goalw [unmark_def] - "unmark(App(b,n,m)) = App(0,unmark(n),unmark(m))"; +Goalw [unmark_def] "unmark(App(b,n,m)) = App(0,unmark(n),unmark(m))"; by (Asm_simp_tac 1); qed "unmark_App"; @@ -42,13 +39,12 @@ (* ------------------------------------------------------------------------- *) Goalw [unmark_def] - "!!u. u:redexes ==> unmark(u):lambda"; + "u:redexes ==> unmark(u):lambda"; by (eresolve_tac [redexes.induct] 1); by (ALLGOALS Asm_simp_tac); qed "unmark_type"; -Goal - "!!u. u:lambda ==> unmark(u) = u"; +Goal "u:lambda ==> unmark(u) = u"; by (eresolve_tac [lambda.induct] 1); by (ALLGOALS Asm_simp_tac); qed "lambda_unmark"; @@ -58,15 +54,13 @@ (* lift and subst preserve lambda *) (* ------------------------------------------------------------------------- *) -Goal - "!!u.[|v:lambda|]==> ALL k:nat. lift_rec(v,k):lambda"; +Goal "[|v:lambda|]==> ALL k:nat. lift_rec(v,k):lambda"; by (eresolve_tac [lambda.induct] 1); by (ALLGOALS(asm_full_simp_tac (addsplit (simpset())))); qed "liftL_typea"; val liftL_type =liftL_typea RS bspec ; -Goal - "!!n.[|v:lambda|]==> ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda"; +Goal "[|v:lambda|]==> ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda"; by (eresolve_tac [lambda.induct] 1); by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps [liftL_type]))); qed "substL_typea"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Sum.ML --- a/src/ZF/Sum.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Sum.ML Wed Jul 15 14:13:18 1998 +0200 @@ -16,7 +16,7 @@ qed "Part_iff"; Goalw [Part_def] - "!!a b A h. [| a : A; a=h(b) |] ==> a : Part(A,h)"; + "[| a : A; a=h(b) |] ==> a : Part(A,h)"; by (Blast_tac 1); qed "Part_eqI"; @@ -152,7 +152,7 @@ qed "case_type"; Goal - "!!u. u: A+B ==> \ + "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))))"; @@ -168,8 +168,7 @@ by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); qed "case_cong"; -Goal - "!!z. z: A+B ==> \ +Goal "z: A+B ==> \ \ case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = \ \ case(%x. c(c'(x)), %y. d(d'(y)), z)"; by Auto_tac; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Univ.ML --- a/src/ZF/Univ.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Univ.ML Wed Jul 15 14:13:18 1998 +0200 @@ -96,14 +96,13 @@ by Safe_tac; qed "singleton_in_Vfrom"; -Goal - "!!A. [| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))"; +Goal "[| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))"; by (rtac subset_mem_Vfrom 1); by Safe_tac; qed "doubleton_in_Vfrom"; Goalw [Pair_def] - "!!A. [| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> \ + "[| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> \ \ : Vfrom(A,succ(succ(i)))"; by (REPEAT (ares_tac [doubleton_in_Vfrom] 1)); qed "Pair_in_Vfrom"; @@ -245,12 +244,12 @@ qed "one_in_VLimit"; Goalw [Inl_def] - "!!A a. [| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)"; + "[| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)"; by (REPEAT (ares_tac [zero_in_VLimit, Pair_in_VLimit] 1)); qed "Inl_in_VLimit"; Goalw [Inr_def] - "!!A b. [| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)"; + "[| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)"; by (REPEAT (ares_tac [one_in_VLimit, Pair_in_VLimit] 1)); qed "Inr_in_VLimit"; @@ -284,8 +283,7 @@ by (Blast_tac 1); qed "Transset_Pair_subset"; -Goal - "!!a b.[| <= Vfrom(A,i); Transset(A); Limit(i) |] ==> \ +Goal "[| <= Vfrom(A,i); Transset(A); Limit(i) |] ==> \ \ : Vfrom(A,i)"; by (etac (Transset_Pair_subset RS conjE) 1); by (etac Transset_Vfrom 1); @@ -317,8 +315,7 @@ (** products **) -Goal - "!!A. [| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] ==> \ +Goal "[| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] ==> \ \ a*b : Vfrom(A, succ(succ(succ(j))))"; by (dtac Transset_Vfrom 1); by (rtac subset_mem_Vfrom 1); @@ -337,7 +334,7 @@ (** Disjoint sums, aka Quine ordered pairs **) Goalw [sum_def] - "!!A. [| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A); 1:j |] ==> \ + "[| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A); 1:j |] ==> \ \ a+b : Vfrom(A, succ(succ(succ(j))))"; by (dtac Transset_Vfrom 1); by (rtac subset_mem_Vfrom 1); @@ -357,7 +354,7 @@ (** function space! **) Goalw [Pi_def] - "!!A. [| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] ==> \ + "[| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] ==> \ \ a->b : Vfrom(A, succ(succ(succ(succ(j)))))"; by (dtac Transset_Vfrom 1); by (rtac subset_mem_Vfrom 1); @@ -380,7 +377,7 @@ qed "fun_in_VLimit"; Goalw [Pi_def] - "!!A. [| a: Vfrom(A,j); Transset(A) |] ==> \ + "[| a: Vfrom(A,j); Transset(A) |] ==> \ \ Pow(a) : Vfrom(A, succ(succ(j)))"; by (dtac Transset_Vfrom 1); by (rtac subset_mem_Vfrom 1); @@ -390,7 +387,7 @@ qed "Pow_in_Vfrom"; Goal - "!!a. [| a: Vfrom(A,i); Limit(i); Transset(A) |] ==> Pow(a) : Vfrom(A,i)"; + "[| 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); @@ -563,12 +560,12 @@ qed "singleton_in_univ"; Goalw [univ_def] - "!!A a. [| a: univ(A); b: univ(A) |] ==> {a,b} : univ(A)"; + "[| a: univ(A); b: univ(A) |] ==> {a,b} : univ(A)"; by (REPEAT (ares_tac [doubleton_in_VLimit, Limit_nat] 1)); qed "doubleton_in_univ"; Goalw [univ_def] - "!!A a. [| a: univ(A); b: univ(A) |] ==> : univ(A)"; + "[| a: univ(A); b: univ(A) |] ==> : univ(A)"; by (REPEAT (ares_tac [Pair_in_VLimit, Limit_nat] 1)); qed "Pair_in_univ"; @@ -630,8 +627,7 @@ (** Closure under finite powerset **) -Goal - "!!i. [| b: Fin(Vfrom(A,i)); Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j EX j. b <= Vfrom(A,j) & j n -> Vfrom(A,i) <= Vfrom(A,i)"; +Goal "[| n: nat; Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)"; by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1); by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, nat_subset_VLimit, subset_refl] 1)); @@ -673,8 +668,7 @@ (** Closure under finite function space **) (*General but seldom-used version; normally the domain is fixed*) -Goal - "!!i. Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)"; +Goal "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)"; by (resolve_tac [FiniteFun.dom_subset RS subset_trans] 1); by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, subset_refl] 1)); val FiniteFun_VLimit1 = result(); @@ -684,19 +678,17 @@ val FiniteFun_univ1 = result(); (*Version for a fixed domain*) -Goal - "!!i. [| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)"; +Goal "[| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)"; by (eresolve_tac [subset_refl RSN (2, FiniteFun_mono) RS subset_trans] 1); by (etac FiniteFun_VLimit1 1); val FiniteFun_VLimit = result(); Goalw [univ_def] - "!!W. W <= univ(A) ==> W -||> univ(A) <= univ(A)"; + "W <= univ(A) ==> W -||> univ(A) <= univ(A)"; by (etac (Limit_nat RSN (2, FiniteFun_VLimit)) 1); val FiniteFun_univ = result(); -Goal - "!!W. [| f: W -||> univ(A); W <= univ(A) |] ==> f : univ(A)"; +Goal "[| f: W -||> univ(A); W <= univ(A) |] ==> f : univ(A)"; by (eresolve_tac [FiniteFun_univ RS subsetD] 1); by (assume_tac 1); val FiniteFun_in_univ = result(); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/WF.ML --- a/src/ZF/WF.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/WF.ML Wed Jul 15 14:13:18 1998 +0200 @@ -24,12 +24,12 @@ (** Equivalences between wf and wf_on **) -Goalw [wf_def, wf_on_def] "!!A r. wf(r) ==> wf[A](r)"; +Goalw [wf_def, wf_on_def] "wf(r) ==> wf[A](r)"; by (Clarify_tac 1); (*essential for Blast_tac's efficiency*) by (Blast_tac 1); qed "wf_imp_wf_on"; -Goalw [wf_def, wf_on_def] "!!r. wf[field(r)](r) ==> wf(r)"; +Goalw [wf_def, wf_on_def] "wf[field(r)](r) ==> wf(r)"; by (Fast_tac 1); qed "wf_on_field_imp_wf"; @@ -37,12 +37,12 @@ by (blast_tac (claset() addIs [wf_imp_wf_on, wf_on_field_imp_wf]) 1); qed "wf_iff_wf_on_field"; -Goalw [wf_on_def, wf_def] "!!A B r. [| wf[A](r); B<=A |] ==> wf[B](r)"; +Goalw [wf_on_def, wf_def] "[| wf[A](r); B<=A |] ==> wf[B](r)"; by (Clarify_tac 1); (*essential for Blast_tac's efficiency*) by (Blast_tac 1); qed "wf_on_subset_A"; -Goalw [wf_on_def, wf_def] "!!A r s. [| wf[A](r); s<=r |] ==> wf[A](s)"; +Goalw [wf_on_def, wf_def] "[| wf[A](r); s<=r |] ==> wf[A](s)"; by (Clarify_tac 1); (*essential for Blast_tac's efficiency*) by (Blast_tac 1); qed "wf_on_subset_r"; @@ -162,10 +162,8 @@ (*Needed to prove well_ordI. Could also reason that wf[A](r) means wf(r Int A*A); thus wf( (r Int A*A)^+ ) and use wf_not_refl *) -Goal - "!!r. [| wf[A](r); :r; :r; :r; a:A; b:A; c:A |] ==> P"; -by (subgoal_tac - "ALL y:A. ALL z:A. :r --> :r --> :r --> P" 1); +Goal "[| wf[A](r); :r; :r; :r; a:A; b:A; c:A |] ==> P"; +by (subgoal_tac "ALL y:A. ALL z:A. :r --> :r --> :r --> P" 1); by (wf_on_ind_tac "a" [] 2); by (Blast_tac 2); by (Blast_tac 1); @@ -225,11 +223,10 @@ (*** NOTE! some simplifications need a different solver!! ***) val wf_super_ss = simpset() setSolver indhyp_tac; -val prems = goalw WF.thy [is_recfun_def] +Goalw [is_recfun_def] "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] ==> \ \ :r --> :r --> f`x=g`x"; -by (cut_facts_tac prems 1); -by (wf_ind_tac "x" prems 1); +by (wf_ind_tac "x" [] 1); by (REPEAT (rtac impI 1 ORELSE etac ssubst 1)); by (rewtac restrict_def); by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1); @@ -286,15 +283,14 @@ (*** Unfolding wftrec ***) -val prems = goal WF.thy - "[| wf(r); trans(r); :r |] ==> \ -\ restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"; -by (REPEAT (ares_tac (prems @ [is_recfun_cut, unfold_the_recfun]) 1)); +Goal "[| wf(r); trans(r); :r |] ==> \ +\ restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"; +by (REPEAT (ares_tac [is_recfun_cut, unfold_the_recfun] 1)); qed "the_recfun_cut"; (*NOT SUITABLE FOR REWRITING: it is recursive!*) Goalw [wftrec_def] - "!!r. [| wf(r); trans(r) |] ==> \ + "[| wf(r); trans(r) |] ==> \ \ wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))"; by (stac (rewrite_rule [is_recfun_def] unfold_the_recfun) 1); by (ALLGOALS @@ -334,7 +330,7 @@ Goalw [wf_on_def, wfrec_on_def] - "!!A r. [| wf[A](r); a: A |] ==> \ + "[| wf[A](r); a: A |] ==> \ \ wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))"; by (etac (wfrec RS trans) 1); by (asm_simp_tac (simpset() addsimps [vimage_Int_square, cons_subset_iff]) 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/Zorn.ML --- a/src/ZF/Zorn.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/Zorn.ML Wed Jul 15 14:13:18 1998 +0200 @@ -26,12 +26,12 @@ (*** Section 2. The Transfinite Construction ***) Goalw [increasing_def] - "!!f A. f: increasing(A) ==> f: Pow(A)->Pow(A)"; + "f: increasing(A) ==> f: Pow(A)->Pow(A)"; by (etac CollectD1 1); qed "increasingD1"; Goalw [increasing_def] - "!!f A. [| f: increasing(A); x<=A |] ==> x <= f`x"; + "[| f: increasing(A); x<=A |] ==> x <= f`x"; by (eresolve_tac [CollectD2 RS spec RS mp] 1); by (assume_tac 1); qed "increasingD2"; @@ -106,16 +106,14 @@ qed "TFin_linear_lemma2"; (*a more convenient form for Lemma 2*) -Goal - "!!m n. [| n<=m; m: TFin(S,next); n: TFin(S,next); next: increasing(S) \ +Goal "[| n<=m; m: TFin(S,next); n: TFin(S,next); next: increasing(S) \ \ |] ==> n=m | next`n<=m"; by (rtac (TFin_linear_lemma2 RS bspec RS mp) 1); by (REPEAT (assume_tac 1)); qed "TFin_subsetD"; (*Consequences from section 3.3 -- Property 3.2, the ordering is total*) -Goal - "!!m n. [| m: TFin(S,next); n: TFin(S,next); next: increasing(S) \ +Goal "[| m: TFin(S,next); n: TFin(S,next); next: increasing(S) \ \ |] ==> n<=m | m<=n"; by (rtac (TFin_linear_lemma2 RSN (3,TFin_linear_lemma1) RS disjE) 1); by (REPEAT (assume_tac 1) THEN etac disjI2 1); @@ -136,8 +134,7 @@ qed "equal_next_upper"; (*Property 3.3 of section 3.3*) -Goal - "!!m. [| m: TFin(S,next); next: increasing(S) \ +Goal "[| m: TFin(S,next); next: increasing(S) \ \ |] ==> m = next`m <-> m = Union(TFin(S,next))"; by (rtac iffI 1); by (rtac (Union_upper RS equalityI) 1); @@ -167,8 +164,7 @@ by (rtac Collect_subset 1); qed "maxchain_subset_chain"; -Goal - "!!S. [| ch : (PROD X:Pow(chain(S)) - {0}. X); \ +Goal "[| ch : (PROD X:Pow(chain(S)) - {0}. X); \ \ X : chain(S); X ~: maxchain(S) \ \ |] ==> ch ` super(S,X) : super(S,X)"; by (etac apply_type 1); @@ -176,8 +172,7 @@ by (Blast_tac 1); qed "choice_super"; -Goal - "!!S. [| ch : (PROD X:Pow(chain(S)) - {0}. X); \ +Goal "[| ch : (PROD X:Pow(chain(S)) - {0}. X); \ \ X : chain(S); X ~: maxchain(S) \ \ |] ==> ch ` super(S,X) ~= X"; by (rtac notI 1); @@ -188,8 +183,7 @@ qed "choice_not_equals"; (*This justifies Definition 4.4*) -Goal - "!!S. ch: (PROD X: Pow(chain(S))-{0}. X) ==> \ +Goal "ch: (PROD X: Pow(chain(S))-{0}. X) ==> \ \ EX next: increasing(S). ALL X: Pow(S). \ \ next`X = if(X: chain(S)-maxchain(S), ch`super(S,X), X)"; by (rtac bexI 1); @@ -214,7 +208,7 @@ (*Lemma 4*) Goal - "!!S. [| c: TFin(S,next); \ + "[| c: TFin(S,next); \ \ ch: (PROD X: Pow(chain(S))-{0}. X); \ \ next: increasing(S); \ \ ALL X: Pow(S). next`X = \ @@ -258,12 +252,11 @@ (*Used in the proof of Zorn's Lemma*) Goalw [chain_def] - "!!c. [| c: chain(A); z: A; ALL x:c. x<=z |] ==> cons(z,c) : chain(A)"; + "[| c: chain(A); z: A; ALL x:c. x<=z |] ==> cons(z,c) : chain(A)"; by (Blast_tac 1); qed "chain_extend"; -Goal - "!!S. ALL c: chain(S). Union(c) : S ==> EX y:S. ALL z:S. y<=z --> y=z"; +Goal "ALL c: chain(S). Union(c) : S ==> EX y:S. ALL z:S. y<=z --> y=z"; by (resolve_tac [Hausdorff RS exE] 1); by (asm_full_simp_tac (simpset() addsimps [maxchain_def]) 1); by (rename_tac "c" 1); @@ -310,8 +303,7 @@ qed "well_ord_TFin_lemma"; (*This theorem just packages the previous result*) -Goal - "!!S. next: increasing(S) ==> \ +Goal "next: increasing(S) ==> \ \ well_ord(TFin(S,next), Subset_rel(TFin(S,next)))"; by (rtac well_ordI 1); by (rewrite_goals_tac [Subset_rel_def, linear_def]); @@ -341,8 +333,7 @@ qed "choice_Diff"; (*This justifies Definition 6.1*) -Goal - "!!S. ch: (PROD X: Pow(S)-{0}. X) ==> \ +Goal "ch: (PROD X: Pow(S)-{0}. X) ==> \ \ EX next: increasing(S). ALL X: Pow(S). \ \ next`X = if(X=S, S, cons(ch`(S-X), X))"; by (rtac bexI 1); @@ -364,8 +355,7 @@ (*The construction of the injection*) -Goal - "!!S. [| ch: (PROD X: Pow(S)-{0}. X); \ +Goal "[| ch: (PROD X: Pow(S)-{0}. X); \ \ next: increasing(S); \ \ ALL X: Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) \ \ |] ==> (lam x:S. Union({y: TFin(S,next). x~: y})) \ diff -r 1ea751ae62b2 -r 825877190618 src/ZF/equalities.ML --- a/src/ZF/equalities.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/equalities.ML Wed Jul 15 14:13:18 1998 +0200 @@ -491,12 +491,12 @@ qed "vimage_Int_subset"; Goalw [function_def] - "!!f. function(f) ==> f-``(A Int B) = (f-``A) Int (f-``B)"; + "function(f) ==> f-``(A Int B) = (f-``A) Int (f-``B)"; by (Blast_tac 1); qed "function_vimage_Int"; Goalw [function_def] - "!!f. function(f) ==> f-``(A-B) = (f-``A) - (f-``B)"; + "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)"; by (Blast_tac 1); qed "function_vimage_Diff"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/ex/Bin.ML --- a/src/ZF/ex/Bin.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/ex/Bin.ML Wed Jul 15 14:13:18 1998 +0200 @@ -102,41 +102,41 @@ val bin_typechecks0 = bin_rec_type :: bin.intrs; Goalw [integ_of_bin_def] - "!!w. w: bin ==> integ_of_bin(w) : integ"; + "w: bin ==> integ_of_bin(w) : integ"; by (typechk_tac (bin_typechecks0@integ_typechecks@ nat_typechecks@[bool_into_nat])); qed "integ_of_bin_type"; Goalw [norm_Bcons_def] - "!!w. [| w: bin; b: bool |] ==> norm_Bcons(w,b) : bin"; + "[| w: bin; b: bool |] ==> norm_Bcons(w,b) : bin"; by (etac bin.elim 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps bin.case_eqns))); by (typechk_tac (bin_typechecks0@bool_typechecks)); qed "norm_Bcons_type"; Goalw [bin_succ_def] - "!!w. w: bin ==> bin_succ(w) : bin"; + "w: bin ==> bin_succ(w) : bin"; by (typechk_tac ([norm_Bcons_type]@bin_typechecks0@bool_typechecks)); qed "bin_succ_type"; Goalw [bin_pred_def] - "!!w. w: bin ==> bin_pred(w) : bin"; + "w: bin ==> bin_pred(w) : bin"; by (typechk_tac ([norm_Bcons_type]@bin_typechecks0@bool_typechecks)); qed "bin_pred_type"; Goalw [bin_minus_def] - "!!w. w: bin ==> bin_minus(w) : bin"; + "w: bin ==> bin_minus(w) : bin"; by (typechk_tac ([bin_pred_type]@bin_typechecks0@bool_typechecks)); qed "bin_minus_type"; Goalw [bin_add_def] - "!!v w. [| v: bin; w: bin |] ==> bin_add(v,w) : bin"; + "[| v: bin; w: bin |] ==> bin_add(v,w) : bin"; by (typechk_tac ([norm_Bcons_type, bin_succ_type, bin_pred_type]@ bin_typechecks0@ bool_typechecks@ZF_typechecks)); qed "bin_add_type"; Goalw [bin_mult_def] - "!!v w. [| v: bin; w: bin |] ==> bin_mult(v,w) : bin"; + "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin"; by (typechk_tac ([norm_Bcons_type, bin_minus_type, bin_add_type]@ bin_typechecks0@ bool_typechecks)); qed "bin_mult_type"; @@ -177,8 +177,7 @@ (*norm_Bcons preserves the integer value of its argument*) -Goal - "!!w. [| w: bin; b: bool |] ==> \ +Goal "[| w: bin; b: bool |] ==> \ \ integ_of_bin(norm_Bcons(w,b)) = integ_of_bin(Bcons(w,b))"; by (etac bin.elim 1); by (asm_simp_tac (simpset() addsimps norm_Bcons_simps) 3); @@ -186,8 +185,7 @@ by (ALLGOALS (asm_simp_tac (simpset() addsimps (norm_Bcons_simps)))); qed "integ_of_bin_norm_Bcons"; -Goal - "!!w. w: bin ==> integ_of_bin(bin_succ(w)) = $#1 $+ integ_of_bin(w)"; +Goal "w: bin ==> integ_of_bin(bin_succ(w)) = $#1 $+ integ_of_bin(w)"; by (etac bin.induct 1); by (Simp_tac 1); by (Simp_tac 1); @@ -196,8 +194,7 @@ (asm_simp_tac (simpset() addsimps integ_of_bin_norm_Bcons::zadd_ac))); qed "integ_of_bin_succ"; -Goal - "!!w. w: bin ==> integ_of_bin(bin_pred(w)) = $~ ($#1) $+ integ_of_bin(w)"; +Goal "w: bin ==> integ_of_bin(bin_pred(w)) = $~ ($#1) $+ integ_of_bin(w)"; by (etac bin.induct 1); by (Simp_tac 1); by (Simp_tac 1); @@ -214,8 +211,7 @@ Addsimps (bin_recs bin_minus_def @ [integ_of_bin_succ, integ_of_bin_pred]); -Goal - "!!w. w: bin ==> integ_of_bin(bin_minus(w)) = $~ integ_of_bin(w)"; +Goal "w: bin ==> integ_of_bin(bin_minus(w)) = $~ integ_of_bin(w)"; by (etac bin.induct 1); by (Simp_tac 1); by (Simp_tac 1); @@ -244,7 +240,7 @@ qed "bin_add_Bcons_Minus"; Goalw [bin_add_def] - "!!w y. [| w: bin; y: bool |] ==> \ + "[| w: bin; y: bool |] ==> \ \ bin_add(Bcons(v,x), Bcons(w,y)) = \ \ norm_Bcons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)"; by (Asm_simp_tac 1); @@ -257,8 +253,7 @@ Addsimps [bool_subset_nat RS subsetD]; -Goal - "!!v. v: bin ==> \ +Goal "v: bin ==> \ \ ALL w: bin. integ_of_bin(bin_add(v,w)) = \ \ integ_of_bin(v) $+ integ_of_bin(w)"; by (etac bin.induct 1); @@ -329,20 +324,17 @@ (** extra rules for bin_add **) -Goal - "!!w. w: bin ==> bin_add(Bcons(v,1), Bcons(w,1)) = \ +Goal "w: bin ==> bin_add(Bcons(v,1), Bcons(w,1)) = \ \ norm_Bcons(bin_add(v, bin_succ(w)), 0)"; by (Asm_simp_tac 1); qed "bin_add_Bcons_Bcons11"; -Goal - "!!w. w: bin ==> bin_add(Bcons(v,1), Bcons(w,0)) = \ +Goal "w: bin ==> bin_add(Bcons(v,1), Bcons(w,0)) = \ \ norm_Bcons(bin_add(v,w), 1)"; by (Asm_simp_tac 1); qed "bin_add_Bcons_Bcons10"; -Goal - "!!w y. [| w: bin; y: bool |] ==> \ +Goal "[| w: bin; y: bool |] ==> \ \ bin_add(Bcons(v,0), Bcons(w,y)) = norm_Bcons(bin_add(v,w), y)"; by (Asm_simp_tac 1); qed "bin_add_Bcons_Bcons0"; @@ -351,8 +343,7 @@ val [bin_mult_Plus, bin_mult_Minus, _] = bin_recs bin_mult_def; -Goal - "bin_mult(Bcons(v,1), w) = bin_add(norm_Bcons(bin_mult(v,w),0), w)"; +Goal "bin_mult(Bcons(v,1), w) = bin_add(norm_Bcons(bin_mult(v,w),0), w)"; by (Simp_tac 1); qed "bin_mult_Bcons1"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/ex/CoUnit.ML --- a/src/ZF/ex/CoUnit.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/ex/CoUnit.ML Wed Jul 15 14:13:18 1998 +0200 @@ -51,8 +51,7 @@ qed "lfp_Con2_in_counit2"; (*Lemma for proving finality. Borrowed from ex/llist_eq.ML!*) -Goal - "!!i. Ord(i) ==> ALL x y. x: counit2 & y: counit2 --> x Int Vset(i) <= y"; +Goal "Ord(i) ==> ALL x y. x: counit2 & y: counit2 --> x Int Vset(i) <= y"; by (etac trans_induct 1); by (safe_tac subset_cs); by (etac counit2.elim 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/ex/Limit.ML --- a/src/ZF/ex/Limit.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/ex/Limit.ML Wed Jul 15 14:13:18 1998 +0200 @@ -1105,12 +1105,12 @@ (*----------------------------------------------------------------------*) Goalw [set_def,iprod_def] (* iprodI *) - "!!z. x:(PROD n:nat. set(DD`n)) ==> x:set(iprod(DD))"; + "x:(PROD n:nat. set(DD`n)) ==> x:set(iprod(DD))"; by (Asm_full_simp_tac 1); qed "iprodI"; Goalw [set_def,iprod_def] (* iprodE *) - "!!z. x:set(iprod(DD)) ==> x:(PROD n:nat. set(DD`n))"; + "x:set(iprod(DD)) ==> x:(PROD n:nat. set(DD`n))"; by (Asm_full_simp_tac 1); qed "iprodE"; @@ -1296,17 +1296,17 @@ *) Goalw [set_def,mkcpo_def] (* mkcpoD1 *) - "!!z. x:set(mkcpo(D,P))==> x:set(D)"; + "x:set(mkcpo(D,P))==> x:set(D)"; by (Asm_full_simp_tac 1); qed "mkcpoD1"; Goalw [set_def,mkcpo_def] (* mkcpoD2 *) - "!!z. x:set(mkcpo(D,P))==> P(x)"; + "x:set(mkcpo(D,P))==> P(x)"; by (Asm_full_simp_tac 1); qed "mkcpoD2"; Goalw [rel_def,mkcpo_def] (* rel_mkcpoE *) - "!!a. rel(mkcpo(D,P),x,y) ==> rel(D,x,y)"; + "rel(mkcpo(D,P),x,y) ==> rel(D,x,y)"; by (Asm_full_simp_tac 1); qed "rel_mkcpoE"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/ex/ListN.ML --- a/src/ZF/ex/ListN.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/ex/ListN.ML Wed Jul 15 14:13:18 1998 +0200 @@ -36,8 +36,7 @@ qed "listn_mono"; Goal - "!!n l. [| : listn(A); : listn(A) |] ==> \ -\ : listn(A)"; + "[| : 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 1ea751ae62b2 -r 825877190618 src/ZF/ex/Primes.ML --- a/src/ZF/ex/Primes.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/ex/Primes.ML Wed Jul 15 14:13:18 1998 +0200 @@ -56,7 +56,7 @@ qed "egcd_0"; Goalw [egcd_def] - "!!m. [| 0 egcd(m,n) = egcd(n, m mod n)"; + "[| 0 egcd(m,n) = egcd(n, m mod n)"; by (res_inst_tac [("P", "%z. ?left(z) = ?right")] (transrec RS ssubst) 1); by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq RS not_sym, mod_less_divisor RS ltD]) 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/ex/Primrec.ML --- a/src/ZF/ex/Primrec.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/ex/Primrec.ML Wed Jul 15 14:13:18 1998 +0200 @@ -25,32 +25,32 @@ simpset_ref() := simpset() setSolver (type_auto_tac pr_typechecks); Goalw [SC_def] - "!!x l. [| x:nat; l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)"; + "[| x:nat; l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)"; by (Asm_simp_tac 1); qed "SC"; Goalw [CONST_def] - "!!l. [| l: list(nat) |] ==> CONST(k) ` l = k"; + "[| l: list(nat) |] ==> CONST(k) ` l = k"; by (Asm_simp_tac 1); qed "CONST"; Goalw [PROJ_def] - "!!l. [| x: nat; l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x"; + "[| x: nat; l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x"; by (Asm_simp_tac 1); qed "PROJ_0"; Goalw [COMP_def] - "!!l. [| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]"; + "[| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]"; by (Asm_simp_tac 1); qed "COMP_1"; Goalw [PREC_def] - "!!l. l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l"; + "l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l"; by (Asm_simp_tac 1); qed "PREC_0"; Goalw [PREC_def] - "!!l. [| x:nat; l: list(nat) |] ==> \ + "[| x:nat; l: list(nat) |] ==> \ \ PREC(f,g) ` (Cons(succ(x),l)) = \ \ g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))"; by (Asm_simp_tac 1); @@ -99,7 +99,7 @@ (*Could be proved in Primrec0, like the previous two cases, but using primrec_into_fun makes type-checking easier!*) Goalw [ACK_def] - "!!i j. [| i:nat; j:nat |] ==> \ + "[| i:nat; j:nat |] ==> \ \ ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))"; by (asm_simp_tac (simpset() addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1); qed "ack_succ_succ"; @@ -135,15 +135,13 @@ qed "ack_lt_mono2"; (*PROPERTY A 5', monotonicity for le *) -Goal - "!!i j k. [| j le k; i: nat; k:nat |] ==> ack(i,j) le ack(i,k)"; +Goal "[| j le k; i: nat; k:nat |] ==> ack(i,j) le ack(i,k)"; by (res_inst_tac [("f", "%j. ack(i,j)")] Ord_lt_mono_imp_le_mono 1); by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS nat_into_Ord] 1)); qed "ack_le_mono2"; (*PROPERTY A 6*) -Goal - "!!i j. [| i:nat; j:nat |] ==> ack(i, succ(j)) le ack(succ(i), j)"; +Goal "[| i:nat; j:nat |] ==> ack(i, succ(j)) le ack(succ(i), j)"; by (nat_ind_tac "j" [] 1); by (ALLGOALS Asm_simp_tac); by (rtac ack_le_mono2 1); @@ -168,8 +166,7 @@ qed "ack_lt_mono1"; (*PROPERTY A 7', monotonicity for le *) -Goal - "!!i j k. [| i le j; j:nat; k:nat |] ==> ack(i,k) le ack(j,k)"; +Goal "[| i le j; j:nat; k:nat |] ==> ack(i,k) le ack(j,k)"; by (res_inst_tac [("f", "%j. ack(j,k)")] Ord_lt_mono_imp_le_mono 1); by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS nat_into_Ord] 1)); qed "ack_le_mono1"; @@ -187,8 +184,7 @@ qed "ack_2"; (*PROPERTY A 10*) -Goal - "!!i1 i2 j. [| i1:nat; i2:nat; j:nat |] ==> \ +Goal "[| i1:nat; i2:nat; j:nat |] ==> \ \ ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)"; by (rtac (ack2_le_ack1 RSN (2,lt_trans2)) 1); by (Asm_simp_tac 1); @@ -198,8 +194,7 @@ qed "ack_nest_bound"; (*PROPERTY A 11*) -Goal - "!!i1 i2 j. [| i1:nat; i2:nat; j:nat |] ==> \ +Goal "[| i1:nat; i2:nat; j:nat |] ==> \ \ ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)"; by (res_inst_tac [("j", "ack(succ(1), ack(i1 #+ i2, j))")] lt_trans 1); by (asm_simp_tac (simpset() addsimps [ack_2]) 1); @@ -212,8 +207,7 @@ (*PROPERTY A 12. Article uses existential quantifier but the ALF proof used k#+4. Quantified version must be nested EX k'. ALL i,j... *) -Goal - "!!i j k. [| i < ack(k,j); j:nat; k:nat |] ==> \ +Goal "[| i < ack(k,j); j:nat; k:nat |] ==> \ \ i#+j < ack(succ(succ(succ(succ(k)))), j)"; by (res_inst_tac [("j", "ack(k,j) #+ ack(0,j)")] lt_trans 1); by (rtac (ack_add_bound RS lt_trans2) 2); @@ -226,7 +220,7 @@ Addsimps [list_add_type, nat_into_Ord]; Goalw [SC_def] - "!!l. l: list(nat) ==> SC ` l < ack(1, list_add(l))"; + "l: list(nat) ==> SC ` l < ack(1, list_add(l))"; by (etac list.elim 1); by (asm_simp_tac (simpset() addsimps [succ_iff]) 1); by (asm_simp_tac (simpset() addsimps [ack_1, add_le_self]) 1); @@ -241,12 +235,12 @@ qed "lt_ack1"; Goalw [CONST_def] - "!!l. [| l: list(nat); k: nat |] ==> CONST(k) ` l < ack(k, list_add(l))"; + "[| l: list(nat); k: nat |] ==> CONST(k) ` l < ack(k, list_add(l))"; by (asm_simp_tac (simpset() addsimps [lt_ack1]) 1); qed "CONST_case"; Goalw [PROJ_def] - "!!l. l: list(nat) ==> ALL i:nat. PROJ(i) ` l < ack(0, list_add(l))"; + "l: list(nat) ==> ALL i:nat. PROJ(i) ` l < ack(0, list_add(l))"; by (Asm_simp_tac 1); by (etac list.induct 1); by (asm_simp_tac (simpset() addsimps [nat_0_le]) 1); @@ -264,7 +258,7 @@ (** COMP case **) Goal - "!!fs. fs : list({f: primrec . \ + "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). \ @@ -283,7 +277,7 @@ qed "COMP_map_lemma"; Goalw [COMP_def] - "!!g. [| kg: nat; \ + "[| kg: nat; \ \ ALL l:list(nat). g`l < ack(kg, list_add(l)); \ \ fs : list({f: primrec . \ \ EX kf:nat. ALL l:list(nat). \ @@ -303,7 +297,7 @@ (** PREC case **) Goalw [PREC_def] - "!!f g. [| ALL l:list(nat). f`l #+ list_add(l) < ack(kf, list_add(l)); \ + "[| ALL l:list(nat). f`l #+ list_add(l) < ack(kf, list_add(l)); \ \ ALL l:list(nat). g`l #+ list_add(l) < ack(kg, list_add(l)); \ \ f: primrec; kf: nat; \ \ g: primrec; kg: nat; \ @@ -333,13 +327,11 @@ by (tc_tac []); qed "PREC_case_lemma"; -Goal - "!!f g. [| f: primrec; kf: nat; \ -\ g: primrec; kg: nat; \ -\ ALL l:list(nat). f`l < ack(kf, list_add(l)); \ -\ ALL l:list(nat). g`l < ack(kg, list_add(l)) \ -\ |] ==> EX k:nat. ALL l: list(nat). \ -\ PREC(f,g)`l< ack(k, list_add(l))"; +Goal "[| f: primrec; kf: nat; \ +\ g: primrec; kg: nat; \ +\ ALL l:list(nat). f`l < ack(kf, list_add(l)); \ +\ ALL l:list(nat). g`l < ack(kg, list_add(l)) \ +\ |] ==> EX k:nat. ALL l: list(nat). PREC(f,g)`l< ack(k, list_add(l))"; by (rtac (ballI RS bexI) 1); by (rtac ([add_le_self, PREC_case_lemma] MRS lt_trans1) 1); by (REPEAT @@ -349,8 +341,7 @@ rtac (ack_add_bound2 RS ballI) THEN' etac bspec]))); qed "PREC_case"; -Goal - "!!f. f:primrec ==> EX k:nat. ALL l:list(nat). f`l < ack(k, list_add(l))"; +Goal "f:primrec ==> EX k:nat. ALL l:list(nat). f`l < ack(k, list_add(l))"; by (etac primrec.induct 1); by Safe_tac; by (DEPTH_SOLVE @@ -358,8 +349,7 @@ bexI, ballI] @ nat_typechecks) 1)); qed "ack_bounds_primrec"; -Goal - "~ (lam l:list(nat). list_case(0, %x xs. ack(x,x), l)) : primrec"; +Goal "~ (lam l:list(nat). list_case(0, %x xs. ack(x,x), l)) : primrec"; by (rtac notI 1); by (etac (ack_bounds_primrec RS bexE) 1); by (rtac lt_irrefl 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/ex/Ramsey.ML --- a/src/ZF/ex/Ramsey.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/ex/Ramsey.ML Wed Jul 15 14:13:18 1998 +0200 @@ -27,7 +27,7 @@ qed "Clique0"; Goalw [Clique_def] - "!!C V E. [| Clique(C,V',E); V'<=V |] ==> Clique(C,V,E)"; + "[| Clique(C,V',E); V'<=V |] ==> Clique(C,V,E)"; by (Fast_tac 1); qed "Clique_superset"; @@ -35,8 +35,7 @@ by (Fast_tac 1); qed "Indept0"; -val prems = goalw Ramsey.thy [Indept_def] - "!!I V E. [| Indept(I,V',E); V'<=V |] ==> Indept(I,V,E)"; +Goalw [Indept_def] "[| Indept(I,V',E); V'<=V |] ==> Indept(I,V,E)"; by (Fast_tac 1); qed "Indept_superset"; @@ -47,17 +46,17 @@ qed "Atleast0"; Goalw [Atleast_def] - "!!m A. Atleast(succ(m),A) ==> EX x:A. Atleast(m, A-{x})"; + "Atleast(succ(m),A) ==> EX x:A. Atleast(m, A-{x})"; by (fast_tac (claset() addEs [inj_is_fun RS apply_type, inj_succ_restrict]) 1); qed "Atleast_succD"; Goalw [Atleast_def] - "!!n A. [| Atleast(n,A); A<=B |] ==> Atleast(n,B)"; + "[| Atleast(n,A); A<=B |] ==> Atleast(n,B)"; by (fast_tac (claset() addEs [inj_weaken_type]) 1); qed "Atleast_superset"; Goalw [Atleast_def,succ_def] - "!!m. [| Atleast(m,B); b~: B |] ==> Atleast(succ(m), cons(b,B))"; + "[| Atleast(m,B); b~: B |] ==> Atleast(succ(m), cons(b,B))"; by (etac exE 1); by (rtac exI 1); by (etac inj_extend 1); @@ -65,8 +64,7 @@ by (assume_tac 1); qed "Atleast_succI"; -Goal - "!!m. [| Atleast(m, B-{x}); x: B |] ==> Atleast(succ(m), B)"; +Goal "[| Atleast(m, B-{x}); x: B |] ==> Atleast(succ(m), B)"; by (etac (Atleast_succI RS Atleast_superset) 1); by (Fast_tac 1); by (Fast_tac 1); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/ex/Rmap.ML --- a/src/ZF/ex/Rmap.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/ex/Rmap.ML Wed Jul 15 14:13:18 1998 +0200 @@ -27,8 +27,7 @@ Sigma_mono, list_mono] 1)); qed "rmap_rel_type"; -Goal - "!!r. A <= domain(r) ==> list(A) <= domain(rmap(r))"; +Goal "A <= domain(r) ==> list(A) <= domain(rmap(r))"; by (rtac subsetI 1); by (etac list.induct 1); by (ALLGOALS Fast_tac); diff -r 1ea751ae62b2 -r 825877190618 src/ZF/ex/TF.ML --- a/src/ZF/ex/TF.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/ex/TF.ML Wed Jul 15 14:13:18 1998 +0200 @@ -143,7 +143,7 @@ Addsimps [list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons]; Goalw [list_of_TF_def] - "!!z A. z: tree_forest(A) ==> list_of_TF(z) : list(tree(A))"; + "z: tree_forest(A) ==> list_of_TF(z) : list(tree(A))"; by (REPEAT (ares_tac ([TF_rec_type,TconsI] @ list_typechecks) 1)); qed "list_of_TF_type"; @@ -151,7 +151,7 @@ Addsimps [TF_of_list_Nil,TF_of_list_Cons]; Goalw [TF_of_list_def] - "!!l A. l: list(tree(A)) ==> TF_of_list(l) : forest(A)"; + "l: list(tree(A)) ==> TF_of_list(l) : forest(A)"; by (REPEAT (ares_tac [list_rec_type, FnilI, FconsI] 1)); qed "TF_of_list_type"; @@ -176,7 +176,7 @@ Addsimps [TF_size_Tcons, TF_size_Fnil, TF_size_Fcons]; Goalw [TF_size_def] - "!!z A. z: tree_forest(A) ==> TF_size(z) : nat"; + "z: tree_forest(A) ==> TF_size(z) : nat"; by (REPEAT (ares_tac [TF_rec_type, add_type, nat_0I, nat_succI] 1)); qed "TF_size_type"; @@ -188,7 +188,7 @@ Addsimps [TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons]; Goalw [TF_preorder_def] - "!!z A. z: tree_forest(A) ==> TF_preorder(z) : list(A)"; + "z: tree_forest(A) ==> TF_preorder(z) : list(A)"; by (REPEAT (ares_tac ([TF_rec_type, app_type] @ list.intrs) 1)); qed "TF_preorder_type"; @@ -221,8 +221,7 @@ by (ALLGOALS Asm_simp_tac); qed "forest_iso"; -Goal - "!!ts. ts: list(tree(A)) ==> list_of_TF(TF_of_list(ts)) = ts"; +Goal "ts: list(tree(A)) ==> list_of_TF(TF_of_list(ts)) = ts"; by (etac list.induct 1); by (ALLGOALS Asm_simp_tac); qed "tree_list_iso"; @@ -234,22 +233,19 @@ by (ALLGOALS Asm_simp_tac); qed "TF_map_ident"; -Goal - "!!z A. z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u. h(j(u)), z)"; +Goal "z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u. h(j(u)), z)"; by (etac tree_forest.induct 1); by (ALLGOALS Asm_simp_tac); qed "TF_map_compose"; (** theorems about TF_size **) -Goal - "!!z A. z: tree_forest(A) ==> TF_size(TF_map(h,z)) = TF_size(z)"; +Goal "z: tree_forest(A) ==> TF_size(TF_map(h,z)) = TF_size(z)"; by (etac tree_forest.induct 1); by (ALLGOALS Asm_simp_tac); qed "TF_size_TF_map"; -Goal - "!!z A. z: tree_forest(A) ==> TF_size(z) = length(TF_preorder(z))"; +Goal "z: tree_forest(A) ==> TF_size(z) = length(TF_preorder(z))"; by (etac tree_forest.induct 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app]))); qed "TF_size_length"; diff -r 1ea751ae62b2 -r 825877190618 src/ZF/ex/Term.ML --- a/src/ZF/ex/Term.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/ex/Term.ML Wed Jul 15 14:13:18 1998 +0200 @@ -158,7 +158,7 @@ bind_thm ("preorder", (preorder_def RS def_term_rec)); Goalw [preorder_def] - "!!t A. t: term(A) ==> preorder(t) : list(A)"; + "t: term(A) ==> preorder(t) : list(A)"; by (REPEAT (ares_tac [term_rec_simple_type, list.Cons_I, flat_type] 1)); qed "preorder_type"; @@ -182,14 +182,12 @@ by (asm_simp_tac (simpset() addsimps [map_ident]) 1); qed "term_map_ident"; -Goal - "!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u. f(g(u)), t)"; +Goal "t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u. f(g(u)), t)"; by (etac term_induct_eqn 1); by (asm_simp_tac (simpset() addsimps [map_compose]) 1); qed "term_map_compose"; -Goal - "!!t A. t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))"; +Goal "t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))"; by (etac term_induct_eqn 1); by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym, map_compose]) 1); qed "term_map_reflect"; @@ -197,8 +195,7 @@ (** theorems about term_size **) -Goal - "!!t A. t: term(A) ==> term_size(term_map(f,t)) = term_size(t)"; +Goal "t: term(A) ==> term_size(term_map(f,t)) = term_size(t)"; by (etac term_induct_eqn 1); by (asm_simp_tac (simpset() addsimps [map_compose]) 1); qed "term_size_term_map"; @@ -226,8 +223,7 @@ (** theorems about preorder **) -Goal - "!!t A. t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))"; +Goal "t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))"; by (etac term_induct_eqn 1); by (asm_simp_tac (simpset() addsimps [map_compose, map_flat]) 1); qed "preorder_term_map";