eliminated irregular aliasses
authorhaftmann
Sun Oct 16 09:31:05 2016 +0200 (2016-10-16)
changeset 64243aee949f6642d
parent 64242 93c6f0da5c70
child 64244 e7102c40783c
eliminated irregular aliasses
NEWS
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Divides.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Number_Theory/Eratosthenes.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Old_Number_Theory/Pocklington.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Word/Word.thy
     1.1 --- a/NEWS	Sun Oct 16 09:31:05 2016 +0200
     1.2 +++ b/NEWS	Sun Oct 16 09:31:05 2016 +0200
     1.3 @@ -270,6 +270,8 @@
     1.4      minus_div_eq_mod2 ~> minus_mult_div_eq_mod
     1.5      minus_mod_eq_div ~> minus_mod_eq_div_mult
     1.6      minus_mod_eq_div2 ~> minus_mod_eq_mult_div
     1.7 +    div_mod_equality' ~> minus_mod_eq_div_mult [symmetric]
     1.8 +    mod_div_equality' ~> minus_div_mult_eq_mod [symmetric]
     1.9  INCOMPATIBILITY.
    1.10  
    1.11  * Dedicated syntax LENGTH('a) for length of types.
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 16 09:31:05 2016 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 16 09:31:05 2016 +0200
     2.3 @@ -4426,7 +4426,7 @@
     2.4    "n \<le> m \<longleftrightarrow> real n \<le> real m"
     2.5    "n < m \<longleftrightarrow> real n < real m"
     2.6    "n \<in> {m .. l} \<longleftrightarrow> real n \<in> {real m .. real l}"
     2.7 -  by (simp_all add: real_div_nat_eq_floor_of_divide div_mult_mod_eq')
     2.8 +  by (simp_all add: real_div_nat_eq_floor_of_divide minus_div_mult_eq_mod [symmetric])
     2.9  
    2.10  ML_file "approximation.ML"
    2.11  
     3.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Sun Oct 16 09:31:05 2016 +0200
     3.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sun Oct 16 09:31:05 2016 +0200
     3.3 @@ -56,7 +56,7 @@
     3.4        addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
     3.5      val simpset0 =
     3.6        put_simpset HOL_basic_ss ctxt
     3.7 -      addsimps @{thms div_mult_mod_eq' Suc_eq_plus1 simp_thms}
     3.8 +      addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1 simp_thms}
     3.9        |> fold Splitter.add_split @{thms split_zdiv split_zmod split_div' split_min split_max}
    3.10      (* Simp rules for changing (n::int) to int n *)
    3.11      val simpset1 =
     4.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Sun Oct 16 09:31:05 2016 +0200
     4.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sun Oct 16 09:31:05 2016 +0200
     4.3 @@ -31,7 +31,6 @@
     4.4               @{thm uminus_add_conv_diff [symmetric]}, @{thm "minus_divide_left"}]
     4.5  val comp_ths = distinct Thm.eq_thm (ths @ comp_arith @ @{thms simp_thms});
     4.6  
     4.7 -val div_mult_mod_eq' = @{thm "div_mult_mod_eq'"};
     4.8  val mod_add_eq = @{thm "mod_add_eq"} RS sym;
     4.9  
    4.10  fun prepare_for_mir q fm = 
    4.11 @@ -80,7 +79,7 @@
    4.12                          addsimps @{thms add.assoc add.commute add.left_commute}
    4.13                          addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
    4.14      val simpset0 = put_simpset HOL_basic_ss ctxt
    4.15 -      addsimps [div_mult_mod_eq', @{thm Suc_eq_plus1}]
    4.16 +      addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1}
    4.17        addsimps comp_ths
    4.18        |> fold Splitter.add_split
    4.19            [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"},
     5.1 --- a/src/HOL/Divides.thy	Sun Oct 16 09:31:05 2016 +0200
     5.2 +++ b/src/HOL/Divides.thy	Sun Oct 16 09:31:05 2016 +0200
     5.3 @@ -1387,12 +1387,7 @@
     5.4    qed
     5.5  qed
     5.6  
     5.7 -theorem div_mult_mod_eq' [nitpick_unfold]: "(m::nat) mod n = m - (m div n) * n"
     5.8 -  using div_mult_mod_eq [of m n] by arith
     5.9 -
    5.10 -lemma div_mod_equality': "(m::nat) div n * n = m - m mod n"
    5.11 -  using div_mult_mod_eq [of m n] by arith
    5.12 -(* FIXME: very similar to mult_div_cancel *)
    5.13 +declare minus_div_mult_eq_mod [symmetric, where ?'a = nat, nitpick_unfold]
    5.14  
    5.15  lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
    5.16    apply rule
     6.1 --- a/src/HOL/Library/RBT_Impl.thy	Sun Oct 16 09:31:05 2016 +0200
     6.2 +++ b/src/HOL/Library/RBT_Impl.thy	Sun Oct 16 09:31:05 2016 +0200
     6.3 @@ -1416,7 +1416,7 @@
     6.4          moreover note feven[unfolded feven_def]
     6.5            (* FIXME: why does by(rule feven[unfolded feven_def]) not work? *)
     6.6          ultimately have "P (2 * (n div 2)) kvs" by -
     6.7 -        thus ?thesis using True by (metis div_mod_equality' minus_nat.diff_0 mult.commute)
     6.8 +        thus ?thesis using True by (metis minus_mod_eq_div_mult [symmetric] minus_nat.diff_0 mult.commute)
     6.9        next
    6.10          case False note ge0
    6.11          moreover from "1.prems" have n2: "n div 2 \<le> length kvs" by simp
    6.12 @@ -1462,7 +1462,7 @@
    6.13          moreover note geven[unfolded geven_def]
    6.14          ultimately have "Q (2 * (n div 2)) kvs" by -
    6.15          thus ?thesis using True 
    6.16 -          by(metis div_mod_equality' minus_nat.diff_0 mult.commute)
    6.17 +          by(metis minus_mod_eq_div_mult [symmetric] minus_nat.diff_0 mult.commute)
    6.18        next
    6.19          case False note ge0
    6.20          moreover from "2.prems" have n2: "n div 2 \<le> length kvs" by simp
     7.1 --- a/src/HOL/Number_Theory/Eratosthenes.thy	Sun Oct 16 09:31:05 2016 +0200
     7.2 +++ b/src/HOL/Number_Theory/Eratosthenes.thy	Sun Oct 16 09:31:05 2016 +0200
     7.3 @@ -143,7 +143,7 @@
     7.4        then have "u + (w - u mod w) = w + (u - u mod w)"
     7.5          by simp
     7.6        then have "u + (w - u mod w) = w + u div w * w"
     7.7 -        by (simp add: div_mod_equality' [symmetric])
     7.8 +        by (simp add: minus_mod_eq_div_mult)
     7.9      }
    7.10      then have "w dvd v + w + r + (w - v mod w) \<longleftrightarrow> w dvd m + w + r + (w - m mod w)"
    7.11        by (simp add: add.assoc add.left_commute [of m] add.left_commute [of v]
     8.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:05 2016 +0200
     8.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:05 2016 +0200
     8.3 @@ -510,7 +510,7 @@
     8.4        also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r]
     8.5          by (simp add: algebra_simps)
     8.6        finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" .
     8.7 -    qed (auto simp: gcd_eucl_non_0 algebra_simps div_mod_equality')
     8.8 +    qed (auto simp: gcd_eucl_non_0 algebra_simps minus_mod_eq_div_mult [symmetric])
     8.9      finally show ?thesis .
    8.10    qed
    8.11  qed
     9.1 --- a/src/HOL/Old_Number_Theory/Pocklington.thy	Sun Oct 16 09:31:05 2016 +0200
     9.2 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Sun Oct 16 09:31:05 2016 +0200
     9.3 @@ -1241,8 +1241,8 @@
     9.4          unfolding mod_eq_0_iff by blast
     9.5        hence eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
     9.6        from qrn[symmetric] have qn1: "q dvd n - 1" unfolding dvd_def by auto
     9.7 -      from dvd_trans[OF p(2) qn1] div_mod_equality'[of "n - 1" p]
     9.8 -      have npp: "(n - 1) div p * p = n - 1" by (simp add: dvd_eq_mod_eq_0)
     9.9 +      with p(2) have npp: "(n - 1) div p * p = n - 1"
    9.10 +        by (auto intro: dvd_div_mult_self dvd_trans)
    9.11        with eq0 have "a^ (n - 1) = (n*s)^p"
    9.12          by (simp add: power_mult[symmetric])
    9.13        hence "1 = (n*s)^(Suc (p - 1)) mod n" using bqn p01 by simp
    10.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sun Oct 16 09:31:05 2016 +0200
    10.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sun Oct 16 09:31:05 2016 +0200
    10.3 @@ -835,7 +835,7 @@
    10.4     addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}])
    10.5  val splits_ss =
    10.6    simpset_of (put_simpset comp_ss @{context}
    10.7 -    addsimps [@{thm "div_mult_mod_eq'"}]
    10.8 +    addsimps [@{thm minus_div_mult_eq_mod [symmetric]}]
    10.9      |> fold Splitter.add_split
   10.10        [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
   10.11         @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
    11.1 --- a/src/HOL/Word/Word.thy	Sun Oct 16 09:31:05 2016 +0200
    11.2 +++ b/src/HOL/Word/Word.thy	Sun Oct 16 09:31:05 2016 +0200
    11.3 @@ -3867,7 +3867,7 @@
    11.4     apply clarsimp
    11.5    apply (clarsimp simp add : nth_append size_rcat_lem)
    11.6    apply (simp (no_asm_use) only:  mult_Suc [symmetric] 
    11.7 -         td_gal_lt_len less_Suc_eq_le div_mult_mod_eq')
    11.8 +         td_gal_lt_len less_Suc_eq_le minus_div_mult_eq_mod [symmetric])
    11.9    apply clarsimp
   11.10    done
   11.11