More tidying and removal of "\!\!... from Goal commands
--- 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";
--- 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);
--- 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<m; m:nat; l:nat; \
@@ -418,7 +418,7 @@
qed "ex_eq_succ";
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)}; \
@@ -503,7 +503,7 @@
qed "well_ord_subsets_lepoll_n";
Goalw [LL_def, MM_def]
- "!!x. t_n <= {v:Pow(x Un y). v eqpoll n} \
+ "t_n <= {v:Pow(x Un y). v eqpoll n} \
\ ==> 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));
--- 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";
--- 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);
--- 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);
--- 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);
--- 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,B2> & B1 eqpoll B2 \
+ "ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2 \
\ ==> 0 ~: { bij(fst(B),snd(B)). B:A }";
by (rtac notI 1);
by (etac RepFunE 1);
--- 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);
--- 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. <f``k, f`k> : R}); \
+"[| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \
\ ALL n:nat. <f`n, f`succ(n)> : \
\ {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1)) \
\ & restrict(z2, domain(z1)) = z1}; \
@@ -137,7 +137,7 @@
val lemma2 = result();
Goal
-"!!X.[| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \
+"[| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \
\ ALL n:nat. <f`n, f`succ(n)> : \
\ {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1)) \
\ & restrict(z2, domain(z1)) = z1}; \
@@ -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. <f`k, f`succ(k)> : R}); \
\ RR = {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f)) \
\ & (ALL f:z1. restrict(z2, domain(f)) = f)) | \
@@ -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(<n, y>, 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<nat. <f``b, f`b> : \
+"[| ALL b<nat. <f``b, f`b> : \
\ {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f)) & \
\ (ALL f:z1. restrict(z2, domain(f)) = f)) | \
\ (~ (EX g:XX. domain(g)=succ(UN f:z1. domain(f)) & \
@@ -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. <f`k, f`succ(k)> : R}); \
\ ALL b<nat. <f``b, f`b> : \
\ {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f)) \
@@ -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);
--- 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";
--- 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})";
--- 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();
--- 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";
--- 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<n; m:nat; n:nat |] ==> m div n : nat";
+ "[| 0<n; m:nat; n:nat |] ==> 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);
--- 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";
--- 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. <x,b>")] 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<L |] ==> K le (K |*| L)";
+ "[| Card(K); Ord(L); 0<L |] ==> 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 <w,y>:A*B. <f`w, fa`y>")] exI 1);
by (res_inst_tac [("d", "%<w,y>.<converse(f)`w, converse(fa)`y>")]
@@ -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 <x,y>:K*K. <x Un y, x, y>) : inj(K*K, K*K*K)";
+ "Ord(K) ==> (lam <x,y>:K*K. <x Un y, x, y>) : 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<K; y<K; z<K |] ==> \
+ "[| x<K; y<K; z<K |] ==> \
\ <<x,y>, <z,z>> : 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<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)";
+ "z<K ==> pred(K*K, <z,z>, 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<z; y<z; z<K |] ==> <<x,y>, <z,z>> : csquare_rel(K)";
+ "[| x<z; y<z; z<K |] ==> <<x,y>, <z,z>> : csquare_rel(K)";
by (subgoals_tac ["x<K", "y<K"] 1);
by (REPEAT (eresolve_tac [asm_rl, lt_trans] 2));
by (REPEAT (etac ltE 1));
@@ -425,7 +425,7 @@
(*Part of the traditional proof. UNUSED since it's harder to prove & apply *)
Goalw [csquare_rel_def]
- "!!K. [| x le z; y le z; z<K |] ==> \
+ "[| x le z; y le z; z<K |] ==> \
\ <<x,y>, <z,z>> : csquare_rel(K) | x=z & y=z";
by (subgoals_tac ["x<K", "y<K"] 1);
by (REPEAT (eresolve_tac [asm_rl, lt_trans1] 2));
@@ -440,8 +440,7 @@
(** The cardinality of initial segments **)
-Goal
- "!!K. [| Limit(K); x<K; y<K; z=succ(x Un y) |] ==> \
+Goal "[| Limit(K); x<K; y<K; z=succ(x Un y) |] ==> \
\ ordermap(K*K, csquare_rel(K)) ` <x,y> < \
\ ordermap(K*K, csquare_rel(K)) ` <z,z>";
by (subgoals_tac ["z<K", "well_ord(K*K, csquare_rel(K))"] 1);
@@ -456,7 +455,7 @@
(*Kunen: "each <x,y>: K*K has no more than z*z predecessors..." (page 29) *)
Goalw [cmult_def]
- "!!K. [| Limit(K); x<K; y<K; z=succ(x Un y) |] ==> \
+ "[| Limit(K); x<K; y<K; z=succ(x Un y) |] ==> \
\ | ordermap(K*K, csquare_rel(K)) ` <x,y> | 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<L |] ==> csucc(K) le L";
+ "[| Card(L); K<L |] ==> 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]);
--- 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*)
--- 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; \
\ <te, e_fn(x, e), t>:ElabRel; ve_dom(ve) = te_dom(te); \
\ {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}: \
\ Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |] ==> \
@@ -47,7 +47,7 @@
(* Properties of the pointwise extension to environments *)
Goalw [hastyenv_def]
- "!!ve.[| ve:ValEnv; te:TyEnv; hastyenv(ve,te); <v,t>:HasTyRel |] ==> \
+ "[| ve:ValEnv; te:TyEnv; hastyenv(ve,te); <v,t>: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);
--- 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);<te,e_const(c),t>:ElabRel |] ==> \
+Goal "[| c:Const; hastyenv(ve,te);<te,e_const(c),t>:ElabRel |] ==> \
\ <v_const(c), t> : HasTyRel";
by (Fast_tac 1);
qed "consistency_const";
Goalw [hastyenv_def]
- "!!t. [| x:ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel |] ==> \
+ "[| x:ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel |] ==> \
\ <ve_app(ve,x),t>: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); \
\ <te,e_fn(x,e),t>:ElabRel \
\ |] ==> <v_clos(x, e, ve), t> : HasTyRel";
by (Best_tac 1);
@@ -143,8 +142,7 @@
fun mt_cases_tac t = ((rtac t 1) THEN (TRYALL assume_tac));
-Goal
- "!!e. <ve,e,v>:EvalRel ==> \
+Goal "<ve,e,v>:EvalRel ==> \
\ (ALL t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)";
by (etac EvalRel.induct 1);
by (safe_tac ZF_cs);
--- 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);
--- 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);
--- 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);
--- 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";
--- 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. <x,y> : r --> <y,x> : 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); <a,b>: r |] ==> r``{a} <= r``{b}";
+ "[| sym(r); trans(r); <a,b>: r |] ==> r``{a} <= r``{b}";
by (Blast_tac 1);
qed "equiv_class_subset";
Goalw [equiv_def]
- "!!A r. [| equiv(A,r); <a,b>: r |] ==> r``{a} = r``{b}";
+ "[| equiv(A,r); <a,b>: 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 |] ==> <a,b>: r";
+ "[| equiv(A,r); r``{b} <= r``{a}; b: A |] ==> <a,b>: 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}) |] ==> <a,b>: r";
+ "[| equiv(A,r); x: (r``{a} Int r``{b}) |] ==> <a,b>: r";
by (Blast_tac 1);
qed "equiv_class_nondisjoint";
@@ -79,13 +79,13 @@
qed "equiv_type";
Goal
- "!!A r. equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A";
+ "equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A";
by (blast_tac (claset() addIs [eq_equiv_class, equiv_class_eq]
addDs [equiv_type]) 1);
qed "equiv_class_eq_iff";
Goal
- "!!A r. [| equiv(A,r); x: A; y: A |] ==> r``{x} = r``{y} <-> <x,y>: r";
+ "[| equiv(A,r); x: A; y: A |] ==> r``{x} = r``{y} <-> <x,y>: r";
by (blast_tac (claset() addIs [eq_equiv_class, equiv_class_eq]
addDs [equiv_type]) 1);
qed "eq_equiv_class_iff";
@@ -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";
--- 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);
--- 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";
--- 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";
--- 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<n --> P(m,n))";
by (etac nat_induct 1);
by (ALLGOALS (*blast_tac gives PROOF FAILED*)
--- 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); <y,x>:r; x:A; y:A \
+ "[| trans[A](r); <y,x>: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); <x,y>: r; x:A; y:A |] ==> \
+ "[| f: ord_iso(A,r,B,s); <x,y>: r; x:A; y:A |] ==> \
\ <f`x, f`y> : s";
by (Blast_tac 1);
qed "ord_iso_apply";
Goalw [ord_iso_def]
- "!!f. [| f: ord_iso(A,r,B,s); <x,y>: s; x:B; y:B |] ==> \
+ "[| f: ord_iso(A,r,B,s); <x,y>: s; x:B; y:B |] ==> \
\ <converse(f) ` x, converse(f) ` y> : 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 |] \
\ ==> ~ <f`y, y>: 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); <a,c>: r; \
+ "[| well_ord(A,r); well_ord(B,s); <a,c>: r; \
\ f : ord_iso(pred(A,a,r), r, pred(B,b,s), s); \
\ g : ord_iso(pred(A,c,r), r, pred(B,d,s), s); \
\ a:A; c:A; b:B; d:B |] ==> <b,d>: s";
@@ -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 |] \
\ ==> ~ <g`y, f`y> : 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);
--- 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. <<a',b'>, <a,b>> : rmult(A,r,B,s) <-> \
+ "<<a',b'>, <a,b>> : rmult(A,r,B,s) <-> \
\ (<a',a>: r & a':A & a:A & b': B & 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 <x,y>:A*B. <f`x, g`y>) : bij(A*B, C*D)";
by (res_inst_tac [("d", "%<x,y>. <converse(f)`x, converse(g)`y>")]
lam_bijective 1);
@@ -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 <x,y>:A*B. <f`x, g`y>) \
\ : 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. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))";
by (resolve_tac [singleton_prod_bij RS ord_isoI] 1);
by (Asm_simp_tac 1);
@@ -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.<a,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.<a,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";
--- 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<i ==> pred(i, j, Memrel(i)) = j";
+ "j<i ==> 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<i; f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R";
+ "[| j<i; f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R";
by (forward_tac [lt_pred_Memrel] 1);
by (etac ltE 1);
by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN
@@ -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. [| <w,x>: r; wf[A](r); w: A; x: A |] ==> \
+ "[| <w,x>: r; wf[A](r); w: A; x: A |] ==> \
\ ordermap(A,r)`w : ordermap(A,r)`x";
by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
by (assume_tac 1);
@@ -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 |] ==> <w,x>: 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<j |] ==> \
+ "[| well_ord(A,r); k<j |] ==> \
\ ordertype(A+k, radd(A, r, k, Memrel(j))) = \
\ ordertype(A+k, radd(A, r, k, Memrel(k)))";
by (etac ltE 1);
@@ -451,7 +451,7 @@
qed "oadd_lt_mono2";
Goal
- "!!i j k. [| i++j < i++k; Ord(i); Ord(j); Ord(k) |] ==> 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
@@ -459,12 +459,12 @@
qed "oadd_lt_cancel2";
Goal
- "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> i++j < i++k <-> j<k";
+ "[| Ord(i); Ord(j); Ord(k) |] ==> i++j < i++k <-> j<k";
by (blast_tac (claset() addSIs [oadd_lt_mono2] addSDs [oadd_lt_cancel2]) 1);
qed "oadd_lt_iff2";
Goal
- "!!i j k. [| i++j = i++k; Ord(i); Ord(j); Ord(k) |] ==> 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<i | (EX l:j. k = i++l )";
+ "[| k < i++j; Ord(i); Ord(j) |] ==> k<i | (EX l:j. k = i++l )";
(*Rotate the hypotheses so that simplification will work*)
by (etac revcut_rl 1);
by (asm_full_simp_tac
@@ -491,7 +491,7 @@
(*** Ordinal addition with successor -- via associativity! ***)
Goalw [oadd_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 ([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, <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, <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; j'<j |] ==> \
+ "[| i'<i; j'<j |] ==> \
\ ordertype(pred(i*j, <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<j**i |] ==> \
+ "[| Ord(i); Ord(j); k<j**i |] ==> \
\ EX j' i'. k = j**i' ++ j' & j'<j & i'<i";
by (asm_full_simp_tac (simpset() addsimps [ordertype_pred_unfold,
well_ord_rmult, well_ord_Memrel]) 1);
@@ -718,7 +718,7 @@
qed "lt_omult";
Goalw [omult_def]
- "!!i j. [| j'<j; i'<i |] ==> j**i' ++ j' < j**i";
+ "[| j'<j; i'<i |] ==> 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'<j; 0<i |] ==> i'**j' < i**j";
+Goal "[| i' le i; j'<j; 0<i |] ==> 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));
--- 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) ==> <a,b> : Memrel(A) <-> a:b & b:A";
+ "Transset(A) ==> <a,b> : 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<i; ALL y. succ(y) ~= i |] ==> Limit(i)";
+ "[| 0<i; ALL y. succ(y) ~= i |] ==> Limit(i)";
by (safe_tac subset_cs);
by (rtac (not_le_iff_lt RS iffD1) 2);
by (blast_tac le_cs 4);
--- 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. [| <a,b>:f; <c,b>:f; f: inj(A,B) |] ==> a=c";
+ "[| <a,b>:f; <c,b>: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(<a,b>,f) : inj(cons(a,A), cons(b,B))";
by (fast_tac (claset() addIs [apply_type]
addss (simpset() addsimps [fun_extend, fun_extend_apply2,
--- 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 = <x;y> --> R(c(x,y)))";
+ "u: A<*>B ==> R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))";
by Auto_tac;
qed "expand_qsplit";
--- 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) |] ==> <a;b> <= univ(A)";
+ "[| a <= univ(A); b <= univ(A) |] ==> <a;b> <= 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) |] ==> <a;b> : quniv(A)";
+ "[| a: quniv(A); b: quniv(A) |] ==> <a;b> : 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. <a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)";
+ "<a;b> : 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 <a;b> with Vfrom... ***)
Goalw [QPair_def,sum_def]
- "!!X. Transset(X) ==> \
+ "Transset(X) ==> \
\ <a;b> Int Vfrom(X, succ(i)) <= <a Int Vfrom(X,i); b Int Vfrom(X,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) ==> \
\ <a;b> Int Vfrom(X,i) <= <a Int Vfrom(X,i); b 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) \
\ |] ==> <a;b> Int Vset(i) <= (UN j:i. <a Int Vset(j); b Int Vset(j)>)";
by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
(*0 case*)
--- 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); <a,b>:r; <b,c>:r |] ==> <a,c>:r";
+ "[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r";
by (Blast_tac 1);
qed "transD";
Goalw [trans_on_def]
- "!!r. [| trans[A](r); <a,b>:r; <b,c>:r; a:A; b:A; c:A |] ==> <a,c>:r";
+ "[| trans[A](r); <a,b>:r; <b,c>:r; a:A; b:A; c:A |] ==> <a,c>:r";
by (Blast_tac 1);
qed "trans_onD";
--- 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();
--- 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);
--- 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";
--- 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);
--- 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))));
--- 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<n,Var(i),Var(succ(i)))";
+ "[|n:nat; i:nat|]==> lift_rec(Var(i),n) =if(i<n,Var(i),Var(succ(i)))";
by (Asm_full_simp_tac 1);
qed "lift_rec_Var";
Goalw [lift_rec_def]
- "!!n.[|n:nat; i:nat; k:nat; k le 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<k |]==> lift_rec(Var(i),k) = Var(i)";
+ "[|i:nat; k:nat; i<k |]==> 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<i,Var(i#-1),if(k=i,u,Var(i)))";
by (asm_full_simp_tac (simpset() addsimps [gt_not_eq,leI]) 1);
qed "subst_Var";
Goalw [subst_rec_def]
- "!!n.[|n:nat; u:redexes|]==> 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|]==> \
+ "[|n:nat; u:redexes; p:nat; p<n|]==> \
\ 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<p|]==> \
+ "[|n:nat; u:redexes; p:nat; n<p|]==> \
\ 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
--- 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";
--- 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;
--- 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) |] ==> \
\ <a,b> : 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.[| <a,b> <= Vfrom(A,i); Transset(A); Limit(i) |] ==> \
+Goal "[| <a,b> <= Vfrom(A,i); Transset(A); Limit(i) |] ==> \
\ <a,b> : 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) |] ==> <a,b> : univ(A)";
+ "[| a: univ(A); b: univ(A) |] ==> <a,b> : 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<i";
+Goal "[| b: Fin(Vfrom(A,i)); Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
by (etac Fin_induct 1);
by (blast_tac (claset() addSDs [Limit_has_0]) 1);
by Safe_tac;
@@ -656,8 +652,7 @@
(** Closure under finite powers (functions from a fixed natural number) **)
-Goal
- "!!i. [| n: nat; Limit(i) |] ==> 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();
--- 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); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P";
-by (subgoal_tac
- "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P" 1);
+Goal "[| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P";
+by (subgoal_tac "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>: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) |] ==> \
\ <x,a>:r --> <x,b>: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); <b,a>: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); <b,a>: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);
--- 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})) \
--- 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";
--- 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";
--- 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);
--- 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";
--- 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. [| <n,l> : listn(A); <n',l'> : listn(A) |] ==> \
-\ <n#+n', l@l'> : listn(A)";
+ "[| <n,l> : listn(A); <n',l'> : listn(A) |] ==> <n#+n', l@l'> : listn(A)";
by (etac listn.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps listn.intrs)));
qed "listn_append";
--- a/src/ZF/ex/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<n; m:nat; n:nat |] ==> egcd(m,n) = egcd(n, m mod n)";
+ "[| 0<n; m:nat; n:nat |] ==> 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);
--- 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);
--- 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);
--- 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);
--- 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";
--- 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";