Added div+mod cancelling simproc
authornipkow
Fri Aug 23 07:41:05 2002 +0200 (2002-08-23)
changeset 1351742efec18f5b2
parent 13516 13a6103b9ac4
child 13518 a0749ce05100
Added div+mod cancelling simproc
src/HOL/Divides.thy
src/HOL/Divides_lemmas.ML
src/HOL/HoareParallel/OG_Examples.thy
src/HOL/HoareParallel/RG_Examples.thy
src/HOL/Hyperreal/EvenOdd.ML
src/HOL/Integ/IntDiv.thy
src/HOL/Integ/IntDiv_setup.ML
src/HOL/Integ/nat_bin.ML
src/HOL/IsaMakefile
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/ROOT.ML
src/HOL/arith_data.ML
     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.4  				   add_diff_inverse, diff_less])));
     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.40 +  let val simps = add_0 :: add_0_right :: add_ac
    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.50 +Addsimprocs[cancel_div_mod_proc];
    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.67      (claset() addEs [sym],
    2.68       simpset() addsimps mult_ac@[Divides.quorem_def]));
    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.76       simpset() addsimps split_ifs@mult_ac@
    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.84       simpset() addsimps split_ifs@mult_ac@
    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.92       simpset() addsimps mult_ac@
    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.99  	       simpset() addsimps [mult_commute, 
   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.105 -by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2);
   2.106 +by (asm_simp_tac (HOL_basic_ss addsimps [dvd_add, dvd_mult]) 2);
   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.114 -by (full_simp_tac (simpset() addsimps add_ac) 1); 
   2.115 +by (full_simp_tac (HOL_basic_ss addsimps add_ac) 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.28   apply(simp add: mod_div_equality [symmetric])
    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.8 -    addsimps [mod_div_equality]));
     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.18 +by(simp add: zmod_zdiv_equality[symmetric])
    6.19 +
    6.20 +lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k"
    6.21 +by(simp add: zmult_commute zmod_zdiv_equality[symmetric])
    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.31  by (force simp add: split_ifs quorem_def linorder_neq_iff zadd_zmult_distrib2
    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.56  by (force simp add: split_ifs quorem_def linorder_neq_iff zadd_zmult_distrib2
    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.62  lemma zdiv_zadd1_eq:
    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.69                     int_0_less_mult_iff zadd_zmult_distrib2 [symmetric] 
    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.30 +  let val simps = zdiff_def :: Int_Numeral_Simprocs.add_0s @ zadd_ac
    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 +
    7.40 +Addsimprocs[cancel_zdiv_zmod_proc];
     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.6  	                 numeral_0_eq_0, zadd_int, zmult_int]) 1);
     8.7 -by (rtac (mod_div_equality RS sym RS trans) 1);
     8.8 -by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 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.15  		          numeral_0_eq_0, zadd_int, zmult_int]) 1);
    8.16 -by (rtac (mod_div_equality RS sym RS trans) 1);
    8.17 -by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 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.7 -  apply (simp add: zdvd_zadd zdvd_zmult2)
    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.18 +  apply (simp add:zdiff_eq_eq eq_zdiff_eq zadd_commute)
   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.33 +by(simp add: zdiff_zmult_distrib2 zadd_zdiff_eq eq_zdiff_eq zadd_ac)
   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.42 -   apply (subst zadd_commute)
   10.43 -   apply (subst zmult_assoc [symmetric])
   10.44 -   apply (rule_tac zmod_zdiv_equality)
   10.45 +   apply(simp add:zmult_assoc [symmetric])
   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.37  val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
   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),