src/HOL/Arith.ML
changeset 3366 2402c6ab1561
parent 3352 04502e5431fb
child 3381 2bac33ec2b0d
     1.1 --- a/src/HOL/Arith.ML	Fri May 30 15:14:59 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Fri May 30 15:15:57 1997 +0200
     1.3 @@ -388,6 +388,13 @@
     1.4  qed "diff_add_inverse2";
     1.5  Addsimps [diff_add_inverse2];
     1.6  
     1.7 +goal Arith.thy "!!i j k::nat. i<=j ==> (j-i=k) = (j=k+i)";
     1.8 +by (Step_tac 1);
     1.9 +by (ALLGOALS 
    1.10 +    (asm_simp_tac
    1.11 +     (!simpset addsimps [add_diff_inverse, not_less_iff_le, add_commute])));
    1.12 +qed "le_imp_diff_is_add";
    1.13 +
    1.14  val [prem] = goal Arith.thy "m < Suc(n) ==> m-n = 0";
    1.15  by (rtac (prem RS rev_mp) 1);
    1.16  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.17 @@ -470,154 +477,6 @@
    1.18  (*NOT added as rewrites, since sometimes they are used from right-to-left*)
    1.19  
    1.20  
    1.21 -(** Less-then properties **)
    1.22 -
    1.23 -(*In ordinary notation: if 0<n and n<=m then m-n < m *)
    1.24 -goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m";
    1.25 -by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
    1.26 -by (Blast_tac 1);
    1.27 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.28 -by (ALLGOALS(asm_simp_tac(!simpset addsimps [diff_less_Suc])));
    1.29 -qed "diff_less";
    1.30 -
    1.31 -val wf_less_trans = [eq_reflection, wf_pred_nat RS wf_trancl] MRS 
    1.32 -                    def_wfrec RS trans;
    1.33 -
    1.34 -goalw Nat.thy [less_def] "(m,n) : pred_nat^+ = (m<n)";
    1.35 -by (rtac refl 1);
    1.36 -qed "less_eq";
    1.37 -
    1.38 -(*** Remainder ***)
    1.39 -
    1.40 -goal Arith.thy "(%m. m mod n) = wfrec (trancl pred_nat) \
    1.41 -             \                      (%f j. if j<n then j else f (j-n))";
    1.42 -by (simp_tac (!simpset addsimps [mod_def]) 1);
    1.43 -qed "mod_eq";
    1.44 -
    1.45 -goal Arith.thy "!!m. m<n ==> m mod n = m";
    1.46 -by (rtac (mod_eq RS wf_less_trans) 1);
    1.47 -by (Asm_simp_tac 1);
    1.48 -qed "mod_less";
    1.49 -
    1.50 -goal Arith.thy "!!m. [| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n";
    1.51 -by (rtac (mod_eq RS wf_less_trans) 1);
    1.52 -by (asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
    1.53 -qed "mod_geq";
    1.54 -
    1.55 -goal thy "!!n. 0<n ==> n mod n = 0";
    1.56 -by (rtac (mod_eq RS wf_less_trans) 1);
    1.57 -by (asm_simp_tac (!simpset addsimps [mod_less, diff_self_eq_0,
    1.58 -				     cut_def, less_eq]) 1);
    1.59 -qed "mod_nn_is_0";
    1.60 -
    1.61 -goal thy "!!n. 0<n ==> (m+n) mod n = m mod n";
    1.62 -by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1);
    1.63 -by (stac (mod_geq RS sym) 2);
    1.64 -by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [add_commute])));
    1.65 -qed "mod_eq_add";
    1.66 -
    1.67 -goal thy "!!n. 0<n ==> m*n mod n = 0";
    1.68 -by (induct_tac "m" 1);
    1.69 -by (asm_simp_tac (!simpset addsimps [mod_less]) 1);
    1.70 -by (dres_inst_tac [("m","m*n")] mod_eq_add 1);
    1.71 -by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1);
    1.72 -qed "mod_prod_nn_is_0";
    1.73 -
    1.74 -
    1.75 -(*** Quotient ***)
    1.76 -
    1.77 -goal Arith.thy "(%m. m div n) = wfrec (trancl pred_nat) \
    1.78 -                        \            (%f j. if j<n then 0 else Suc (f (j-n)))";
    1.79 -by (simp_tac (!simpset addsimps [div_def]) 1);
    1.80 -qed "div_eq";
    1.81 -
    1.82 -goal Arith.thy "!!m. m<n ==> m div n = 0";
    1.83 -by (rtac (div_eq RS wf_less_trans) 1);
    1.84 -by (Asm_simp_tac 1);
    1.85 -qed "div_less";
    1.86 -
    1.87 -goal Arith.thy "!!M. [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
    1.88 -by (rtac (div_eq RS wf_less_trans) 1);
    1.89 -by (asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
    1.90 -qed "div_geq";
    1.91 -
    1.92 -(*Main Result about quotient and remainder.*)
    1.93 -goal Arith.thy "!!m. 0<n ==> (m div n)*n + m mod n = m";
    1.94 -by (res_inst_tac [("n","m")] less_induct 1);
    1.95 -by (rename_tac "k" 1);    (*Variable name used in line below*)
    1.96 -by (case_tac "k<n" 1);
    1.97 -by (ALLGOALS (asm_simp_tac(!simpset addsimps ([add_assoc] @
    1.98 -                       [mod_less, mod_geq, div_less, div_geq,
    1.99 -                        add_diff_inverse, diff_less]))));
   1.100 -qed "mod_div_equality";
   1.101 -
   1.102 -
   1.103 -(*** Further facts about mod (mainly for the mutilated chess board ***)
   1.104 -
   1.105 -goal Arith.thy
   1.106 -    "!!m n. 0<n ==> \
   1.107 -\           Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
   1.108 -by (res_inst_tac [("n","m")] less_induct 1);
   1.109 -by (excluded_middle_tac "Suc(na)<n" 1);
   1.110 -(* case Suc(na) < n *)
   1.111 -by (forward_tac [lessI RS less_trans] 2);
   1.112 -by (asm_simp_tac (!simpset addsimps [mod_less, less_not_refl2 RS not_sym]) 2);
   1.113 -(* case n <= Suc(na) *)
   1.114 -by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, mod_geq]) 1);
   1.115 -by (etac (le_imp_less_or_eq RS disjE) 1);
   1.116 -by (asm_simp_tac (!simpset addsimps [Suc_diff_n]) 1);
   1.117 -by (asm_full_simp_tac (!simpset addsimps [not_less_eq RS sym, 
   1.118 -                                          diff_less, mod_geq]) 1);
   1.119 -by (asm_simp_tac (!simpset addsimps [mod_less]) 1);
   1.120 -qed "mod_Suc";
   1.121 -
   1.122 -goal Arith.thy "!!m n. 0<n ==> m mod n < n";
   1.123 -by (res_inst_tac [("n","m")] less_induct 1);
   1.124 -by (excluded_middle_tac "na<n" 1);
   1.125 -(*case na<n*)
   1.126 -by (asm_simp_tac (!simpset addsimps [mod_less]) 2);
   1.127 -(*case n le na*)
   1.128 -by (asm_full_simp_tac (!simpset addsimps [mod_geq, diff_less]) 1);
   1.129 -qed "mod_less_divisor";
   1.130 -
   1.131 -
   1.132 -(** Evens and Odds **)
   1.133 -
   1.134 -(*With less_zeroE, causes case analysis on b<2*)
   1.135 -AddSEs [less_SucE];
   1.136 -
   1.137 -goal thy "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
   1.138 -by (subgoal_tac "k mod 2 < 2" 1);
   1.139 -by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
   1.140 -by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   1.141 -by (Blast_tac 1);
   1.142 -qed "mod2_cases";
   1.143 -
   1.144 -goal thy "Suc(Suc(m)) mod 2 = m mod 2";
   1.145 -by (subgoal_tac "m mod 2 < 2" 1);
   1.146 -by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
   1.147 -by (Step_tac 1);
   1.148 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [mod_Suc])));
   1.149 -qed "mod2_Suc_Suc";
   1.150 -Addsimps [mod2_Suc_Suc];
   1.151 -
   1.152 -goal Arith.thy "!!m. m mod 2 ~= 0 ==> m mod 2 = 1";
   1.153 -by (subgoal_tac "m mod 2 < 2" 1);
   1.154 -by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
   1.155 -by (safe_tac (!claset addSEs [lessE]));
   1.156 -by (ALLGOALS (blast_tac (!claset addIs [sym])));
   1.157 -qed "mod2_neq_0";
   1.158 -
   1.159 -goal thy "(m+m) mod 2 = 0";
   1.160 -by (induct_tac "m" 1);
   1.161 -by (simp_tac (!simpset addsimps [mod_less]) 1);
   1.162 -by (asm_simp_tac (!simpset addsimps [mod2_Suc_Suc, add_Suc_right]) 1);
   1.163 -qed "mod2_add_self";
   1.164 -Addsimps [mod2_add_self];
   1.165 -
   1.166 -Delrules [less_SucE];
   1.167 -
   1.168 -
   1.169  (*** Monotonicity of Multiplication ***)
   1.170  
   1.171  goal Arith.thy "!!i::nat. i<=j ==> i*k<=j*k";
   1.172 @@ -688,44 +547,6 @@
   1.173  Addsimps [mult_cancel1, mult_cancel2];
   1.174  
   1.175  
   1.176 -(*** More division laws ***)
   1.177 -
   1.178 -goal thy "!!n. 0<n ==> m*n div n = m";
   1.179 -by (cut_inst_tac [("m", "m*n")] mod_div_equality 1);
   1.180 -ba 1;
   1.181 -by (asm_full_simp_tac (!simpset addsimps [mod_prod_nn_is_0]) 1);
   1.182 -qed "div_prod_nn_is_m";
   1.183 -Addsimps [div_prod_nn_is_m];
   1.184 -
   1.185 -(*Cancellation law for division*)
   1.186 -goal Arith.thy "!!k. [| 0<n; 0<k |] ==> (k*m) div (k*n) = m div n";
   1.187 -by (res_inst_tac [("n","m")] less_induct 1);
   1.188 -by (case_tac "na<n" 1);
   1.189 -by (asm_simp_tac (!simpset addsimps [div_less, zero_less_mult_iff, 
   1.190 -                                     mult_less_mono2]) 1);
   1.191 -by (subgoal_tac "~ k*na < k*n" 1);
   1.192 -by (asm_simp_tac
   1.193 -     (!simpset addsimps [zero_less_mult_iff, div_geq,
   1.194 -                         diff_mult_distrib2 RS sym, diff_less]) 1);
   1.195 -by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, 
   1.196 -                                          le_refl RS mult_le_mono]) 1);
   1.197 -qed "div_cancel";
   1.198 -Addsimps [div_cancel];
   1.199 -
   1.200 -goal Arith.thy "!!k. [| 0<n; 0<k |] ==> (k*m) mod (k*n) = k * (m mod n)";
   1.201 -by (res_inst_tac [("n","m")] less_induct 1);
   1.202 -by (case_tac "na<n" 1);
   1.203 -by (asm_simp_tac (!simpset addsimps [mod_less, zero_less_mult_iff, 
   1.204 -                                     mult_less_mono2]) 1);
   1.205 -by (subgoal_tac "~ k*na < k*n" 1);
   1.206 -by (asm_simp_tac
   1.207 -     (!simpset addsimps [zero_less_mult_iff, mod_geq,
   1.208 -                         diff_mult_distrib2 RS sym, diff_less]) 1);
   1.209 -by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, 
   1.210 -                                          le_refl RS mult_le_mono]) 1);
   1.211 -qed "mult_mod_distrib";
   1.212 -
   1.213 -
   1.214  (** Lemma for gcd **)
   1.215  
   1.216  goal Arith.thy "!!m n. m = m*n ==> n=1 | m=0";