# HG changeset patch # User haftmann # Date 1476603065 -7200 # Node ID aee949f6642dffa565ecc74e42330190309e44e4 # Parent 93c6f0da5c702d2dc7f4fcddfa147b9762f462ba eliminated irregular aliasses diff -r 93c6f0da5c70 -r aee949f6642d NEWS --- a/NEWS Sun Oct 16 09:31:05 2016 +0200 +++ b/NEWS Sun Oct 16 09:31:05 2016 +0200 @@ -270,6 +270,8 @@ minus_div_eq_mod2 ~> minus_mult_div_eq_mod minus_mod_eq_div ~> minus_mod_eq_div_mult minus_mod_eq_div2 ~> minus_mod_eq_mult_div + div_mod_equality' ~> minus_mod_eq_div_mult [symmetric] + mod_div_equality' ~> minus_div_mult_eq_mod [symmetric] INCOMPATIBILITY. * Dedicated syntax LENGTH('a) for length of types. diff -r 93c6f0da5c70 -r aee949f6642d src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Sun Oct 16 09:31:05 2016 +0200 +++ b/src/HOL/Decision_Procs/Approximation.thy Sun Oct 16 09:31:05 2016 +0200 @@ -4426,7 +4426,7 @@ "n \ m \ real n \ real m" "n < m \ real n < real m" "n \ {m .. l} \ real n \ {real m .. real l}" - by (simp_all add: real_div_nat_eq_floor_of_divide div_mult_mod_eq') + by (simp_all add: real_div_nat_eq_floor_of_divide minus_div_mult_eq_mod [symmetric]) ML_file "approximation.ML" diff -r 93c6f0da5c70 -r aee949f6642d src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Sun Oct 16 09:31:05 2016 +0200 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Sun Oct 16 09:31:05 2016 +0200 @@ -56,7 +56,7 @@ addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}] val simpset0 = put_simpset HOL_basic_ss ctxt - addsimps @{thms div_mult_mod_eq' Suc_eq_plus1 simp_thms} + addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1 simp_thms} |> fold Splitter.add_split @{thms split_zdiv split_zmod split_div' split_min split_max} (* Simp rules for changing (n::int) to int n *) val simpset1 = diff -r 93c6f0da5c70 -r aee949f6642d src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Sun Oct 16 09:31:05 2016 +0200 +++ b/src/HOL/Decision_Procs/mir_tac.ML Sun Oct 16 09:31:05 2016 +0200 @@ -31,7 +31,6 @@ @{thm uminus_add_conv_diff [symmetric]}, @{thm "minus_divide_left"}] val comp_ths = distinct Thm.eq_thm (ths @ comp_arith @ @{thms simp_thms}); -val div_mult_mod_eq' = @{thm "div_mult_mod_eq'"}; val mod_add_eq = @{thm "mod_add_eq"} RS sym; fun prepare_for_mir q fm = @@ -80,7 +79,7 @@ addsimps @{thms add.assoc add.commute add.left_commute} addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}] val simpset0 = put_simpset HOL_basic_ss ctxt - addsimps [div_mult_mod_eq', @{thm Suc_eq_plus1}] + addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1} addsimps comp_ths |> fold Splitter.add_split [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, diff -r 93c6f0da5c70 -r aee949f6642d src/HOL/Divides.thy --- a/src/HOL/Divides.thy Sun Oct 16 09:31:05 2016 +0200 +++ b/src/HOL/Divides.thy Sun Oct 16 09:31:05 2016 +0200 @@ -1387,12 +1387,7 @@ qed qed -theorem div_mult_mod_eq' [nitpick_unfold]: "(m::nat) mod n = m - (m div n) * n" - using div_mult_mod_eq [of m n] by arith - -lemma div_mod_equality': "(m::nat) div n * n = m - m mod n" - using div_mult_mod_eq [of m n] by arith -(* FIXME: very similar to mult_div_cancel *) +declare minus_div_mult_eq_mod [symmetric, where ?'a = nat, nitpick_unfold] lemma div_eq_dividend_iff: "a \ 0 \ (a :: nat) div b = a \ b = 1" apply rule diff -r 93c6f0da5c70 -r aee949f6642d src/HOL/Library/RBT_Impl.thy --- a/src/HOL/Library/RBT_Impl.thy Sun Oct 16 09:31:05 2016 +0200 +++ b/src/HOL/Library/RBT_Impl.thy Sun Oct 16 09:31:05 2016 +0200 @@ -1416,7 +1416,7 @@ moreover note feven[unfolded feven_def] (* FIXME: why does by(rule feven[unfolded feven_def]) not work? *) ultimately have "P (2 * (n div 2)) kvs" by - - thus ?thesis using True by (metis div_mod_equality' minus_nat.diff_0 mult.commute) + thus ?thesis using True by (metis minus_mod_eq_div_mult [symmetric] minus_nat.diff_0 mult.commute) next case False note ge0 moreover from "1.prems" have n2: "n div 2 \ length kvs" by simp @@ -1462,7 +1462,7 @@ moreover note geven[unfolded geven_def] ultimately have "Q (2 * (n div 2)) kvs" by - thus ?thesis using True - by(metis div_mod_equality' minus_nat.diff_0 mult.commute) + by(metis minus_mod_eq_div_mult [symmetric] minus_nat.diff_0 mult.commute) next case False note ge0 moreover from "2.prems" have n2: "n div 2 \ length kvs" by simp diff -r 93c6f0da5c70 -r aee949f6642d src/HOL/Number_Theory/Eratosthenes.thy --- a/src/HOL/Number_Theory/Eratosthenes.thy Sun Oct 16 09:31:05 2016 +0200 +++ b/src/HOL/Number_Theory/Eratosthenes.thy Sun Oct 16 09:31:05 2016 +0200 @@ -143,7 +143,7 @@ then have "u + (w - u mod w) = w + (u - u mod w)" by simp then have "u + (w - u mod w) = w + u div w * w" - by (simp add: div_mod_equality' [symmetric]) + by (simp add: minus_mod_eq_div_mult) } then have "w dvd v + w + r + (w - v mod w) \ w dvd m + w + r + (w - m mod w)" by (simp add: add.assoc add.left_commute [of m] add.left_commute [of v] diff -r 93c6f0da5c70 -r aee949f6642d src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sun Oct 16 09:31:05 2016 +0200 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sun Oct 16 09:31:05 2016 +0200 @@ -510,7 +510,7 @@ also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r] by (simp add: algebra_simps) finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" . - qed (auto simp: gcd_eucl_non_0 algebra_simps div_mod_equality') + qed (auto simp: gcd_eucl_non_0 algebra_simps minus_mod_eq_div_mult [symmetric]) finally show ?thesis . qed qed diff -r 93c6f0da5c70 -r aee949f6642d src/HOL/Old_Number_Theory/Pocklington.thy --- a/src/HOL/Old_Number_Theory/Pocklington.thy Sun Oct 16 09:31:05 2016 +0200 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy Sun Oct 16 09:31:05 2016 +0200 @@ -1241,8 +1241,8 @@ unfolding mod_eq_0_iff by blast hence eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp from qrn[symmetric] have qn1: "q dvd n - 1" unfolding dvd_def by auto - from dvd_trans[OF p(2) qn1] div_mod_equality'[of "n - 1" p] - have npp: "(n - 1) div p * p = n - 1" by (simp add: dvd_eq_mod_eq_0) + with p(2) have npp: "(n - 1) div p * p = n - 1" + by (auto intro: dvd_div_mult_self dvd_trans) with eq0 have "a^ (n - 1) = (n*s)^p" by (simp add: power_mult[symmetric]) hence "1 = (n*s)^(Suc (p - 1)) mod n" using bqn p01 by simp diff -r 93c6f0da5c70 -r aee949f6642d src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Sun Oct 16 09:31:05 2016 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Sun Oct 16 09:31:05 2016 +0200 @@ -835,7 +835,7 @@ addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]) val splits_ss = simpset_of (put_simpset comp_ss @{context} - addsimps [@{thm "div_mult_mod_eq'"}] + addsimps [@{thm minus_div_mult_eq_mod [symmetric]}] |> fold Splitter.add_split [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]) diff -r 93c6f0da5c70 -r aee949f6642d src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Sun Oct 16 09:31:05 2016 +0200 +++ b/src/HOL/Word/Word.thy Sun Oct 16 09:31:05 2016 +0200 @@ -3867,7 +3867,7 @@ apply clarsimp apply (clarsimp simp add : nth_append size_rcat_lem) apply (simp (no_asm_use) only: mult_Suc [symmetric] - td_gal_lt_len less_Suc_eq_le div_mult_mod_eq') + td_gal_lt_len less_Suc_eq_le minus_div_mult_eq_mod [symmetric]) apply clarsimp done