tidying
authorpaulson
Mon Sep 07 10:40:17 1998 +0200 (1998-09-07)
changeset 54290833486c23ce
parent 5428 5a6c4f666a25
child 5430 4a179dba527a
tidying
src/HOL/Arith.ML
src/HOL/arith_data.ML
     1.1 --- a/src/HOL/Arith.ML	Fri Sep 04 13:24:10 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Mon Sep 07 10:40:17 1998 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4      "0 - n = 0"
     1.5   (fn _ => [induct_tac "n" 1,  ALLGOALS Asm_simp_tac]);
     1.6  
     1.7 -(*Must simplify BEFORE the induction!!  (Else we get a critical pair)
     1.8 +(*Must simplify BEFORE the induction!  (Else we get a critical pair)
     1.9    Suc(m) - Suc(n)   rewrites to   pred(Suc(m) - n)  *)
    1.10  qed_goal "diff_Suc_Suc" thy
    1.11      "Suc(m) - Suc(n) = m - n"
    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 "!!k::nat. (k + m = k + n) = (m=n)";
    1.17 +Goal "(k + m = k + n) = (m=(n::nat))";
    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 "!!k::nat. (m + k = n + k) = (m=n)";
    1.24 +Goal "(m + k = n + k) = (m=(n::nat))";
    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 "!!k::nat. (k + m <= k + n) = (m<=n)";
    1.31 +Goal "(k + m <= k + n) = (m<=(n::nat))";
    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 "!!k::nat. (k + m < k + n) = (m<n)";
    1.38 +Goal "(k + m < k + n) = (m<(n::nat))";
    1.39  by (induct_tac "k" 1);
    1.40  by (Simp_tac 1);
    1.41  by (Asm_simp_tac 1);
    1.42 @@ -110,7 +110,7 @@
    1.43  qed "pred_add_is_0";
    1.44  Addsimps [pred_add_is_0];
    1.45  
    1.46 -(* Could be generalized, eg to "!!n. k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
    1.47 +(* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
    1.48  Goal "0<n ==> m + (n-1) = (m+n)-1";
    1.49  by (exhaust_tac "m" 1);
    1.50  by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
    1.51 @@ -118,7 +118,7 @@
    1.52  qed "add_pred";
    1.53  Addsimps [add_pred];
    1.54  
    1.55 -Goal "!!m::nat. m + n = m ==> n = 0";
    1.56 +Goal "m + n = m ==> n = 0";
    1.57  by (dtac (add_0_right RS ssubst) 1);
    1.58  by (asm_full_simp_tac (simpset() addsimps [add_assoc]
    1.59                                   delsimps [add_0_right]) 1);
    1.60 @@ -150,6 +150,11 @@
    1.61  bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans)));
    1.62  bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
    1.63  
    1.64 +Goal "(m<n) = (? k. n=Suc(m+k))";
    1.65 +by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1);
    1.66 +qed "less_iff_Suc_add";
    1.67 +
    1.68 +
    1.69  (*"i <= j ==> i <= j+m"*)
    1.70  bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans));
    1.71  
    1.72 @@ -169,12 +174,12 @@
    1.73  by (blast_tac (claset() addDs [Suc_lessD]) 1);
    1.74  qed "add_lessD1";
    1.75  
    1.76 -Goal "!!i::nat. ~ (i+j < i)";
    1.77 +Goal "~ (i+j < (i::nat))";
    1.78  by (rtac notI 1);
    1.79  by (etac (add_lessD1 RS less_irrefl) 1);
    1.80  qed "not_add_less1";
    1.81  
    1.82 -Goal "!!i::nat. ~ (j+i < i)";
    1.83 +Goal "~ (j+i < (i::nat))";
    1.84  by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1);
    1.85  qed "not_add_less2";
    1.86  AddIffs [not_add_less1, not_add_less2];
    1.87 @@ -185,20 +190,21 @@
    1.88  by (blast_tac (claset() addDs [Suc_leD]) 1);
    1.89  qed_spec_mp "add_leD1";
    1.90  
    1.91 -Goal "!!n::nat. m+k<=n ==> k<=n";
    1.92 +Goal "m+k<=n ==> k<=(n::nat)";
    1.93  by (full_simp_tac (simpset() addsimps [add_commute]) 1);
    1.94  by (etac add_leD1 1);
    1.95  qed_spec_mp "add_leD2";
    1.96  
    1.97 -Goal "!!n::nat. m+k<=n ==> m<=n & k<=n";
    1.98 +Goal "m+k<=n ==> m<=n & k<=(n::nat)";
    1.99  by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1);
   1.100  bind_thm ("add_leE", result() RS conjE);
   1.101  
   1.102 -Goal "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
   1.103 +(*needs !!k for add_ac to work*)
   1.104 +Goal "!!k:: nat. [| k<l;  m+l = k+n |] ==> m<n";
   1.105  by (safe_tac (claset() addSDs [less_eq_Suc_add]));
   1.106  by (asm_full_simp_tac
   1.107      (simpset() delsimps [add_Suc_right]
   1.108 -                addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1);
   1.109 +               addsimps ([add_Suc_right RS sym, add_left_cancel] @ add_ac)) 1);
   1.110  by (etac subst 1);
   1.111  by (simp_tac (simpset() addsimps [less_add_Suc1]) 1);
   1.112  qed "less_add_eq_less";
   1.113 @@ -207,13 +213,13 @@
   1.114  (*** Monotonicity of Addition ***)
   1.115  
   1.116  (*strict, in 1st argument*)
   1.117 -Goal "!!i j k::nat. i < j ==> i + k < j + k";
   1.118 +Goal "i < j ==> i + k < j + (k::nat)";
   1.119  by (induct_tac "k" 1);
   1.120  by (ALLGOALS Asm_simp_tac);
   1.121  qed "add_less_mono1";
   1.122  
   1.123  (*strict, in both arguments*)
   1.124 -Goal "!!i j k::nat. [|i < j; k < l|] ==> i + k < j + l";
   1.125 +Goal "[|i < j; k < l|] ==> i + k < j + (l::nat)";
   1.126  by (rtac (add_less_mono1 RS less_trans) 1);
   1.127  by (REPEAT (assume_tac 1));
   1.128  by (induct_tac "j" 1);
   1.129 @@ -231,18 +237,16 @@
   1.130  qed "less_mono_imp_le_mono";
   1.131  
   1.132  (*non-strict, in 1st argument*)
   1.133 -Goal "!!i j k::nat. i<=j ==> i + k <= j + k";
   1.134 +Goal "i<=j ==> i + k <= j + (k::nat)";
   1.135  by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1);
   1.136  by (etac add_less_mono1 1);
   1.137  by (assume_tac 1);
   1.138  qed "add_le_mono1";
   1.139  
   1.140  (*non-strict, in both arguments*)
   1.141 -Goal "!!k l::nat. [|i<=j;  k<=l |] ==> i + k <= j + l";
   1.142 +Goal "[|i<=j;  k<=l |] ==> i + k <= j + (l::nat)";
   1.143  by (etac (add_le_mono1 RS le_trans) 1);
   1.144  by (simp_tac (simpset() addsimps [add_commute]) 1);
   1.145 -(*j moves to the end because it is free while k, l are bound*)
   1.146 -by (etac add_le_mono1 1);
   1.147  qed "add_le_mono";
   1.148  
   1.149  
   1.150 @@ -298,7 +302,7 @@
   1.151  qed "mult_is_0";
   1.152  Addsimps [mult_is_0];
   1.153  
   1.154 -Goal "!!m::nat. m <= m*m";
   1.155 +Goal "m <= m*(m::nat)";
   1.156  by (induct_tac "m" 1);
   1.157  by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym])));
   1.158  by (etac (le_add2 RSN (2,le_trans)) 1);
   1.159 @@ -337,13 +341,18 @@
   1.160  by (ALLGOALS Asm_simp_tac);
   1.161  qed "Suc_diff_le";
   1.162  
   1.163 +Goal "n<=(l::nat) --> Suc l - n + m = Suc (l - n + m)";
   1.164 +by (res_inst_tac [("m","n"),("n","l")] diff_induct 1);
   1.165 +by (ALLGOALS Asm_simp_tac);
   1.166 +qed_spec_mp "Suc_diff_add_le";
   1.167 +
   1.168  Goal "m - n < Suc(m)";
   1.169  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.170  by (etac less_SucE 3);
   1.171  by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
   1.172  qed "diff_less_Suc";
   1.173  
   1.174 -Goal "!!m::nat. m - n <= m";
   1.175 +Goal "m - n <= (m::nat)";
   1.176  by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
   1.177  by (ALLGOALS Asm_simp_tac);
   1.178  qed "diff_le_self";
   1.179 @@ -385,33 +394,33 @@
   1.180  by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
   1.181  qed "diff_commute";
   1.182  
   1.183 -Goal "!!i j k:: nat. k<=j --> j<=i --> i - (j - k) = i - j + k";
   1.184 +Goal "k<=j --> j<=i --> i - (j - k) = i - j + (k::nat)";
   1.185  by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
   1.186  by (ALLGOALS Asm_simp_tac);
   1.187  by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_Suc_eq]) 1);
   1.188  qed_spec_mp "diff_diff_right";
   1.189  
   1.190 -Goal "!!i j k:: nat. k<=j --> (i + j) - k = i + (j - k)";
   1.191 +Goal "k <= (j::nat) --> (i + j) - k = i + (j - k)";
   1.192  by (res_inst_tac [("m","j"),("n","k")] diff_induct 1);
   1.193  by (ALLGOALS Asm_simp_tac);
   1.194  qed_spec_mp "diff_add_assoc";
   1.195  
   1.196 -Goal "!!i j k:: nat. k<=j --> (j + i) - k = i + (j - k)";
   1.197 +Goal "k <= (j::nat) --> (j + i) - k = i + (j - k)";
   1.198  by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1);
   1.199  qed_spec_mp "diff_add_assoc2";
   1.200  
   1.201 -Goal "!!n::nat. (n+m) - n = m";
   1.202 +Goal "(n+m) - n = (m::nat)";
   1.203  by (induct_tac "n" 1);
   1.204  by (ALLGOALS Asm_simp_tac);
   1.205  qed "diff_add_inverse";
   1.206  Addsimps [diff_add_inverse];
   1.207  
   1.208 -Goal "!!n::nat.(m+n) - n = m";
   1.209 +Goal "(m+n) - n = (m::nat)";
   1.210  by (simp_tac (simpset() addsimps [diff_add_assoc]) 1);
   1.211  qed "diff_add_inverse2";
   1.212  Addsimps [diff_add_inverse2];
   1.213  
   1.214 -Goal "!!i j k::nat. i<=j ==> (j-i=k) = (j=k+i)";
   1.215 +Goal "i <= (j::nat) ==> (j-i=k) = (j=k+i)";
   1.216  by Safe_tac;
   1.217  by (ALLGOALS Asm_simp_tac);
   1.218  qed "le_imp_diff_is_add";
   1.219 @@ -457,20 +466,20 @@
   1.220  by (REPEAT (ares_tac ([impI,allI]@prems) 1));
   1.221  qed "zero_induct";
   1.222  
   1.223 -Goal "!!k::nat. (k+m) - (k+n) = m - n";
   1.224 +Goal "(k+m) - (k+n) = m - (n::nat)";
   1.225  by (induct_tac "k" 1);
   1.226  by (ALLGOALS Asm_simp_tac);
   1.227  qed "diff_cancel";
   1.228  Addsimps [diff_cancel];
   1.229  
   1.230 -Goal "!!m::nat. (m+k) - (n+k) = m - n";
   1.231 +Goal "(m+k) - (n+k) = m - (n::nat)";
   1.232  val add_commute_k = read_instantiate [("n","k")] add_commute;
   1.233  by (asm_simp_tac (simpset() addsimps ([add_commute_k])) 1);
   1.234  qed "diff_cancel2";
   1.235  Addsimps [diff_cancel2];
   1.236  
   1.237  (*From Clemens Ballarin, proof by lcp*)
   1.238 -Goal "!!n::nat. [| k<=n; n<=m |] ==> (m-k) - (n-k) = m-n";
   1.239 +Goal "[| k<=n; n<=m |] ==> (m-k) - (n-k) = m-(n::nat)";
   1.240  by (REPEAT (etac rev_mp 1));
   1.241  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.242  by (ALLGOALS Asm_simp_tac);
   1.243 @@ -478,7 +487,7 @@
   1.244  by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_Suc_eq]) 1);
   1.245  qed "diff_right_cancel";
   1.246  
   1.247 -Goal "!!n::nat. n - (n+m) = 0";
   1.248 +Goal "n - (n+m) = 0";
   1.249  by (induct_tac "n" 1);
   1.250  by (ALLGOALS Asm_simp_tac);
   1.251  qed "diff_add_0";
   1.252 @@ -501,13 +510,13 @@
   1.253  
   1.254  (*** Monotonicity of Multiplication ***)
   1.255  
   1.256 -Goal "!!i::nat. i<=j ==> i*k<=j*k";
   1.257 +Goal "i <= (j::nat) ==> i*k<=j*k";
   1.258  by (induct_tac "k" 1);
   1.259  by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
   1.260  qed "mult_le_mono1";
   1.261  
   1.262  (*<=monotonicity, BOTH arguments*)
   1.263 -Goal "!!i::nat. [| i<=j; k<=l |] ==> i*k<=j*l";
   1.264 +Goal "[| i <= (j::nat); k <= l |] ==> i*k <= j*l";
   1.265  by (etac (mult_le_mono1 RS le_trans) 1);
   1.266  by (rtac le_trans 1);
   1.267  by (stac mult_commute 2);
   1.268 @@ -516,14 +525,14 @@
   1.269  qed "mult_le_mono";
   1.270  
   1.271  (*strict, in 1st argument; proof is by induction on k>0*)
   1.272 -Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
   1.273 +Goal "[| i<j; 0<k |] ==> k*i < k*j";
   1.274  by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1);
   1.275  by (Asm_simp_tac 1);
   1.276  by (induct_tac "x" 1);
   1.277  by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));
   1.278  qed "mult_less_mono2";
   1.279  
   1.280 -Goal "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
   1.281 +Goal "[| i<j; 0<k |] ==> i*k < j*k";
   1.282  by (dtac mult_less_mono2 1);
   1.283  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
   1.284  qed "mult_less_mono1";
   1.285 @@ -599,7 +608,7 @@
   1.286  
   1.287  (*** Subtraction laws -- mostly from Clemens Ballarin ***)
   1.288  
   1.289 -Goal "!! a b c::nat. [| a < b; c <= a |] ==> a-c < b-c";
   1.290 +Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
   1.291  by (subgoal_tac "c+(a-c) < c+(b-c)" 1);
   1.292  by (Full_simp_tac 1);
   1.293  by (subgoal_tac "c <= b" 1);
   1.294 @@ -607,7 +616,7 @@
   1.295  by (Asm_simp_tac 1);
   1.296  qed "diff_less_mono";
   1.297  
   1.298 -Goal "!! a b c::nat. a+b < c ==> a < c-b";
   1.299 +Goal "a+b < (c::nat) ==> a < c-b";
   1.300  by (dtac diff_less_mono 1);
   1.301  by (rtac le_add2 1);
   1.302  by (Asm_full_simp_tac 1);
   1.303 @@ -628,14 +637,14 @@
   1.304  by (asm_simp_tac (simpset() addsimps [Suc_diff_le RS sym]) 1);
   1.305  qed "Suc_diff_Suc";
   1.306  
   1.307 -Goal "!! i::nat. i <= n ==> n - (n - i) = i";
   1.308 +Goal "i <= (n::nat) ==> n - (n - i) = i";
   1.309  by (etac rev_mp 1);
   1.310  by (res_inst_tac [("m","n"),("n","i")] diff_induct 1);
   1.311  by (ALLGOALS (asm_simp_tac  (simpset() addsimps [Suc_diff_le])));
   1.312  qed "diff_diff_cancel";
   1.313  Addsimps [diff_diff_cancel];
   1.314  
   1.315 -Goal "!!k::nat. k <= n ==> m <= n + m - k";
   1.316 +Goal "k <= (n::nat) ==> m <= n + m - k";
   1.317  by (etac rev_mp 1);
   1.318  by (res_inst_tac [("m", "k"), ("n", "n")] diff_induct 1);
   1.319  by (Simp_tac 1);
   1.320 @@ -643,7 +652,7 @@
   1.321  by (Simp_tac 1);
   1.322  qed "le_add_diff";
   1.323  
   1.324 -Goal "!!i::nat. 0<k ==> j<i --> j+k-i < k";
   1.325 +Goal "0<k ==> j<i --> j+k-i < k";
   1.326  by (res_inst_tac [("m","j"),("n","i")] diff_induct 1);
   1.327  by (ALLGOALS Asm_simp_tac);
   1.328  qed_spec_mp "add_diff_less";
   1.329 @@ -701,14 +710,14 @@
   1.330  (** (Anti)Monotonicity of subtraction -- by Stefan Merz **)
   1.331  
   1.332  (* Monotonicity of subtraction in first argument *)
   1.333 -Goal "!!n::nat. m<=n --> (m-l) <= (n-l)";
   1.334 +Goal "m <= (n::nat) --> (m-l) <= (n-l)";
   1.335  by (induct_tac "n" 1);
   1.336  by (Simp_tac 1);
   1.337  by (simp_tac (simpset() addsimps [le_Suc_eq]) 1);
   1.338  by (blast_tac (claset() addIs [diff_le_Suc_diff, le_trans]) 1);
   1.339  qed_spec_mp "diff_le_mono";
   1.340  
   1.341 -Goal "!!n::nat. m<=n ==> (l-n) <= (l-m)";
   1.342 +Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
   1.343  by (induct_tac "l" 1);
   1.344  by (Simp_tac 1);
   1.345  by (case_tac "n <= na" 1);
     2.1 --- a/src/HOL/arith_data.ML	Fri Sep 04 13:24:10 1998 +0200
     2.2 +++ b/src/HOL/arith_data.ML	Mon Sep 07 10:40:17 1998 +0200
     2.3 @@ -222,13 +222,13 @@
     2.4  
     2.5  
     2.6  (*This proof requires natdiff_cancel_sums*)
     2.7 -goal Arith.thy "!!n::nat. m<n --> m<l --> (l-n) < (l-m)";
     2.8 +Goal "m < (n::nat) --> m<l --> (l-n) < (l-m)";
     2.9  by (induct_tac "l" 1);
    2.10  by (Simp_tac 1);
    2.11  by (Clarify_tac 1);
    2.12  by (etac less_SucE 1);
    2.13 +by (Clarify_tac 2);
    2.14 +by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 2);
    2.15  by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
    2.16  				      Suc_diff_le]) 1);
    2.17 -by (Clarify_tac 1);
    2.18 -by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 1);
    2.19  qed_spec_mp "diff_less_mono2";