Tidying and a couple of useful lemmas
authorpaulson
Mon May 26 12:36:16 1997 +0200 (1997-05-26)
changeset 3339cfa72a70f2b5
parent 3338 b99d750f6a37
child 3340 a886795c9dce
Tidying and a couple of useful lemmas
src/HOL/Arith.ML
     1.1 --- a/src/HOL/Arith.ML	Mon May 26 12:34:54 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Mon May 26 12:36:16 1997 +0200
     1.3 @@ -34,49 +34,37 @@
     1.4  
     1.5  qed_goalw "diff_0_eq_0" Arith.thy [pred_def]
     1.6      "0 - n = 0"
     1.7 - (fn _ => [nat_ind_tac "n" 1,  ALLGOALS Asm_simp_tac]);
     1.8 + (fn _ => [induct_tac "n" 1,  ALLGOALS Asm_simp_tac]);
     1.9  
    1.10  (*Must simplify BEFORE the induction!!  (Else we get a critical pair)
    1.11    Suc(m) - Suc(n)   rewrites to   pred(Suc(m) - n)  *)
    1.12  qed_goalw "diff_Suc_Suc" Arith.thy [pred_def]
    1.13      "Suc(m) - Suc(n) = m - n"
    1.14   (fn _ =>
    1.15 -  [Simp_tac 1, nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
    1.16 +  [Simp_tac 1, induct_tac "n" 1, ALLGOALS Asm_simp_tac]);
    1.17  
    1.18  Addsimps [diff_0_eq_0, diff_Suc_Suc];
    1.19  
    1.20  
    1.21 -goal Arith.thy "!!k. 0<k ==> EX j. k = Suc(j)";
    1.22 -by (etac rev_mp 1);
    1.23 -by (nat_ind_tac "k" 1);
    1.24 -by (Simp_tac 1);
    1.25 -by (Blast_tac 1);
    1.26 -val lemma = result();
    1.27 -
    1.28 -(* [| 0 < k; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
    1.29 -bind_thm ("zero_less_natE", lemma RS exE);
    1.30 -
    1.31 -
    1.32 -
    1.33  (**** Inductive properties of the operators ****)
    1.34  
    1.35  (*** Addition ***)
    1.36  
    1.37  qed_goal "add_0_right" Arith.thy "m + 0 = m"
    1.38 - (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
    1.39 + (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
    1.40  
    1.41  qed_goal "add_Suc_right" Arith.thy "m + Suc(n) = Suc(m+n)"
    1.42 - (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
    1.43 + (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
    1.44  
    1.45  Addsimps [add_0_right,add_Suc_right];
    1.46  
    1.47  (*Associative law for addition*)
    1.48  qed_goal "add_assoc" Arith.thy "(m + n) + k = m + ((n + k)::nat)"
    1.49 - (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
    1.50 + (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
    1.51  
    1.52  (*Commutative law for addition*)  
    1.53  qed_goal "add_commute" Arith.thy "m + n = n + (m::nat)"
    1.54 - (fn _ =>  [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
    1.55 + (fn _ =>  [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
    1.56  
    1.57  qed_goal "add_left_commute" Arith.thy "x+(y+z)=y+((x+z)::nat)"
    1.58   (fn _ => [rtac (add_commute RS trans) 1, rtac (add_assoc RS trans) 1,
    1.59 @@ -86,25 +74,25 @@
    1.60  val add_ac = [add_assoc, add_commute, add_left_commute];
    1.61  
    1.62  goal Arith.thy "!!k::nat. (k + m = k + n) = (m=n)";
    1.63 -by (nat_ind_tac "k" 1);
    1.64 +by (induct_tac "k" 1);
    1.65  by (Simp_tac 1);
    1.66  by (Asm_simp_tac 1);
    1.67  qed "add_left_cancel";
    1.68  
    1.69  goal Arith.thy "!!k::nat. (m + k = n + k) = (m=n)";
    1.70 -by (nat_ind_tac "k" 1);
    1.71 +by (induct_tac "k" 1);
    1.72  by (Simp_tac 1);
    1.73  by (Asm_simp_tac 1);
    1.74  qed "add_right_cancel";
    1.75  
    1.76  goal Arith.thy "!!k::nat. (k + m <= k + n) = (m<=n)";
    1.77 -by (nat_ind_tac "k" 1);
    1.78 +by (induct_tac "k" 1);
    1.79  by (Simp_tac 1);
    1.80  by (Asm_simp_tac 1);
    1.81  qed "add_left_cancel_le";
    1.82  
    1.83  goal Arith.thy "!!k::nat. (k + m < k + n) = (m<n)";
    1.84 -by (nat_ind_tac "k" 1);
    1.85 +by (induct_tac "k" 1);
    1.86  by (Simp_tac 1);
    1.87  by (Asm_simp_tac 1);
    1.88  qed "add_left_cancel_less";
    1.89 @@ -112,20 +100,22 @@
    1.90  Addsimps [add_left_cancel, add_right_cancel,
    1.91            add_left_cancel_le, add_left_cancel_less];
    1.92  
    1.93 +(** Reasoning about m+0=0, etc. **)
    1.94 +
    1.95  goal Arith.thy "(m+n = 0) = (m=0 & n=0)";
    1.96 -by (nat_ind_tac "m" 1);
    1.97 +by (induct_tac "m" 1);
    1.98  by (ALLGOALS Asm_simp_tac);
    1.99  qed "add_is_0";
   1.100  Addsimps [add_is_0];
   1.101  
   1.102  goal Arith.thy "(pred (m+n) = 0) = (m=0 & pred n = 0 | pred m = 0 & n=0)";
   1.103 -by (nat_ind_tac "m" 1);
   1.104 +by (induct_tac "m" 1);
   1.105  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.106  qed "pred_add_is_0";
   1.107  Addsimps [pred_add_is_0];
   1.108  
   1.109  goal Arith.thy "!!n. n ~= 0 ==> m + pred n = pred(m+n)";
   1.110 -by (nat_ind_tac "m" 1);
   1.111 +by (induct_tac "m" 1);
   1.112  by (ALLGOALS Asm_simp_tac);
   1.113  qed "add_pred";
   1.114  Addsimps [add_pred];
   1.115 @@ -133,21 +123,25 @@
   1.116  
   1.117  (**** Additional theorems about "less than" ****)
   1.118  
   1.119 -goal Arith.thy "? k::nat. n = n+k";
   1.120 -by (res_inst_tac [("x","0")] exI 1);
   1.121 +goal Arith.thy "i<j --> (EX k. j = Suc(i+k))";
   1.122 +by (induct_tac "j" 1);
   1.123  by (Simp_tac 1);
   1.124 +by (blast_tac (!claset addSEs [less_SucE] 
   1.125 +                       addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
   1.126  val lemma = result();
   1.127  
   1.128 +(* [| i<j;  !!x. j = Suc(i+x) ==> Q |] ==> Q *)
   1.129 +bind_thm ("less_natE", lemma RS mp RS exE);
   1.130 +
   1.131  goal Arith.thy "!!m. m<n --> (? k. n=Suc(m+k))";
   1.132 -by (nat_ind_tac "n" 1);
   1.133 +by (induct_tac "n" 1);
   1.134  by (ALLGOALS (simp_tac (!simpset addsimps [less_Suc_eq])));
   1.135 -by (step_tac (!claset addSIs [lemma]) 1);
   1.136 -by (res_inst_tac [("x","Suc(k)")] exI 1);
   1.137 -by (Simp_tac 1);
   1.138 +by (blast_tac (!claset addSEs [less_SucE] 
   1.139 +                       addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
   1.140  qed_spec_mp "less_eq_Suc_add";
   1.141  
   1.142  goal Arith.thy "n <= ((m + n)::nat)";
   1.143 -by (nat_ind_tac "m" 1);
   1.144 +by (induct_tac "m" 1);
   1.145  by (ALLGOALS Simp_tac);
   1.146  by (etac le_trans 1);
   1.147  by (rtac (lessI RS less_imp_le) 1);
   1.148 @@ -175,7 +169,7 @@
   1.149  
   1.150  goal Arith.thy "!!i. i+j < (k::nat) ==> i<k";
   1.151  by (etac rev_mp 1);
   1.152 -by (nat_ind_tac "j" 1);
   1.153 +by (induct_tac "j" 1);
   1.154  by (ALLGOALS Asm_simp_tac);
   1.155  by (blast_tac (!claset addDs [Suc_lessD]) 1);
   1.156  qed "add_lessD1";
   1.157 @@ -201,7 +195,7 @@
   1.158  qed "less_imp_add_less";
   1.159  
   1.160  goal Arith.thy "m+k<=n --> m<=(n::nat)";
   1.161 -by (nat_ind_tac "k" 1);
   1.162 +by (induct_tac "k" 1);
   1.163  by (ALLGOALS Asm_simp_tac);
   1.164  by (blast_tac (!claset addDs [Suc_leD]) 1);
   1.165  qed_spec_mp "add_leD1";
   1.166 @@ -229,7 +223,7 @@
   1.167  
   1.168  (*strict, in 1st argument*)
   1.169  goal Arith.thy "!!i j k::nat. i < j ==> i + k < j + k";
   1.170 -by (nat_ind_tac "k" 1);
   1.171 +by (induct_tac "k" 1);
   1.172  by (ALLGOALS Asm_simp_tac);
   1.173  qed "add_less_mono1";
   1.174  
   1.175 @@ -237,7 +231,7 @@
   1.176  goal Arith.thy "!!i j k::nat. [|i < j; k < l|] ==> i + k < j + l";
   1.177  by (rtac (add_less_mono1 RS less_trans) 1);
   1.178  by (REPEAT (assume_tac 1));
   1.179 -by (nat_ind_tac "j" 1);
   1.180 +by (induct_tac "j" 1);
   1.181  by (ALLGOALS Asm_simp_tac);
   1.182  qed "add_less_mono";
   1.183  
   1.184 @@ -271,11 +265,11 @@
   1.185  
   1.186  (*right annihilation in product*)
   1.187  qed_goal "mult_0_right" Arith.thy "m * 0 = 0"
   1.188 - (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
   1.189 + (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
   1.190  
   1.191  (*right successor law for multiplication*)
   1.192  qed_goal "mult_Suc_right" Arith.thy  "m * Suc(n) = m + (m * n)"
   1.193 - (fn _ => [nat_ind_tac "m" 1,
   1.194 + (fn _ => [induct_tac "m" 1,
   1.195             ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
   1.196  
   1.197  Addsimps [mult_0_right, mult_Suc_right];
   1.198 @@ -290,20 +284,20 @@
   1.199  
   1.200  (*Commutative law for multiplication*)
   1.201  qed_goal "mult_commute" Arith.thy "m * n = n * (m::nat)"
   1.202 - (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
   1.203 + (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
   1.204  
   1.205  (*addition distributes over multiplication*)
   1.206  qed_goal "add_mult_distrib" Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)"
   1.207 - (fn _ => [nat_ind_tac "m" 1,
   1.208 + (fn _ => [induct_tac "m" 1,
   1.209             ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
   1.210  
   1.211  qed_goal "add_mult_distrib2" Arith.thy "k*(m + n) = (k*m) + ((k*n)::nat)"
   1.212 - (fn _ => [nat_ind_tac "m" 1,
   1.213 + (fn _ => [induct_tac "m" 1,
   1.214             ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
   1.215  
   1.216  (*Associative law for multiplication*)
   1.217  qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)"
   1.218 -  (fn _ => [nat_ind_tac "m" 1, 
   1.219 +  (fn _ => [induct_tac "m" 1, 
   1.220              ALLGOALS (asm_simp_tac (!simpset addsimps [add_mult_distrib]))]);
   1.221  
   1.222  qed_goal "mult_left_commute" Arith.thy "x*(y*z) = y*((x*z)::nat)"
   1.223 @@ -313,8 +307,8 @@
   1.224  val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
   1.225  
   1.226  goal Arith.thy "(m*n = 0) = (m=0 | n=0)";
   1.227 -by (nat_ind_tac "m" 1);
   1.228 -by (nat_ind_tac "n" 2);
   1.229 +by (induct_tac "m" 1);
   1.230 +by (induct_tac "n" 2);
   1.231  by (ALLGOALS Asm_simp_tac);
   1.232  qed "mult_is_0";
   1.233  Addsimps [mult_is_0];
   1.234 @@ -323,11 +317,11 @@
   1.235  (*** Difference ***)
   1.236  
   1.237  qed_goal "pred_Suc_diff" Arith.thy "pred(Suc m - n) = m - n"
   1.238 - (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
   1.239 + (fn _ => [induct_tac "n" 1, ALLGOALS Asm_simp_tac]);
   1.240  Addsimps [pred_Suc_diff];
   1.241  
   1.242  qed_goal "diff_self_eq_0" Arith.thy "m - m = 0"
   1.243 - (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
   1.244 + (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
   1.245  Addsimps [diff_self_eq_0];
   1.246  
   1.247  (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
   1.248 @@ -354,7 +348,7 @@
   1.249  qed "diff_le_self";
   1.250  
   1.251  goal Arith.thy "!!n::nat. (n+m) - n = m";
   1.252 -by (nat_ind_tac "n" 1);
   1.253 +by (induct_tac "n" 1);
   1.254  by (ALLGOALS Asm_simp_tac);
   1.255  qed "diff_add_inverse";
   1.256  Addsimps [diff_add_inverse];
   1.257 @@ -406,7 +400,7 @@
   1.258  qed "zero_induct";
   1.259  
   1.260  goal Arith.thy "!!k::nat. (k+m) - (k+n) = m - n";
   1.261 -by (nat_ind_tac "k" 1);
   1.262 +by (induct_tac "k" 1);
   1.263  by (ALLGOALS Asm_simp_tac);
   1.264  qed "diff_cancel";
   1.265  Addsimps [diff_cancel];
   1.266 @@ -421,7 +415,7 @@
   1.267  goal Arith.thy "!!n::nat. [| k<=n; n<=m |] ==> (m-k) - (n-k) = m-n";
   1.268  by (subgoal_tac "k<=n --> n<=m --> (m-k) - (n-k) = m-n" 1);
   1.269  by (Asm_full_simp_tac 1);
   1.270 -by (nat_ind_tac "k" 1);
   1.271 +by (induct_tac "k" 1);
   1.272  by (Simp_tac 1);
   1.273  (* Induction step *)
   1.274  by (subgoal_tac "Suc na <= m --> n <= m --> Suc na <= n --> \
   1.275 @@ -434,7 +428,7 @@
   1.276  qed "diff_right_cancel";
   1.277  
   1.278  goal Arith.thy "!!n::nat. n - (n+m) = 0";
   1.279 -by (nat_ind_tac "n" 1);
   1.280 +by (induct_tac "n" 1);
   1.281  by (ALLGOALS Asm_simp_tac);
   1.282  qed "diff_add_0";
   1.283  Addsimps [diff_add_0];
   1.284 @@ -500,7 +494,7 @@
   1.285  qed "mod_eq_add";
   1.286  
   1.287  goal thy "!!n. 0<n ==> m*n mod n = 0";
   1.288 -by (nat_ind_tac "m" 1);
   1.289 +by (induct_tac "m" 1);
   1.290  by (asm_simp_tac (!simpset addsimps [mod_less]) 1);
   1.291  by (dres_inst_tac [("m","m*n")] mod_eq_add 1);
   1.292  by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1);
   1.293 @@ -592,7 +586,7 @@
   1.294  qed "mod2_neq_0";
   1.295  
   1.296  goal thy "(m+m) mod 2 = 0";
   1.297 -by (nat_ind_tac "m" 1);
   1.298 +by (induct_tac "m" 1);
   1.299  by (simp_tac (!simpset addsimps [mod_less]) 1);
   1.300  by (asm_simp_tac (!simpset addsimps [mod2_Suc_Suc, add_Suc_right]) 1);
   1.301  qed "mod2_add_self";
   1.302 @@ -604,7 +598,7 @@
   1.303  (*** Monotonicity of Multiplication ***)
   1.304  
   1.305  goal Arith.thy "!!i::nat. i<=j ==> i*k<=j*k";
   1.306 -by (nat_ind_tac "k" 1);
   1.307 +by (induct_tac "k" 1);
   1.308  by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_le_mono])));
   1.309  qed "mult_le_mono1";
   1.310  
   1.311 @@ -619,9 +613,9 @@
   1.312  
   1.313  (*strict, in 1st argument; proof is by induction on k>0*)
   1.314  goal Arith.thy "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
   1.315 -by (etac zero_less_natE 1);
   1.316 +by (eres_inst_tac [("i","0")] less_natE 1);
   1.317  by (Asm_simp_tac 1);
   1.318 -by (nat_ind_tac "x" 1);
   1.319 +by (induct_tac "x" 1);
   1.320  by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_less_mono])));
   1.321  qed "mult_less_mono2";
   1.322  
   1.323 @@ -631,15 +625,15 @@
   1.324  qed "mult_less_mono1";
   1.325  
   1.326  goal Arith.thy "(0 < m*n) = (0<m & 0<n)";
   1.327 -by (nat_ind_tac "m" 1);
   1.328 -by (nat_ind_tac "n" 2);
   1.329 +by (induct_tac "m" 1);
   1.330 +by (induct_tac "n" 2);
   1.331  by (ALLGOALS Asm_simp_tac);
   1.332  qed "zero_less_mult_iff";
   1.333  
   1.334  goal Arith.thy "(m*n = 1) = (m=1 & n=1)";
   1.335 -by (nat_ind_tac "m" 1);
   1.336 +by (induct_tac "m" 1);
   1.337  by (Simp_tac 1);
   1.338 -by (nat_ind_tac "n" 1);
   1.339 +by (induct_tac "n" 1);
   1.340  by (Simp_tac 1);
   1.341  by (fast_tac (!claset addss !simpset) 1);
   1.342  qed "mult_eq_1_iff";