# HG changeset patch # User nipkow # Date 1030081265 -7200 # Node ID 42efec18f5b255fab12c1144d89fbb686584fbcc # Parent 13a6103b9ac4dc4ab6d16594df9df647cb0ee785 Added div+mod cancelling simproc diff -r 13a6103b9ac4 -r 42efec18f5b2 src/HOL/Divides.thy --- 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 \ P 0) \ (k \ 0 \ (!i. !j P i)))" @@ -85,7 +80,7 @@ assume not0: "k \ 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 \ 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 diff -r 13a6103b9ac4 -r 42efec18f5b2 src/HOL/Divides_lemmas.ML --- 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 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"; - diff -r 13a6103b9ac4 -r 42efec18f5b2 src/HOL/HoareParallel/OG_Examples.thy --- 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: "\(c::nat) \ a ;a < b\ \ b - a \ b - c" -by (simp split: nat_diff_split) - -lemma nat_lemma2: "\ b = m*(n::nat) + t; a = s*n + t ; b - a < n \ \ m - s = 0" +lemma nat_lemma2: "\ b = m*(n::nat) + t; a = s*n + u; t=u; b-a < n \ \ m \ 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 "\ < n" finally have "m - s < 1" by simp thus ?thesis by arith qed -lemma less_imp_diff_is_0: "m < Suc(n) \ m-n = 0" -by arith lemma mod_lemma: "\ (c::nat) \ a; a < b; b - c < n \ \ b mod n \ 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 \ 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 = diff -r 13a6103b9ac4 -r 42efec18f5b2 src/HOL/HoareParallel/RG_Examples.thy --- 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 :"\i < (n::nat); a mod n = i; j < a + n; j mod n = i; a < j\ \ 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 diff -r 13a6103b9ac4 -r 42efec18f5b2 src/HOL/Hyperreal/EvenOdd.ML --- 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"; diff -r 13a6103b9ac4 -r 42efec18f5b2 src/HOL/Integ/IntDiv.thy --- 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: diff -r 13a6103b9ac4 -r 42efec18f5b2 src/HOL/Integ/IntDiv_setup.ML --- /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]; diff -r 13a6103b9ac4 -r 42efec18f5b2 src/HOL/Integ/nat_bin.ML --- 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' = \ diff -r 13a6103b9ac4 -r 42efec18f5b2 src/HOL/IsaMakefile --- 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 \ diff -r 13a6103b9ac4 -r 42efec18f5b2 src/HOL/NumberTheory/IntPrimes.thy --- 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)) = (\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) \ y ==> x \ y ==> x < y" diff -r 13a6103b9ac4 -r 42efec18f5b2 src/HOL/ROOT.ML --- 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"; diff -r 13a6103b9ac4 -r 42efec18f5b2 src/HOL/arith_data.ML --- 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),