--- a/src/HOL/Divides.thy Fri Aug 23 07:34:20 2002 +0200
+++ b/src/HOL/Divides.thy Fri Aug 23 07:41:05 2002 +0200
@@ -44,11 +44,6 @@
use "Divides_lemmas.ML"
-lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
-apply(insert mod_div_equality[of m n])
-apply(simp only:mult_ac)
-done
-
lemma split_div:
"P(n div k :: nat) =
((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
@@ -85,7 +80,7 @@
assume not0: "k \<noteq> 0"
with Q have R: ?R by simp
from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
- show ?P by(simp add:mod_div_equality2)
+ show ?P by simp
qed
qed
@@ -118,7 +113,7 @@
assume not0: "k \<noteq> 0"
with Q have R: ?R by simp
from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
- show ?P by(simp add:mod_div_equality2)
+ show ?P by simp
qed
qed
@@ -145,7 +140,7 @@
next
assume Q: ?Q
from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
- show ?P by(simp add:mod_div_equality2)
+ show ?P by simp
qed
lemma split_mod:
@@ -163,7 +158,7 @@
next
assume Q: ?Q
from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
- show ?P by(simp add:mod_div_equality2)
+ show ?P by simp
qed
*)
end
--- a/src/HOL/Divides_lemmas.ML Fri Aug 23 07:34:20 2002 +0200
+++ b/src/HOL/Divides_lemmas.ML Fri Aug 23 07:41:05 2002 +0200
@@ -180,10 +180,55 @@
add_diff_inverse, diff_less])));
qed "mod_div_equality";
+Goal "n * (m div n) + m mod n = (m::nat)";
+by(cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1);
+by(asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
+qed "mod_div_equality2";
+
+(*-----------------------------------------------------------------------*)
+(*Simproc for cancelling div and mod *)
+(*-----------------------------------------------------------------------*)
+
+Goal "((m div n)*n + m mod n) + k = (m::nat) + k";
+by(simp_tac (simpset() addsimps [mod_div_equality]) 1);
+qed "div_mod_equality";
+
+Goal "(n*(m div n) + m mod n) + k = (m::nat) + k";
+by(simp_tac (simpset() addsimps [thm"mod_div_equality2"]) 1);
+qed "div_mod_equality2";
+
+structure CancelDivModData =
+struct
+
+val div_name = "Divides.op div";
+val mod_name = "Divides.op mod";
+val mk_binop = HOLogic.mk_binop;
+val mk_sum = NatArithUtils.mk_sum;
+val dest_sum = NatArithUtils.dest_sum;
+
+(*logic*)
+
+val div_mod_eqs = map mk_meta_eq [div_mod_equality,div_mod_equality2]
+
+val trans = trans
+
+val prove_eq_sums =
+ let val simps = add_0 :: add_0_right :: add_ac
+ in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all simps) end
+
+end;
+
+structure CancelDivMod = CancelDivModFun(CancelDivModData);
+
+val cancel_div_mod_proc = NatArithUtils.prep_simproc
+ ("cancel_div_mod", ["(m::nat) + n"], CancelDivMod.proc);
+
+Addsimprocs[cancel_div_mod_proc];
+
+
(* a simple rearrangement of mod_div_equality: *)
Goal "(n::nat) * (m div n) = m - (m mod n)";
-by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1);
-by (full_simp_tac (simpset() addsimps mult_ac) 1);
+by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality2 1);
by (arith_tac 1);
qed "mult_div_cancel";
@@ -240,7 +285,6 @@
qed "unique_remainder";
Goal "0 < b ==> quorem ((a, b), (a div b, a mod b))";
-by (cut_inst_tac [("m","a"),("n","b")] mod_div_equality 1);
by (auto_tac
(claset() addEs [sym],
simpset() addsimps mult_ac@[Divides.quorem_def]));
@@ -271,7 +315,6 @@
Goal "[| quorem((b,c),(q,r)); 0 < c |] \
\ ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))";
-by (cut_inst_tac [("m", "a*r"), ("n","c")] mod_div_equality 1);
by (auto_tac
(claset(),
simpset() addsimps split_ifs@mult_ac@
@@ -304,7 +347,6 @@
Goal "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); 0 < c |] \
\ ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))";
-by (cut_inst_tac [("m", "ar+br"), ("n","c")] mod_div_equality 1);
by (auto_tac
(claset(),
simpset() addsimps split_ifs@mult_ac@
@@ -339,7 +381,6 @@
Goal "[| quorem ((a,b), (q,r)); 0 < b; 0 < c |] \
\ ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))";
-by (cut_inst_tac [("m", "q"), ("n","c")] mod_div_equality 1);
by (auto_tac
(claset(),
simpset() addsimps mult_ac@
@@ -357,7 +398,6 @@
Goal "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)";
by (div_undefined_case_tac "b=0" 1);
by (div_undefined_case_tac "c=0" 1);
-by (cut_inst_tac [("m", "a"), ("n","b")] mod_div_equality 1);
by (auto_tac (claset(),
simpset() addsimps [mult_commute,
quorem_div_mod RS lemma RS quorem_mod]));
@@ -614,7 +654,7 @@
Goal "[| (k::nat) dvd m mod n; k dvd n |] ==> k dvd m";
by (subgoal_tac "k dvd (m div n)*n + m mod n" 1);
-by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2);
+by (asm_simp_tac (HOL_basic_ss addsimps [dvd_add, dvd_mult]) 2);
by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
qed "dvd_mod_imp_dvd";
@@ -690,7 +730,6 @@
(*Loses information, namely we also have r<d provided d is nonzero*)
Goal "(m mod d = r) ==> EX q::nat. m = r + q*d";
by (cut_inst_tac [("m","m")] mod_div_equality 1);
-by (full_simp_tac (simpset() addsimps add_ac) 1);
+by (full_simp_tac (HOL_basic_ss addsimps add_ac) 1);
by (blast_tac (claset() addIs [sym]) 1);
qed "mod_eqD";
-
--- a/src/HOL/HoareParallel/OG_Examples.thy Fri Aug 23 07:34:20 2002 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy Fri Aug 23 07:41:05 2002 +0200
@@ -340,44 +340,38 @@
subsubsection {* Previous lemmas *}
-lemma nat_lemma1: "\<lbrakk>(c::nat) \<le> a ;a < b\<rbrakk> \<Longrightarrow> b - a \<le> b - c"
-by (simp split: nat_diff_split)
-
-lemma nat_lemma2: "\<lbrakk> b = m*(n::nat) + t; a = s*n + t ; b - a < n \<rbrakk> \<Longrightarrow> m - s = 0"
+lemma nat_lemma2: "\<lbrakk> b = m*(n::nat) + t; a = s*n + u; t=u; b-a < n \<rbrakk> \<Longrightarrow> m \<le> s"
proof -
- assume "b = m*(n::nat) + t" and "a = s*n + t"
+ assume "b = m*(n::nat) + t" "a = s*n + u" "t=u"
hence "(m - s) * n = b - a" by (simp add: diff_mult_distrib)
also assume "\<dots> < n"
finally have "m - s < 1" by simp
thus ?thesis by arith
qed
-lemma less_imp_diff_is_0: "m < Suc(n) \<Longrightarrow> m-n = 0"
-by arith
lemma mod_lemma: "\<lbrakk> (c::nat) \<le> a; a < b; b - c < n \<rbrakk> \<Longrightarrow> b mod n \<noteq> a mod n"
apply(subgoal_tac "b=b div n*n + b mod n" )
prefer 2 apply (simp add: mod_div_equality [symmetric])
apply(subgoal_tac "a=a div n*n + a mod n")
prefer 2
apply(simp add: mod_div_equality [symmetric])
-apply(frule nat_lemma1 , assumption)
+apply(subgoal_tac "b - a \<le> b - c")
+ prefer 2 apply arith
apply(drule le_less_trans)
back
apply assumption
apply(frule less_not_refl2)
apply(drule less_imp_le)
-apply (drule_tac m = "a" in div_le_mono)
-apply(drule_tac m = "a div n" in le_imp_less_Suc)
-apply(drule less_imp_diff_is_0)
+apply (drule_tac m = "a" and k = n in div_le_mono)
apply(safe)
-apply(simp)
-apply(frule_tac b = "b" and a = "a" and n = "n" in nat_lemma2 , assumption)
+apply(frule_tac b = "b" and a = "a" and n = "n" in nat_lemma2, assumption, assumption)
apply assumption
-apply(drule diffs0_imp_equal)
-apply(simp)
+apply(drule order_antisym, assumption)
+apply(rotate_tac -3)
apply(simp)
done
+
subsubsection {* Producer/Consumer Algorithm *}
record Producer_consumer =
--- a/src/HOL/HoareParallel/RG_Examples.thy Fri Aug 23 07:34:20 2002 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy Fri Aug 23 07:41:05 2002 +0200
@@ -278,14 +278,14 @@
lemma mod_aux :"\<lbrakk>i < (n::nat); a mod n = i; j < a + n; j mod n = i; a < j\<rbrakk> \<Longrightarrow> False"
apply(subgoal_tac "a=a div n*n + a mod n" )
- prefer 2 apply (simp (no_asm_use) only: mod_div_equality [symmetric])
+ prefer 2 apply (simp (no_asm_use))
apply(subgoal_tac "j=j div n*n + j mod n")
- prefer 2 apply (simp (no_asm_use) only: mod_div_equality [symmetric])
+ prefer 2 apply (simp (no_asm_use))
apply simp
apply(subgoal_tac "a div n*n < j div n*n")
prefer 2 apply arith
apply(subgoal_tac "j div n*n < (a div n + 1)*n")
-prefer 2 apply simp
+prefer 2 apply simp
apply (simp only:mult_less_cancel2)
apply arith
done
--- a/src/HOL/Hyperreal/EvenOdd.ML Fri Aug 23 07:34:20 2002 +0200
+++ b/src/HOL/Hyperreal/EvenOdd.ML Fri Aug 23 07:41:05 2002 +0200
@@ -253,8 +253,7 @@
(* Some mod and div stuff *)
Goal "n ~= (0::nat) ==> (m = m div n * n + m mod n) & m mod n < n";
-by (auto_tac (claset() addIs [mod_less_divisor],simpset()
- addsimps [mod_div_equality]));
+by (auto_tac (claset() addIs [mod_less_divisor],simpset()));
qed "mod_div_eq_less";
Goal "(k*n + m) mod n = m mod (n::nat)";
@@ -273,7 +272,7 @@
by (etac exE 1);
by (Asm_simp_tac 1);
by (res_inst_tac [("t","m"),("n1","n")] (mod_div_equality RS subst) 1);
-by Auto_tac;
+by (auto_tac (claset(),simpset() delsimprocs [cancel_div_mod_proc]));
qed "mod_Suc_eq_Suc_mod";
Goal "even n = (even (n mod 4))";
@@ -281,7 +280,7 @@
by (etac exE 1);
by (Asm_simp_tac 1);
by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (auto_tac (claset(),simpset() addsimps [even_mult,even_num_iff]));
+by (auto_tac (claset(),simpset() addsimps [even_mult,even_num_iff] delsimprocs [cancel_div_mod_proc]));
qed "even_even_mod_4_iff";
Goal "odd n = (odd (n mod 4))";
@@ -309,17 +308,17 @@
Goal "n mod 4 = 1 ==> odd(n)";
by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (auto_tac (claset(),simpset() addsimps [odd_num_iff]));
+by (auto_tac (claset(),simpset() addsimps [odd_num_iff] delsimprocs [cancel_div_mod_proc]));
qed "lemma_mod_4_odd_n";
Goal "n mod 4 = 2 ==> even(n)";
by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (auto_tac (claset(),simpset() addsimps [even_num_iff]));
+by (auto_tac (claset(),simpset() addsimps [even_num_iff] delsimprocs [cancel_div_mod_proc]));
qed "lemma_mod_4_even_n2";
Goal "n mod 4 = 3 ==> odd(n)";
by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (auto_tac (claset(),simpset() addsimps [odd_num_iff]));
+by (auto_tac (claset(),simpset() addsimps [odd_num_iff] delsimprocs [cancel_div_mod_proc]));
qed "lemma_mod_4_odd_n2";
Goal "even n ==> ((-1) ^ n) = (1::real)";
@@ -344,7 +343,7 @@
Goal "n mod 4 = 3 ==> odd((n - 1) div 2)";
by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (asm_full_simp_tac (simpset() addsimps [odd_num_iff]) 1);
+by (asm_full_simp_tac (simpset() addsimps [odd_num_iff] delsimprocs [cancel_div_mod_proc]) 1);
val lemma_odd_mod_4_div_2 = result();
Goal "(4 * n) div 2 = (2::nat) * n";
--- a/src/HOL/Integ/IntDiv.thy Fri Aug 23 07:34:20 2002 +0200
+++ b/src/HOL/Integ/IntDiv.thy Fri Aug 23 07:41:05 2002 +0200
@@ -31,7 +31,8 @@
*)
-theory IntDiv = IntArith + Recdef:
+theory IntDiv = IntArith + Recdef
+ files ("IntDiv_setup.ML"):
declare zless_nat_conj [simp]
@@ -221,6 +222,14 @@
apply (auto simp add: quorem_def div_def mod_def)
done
+lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"
+by(simp add: zmod_zdiv_equality[symmetric])
+
+lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k"
+by(simp add: zmult_commute zmod_zdiv_equality[symmetric])
+
+use "IntDiv_setup.ML"
+
lemma pos_mod_conj : "(0::int) < b ==> 0 <= a mod b & a mod b < b"
apply (cut_tac a = a and b = b in divAlg_correct)
apply (auto simp add: quorem_def mod_def)
@@ -572,8 +581,7 @@
"[| quorem((b,c),(q,r)); c ~= 0 |]
==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
by (force simp add: split_ifs quorem_def linorder_neq_iff zadd_zmult_distrib2
- pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound
- zmod_zdiv_equality)
+ pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
@@ -610,7 +618,13 @@
by (simp add: zmult_commute zmod_zmult1_eq)
lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
-by (cut_tac a = m and b = d in zmod_zdiv_equality, auto)
+proof
+ assume "m mod d = 0"
+ from this zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto
+next
+ assume "EX q::int. m = d*q"
+ thus "m mod d = 0" by auto
+qed
declare zmod_eq_0_iff [THEN iffD1, dest!]
@@ -621,8 +635,7 @@
"[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c ~= 0 |]
==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
by (force simp add: split_ifs quorem_def linorder_neq_iff zadd_zmult_distrib2
- pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound
- zmod_zdiv_equality)
+ pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
lemma zdiv_zadd1_eq:
@@ -720,7 +733,7 @@
lemma zmult2_lemma: "[| quorem ((a,b), (q,r)); b ~= 0; 0 < c |]
==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
-by (auto simp add: zmult_ac zmod_zdiv_equality quorem_def linorder_neq_iff
+by (auto simp add: zmult_ac quorem_def linorder_neq_iff
int_0_less_mult_iff zadd_zmult_distrib2 [symmetric]
lemma1 lemma2 lemma3 lemma4)
@@ -796,7 +809,7 @@
txt{*converse direction*}
apply (drule_tac x = "n div k" in spec)
apply (drule_tac x = "n mod k" in spec)
-apply (simp add: pos_mod_bound pos_mod_sign zmod_zdiv_equality [symmetric])
+apply (simp add: pos_mod_bound pos_mod_sign)
done
lemma split_neg_lemma:
@@ -811,7 +824,7 @@
txt{*converse direction*}
apply (drule_tac x = "n div k" in spec)
apply (drule_tac x = "n mod k" in spec)
-apply (simp add: neg_mod_bound neg_mod_sign zmod_zdiv_equality [symmetric])
+apply (simp add: neg_mod_bound neg_mod_sign)
done
lemma split_zdiv:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/IntDiv_setup.ML Fri Aug 23 07:41:05 2002 +0200
@@ -0,0 +1,37 @@
+(* Title: HOL/Integ/IntDiv_setup.ML
+ ID: $Id$
+ Author: Tobias Nipkow, Informatik, TU Muenchen
+ Copyright 2002 TU Muenchen
+
+Simproc for cancelling div and mod
+*)
+
+
+structure CancelDivModData =
+struct
+
+val div_name = "Divides.op div";
+val mod_name = "Divides.op mod";
+val mk_binop = HOLogic.mk_binop;
+val mk_sum = Int_Numeral_Simprocs.mk_sum;
+val dest_sum = Int_Numeral_Simprocs.dest_sum;
+
+(*logic*)
+
+val div_mod_eqs =
+ map mk_meta_eq [thm"zdiv_zmod_equality",thm"zdiv_zmod_equality2"]
+
+val trans = trans
+
+val prove_eq_sums =
+ let val simps = zdiff_def :: Int_Numeral_Simprocs.add_0s @ zadd_ac
+ in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all simps) end
+
+end;
+
+structure CancelDivMod = CancelDivModFun(CancelDivModData);
+
+val cancel_zdiv_zmod_proc = NatArithUtils.prep_simproc
+ ("cancel_zdiv_zmod", ["(m::int) + n"], CancelDivMod.proc);
+
+Addsimprocs[cancel_zdiv_zmod_proc];
--- a/src/HOL/Integ/nat_bin.ML Fri Aug 23 07:34:20 2002 +0200
+++ b/src/HOL/Integ/nat_bin.ML Fri Aug 23 07:41:05 2002 +0200
@@ -174,8 +174,6 @@
by (asm_full_simp_tac
(simpset() addsimps [nat_less_iff RS sym, quorem_def,
numeral_0_eq_0, zadd_int, zmult_int]) 1);
-by (rtac (mod_div_equality RS sym RS trans) 1);
-by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
qed "nat_div_distrib";
Goal "(number_of v :: nat) div number_of v' = \
@@ -207,8 +205,6 @@
by (asm_full_simp_tac
(simpset() addsimps [nat_less_iff RS sym, quorem_def,
numeral_0_eq_0, zadd_int, zmult_int]) 1);
-by (rtac (mod_div_equality RS sym RS trans) 1);
-by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
qed "nat_mod_distrib";
Goal "(number_of v :: nat) mod number_of v' = \
--- a/src/HOL/IsaMakefile Fri Aug 23 07:34:20 2002 +0200
+++ b/src/HOL/IsaMakefile Fri Aug 23 07:41:05 2002 +0200
@@ -73,6 +73,7 @@
$(SRC)/Provers/Arith/combine_numerals.ML \
$(SRC)/Provers/Arith/cancel_numeral_factor.ML \
$(SRC)/Provers/Arith/extract_common_term.ML \
+ $(SRC)/Provers/Arith/cancel_div_mod.ML \
$(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
$(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
--- a/src/HOL/NumberTheory/IntPrimes.thy Fri Aug 23 07:34:20 2002 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy Fri Aug 23 07:41:05 2002 +0200
@@ -183,7 +183,7 @@
lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
apply (subgoal_tac "k dvd n * (m div n) + m mod n")
apply (simp add: zmod_zdiv_equality [symmetric])
- apply (simp add: zdvd_zadd zdvd_zmult2)
+ apply (simp only: zdvd_zadd zdvd_zmult2)
done
lemma zdvd_iff_zmod_eq_0: "(k dvd n) = (n mod (k::int) = 0)"
@@ -602,8 +602,7 @@
apply (rule_tac x = "a mod m" in exI)
apply (auto simp add: pos_mod_sign pos_mod_bound)
apply (rule_tac x = "-(a div m)" in exI)
- apply (cut_tac a = a and b = m in zmod_zdiv_equality)
- apply auto
+ apply (simp add:zdiff_eq_eq eq_zdiff_eq zadd_commute)
done
lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)"
@@ -624,13 +623,8 @@
done
lemma aux: "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
- apply (rule_tac "s" = "(m * (a div m) + a mod m) - (m * (b div m) + b mod m)"
- in trans)
- prefer 2
- apply (simp add: zdiff_zmult_distrib2)
- apply (rule aux)
- apply (rule_tac [!] zmod_zdiv_equality)
- done
+by(simp add: zdiff_zmult_distrib2 zadd_zdiff_eq eq_zdiff_eq zadd_ac)
+
lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
apply (unfold zcong_def)
@@ -685,9 +679,7 @@
prefer 2
apply (subst zcong_iff_lin)
apply (rule_tac x = "k * (a div (m * k))" in exI)
- apply (subst zadd_commute)
- apply (subst zmult_assoc [symmetric])
- apply (rule_tac zmod_zdiv_equality)
+ apply(simp add:zmult_assoc [symmetric])
apply assumption
done
@@ -756,11 +748,7 @@
==> (r' mod r) = (s' - (r' div r) * s) * m + (t' - (r' div r) * t) * (n::int)"
apply (rule trans)
apply (rule_tac [2] aux [symmetric])
- apply simp
- apply (subst eq_zdiff_eq)
- apply (rule trans [symmetric])
- apply (rule_tac b = "s * m + t * n" in zmod_zdiv_equality)
- apply (simp add: zmult_commute)
+ apply (simp add: eq_zdiff_eq zmult_commute)
done
lemma order_le_neq_implies_less: "(x::'a::order) \<le> y ==> x \<noteq> y ==> x < y"
--- a/src/HOL/ROOT.ML Fri Aug 23 07:34:20 2002 +0200
+++ b/src/HOL/ROOT.ML Fri Aug 23 07:41:05 2002 +0200
@@ -34,6 +34,7 @@
use "~~/src/Provers/Arith/combine_numerals.ML";
use "~~/src/Provers/Arith/cancel_numeral_factor.ML";
use "~~/src/Provers/Arith/extract_common_term.ML";
+use "~~/src/Provers/Arith/cancel_div_mod.ML";
with_path "Integ" use_thy "Main";
--- a/src/HOL/arith_data.ML Fri Aug 23 07:34:20 2002 +0200
+++ b/src/HOL/arith_data.ML Fri Aug 23 07:41:05 2002 +0200
@@ -9,16 +9,9 @@
(* 1. Cancellation of common terms *)
(*---------------------------------------------------------------------------*)
-signature ARITH_DATA =
-sig
- val nat_cancel_sums_add: simproc list
- val nat_cancel_sums: simproc list
-end;
-
-structure ArithData: ARITH_DATA =
+structure NatArithUtils =
struct
-
(** abstract syntax of structure nat: 0, Suc, + **)
(* mk_sum, mk_norm_sum *)
@@ -58,11 +51,11 @@
val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
-fun prove_conv expand_tac norm_tac sg (t, u) =
- mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
+fun prove_conv expand_tac norm_tac sg tu =
+ mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv tu))
(K [expand_tac, norm_tac]))
handle ERROR => error ("The error(s) above occurred while trying to prove " ^
- (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
+ (string_of_cterm (cterm_of sg (mk_eqv tu))));
val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
(fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
@@ -75,6 +68,21 @@
val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
+fun prep_simproc (name, pats, proc) =
+ Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
+
+end;
+
+signature ARITH_DATA =
+sig
+ val nat_cancel_sums_add: simproc list
+ val nat_cancel_sums: simproc list
+end;
+
+structure ArithData: ARITH_DATA =
+struct
+
+open NatArithUtils;
(** cancel common summands **)
@@ -138,9 +146,6 @@
(** prepare nat_cancel simprocs **)
-fun prep_simproc (name, pats, proc) =
- Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
-
val nat_cancel_sums_add = map prep_simproc
[("nateq_cancel_sums",
["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"], EqCancelSums.proc),