author nipkow Fri Aug 23 07:41:05 2002 +0200 (2002-08-23) changeset 13517 42efec18f5b2 parent 13516 13a6103b9ac4 child 13518 a0749ce05100
 src/HOL/Divides.thy file | annotate | diff | revisions src/HOL/Divides_lemmas.ML file | annotate | diff | revisions src/HOL/HoareParallel/OG_Examples.thy file | annotate | diff | revisions src/HOL/HoareParallel/RG_Examples.thy file | annotate | diff | revisions src/HOL/Hyperreal/EvenOdd.ML file | annotate | diff | revisions src/HOL/Integ/IntDiv.thy file | annotate | diff | revisions src/HOL/Integ/IntDiv_setup.ML file | annotate | diff | revisions src/HOL/Integ/nat_bin.ML file | annotate | diff | revisions src/HOL/IsaMakefile file | annotate | diff | revisions src/HOL/NumberTheory/IntPrimes.thy file | annotate | diff | revisions src/HOL/ROOT.ML file | annotate | diff | revisions src/HOL/arith_data.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Divides.thy	Fri Aug 23 07:34:20 2002 +0200
1.2 +++ b/src/HOL/Divides.thy	Fri Aug 23 07:41:05 2002 +0200
1.3 @@ -44,11 +44,6 @@
1.4
1.5  use "Divides_lemmas.ML"
1.6
1.7 -lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
1.8 -apply(insert mod_div_equality[of m n])
1.9 -apply(simp only:mult_ac)
1.10 -done
1.11 -
1.12  lemma split_div:
1.13   "P(n div k :: nat) =
1.14   ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
1.15 @@ -85,7 +80,7 @@
1.16      assume not0: "k \<noteq> 0"
1.17      with Q have R: ?R by simp
1.18      from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
1.19 -    show ?P by(simp add:mod_div_equality2)
1.20 +    show ?P by simp
1.21    qed
1.22  qed
1.23
1.24 @@ -118,7 +113,7 @@
1.25      assume not0: "k \<noteq> 0"
1.26      with Q have R: ?R by simp
1.27      from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
1.28 -    show ?P by(simp add:mod_div_equality2)
1.29 +    show ?P by simp
1.30    qed
1.31  qed
1.32
1.33 @@ -145,7 +140,7 @@
1.34  next
1.35    assume Q: ?Q
1.36    from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
1.37 -  show ?P by(simp add:mod_div_equality2)
1.38 +  show ?P by simp
1.39  qed
1.40
1.41  lemma split_mod:
1.42 @@ -163,7 +158,7 @@
1.43  next
1.44    assume Q: ?Q
1.45    from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
1.46 -  show ?P by(simp add:mod_div_equality2)
1.47 +  show ?P by simp
1.48  qed
1.49  *)
1.50  end
```
```     2.1 --- a/src/HOL/Divides_lemmas.ML	Fri Aug 23 07:34:20 2002 +0200
2.2 +++ b/src/HOL/Divides_lemmas.ML	Fri Aug 23 07:41:05 2002 +0200
2.3 @@ -180,10 +180,55 @@
2.5  qed "mod_div_equality";
2.6
2.7 +Goal "n * (m div n) + m mod n = (m::nat)";
2.8 +by(cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1);
2.9 +by(asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
2.10 +qed "mod_div_equality2";
2.11 +
2.12 +(*-----------------------------------------------------------------------*)
2.13 +(*Simproc for cancelling div and mod                                     *)
2.14 +(*-----------------------------------------------------------------------*)
2.15 +
2.16 +Goal "((m div n)*n + m mod n) + k = (m::nat) + k";
2.17 +by(simp_tac (simpset() addsimps [mod_div_equality]) 1);
2.18 +qed "div_mod_equality";
2.19 +
2.20 +Goal "(n*(m div n) + m mod n) + k = (m::nat) + k";
2.21 +by(simp_tac (simpset() addsimps [thm"mod_div_equality2"]) 1);
2.22 +qed "div_mod_equality2";
2.23 +
2.24 +structure CancelDivModData =
2.25 +struct
2.26 +
2.27 +val div_name = "Divides.op div";
2.28 +val mod_name = "Divides.op mod";
2.29 +val mk_binop = HOLogic.mk_binop;
2.30 +val mk_sum = NatArithUtils.mk_sum;
2.31 +val dest_sum = NatArithUtils.dest_sum;
2.32 +
2.33 +(*logic*)
2.34 +
2.35 +val div_mod_eqs = map mk_meta_eq [div_mod_equality,div_mod_equality2]
2.36 +
2.37 +val trans = trans
2.38 +
2.39 +val prove_eq_sums =
2.41 +  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all simps) end
2.42 +
2.43 +end;
2.44 +
2.45 +structure CancelDivMod = CancelDivModFun(CancelDivModData);
2.46 +
2.47 +val cancel_div_mod_proc = NatArithUtils.prep_simproc
2.48 +      ("cancel_div_mod", ["(m::nat) + n"], CancelDivMod.proc);
2.49 +
2.51 +
2.52 +
2.53  (* a simple rearrangement of mod_div_equality: *)
2.54  Goal "(n::nat) * (m div n) = m - (m mod n)";
2.55 -by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1);
2.56 -by (full_simp_tac (simpset() addsimps mult_ac) 1);
2.57 +by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality2 1);
2.58  by (arith_tac 1);
2.59  qed "mult_div_cancel";
2.60
2.61 @@ -240,7 +285,6 @@
2.62  qed "unique_remainder";
2.63
2.64  Goal "0 < b ==> quorem ((a, b), (a div b, a mod b))";
2.65 -by (cut_inst_tac [("m","a"),("n","b")] mod_div_equality 1);
2.66  by (auto_tac
2.69 @@ -271,7 +315,6 @@
2.70
2.71  Goal "[| quorem((b,c),(q,r));  0 < c |] \
2.72  \     ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))";
2.73 -by (cut_inst_tac [("m", "a*r"), ("n","c")] mod_div_equality 1);
2.74  by (auto_tac
2.75      (claset(),
2.77 @@ -304,7 +347,6 @@
2.78
2.79  Goal "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |] \
2.80  \     ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))";
2.81 -by (cut_inst_tac [("m", "ar+br"), ("n","c")] mod_div_equality 1);
2.82  by (auto_tac
2.83      (claset(),
2.85 @@ -339,7 +381,6 @@
2.86
2.87  Goal "[| quorem ((a,b), (q,r));  0 < b;  0 < c |] \
2.88  \     ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))";
2.89 -by (cut_inst_tac [("m", "q"), ("n","c")] mod_div_equality 1);
2.90  by (auto_tac
2.91      (claset(),
2.93 @@ -357,7 +398,6 @@
2.94  Goal "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)";
2.95  by (div_undefined_case_tac "b=0" 1);
2.96  by (div_undefined_case_tac "c=0" 1);
2.97 -by (cut_inst_tac [("m", "a"), ("n","b")] mod_div_equality 1);
2.98  by (auto_tac (claset(),
2.100  				   quorem_div_mod RS lemma RS quorem_mod]));
2.101 @@ -614,7 +654,7 @@
2.102
2.103  Goal "[| (k::nat) dvd m mod n;  k dvd n |] ==> k dvd m";
2.104  by (subgoal_tac "k dvd (m div n)*n + m mod n" 1);
2.107  by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
2.108  qed "dvd_mod_imp_dvd";
2.109
2.110 @@ -690,7 +730,6 @@
2.111  (*Loses information, namely we also have r<d provided d is nonzero*)
2.112  Goal "(m mod d = r) ==> EX q::nat. m = r + q*d";
2.113  by (cut_inst_tac [("m","m")] mod_div_equality 1);
2.116  by (blast_tac (claset() addIs [sym]) 1);
2.117  qed "mod_eqD";
2.118 -
```
```     3.1 --- a/src/HOL/HoareParallel/OG_Examples.thy	Fri Aug 23 07:34:20 2002 +0200
3.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy	Fri Aug 23 07:41:05 2002 +0200
3.3 @@ -340,44 +340,38 @@
3.4
3.5  subsubsection {* Previous lemmas *}
3.6
3.7 -lemma nat_lemma1: "\<lbrakk>(c::nat) \<le> a ;a < b\<rbrakk> \<Longrightarrow> b - a \<le> b - c"
3.8 -by (simp split: nat_diff_split)
3.9 -
3.10 -lemma nat_lemma2: "\<lbrakk> b = m*(n::nat) + t; a = s*n + t ; b - a < n \<rbrakk> \<Longrightarrow> m - s = 0"
3.11 +lemma nat_lemma2: "\<lbrakk> b = m*(n::nat) + t; a = s*n + u; t=u; b-a < n \<rbrakk> \<Longrightarrow> m \<le> s"
3.12  proof -
3.13 -  assume "b = m*(n::nat) + t" and "a = s*n + t"
3.14 +  assume "b = m*(n::nat) + t" "a = s*n + u" "t=u"
3.15    hence "(m - s) * n = b - a" by (simp add: diff_mult_distrib)
3.16    also assume "\<dots> < n"
3.17    finally have "m - s < 1" by simp
3.18    thus ?thesis by arith
3.19  qed
3.20
3.21 -lemma less_imp_diff_is_0: "m < Suc(n) \<Longrightarrow> m-n = 0"
3.22 -by arith
3.23  lemma mod_lemma: "\<lbrakk> (c::nat) \<le> a; a < b; b - c < n \<rbrakk> \<Longrightarrow> b mod n \<noteq> a mod n"
3.24  apply(subgoal_tac "b=b div n*n + b mod n" )
3.25   prefer 2  apply (simp add: mod_div_equality [symmetric])
3.26  apply(subgoal_tac "a=a div n*n + a mod n")
3.27   prefer 2
3.29 -apply(frule nat_lemma1 , assumption)
3.30 +apply(subgoal_tac "b - a \<le> b - c")
3.31 + prefer 2 apply arith
3.32  apply(drule le_less_trans)
3.33  back
3.34   apply assumption
3.35  apply(frule less_not_refl2)
3.36  apply(drule less_imp_le)
3.37 -apply (drule_tac m = "a" in div_le_mono)
3.38 -apply(drule_tac m = "a div n" in le_imp_less_Suc)
3.39 -apply(drule less_imp_diff_is_0)
3.40 +apply (drule_tac m = "a" and k = n in div_le_mono)
3.41  apply(safe)
3.42 -apply(simp)
3.43 -apply(frule_tac b = "b" and a = "a" and n = "n" in nat_lemma2 , assumption)
3.44 +apply(frule_tac b = "b" and a = "a" and n = "n" in nat_lemma2, assumption, assumption)
3.45  apply assumption
3.46 -apply(drule  diffs0_imp_equal)
3.47 -apply(simp)
3.48 +apply(drule order_antisym, assumption)
3.49 +apply(rotate_tac -3)
3.50  apply(simp)
3.51  done
3.52
3.53 +
3.54  subsubsection {* Producer/Consumer Algorithm *}
3.55
3.56  record Producer_consumer =
```
```     4.1 --- a/src/HOL/HoareParallel/RG_Examples.thy	Fri Aug 23 07:34:20 2002 +0200
4.2 +++ b/src/HOL/HoareParallel/RG_Examples.thy	Fri Aug 23 07:41:05 2002 +0200
4.3 @@ -278,14 +278,14 @@
4.4
4.5  lemma mod_aux :"\<lbrakk>i < (n::nat); a mod n = i;  j < a + n; j mod n = i; a < j\<rbrakk> \<Longrightarrow> False"
4.6  apply(subgoal_tac "a=a div n*n + a mod n" )
4.7 - prefer 2 apply (simp (no_asm_use) only: mod_div_equality [symmetric])
4.8 + prefer 2 apply (simp (no_asm_use))
4.9  apply(subgoal_tac "j=j div n*n + j mod n")
4.10 - prefer 2 apply (simp (no_asm_use) only: mod_div_equality [symmetric])
4.11 + prefer 2 apply (simp (no_asm_use))
4.12  apply simp
4.13  apply(subgoal_tac "a div n*n < j div n*n")
4.14  prefer 2 apply arith
4.15  apply(subgoal_tac "j div n*n < (a div n + 1)*n")
4.16 -prefer 2 apply simp
4.17 +prefer 2 apply simp
4.18  apply (simp only:mult_less_cancel2)
4.19  apply arith
4.20  done
```
```     5.1 --- a/src/HOL/Hyperreal/EvenOdd.ML	Fri Aug 23 07:34:20 2002 +0200
5.2 +++ b/src/HOL/Hyperreal/EvenOdd.ML	Fri Aug 23 07:41:05 2002 +0200
5.3 @@ -253,8 +253,7 @@
5.4  (* Some mod and div stuff *)
5.5
5.6  Goal "n ~= (0::nat) ==> (m = m div n * n + m mod n) & m mod n < n";
5.7 -by (auto_tac (claset() addIs [mod_less_divisor],simpset()
5.9 +by (auto_tac (claset() addIs [mod_less_divisor],simpset()));
5.10  qed "mod_div_eq_less";
5.11
5.12  Goal "(k*n + m) mod n = m mod (n::nat)";
5.13 @@ -273,7 +272,7 @@
5.14  by (etac exE 1);
5.15  by (Asm_simp_tac 1);
5.16  by (res_inst_tac [("t","m"),("n1","n")] (mod_div_equality RS subst) 1);
5.17 -by Auto_tac;
5.18 +by (auto_tac (claset(),simpset() delsimprocs [cancel_div_mod_proc]));
5.19  qed "mod_Suc_eq_Suc_mod";
5.20
5.21  Goal "even n = (even (n mod 4))";
5.22 @@ -281,7 +280,7 @@
5.23  by (etac exE 1);
5.24  by (Asm_simp_tac 1);
5.25  by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
5.26 -by (auto_tac (claset(),simpset() addsimps [even_mult,even_num_iff]));
5.27 +by (auto_tac (claset(),simpset() addsimps [even_mult,even_num_iff] delsimprocs [cancel_div_mod_proc]));
5.28  qed "even_even_mod_4_iff";
5.29
5.30  Goal "odd n = (odd (n mod 4))";
5.31 @@ -309,17 +308,17 @@
5.32
5.33  Goal "n mod 4 = 1 ==> odd(n)";
5.34  by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
5.35 -by (auto_tac (claset(),simpset() addsimps [odd_num_iff]));
5.36 +by (auto_tac (claset(),simpset() addsimps [odd_num_iff] delsimprocs [cancel_div_mod_proc]));
5.37  qed "lemma_mod_4_odd_n";
5.38
5.39  Goal "n mod 4 = 2 ==> even(n)";
5.40  by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
5.41 -by (auto_tac (claset(),simpset() addsimps [even_num_iff]));
5.42 +by (auto_tac (claset(),simpset() addsimps [even_num_iff] delsimprocs [cancel_div_mod_proc]));
5.43  qed "lemma_mod_4_even_n2";
5.44
5.45  Goal "n mod 4 = 3 ==> odd(n)";
5.46  by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
5.47 -by (auto_tac (claset(),simpset() addsimps [odd_num_iff]));
5.48 +by (auto_tac (claset(),simpset() addsimps [odd_num_iff] delsimprocs [cancel_div_mod_proc]));
5.49  qed "lemma_mod_4_odd_n2";
5.50
5.51  Goal "even n ==> ((-1) ^ n) = (1::real)";
5.52 @@ -344,7 +343,7 @@
5.53
5.54  Goal "n mod 4 = 3 ==> odd((n - 1) div 2)";
5.55  by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
5.56 -by (asm_full_simp_tac (simpset() addsimps [odd_num_iff]) 1);
5.57 +by (asm_full_simp_tac (simpset() addsimps [odd_num_iff] delsimprocs [cancel_div_mod_proc]) 1);
5.58  val lemma_odd_mod_4_div_2 = result();
5.59
5.60  Goal "(4 * n) div 2 = (2::nat) * n";
```
```     6.1 --- a/src/HOL/Integ/IntDiv.thy	Fri Aug 23 07:34:20 2002 +0200
6.2 +++ b/src/HOL/Integ/IntDiv.thy	Fri Aug 23 07:41:05 2002 +0200
6.3 @@ -31,7 +31,8 @@
6.4  *)
6.5
6.6
6.7 -theory IntDiv = IntArith + Recdef:
6.8 +theory IntDiv = IntArith + Recdef
6.9 +  files ("IntDiv_setup.ML"):
6.10
6.11  declare zless_nat_conj [simp]
6.12
6.13 @@ -221,6 +222,14 @@
6.14  apply (auto simp add: quorem_def div_def mod_def)
6.15  done
6.16
6.17 +lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"
6.19 +
6.20 +lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k"
6.22 +
6.23 +use "IntDiv_setup.ML"
6.24 +
6.25  lemma pos_mod_conj : "(0::int) < b ==> 0 <= a mod b & a mod b < b"
6.26  apply (cut_tac a = a and b = b in divAlg_correct)
6.27  apply (auto simp add: quorem_def mod_def)
6.28 @@ -572,8 +581,7 @@
6.29       "[| quorem((b,c),(q,r));  c ~= 0 |]
6.30        ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
6.32 -                    pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound
6.33 -                    zmod_zdiv_equality)
6.34 +                    pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
6.35
6.36  lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
6.37  apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
6.38 @@ -610,7 +618,13 @@
6.39  by (simp add: zmult_commute zmod_zmult1_eq)
6.40
6.41  lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
6.42 -by (cut_tac a = m and b = d in zmod_zdiv_equality, auto)
6.43 +proof
6.44 +  assume "m mod d = 0"
6.45 +  from this zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto
6.46 +next
6.47 +  assume "EX q::int. m = d*q"
6.48 +  thus "m mod d = 0" by auto
6.49 +qed
6.50
6.51  declare zmod_eq_0_iff [THEN iffD1, dest!]
6.52
6.53 @@ -621,8 +635,7 @@
6.54       "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c ~= 0 |]
6.55        ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
6.57 -                    pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound
6.58 -                    zmod_zdiv_equality)
6.59 +                    pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
6.60
6.61  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
6.63 @@ -720,7 +733,7 @@
6.64
6.65  lemma zmult2_lemma: "[| quorem ((a,b), (q,r));  b ~= 0;  0 < c |]
6.66        ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
6.67 -by (auto simp add: zmult_ac zmod_zdiv_equality quorem_def linorder_neq_iff
6.68 +by (auto simp add: zmult_ac quorem_def linorder_neq_iff
6.70                     lemma1 lemma2 lemma3 lemma4)
6.71
6.72 @@ -796,7 +809,7 @@
6.73  txt{*converse direction*}
6.74  apply (drule_tac x = "n div k" in spec)
6.75  apply (drule_tac x = "n mod k" in spec)
6.76 -apply (simp add: pos_mod_bound pos_mod_sign zmod_zdiv_equality [symmetric])
6.77 +apply (simp add: pos_mod_bound pos_mod_sign)
6.78  done
6.79
6.80  lemma split_neg_lemma:
6.81 @@ -811,7 +824,7 @@
6.82  txt{*converse direction*}
6.83  apply (drule_tac x = "n div k" in spec)
6.84  apply (drule_tac x = "n mod k" in spec)
6.85 -apply (simp add: neg_mod_bound neg_mod_sign zmod_zdiv_equality [symmetric])
6.86 +apply (simp add: neg_mod_bound neg_mod_sign)
6.87  done
6.88
6.89  lemma split_zdiv:
```
```     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/Integ/IntDiv_setup.ML	Fri Aug 23 07:41:05 2002 +0200
7.3 @@ -0,0 +1,37 @@
7.4 +(*  Title:      HOL/Integ/IntDiv_setup.ML
7.5 +    ID:         \$Id\$
7.6 +    Author:     Tobias Nipkow, Informatik, TU Muenchen
7.7 +    Copyright   2002  TU Muenchen
7.8 +
7.9 +Simproc for cancelling div and mod
7.10 +*)
7.11 +
7.12 +
7.13 +structure CancelDivModData =
7.14 +struct
7.15 +
7.16 +val div_name = "Divides.op div";
7.17 +val mod_name = "Divides.op mod";
7.18 +val mk_binop = HOLogic.mk_binop;
7.19 +val mk_sum = Int_Numeral_Simprocs.mk_sum;
7.20 +val dest_sum = Int_Numeral_Simprocs.dest_sum;
7.21 +
7.22 +(*logic*)
7.23 +
7.24 +val div_mod_eqs =
7.25 +  map mk_meta_eq [thm"zdiv_zmod_equality",thm"zdiv_zmod_equality2"]
7.26 +
7.27 +val trans = trans
7.28 +
7.29 +val prove_eq_sums =
7.31 +  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all simps) end
7.32 +
7.33 +end;
7.34 +
7.35 +structure CancelDivMod = CancelDivModFun(CancelDivModData);
7.36 +
7.37 +val cancel_zdiv_zmod_proc = NatArithUtils.prep_simproc
7.38 +      ("cancel_zdiv_zmod", ["(m::int) + n"], CancelDivMod.proc);
7.39 +
```
```     8.1 --- a/src/HOL/Integ/nat_bin.ML	Fri Aug 23 07:34:20 2002 +0200
8.2 +++ b/src/HOL/Integ/nat_bin.ML	Fri Aug 23 07:41:05 2002 +0200
8.3 @@ -174,8 +174,6 @@
8.4  by (asm_full_simp_tac
8.5      (simpset() addsimps [nat_less_iff RS sym, quorem_def,
8.7 -by (rtac (mod_div_equality RS sym RS trans) 1);
8.9  qed "nat_div_distrib";
8.10
8.11  Goal "(number_of v :: nat)  div  number_of v' = \
8.12 @@ -207,8 +205,6 @@
8.13  by (asm_full_simp_tac
8.14       (simpset() addsimps [nat_less_iff RS sym, quorem_def,
8.16 -by (rtac (mod_div_equality RS sym RS trans) 1);
8.18  qed "nat_mod_distrib";
8.19
8.20  Goal "(number_of v :: nat)  mod  number_of v' = \
```
```     9.1 --- a/src/HOL/IsaMakefile	Fri Aug 23 07:34:20 2002 +0200
9.2 +++ b/src/HOL/IsaMakefile	Fri Aug 23 07:41:05 2002 +0200
9.3 @@ -73,6 +73,7 @@
9.4    \$(SRC)/Provers/Arith/combine_numerals.ML \
9.5    \$(SRC)/Provers/Arith/cancel_numeral_factor.ML \
9.6    \$(SRC)/Provers/Arith/extract_common_term.ML \
9.7 +  \$(SRC)/Provers/Arith/cancel_div_mod.ML \
9.8    \$(SRC)/Provers/Arith/fast_lin_arith.ML \$(SRC)/Provers/blast.ML \
9.9    \$(SRC)/Provers/clasimp.ML \$(SRC)/Provers/classical.ML \
9.10    \$(SRC)/Provers/hypsubst.ML \$(SRC)/Provers/induct_method.ML \
```
```    10.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Fri Aug 23 07:34:20 2002 +0200
10.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Fri Aug 23 07:41:05 2002 +0200
10.3 @@ -183,7 +183,7 @@
10.4  lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
10.5    apply (subgoal_tac "k dvd n * (m div n) + m mod n")
10.6     apply (simp add: zmod_zdiv_equality [symmetric])
10.8 +  apply (simp only: zdvd_zadd zdvd_zmult2)
10.9    done
10.10
10.11  lemma zdvd_iff_zmod_eq_0: "(k dvd n) = (n mod (k::int) = 0)"
10.12 @@ -602,8 +602,7 @@
10.13    apply (rule_tac x = "a mod m" in exI)
10.14    apply (auto simp add: pos_mod_sign pos_mod_bound)
10.15    apply (rule_tac x = "-(a div m)" in exI)
10.16 -  apply (cut_tac a = a and b = m in zmod_zdiv_equality)
10.17 -  apply auto
10.19    done
10.20
10.21  lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)"
10.22 @@ -624,13 +623,8 @@
10.23    done
10.24
10.25  lemma aux: "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
10.26 -  apply (rule_tac "s" = "(m * (a div m) + a mod m) - (m * (b div m) + b mod m)"
10.27 -    in trans)
10.28 -   prefer 2
10.29 -   apply (simp add: zdiff_zmult_distrib2)
10.30 -  apply (rule aux)
10.31 -   apply (rule_tac [!] zmod_zdiv_equality)
10.32 -  done
10.34 +
10.35
10.36  lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
10.37    apply (unfold zcong_def)
10.38 @@ -685,9 +679,7 @@
10.39     prefer 2
10.40     apply (subst zcong_iff_lin)
10.41     apply (rule_tac x = "k * (a div (m * k))" in exI)
10.43 -   apply (subst zmult_assoc [symmetric])
10.44 -   apply (rule_tac zmod_zdiv_equality)
10.46    apply assumption
10.47    done
10.48
10.49 @@ -756,11 +748,7 @@
10.50      ==> (r' mod r) = (s' - (r' div r) * s) * m + (t' - (r' div r) * t) * (n::int)"
10.51    apply (rule trans)
10.52     apply (rule_tac [2] aux [symmetric])
10.53 -  apply simp
10.54 -  apply (subst eq_zdiff_eq)
10.55 -  apply (rule trans [symmetric])
10.56 -  apply (rule_tac b = "s * m + t * n" in zmod_zdiv_equality)
10.57 -  apply (simp add: zmult_commute)
10.58 +  apply (simp add: eq_zdiff_eq zmult_commute)
10.59    done
10.60
10.61  lemma order_le_neq_implies_less: "(x::'a::order) \<le> y ==> x \<noteq> y ==> x < y"
```
```    11.1 --- a/src/HOL/ROOT.ML	Fri Aug 23 07:34:20 2002 +0200
11.2 +++ b/src/HOL/ROOT.ML	Fri Aug 23 07:41:05 2002 +0200
11.3 @@ -34,6 +34,7 @@
11.4  use "~~/src/Provers/Arith/combine_numerals.ML";
11.5  use "~~/src/Provers/Arith/cancel_numeral_factor.ML";
11.6  use "~~/src/Provers/Arith/extract_common_term.ML";
11.7 +use "~~/src/Provers/Arith/cancel_div_mod.ML";
11.8
11.9  with_path "Integ" use_thy "Main";
11.10
```
```    12.1 --- a/src/HOL/arith_data.ML	Fri Aug 23 07:34:20 2002 +0200
12.2 +++ b/src/HOL/arith_data.ML	Fri Aug 23 07:41:05 2002 +0200
12.3 @@ -9,16 +9,9 @@
12.4  (* 1. Cancellation of common terms                                           *)
12.5  (*---------------------------------------------------------------------------*)
12.6
12.7 -signature ARITH_DATA =
12.8 -sig
12.9 -  val nat_cancel_sums_add: simproc list
12.10 -  val nat_cancel_sums: simproc list
12.11 -end;
12.12 -
12.13 -structure ArithData: ARITH_DATA =
12.14 +structure NatArithUtils =
12.15  struct
12.16
12.17 -
12.18  (** abstract syntax of structure nat: 0, Suc, + **)
12.19
12.20  (* mk_sum, mk_norm_sum *)
12.21 @@ -58,11 +51,11 @@
12.22
12.23  val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
12.24
12.25 -fun prove_conv expand_tac norm_tac sg (t, u) =
12.26 -  mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
12.27 +fun prove_conv expand_tac norm_tac sg tu =
12.28 +  mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv tu))
12.29      (K [expand_tac, norm_tac]))
12.30    handle ERROR => error ("The error(s) above occurred while trying to prove " ^
12.31 -    (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
12.32 +    (string_of_cterm (cterm_of sg (mk_eqv tu))));
12.33
12.34  val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
12.35    (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
12.36 @@ -75,6 +68,21 @@
12.38  val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
12.39
12.40 +fun prep_simproc (name, pats, proc) =
12.41 +  Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
12.42 +
12.43 +end;
12.44 +
12.45 +signature ARITH_DATA =
12.46 +sig
12.47 +  val nat_cancel_sums_add: simproc list
12.48 +  val nat_cancel_sums: simproc list
12.49 +end;
12.50 +
12.51 +structure ArithData: ARITH_DATA =
12.52 +struct
12.53 +
12.54 +open NatArithUtils;
12.55
12.56
12.57  (** cancel common summands **)
12.58 @@ -138,9 +146,6 @@
12.59
12.60  (** prepare nat_cancel simprocs **)
12.61
12.62 -fun prep_simproc (name, pats, proc) =
12.63 -  Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
12.64 -
12.65  val nat_cancel_sums_add = map prep_simproc
12.66    [("nateq_cancel_sums",
12.67       ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"], EqCancelSums.proc),
```