src/HOL/Arith.ML
changeset 5069 3ea049f7979d
parent 4830 bd73675adbed
child 5078 7b5ea59c0275
     1.1 --- a/src/HOL/Arith.ML	Mon Jun 22 17:13:09 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Mon Jun 22 17:26:46 1998 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  (* Could be (and is, below) generalized in various ways;
     1.5     However, none of the generalizations are currently in the simpset,
     1.6     and I dread to think what happens if I put them in *)
     1.7 -goal thy "!!n. 0 < n ==> Suc(n-1) = n";
     1.8 +Goal "!!n. 0 < n ==> Suc(n-1) = n";
     1.9  by (asm_simp_tac (simpset() addsplits [split_nat_case]) 1);
    1.10  qed "Suc_pred";
    1.11  Addsimps [Suc_pred];
    1.12 @@ -63,25 +63,25 @@
    1.13  (*Addition is an AC-operator*)
    1.14  val add_ac = [add_assoc, add_commute, add_left_commute];
    1.15  
    1.16 -goal thy "!!k::nat. (k + m = k + n) = (m=n)";
    1.17 +Goal "!!k::nat. (k + m = k + n) = (m=n)";
    1.18  by (induct_tac "k" 1);
    1.19  by (Simp_tac 1);
    1.20  by (Asm_simp_tac 1);
    1.21  qed "add_left_cancel";
    1.22  
    1.23 -goal thy "!!k::nat. (m + k = n + k) = (m=n)";
    1.24 +Goal "!!k::nat. (m + k = n + k) = (m=n)";
    1.25  by (induct_tac "k" 1);
    1.26  by (Simp_tac 1);
    1.27  by (Asm_simp_tac 1);
    1.28  qed "add_right_cancel";
    1.29  
    1.30 -goal thy "!!k::nat. (k + m <= k + n) = (m<=n)";
    1.31 +Goal "!!k::nat. (k + m <= k + n) = (m<=n)";
    1.32  by (induct_tac "k" 1);
    1.33  by (Simp_tac 1);
    1.34  by (Asm_simp_tac 1);
    1.35  qed "add_left_cancel_le";
    1.36  
    1.37 -goal thy "!!k::nat. (k + m < k + n) = (m<n)";
    1.38 +Goal "!!k::nat. (k + m < k + n) = (m<n)";
    1.39  by (induct_tac "k" 1);
    1.40  by (Simp_tac 1);
    1.41  by (Asm_simp_tac 1);
    1.42 @@ -92,26 +92,26 @@
    1.43  
    1.44  (** Reasoning about m+0=0, etc. **)
    1.45  
    1.46 -goal thy "(m+n = 0) = (m=0 & n=0)";
    1.47 +Goal "(m+n = 0) = (m=0 & n=0)";
    1.48  by (induct_tac "m" 1);
    1.49  by (ALLGOALS Asm_simp_tac);
    1.50  qed "add_is_0";
    1.51  AddIffs [add_is_0];
    1.52  
    1.53 -goal thy "(0<m+n) = (0<m | 0<n)";
    1.54 +Goal "(0<m+n) = (0<m | 0<n)";
    1.55  by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
    1.56  qed "add_gr_0";
    1.57  AddIffs [add_gr_0];
    1.58  
    1.59  (* FIXME: really needed?? *)
    1.60 -goal thy "((m+n)-1 = 0) = (m=0 & n-1 = 0 | m-1 = 0 & n=0)";
    1.61 +Goal "((m+n)-1 = 0) = (m=0 & n-1 = 0 | m-1 = 0 & n=0)";
    1.62  by (exhaust_tac "m" 1);
    1.63  by (ALLGOALS (fast_tac (claset() addss (simpset()))));
    1.64  qed "pred_add_is_0";
    1.65  Addsimps [pred_add_is_0];
    1.66  
    1.67  (* Could be generalized, eg to "!!n. k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
    1.68 -goal thy "!!n. 0<n ==> m + (n-1) = (m+n)-1";
    1.69 +Goal "!!n. 0<n ==> m + (n-1) = (m+n)-1";
    1.70  by (exhaust_tac "m" 1);
    1.71  by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
    1.72                                        addsplits [split_nat_case])));
    1.73 @@ -121,7 +121,7 @@
    1.74  
    1.75  (**** Additional theorems about "less than" ****)
    1.76  
    1.77 -goal thy "i<j --> (EX k. j = Suc(i+k))";
    1.78 +Goal "i<j --> (EX k. j = Suc(i+k))";
    1.79  by (induct_tac "j" 1);
    1.80  by (Simp_tac 1);
    1.81  by (blast_tac (claset() addSEs [less_SucE] 
    1.82 @@ -131,21 +131,21 @@
    1.83  (* [| i<j;  !!x. j = Suc(i+x) ==> Q |] ==> Q *)
    1.84  bind_thm ("less_natE", lemma RS mp RS exE);
    1.85  
    1.86 -goal thy "!!m. m<n --> (? k. n=Suc(m+k))";
    1.87 +Goal "!!m. m<n --> (? k. n=Suc(m+k))";
    1.88  by (induct_tac "n" 1);
    1.89  by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
    1.90  by (blast_tac (claset() addSEs [less_SucE] 
    1.91                         addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
    1.92  qed_spec_mp "less_eq_Suc_add";
    1.93  
    1.94 -goal thy "n <= ((m + n)::nat)";
    1.95 +Goal "n <= ((m + n)::nat)";
    1.96  by (induct_tac "m" 1);
    1.97  by (ALLGOALS Simp_tac);
    1.98  by (etac le_trans 1);
    1.99  by (rtac (lessI RS less_imp_le) 1);
   1.100  qed "le_add2";
   1.101  
   1.102 -goal thy "n <= ((n + m)::nat)";
   1.103 +Goal "n <= ((n + m)::nat)";
   1.104  by (simp_tac (simpset() addsimps add_ac) 1);
   1.105  by (rtac le_add2 1);
   1.106  qed "le_add1";
   1.107 @@ -165,49 +165,49 @@
   1.108  (*"i < j ==> i < m+j"*)
   1.109  bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
   1.110  
   1.111 -goal thy "!!i. i+j < (k::nat) ==> i<k";
   1.112 +Goal "!!i. i+j < (k::nat) ==> i<k";
   1.113  by (etac rev_mp 1);
   1.114  by (induct_tac "j" 1);
   1.115  by (ALLGOALS Asm_simp_tac);
   1.116  by (blast_tac (claset() addDs [Suc_lessD]) 1);
   1.117  qed "add_lessD1";
   1.118  
   1.119 -goal thy "!!i::nat. ~ (i+j < i)";
   1.120 +Goal "!!i::nat. ~ (i+j < i)";
   1.121  by (rtac notI 1);
   1.122  by (etac (add_lessD1 RS less_irrefl) 1);
   1.123  qed "not_add_less1";
   1.124  
   1.125 -goal thy "!!i::nat. ~ (j+i < i)";
   1.126 +Goal "!!i::nat. ~ (j+i < i)";
   1.127  by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1);
   1.128  qed "not_add_less2";
   1.129  AddIffs [not_add_less1, not_add_less2];
   1.130  
   1.131 -goal thy "!!k::nat. m <= n ==> m <= n+k";
   1.132 +Goal "!!k::nat. m <= n ==> m <= n+k";
   1.133  by (etac le_trans 1);
   1.134  by (rtac le_add1 1);
   1.135  qed "le_imp_add_le";
   1.136  
   1.137 -goal thy "!!k::nat. m < n ==> m < n+k";
   1.138 +Goal "!!k::nat. m < n ==> m < n+k";
   1.139  by (etac less_le_trans 1);
   1.140  by (rtac le_add1 1);
   1.141  qed "less_imp_add_less";
   1.142  
   1.143 -goal thy "m+k<=n --> m<=(n::nat)";
   1.144 +Goal "m+k<=n --> m<=(n::nat)";
   1.145  by (induct_tac "k" 1);
   1.146  by (ALLGOALS Asm_simp_tac);
   1.147  by (blast_tac (claset() addDs [Suc_leD]) 1);
   1.148  qed_spec_mp "add_leD1";
   1.149  
   1.150 -goal thy "!!n::nat. m+k<=n ==> k<=n";
   1.151 +Goal "!!n::nat. m+k<=n ==> k<=n";
   1.152  by (full_simp_tac (simpset() addsimps [add_commute]) 1);
   1.153  by (etac add_leD1 1);
   1.154  qed_spec_mp "add_leD2";
   1.155  
   1.156 -goal thy "!!n::nat. m+k<=n ==> m<=n & k<=n";
   1.157 +Goal "!!n::nat. m+k<=n ==> m<=n & k<=n";
   1.158  by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1);
   1.159  bind_thm ("add_leE", result() RS conjE);
   1.160  
   1.161 -goal thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
   1.162 +Goal "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
   1.163  by (safe_tac (claset() addSDs [less_eq_Suc_add]));
   1.164  by (asm_full_simp_tac
   1.165      (simpset() delsimps [add_Suc_right]
   1.166 @@ -220,13 +220,13 @@
   1.167  (*** Monotonicity of Addition ***)
   1.168  
   1.169  (*strict, in 1st argument*)
   1.170 -goal thy "!!i j k::nat. i < j ==> i + k < j + k";
   1.171 +Goal "!!i j k::nat. i < j ==> i + k < j + k";
   1.172  by (induct_tac "k" 1);
   1.173  by (ALLGOALS Asm_simp_tac);
   1.174  qed "add_less_mono1";
   1.175  
   1.176  (*strict, in both arguments*)
   1.177 -goal thy "!!i j k::nat. [|i < j; k < l|] ==> i + k < j + l";
   1.178 +Goal "!!i j k::nat. [|i < j; k < l|] ==> i + k < j + l";
   1.179  by (rtac (add_less_mono1 RS less_trans) 1);
   1.180  by (REPEAT (assume_tac 1));
   1.181  by (induct_tac "j" 1);
   1.182 @@ -244,14 +244,14 @@
   1.183  qed "less_mono_imp_le_mono";
   1.184  
   1.185  (*non-strict, in 1st argument*)
   1.186 -goal thy "!!i j k::nat. i<=j ==> i + k <= j + k";
   1.187 +Goal "!!i j k::nat. i<=j ==> i + k <= j + k";
   1.188  by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1);
   1.189  by (etac add_less_mono1 1);
   1.190  by (assume_tac 1);
   1.191  qed "add_le_mono1";
   1.192  
   1.193  (*non-strict, in both arguments*)
   1.194 -goal thy "!!k l::nat. [|i<=j;  k<=l |] ==> i + k <= j + l";
   1.195 +Goal "!!k l::nat. [|i<=j;  k<=l |] ==> i + k <= j + l";
   1.196  by (etac (add_le_mono1 RS le_trans) 1);
   1.197  by (simp_tac (simpset() addsimps [add_commute]) 1);
   1.198  (*j moves to the end because it is free while k, l are bound*)
   1.199 @@ -272,11 +272,11 @@
   1.200  
   1.201  Addsimps [mult_0_right, mult_Suc_right];
   1.202  
   1.203 -goal thy "1 * n = n";
   1.204 +Goal "1 * n = n";
   1.205  by (Asm_simp_tac 1);
   1.206  qed "mult_1";
   1.207  
   1.208 -goal thy "n * 1 = n";
   1.209 +Goal "n * 1 = n";
   1.210  by (Asm_simp_tac 1);
   1.211  qed "mult_1_right";
   1.212  
   1.213 @@ -304,14 +304,14 @@
   1.214  
   1.215  val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
   1.216  
   1.217 -goal thy "(m*n = 0) = (m=0 | n=0)";
   1.218 +Goal "(m*n = 0) = (m=0 | n=0)";
   1.219  by (induct_tac "m" 1);
   1.220  by (induct_tac "n" 2);
   1.221  by (ALLGOALS Asm_simp_tac);
   1.222  qed "mult_is_0";
   1.223  Addsimps [mult_is_0];
   1.224  
   1.225 -goal thy "!!m::nat. m <= m*m";
   1.226 +Goal "!!m::nat. m <= m*m";
   1.227  by (induct_tac "m" 1);
   1.228  by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym])));
   1.229  by (etac (le_add2 RSN (2,le_trans)) 1);
   1.230 @@ -326,16 +326,16 @@
   1.231  Addsimps [diff_self_eq_0];
   1.232  
   1.233  (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
   1.234 -goal thy "~ m<n --> n+(m-n) = (m::nat)";
   1.235 +Goal "~ m<n --> n+(m-n) = (m::nat)";
   1.236  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.237  by (ALLGOALS Asm_simp_tac);
   1.238  qed_spec_mp "add_diff_inverse";
   1.239  
   1.240 -goal thy "!!m. n<=m ==> n+(m-n) = (m::nat)";
   1.241 +Goal "!!m. n<=m ==> n+(m-n) = (m::nat)";
   1.242  by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1);
   1.243  qed "le_add_diff_inverse";
   1.244  
   1.245 -goal thy "!!m. n<=m ==> (m-n)+n = (m::nat)";
   1.246 +Goal "!!m. n<=m ==> (m-n)+n = (m::nat)";
   1.247  by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1);
   1.248  qed "le_add_diff_inverse2";
   1.249  
   1.250 @@ -350,13 +350,13 @@
   1.251  by (ALLGOALS Asm_simp_tac);
   1.252  qed "Suc_diff_n";
   1.253  
   1.254 -goal thy "m - n < Suc(m)";
   1.255 +Goal "m - n < Suc(m)";
   1.256  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.257  by (etac less_SucE 3);
   1.258  by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
   1.259  qed "diff_less_Suc";
   1.260  
   1.261 -goal thy "!!m::nat. m - n <= m";
   1.262 +Goal "!!m::nat. m - n <= m";
   1.263  by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
   1.264  by (ALLGOALS Asm_simp_tac);
   1.265  qed "diff_le_self";
   1.266 @@ -365,61 +365,61 @@
   1.267  (* j<k ==> j-n < k *)
   1.268  bind_thm ("less_imp_diff_less", diff_le_self RS le_less_trans);
   1.269  
   1.270 -goal thy "!!i::nat. i-j-k = i - (j+k)";
   1.271 +Goal "!!i::nat. i-j-k = i - (j+k)";
   1.272  by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
   1.273  by (ALLGOALS Asm_simp_tac);
   1.274  qed "diff_diff_left";
   1.275  
   1.276 -goal Arith.thy "(Suc m - n) - Suc k = m - n - k";
   1.277 +Goal "(Suc m - n) - Suc k = m - n - k";
   1.278  by (simp_tac (simpset() addsimps [diff_diff_left]) 1);
   1.279  qed "Suc_diff_diff";
   1.280  Addsimps [Suc_diff_diff];
   1.281  
   1.282 -goal thy "!!n. 0<n ==> n - Suc i < n";
   1.283 +Goal "!!n. 0<n ==> n - Suc i < n";
   1.284  by (res_inst_tac [("n","n")] natE 1);
   1.285  by Safe_tac;
   1.286  by (asm_simp_tac (simpset() addsimps [le_eq_less_Suc RS sym]) 1);
   1.287  qed "diff_Suc_less";
   1.288  Addsimps [diff_Suc_less];
   1.289  
   1.290 -goal thy "!!n::nat. m - n <= Suc m - n";
   1.291 +Goal "!!n::nat. m - n <= Suc m - n";
   1.292  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.293  by (ALLGOALS Asm_simp_tac);
   1.294  qed "diff_le_Suc_diff";
   1.295  
   1.296  (*This and the next few suggested by Florian Kammueller*)
   1.297 -goal thy "!!i::nat. i-j-k = i-k-j";
   1.298 +Goal "!!i::nat. i-j-k = i-k-j";
   1.299  by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
   1.300  qed "diff_commute";
   1.301  
   1.302 -goal thy "!!i j k:: nat. k<=j --> j<=i --> i - (j - k) = i - j + k";
   1.303 +Goal "!!i j k:: nat. k<=j --> j<=i --> i - (j - k) = i - j + k";
   1.304  by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
   1.305  by (ALLGOALS Asm_simp_tac);
   1.306  by (asm_simp_tac
   1.307      (simpset() addsimps [Suc_diff_n, le_imp_less_Suc, le_Suc_eq]) 1);
   1.308  qed_spec_mp "diff_diff_right";
   1.309  
   1.310 -goal thy "!!i j k:: nat. k<=j --> (i + j) - k = i + (j - k)";
   1.311 +Goal "!!i j k:: nat. k<=j --> (i + j) - k = i + (j - k)";
   1.312  by (res_inst_tac [("m","j"),("n","k")] diff_induct 1);
   1.313  by (ALLGOALS Asm_simp_tac);
   1.314  qed_spec_mp "diff_add_assoc";
   1.315  
   1.316 -goal thy "!!i j k:: nat. k<=j --> (j + i) - k = i + (j - k)";
   1.317 +Goal "!!i j k:: nat. k<=j --> (j + i) - k = i + (j - k)";
   1.318  by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1);
   1.319  qed_spec_mp "diff_add_assoc2";
   1.320  
   1.321 -goal thy "!!n::nat. (n+m) - n = m";
   1.322 +Goal "!!n::nat. (n+m) - n = m";
   1.323  by (induct_tac "n" 1);
   1.324  by (ALLGOALS Asm_simp_tac);
   1.325  qed "diff_add_inverse";
   1.326  Addsimps [diff_add_inverse];
   1.327  
   1.328 -goal thy "!!n::nat.(m+n) - n = m";
   1.329 +Goal "!!n::nat.(m+n) - n = m";
   1.330  by (simp_tac (simpset() addsimps [diff_add_assoc]) 1);
   1.331  qed "diff_add_inverse2";
   1.332  Addsimps [diff_add_inverse2];
   1.333  
   1.334 -goal thy "!!i j k::nat. i<=j ==> (j-i=k) = (j=k+i)";
   1.335 +Goal "!!i j k::nat. i<=j ==> (j-i=k) = (j=k+i)";
   1.336  by Safe_tac;
   1.337  by (ALLGOALS Asm_simp_tac);
   1.338  qed "le_imp_diff_is_add";
   1.339 @@ -442,15 +442,15 @@
   1.340  by (ALLGOALS Asm_simp_tac);
   1.341  qed "less_imp_diff_positive";
   1.342  
   1.343 -goal thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
   1.344 +Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
   1.345  by (simp_tac (simpset() addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]) 1);
   1.346  qed "if_Suc_diff_n";
   1.347  
   1.348 -goal thy "Suc(m)-n <= Suc(m-n)";
   1.349 +Goal "Suc(m)-n <= Suc(m-n)";
   1.350  by (simp_tac (simpset() addsimps [if_Suc_diff_n]) 1);
   1.351  qed "diff_Suc_le_Suc_diff";
   1.352  
   1.353 -goal thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
   1.354 +Goal "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
   1.355  by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
   1.356  by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
   1.357  qed "zero_induct_lemma";
   1.358 @@ -461,20 +461,20 @@
   1.359  by (REPEAT (ares_tac ([impI,allI]@prems) 1));
   1.360  qed "zero_induct";
   1.361  
   1.362 -goal thy "!!k::nat. (k+m) - (k+n) = m - n";
   1.363 +Goal "!!k::nat. (k+m) - (k+n) = m - n";
   1.364  by (induct_tac "k" 1);
   1.365  by (ALLGOALS Asm_simp_tac);
   1.366  qed "diff_cancel";
   1.367  Addsimps [diff_cancel];
   1.368  
   1.369 -goal thy "!!m::nat. (m+k) - (n+k) = m - n";
   1.370 +Goal "!!m::nat. (m+k) - (n+k) = m - n";
   1.371  val add_commute_k = read_instantiate [("n","k")] add_commute;
   1.372  by (asm_simp_tac (simpset() addsimps ([add_commute_k])) 1);
   1.373  qed "diff_cancel2";
   1.374  Addsimps [diff_cancel2];
   1.375  
   1.376  (*From Clemens Ballarin*)
   1.377 -goal thy "!!n::nat. [| k<=n; n<=m |] ==> (m-k) - (n-k) = m-n";
   1.378 +Goal "!!n::nat. [| k<=n; n<=m |] ==> (m-k) - (n-k) = m-n";
   1.379  by (subgoal_tac "k<=n --> n<=m --> (m-k) - (n-k) = m-n" 1);
   1.380  by (Asm_full_simp_tac 1);
   1.381  by (induct_tac "k" 1);
   1.382 @@ -489,7 +489,7 @@
   1.383  		       addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1);
   1.384  qed "diff_right_cancel";
   1.385  
   1.386 -goal thy "!!n::nat. n - (n+m) = 0";
   1.387 +Goal "!!n::nat. n - (n+m) = 0";
   1.388  by (induct_tac "n" 1);
   1.389  by (ALLGOALS Asm_simp_tac);
   1.390  qed "diff_add_0";
   1.391 @@ -497,12 +497,12 @@
   1.392  
   1.393  (** Difference distributes over multiplication **)
   1.394  
   1.395 -goal thy "!!m::nat. (m - n) * k = (m * k) - (n * k)";
   1.396 +Goal "!!m::nat. (m - n) * k = (m * k) - (n * k)";
   1.397  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.398  by (ALLGOALS Asm_simp_tac);
   1.399  qed "diff_mult_distrib" ;
   1.400  
   1.401 -goal thy "!!m::nat. k * (m - n) = (k * m) - (k * n)";
   1.402 +Goal "!!m::nat. k * (m - n) = (k * m) - (k * n)";
   1.403  val mult_commute_k = read_instantiate [("m","k")] mult_commute;
   1.404  by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1);
   1.405  qed "diff_mult_distrib2" ;
   1.406 @@ -511,13 +511,13 @@
   1.407  
   1.408  (*** Monotonicity of Multiplication ***)
   1.409  
   1.410 -goal thy "!!i::nat. i<=j ==> i*k<=j*k";
   1.411 +Goal "!!i::nat. i<=j ==> i*k<=j*k";
   1.412  by (induct_tac "k" 1);
   1.413  by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
   1.414  qed "mult_le_mono1";
   1.415  
   1.416  (*<=monotonicity, BOTH arguments*)
   1.417 -goal thy "!!i::nat. [| i<=j; k<=l |] ==> i*k<=j*l";
   1.418 +Goal "!!i::nat. [| i<=j; k<=l |] ==> i*k<=j*l";
   1.419  by (etac (mult_le_mono1 RS le_trans) 1);
   1.420  by (rtac le_trans 1);
   1.421  by (stac mult_commute 2);
   1.422 @@ -526,26 +526,26 @@
   1.423  qed "mult_le_mono";
   1.424  
   1.425  (*strict, in 1st argument; proof is by induction on k>0*)
   1.426 -goal thy "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
   1.427 +Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
   1.428  by (eres_inst_tac [("i","0")] less_natE 1);
   1.429  by (Asm_simp_tac 1);
   1.430  by (induct_tac "x" 1);
   1.431  by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));
   1.432  qed "mult_less_mono2";
   1.433  
   1.434 -goal thy "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
   1.435 +Goal "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
   1.436  by (dtac mult_less_mono2 1);
   1.437  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
   1.438  qed "mult_less_mono1";
   1.439  
   1.440 -goal thy "(0 < m*n) = (0<m & 0<n)";
   1.441 +Goal "(0 < m*n) = (0<m & 0<n)";
   1.442  by (induct_tac "m" 1);
   1.443  by (induct_tac "n" 2);
   1.444  by (ALLGOALS Asm_simp_tac);
   1.445  qed "zero_less_mult_iff";
   1.446  Addsimps [zero_less_mult_iff];
   1.447  
   1.448 -goal thy "(m*n = 1) = (m=1 & n=1)";
   1.449 +Goal "(m*n = 1) = (m=1 & n=1)";
   1.450  by (induct_tac "m" 1);
   1.451  by (Simp_tac 1);
   1.452  by (induct_tac "n" 1);
   1.453 @@ -554,29 +554,29 @@
   1.454  qed "mult_eq_1_iff";
   1.455  Addsimps [mult_eq_1_iff];
   1.456  
   1.457 -goal thy "!!k. 0<k ==> (m*k < n*k) = (m<n)";
   1.458 +Goal "!!k. 0<k ==> (m*k < n*k) = (m<n)";
   1.459  by (safe_tac (claset() addSIs [mult_less_mono1]));
   1.460  by (cut_facts_tac [less_linear] 1);
   1.461  by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
   1.462  qed "mult_less_cancel2";
   1.463  
   1.464 -goal thy "!!k. 0<k ==> (k*m < k*n) = (m<n)";
   1.465 +Goal "!!k. 0<k ==> (k*m < k*n) = (m<n)";
   1.466  by (dtac mult_less_cancel2 1);
   1.467  by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
   1.468  qed "mult_less_cancel1";
   1.469  Addsimps [mult_less_cancel1, mult_less_cancel2];
   1.470  
   1.471 -goal thy "(Suc k * m < Suc k * n) = (m < n)";
   1.472 +Goal "(Suc k * m < Suc k * n) = (m < n)";
   1.473  by (rtac mult_less_cancel1 1);
   1.474  by (Simp_tac 1);
   1.475  qed "Suc_mult_less_cancel1";
   1.476  
   1.477 -goalw thy [le_def] "(Suc k * m <= Suc k * n) = (m <= n)";
   1.478 +Goalw [le_def] "(Suc k * m <= Suc k * n) = (m <= n)";
   1.479  by (simp_tac (simpset_of HOL.thy) 1);
   1.480  by (rtac Suc_mult_less_cancel1 1);
   1.481  qed "Suc_mult_le_cancel1";
   1.482  
   1.483 -goal thy "!!k. 0<k ==> (m*k = n*k) = (m=n)";
   1.484 +Goal "!!k. 0<k ==> (m*k = n*k) = (m=n)";
   1.485  by (cut_facts_tac [less_linear] 1);
   1.486  by Safe_tac;
   1.487  by (assume_tac 2);
   1.488 @@ -584,13 +584,13 @@
   1.489  by (ALLGOALS Asm_full_simp_tac);
   1.490  qed "mult_cancel2";
   1.491  
   1.492 -goal thy "!!k. 0<k ==> (k*m = k*n) = (m=n)";
   1.493 +Goal "!!k. 0<k ==> (k*m = k*n) = (m=n)";
   1.494  by (dtac mult_cancel2 1);
   1.495  by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
   1.496  qed "mult_cancel1";
   1.497  Addsimps [mult_cancel1, mult_cancel2];
   1.498  
   1.499 -goal thy "(Suc k * m = Suc k * n) = (m = n)";
   1.500 +Goal "(Suc k * m = Suc k * n) = (m = n)";
   1.501  by (rtac mult_cancel1 1);
   1.502  by (Simp_tac 1);
   1.503  qed "Suc_mult_cancel1";
   1.504 @@ -598,7 +598,7 @@
   1.505  
   1.506  (** Lemma for gcd **)
   1.507  
   1.508 -goal thy "!!m n. m = m*n ==> n=1 | m=0";
   1.509 +Goal "!!m n. m = m*n ==> n=1 | m=0";
   1.510  by (dtac sym 1);
   1.511  by (rtac disjCI 1);
   1.512  by (rtac nat_less_cases 1 THEN assume_tac 2);
   1.513 @@ -609,7 +609,7 @@
   1.514  
   1.515  (*** Subtraction laws -- mostly from Clemens Ballarin ***)
   1.516  
   1.517 -goal thy "!! a b c::nat. [| a < b; c <= a |] ==> a-c < b-c";
   1.518 +Goal "!! a b c::nat. [| a < b; c <= a |] ==> a-c < b-c";
   1.519  by (subgoal_tac "c+(a-c) < c+(b-c)" 1);
   1.520  by (Full_simp_tac 1);
   1.521  by (subgoal_tac "c <= b" 1);
   1.522 @@ -617,29 +617,29 @@
   1.523  by (Asm_simp_tac 1);
   1.524  qed "diff_less_mono";
   1.525  
   1.526 -goal thy "!! a b c::nat. a+b < c ==> a < c-b";
   1.527 +Goal "!! a b c::nat. a+b < c ==> a < c-b";
   1.528  by (dtac diff_less_mono 1);
   1.529  by (rtac le_add2 1);
   1.530  by (Asm_full_simp_tac 1);
   1.531  qed "add_less_imp_less_diff";
   1.532  
   1.533 -goal thy "!! n. n <= m ==> Suc m - n = Suc (m - n)";
   1.534 +Goal "!! n. n <= m ==> Suc m - n = Suc (m - n)";
   1.535  by (asm_full_simp_tac (simpset() addsimps [Suc_diff_n, le_eq_less_Suc]) 1);
   1.536  qed "Suc_diff_le";
   1.537  
   1.538 -goal thy "!! n. Suc i <= n ==> Suc (n - Suc i) = n - i";
   1.539 +Goal "!! n. Suc i <= n ==> Suc (n - Suc i) = n - i";
   1.540  by (asm_full_simp_tac
   1.541      (simpset() addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1);
   1.542  qed "Suc_diff_Suc";
   1.543  
   1.544 -goal thy "!! i::nat. i <= n ==> n - (n - i) = i";
   1.545 +Goal "!! i::nat. i <= n ==> n - (n - i) = i";
   1.546  by (etac rev_mp 1);
   1.547  by (res_inst_tac [("m","n"),("n","i")] diff_induct 1);
   1.548  by (ALLGOALS (asm_simp_tac  (simpset() addsimps [Suc_diff_le])));
   1.549  qed "diff_diff_cancel";
   1.550  Addsimps [diff_diff_cancel];
   1.551  
   1.552 -goal thy "!!k::nat. k <= n ==> m <= n + m - k";
   1.553 +Goal "!!k::nat. k <= n ==> m <= n + m - k";
   1.554  by (etac rev_mp 1);
   1.555  by (res_inst_tac [("m", "k"), ("n", "n")] diff_induct 1);
   1.556  by (Simp_tac 1);
   1.557 @@ -647,7 +647,7 @@
   1.558  by (Simp_tac 1);
   1.559  qed "le_add_diff";
   1.560  
   1.561 -goal Arith.thy "!!i::nat. 0<k ==> j<i --> j+k-i < k";
   1.562 +Goal "!!i::nat. 0<k ==> j<i --> j+k-i < k";
   1.563  by (res_inst_tac [("m","j"),("n","i")] diff_induct 1);
   1.564  by (ALLGOALS Asm_simp_tac);
   1.565  qed_spec_mp "add_diff_less";
   1.566 @@ -657,14 +657,14 @@
   1.567  (** (Anti)Monotonicity of subtraction -- by Stefan Merz **)
   1.568  
   1.569  (* Monotonicity of subtraction in first argument *)
   1.570 -goal thy "!!n::nat. m<=n --> (m-l) <= (n-l)";
   1.571 +Goal "!!n::nat. m<=n --> (m-l) <= (n-l)";
   1.572  by (induct_tac "n" 1);
   1.573  by (Simp_tac 1);
   1.574  by (simp_tac (simpset() addsimps [le_Suc_eq]) 1);
   1.575  by (blast_tac (claset() addIs [diff_le_Suc_diff, le_trans]) 1);
   1.576  qed_spec_mp "diff_le_mono";
   1.577  
   1.578 -goal thy "!!n::nat. m<=n ==> (l-n) <= (l-m)";
   1.579 +Goal "!!n::nat. m<=n ==> (l-n) <= (l-m)";
   1.580  by (induct_tac "l" 1);
   1.581  by (Simp_tac 1);
   1.582  by (case_tac "n <= l" 1);