--- a/src/CCL/Set.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/CCL/Set.ML Wed Jul 15 10:15:13 1998 +0200
@@ -116,7 +116,7 @@
qed_goal "subset_refl" Set.thy "A <= A"
(fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]);
-Goal "!!A B C. [| A<=B; B<=C |] ==> A<=C";
+Goal "[| A<=B; B<=C |] ==> A<=C";
by (rtac subsetI 1);
by (REPEAT (eresolve_tac [asm_rl, subsetD] 1));
qed "subset_trans";
--- a/src/HOL/Arith.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Arith.ML Wed Jul 15 10:15:13 1998 +0200
@@ -28,7 +28,7 @@
(* Could be (and is, below) generalized in various ways;
However, none of the generalizations are currently in the simpset,
and I dread to think what happens if I put them in *)
-Goal "!!n. 0 < n ==> Suc(n-1) = n";
+Goal "0 < n ==> Suc(n-1) = n";
by (asm_simp_tac (simpset() addsplits [split_nat_case]) 1);
qed "Suc_pred";
Addsimps [Suc_pred];
@@ -111,7 +111,7 @@
Addsimps [pred_add_is_0];
(* Could be generalized, eg to "!!n. k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
-Goal "!!n. 0<n ==> m + (n-1) = (m+n)-1";
+Goal "0<n ==> m + (n-1) = (m+n)-1";
by (exhaust_tac "m" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
addsplits [split_nat_case])));
@@ -128,7 +128,7 @@
(**** Additional theorems about "less than" ****)
(*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
-Goal "!!m. m<n --> (? k. n=Suc(m+k))";
+Goal "m<n --> (? k. n=Suc(m+k))";
by (induct_tac "n" 1);
by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
by (blast_tac (claset() addSEs [less_SucE]
@@ -162,7 +162,7 @@
(*"i < j ==> i < m+j"*)
bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
-Goal "!!i. i+j < (k::nat) ==> i<k";
+Goal "i+j < (k::nat) ==> i<k";
by (etac rev_mp 1);
by (induct_tac "j" 1);
by (ALLGOALS Asm_simp_tac);
@@ -328,11 +328,11 @@
by (ALLGOALS Asm_simp_tac);
qed_spec_mp "add_diff_inverse";
-Goal "!!m. n<=m ==> n+(m-n) = (m::nat)";
+Goal "n<=m ==> n+(m-n) = (m::nat)";
by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1);
qed "le_add_diff_inverse";
-Goal "!!m. n<=m ==> (m-n)+n = (m::nat)";
+Goal "n<=m ==> (m-n)+n = (m::nat)";
by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1);
qed "le_add_diff_inverse2";
@@ -372,7 +372,7 @@
qed "Suc_diff_diff";
Addsimps [Suc_diff_diff];
-Goal "!!n. 0<n ==> n - Suc i < n";
+Goal "0<n ==> n - Suc i < n";
by (res_inst_tac [("n","n")] natE 1);
by Safe_tac;
by (asm_simp_tac (simpset() addsimps [le_eq_less_Suc RS sym]) 1);
@@ -557,13 +557,13 @@
qed "mult_eq_1_iff";
Addsimps [mult_eq_1_iff];
-Goal "!!k. 0<k ==> (m*k < n*k) = (m<n)";
+Goal "0<k ==> (m*k < n*k) = (m<n)";
by (safe_tac (claset() addSIs [mult_less_mono1]));
by (cut_facts_tac [less_linear] 1);
by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
qed "mult_less_cancel2";
-Goal "!!k. 0<k ==> (k*m < k*n) = (m<n)";
+Goal "0<k ==> (k*m < k*n) = (m<n)";
by (dtac mult_less_cancel2 1);
by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
qed "mult_less_cancel1";
@@ -579,7 +579,7 @@
by (rtac Suc_mult_less_cancel1 1);
qed "Suc_mult_le_cancel1";
-Goal "!!k. 0<k ==> (m*k = n*k) = (m=n)";
+Goal "0<k ==> (m*k = n*k) = (m=n)";
by (cut_facts_tac [less_linear] 1);
by Safe_tac;
by (assume_tac 2);
@@ -587,7 +587,7 @@
by (ALLGOALS Asm_full_simp_tac);
qed "mult_cancel2";
-Goal "!!k. 0<k ==> (k*m = k*n) = (m=n)";
+Goal "0<k ==> (k*m = k*n) = (m=n)";
by (dtac mult_cancel2 1);
by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
qed "mult_cancel1";
@@ -601,7 +601,7 @@
(** Lemma for gcd **)
-Goal "!!m n. m = m*n ==> n=1 | m=0";
+Goal "m = m*n ==> n=1 | m=0";
by (dtac sym 1);
by (rtac disjCI 1);
by (rtac nat_less_cases 1 THEN assume_tac 2);
@@ -626,11 +626,11 @@
by (Asm_full_simp_tac 1);
qed "add_less_imp_less_diff";
-Goal "!! n. n <= m ==> Suc m - n = Suc (m - n)";
+Goal "n <= m ==> Suc m - n = Suc (m - n)";
by (asm_full_simp_tac (simpset() addsimps [Suc_diff_n, le_eq_less_Suc]) 1);
qed "Suc_diff_le";
-Goal "!! n. Suc i <= n ==> Suc (n - Suc i) = n - i";
+Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
by (asm_full_simp_tac
(simpset() addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1);
qed "Suc_diff_Suc";
--- a/src/HOL/Divides.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Divides.ML Wed Jul 15 10:15:13 1998 +0200
@@ -27,18 +27,18 @@
by (simp_tac (simpset() addsimps [mod_def]) 1);
qed "mod_eq";
-Goal "!!m. m<n ==> m mod n = m";
+Goal "m<n ==> m mod n = m";
by (rtac (mod_eq RS wf_less_trans) 1);
by (Asm_simp_tac 1);
qed "mod_less";
-Goal "!!m. [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n";
+Goal "[| 0<n; ~m<n |] ==> m mod n = (m-n) mod n";
by (rtac (mod_eq RS wf_less_trans) 1);
by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
qed "mod_geq";
(*NOT suitable for rewriting: loops*)
-Goal "!!m. 0<n ==> m mod n = (if m<n then m else (m-n) mod n)";
+Goal "0<n ==> m mod n = (if m<n then m else (m-n) mod n)";
by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1);
qed "mod_if";
@@ -48,17 +48,17 @@
qed "mod_1";
Addsimps [mod_1];
-Goal "!!n. 0<n ==> n mod n = 0";
+Goal "0<n ==> n mod n = 0";
by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1);
qed "mod_self";
-Goal "!!n. 0<n ==> (m+n) mod n = m mod n";
+Goal "0<n ==> (m+n) mod n = m mod n";
by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1);
by (stac (mod_geq RS sym) 2);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
qed "mod_add_self2";
-Goal "!!k. 0<n ==> (n+m) mod n = m mod n";
+Goal "0<n ==> (n+m) mod n = m mod n";
by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1);
qed "mod_add_self1";
@@ -67,13 +67,13 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [mod_add_self1]))));
qed "mod_mult_self1";
-Goal "!!m. 0<n ==> (m + n*k) mod n = m mod n";
+Goal "0<n ==> (m + n*k) mod n = m mod n";
by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1);
qed "mod_mult_self2";
Addsimps [mod_mult_self1, mod_mult_self2];
-Goal "!!k. [| 0<k; 0<n |] ==> (m mod n)*k = (m*k) mod (n*k)";
+Goal "[| 0<k; 0<n |] ==> (m mod n)*k = (m*k) mod (n*k)";
by (res_inst_tac [("n","m")] less_induct 1);
by (stac mod_if 1);
by (Asm_simp_tac 1);
@@ -81,7 +81,7 @@
diff_less, diff_mult_distrib]) 1);
qed "mod_mult_distrib";
-Goal "!!k. [| 0<k; 0<n |] ==> k*(m mod n) = (k*m) mod (k*n)";
+Goal "[| 0<k; 0<n |] ==> k*(m mod n) = (k*m) mod (k*n)";
by (res_inst_tac [("n","m")] less_induct 1);
by (stac mod_if 1);
by (Asm_simp_tac 1);
@@ -89,7 +89,7 @@
diff_less, diff_mult_distrib2]) 1);
qed "mod_mult_distrib2";
-Goal "!!n. 0<n ==> m*n mod n = 0";
+Goal "0<n ==> m*n mod n = 0";
by (induct_tac "m" 1);
by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
by (dres_inst_tac [("m","m*n")] mod_add_self2 1);
@@ -104,23 +104,23 @@
by (simp_tac (simpset() addsimps [div_def]) 1);
qed "div_eq";
-Goal "!!m. m<n ==> m div n = 0";
+Goal "m<n ==> m div n = 0";
by (rtac (div_eq RS wf_less_trans) 1);
by (Asm_simp_tac 1);
qed "div_less";
-Goal "!!M. [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)";
+Goal "[| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)";
by (rtac (div_eq RS wf_less_trans) 1);
by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
qed "div_geq";
(*NOT suitable for rewriting: loops*)
-Goal "!!m. 0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
+Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
qed "div_if";
(*Main Result about quotient and remainder.*)
-Goal "!!m. 0<n ==> (m div n)*n + m mod n = m";
+Goal "0<n ==> (m div n)*n + m mod n = m";
by (res_inst_tac [("n","m")] less_induct 1);
by (stac mod_if 1);
by (ALLGOALS (asm_simp_tac
@@ -130,7 +130,7 @@
qed "mod_div_equality";
(* a simple rearrangement of mod_div_equality: *)
-Goal "!!k. 0<k ==> k*(m div k) = m - (m mod k)";
+Goal "0<k ==> k*(m div k) = m - (m mod k)";
by (dres_inst_tac [("m","m")] mod_div_equality 1);
by (EVERY1[etac subst, simp_tac (simpset() addsimps mult_ac),
K(IF_UNSOLVED no_tac)]);
@@ -142,18 +142,18 @@
qed "div_1";
Addsimps [div_1];
-Goal "!!n. 0<n ==> n div n = 1";
+Goal "0<n ==> n div n = 1";
by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
qed "div_self";
-Goal "!!n. 0<n ==> (m+n) div n = Suc (m div n)";
+Goal "0<n ==> (m+n) div n = Suc (m div n)";
by (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n)" 1);
by (stac (div_geq RS sym) 2);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
qed "div_add_self2";
-Goal "!!k. 0<n ==> (n+m) div n = Suc (m div n)";
+Goal "0<n ==> (n+m) div n = Suc (m div n)";
by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1);
qed "div_add_self1";
@@ -162,7 +162,7 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [div_add_self1]))));
qed "div_mult_self1";
-Goal "!!m. 0<n ==> (m + n*k) div n = k + m div n";
+Goal "0<n ==> (m + n*k) div n = k + m div n";
by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1);
qed "div_mult_self2";
@@ -170,10 +170,10 @@
(* Monotonicity of div in first argument *)
-Goal "!!n. 0<k ==> ALL m. m <= n --> (m div k) <= (n div k)";
+Goal "0<k ==> ALL m. m <= n --> (m div k) <= (n div k)";
by (res_inst_tac [("n","n")] less_induct 1);
by (Clarify_tac 1);
-by (case_tac "na<k" 1);
+by (case_tac "n<k" 1);
(* 1 case n<k *)
by (subgoal_tac "m<k" 1);
by (asm_simp_tac (simpset() addsimps [div_less]) 1);
@@ -188,7 +188,7 @@
(* Antimonotonicity of div in second argument *)
-Goal "!!k m n. [| 0<m; m<=n |] ==> (k div n) <= (k div m)";
+Goal "[| 0<m; m<=n |] ==> (k div n) <= (k div m)";
by (subgoal_tac "0<n" 1);
by (trans_tac 2);
by (res_inst_tac [("n","k")] less_induct 1);
@@ -205,7 +205,7 @@
by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 1));
qed "div_le_mono2";
-Goal "!!m n. 0<n ==> m div n <= m";
+Goal "0<n ==> m div n <= m";
by (subgoal_tac "m div n <= m div 1" 1);
by (Asm_full_simp_tac 1);
by (rtac div_le_mono2 1);
@@ -214,7 +214,7 @@
Addsimps [div_le_dividend];
(* Similar for "less than" *)
-Goal "!!m n. 1<n ==> (0 < m) --> (m div n < m)";
+Goal "1<n ==> (0 < m) --> (m div n < m)";
by (res_inst_tac [("n","m")] less_induct 1);
by (Simp_tac 1);
by (rename_tac "m" 1);
@@ -255,7 +255,7 @@
by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
qed "mod_Suc";
-Goal "!!m n. 0<n ==> m mod n < n";
+Goal "0<n ==> m mod n < n";
by (res_inst_tac [("n","m")] less_induct 1);
by (excluded_middle_tac "na<n" 1);
(*case na<n*)
@@ -270,7 +270,7 @@
(*With less_zeroE, causes case analysis on b<2*)
AddSEs [less_SucE];
-Goal "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
+Goal "b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
by (subgoal_tac "k mod 2 < 2" 1);
by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
by (Asm_simp_tac 1);
@@ -311,7 +311,7 @@
(*** More division laws ***)
-Goal "!!n. 0<n ==> m*n div n = m";
+Goal "0<n ==> m*n div n = m";
by (cut_inst_tac [("m", "m*n")] mod_div_equality 1);
by (assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1);
@@ -319,7 +319,7 @@
Addsimps [div_mult_self_is_m];
(*Cancellation law for division*)
-Goal "!!k. [| 0<n; 0<k |] ==> (k*m) div (k*n) = m div n";
+Goal "[| 0<n; 0<k |] ==> (k*m) div (k*n) = m div n";
by (res_inst_tac [("n","m")] less_induct 1);
by (case_tac "na<n" 1);
by (asm_simp_tac (simpset() addsimps [div_less, zero_less_mult_iff,
@@ -333,7 +333,7 @@
qed "div_cancel";
Addsimps [div_cancel];
-Goal "!!k. [| 0<n; 0<k |] ==> (k*m) mod (k*n) = k * (m mod n)";
+Goal "[| 0<n; 0<k |] ==> (k*m) mod (k*n) = k * (m mod n)";
by (res_inst_tac [("n","m")] less_induct 1);
by (case_tac "na<n" 1);
by (asm_simp_tac (simpset() addsimps [mod_less, zero_less_mult_iff,
@@ -356,7 +356,7 @@
qed "dvd_0_right";
Addsimps [dvd_0_right];
-Goalw [dvd_def] "!!m. 0 dvd m ==> m = 0";
+Goalw [dvd_def] "0 dvd m ==> m = 0";
by (fast_tac (claset() addss simpset()) 1);
qed "dvd_0_left";
@@ -370,33 +370,33 @@
qed "dvd_refl";
Addsimps [dvd_refl];
-Goalw [dvd_def] "!!m n p. [| m dvd n; n dvd p |] ==> m dvd p";
+Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd p";
by (blast_tac (claset() addIs [mult_assoc] ) 1);
qed "dvd_trans";
-Goalw [dvd_def] "!!m n. [| m dvd n; n dvd m |] ==> m=n";
+Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m=n";
by (fast_tac (claset() addDs [mult_eq_self_implies_10]
addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1);
qed "dvd_anti_sym";
-Goalw [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m + n)";
+Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m + n)";
by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1);
qed "dvd_add";
-Goalw [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m-n)";
+Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n)";
by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1);
qed "dvd_diff";
-Goal "!!k. [| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m";
+Goal "[| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m";
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
by (blast_tac (claset() addIs [dvd_add]) 1);
qed "dvd_diffD";
-Goalw [dvd_def] "!!k. k dvd n ==> k dvd (m*n)";
+Goalw [dvd_def] "k dvd n ==> k dvd (m*n)";
by (blast_tac (claset() addIs [mult_left_commute]) 1);
qed "dvd_mult";
-Goal "!!k. k dvd m ==> k dvd (m*n)";
+Goal "k dvd m ==> k dvd (m*n)";
by (stac mult_commute 1);
by (etac dvd_mult 1);
qed "dvd_mult2";
@@ -404,7 +404,7 @@
(* k dvd (m*k) *)
AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
-Goalw [dvd_def] "!!m. [| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
+Goalw [dvd_def] "[| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
by (Clarify_tac 1);
by (full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 1);
by (res_inst_tac
@@ -414,30 +414,30 @@
mult_mod_distrib, add_mult_distrib2]) 1);
qed "dvd_mod";
-Goal "!!k. [| k dvd (m mod n); k dvd n; 0<n |] ==> k dvd m";
+Goal "[| k dvd (m mod n); k dvd n; 0<n |] ==> k dvd m";
by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2);
by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
qed "dvd_mod_imp_dvd";
-Goalw [dvd_def] "!!k m n. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
+Goalw [dvd_def] "!!k. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
by (etac exE 1);
by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
by (Blast_tac 1);
qed "dvd_mult_cancel";
-Goalw [dvd_def] "!!i j. [| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)";
+Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)";
by (Clarify_tac 1);
by (res_inst_tac [("x","k*ka")] exI 1);
by (asm_simp_tac (simpset() addsimps mult_ac) 1);
qed "mult_dvd_mono";
-Goalw [dvd_def] "!!c. (i*j) dvd k ==> i dvd k";
+Goalw [dvd_def] "(i*j) dvd k ==> i dvd k";
by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
by (Blast_tac 1);
qed "dvd_mult_left";
-Goalw [dvd_def] "!!n. [| k dvd n; 0 < n |] ==> k <= n";
+Goalw [dvd_def] "[| k dvd n; 0 < n |] ==> k <= n";
by (Clarify_tac 1);
by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff])));
by (etac conjE 1);
@@ -447,11 +447,11 @@
by (Simp_tac 1);
qed "dvd_imp_le";
-Goalw [dvd_def] "!!k. 0<k ==> (k dvd n) = (n mod k = 0)";
+Goalw [dvd_def] "0<k ==> (k dvd n) = (n mod k = 0)";
by Safe_tac;
+by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
+by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1);
by (stac mult_commute 1);
by (Asm_simp_tac 1);
-by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1);
-by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
by (Blast_tac 1);
qed "dvd_eq_mod_eq_0";
--- a/src/HOL/Finite.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Finite.ML Wed Jul 15 10:15:13 1998 +0200
@@ -42,7 +42,7 @@
qed "finite_UnI";
(*Every subset of a finite set is finite*)
-Goal "!!B. finite B ==> ALL A. A<=B --> finite A";
+Goal "finite B ==> ALL A. A<=B --> finite A";
by (etac finite_induct 1);
by (Simp_tac 1);
by (safe_tac (claset() addSDs [subset_insert_iff RS iffD1]));
@@ -50,7 +50,7 @@
by (ALLGOALS Asm_simp_tac);
val lemma = result();
-Goal "!!A. [| A<=B; finite B |] ==> finite A";
+Goal "[| A<=B; finite B |] ==> finite A";
by (dtac lemma 1);
by (Blast_tac 1);
qed "finite_subset";
@@ -70,7 +70,7 @@
Addsimps[finite_insert];
(*The image of a finite set is finite *)
-Goal "!!F. finite F ==> finite(h``F)";
+Goal "finite F ==> finite(h``F)";
by (etac finite_induct 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
@@ -111,7 +111,7 @@
AddIffs [finite_Diff_singleton];
(*Lemma for proving finite_imageD*)
-Goal "!!A. finite B ==> !A. f``A = B --> inj_on f A --> finite A";
+Goal "finite B ==> !A. f``A = B --> inj_on f A --> finite A";
by (etac finite_induct 1);
by (ALLGOALS Asm_simp_tac);
by (Clarify_tac 1);
@@ -127,7 +127,7 @@
(asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff])));
val lemma = result();
-Goal "!!A. [| finite(f``A); inj_on f A |] ==> finite A";
+Goal "[| finite(f``A); inj_on f A |] ==> finite A";
by (dtac lemma 1);
by (Blast_tac 1);
qed "finite_imageD";
@@ -151,7 +151,7 @@
(** The powerset of a finite set **)
-Goal "!!A. finite(Pow A) ==> finite A";
+Goal "finite(Pow A) ==> finite A";
by (subgoal_tac "finite ((%x.{x})``A)" 1);
by (rtac finite_subset 2);
by (assume_tac 3);
@@ -273,7 +273,7 @@
by (Blast_tac 1);
val lemma = result();
-Goal "!!A. [| finite A; x ~: A |] ==> \
+Goal "[| finite A; x ~: A |] ==> \
\ (LEAST n. ? f. insert x A = {f i|i. i<n}) = Suc(LEAST n. ? f. A={f i|i. i<n})";
by (rtac Least_equality 1);
by (dtac finite_has_card 1);
@@ -309,12 +309,12 @@
qed "card_insert_disjoint";
Addsimps [card_insert_disjoint];
-Goal "!!A. finite A ==> card A <= card (insert x A)";
+Goal "finite A ==> card A <= card (insert x A)";
by (case_tac "x: A" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb])));
qed "card_insert_le";
-Goal "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
+Goal "finite A ==> !B. B <= A --> card(B) <= card(A)";
by (etac finite_induct 1);
by (Simp_tac 1);
by (Clarify_tac 1);
@@ -325,13 +325,13 @@
(simpset() addsimps [subset_insert_iff, finite_subset])) 1);
qed_spec_mp "card_mono";
-Goal "!!A B. [| finite A; finite B |]\
+Goal "[| finite A; finite B |]\
\ ==> A Int B = {} --> card(A Un B) = card A + card B";
by (etac finite_induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Int_insert_left])));
qed_spec_mp "card_Un_disjoint";
-Goal "!!A. [| finite A; B<=A |] ==> card A - card B = card (A - B)";
+Goal "[| finite A; B<=A |] ==> card A - card B = card (A - B)";
by (subgoal_tac "(A-B) Un B = A" 1);
by (Blast_tac 2);
by (rtac (add_right_cancel RS iffD1) 1);
@@ -344,18 +344,18 @@
add_diff_inverse, card_mono, finite_subset])));
qed "card_Diff_subset";
-Goal "!!A. [| finite A; x: A |] ==> Suc(card(A-{x})) = card A";
+Goal "[| finite A; x: A |] ==> Suc(card(A-{x})) = card A";
by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1);
by (assume_tac 1);
by (Asm_simp_tac 1);
qed "card_Suc_Diff";
-Goal "!!A. [| finite A; x: A |] ==> card(A-{x}) < card A";
+Goal "[| finite A; x: A |] ==> card(A-{x}) < card A";
by (rtac Suc_less_SucD 1);
by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
qed "card_Diff";
-Goal "!!A. finite A ==> card(A-{x}) <= card A";
+Goal "finite A ==> card(A-{x}) <= card A";
by (case_tac "x: A" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff, less_imp_le])));
qed "card_Diff_le";
@@ -363,14 +363,14 @@
(*** Cardinality of the Powerset ***)
-Goal "!!A. finite A ==> card(insert x A) = Suc(card(A-{x}))";
+Goal "finite A ==> card(insert x A) = Suc(card(A-{x}))";
by (case_tac "x:A" 1);
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [card_Suc_Diff, insert_absorb])));
qed "card_insert";
Addsimps [card_insert];
-Goal "!!A. finite(A) ==> inj_on f A --> card (f `` A) = card A";
+Goal "finite(A) ==> inj_on f A --> card (f `` A) = card A";
by (etac finite_induct 1);
by (ALLGOALS Asm_simp_tac);
by Safe_tac;
@@ -382,7 +382,7 @@
by (Blast_tac 1);
qed_spec_mp "card_image";
-Goal "!!A. finite A ==> card (Pow A) = 2 ^ card A";
+Goal "finite A ==> card (Pow A) = 2 ^ card A";
by (etac finite_induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert])));
by (stac card_Un_disjoint 1);
@@ -418,7 +418,7 @@
(*Relates to equivalence classes. Based on a theorem of F. Kammueller's.
The "finite C" premise is redundant*)
-Goal "!!C. finite C ==> finite (Union C) --> \
+Goal "finite C ==> finite (Union C) --> \
\ (! c : C. k dvd card c) --> \
\ (! c1: C. ! c2: C. c1 ~= c2 --> c1 Int c2 = {}) \
\ --> k dvd card(Union C)";
--- a/src/HOL/Fun.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Fun.ML Wed Jul 15 10:15:13 1998 +0200
@@ -97,7 +97,7 @@
by (REPEAT (resolve_tac prems 1));
qed "inj_onD";
-Goal "!!x y.[| inj_on f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)";
+Goal "[| inj_on f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)";
by (blast_tac (claset() addSDs [inj_onD]) 1);
qed "inj_on_iff";
@@ -135,7 +135,7 @@
by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
qed "inv_injective";
-Goal "!!f. [| inj(f); A<=range(f) |] ==> inj_on (inv f) A";
+Goal "[| inj(f); A<=range(f) |] ==> inj_on (inv f) A";
by (fast_tac (claset() addIs [inj_onI]
addEs [inv_injective,injD]) 1);
qed "inj_on_inv";
@@ -150,11 +150,11 @@
by (Blast_tac 1);
qed "inj_on_image_set_diff";
-Goalw [inj_def] "!!f. inj f ==> f``(A Int B) = f``A Int f``B";
+Goalw [inj_def] "inj f ==> f``(A Int B) = f``A Int f``B";
by (Blast_tac 1);
qed "image_Int";
-Goalw [inj_def] "!!f. inj f ==> f``(A-B) = f``A - f``B";
+Goalw [inj_def] "inj f ==> f``(A-B) = f``A - f``B";
by (Blast_tac 1);
qed "image_set_diff";
--- a/src/HOL/IOA/Asig.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/IOA/Asig.ML Wed Jul 15 10:15:13 1998 +0200
@@ -10,10 +10,10 @@
val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def];
-Goal "!!a.[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
+Goal "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
qed"int_and_ext_is_act";
-Goal "!!a.[|a:externals(S)|] ==> a:actions(S)";
+Goal "[|a:externals(S)|] ==> a:actions(S)";
by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
qed"ext_is_act";
--- a/src/HOL/IOA/IOA.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/IOA/IOA.ML Wed Jul 15 10:15:13 1998 +0200
@@ -46,7 +46,7 @@
by (Fast_tac 1);
qed "mk_trace_thm";
-Goalw [reachable_def] "!!A. s:starts_of(A) ==> reachable A s";
+Goalw [reachable_def] "s:starts_of(A) ==> reachable A s";
by (res_inst_tac [("x","(%i. None,%i. s)")] bexI 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset() addsimps exec_rws) 1);
--- a/src/HOL/IOA/Solve.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/IOA/Solve.ML Wed Jul 15 10:15:13 1998 +0200
@@ -65,7 +65,7 @@
by (Fast_tac 1);
val externals_of_par_extra = result();
-Goal "!!s.[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
+Goal "[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
by (etac bexE 1);
by (res_inst_tac [("x",
@@ -85,7 +85,7 @@
(* Exact copy of proof of comp1_reachable for the second
component of a parallel composition. *)
-Goal "!!s.[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
+Goal "[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
by (etac bexE 1);
by (res_inst_tac [("x",
@@ -105,7 +105,7 @@
Delsplits [split_if];
(* Composition of possibility-mappings *)
-Goalw [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \
+Goalw [is_weak_pmap_def] "[| is_weak_pmap f C1 A1 & \
\ externals(asig_of(A1))=externals(asig_of(C1)) &\
\ is_weak_pmap g C2 A2 & \
\ externals(asig_of(A2))=externals(asig_of(C2)) & \
@@ -149,7 +149,7 @@
qed"fxg_is_weak_pmap_of_product_IOA";
-Goal "!!s.[| reachable (rename C g) s |] ==> reachable C s";
+Goal "[| reachable (rename C g) s |] ==> reachable C s";
by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
by (etac bexE 1);
by (res_inst_tac [("x",
@@ -166,7 +166,7 @@
qed"reachable_rename_ioa";
-Goal "!!f.[| is_weak_pmap f C A |]\
+Goal "[| is_weak_pmap f C A |]\
\ ==> (is_weak_pmap f (rename C g) (rename A g))";
by (asm_full_simp_tac (simpset() addsimps [is_weak_pmap_def]) 1);
by (rtac conjI 1);
--- a/src/HOL/Induct/Acc.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Acc.ML Wed Jul 15 10:15:13 1998 +0200
@@ -18,7 +18,7 @@
map (rewrite_rule [pred_def]) acc.intrs)) 1);
qed "accI";
-Goal "!!a b r. [| b: acc(r); (a,b): r |] ==> a: acc(r)";
+Goal "[| b: acc(r); (a,b): r |] ==> a: acc(r)";
by (etac acc.elim 1);
by (rewtac pred_def);
by (Fast_tac 1);
--- a/src/HOL/Induct/Com.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Com.ML Wed Jul 15 10:15:13 1998 +0200
@@ -19,7 +19,7 @@
AddSEs exec_elim_cases;
(*This theorem justifies using "exec" in the inductive definition of "eval"*)
-Goalw exec.defs "!!A B. A<=B ==> exec(A) <= exec(B)";
+Goalw exec.defs "A<=B ==> exec(A) <= exec(B)";
by (rtac lfp_mono 1);
by (REPEAT (ares_tac basic_monos 1));
qed "exec_mono";
@@ -29,7 +29,7 @@
Unify.search_bound := 60;
(*Command execution is functional (deterministic) provided evaluation is*)
-Goal "!!x. Function ev ==> Function(exec ev)";
+Goal "Function ev ==> Function(exec ev)";
by (simp_tac (simpset() addsimps [Function_def, Unique_def]) 1);
by (REPEAT (rtac allI 1));
by (rtac impI 1);
@@ -48,7 +48,7 @@
by (Simp_tac 1);
qed "assign_same";
-Goalw [assign_def] "!!y. y~=x ==> (s[v/x])y = s y";
+Goalw [assign_def] "y~=x ==> (s[v/x])y = s y";
by (Asm_simp_tac 1);
qed "assign_different";
--- a/src/HOL/Induct/Comb.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Comb.ML Wed Jul 15 10:15:13 1998 +0200
@@ -55,22 +55,22 @@
AddIs [contract.Ap1, contract.Ap2];
AddSEs [K_contractE, S_contractE, Ap_contractE];
-Goalw [I_def] "!!z. I -1-> z ==> P";
+Goalw [I_def] "I -1-> z ==> P";
by (Blast_tac 1);
qed "I_contract_E";
AddSEs [I_contract_E];
-Goal "!!x z. K#x -1-> z ==> (EX x'. z = K#x' & x -1-> x')";
+Goal "K#x -1-> z ==> (EX x'. z = K#x' & x -1-> x')";
by (Blast_tac 1);
qed "K1_contractD";
AddSEs [K1_contractD];
-Goal "!!x z. x ---> y ==> x#z ---> y#z";
+Goal "x ---> y ==> x#z ---> y#z";
by (etac rtrancl_induct 1);
by (ALLGOALS (blast_tac (claset() addIs [r_into_rtrancl, rtrancl_trans])));
qed "Ap_reduce1";
-Goal "!!x z. x ---> y ==> z#x ---> z#y";
+Goal "x ---> y ==> z#x ---> z#y";
by (etac rtrancl_induct 1);
by (ALLGOALS (blast_tac (claset() addIs [r_into_rtrancl, rtrancl_trans])));
qed "Ap_reduce2";
@@ -108,12 +108,12 @@
(*** Basic properties of parallel contraction ***)
-Goal "!!x z. K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
+Goal "K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
by (Blast_tac 1);
qed "K1_parcontractD";
AddSDs [K1_parcontractD];
-Goal "!!x z. S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
+Goal "S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
by (Blast_tac 1);
qed "S1_parcontractD";
AddSDs [S1_parcontractD];
--- a/src/HOL/Induct/Exp.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Exp.ML Wed Jul 15 10:15:13 1998 +0200
@@ -97,7 +97,7 @@
qed "Function_eval";
-Goal "!!x. (e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)";
+Goal "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)";
by (etac eval_induct 1);
by (ALLGOALS Asm_simp_tac);
val lemma = result();
@@ -107,7 +107,7 @@
(*This theorem says that "WHILE TRUE DO c" cannot terminate*)
-Goal "!!x. (c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False";
+Goal "(c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False";
by (etac exec.induct 1);
by Auto_tac;
bind_thm ("while_true_E", refl RSN (2, result() RS mp));
@@ -115,7 +115,7 @@
(** Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP and WHILE e DO c **)
-Goal "!!x. (c',s) -[eval]-> t ==> \
+Goal "(c',s) -[eval]-> t ==> \
\ (c' = WHILE e DO c) --> \
\ (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t";
by (etac exec.induct 1);
@@ -124,7 +124,7 @@
bind_thm ("while_if1", refl RSN (2, result() RS mp));
-Goal "!!x. (c',s) -[eval]-> t ==> \
+Goal "(c',s) -[eval]-> t ==> \
\ (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) --> \
\ (WHILE e DO c, s) -[eval]-> t";
by (etac exec.induct 1);
@@ -143,7 +143,7 @@
(** Equivalence of (IF e THEN c1 ELSE c2);;c
and IF e THEN (c1;;c) ELSE (c2;;c) **)
-Goal "!!x. (c',s) -[eval]-> t ==> \
+Goal "(c',s) -[eval]-> t ==> \
\ (c' = (IF e THEN c1 ELSE c2);;c) --> \
\ (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t";
by (etac exec.induct 1);
@@ -152,7 +152,7 @@
bind_thm ("if_semi1", refl RSN (2, result() RS mp));
-Goal "!!x. (c',s) -[eval]-> t ==> \
+Goal "(c',s) -[eval]-> t ==> \
\ (c' = IF e THEN (c1;;c) ELSE (c2;;c)) --> \
\ ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t";
by (etac exec.induct 1);
@@ -172,7 +172,7 @@
and VALOF c1;;c2 RESULTIS e
**)
-Goal "!!x. (e',s) -|-> (v,s') ==> \
+Goal "(e',s) -|-> (v,s') ==> \
\ (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) --> \
\ (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')";
by (etac eval_induct 1);
@@ -181,7 +181,7 @@
bind_thm ("valof_valof1", refl RSN (2, result() RS mp));
-Goal "!!x. (e',s) -|-> (v,s') ==> \
+Goal "(e',s) -|-> (v,s') ==> \
\ (e' = VALOF c1;;c2 RESULTIS e) --> \
\ (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')";
by (etac eval_induct 1);
@@ -198,7 +198,7 @@
(** Equivalence of VALOF SKIP RESULTIS e and e **)
-Goal "!!x. (e',s) -|-> (v,s') ==> \
+Goal "(e',s) -|-> (v,s') ==> \
\ (e' = VALOF SKIP RESULTIS e) --> \
\ (e, s) -|-> (v,s')";
by (etac eval_induct 1);
@@ -206,7 +206,7 @@
by (Blast_tac 1);
bind_thm ("valof_skip1", refl RSN (2, result() RS mp));
-Goal "!!x. (e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')";
+Goal "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')";
by (Blast_tac 1);
qed "valof_skip2";
@@ -217,7 +217,7 @@
(** Equivalence of VALOF x:=e RESULTIS x and e **)
-Goal "!!x. (e',s) -|-> (v,s'') ==> \
+Goal "(e',s) -|-> (v,s'') ==> \
\ (e' = VALOF x:=e RESULTIS X x) --> \
\ (EX s'. (e, s) -|-> (v,s') & (s'' = s'[v/x]))";
by (etac eval_induct 1);
@@ -229,7 +229,7 @@
bind_thm ("valof_assign1", refl RSN (2, result() RS mp));
-Goal "!!x. (e,s) -|-> (v,s') ==> \
+Goal "(e,s) -|-> (v,s') ==> \
\ (VALOF x:=e RESULTIS X x, s) -|-> (v,s'[v/x])";
by (Blast_tac 1);
qed "valof_assign2";
--- a/src/HOL/Induct/LFilter.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/LFilter.ML Wed Jul 15 10:15:13 1998 +0200
@@ -18,19 +18,19 @@
AddSEs [findRel_LConsE];
-Goal "!!p. (l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
+Goal "(l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
by (etac findRel.induct 1);
by (Blast_tac 1);
by (Blast_tac 1);
qed_spec_mp "findRel_functional";
-Goal "!!p. (l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
+Goal "(l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
by (etac findRel.induct 1);
by (Blast_tac 1);
by (Blast_tac 1);
qed_spec_mp "findRel_imp_LCons";
-Goal "!!p. (LNil,l): findRel p ==> R";
+Goal "(LNil,l): findRel p ==> R";
by (blast_tac (claset() addEs [findRel.elim]) 1);
qed "findRel_LNil";
@@ -39,7 +39,7 @@
(*** Properties of Domain (findRel p) ***)
-Goal "!!p. LCons x l : Domain(findRel p) = (p x | l : Domain(findRel p))";
+Goal "LCons x l : Domain(findRel p) = (p x | l : Domain(findRel p))";
by (case_tac "p x" 1);
by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
qed "LCons_Domain_findRel";
@@ -73,22 +73,22 @@
qed "find_LNil";
Addsimps [find_LNil];
-Goalw [find_def] "!!p. (l,l') : findRel p ==> find p l = l'";
+Goalw [find_def] "(l,l') : findRel p ==> find p l = l'";
by (blast_tac (claset() addDs [findRel_functional]) 1);
qed "findRel_imp_find";
Addsimps [findRel_imp_find];
-Goal "!!p. p x ==> find p (LCons x l) = LCons x l";
+Goal "p x ==> find p (LCons x l) = LCons x l";
by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
qed "find_LCons_found";
Addsimps [find_LCons_found];
-Goalw [find_def] "!!p. l ~: Domain(findRel p) ==> find p l = LNil";
+Goalw [find_def] "l ~: Domain(findRel p) ==> find p l = LNil";
by (Blast_tac 1);
qed "diverge_find_LNil";
Addsimps [diverge_find_LNil];
-Goal "!!p. ~ (p x) ==> find p (LCons x l) = find p l";
+Goal "~ (p x) ==> find p (LCons x l) = find p l";
by (case_tac "LCons x l : Domain(findRel p)" 1);
by (Asm_full_simp_tac 2);
by (Clarify_tac 1);
@@ -111,7 +111,7 @@
qed "lfilter_LNil";
Addsimps [lfilter_LNil];
-Goal "!!p. l ~: Domain(findRel p) ==> lfilter p l = LNil";
+Goal "l ~: Domain(findRel p) ==> lfilter p l = LNil";
by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
by (Asm_simp_tac 1);
qed "diverge_lfilter_LNil";
@@ -119,7 +119,7 @@
Addsimps [diverge_lfilter_LNil];
-Goal "!!p. p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
+Goal "p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
by (Asm_simp_tac 1);
qed "lfilter_LCons_found";
@@ -127,7 +127,7 @@
subsumes both*)
-Goal "!!p. (l, LCons x l') : findRel p \
+Goal "(l, LCons x l') : findRel p \
\ ==> lfilter p l = LCons x (lfilter p l')";
by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
by (Asm_simp_tac 1);
@@ -136,7 +136,7 @@
Addsimps [findRel_imp_lfilter];
-Goal "!!p. ~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
+Goal "~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
by (case_tac "LCons x l : Domain(findRel p)" 1);
by (Asm_full_simp_tac 2);
@@ -155,7 +155,7 @@
Addsimps [lfilter_LCons];
-Goal "!!p. lfilter p l = LNil ==> l ~: Domain(findRel p)";
+Goal "lfilter p l = LNil ==> l ~: Domain(findRel p)";
by (rtac notI 1);
by (etac Domain_findRelE 1);
by (etac rev_mp 1);
@@ -163,7 +163,7 @@
qed "lfilter_eq_LNil";
-Goal "!!p. lfilter p l = LCons x l' --> \
+Goal "lfilter p l = LCons x l' --> \
\ (EX l''. l' = lfilter p l'' & (l, LCons x l'') : findRel p)";
by (stac (lfilter_def RS def_llist_corec) 1);
by (case_tac "l : Domain(findRel p)" 1);
@@ -205,7 +205,7 @@
lfilter p (lfilter q l) = lfilter (%x. p x & q x) l
***)
-Goal "!!p. (l,l') : findRel q \
+Goal "(l,l') : findRel q \
\ ==> l' = LCons x l'' --> p x --> (l,l') : findRel (%x. p x & q x)";
by (etac findRel.induct 1);
by (blast_tac (claset() addIs findRel.intrs) 1);
@@ -214,7 +214,7 @@
val findRel_conj = refl RSN (2, findRel_conj_lemma);
-Goal "!!p. (l,l'') : findRel (%x. p x & q x) \
+Goal "(l,l'') : findRel (%x. p x & q x) \
\ ==> (l, LCons x l') : findRel q --> ~ p x \
\ --> l' : Domain (findRel (%x. p x & q x))";
by (etac findRel.induct 1);
@@ -222,7 +222,7 @@
qed_spec_mp "findRel_not_conj_Domain";
-Goal "!!p. (l,lxx) : findRel q ==> \
+Goal "(l,lxx) : findRel q ==> \
\ lxx = LCons x lx --> (lx,lz) : findRel(%x. p x & q x) --> ~ p x \
\ --> (l,lz) : findRel (%x. p x & q x)";
by (etac findRel.induct 1);
@@ -230,7 +230,7 @@
qed_spec_mp "findRel_conj2";
-Goal "!!p. (lx,ly) : findRel p \
+Goal "(lx,ly) : findRel p \
\ ==> ALL l. lx = lfilter q l \
\ --> l : Domain (findRel(%x. p x & q x))";
by (etac findRel.induct 1);
@@ -245,7 +245,7 @@
qed_spec_mp "findRel_lfilter_Domain_conj";
-Goal "!!p. (l,l'') : findRel(%x. p x & q x) \
+Goal "(l,l'') : findRel(%x. p x & q x) \
\ ==> l'' = LCons y l' --> \
\ (lfilter q l, LCons y (lfilter q l')) : findRel p";
by (etac findRel.induct 1);
@@ -299,13 +299,13 @@
lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)
***)
-Goal "!!p. (l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
+Goal "(l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
by (etac findRel.induct 1);
by (ALLGOALS Asm_full_simp_tac);
qed "findRel_lmap_Domain";
-Goal "!!p. lmap f l = LCons x l' --> \
+Goal "lmap f l = LCons x l' --> \
\ (EX y l''. x = f y & l' = lmap f l'' & l = LCons y l'')";
by (stac (lmap_def RS def_llist_corec) 1);
by (res_inst_tac [("l", "l")] llistE 1);
@@ -313,7 +313,7 @@
qed_spec_mp "lmap_eq_LCons";
-Goal "!!p. (lx,ly) : findRel p ==> \
+Goal "(lx,ly) : findRel p ==> \
\ ALL l. lmap f l = lx --> ly = LCons x l' --> \
\ (EX y l''. x = f y & l' = lmap f l'' & \
\ (l, LCons y l'') : findRel(%x. p(f x)))";
--- a/src/HOL/Induct/LList.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/LList.ML Wed Jul 15 10:15:13 1998 +0200
@@ -13,7 +13,7 @@
Addsplits [split_split, split_sum_case];
(*This justifies using llist in other recursive type definitions*)
-Goalw llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
+Goalw llist.defs "A<=B ==> llist(A) <= llist(B)";
by (rtac gfp_mono 1);
by (REPEAT (ares_tac basic_monos 1));
qed "llist_mono";
@@ -190,7 +190,7 @@
THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
**)
-Goalw [LListD_Fun_def] "!!A B. A<=B ==> LListD_Fun r A <= LListD_Fun r B";
+Goalw [LListD_Fun_def] "A<=B ==> LListD_Fun r A <= LListD_Fun r B";
by (REPEAT (ares_tac basic_monos 1));
qed "LListD_Fun_mono";
@@ -335,7 +335,7 @@
(*A typical use of co-induction to show membership in the gfp.
The containing set is simply the singleton {Lconst(M)}. *)
-Goal "!!M A. M:A ==> Lconst(M): llist(A)";
+Goal "M:A ==> Lconst(M): llist(A)";
by (rtac (singletonI RS llist_coinduct) 1);
by Safe_tac;
by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1);
@@ -522,12 +522,12 @@
Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI];
-Goal "!!M. M: llist(A) ==> Lappend NIL M = M";
+Goal "M: llist(A) ==> Lappend NIL M = M";
by (etac LList_fun_equalityI 1);
by (ALLGOALS Asm_simp_tac);
qed "Lappend_NIL";
-Goal "!!M. M: llist(A) ==> Lappend M NIL = M";
+Goal "M: llist(A) ==> Lappend M NIL = M";
by (etac LList_fun_equalityI 1);
by (ALLGOALS Asm_simp_tac);
qed "Lappend_NIL2";
--- a/src/HOL/Induct/Mutil.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Mutil.ML Wed Jul 15 10:15:13 1998 +0200
@@ -10,7 +10,7 @@
(** The union of two disjoint tilings is a tiling **)
-Goal "!!t. t: tiling A ==> \
+Goal "t: tiling A ==> \
\ u: tiling A --> t <= Compl u --> t Un u : tiling A";
by (etac tiling.induct 1);
by (Simp_tac 1);
@@ -101,7 +101,7 @@
(*** Dominoes ***)
-Goal "!!d. [| d:domino; b<2 |] ==> EX i j. evnodd d b = {(i,j)}";
+Goal "[| d:domino; b<2 |] ==> EX i j. evnodd d b = {(i,j)}";
by (eresolve_tac [domino.elim] 1);
by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2);
by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
@@ -111,20 +111,20 @@
THEN Blast_tac 1));
qed "domino_singleton";
-Goal "!!d. d:domino ==> finite d";
+Goal "d:domino ==> finite d";
by (blast_tac (claset() addSEs [domino.elim]) 1);
qed "domino_finite";
(*** Tilings of dominoes ***)
-Goal "!!t. t:tiling domino ==> finite t";
+Goal "t:tiling domino ==> finite t";
by (eresolve_tac [tiling.induct] 1);
by (rtac Finites.emptyI 1);
by (blast_tac (claset() addSIs [finite_UnI] addIs [domino_finite]) 1);
qed "tiling_domino_finite";
-Goal "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
+Goal "t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
by (eresolve_tac [tiling.induct] 1);
by (simp_tac (simpset() addsimps [evnodd_def]) 1);
by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1);
@@ -132,7 +132,7 @@
by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
by (Simp_tac 2 THEN assume_tac 1);
by (Clarify_tac 1);
-by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
+by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd t b" 1);
by (asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1);
by (blast_tac (claset() addSDs [evnodd_subset RS subsetD]
addEs [equalityE]) 1);
@@ -140,7 +140,7 @@
(*Final argument is surprisingly complex. Note the use of small simpsets
to avoid moving Sucs, etc.*)
-Goal "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n); \
+Goal "[| t = below(Suc m + Suc m) Times below(Suc n + Suc n); \
\ t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))} \
\ |] ==> t' ~: tiling domino";
by (rtac notI 1);
--- a/src/HOL/Induct/Perm.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Perm.ML Wed Jul 15 10:15:13 1998 +0200
@@ -22,23 +22,23 @@
(** Some examples of rule induction on permutations **)
(*The form of the premise lets the induction bind xs and ys.*)
-Goal "!!xs. xs <~~> ys ==> xs=[] --> ys=[]";
+Goal "xs <~~> ys ==> xs=[] --> ys=[]";
by (etac perm.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "perm_Nil_lemma";
(*A more general version is actually easier to understand!*)
-Goal "!!xs. xs <~~> ys ==> length(xs) = length(ys)";
+Goal "xs <~~> ys ==> length(xs) = length(ys)";
by (etac perm.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "perm_length";
-Goal "!!xs. xs <~~> ys ==> ys <~~> xs";
+Goal "xs <~~> ys ==> ys <~~> xs";
by (etac perm.induct 1);
by (REPEAT (ares_tac perm.intrs 1));
qed "perm_sym";
-Goal "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
+Goal "[| xs <~~> ys |] ==> x mem xs --> x mem ys";
by (etac perm.induct 1);
by (Fast_tac 4);
by (ALLGOALS Asm_simp_tac);
@@ -84,13 +84,13 @@
by (etac perm.Cons 1);
qed "perm_rev";
-Goal "!!xs. xs <~~> ys ==> l@xs <~~> l@ys";
+Goal "xs <~~> ys ==> l@xs <~~> l@ys";
by (list.induct_tac "l" 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset() addsimps [perm.Cons]) 1);
qed "perm_append1";
-Goal "!!xs. xs <~~> ys ==> xs@l <~~> ys@l";
+Goal "xs <~~> ys ==> xs@l <~~> ys@l";
by (rtac (perm_append_swap RS perm.trans) 1);
by (etac (perm_append1 RS perm.trans) 1);
by (rtac perm_append_swap 1);
--- a/src/HOL/Induct/PropLog.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/PropLog.ML Wed Jul 15 10:15:13 1998 +0200
@@ -11,7 +11,7 @@
open PropLog;
(** Monotonicity **)
-Goalw thms.defs "!!G H. G<=H ==> thms(G) <= thms(H)";
+Goalw thms.defs "G<=H ==> thms(G) <= thms(H)";
by (rtac lfp_mono 1);
by (REPEAT (ares_tac basic_monos 1));
qed "thms_mono";
@@ -34,12 +34,12 @@
val weaken_left_Un1 = Un_upper1 RS weaken_left;
val weaken_left_Un2 = Un_upper2 RS weaken_left;
-Goal "!!H. H |- q ==> H |- p->q";
+Goal "H |- q ==> H |- p->q";
by (fast_tac (claset() addIs [thms.K,thms.MP]) 1);
qed "weaken_right";
(*The deduction theorem*)
-Goal "!!H. insert p H |- q ==> H |- p->q";
+Goal "insert p H |- q ==> H |- p->q";
by (etac thms.induct 1);
by (ALLGOALS
(fast_tac (claset() addIs [thms_I, thms.H, thms.K, thms.S, thms.DN,
@@ -75,7 +75,7 @@
Addsimps [eval_false, eval_var, eval_imp];
(*Soundness of the rules wrt truth-table semantics*)
-Goalw [sat_def] "!!H. H |- p ==> H |= p";
+Goalw [sat_def] "H |- p ==> H |= p";
by (etac thms.induct 1);
by (fast_tac (claset() addSDs [eval_imp RS iffD1 RS mp]) 5);
by (ALLGOALS Asm_simp_tac);
@@ -83,7 +83,7 @@
(*** Towards the completeness proof ***)
-Goal "!!H. H |- p->false ==> H |- p->q";
+Goal "H |- p->false ==> H |- p->q";
by (rtac deduction 1);
by (etac (weaken_left_insert RS thms_notE) 1);
by (rtac thms.H 1);
@@ -206,12 +206,12 @@
qed "completeness_0";
(*A semantic analogue of the Deduction Theorem*)
-Goalw [sat_def] "!!p H. insert p H |= q ==> H |= p->q";
+Goalw [sat_def] "insert p H |= q ==> H |= p->q";
by (Simp_tac 1);
by (Fast_tac 1);
qed "sat_imp";
-Goal "!!H. finite H ==> !p. H |= p --> H |- p";
+Goal "finite H ==> !p. H |= p --> H |- p";
by (etac finite_induct 1);
by (safe_tac ((claset_of Fun.thy) addSIs [completeness_0]));
by (rtac (weaken_left_insert RS thms.MP) 1);
@@ -221,6 +221,6 @@
val completeness = completeness_lemma RS spec RS mp;
-Goal "!!H. finite H ==> (H |- p) = (H |= p)";
+Goal "finite H ==> (H |- p) = (H |= p)";
by (fast_tac (claset() addSEs [soundness, completeness]) 1);
qed "syntax_iff_semantics";
--- a/src/HOL/Induct/SList.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/SList.ML Wed Jul 15 10:15:13 1998 +0200
@@ -18,7 +18,7 @@
qed "list_unfold";
(*This justifies using list in other recursive type definitions*)
-Goalw list.defs "!!A B. A<=B ==> list(A) <= list(B)";
+Goalw list.defs "A<=B ==> list(A) <= list(B)";
by (rtac lfp_mono 1);
by (REPEAT (ares_tac basic_monos 1));
qed "list_mono";
@@ -113,7 +113,7 @@
AddIffs [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq];
-Goal "!!N. N: list(A) ==> !M. N ~= CONS M N";
+Goal "N: list(A) ==> !M. N ~= CONS M N";
by (etac list.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "not_CONS_self";
@@ -191,7 +191,7 @@
by (Simp_tac 1);
qed "List_rec_NIL";
-Goal "!!M. [| M: sexp; N: sexp |] ==> \
+Goal "[| M: sexp; N: sexp |] ==> \
\ List_rec (CONS M N) c h = h M N (List_rec N c h)";
by (rtac (List_rec_unfold RS trans) 1);
by (asm_simp_tac (simpset() addsimps [pred_sexp_CONS_I2]) 1);
@@ -246,9 +246,9 @@
by (rtac list_rec_Cons 1);
qed "Rep_map_Cons";
-Goalw [Rep_map_def] "!!f. (!!x. f(x): A) ==> Rep_map f xs: list(A)";
+val prems = Goalw [Rep_map_def] "(!!x. f(x): A) ==> Rep_map f xs: list(A)";
by (rtac list_induct2 1);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
qed "Rep_map_type";
Goalw [Abs_map_def] "Abs_map g NIL = Nil";
@@ -366,11 +366,12 @@
by (ALLGOALS Asm_simp_tac);
qed "map_compose2";
-Goal "!!f. (!!x. f(x): sexp) ==> \
+val prems =
+Goal "(!!x. f(x): sexp) ==> \
\ Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs";
by (list_ind_tac "xs" 1);
by (ALLGOALS (asm_simp_tac(simpset() addsimps
- [Rep_map_type, list_sexp RS subsetD])));
+ (prems@[Rep_map_type, list_sexp RS subsetD]))));
qed "Abs_Rep_map";
Addsimps [append_Nil4, map_ident2];
--- a/src/HOL/Induct/Simult.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Simult.ML Wed Jul 15 10:15:13 1998 +0200
@@ -23,7 +23,7 @@
val TF_unfold = TF_fun_mono RS (TF_def RS def_lfp_Tarski);
-Goalw [TF_def] "!!A B. A<=B ==> TF(A) <= TF(B)";
+Goalw [TF_def] "A<=B ==> TF(A) <= TF(B)";
by (REPEAT (ares_tac [lfp_mono, subset_refl, usum_mono, uprod_mono] 1));
qed "TF_mono";
--- a/src/HOL/Induct/Term.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Term.ML Wed Jul 15 10:15:13 1998 +0200
@@ -17,7 +17,7 @@
qed "term_unfold";
(*This justifies using term in other recursive type definitions*)
-Goalw term.defs "!!A B. A<=B ==> term(A) <= term(B)";
+Goalw term.defs "A<=B ==> term(A) <= term(B)";
by (REPEAT (ares_tac ([lfp_mono, list_mono] @ basic_monos) 1));
qed "term_mono";
--- a/src/HOL/Integ/Equiv.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Integ/Equiv.ML Wed Jul 15 10:15:13 1998 +0200
@@ -49,7 +49,7 @@
by (Blast_tac 1);
qed "equiv_class_subset";
-Goal "!!A r. [| equiv A r; (a,b): r |] ==> r^^{a} = r^^{b}";
+Goal "[| equiv A r; (a,b): r |] ==> r^^{a} = r^^{b}";
by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
by (rewrite_goals_tac [equiv_def,sym_def]);
by (Blast_tac 1);
@@ -98,7 +98,7 @@
(** Introduction/elimination rules -- needed? **)
-Goalw [quotient_def] "!!A. x:A ==> r^^{x}: A/r";
+Goalw [quotient_def] "x:A ==> r^^{x}: A/r";
by (Blast_tac 1);
qed "quotientI";
@@ -139,7 +139,7 @@
**)
(*Conversion rule*)
-Goal "!!A r. [| equiv A r; congruent r b; a: A |] \
+Goal "[| equiv A r; congruent r b; a: A |] \
\ ==> (UN x:r^^{a}. b(x)) = b(a)";
by (rtac (equiv_class_self RS UN_singleton) 1 THEN REPEAT (assume_tac 1));
by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]);
@@ -244,7 +244,7 @@
(*** Cardinality results suggested by Florian Kammueller ***)
(*Recall that equiv A r implies r <= A Times A (equiv_type) *)
-Goal "!!A. [| finite A; r <= A Times A |] ==> finite (A/r)";
+Goal "[| finite A; r <= A Times A |] ==> finite (A/r)";
by (rtac finite_subset 1);
by (etac (finite_Pow_iff RS iffD2) 2);
by (rewtac quotient_def);
@@ -258,7 +258,7 @@
by (Blast_tac 1);
qed "finite_equiv_class";
-Goal "!!A. [| finite A; equiv A r; ! X : A/r. k dvd card(X) |] \
+Goal "[| finite A; equiv A r; ! X : A/r. k dvd card(X) |] \
\ ==> k dvd card(A)";
by (rtac (Union_quotient RS subst) 1);
by (assume_tac 1);
--- a/src/HOL/Integ/Integ.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Integ/Integ.ML Wed Jul 15 10:15:13 1998 +0200
@@ -568,7 +568,7 @@
by (simp_tac (simpset() addsimps [zadd, zminus]) 1);
qed "zless_zadd_Suc";
-Goal "!!z1 z2 z3. [| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
+Goal "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
by (simp_tac
(simpset() addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1);
@@ -598,7 +598,7 @@
(* z<z ==> R *)
bind_thm ("zless_irrefl", (zless_not_refl RS notE));
-Goal "!!w. z<w ==> w ~= (z::int)";
+Goal "z<w ==> w ~= (z::int)";
by (fast_tac (claset() addEs [zless_irrefl]) 1);
qed "zless_not_refl2";
@@ -629,30 +629,30 @@
by (simp_tac (simpset() addsimps [zless_eq_less]) 1);
qed "zle_eq_le";
-Goalw [zle_def] "!!w. ~(w<z) ==> z<=(w::int)";
+Goalw [zle_def] "~(w<z) ==> z<=(w::int)";
by (assume_tac 1);
qed "zleI";
-Goalw [zle_def] "!!w. z<=w ==> ~(w<(z::int))";
+Goalw [zle_def] "z<=w ==> ~(w<(z::int))";
by (assume_tac 1);
qed "zleD";
val zleE = make_elim zleD;
-Goalw [zle_def] "!!z. ~ z <= w ==> w<(z::int)";
+Goalw [zle_def] "~ z <= w ==> w<(z::int)";
by (Fast_tac 1);
qed "not_zleE";
-Goalw [zle_def] "!!z. z < w ==> z <= (w::int)";
+Goalw [zle_def] "z < w ==> z <= (w::int)";
by (fast_tac (claset() addEs [zless_asym]) 1);
qed "zless_imp_zle";
-Goalw [zle_def] "!!z. z <= w ==> z < w | z=(w::int)";
+Goalw [zle_def] "z <= w ==> z < w | z=(w::int)";
by (cut_facts_tac [zless_linear] 1);
by (fast_tac (claset() addEs [zless_irrefl,zless_asym]) 1);
qed "zle_imp_zless_or_eq";
-Goalw [zle_def] "!!z. z<w | z=w ==> z <=(w::int)";
+Goalw [zle_def] "z<w | z=w ==> z <=(w::int)";
by (cut_facts_tac [zless_linear] 1);
by (fast_tac (claset() addEs [zless_irrefl,zless_asym]) 1);
qed "zless_or_eq_imp_zle";
@@ -670,12 +670,12 @@
by (fast_tac (claset() addIs [zless_trans]) 1);
qed "zle_zless_trans";
-Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::int)";
+Goal "[| i <= j; j <= k |] ==> i <= (k::int)";
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
rtac zless_or_eq_imp_zle, fast_tac (claset() addIs [zless_trans])]);
qed "zle_trans";
-Goal "!!z. [| z <= w; w <= z |] ==> z = (w::int)";
+Goal "[| z <= w; w <= z |] ==> z = (w::int)";
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
fast_tac (claset() addEs [zless_irrefl,zless_asym])]);
qed "zle_anti_sym";
@@ -736,7 +736,7 @@
Addsimps [zless_eq_less, zle_eq_le,
znegative_zminus_znat, not_znegative_znat];
-Goal "!! x. (x::int) = y ==> x <= y";
+Goal "(x::int) = y ==> x <= y";
by (etac subst 1); by (rtac zle_refl 1);
qed "zequalD1";
@@ -822,16 +822,16 @@
Addsimps [zminus_zless_zminus, zminus_zle_zminus,
negative_eq_positive, not_znat_zless_negative];
-Goalw [zdiff_def,zless_def] "!! x. znegative x = (x < $# 0)";
+Goalw [zdiff_def,zless_def] "znegative x = (x < $# 0)";
by Auto_tac;
qed "znegative_less_0";
-Goalw [zdiff_def,zless_def] "!! x. (~znegative x) = ($# 0 <= x)";
+Goalw [zdiff_def,zless_def] "(~znegative x) = ($# 0 <= x)";
by (stac znegative_less_0 1);
by (safe_tac (HOL_cs addSDs[zleD,not_zleE,zleI]) );
qed "not_znegative_ge_0";
-Goal "!! x. znegative x ==> ? n. x = $~ $# Suc n";
+Goal "znegative x ==> ? n. x = $~ $# Suc n";
by (dtac (znegative_less_0 RS iffD1 RS zless_eq_zadd_Suc) 1);
by (etac exE 1);
by (rtac exI 1);
@@ -839,7 +839,7 @@
by (auto_tac(claset(), simpset() addsimps [zadd_assoc]));
qed "znegativeD";
-Goal "!! x. ~znegative x ==> ? n. x = $# n";
+Goal "~znegative x ==> ? n. x = $# n";
by (dtac (not_znegative_ge_0 RS iffD1) 1);
by (dtac zle_imp_zless_or_eq 1);
by (etac disjE 1);
--- a/src/HOL/Map.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Map.ML Wed Jul 15 10:15:13 1998 +0200
@@ -108,7 +108,7 @@
qed "ran_empty";
Addsimps [ran_empty];
-Goalw [ran_def] "!!X. m a = None ==> ran(m[a|->b]) = insert b (ran m)";
+Goalw [ran_def] "m a = None ==> ran(m[a|->b]) = insert b (ran m)";
by Auto_tac;
by (subgoal_tac "~(aa = a)" 1);
by Auto_tac;
--- a/src/HOL/NatDef.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/NatDef.ML Wed Jul 15 10:15:13 1998 +0200
@@ -130,7 +130,7 @@
bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
-Goal "!!n. n ~= 0 ==> EX m. n = Suc m";
+Goal "n ~= 0 ==> EX m. n = Suc m";
by (rtac natE 1);
by (REPEAT (Blast_tac 1));
qed "not0_implies_Suc";
@@ -246,7 +246,7 @@
(* n<n ==> R *)
bind_thm ("less_irrefl", (less_not_refl RS notE));
-Goal "!!m. n<m ==> m ~= (n::nat)";
+Goal "n<m ==> m ~= (n::nat)";
by (blast_tac (claset() addSEs [less_irrefl]) 1);
qed "less_not_refl2";
@@ -313,14 +313,14 @@
qed "not_gr0";
Addsimps [not_gr0];
-Goal "!!m. m<n ==> 0 < n";
+Goal "m<n ==> 0 < n";
by (dtac gr_implies_not0 1);
by (Asm_full_simp_tac 1);
qed "gr_implies_gr0";
Addsimps [gr_implies_gr0];
-Goal "!!m n. m<n ==> Suc(m) < Suc(n)";
+Goal "m<n ==> Suc(m) < Suc(n)";
by (etac rev_mp 1);
by (nat_ind_tac "n" 1);
by (ALLGOALS (fast_tac (claset() addEs [less_trans, lessE])));
@@ -354,7 +354,7 @@
(** Inductive (?) properties **)
-Goal "!!m. [| m<n; Suc m ~= n |] ==> Suc(m) < n";
+Goal "[| m<n; Suc m ~= n |] ==> Suc(m) < n";
by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
by (blast_tac (claset() addSEs [less_irrefl, less_SucE] addEs [less_asym]) 1);
qed "Suc_lessI";
@@ -375,7 +375,7 @@
by (assume_tac 1);
qed "Suc_lessE";
-Goal "!!m n. Suc(m) < Suc(n) ==> m<n";
+Goal "Suc(m) < Suc(n) ==> m<n";
by (blast_tac (claset() addEs [lessE, make_elim Suc_lessD]) 1);
qed "Suc_less_SucD";
@@ -390,7 +390,7 @@
qed "not_Suc_n_less_n";
Addsimps [not_Suc_n_less_n];
-Goal "!!i. i<j ==> j<k --> Suc i < k";
+Goal "i<j ==> j<k --> Suc i < k";
by (nat_ind_tac "k" 1);
by (ALLGOALS (asm_simp_tac (simpset())));
by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
@@ -456,7 +456,7 @@
n_not_Suc_n, Suc_n_not_n,
nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
-Goal "!!m. (m <= Suc(n)) = (m<=n | m = Suc n)";
+Goal "(m <= Suc(n)) = (m<=n | m = Suc n)";
by (simp_tac (simpset() addsimps [le_eq_less_Suc]) 1);
by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1);
qed "le_Suc_eq";
@@ -501,7 +501,7 @@
by (blast_tac (claset() addIs [leI] addEs [leE]) 1);
qed "not_less_iff_le";
-Goalw [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
+Goalw [le_def] "~ m <= n ==> n<(m::nat)";
by (Blast_tac 1);
qed "not_leE";
@@ -509,12 +509,12 @@
by (Simp_tac 1);
qed "not_le_iff_less";
-Goalw [le_def] "!!m. m < n ==> Suc(m) <= n";
+Goalw [le_def] "m < n ==> Suc(m) <= n";
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
by (blast_tac (claset() addSEs [less_irrefl,less_asym]) 1);
qed "Suc_leI"; (*formerly called lessD*)
-Goalw [le_def] "!!m. Suc(m) <= n ==> m <= n";
+Goalw [le_def] "Suc(m) <= n ==> m <= n";
by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
qed "Suc_leD";
@@ -530,25 +530,25 @@
by (blast_tac (claset() addIs [Suc_leI, Suc_le_lessD]) 1);
qed "Suc_le_eq";
-Goalw [le_def] "!!m. m <= n ==> m <= Suc n";
+Goalw [le_def] "m <= n ==> m <= Suc n";
by (blast_tac (claset() addDs [Suc_lessD]) 1);
qed "le_SucI";
Addsimps[le_SucI];
bind_thm ("le_Suc", not_Suc_n_less_n RS leI);
-Goalw [le_def] "!!m. m < n ==> m <= (n::nat)";
+Goalw [le_def] "m < n ==> m <= (n::nat)";
by (blast_tac (claset() addEs [less_asym]) 1);
qed "less_imp_le";
(** Equivalence of m<=n and m<n | m=n **)
-Goalw [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
+Goalw [le_def] "m <= n ==> m < n | m=(n::nat)";
by (cut_facts_tac [less_linear] 1);
by (blast_tac (claset() addEs [less_irrefl,less_asym]) 1);
qed "le_imp_less_or_eq";
-Goalw [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
+Goalw [le_def] "m<n | m=n ==> m <=(n::nat)";
by (cut_facts_tac [less_linear] 1);
by (blast_tac (claset() addSEs [less_irrefl] addEs [less_asym]) 1);
qed "less_or_eq_imp_le";
@@ -564,22 +564,22 @@
by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
qed "le_refl";
-Goal "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
+Goal "[| i <= j; j < k |] ==> i < (k::nat)";
by (blast_tac (claset() addSDs [le_imp_less_or_eq]
addIs [less_trans]) 1);
qed "le_less_trans";
-Goal "!!i. [| i < j; j <= k |] ==> i < (k::nat)";
+Goal "[| i < j; j <= k |] ==> i < (k::nat)";
by (blast_tac (claset() addSDs [le_imp_less_or_eq]
addIs [less_trans]) 1);
qed "less_le_trans";
-Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
+Goal "[| i <= j; j <= k |] ==> i <= (k::nat)";
by (blast_tac (claset() addSDs [le_imp_less_or_eq]
addIs [less_or_eq_imp_le, less_trans]) 1);
qed "le_trans";
-Goal "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
+Goal "[| m <= n; n <= m |] ==> m = (n::nat)";
(*order_less_irrefl could make this proof fail*)
by (blast_tac (claset() addSDs [le_imp_less_or_eq]
addSEs [less_irrefl] addEs [less_asym]) 1);
--- a/src/HOL/Ord.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Ord.ML Wed Jul 15 10:15:13 1998 +0200
@@ -42,8 +42,8 @@
(** min **)
-Goalw [min_def] "!!least. (!!x. least <= x) ==> min least x = least";
-by (Asm_simp_tac 1);
+val prems = Goalw [min_def] "(!!x. least <= x) ==> min least x = least";
+by (simp_tac (simpset() addsimps prems) 1);
qed "min_leastL";
val prems = goalw thy [min_def]
--- a/src/HOL/Power.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Power.ML Wed Jul 15 10:15:13 1998 +0200
@@ -22,7 +22,7 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps [power_add])));
qed "power_mult";
-Goal "!! i. 0 < i ==> 0 < i^n";
+Goal "0 < i ==> 0 < i^n";
by (induct_tac "n" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [zero_less_mult_iff])));
qed "zero_less_power";
@@ -33,14 +33,14 @@
by (Blast_tac 1);
qed "le_imp_power_dvd";
-Goal "!! i r. [| 0 < i; i^m < i^n |] ==> m<n";
+Goal "[| 0 < i; i^m < i^n |] ==> m<n";
by (rtac ccontr 1);
by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
by (etac zero_less_power 1);
by (contr_tac 1);
qed "power_less_imp_less";
-Goal "!!n. k^j dvd n --> i<j --> k^i dvd n";
+Goal "k^j dvd n --> i<j --> k^i dvd n";
by (induct_tac "j" 1);
by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
by (stac mult_commute 1);
--- a/src/HOL/Prod.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Prod.ML Wed Jul 15 10:15:13 1998 +0200
@@ -189,7 +189,7 @@
by (Asm_simp_tac 1);
qed "splitI2";
-Goal "!!a b c. c a b ==> split c (a,b)";
+Goal "c a b ==> split c (a,b)";
by (Asm_simp_tac 1);
qed "splitI";
@@ -204,11 +204,11 @@
rtac (split_beta RS subst) 1,
rtac (hd prems) 1]);
-Goal "!!R a b. split R (a,b) ==> R a b";
+Goal "split R (a,b) ==> R a b";
by (etac (split RS iffD1) 1);
qed "splitD";
-Goal "!!a b c. z: c a b ==> z: split c (a,b)";
+Goal "z: c a b ==> z: split c (a,b)";
by (Asm_simp_tac 1);
qed "mem_splitI";
@@ -241,7 +241,7 @@
but cannot be used as rewrite rule:
### Cannot add premise as rewrite rule because it contains (type) unknowns:
### ?y = .x
-Goal "!!P. [| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
+Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
by (rtac select_equality 1);
by ( Simp_tac 1);
by (split_all_tac 1);
--- a/src/HOL/Real/Lubs.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Real/Lubs.ML Wed Jul 15 10:15:13 1998 +0200
@@ -10,34 +10,34 @@
(*------------------------------------------------------------------------
Rules for *<= and <=*
------------------------------------------------------------------------*)
-Goalw [setle_def] "!!x. ALL y: S. y <= x ==> S *<= x";
+Goalw [setle_def] "ALL y: S. y <= x ==> S *<= x";
by (assume_tac 1);
qed "setleI";
-Goalw [setle_def] "!!x. [| S *<= x; y: S |] ==> y <= x";
+Goalw [setle_def] "[| S *<= x; y: S |] ==> y <= x";
by (Fast_tac 1);
qed "setleD";
-Goalw [setge_def] "!!x. ALL y: S. x<= y ==> x <=* S";
+Goalw [setge_def] "ALL y: S. x<= y ==> x <=* S";
by (assume_tac 1);
qed "setgeI";
-Goalw [setge_def] "!!x. [| x <=* S; y: S |] ==> x <= y";
+Goalw [setge_def] "[| x <=* S; y: S |] ==> x <= y";
by (Fast_tac 1);
qed "setgeD";
(*------------------------------------------------------------------------
Rules about leastP, ub and lub
------------------------------------------------------------------------*)
-Goalw [leastP_def] "!!x. leastP P x ==> P x";
+Goalw [leastP_def] "leastP P x ==> P x";
by (Step_tac 1);
qed "leastPD1";
-Goalw [leastP_def] "!!x. leastP P x ==> x <=* Collect P";
+Goalw [leastP_def] "leastP P x ==> x <=* Collect P";
by (Step_tac 1);
qed "leastPD2";
-Goal "!!x. [| leastP P x; y: Collect P |] ==> x <= y";
+Goal "[| leastP P x; y: Collect P |] ==> x <= y";
by (blast_tac (claset() addSDs [leastPD2,setgeD]) 1);
qed "leastPD3";
@@ -51,19 +51,19 @@
by (Step_tac 1);
qed "isLubD1a";
-Goalw [isUb_def] "!!x. isLub R S x ==> isUb R S x";
+Goalw [isUb_def] "isLub R S x ==> isUb R S x";
by (blast_tac (claset() addDs [isLubD1,isLubD1a]) 1);
qed "isLub_isUb";
-Goal "!!x. [| isLub R S x; y : S |] ==> y <= x";
+Goal "[| isLub R S x; y : S |] ==> y <= x";
by (blast_tac (claset() addSDs [isLubD1,setleD]) 1);
qed "isLubD2";
-Goalw [isLub_def] "!!x. isLub R S x ==> leastP(isUb R S) x";
+Goalw [isLub_def] "isLub R S x ==> leastP(isUb R S) x";
by (assume_tac 1);
qed "isLubD3";
-Goalw [isLub_def] "!!x. leastP(isUb R S) x ==> isLub R S x";
+Goalw [isLub_def] "leastP(isUb R S) x ==> isLub R S x";
by (assume_tac 1);
qed "isLubI1";
@@ -72,27 +72,27 @@
by (Step_tac 1);
qed "isLubI2";
-Goalw [isUb_def] "!!x. [| isUb R S x; y : S |] ==> y <= x";
+Goalw [isUb_def] "[| isUb R S x; y : S |] ==> y <= x";
by (fast_tac (claset() addDs [setleD]) 1);
qed "isUbD";
-Goalw [isUb_def] "!!x. isUb R S x ==> S *<= x";
+Goalw [isUb_def] "isUb R S x ==> S *<= x";
by (Step_tac 1);
qed "isUbD2";
-Goalw [isUb_def] "!!x. isUb R S x ==> x: R";
+Goalw [isUb_def] "isUb R S x ==> x: R";
by (Step_tac 1);
qed "isUbD2a";
-Goalw [isUb_def] "!!x. [| S *<= x; x: R |] ==> isUb R S x";
+Goalw [isUb_def] "[| S *<= x; x: R |] ==> isUb R S x";
by (Step_tac 1);
qed "isUbI";
-Goalw [isLub_def] "!!x. [| isLub R S x; isUb R S y |] ==> x <= y";
+Goalw [isLub_def] "[| isLub R S x; isUb R S y |] ==> x <= y";
by (blast_tac (claset() addSIs [leastPD3]) 1);
qed "isLub_le_isUb";
-Goalw [ubs_def,isLub_def] "!!x. isLub R S x ==> x <=* ubs R S";
+Goalw [ubs_def,isLub_def] "isLub R S x ==> x <=* ubs R S";
by (etac leastPD2 1);
qed "isLub_ubs";
--- a/src/HOL/Real/PNat.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Real/PNat.ML Wed Jul 15 10:15:13 1998 +0200
@@ -102,12 +102,12 @@
Addsimps [zero_not_mem_pnat];
-Goal "!!x. x : pnat ==> 0 < x";
+Goal "x : pnat ==> 0 < x";
by (dtac (pnat_unfold RS subst) 1);
by Auto_tac;
qed "mem_pnat_gt_zero";
-Goal "!!x. 0 < x ==> x: pnat";
+Goal "0 < x ==> x: pnat";
by (stac pnat_unfold 1);
by (dtac (gr_implies_not0 RS not0_implies_Suc) 1);
by (etac exE 1 THEN Asm_simp_tac 1);
@@ -177,7 +177,7 @@
bind_thm ("pSuc_n_not_n", n_not_pSuc_n RS not_sym);
-Goal "!!n. n ~= 1p ==> EX m. n = pSuc m";
+Goal "n ~= 1p ==> EX m. n = pSuc m";
by (rtac pnatE 1);
by (REPEAT (Blast_tac 1));
qed "not1p_implies_pSuc";
@@ -245,14 +245,14 @@
by ((etac less_trans 1) THEN assume_tac 1);
qed "pnat_less_trans";
-Goalw [pnat_less_def] "!!x. x < (y::pnat) ==> ~ y < x";
+Goalw [pnat_less_def] "x < (y::pnat) ==> ~ y < x";
by (etac less_not_sym 1);
qed "pnat_less_not_sym";
(* [| x < y; y < x |] ==> P *)
bind_thm ("pnat_less_asym",pnat_less_not_sym RS notE);
-Goalw [pnat_less_def] "!!x. ~ y < (y::pnat)";
+Goalw [pnat_less_def] "~ y < (y::pnat)";
by Auto_tac;
qed "pnat_less_not_refl";
@@ -304,11 +304,11 @@
(*** pnat_le ***)
-Goalw [pnat_le_def] "!!x. ~ (x::pnat) < y ==> y <= x";
+Goalw [pnat_le_def] "~ (x::pnat) < y ==> y <= x";
by (assume_tac 1);
qed "pnat_leI";
-Goalw [pnat_le_def] "!!x. (x::pnat) <= y ==> ~ y < x";
+Goalw [pnat_le_def] "(x::pnat) <= y ==> ~ y < x";
by (assume_tac 1);
qed "pnat_leD";
@@ -318,22 +318,22 @@
by (blast_tac (claset() addIs [pnat_leI] addEs [pnat_leE]) 1);
qed "pnat_not_less_iff_le";
-Goalw [pnat_le_def] "!!x. ~(x::pnat) <= y ==> y < x";
+Goalw [pnat_le_def] "~(x::pnat) <= y ==> y < x";
by (Blast_tac 1);
qed "pnat_not_leE";
-Goalw [pnat_le_def] "!!x. (x::pnat) < y ==> x <= y";
+Goalw [pnat_le_def] "(x::pnat) < y ==> x <= y";
by (blast_tac (claset() addEs [pnat_less_asym]) 1);
qed "pnat_less_imp_le";
(** Equivalence of m<=n and m<n | m=n **)
-Goalw [pnat_le_def] "!!m. m <= n ==> m < n | m=(n::pnat)";
+Goalw [pnat_le_def] "m <= n ==> m < n | m=(n::pnat)";
by (cut_facts_tac [pnat_less_linear] 1);
by (blast_tac (claset() addEs [pnat_less_irrefl,pnat_less_asym]) 1);
qed "pnat_le_imp_less_or_eq";
-Goalw [pnat_le_def] "!!m. m<n | m=n ==> m <=(n::pnat)";
+Goalw [pnat_le_def] "m<n | m=n ==> m <=(n::pnat)";
by (cut_facts_tac [pnat_less_linear] 1);
by (blast_tac (claset() addSEs [pnat_less_irrefl] addEs [pnat_less_asym]) 1);
qed "pnat_less_or_eq_imp_le";
@@ -351,19 +351,19 @@
by (blast_tac (claset() addIs [pnat_less_trans]) 1);
qed "pnat_le_less_trans";
-Goal "!!i. [| i < j; j <= k |] ==> i < (k::pnat)";
+Goal "[| i < j; j <= k |] ==> i < (k::pnat)";
by (dtac pnat_le_imp_less_or_eq 1);
by (blast_tac (claset() addIs [pnat_less_trans]) 1);
qed "pnat_less_le_trans";
-Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::pnat)";
+Goal "[| i <= j; j <= k |] ==> i <= (k::pnat)";
by (EVERY1[dtac pnat_le_imp_less_or_eq,
dtac pnat_le_imp_less_or_eq,
rtac pnat_less_or_eq_imp_le,
blast_tac (claset() addIs [pnat_less_trans])]);
qed "pnat_le_trans";
-Goal "!!m. [| m <= n; n <= m |] ==> m = (n::pnat)";
+Goal "[| m <= n; n <= m |] ==> m = (n::pnat)";
by (EVERY1[dtac pnat_le_imp_less_or_eq,
dtac pnat_le_imp_less_or_eq,
blast_tac (claset() addIs [pnat_less_asym])]);
@@ -440,7 +440,7 @@
(*"i < j ==> i < m + j"*)
bind_thm ("pnat_trans_less_add2", pnat_le_add2 RSN (2,pnat_less_le_trans));
-Goalw [pnat_less_def] "!!i. i+j < (k::pnat) ==> i<k";
+Goalw [pnat_less_def] "i+j < (k::pnat) ==> i<k";
by (auto_tac (claset() addEs [add_lessD1],
simpset() addsimps [sum_Rep_pnat_sum RS sym]));
qed "pnat_add_lessD1";
--- a/src/HOL/Real/PRat.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Real/PRat.ML Wed Jul 15 10:15:13 1998 +0200
@@ -302,7 +302,7 @@
prat_mult_1,prat_mult_1_right]) 1);
qed "prat_qinv_left_ex1";
-Goal "!!y. x * y = $# Abs_pnat 1 ==> x = qinv y";
+Goal "x * y = $# Abs_pnat 1 ==> x = qinv y";
by (cut_inst_tac [("q","y")] prat_mult_qinv 1);
by (res_inst_tac [("x1","y")] (prat_qinv_left_ex1 RS ex1E) 1);
by (Blast_tac 1);
@@ -580,32 +580,32 @@
by (simp_tac (simpset() addsimps [prat_self_less_add_right]) 1);
qed "prat_self_less_add_left";
-Goalw [prat_less_def] "!!y. $#1p < y ==> (x::prat) < x * y";
+Goalw [prat_less_def] "$#1p < y ==> (x::prat) < x * y";
by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
prat_add_mult_distrib2]));
qed "prat_self_less_mult_right";
(*** Properties of <= ***)
-Goalw [prat_le_def] "!!w. ~(w < z) ==> z <= (w::prat)";
+Goalw [prat_le_def] "~(w < z) ==> z <= (w::prat)";
by (assume_tac 1);
qed "prat_leI";
-Goalw [prat_le_def] "!!w. z<=w ==> ~(w<(z::prat))";
+Goalw [prat_le_def] "z<=w ==> ~(w<(z::prat))";
by (assume_tac 1);
qed "prat_leD";
val prat_leE = make_elim prat_leD;
-Goal "!!w. (~(w < z)) = (z <= (w::prat))";
+Goal "(~(w < z)) = (z <= (w::prat))";
by (fast_tac (claset() addSIs [prat_leI,prat_leD]) 1);
qed "prat_less_le_iff";
-Goalw [prat_le_def] "!!z. ~ z <= w ==> w<(z::prat)";
+Goalw [prat_le_def] "~ z <= w ==> w<(z::prat)";
by (Fast_tac 1);
qed "not_prat_leE";
-Goalw [prat_le_def] "!!z. z < w ==> z <= (w::prat)";
+Goalw [prat_le_def] "z < w ==> z <= (w::prat)";
by (fast_tac (claset() addEs [prat_less_asym]) 1);
qed "prat_less_imp_le";
@@ -614,7 +614,7 @@
by (fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym]) 1);
qed "prat_le_imp_less_or_eq";
-Goalw [prat_le_def] "!!z. z<w | z=w ==> z <=(w::prat)";
+Goalw [prat_le_def] "z<w | z=w ==> z <=(w::prat)";
by (cut_facts_tac [prat_linear] 1);
by (fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym]) 1);
qed "prat_less_or_eq_imp_le";
@@ -637,17 +637,17 @@
by (fast_tac (claset() addIs [prat_less_trans]) 1);
qed "prat_less_le_trans";
-Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::prat)";
+Goal "[| i <= j; j <= k |] ==> i <= (k::prat)";
by (EVERY1 [dtac prat_le_imp_less_or_eq, dtac prat_le_imp_less_or_eq,
rtac prat_less_or_eq_imp_le, fast_tac (claset() addIs [prat_less_trans])]);
qed "prat_le_trans";
-Goal "!!z. [| z <= w; w <= z |] ==> z = (w::prat)";
+Goal "[| z <= w; w <= z |] ==> z = (w::prat)";
by (EVERY1 [dtac prat_le_imp_less_or_eq, dtac prat_le_imp_less_or_eq,
fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym])]);
qed "prat_le_anti_sym";
-Goal "!!x. [| ~ y < x; y ~= x |] ==> x < (y::prat)";
+Goal "[| ~ y < x; y ~= x |] ==> x < (y::prat)";
by (rtac not_prat_leE 1);
by (fast_tac (claset() addDs [prat_le_imp_less_or_eq]) 1);
qed "not_less_not_eq_prat_less";
--- a/src/HOL/Real/PReal.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Real/PReal.ML Wed Jul 15 10:15:13 1998 +0200
@@ -35,7 +35,7 @@
Addsimps [one_set_mem_preal];
-Goalw [preal_def] "!!x. x : preal ==> {} < x";
+Goalw [preal_def] "x : preal ==> {} < x";
by (Fast_tac 1);
qed "preal_psubset_empty";
@@ -188,7 +188,7 @@
(* A positive fraction not in a positive real is an upper bound *)
(* Gleason p. 122 - Remark (1) *)
-Goal "!!x. x ~: Rep_preal(R) ==> !y: Rep_preal(R). y < x";
+Goal "x ~: Rep_preal(R) ==> !y: Rep_preal(R). y < x";
by (cut_inst_tac [("x1","R")] (Rep_preal RS prealE_lemma) 1);
by (auto_tac (claset() addIs [not_less_not_eq_prat_less],simpset()));
qed "not_in_preal_ub";
@@ -488,40 +488,40 @@
simpset() addsimps [prat_add_mult_distrib2]));
qed "lemma_prat_add_mult_mono";
-Goal "!!xb. [| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
+Goal "[| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
\ Rep_preal w; yb: Rep_preal w |] ==> \
\ xb * ya + xc * yb: Rep_preal (z1 * w + z2 * w)";
by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1);
qed "lemma_add_mult_mem_Rep_preal";
-Goal "!!xb. [| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
+Goal "[| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
\ Rep_preal w; yb: Rep_preal w |] ==> \
\ yb*(xb + xc): Rep_preal (w*(z1 + z2))";
by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1);
qed "lemma_add_mult_mem_Rep_preal1";
-Goal "!!x. x: Rep_preal (w * z1 + w * z2) ==> \
+Goal "x: Rep_preal (w * z1 + w * z2) ==> \
\ x: Rep_preal (w * (z1 + z2))";
by (auto_tac (claset() addSDs [mem_Rep_preal_addD,mem_Rep_preal_multD],
simpset()));
-by (forw_inst_tac [("ya","xb"),("yb","xc"),("xb","ya"),("xc","yb")]
+by (forw_inst_tac [("ya","xa"),("yb","xb"),("xb","ya"),("xc","yb")]
lemma_add_mult_mem_Rep_preal1 1);
by Auto_tac;
-by (res_inst_tac [("q1.0","xb"),("q2.0","xc")] prat_linear_less2 1);
+by (res_inst_tac [("q1.0","xa"),("q2.0","xb")] prat_linear_less2 1);
by (dres_inst_tac [("b","ya"),("c","yb")] lemma_prat_add_mult_mono 1);
by (rtac (Rep_preal RS prealE_lemma3b) 1);
by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib2]));
-by (dres_inst_tac [("ya","xc"),("yb","xb"),("xc","ya"),("xb","yb")]
+by (dres_inst_tac [("ya","xb"),("yb","xa"),("xc","ya"),("xb","yb")]
lemma_add_mult_mem_Rep_preal1 1);
by Auto_tac;
by (dres_inst_tac [("b","yb"),("c","ya")] lemma_prat_add_mult_mono 1);
by (rtac (Rep_preal RS prealE_lemma3b) 1);
-by (thin_tac "xc * ya + xc * yb : Rep_preal (w * (z1 + z2))" 1);
+by (thin_tac "xb * ya + xb * yb : Rep_preal (w * (z1 + z2))" 1);
by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib,
prat_add_commute] @ preal_add_ac ));
qed "lemma_preal_add_mult_distrib";
-Goal "!!x. x: Rep_preal (w * (z1 + z2)) ==> \
+Goal "x: Rep_preal (w * (z1 + z2)) ==> \
\ x: Rep_preal (w * z1 + w * z2)";
by (auto_tac (claset() addSDs [mem_Rep_preal_addD,mem_Rep_preal_multD]
addSIs [bexI,mem_Rep_preal_addI,mem_Rep_preal_multI],
@@ -610,7 +610,7 @@
qed "preal_mem_inv_set";
(*more lemmas for inverse *)
-Goal "!!x. x: Rep_preal(pinv(A)*A) ==> x: Rep_preal(@#($#Abs_pnat 1))";
+Goal "x: Rep_preal(pinv(A)*A) ==> x: Rep_preal(@#($#Abs_pnat 1))";
by (auto_tac (claset() addSDs [mem_Rep_preal_multD],
simpset() addsimps [pinv_def,preal_prat_def] ));
by (dtac (preal_mem_inv_set RS Abs_preal_inverse RS subst) 1);
@@ -620,7 +620,7 @@
qed "preal_mem_mult_invD";
(*** Gleason's Lemma 9-3.4 p 122 ***)
-Goal "!!p. ! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
+Goal "! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
\ ? xb : Rep_preal(A). xb + ($#p)*x : Rep_preal(A)";
by (cut_facts_tac [mem_Rep_preal_Ex] 1);
by (res_inst_tac [("n","p")] pnat_induct 1);
@@ -637,7 +637,7 @@
simpset() addsimps [prat_mult,pre_lemma_gleason9_34b,pnat_mult_assoc]));
qed "lemma1b_gleason9_34";
-Goal "!!A. ! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> False";
+Goal "! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> False";
by (cut_inst_tac [("X","A")] not_mem_Rep_preal_Ex 1);
by (etac exE 1);
by (dtac not_in_preal_ub 1);
@@ -673,7 +673,7 @@
(******)
(*** FIXME: long! ***)
-Goal "!!A. $#1p < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
+Goal "$#1p < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
by (res_inst_tac [("X1","A")] (mem_Rep_preal_Ex RS exE) 1);
by (res_inst_tac [("Q","xa*x : Rep_preal(A)")] (excluded_middle RS disjE) 1);
by (Fast_tac 1);
@@ -696,13 +696,13 @@
by Auto_tac;
qed "lemma_gleason9_36";
-Goal "!!A. $#Abs_pnat 1 < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
+Goal "$#Abs_pnat 1 < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
by (rtac lemma_gleason9_36 1);
by (asm_simp_tac (simpset() addsimps [pnat_one_def]) 1);
qed "lemma_gleason9_36a";
(*** Part 2 of existence of inverse ***)
-Goal "!!x. x: Rep_preal(@#($#Abs_pnat 1)) ==> x: Rep_preal(pinv(A)*A)";
+Goal "x: Rep_preal(@#($#Abs_pnat 1)) ==> x: Rep_preal(pinv(A)*A)";
by (auto_tac (claset() addSIs [mem_Rep_preal_multI],
simpset() addsimps [pinv_def,preal_prat_def] ));
by (rtac (preal_mem_inv_set RS Abs_preal_inverse RS ssubst) 1);
@@ -786,11 +786,11 @@
by (auto_tac (claset(),simpset() addsimps [preal_less_def,psubset_def]));
qed "not_preal_leE";
-Goal "!!w. ~(w < z) ==> z <= (w::preal)";
+Goal "~(w < z) ==> z <= (w::preal)";
by (fast_tac (claset() addIs [not_preal_leE]) 1);
qed "preal_leI";
-Goal "!!w. (~(w < z)) = (z <= (w::preal))";
+Goal "(~(w < z)) = (z <= (w::preal))";
by (fast_tac (claset() addSIs [preal_leI,preal_leD]) 1);
qed "preal_less_le_iff";
@@ -827,17 +827,17 @@
by (fast_tac (claset() addIs [preal_less_trans]) 1);
qed "preal_less_le_trans";
-Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::preal)";
+Goal "[| i <= j; j <= k |] ==> i <= (k::preal)";
by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq,
rtac preal_less_or_eq_imp_le, fast_tac (claset() addIs [preal_less_trans])]);
qed "preal_le_trans";
-Goal "!!z. [| z <= w; w <= z |] ==> z = (w::preal)";
+Goal "[| z <= w; w <= z |] ==> z = (w::preal)";
by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq,
fast_tac (claset() addEs [preal_less_irrefl,preal_less_asym])]);
qed "preal_le_anti_sym";
-Goal "!!x. [| ~ y < x; y ~= x |] ==> x < (y::preal)";
+Goal "[| ~ y < x; y ~= x |] ==> x < (y::preal)";
by (rtac not_preal_leE 1);
by (fast_tac (claset() addDs [preal_le_imp_less_or_eq]) 1);
qed "not_less_not_eq_preal_less";
@@ -849,7 +849,7 @@
(**** Define the D required and show that it is a positive real ****)
(* useful lemmas - proved elsewhere? *)
-Goalw [psubset_def] "!!A. A < B ==> ? x. x ~: A & x : B";
+Goalw [psubset_def] "A < B ==> ? x. x ~: A & x : B";
by (etac conjE 1);
by (etac swap 1);
by (etac equalityI 1);
@@ -911,7 +911,7 @@
qed "preal_less_set_not_prat_set";
(** Part 3 of Dedekind sections def **)
-Goal "!!A. A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
+Goal "A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
\ !z. z < y --> z : {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
by Auto_tac;
by (dres_inst_tac [("x","n")] prat_add_less2_mono2 1);
@@ -919,7 +919,7 @@
by Auto_tac;
qed "preal_less_set_lemma3";
-Goal "!!A. A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
+Goal "A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
\ Bex {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} (op < y)";
by Auto_tac;
by (dtac (Rep_preal RS prealE_lemma4a) 1);
@@ -954,7 +954,7 @@
(** proving that B <= A + D --- trickier **)
(** lemma **)
-Goal "!!x. x : Rep_preal(B) ==> ? e. x + e : Rep_preal(B)";
+Goal "x : Rep_preal(B) ==> ? e. x + e : Rep_preal(B)";
by (dtac (Rep_preal RS prealE_lemma4a) 1);
by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
qed "lemma_sum_mem_Rep_preal_ex";
@@ -1115,7 +1115,7 @@
(*** Completeness of preal ***)
(*** prove that supremum is a cut ***)
-Goal "!!P. ? (X::preal). X: P ==> \
+Goal "? (X::preal). X: P ==> \
\ ? q. q: {w. ? X. X : P & w : Rep_preal X}";
by Safe_tac;
by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
@@ -1123,14 +1123,14 @@
qed "preal_sup_mem_Ex";
(** Part 1 of Dedekind def **)
-Goal "!!P. ? (X::preal). X: P ==> \
+Goal "? (X::preal). X: P ==> \
\ {} < {w. ? X : P. w : Rep_preal X}";
by (dtac preal_sup_mem_Ex 1);
by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
qed "preal_sup_set_not_empty";
(** Part 2 of Dedekind sections def **)
-Goalw [preal_less_def] "!!P. ? Y. (! X: P. X < Y) \
+Goalw [preal_less_def] "? Y. (! X: P. X < Y) \
\ ==> ? q. q ~: {w. ? X. X: P & w: Rep_preal(X)}"; (**)
by (auto_tac (claset(),simpset() addsimps [psubset_def]));
by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
@@ -1139,7 +1139,7 @@
by (auto_tac (claset() addSDs [bspec],simpset()));
qed "preal_sup_not_mem_Ex";
-Goalw [preal_le_def] "!!P. ? Y. (! X: P. X <= Y) \
+Goalw [preal_le_def] "? Y. (! X: P. X <= Y) \
\ ==> ? q. q ~: {w. ? X. X: P & w: Rep_preal(X)}";
by (Step_tac 1);
by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
@@ -1148,7 +1148,7 @@
by (auto_tac (claset() addSDs [bspec],simpset()));
qed "preal_sup_not_mem_Ex1";
-Goal "!!P. ? Y. (! X: P. X < Y) \
+Goal "? Y. (! X: P. X < Y) \
\ ==> {w. ? X: P. w: Rep_preal(X)} < {q. True}"; (**)
by (dtac preal_sup_not_mem_Ex 1);
by (auto_tac (claset() addSIs [psubsetI],simpset()));
@@ -1156,7 +1156,7 @@
by Auto_tac;
qed "preal_sup_set_not_prat_set";
-Goal "!!P. ? Y. (! X: P. X <= Y) \
+Goal "? Y. (! X: P. X <= Y) \
\ ==> {w. ? X: P. w: Rep_preal(X)} < {q. True}";
by (dtac preal_sup_not_mem_Ex1 1);
by (auto_tac (claset() addSIs [psubsetI],simpset()));
@@ -1165,31 +1165,31 @@
qed "preal_sup_set_not_prat_set1";
(** Part 3 of Dedekind sections def **)
-Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \
+Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \
\ ==> ! y: {w. ? X: P. w: Rep_preal X}. \
\ !z. z < y --> z: {w. ? X: P. w: Rep_preal X}"; (**)
by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
qed "preal_sup_set_lemma3";
-Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
+Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
\ ==> ! y: {w. ? X: P. w: Rep_preal X}. \
\ !z. z < y --> z: {w. ? X: P. w: Rep_preal X}";
by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
qed "preal_sup_set_lemma3_1";
-Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \
+Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \
\ ==> !y: {w. ? X: P. w: Rep_preal X}. \
\ Bex {w. ? X: P. w: Rep_preal X} (op < y)"; (**)
by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
qed "preal_sup_set_lemma4";
-Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
+Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
\ ==> !y: {w. ? X: P. w: Rep_preal X}. \
\ Bex {w. ? X: P. w: Rep_preal X} (op < y)";
by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
qed "preal_sup_set_lemma4_1";
-Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \
+Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \
\ ==> {w. ? X: P. w: Rep_preal(X)}: preal"; (**)
by (rtac prealI2 1);
by (rtac preal_sup_set_not_empty 1);
@@ -1199,7 +1199,7 @@
by Auto_tac;
qed "preal_sup";
-Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
+Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
\ ==> {w. ? X: P. w: Rep_preal(X)}: preal";
by (rtac prealI2 1);
by (rtac preal_sup_set_not_empty 1);
@@ -1209,27 +1209,27 @@
by Auto_tac;
qed "preal_sup1";
-Goalw [psup_def] "!!P. ? Y. (! X:P. X < Y) ==> ! x: P. x <= psup P"; (**)
+Goalw [psup_def] "? Y. (! X:P. X < Y) ==> ! x: P. x <= psup P"; (**)
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
by (rtac (preal_sup RS Abs_preal_inverse RS ssubst) 1);
by Auto_tac;
qed "preal_psup_leI";
-Goalw [psup_def] "!!P. ? Y. (! X:P. X <= Y) ==> ! x: P. x <= psup P";
+Goalw [psup_def] "? Y. (! X:P. X <= Y) ==> ! x: P. x <= psup P";
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
by (rtac (preal_sup1 RS Abs_preal_inverse RS ssubst) 1);
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
qed "preal_psup_leI2";
-Goal "!!P. [| ? Y. (! X:P. X < Y); x : P |] ==> x <= psup P"; (**)
+Goal "[| ? Y. (! X:P. X < Y); x : P |] ==> x <= psup P"; (**)
by (blast_tac (claset() addSDs [preal_psup_leI]) 1);
qed "preal_psup_leI2b";
-Goal "!!P. [| ? Y. (! X:P. X <= Y); x : P |] ==> x <= psup P";
+Goal "[| ? Y. (! X:P. X <= Y); x : P |] ==> x <= psup P";
by (blast_tac (claset() addSDs [preal_psup_leI2]) 1);
qed "preal_psup_leI2a";
-Goalw [psup_def] "!!P. [| ? X. X : P; ! X:P. X < Y |] ==> psup P <= Y"; (**)
+Goalw [psup_def] "[| ? X. X : P; ! X:P. X < Y |] ==> psup P <= Y"; (**)
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
by (dtac (([exI,exI] MRS preal_sup) RS Abs_preal_inverse RS subst) 1);
by (rotate_tac 1 2);
@@ -1237,7 +1237,7 @@
by (auto_tac (claset() addSDs [bspec],simpset() addsimps [preal_less_def,psubset_def]));
qed "psup_le_ub";
-Goalw [psup_def] "!!P. [| ? X. X : P; ! X:P. X <= Y |] ==> psup P <= Y";
+Goalw [psup_def] "[| ? X. X : P; ! X:P. X <= Y |] ==> psup P <= Y";
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
by (dtac (([exI,exI] MRS preal_sup1) RS Abs_preal_inverse RS subst) 1);
by (rotate_tac 1 2);
@@ -1247,7 +1247,7 @@
qed "psup_le_ub1";
(** supremum property **)
-Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \
+Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \
\ ==> (!Y. (? X: P. Y < X) = (Y < psup P))";
by (forward_tac [preal_sup RS Abs_preal_inverse] 1);
by (Fast_tac 1);
@@ -1267,12 +1267,12 @@
(****** Embedding ******)
(*** mapping from prat into preal ***)
-Goal "!!z1. x < z1 + z2 ==> x * z1 * qinv (z1 + z2) < z1";
+Goal "x < z1 + z2 ==> x * z1 * qinv (z1 + z2) < z1";
by (dres_inst_tac [("x","z1 * qinv (z1 + z2)")] prat_mult_less2_mono1 1);
by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
qed "lemma_preal_rat_less";
-Goal "!!z1. x < z1 + z2 ==> x * z2 * qinv (z1 + z2) < z2";
+Goal "x < z1 + z2 ==> x * z2 * qinv (z1 + z2) < z2";
by (stac prat_add_commute 1);
by (dtac (prat_add_commute RS subst) 1);
by (etac lemma_preal_rat_less 1);
@@ -1291,13 +1291,13 @@
prat_add_mult_distrib2 RS sym] @ prat_mult_ac) 1);
qed "preal_prat_add";
-Goal "!!xa. x < xa ==> x*z1*qinv(xa) < z1";
+Goal "x < xa ==> x*z1*qinv(xa) < z1";
by (dres_inst_tac [("x","z1 * qinv xa")] prat_mult_less2_mono1 1);
by (dtac (prat_mult_left_commute RS subst) 1);
by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
qed "lemma_preal_rat_less3";
-Goal "!!xa. xa < z1 * z2 ==> xa*z2*qinv(z1*z2) < z2";
+Goal "xa < z1 * z2 ==> xa*z2*qinv(z1*z2) < z2";
by (dres_inst_tac [("x","z2 * qinv(z1*z2)")] prat_mult_less2_mono1 1);
by (dtac (prat_mult_left_commute RS subst) 1);
by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
--- a/src/HOL/Real/RComplete.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Real/RComplete.ML Wed Jul 15 10:15:13 1998 +0200
@@ -24,7 +24,7 @@
Completeness theorem for the positive reals(again)
----------------------------------------------------------------*)
-Goal "!!S. [| ALL x: S. 0r < x; \
+Goal "[| ALL x: S. 0r < x; \
\ EX x. x: S; \
\ EX u. isUb (UNIV::real set) S u \
\ |] ==> EX t. isLub (UNIV::real set) S t";
@@ -85,7 +85,7 @@
by (auto_tac (claset(),simpset() addsimps [real_add_commute]));
qed "lemma_le_swap2";
-Goal "!!x. [| 0r < x + %~X + 1r; x < xa |] ==> 0r < xa + %~X + 1r";
+Goal "[| 0r < x + %~X + 1r; x < xa |] ==> 0r < xa + %~X + 1r";
by (dtac real_add_less_mono 1);
by (assume_tac 1);
by (dres_inst_tac [("C","%~x"),("A","0r + x")] real_add_less_mono2 1);
@@ -104,13 +104,13 @@
real_add_minus_left,real_add_zero_left]) 1);
qed "lemma_real_complete2";
-Goal "!!x. [| x + %~X + 1r <= S; xa < x |] ==> xa <= S + X + %~1r"; (**)
+Goal "[| x + %~X + 1r <= S; xa < x |] ==> xa <= S + X + %~1r"; (**)
by (rtac (lemma_le_swap2 RS iffD2) 1);
by (etac lemma_real_complete2 1);
by (assume_tac 1);
qed "lemma_real_complete2a";
-Goal "!!x. [| x + %~X + 1r <= S; xa <= x |] ==> xa <= S + X + %~1r";
+Goal "[| x + %~X + 1r <= S; xa <= x |] ==> xa <= S + X + %~1r";
by (rotate_tac 1 1);
by (etac (real_le_imp_less_or_eq RS disjE) 1);
by (blast_tac (claset() addIs [lemma_real_complete2a]) 1);
@@ -173,7 +173,7 @@
real_add_minus,real_add_minus_left,real_add_zero_right]));
qed "lemma_arch";
-Goal "!!x. 0r < x ==> EX n. rinv(%%#n) < x";
+Goal "0r < x ==> EX n. rinv(%%#n) < x";
by (stac real_nat_rinv_Ex_iff 1);
by (EVERY1[rtac ccontr, Asm_full_simp_tac]);
by (fold_tac [real_le_def]);
--- a/src/HOL/Real/Real.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Real/Real.ML Wed Jul 15 10:15:13 1998 +0200
@@ -239,7 +239,7 @@
real_add_zero_right,real_add_zero_left]) 1);
qed "real_minus_left_ex1";
-Goal "!!y. x + y = 0r ==> x = %~y";
+Goal "x + y = 0r ==> x = %~y";
by (cut_inst_tac [("z","y")] real_add_minus_left 1);
by (res_inst_tac [("x1","y")] (real_minus_left_ex1 RS ex1E) 1);
by (Blast_tac 1);
@@ -451,19 +451,19 @@
simpset() addsimps [real_mult_inv_left]));
qed "real_mult_inv_right";
-Goal "!!a. (c::real) ~= 0r ==> (c*a=c*b) = (a=b)";
+Goal "(c::real) ~= 0r ==> (c*a=c*b) = (a=b)";
by Auto_tac;
by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac) 1);
qed "real_mult_left_cancel";
-Goal "!!a. (c::real) ~= 0r ==> (a*c=b*c) = (a=b)";
+Goal "(c::real) ~= 0r ==> (a*c=b*c) = (a=b)";
by (Step_tac 1);
by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac) 1);
qed "real_mult_right_cancel";
-Goalw [rinv_def] "!!x. x ~= 0r ==> rinv(x) ~= 0r";
+Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r";
by (forward_tac [real_mult_inv_left_ex] 1);
by (etac exE 1);
by (rtac selectI2 1);
@@ -473,7 +473,7 @@
Addsimps [real_mult_inv_left,real_mult_inv_right];
-Goal "!!x. x ~= 0r ==> rinv(rinv x) = x";
+Goal "x ~= 0r ==> rinv(rinv x) = x";
by (res_inst_tac [("c1","rinv x")] (real_mult_right_cancel RS iffD1) 1);
by (etac rinv_not_zero 1);
by (auto_tac (claset() addDs [rinv_not_zero],simpset()));
@@ -488,7 +488,7 @@
[real_zero_not_eq_one RS not_sym]));
qed "real_rinv_1";
-Goal "!!x. x ~= 0r ==> rinv(%~x) = %~rinv(x)";
+Goal "x ~= 0r ==> rinv(%~x) = %~rinv(x)";
by (res_inst_tac [("c1","%~x")] (real_mult_right_cancel RS iffD1) 1);
by Auto_tac;
qed "real_minus_rinv";
@@ -637,19 +637,19 @@
qed "real_preal_trichotomy";
Goal "!!x. [| !!m. x = %#m ==> P; \
-\ x = 0r ==> P; \
-\ !!m. x = %~(%#m) ==> P |] ==> P";
+\ x = 0r ==> P; \
+\ !!m. x = %~(%#m) ==> P |] ==> P";
by (cut_inst_tac [("x","x")] real_preal_trichotomy 1);
by Auto_tac;
qed "real_preal_trichotomyE";
-Goalw [real_preal_def] "!!m1 m2. %#m1 < %#m2 ==> m1 < m2";
+Goalw [real_preal_def] "%#m1 < %#m2 ==> m1 < m2";
by (auto_tac (claset(),simpset() addsimps [real_less_def] @ preal_add_ac));
by (auto_tac (claset(),simpset() addsimps [preal_add_assoc RS sym]));
by (auto_tac (claset(),simpset() addsimps preal_add_ac));
qed "real_preal_lessD";
-Goal "!!m1 m2. m1 < m2 ==> %#m1 < %#m2";
+Goal "m1 < m2 ==> %#m1 < %#m2";
by (dtac preal_less_add_left_Ex 1);
by (auto_tac (claset(),simpset() addsimps [real_preal_add,
real_preal_def,real_less_def]));
@@ -743,7 +743,7 @@
addEs [real_less_irrefl]) 1);
qed "real_preal_not_minus_gt_all";
-Goal "!!m1 m2. %~ %#m1 < %~ %#m2 ==> %#m2 < %#m1";
+Goal "%~ %#m1 < %~ %#m2 ==> %#m2 < %#m1";
by (auto_tac (claset(),simpset() addsimps
[real_preal_def,real_less_def,real_minus]));
by (REPEAT(rtac exI 1));
@@ -754,7 +754,7 @@
by (auto_tac (claset(),simpset() addsimps preal_add_ac));
qed "real_preal_minus_less_rev1";
-Goal "!!m1 m2. %#m1 < %#m2 ==> %~ %#m2 < %~ %#m1";
+Goal "%#m1 < %#m2 ==> %~ %#m2 < %~ %#m1";
by (auto_tac (claset(),simpset() addsimps
[real_preal_def,real_less_def,real_minus]));
by (REPEAT(rtac exI 1));
@@ -790,25 +790,25 @@
(*** Properties of <= ***)
-Goalw [real_le_def] "!!w. ~(w < z) ==> z <= (w::real)";
+Goalw [real_le_def] "~(w < z) ==> z <= (w::real)";
by (assume_tac 1);
qed "real_leI";
-Goalw [real_le_def] "!!w. z<=w ==> ~(w<(z::real))";
+Goalw [real_le_def] "z<=w ==> ~(w<(z::real))";
by (assume_tac 1);
qed "real_leD";
val real_leE = make_elim real_leD;
-Goal "!!w. (~(w < z)) = (z <= (w::real))";
+Goal "(~(w < z)) = (z <= (w::real))";
by (fast_tac (claset() addSIs [real_leI,real_leD]) 1);
qed "real_less_le_iff";
-Goalw [real_le_def] "!!z. ~ z <= w ==> w<(z::real)";
+Goalw [real_le_def] "~ z <= w ==> w<(z::real)";
by (Fast_tac 1);
qed "not_real_leE";
-Goalw [real_le_def] "!!z. z < w ==> z <= (w::real)";
+Goalw [real_le_def] "z < w ==> z <= (w::real)";
by (fast_tac (claset() addEs [real_less_asym]) 1);
qed "real_less_imp_le";
@@ -817,7 +817,7 @@
by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
qed "real_le_imp_less_or_eq";
-Goalw [real_le_def] "!!z. z<w | z=w ==> z <=(w::real)";
+Goalw [real_le_def] "z<w | z=w ==> z <=(w::real)";
by (cut_facts_tac [real_linear] 1);
by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
qed "real_less_or_eq_imp_le";
@@ -840,17 +840,17 @@
by (fast_tac (claset() addIs [real_less_trans]) 1);
qed "real_less_le_trans";
-Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::real)";
+Goal "[| i <= j; j <= k |] ==> i <= (k::real)";
by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
rtac real_less_or_eq_imp_le, fast_tac (claset() addIs [real_less_trans])]);
qed "real_le_trans";
-Goal "!!z. [| z <= w; w <= z |] ==> z = (w::real)";
+Goal "[| z <= w; w <= z |] ==> z = (w::real)";
by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
fast_tac (claset() addEs [real_less_irrefl,real_less_asym])]);
qed "real_le_anti_sym";
-Goal "!!x. [| ~ y < x; y ~= x |] ==> x < (y::real)";
+Goal "[| ~ y < x; y ~= x |] ==> x < (y::real)";
by (rtac not_real_leE 1);
by (fast_tac (claset() addDs [real_le_imp_less_or_eq]) 1);
qed "not_less_not_eq_real_less";
@@ -879,23 +879,23 @@
real_preal_not_minus_gt_zero RS notE]) 1);
qed "real_gt_zero_preal_Ex";
-Goal "!!x. %#z < x ==> ? y. x = %#y";
+Goal "%#z < x ==> ? y. x = %#y";
by (blast_tac (claset() addSDs [real_preal_zero_less RS real_less_trans]
addIs [real_gt_zero_preal_Ex RS iffD1]) 1);
qed "real_gt_preal_preal_Ex";
-Goal "!!x. %#z <= x ==> ? y. x = %#y";
+Goal "%#z <= x ==> ? y. x = %#y";
by (blast_tac (claset() addDs [real_le_imp_less_or_eq,
real_gt_preal_preal_Ex]) 1);
qed "real_ge_preal_preal_Ex";
-Goal "!!y. y <= 0r ==> !x. y < %#x";
+Goal "y <= 0r ==> !x. y < %#x";
by (auto_tac (claset() addEs [real_le_imp_less_or_eq RS disjE]
addIs [real_preal_zero_less RSN(2,real_less_trans)],
simpset() addsimps [real_preal_zero_less]));
qed "real_less_all_preal";
-Goal "!!y. ~ 0r < y ==> !x. y < %#x";
+Goal "~ 0r < y ==> !x. y < %#x";
by (blast_tac (claset() addSIs [real_less_all_preal,real_leI]) 1);
qed "real_less_all_real2";
@@ -937,19 +937,19 @@
(* lemmas *)
(** change naff name(s)! **)
-Goal "!!S. (W < S) ==> (0r < S + %~W)";
+Goal "(W < S) ==> (0r < S + %~W)";
by (dtac real_less_add_positive_left_Ex 1);
by (auto_tac (claset(),simpset() addsimps [real_add_minus,
real_add_zero_right] @ real_add_ac));
qed "real_less_sum_gt_zero";
Goal "!!S. T = S + W ==> S = T + %~W";
-by (asm_simp_tac (simpset() addsimps [real_add_minus,
- real_add_zero_right] @ real_add_ac) 1);
+by (asm_simp_tac (simpset() addsimps [real_add_minus, real_add_zero_right]
+ @ real_add_ac) 1);
qed "real_lemma_change_eq_subj";
(* FIXME: long! *)
-Goal "!!W. (0r < S + %~W) ==> (W < S)";
+Goal "(0r < S + %~W) ==> (W < S)";
by (rtac ccontr 1);
by (dtac (real_leI RS real_le_imp_less_or_eq) 1);
by (auto_tac (claset(),
@@ -976,7 +976,7 @@
by (simp_tac (simpset() addsimps [real_add_commute]) 1);
qed "real_less_swap_iff";
-Goal "!!T. [| R + L = S; 0r < L |] ==> R < S";
+Goal "[| R + L = S; 0r < L |] ==> R < S";
by (rtac (real_less_sum_gt_0_iff RS iffD1) 1);
by (auto_tac (claset(),simpset() addsimps [
real_add_minus,real_add_zero_right] @ real_add_ac));
@@ -1075,11 +1075,11 @@
(*** Completeness of reals ***)
(** use supremum property of preal and theorems about real_preal **)
(*** a few lemmas ***)
-Goal "!!P y. ! x:P. 0r < x ==> ((? x:P. y < x) = (? X. %#X : P & y < %#X))";
+Goal "! x:P. 0r < x ==> ((? x:P. y < x) = (? X. %#X : P & y < %#X))";
by (blast_tac (claset() addSDs [bspec,real_gt_zero_preal_Ex RS iffD1]) 1);
qed "real_sup_lemma1";
-Goal "!!P. [| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
+Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
\ ==> (? X. X: {w. %#w : P}) & (? Y. !X: {w. %#w : P}. X < Y)";
by (rtac conjI 1);
by (blast_tac (claset() addDs [bspec,real_gt_zero_preal_Ex RS iffD1]) 1);
@@ -1101,7 +1101,7 @@
(* Supremum property for the set of positive reals *)
(* FIXME: long proof - can be improved - need only have one case split *)
(* will do for now *)
-Goal "!!P. [| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
+Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
\ ==> (? S. !y. (? x: P. y < x) = (y < S))";
by (res_inst_tac [("x","%#psup({w. %#w : P})")] exI 1);
by Auto_tac;
@@ -1156,7 +1156,7 @@
real_add_minus_left,real_add_zero_left]) 1);
qed "real_less_add_left_cancel";
-Goal "!!x. [| 0r < x; 0r < y |] ==> 0r < x + y";
+Goal "[| 0r < x; 0r < y |] ==> 0r < x + y";
by (REPEAT(dtac (real_gt_zero_preal_Ex RS iffD1) 1));
by (rtac (real_gt_zero_preal_Ex RS iffD2) 1);
by (Step_tac 1);
@@ -1267,7 +1267,7 @@
by (Blast_tac 1);
qed "real_nat_less_zero";
-Goal "!!n. 1r <= %%#n";
+Goal "1r <= %%#n";
by (simp_tac (simpset() addsimps [real_nat_one RS sym]) 1);
by (nat_ind_tac "n" 1);
by (auto_tac (claset(),simpset ()
@@ -1284,7 +1284,7 @@
real_not_refl2 RS not_sym) RS rinv_not_zero) 1);
qed "real_nat_rinv_not_zero";
-Goal "!!x. rinv(%%#x) = rinv(%%#y) ==> x = y";
+Goal "rinv(%%#x) = rinv(%%#y) ==> x = y";
by (rtac (inj_real_nat RS injD) 1);
by (res_inst_tac [("n2","x")]
(real_nat_rinv_not_zero RS real_mult_left_cancel RS iffD1) 1);
@@ -1294,7 +1294,7 @@
real_not_refl2 RS not_sym)]) 1);
qed "real_nat_rinv_inj";
-Goal "!!x. 0r < x ==> 0r < rinv x";
+Goal "0r < x ==> 0r < rinv x";
by (EVERY1[rtac ccontr, dtac real_leI]);
by (forward_tac [real_minus_zero_less_iff2 RS iffD2] 1);
by (forward_tac [real_not_refl2 RS not_sym] 1);
@@ -1305,7 +1305,7 @@
simpset() addsimps [real_minus_mult_eq1 RS sym]));
qed "real_rinv_gt_zero";
-Goal "!!x. x < 0r ==> rinv x < 0r";
+Goal "x < 0r ==> rinv x < 0r";
by (forward_tac [real_not_refl2] 1);
by (dtac (real_minus_zero_less_iff RS iffD2) 1);
by (rtac (real_minus_zero_less_iff RS iffD1) 1);
@@ -1370,12 +1370,12 @@
by (asm_full_simp_tac (simpset() addsimps [real_mult_commute]) 1);
qed "real_mult_less_cancel2";
-Goal "!!z. 0r < z ==> (x*z < y*z) = (x < y)";
+Goal "0r < z ==> (x*z < y*z) = (x < y)";
by (blast_tac (claset() addIs [real_mult_less_mono1,
real_mult_less_cancel1]) 1);
qed "real_mult_less_iff1";
-Goal "!!z. 0r < z ==> (z*x < z*y) = (x < y)";
+Goal "0r < z ==> (z*x < z*y) = (x < y)";
by (blast_tac (claset() addIs [real_mult_less_mono2,
real_mult_less_cancel2]) 1);
qed "real_mult_less_iff2";
@@ -1432,7 +1432,7 @@
Addsimps [real_nat_less_iff];
-Goal "!!u. 0r < u ==> (u < rinv (%%#n)) = (%%#n < rinv(u))";
+Goal "0r < u ==> (u < rinv (%%#n)) = (%%#n < rinv(u))";
by (Step_tac 1);
by (res_inst_tac [("n2","n")] (real_nat_less_zero RS
real_rinv_gt_zero RS real_mult_less_cancel1) 1);
@@ -1447,7 +1447,7 @@
real_not_refl2 RS not_sym,real_mult_assoc RS sym]));
qed "real_nat_less_rinv_iff";
-Goal "!!x. 0r < u ==> (u = rinv(%%#n)) = (%%#n = rinv u)";
+Goal "0r < u ==> (u = rinv(%%#n)) = (%%#n = rinv u)";
by (auto_tac (claset(),simpset() addsimps [real_rinv_rinv,
real_nat_less_zero,real_not_refl2 RS not_sym]));
qed "real_nat_rinv_eq_iff";
--- a/src/HOL/Real/RealAbs.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Real/RealAbs.ML Wed Jul 15 10:15:13 1998 +0200
@@ -37,7 +37,7 @@
by (simp_tac (simpset() addsimps [prem,if_not_P]) 1);
qed "rabs_minus_eqI2";
-Goal "!!x. x<=0r ==> rabs x = %~x";
+Goal "x<=0r ==> rabs x = %~x";
by (dtac real_le_imp_less_or_eq 1);
by (fast_tac (HOL_cs addIs [rabs_minus_zero,rabs_minus_eqI2]) 1);
qed "rabs_minus_eqI1";
@@ -86,7 +86,7 @@
simpset() addsimps [real_minus_mult_eq2 RS sym] @real_mult_ac));
qed "rabs_mult";
-Goalw [rabs_def] "!!x. x~= 0r ==> rabs(rinv(x)) = rinv(rabs(x))";
+Goalw [rabs_def] "x~= 0r ==> rabs(rinv(x)) = rinv(rabs(x))";
by (auto_tac (claset(),simpset() addsimps [real_minus_rinv]
setloop (split_tac [expand_if])));
by (ALLGOALS(dtac not_real_leE));
@@ -142,7 +142,7 @@
by (REPEAT (ares_tac [real_add_less_mono] 1));
qed "rabs_add_less";
-Goal "!!x y. [| rabs x < r; rabs y < s |] ==> rabs(x+ %~y) < r+s";
+Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+ %~y) < r+s";
by (rotate_tac 1 1);
by (dtac (rabs_minus_cancel RS ssubst) 1);
by (asm_simp_tac (simpset() addsimps [rabs_add_less]) 1);
@@ -175,13 +175,13 @@
real_le_less_trans]) 1);
qed "rabs_mult_less";
-Goal "!!x. [| rabs x < r; rabs y < s |] \
+Goal "[| rabs x < r; rabs y < s |] \
\ ==> rabs(x)*rabs(y)<r*s";
by (auto_tac (claset() addIs [rabs_mult_less],
simpset() addsimps [rabs_mult RS sym]));
qed "rabs_mult_less2";
-Goal "!! x y r. 1r < rabs x ==> rabs y <= rabs(x*y)";
+Goal "1r < rabs x ==> rabs y <= rabs(x*y)";
by (cut_inst_tac [("x1","y")] (rabs_ge_zero RS real_le_imp_less_or_eq) 1);
by (EVERY1[etac disjE,rtac real_less_imp_le]);
by (dres_inst_tac [("W","1r")] real_less_sum_gt_zero 1);
@@ -194,11 +194,11 @@
by (asm_full_simp_tac (simpset() addsimps [real_le_refl,rabs_mult]) 1);
qed "rabs_mult_le";
-Goal "!!x. [| 1r < rabs x; r < rabs y|] ==> r < rabs(x*y)";
+Goal "[| 1r < rabs x; r < rabs y|] ==> r < rabs(x*y)";
by (fast_tac (HOL_cs addIs [rabs_mult_le, real_less_le_trans]) 1);
qed "rabs_mult_gt";
-Goal "!!r. rabs(x)<r ==> 0r<r";
+Goal "rabs(x)<r ==> 0r<r";
by (blast_tac (claset() addSIs [real_le_less_trans,rabs_ge_zero]) 1);
qed "rabs_less_gt_zero";
@@ -217,7 +217,7 @@
rabs_zero,rabs_minus_zero]) 1);
qed "rabs_disj";
-Goal "!!x. rabs x = y ==> x = y | %~x = y";
+Goal "rabs x = y ==> x = y | %~x = y";
by (dtac sym 1);
by (hyp_subst_tac 1);
by (res_inst_tac [("x1","x")] (rabs_disj RS disjE) 1);
--- a/src/HOL/RelPow.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/RelPow.ML Wed Jul 15 10:15:13 1998 +0200
@@ -15,7 +15,7 @@
by (Simp_tac 1);
qed "rel_pow_0_I";
-Goal "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
+Goal "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
by (Simp_tac 1);
by (Blast_tac 1);
qed "rel_pow_Suc_I";
--- a/src/HOL/Relation.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Relation.ML Wed Jul 15 10:15:13 1998 +0200
@@ -68,7 +68,7 @@
by (Blast_tac 1);
qed "O_assoc";
-Goal "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
+Goal "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
by (Blast_tac 1);
qed "comp_mono";
@@ -91,17 +91,17 @@
(** Natural deduction for r^-1 **)
-Goalw [converse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
+Goalw [converse_def] "((a,b): r^-1) = ((b,a):r)";
by (Simp_tac 1);
qed "converse_iff";
AddIffs [converse_iff];
-Goalw [converse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
+Goalw [converse_def] "(a,b):r ==> (b,a): r^-1";
by (Simp_tac 1);
qed "converseI";
-Goalw [converse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
+Goalw [converse_def] "(a,b) : r^-1 ==> (b,a) : r";
by (Blast_tac 1);
qed "converseD";
--- a/src/HOL/Set.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Set.ML Wed Jul 15 10:15:13 1998 +0200
@@ -13,7 +13,7 @@
Addsimps [Collect_mem_eq];
AddIffs [mem_Collect_eq];
-Goal "!!a. P(a) ==> a : {x. P(x)}";
+Goal "P(a) ==> a : {x. P(x)}";
by (Asm_simp_tac 1);
qed "CollectI";
@@ -325,11 +325,11 @@
Addsimps [Un_iff];
-Goal "!!c. c:A ==> c : A Un B";
+Goal "c:A ==> c : A Un B";
by (Asm_simp_tac 1);
qed "UnI1";
-Goal "!!c. c:B ==> c : A Un B";
+Goal "c:B ==> c : A Un B";
by (Asm_simp_tac 1);
qed "UnI2";
@@ -356,15 +356,15 @@
Addsimps [Int_iff];
-Goal "!!c. [| c:A; c:B |] ==> c : A Int B";
+Goal "[| c:A; c:B |] ==> c : A Int B";
by (Asm_simp_tac 1);
qed "IntI";
-Goal "!!c. c : A Int B ==> c:A";
+Goal "c : A Int B ==> c:A";
by (Asm_full_simp_tac 1);
qed "IntD1";
-Goal "!!c. c : A Int B ==> c:B";
+Goal "c : A Int B ==> c:B";
by (Asm_full_simp_tac 1);
qed "IntD2";
@@ -436,7 +436,7 @@
qed_goal "singletonI" Set.thy "a : {a}"
(fn _=> [ (rtac insertI1 1) ]);
-Goal "!!a. b : {a} ==> b=a";
+Goal "b : {a} ==> b=a";
by (Blast_tac 1);
qed "singletonD";
@@ -445,7 +445,7 @@
qed_goal "singleton_iff" thy "(b : {a}) = (b=a)"
(fn _ => [Blast_tac 1]);
-Goal "!!a b. {a}={b} ==> a=b";
+Goal "{a}={b} ==> a=b";
by (blast_tac (claset() addEs [equalityE]) 1);
qed "singleton_inject";
@@ -469,7 +469,7 @@
Addsimps [UN_iff];
(*The order of the premises presupposes that A is rigid; b may be flexible*)
-Goal "!!b. [| a:A; b: B(a) |] ==> b: (UN x:A. B(x))";
+Goal "[| a:A; b: B(a) |] ==> b: (UN x:A. B(x))";
by Auto_tac;
qed "UN_I";
@@ -504,7 +504,7 @@
by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1));
qed "INT_I";
-Goal "!!b. [| b : (INT x:A. B(x)); a:A |] ==> b: B(a)";
+Goal "[| b : (INT x:A. B(x)); a:A |] ==> b: B(a)";
by Auto_tac;
qed "INT_D";
@@ -536,7 +536,7 @@
Addsimps [Union_iff];
(*The order of the premises presupposes that C is rigid; A may be flexible*)
-Goal "!!X. [| X:C; A:X |] ==> A : Union(C)";
+Goal "[| X:C; A:X |] ==> A : Union(C)";
by Auto_tac;
qed "UnionI";
@@ -565,7 +565,7 @@
(*A "destruct" rule -- every X in C contains A as an element, but
A:X can hold when X:C does not! This rule is analogous to "spec". *)
-Goal "!!X. [| A : Inter(C); X:C |] ==> A:X";
+Goal "[| A : Inter(C); X:C |] ==> A:X";
by Auto_tac;
qed "InterD";
@@ -626,7 +626,7 @@
(*** Range of a function -- just a translation for image! ***)
-Goal "!!b. b=f(x) ==> b : range(f)";
+Goal "b=f(x) ==> b : range(f)";
by (EVERY1 [etac image_eqI, rtac UNIV_I]);
bind_thm ("range_eqI", UNIV_I RSN (2,image_eqI));
--- a/src/HOL/Sexp.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Sexp.ML Wed Jul 15 10:15:13 1998 +0200
@@ -124,7 +124,7 @@
by (rtac sexp_case_Numb 1);
qed "sexp_rec_Numb";
-Goal "!!M. [| M: sexp; N: sexp |] ==> \
+Goal "[| M: sexp; N: sexp |] ==> \
\ sexp_rec (M$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
by (rtac (sexp_rec_unfold RS trans) 1);
by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
--- a/src/HOL/Sum.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Sum.ML Wed Jul 15 10:15:13 1998 +0200
@@ -91,11 +91,11 @@
(** Introduction rules for the injections **)
-Goalw [sum_def] "!!a A B. a : A ==> Inl(a) : A Plus B";
+Goalw [sum_def] "a : A ==> Inl(a) : A Plus B";
by (Blast_tac 1);
qed "InlI";
-Goalw [sum_def] "!!b A B. b : B ==> Inr(b) : A Plus B";
+Goalw [sum_def] "b : B ==> Inr(b) : A Plus B";
by (Blast_tac 1);
qed "InrI";
@@ -189,13 +189,13 @@
by (rtac Int_lower1 1);
qed "Part_subset";
-Goal "!!A B. A<=B ==> Part A h <= Part B h";
+Goal "A<=B ==> Part A h <= Part B h";
by (Blast_tac 1);
qed "Part_mono";
val basic_monos = basic_monos @ [Part_mono];
-Goalw [Part_def] "!!a. a : Part A h ==> a : A";
+Goalw [Part_def] "a : Part A h ==> a : A";
by (etac IntD1 1);
qed "PartD1";
--- a/src/HOL/TLA/hypsubst.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/TLA/hypsubst.ML Wed Jul 15 10:15:13 1998 +0200
@@ -17,10 +17,10 @@
Test data:
-Goal "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
-Goal "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
-Goal "!!y. [| ?x=y; P(?x) |] ==> y = a";
-Goal "!!z. [| ?x=y; P(?x) |] ==> y = a";
+Goal "[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
+Goal "[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
+Goal "[| ?x=y; P(?x) |] ==> y = a";
+Goal "[| ?x=y; P(?x) |] ==> y = a";
by (hyp_subst_tac 1);
by (bound_hyp_subst_tac 1);
--- a/src/HOL/Trancl.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Trancl.ML Wed Jul 15 10:15:13 1998 +0200
@@ -28,7 +28,7 @@
(*Closure under composition with r*)
-Goal "!!r. [| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^*";
+Goal "[| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^*";
by (stac rtrancl_unfold 1);
by (Blast_tac 1);
qed "rtrancl_into_rtrancl";
@@ -40,7 +40,7 @@
qed "r_into_rtrancl";
(*monotonicity of rtrancl*)
-Goalw [rtrancl_def] "!!r s. r <= s ==> r^* <= s^*";
+Goalw [rtrancl_def] "r <= s ==> r^* <= s^*";
by (REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1));
qed "rtrancl_mono";
@@ -120,19 +120,19 @@
qed "rtrancl_idemp_self_comp";
Addsimps [rtrancl_idemp_self_comp];
-Goal "!!r s. r <= s^* ==> r^* <= s^*";
+Goal "r <= s^* ==> r^* <= s^*";
by (dtac rtrancl_mono 1);
by (Asm_full_simp_tac 1);
qed "rtrancl_subset_rtrancl";
-Goal "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*";
+Goal "[| R <= S; S <= R^* |] ==> S^* = R^*";
by (dtac rtrancl_mono 1);
by (dtac rtrancl_mono 1);
by (Asm_full_simp_tac 1);
by (Blast_tac 1);
qed "rtrancl_subset";
-Goal "!!R. (R^* Un S^*)^* = (R Un S)^*";
+Goal "(R^* Un S^*)^* = (R Un S)^*";
by (blast_tac (claset() addSIs [rtrancl_subset]
addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
qed "rtrancl_Un_rtrancl";
@@ -143,14 +143,14 @@
qed "rtrancl_reflcl";
Addsimps [rtrancl_reflcl];
-Goal "!!r. (x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1";
+Goal "(x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1";
by (rtac converseI 1);
by (etac rtrancl_induct 1);
by (rtac rtrancl_refl 1);
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
qed "rtrancl_converseD";
-Goal "!!r. (x,y) : (r^*)^-1 ==> (x,y) : (r^-1)^*";
+Goal "(x,y) : (r^*)^-1 ==> (x,y) : (r^-1)^*";
by (dtac converseD 1);
by (etac rtrancl_induct 1);
by (rtac rtrancl_refl 1);
@@ -204,7 +204,7 @@
(**** The relation trancl ****)
-Goalw [trancl_def] "!!p.[| p:r^+; r <= s |] ==> p:s^+";
+Goalw [trancl_def] "[| p:r^+; r <= s |] ==> p:s^+";
by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1);
qed "trancl_mono";
--- a/src/HOL/Univ.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Univ.ML Wed Jul 15 10:15:13 1998 +0200
@@ -142,11 +142,11 @@
(** Injectiveness of Scons **)
-Goalw [Scons_def] "!!M. M$N <= M'$N' ==> M<=M'";
+Goalw [Scons_def] "M$N <= M'$N' ==> M<=M'";
by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
qed "Scons_inject_lemma1";
-Goalw [Scons_def] "!!M. M$N <= M'$N' ==> N<=N'";
+Goalw [Scons_def] "M$N <= M'$N' ==> N<=N'";
by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
qed "Scons_inject_lemma2";
@@ -297,7 +297,7 @@
(*** Cartesian Product ***)
-Goalw [uprod_def] "!!M N. [| M:A; N:B |] ==> (M$N) : A<*>B";
+Goalw [uprod_def] "[| M:A; N:B |] ==> (M$N) : A<*>B";
by (REPEAT (ares_tac [singletonI,UN_I] 1));
qed "uprodI";
@@ -322,11 +322,11 @@
(*** Disjoint Sum ***)
-Goalw [usum_def] "!!M. M:A ==> In0(M) : A<+>B";
+Goalw [usum_def] "M:A ==> In0(M) : A<+>B";
by (Blast_tac 1);
qed "usum_In0I";
-Goalw [usum_def] "!!N. N:B ==> In1(N) : A<+>B";
+Goalw [usum_def] "N:B ==> In1(N) : A<+>B";
by (Blast_tac 1);
qed "usum_In1I";
@@ -408,23 +408,23 @@
(*** Monotonicity ***)
-Goalw [uprod_def] "!!A B. [| A<=A'; B<=B' |] ==> A<*>B <= A'<*>B'";
+Goalw [uprod_def] "[| A<=A'; B<=B' |] ==> A<*>B <= A'<*>B'";
by (Blast_tac 1);
qed "uprod_mono";
-Goalw [usum_def] "!!A B. [| A<=A'; B<=B' |] ==> A<+>B <= A'<+>B'";
+Goalw [usum_def] "[| A<=A'; B<=B' |] ==> A<+>B <= A'<+>B'";
by (Blast_tac 1);
qed "usum_mono";
-Goalw [Scons_def] "!!M N. [| M<=M'; N<=N' |] ==> M$N <= M'$N'";
+Goalw [Scons_def] "[| M<=M'; N<=N' |] ==> M$N <= M'$N'";
by (Blast_tac 1);
qed "Scons_mono";
-Goalw [In0_def] "!!M N. M<=N ==> In0(M) <= In0(N)";
+Goalw [In0_def] "M<=N ==> In0(M) <= In0(N)";
by (REPEAT (ares_tac [subset_refl,Scons_mono] 1));
qed "In0_mono";
-Goalw [In1_def] "!!M N. M<=N ==> In1(M) <= In1(N)";
+Goalw [In1_def] "M<=N ==> In1(M) <= In1(N)";
by (REPEAT (ares_tac [subset_refl,Scons_mono] 1));
qed "In1_mono";
@@ -471,7 +471,7 @@
(*** Equality : the diagonal relation ***)
-Goalw [diag_def] "!!a A. [| a=b; a:A |] ==> (a,b) : diag(A)";
+Goalw [diag_def] "[| a=b; a:A |] ==> (a,b) : diag(A)";
by (Blast_tac 1);
qed "diag_eqI";
@@ -506,11 +506,11 @@
(*** Equality for Disjoint Sum ***)
-Goalw [dsum_def] "!!r. (M,M'):r ==> (In0(M), In0(M')) : r<++>s";
+Goalw [dsum_def] "(M,M'):r ==> (In0(M), In0(M')) : r<++>s";
by (Blast_tac 1);
qed "dsum_In0I";
-Goalw [dsum_def] "!!r. (N,N'):s ==> (In1(N), In1(N')) : r<++>s";
+Goalw [dsum_def] "(N,N'):s ==> (In1(N), In1(N')) : r<++>s";
by (Blast_tac 1);
qed "dsum_In1I";
@@ -531,11 +531,11 @@
(*** Monotonicity ***)
-Goal "!!r s. [| r<=r'; s<=s' |] ==> r<**>s <= r'<**>s'";
+Goal "[| r<=r'; s<=s' |] ==> r<**>s <= r'<**>s'";
by (Blast_tac 1);
qed "dprod_mono";
-Goal "!!r s. [| r<=r'; s<=s' |] ==> r<++>s <= r'<++>s'";
+Goal "[| r<=r'; s<=s' |] ==> r<++>s <= r'<++>s'";
by (Blast_tac 1);
qed "dsum_mono";
--- a/src/HOL/Vimage.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Vimage.ML Wed Jul 15 10:15:13 1998 +0200
@@ -102,6 +102,6 @@
(** monotonicity **)
-Goal "!!f. A<=B ==> f-``A <= f-``B";
+Goal "A<=B ==> f-``A <= f-``B";
by (Blast_tac 1);
qed "vimage_mono";
--- a/src/HOL/W0/MiniML.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/W0/MiniML.ML Wed Jul 15 10:15:13 1998 +0200
@@ -11,7 +11,7 @@
(* has_type is closed w.r.t. substitution *)
-Goal "!!a e t. a |- e :: t ==> $s a |- e :: $s t";
+Goal "a |- e :: t ==> $s a |- e :: $s t";
by (etac has_type.induct 1);
(* case VarI *)
by (asm_full_simp_tac (simpset() addsimps [app_subst_list]) 1);
--- a/src/HOL/WF.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/WF.ML Wed Jul 15 10:15:13 1998 +0200
@@ -93,7 +93,7 @@
* Wellfoundedness of subsets
*---------------------------------------------------------------------------*)
-Goal "!!r. [| wf(r); p<=r |] ==> wf(p)";
+Goal "[| wf(r); p<=r |] ==> wf(p)";
by (full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
by (Fast_tac 1);
qed "wf_subset";
@@ -164,7 +164,7 @@
by (simp_tac (HOL_ss addsimps [expand_fun_eq]) 1);
qed "cuts_eq";
-Goalw [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
+Goalw [cut_def] "(x,a):r ==> (cut f r a)(x) = f(x)";
by (asm_simp_tac HOL_ss 1);
qed "cut_apply";
--- a/src/HOL/WF_Rel.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/WF_Rel.ML Wed Jul 15 10:15:13 1998 +0200
@@ -32,7 +32,7 @@
* The inverse image into a wellfounded relation is wellfounded.
*---------------------------------------------------------------------------*)
-Goal "!!r. wf(r) ==> wf(inv_image r (f::'a=>'b))";
+Goal "wf(r) ==> wf(inv_image r (f::'a=>'b))";
by (full_simp_tac (simpset() addsimps [inv_image_def, wf_eq_minimal]) 1);
by (Clarify_tac 1);
by (subgoal_tac "? (w::'b). w : {w. ? (x::'a). x: Q & (f x = w)}" 1);
@@ -110,7 +110,7 @@
* Cannot go into WF because it needs Finite
*---------------------------------------------------------------------------*)
-Goal "!!r. finite r ==> acyclic r --> wf r";
+Goal "finite r ==> acyclic r --> wf r";
by (etac finite_induct 1);
by (Blast_tac 1);
by (split_all_tac 1);
@@ -122,7 +122,7 @@
etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1,
etac (acyclic_converse RS iffD2) 1]);
-Goal "!!r. finite r ==> wf r = acyclic r";
+Goal "finite r ==> wf r = acyclic r";
by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
qed "wf_iff_acyclic_if_finite";
--- a/src/HOL/equalities.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/equalities.ML Wed Jul 15 10:15:13 1998 +0200
@@ -51,7 +51,7 @@
bind_thm("empty_not_insert",insert_not_empty RS not_sym);
Addsimps[empty_not_insert];
-Goal "!!a. a:A ==> insert a A = A";
+Goal "a:A ==> insert a A = A";
by (Blast_tac 1);
qed "insert_absorb";
(* Addsimps [insert_absorb] causes recursive (ie quadtratic) calls
@@ -72,12 +72,12 @@
qed "insert_subset";
Addsimps[insert_subset];
-Goal "!!a. insert a A ~= insert a B ==> A ~= B";
+Goal "insert a A ~= insert a B ==> A ~= B";
by (Blast_tac 1);
qed "insert_lim";
(* use new B rather than (A-{a}) to avoid infinite unfolding *)
-Goal "!!a. a:A ==> ? B. A = insert a B & a ~: B";
+Goal "a:A ==> ? B. A = insert a B & a ~: B";
by (res_inst_tac [("x","A-{a}")] exI 1);
by (Blast_tac 1);
qed "mk_disjoint_insert";
@@ -114,7 +114,7 @@
by (Blast_tac 1);
qed "image_image";
-Goal "!!x. x:A ==> insert (f x) (f``A) = f``A";
+Goal "x:A ==> insert (f x) (f``A) = f``A";
by (Blast_tac 1);
qed "insert_image";
Addsimps [insert_image];
@@ -164,11 +164,11 @@
(*Intersection is an AC-operator*)
val Int_ac = [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute];
-Goal "!!A B. B<=A ==> A Int B = B";
+Goal "B<=A ==> A Int B = B";
by (Blast_tac 1);
qed "Int_absorb1";
-Goal "!!A B. A<=B ==> A Int B = A";
+Goal "A<=B ==> A Int B = A";
by (Blast_tac 1);
qed "Int_absorb2";
@@ -243,11 +243,11 @@
(*Union is an AC-operator*)
val Un_ac = [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute];
-Goal "!!A B. A<=B ==> A Un B = B";
+Goal "A<=B ==> A Un B = B";
by (Blast_tac 1);
qed "Un_absorb1";
-Goal "!!A B. B<=A ==> A Un B = A";
+Goal "B<=A ==> A Un B = A";
by (Blast_tac 1);
qed "Un_absorb2";
@@ -446,7 +446,7 @@
qed "UN_singleton";
Addsimps [UN_singleton];
-Goal "!!k. k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)";
+Goal "k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)";
by (Blast_tac 1);
qed "UN_absorb";
@@ -455,7 +455,7 @@
qed "INT_empty";
Addsimps[INT_empty];
-Goal "!!k. k:I ==> A k Int (INT i:I. A i) = (INT i:I. A i)";
+Goal "k:I ==> A k Int (INT i:I. A i) = (INT i:I. A i)";
by (Blast_tac 1);
qed "INT_absorb";
@@ -490,12 +490,12 @@
by (Blast_tac 1);
qed "Inter_image_eq";
-Goal "!!A. A~={} ==> (UN y:A. c) = c";
+Goal "A~={} ==> (UN y:A. c) = c";
by (Blast_tac 1);
qed "UN_constant";
Addsimps[UN_constant];
-Goal "!!A. A~={} ==> (INT y:A. c) = c";
+Goal "A~={} ==> (INT y:A. c) = c";
by (Blast_tac 1);
qed "INT_constant";
Addsimps[INT_constant];
@@ -601,7 +601,7 @@
qed "Diff_cancel";
Addsimps[Diff_cancel];
-Goal "!!A B. A Int B = {} ==> A-B = A";
+Goal "A Int B = {} ==> A-B = A";
by (blast_tac (claset() addEs [equalityE]) 1);
qed "Diff_triv";
@@ -620,7 +620,7 @@
qed "Diff_UNIV";
Addsimps[Diff_UNIV];
-Goal "!!x. x~:A ==> A - insert x B = A-B";
+Goal "x~:A ==> A - insert x B = A-B";
by (Blast_tac 1);
qed "Diff_insert0";
Addsimps [Diff_insert0];
@@ -640,12 +640,12 @@
by (Blast_tac 1);
qed "insert_Diff_if";
-Goal "!!x. x:B ==> insert x A - B = A-B";
+Goal "x:B ==> insert x A - B = A-B";
by (Blast_tac 1);
qed "insert_Diff1";
Addsimps [insert_Diff1];
-Goal "!!a. a:A ==> insert a (A-{a}) = A";
+Goal "a:A ==> insert a (A-{a}) = A";
by (Blast_tac 1);
qed "insert_Diff";
@@ -654,11 +654,11 @@
qed "Diff_disjoint";
Addsimps[Diff_disjoint];
-Goal "!!A. A<=B ==> A Un (B-A) = B";
+Goal "A<=B ==> A Un (B-A) = B";
by (Blast_tac 1);
qed "Diff_partition";
-Goal "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
+Goal "[| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
by (Blast_tac 1);
qed "double_diff";
--- a/src/HOL/ex/Fib.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/ex/Fib.ML Wed Jul 15 10:15:13 1998 +0200
@@ -45,7 +45,7 @@
(* Also add 0 < fib (Suc n) *)
Addsimps [fib_Suc_neq_0, [neq0_conv, fib_Suc_neq_0] MRS iffD1];
-Goal "!!n. 0<n ==> 0 < fib n";
+Goal "0<n ==> 0 < fib n";
by (rtac (not0_implies_Suc RS exE) 1);
by Auto_tac;
qed "fib_gr_0";
@@ -93,12 +93,12 @@
by (asm_simp_tac (simpset() addsimps [gcd_fib_Suc_eq_1, gcd_mult_cancel]) 1);
qed "gcd_fib_add";
-Goal "!!m. m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)";
+Goal "m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)";
by (rtac (gcd_fib_add RS sym RS trans) 1);
by (Asm_simp_tac 1);
qed "gcd_fib_diff";
-Goal "!!m. 0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
+Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
by (res_inst_tac [("n","n")] less_induct 1);
by (stac mod_if 1);
by (Asm_simp_tac 1);
--- a/src/HOL/ex/InSort.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/ex/InSort.ML Wed Jul 15 10:15:13 1998 +0200
@@ -32,7 +32,7 @@
qed "sorted_ins";
Addsimps [sorted_ins];
-Goal "!!f. [| total(f); transf(f) |] ==> sorted f (insort f xs)";
+Goal "[| total(f); transf(f) |] ==> sorted f (insort f xs)";
by (list.induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "sorted_insort";
--- a/src/HOL/ex/MT.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/ex/MT.ML Wed Jul 15 10:15:13 1998 +0200
@@ -574,7 +574,7 @@
(* Introduction rules for hasty *)
-Goalw [hasty_def] "!!c. c isof t ==> v_const(c) hasty t";
+Goalw [hasty_def] "c isof t ==> v_const(c) hasty t";
by (etac hasty_rel_const_coind 1);
qed "hasty_const";
@@ -592,7 +592,7 @@
by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
qed "hasty_elim_const_lem";
-Goal "!!c. v_const(c) hasty t ==> c isof t";
+Goal "v_const(c) hasty t ==> c isof t";
by (dtac hasty_elim_const_lem 1);
by (Blast_tac 1);
qed "hasty_elim_const";
--- a/src/HOL/ex/Primes.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/ex/Primes.ML Wed Jul 15 10:15:13 1998 +0200
@@ -46,7 +46,7 @@
qed "gcd_0";
Addsimps [gcd_0];
-Goal "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)";
+Goal "0<n ==> gcd(m,n) = gcd (n, m mod n)";
by (rtac (gcd_eq RS trans) 1);
by (Asm_simp_tac 1);
by (Blast_tac 1);
@@ -71,7 +71,7 @@
(*Maximality: for all m,n,f naturals,
if f divides m and f divides n then f divides gcd(m,n)*)
-Goal "!!k. (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
+Goal "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
by (ALLGOALS
(asm_full_simp_tac (simpset() addsimps[gcd_non_0, dvd_mod,
@@ -84,7 +84,7 @@
qed "is_gcd";
(*uniqueness of GCDs*)
-Goalw [is_gcd_def] "!!m n. [| is_gcd m a b; is_gcd n a b |] ==> m=n";
+Goalw [is_gcd_def] "[| is_gcd m a b; is_gcd n a b |] ==> m=n";
by (blast_tac (claset() addIs [dvd_anti_sym]) 1);
qed "is_gcd_unique";
@@ -150,20 +150,20 @@
qed "gcd_mult";
Addsimps [gcd_mult];
-Goal "!!k. [| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
+Goal "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
by (subgoal_tac "m = gcd(m*k, m*n)" 1);
by (etac ssubst 1 THEN rtac gcd_greatest 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_mult_distrib2 RS sym])));
qed "relprime_dvd_mult";
-Goalw [prime_def] "!!p. [| p: prime; ~ p dvd n |] ==> gcd (p, n) = 1";
+Goalw [prime_def] "[| p: prime; ~ p dvd n |] ==> gcd (p, n) = 1";
by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd_both 1);
-by (fast_tac (claset() addss (simpset())) 1);
+by Auto_tac;
qed "prime_imp_relprime";
(*This theorem leads immediately to a proof of the uniqueness of factorization.
If p divides a product of primes then it is one of those primes.*)
-Goal "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
+Goal "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
by (blast_tac (claset() addIs [relprime_dvd_mult, prime_imp_relprime]) 1);
qed "prime_dvd_mult";
@@ -192,7 +192,7 @@
gcd_dvd1, gcd_dvd2]) 1);
qed "gcd_dvd_gcd_mult";
-Goal "!!n. gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)";
+Goal "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)";
by (rtac dvd_anti_sym 1);
by (rtac gcd_dvd_gcd_mult 2);
by (rtac ([relprime_dvd_mult, gcd_dvd2] MRS gcd_greatest) 1);
--- a/src/HOL/ex/Primrec.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/ex/Primrec.ML Wed Jul 15 10:15:13 1998 +0200
@@ -71,7 +71,7 @@
qed_spec_mp "ack_less_mono2";
(*PROPERTY A 5', monotonicity for<=*)
-Goal "!!i j k. j<=k ==> ack(i,j)<=ack(i,k)";
+Goal "j<=k ==> ack(i,j)<=ack(i,k)";
by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
by (blast_tac (claset() addIs [ack_less_mono2]) 1);
qed "ack_le_mono2";
@@ -127,13 +127,13 @@
by (blast_tac (claset() addIs [Suc_leI RS le_less_trans, ack_less_mono2]) 1);
val lemma = result();
-Goal "!!i j k. i<j ==> ack(i,k) < ack(j,k)";
+Goal "i<j ==> ack(i,k) < ack(j,k)";
by (dtac less_eq_Suc_add 1);
by (blast_tac (claset() addSIs [lemma]) 1);
qed "ack_less_mono1";
(*PROPERTY A 7', monotonicity for<=*)
-Goal "!!i j k. i<=j ==> ack(i,k)<=ack(j,k)";
+Goal "i<=j ==> ack(i,k)<=ack(j,k)";
by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
by (blast_tac (claset() addIs [ack_less_mono1]) 1);
qed "ack_le_mono1";
@@ -160,7 +160,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) ==> i+j < ack(Suc(Suc(Suc(Suc(k)))), j)";
+Goal "i < ack(k,j) ==> i+j < ack(Suc(Suc(Suc(Suc(k)))), j)";
by (res_inst_tac [("j", "ack(k,j) + ack(0,j)")] less_trans 1);
by (rtac (ack_add_bound RS less_le_trans) 2);
by (Asm_simp_tac 2);
@@ -254,7 +254,7 @@
by (REPEAT (blast_tac (claset() addIs [ack_add_bound2]) 1));
qed "PREC_case";
-Goal "!!f. f:PRIMREC ==> EX k. ALL l. f l < ack(k, list_add l)";
+Goal "f:PRIMREC ==> EX k. ALL l. f l < ack(k, list_add l)";
by (etac PRIMREC.induct 1);
by (ALLGOALS
(blast_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case,
--- a/src/HOLCF/Fix.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOLCF/Fix.ML Wed Jul 15 10:15:13 1998 +0200
@@ -884,7 +884,7 @@
(Simp_tac 1)
]);
-Goal "!! P. [| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
+Goal "[| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
\ ==> adm (%x. P x = Q x)";
by (subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
by (Asm_simp_tac 1);
--- a/src/HOLCF/IMP/Denotational.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOLCF/IMP/Denotational.ML Wed Jul 15 10:15:13 1998 +0200
@@ -22,7 +22,7 @@
qed "dlift_is_Def";
Addsimps [dlift_is_Def];
-Goal "!!c. <c,s> -c-> t ==> D c`(Discr s) = (Def t)";
+Goal "<c,s> -c-> t ==> D c`(Discr s) = (Def t)";
by (etac evalc.induct 1);
by (ALLGOALS Asm_simp_tac);
by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac));
--- a/src/HOLCF/Lift.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOLCF/Lift.ML Wed Jul 15 10:15:13 1998 +0200
@@ -36,9 +36,7 @@
Goal "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==> \
\ cont (%y. lift_case UU (f y) (g y))";
-by (rtac cont2cont_app 1);
-back();
-by (safe_tac set_cs);
+by (res_inst_tac [("tt","g")] cont2cont_app 1);
by (rtac cont_flift1_not_arg 1);
by Auto_tac;
by (rtac cont_flift1_arg 1);
@@ -100,7 +98,7 @@
Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU];
-Goal "!!x. x~=UU ==> (flift2 f)`x~=UU";
+Goal "x~=UU ==> (flift2 f)`x~=UU";
by (def_tac 1);
qed"flift2_nUU";
--- a/src/HOLCF/Lift2.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOLCF/Lift2.ML Wed Jul 15 10:15:13 1998 +0200
@@ -44,7 +44,7 @@
(* Tailoring notUU_I of Pcpo.ML to Undef *)
-Goal "!!x. [| x<<y; ~x=Undef |] ==> ~y=Undef";
+Goal "[| x<<y; ~x=Undef |] ==> ~y=Undef";
by (etac contrapos 1);
by (hyp_subst_tac 1);
by (rtac antisym_less 1);
--- a/src/HOLCF/Lift3.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOLCF/Lift3.ML Wed Jul 15 10:15:13 1998 +0200
@@ -139,13 +139,13 @@
(* Two specific lemmas for the combination of LCF and HOL terms *)
-Goal "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
+Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
by (rtac cont2cont_CF1L 1);
by (REPEAT (resolve_tac cont_lemmas1 1));
by Auto_tac;
qed"cont_fapp_app";
-Goal "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
+Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
by (rtac cont2cont_CF1L 1);
by (etac cont_fapp_app 1);
by (assume_tac 1);
--- a/src/HOLCF/Tr.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOLCF/Tr.ML Wed Jul 15 10:15:13 1998 +0200
@@ -120,7 +120,7 @@
by Auto_tac;
qed"andalso_or";
-Goal "!!t.[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
+Goal "[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
by (rtac iffI 1);
by (res_inst_tac [("p","t")] trE 1);
by Auto_tac;
@@ -176,12 +176,12 @@
val adm_tricks = [adm_trick_1,adm_trick_2];
-Goal "!!f. cont(f) ==> adm (%x. (f x)~=TT)";
+Goal "cont(f) ==> adm (%x. (f x)~=TT)";
by (simp_tac (HOL_basic_ss addsimps adm_tricks) 1);
by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1));
qed"adm_nTT";
-Goal "!!f. cont(f) ==> adm (%x. (f x)~=FF)";
+Goal "cont(f) ==> adm (%x. (f x)~=FF)";
by (simp_tac (HOL_basic_ss addsimps adm_tricks) 1);
by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1));
qed"adm_nFF";
--- a/src/ZF/Cardinal.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/ZF/Cardinal.ML Wed Jul 15 10:15:13 1998 +0200
@@ -257,7 +257,7 @@
(*Need AC to get X lepoll Y ==> |X| le |Y|; see well_ord_lepoll_imp_Card_le
Converse also requires AC, but see well_ord_cardinal_eqE*)
-Goalw [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|";
+Goalw [eqpoll_def,cardinal_def] "X eqpoll Y ==> |X| = |Y|";
by (rtac Least_cong 1);
by (blast_tac (claset() addIs [comp_bij, bij_converse_bij]) 1);
qed "cardinal_cong";
--- a/src/ZF/Coind/Map.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/ZF/Coind/Map.ML Wed Jul 15 10:15:13 1998 +0200
@@ -82,7 +82,7 @@
(* Monotonicity *)
(* ############################################################ *)
-Goalw [PMap_def,TMap_def] "!!A. B<=C ==> PMap(A,B)<=PMap(A,C)";
+Goalw [PMap_def,TMap_def] "B<=C ==> PMap(A,B)<=PMap(A,C)";
by (Fast_tac 1);
qed "map_mono";
--- a/src/ZF/Ordinal.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/ZF/Ordinal.ML Wed Jul 15 10:15:13 1998 +0200
@@ -103,7 +103,7 @@
(*** Lemmas for ordinals ***)
-Goalw [Ord_def,Transset_def] "!!i j.[| Ord(i); j:i |] ==> Ord(j)";
+Goalw [Ord_def,Transset_def] "[| Ord(i); j:i |] ==> Ord(j)";
by (Blast_tac 1);
qed "Ord_in_Ord";
@@ -117,7 +117,7 @@
ORELSE eresolve_tac [Ord_contains_Transset, subsetD] 1));
qed "Ord_subset_Ord";
-Goalw [Ord_def,Transset_def] "!!i j. [| j:i; Ord(i) |] ==> j<=i";
+Goalw [Ord_def,Transset_def] "[| j:i; Ord(i) |] ==> j<=i";
by (Blast_tac 1);
qed "OrdmemD";
--- a/src/ZF/Perm.ML Tue Jul 14 13:33:12 1998 +0200
+++ b/src/ZF/Perm.ML Wed Jul 15 10:15:13 1998 +0200
@@ -133,7 +133,7 @@
by (rtac (prem RS lam_mono) 1);
qed "id_mono";
-Goalw [inj_def,id_def] "!!A B. A<=B ==> id(A): inj(A,B)";
+Goalw [inj_def,id_def] "A<=B ==> id(A): inj(A,B)";
by (REPEAT (ares_tac [CollectI,lam_type] 1));
by (etac subsetD 1 THEN assume_tac 1);
by (Simp_tac 1);