new simp rule
authorhaftmann
Thu Nov 23 13:00:00 2017 +0000 (6 months ago)
changeset 670836b2c0681ef28
parent 67082 4e4bea76e559
child 67084 e138d96ed083
new simp rule
src/HOL/Divides.thy
src/HOL/Euclidean_Division.thy
src/HOL/Number_Theory/Euler_Criterion.thy
src/HOL/Parity.thy
     1.1 --- a/src/HOL/Divides.thy	Tue Nov 21 17:18:10 2017 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Nov 23 13:00:00 2017 +0000
     1.3 @@ -904,11 +904,11 @@
     1.4    
     1.5  subsubsection \<open>Quotients of Signs\<close>
     1.6  
     1.7 -lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
     1.8 -by (simp add: divide_int_def)
     1.9 +lemma div_eq_minus1: "0 < b \<Longrightarrow> - 1 div b = - 1" for b :: int
    1.10 +  by (simp add: divide_int_def)
    1.11  
    1.12 -lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
    1.13 -by (simp add: modulo_int_def)
    1.14 +lemma zmod_minus1: "0 < b \<Longrightarrow> - 1 mod b = b - 1" for b :: int
    1.15 +  by (auto simp add: modulo_int_def)
    1.16  
    1.17  lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
    1.18  apply (subgoal_tac "a div b \<le> -1", force)
     2.1 --- a/src/HOL/Euclidean_Division.thy	Tue Nov 21 17:18:10 2017 +0100
     2.2 +++ b/src/HOL/Euclidean_Division.thy	Thu Nov 23 13:00:00 2017 +0000
     2.3 @@ -1084,6 +1084,10 @@
     2.4    and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
     2.5    by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+
     2.6  
     2.7 +lemma Suc_0_mod_eq [simp]:
     2.8 +  "Suc 0 mod n = of_bool (n \<noteq> Suc 0)"
     2.9 +  by (cases n) simp_all
    2.10 +
    2.11  context
    2.12    fixes m n q :: nat
    2.13  begin
     3.1 --- a/src/HOL/Number_Theory/Euler_Criterion.thy	Tue Nov 21 17:18:10 2017 +0100
     3.2 +++ b/src/HOL/Number_Theory/Euler_Criterion.thy	Thu Nov 23 13:00:00 2017 +0000
     3.3 @@ -13,9 +13,24 @@
     3.4    assumes p_a_relprime: "[a \<noteq> 0](mod p)"
     3.5  begin
     3.6  
     3.7 -private lemma odd_p: "odd p" using p_ge_2 p_prime prime_odd_nat by blast
     3.8 +private lemma odd_p: "odd p"
     3.9 +  using p_ge_2 p_prime prime_odd_nat by blast
    3.10  
    3.11 -private lemma p_minus_1_int: "int (p - 1) = int p - 1" using p_prime prime_ge_1_nat by force
    3.12 +private lemma p_minus_1_int:
    3.13 +  "int (p - 1) = int p - 1" using p_prime prime_ge_1_nat by force
    3.14 +
    3.15 +private lemma p_not_eq_Suc_0 [simp]:
    3.16 +  "p \<noteq> Suc 0"
    3.17 +  using p_ge_2 by simp
    3.18 +
    3.19 +private lemma one_mod_int_p_eq [simp]:
    3.20 +  "1 mod int p = 1"
    3.21 +proof -
    3.22 +  from p_ge_2 have "int 1 mod int p = int 1"
    3.23 +    by simp
    3.24 +  then show ?thesis
    3.25 +    by simp
    3.26 +qed
    3.27  
    3.28  private lemma E_1:
    3.29    assumes "QuadRes (int p) a"
    3.30 @@ -41,7 +56,7 @@
    3.31      moreover from odd_p have "\<bar>b\<bar> ^ (p - Suc 0) = b ^ (p - Suc 0)"
    3.32        by (simp add: power_even_abs)
    3.33      ultimately show ?thesis
    3.34 -      by (simp add: zmod_int cong_def)
    3.35 +      by (auto simp add: cong_def zmod_int)
    3.36    qed
    3.37    ultimately show ?thesis
    3.38      by (auto intro: cong_trans)
    3.39 @@ -68,8 +83,10 @@
    3.40      by (simp add: ac_simps)
    3.41    then obtain y' where y': "[x * y' = 1] (mod p)" using cong_solve_coprime_int by blast
    3.42    moreover define y where "y = y' * a mod p"
    3.43 -  ultimately have "[x * y = a] (mod p)" using mod_mult_right_eq[of x "y' * a" p]
    3.44 -    cong_scalar_right [of "x * y'"] unfolding cong_def mult.assoc by auto
    3.45 +  ultimately have "[x * y = a] (mod p)"
    3.46 +    using mod_mult_right_eq [of x "y' * a" p]
    3.47 +    cong_scalar_right [of "x * y'" 1 "int p" a]
    3.48 +    by (auto simp add: cong_def ac_simps)
    3.49    moreover have "y \<in> {0 .. int p - 1}" unfolding y_def using p_ge_2 by auto
    3.50    hence "y \<in> S1" using calculation cong_altdef_int p_a_relprime S1_def by auto
    3.51    ultimately have "P x y" unfolding P_def by blast
     4.1 --- a/src/HOL/Parity.thy	Tue Nov 21 17:18:10 2017 +0100
     4.2 +++ b/src/HOL/Parity.thy	Thu Nov 23 13:00:00 2017 +0000
     4.3 @@ -191,12 +191,11 @@
     4.4  lemma one_mod_2_pow_eq [simp]:
     4.5    "1 mod (2 ^ n) = of_bool (n > 0)"
     4.6  proof -
     4.7 -  have "1 mod (2 ^ n) = (of_bool (n > 0) :: nat)"
     4.8 -    by (induct n) (simp_all add: mod_mult2_eq)
     4.9 -  then have "of_nat (1 mod (2 ^ n)) = of_bool (n > 0)"
    4.10 +  have "1 mod (2 ^ n) = of_nat (1 mod (2 ^ n))"
    4.11 +    using of_nat_mod [of 1 "2 ^ n"] by simp
    4.12 +  also have "\<dots> = of_bool (n > 0)"
    4.13      by simp
    4.14 -  then show ?thesis
    4.15 -    by (simp add: of_nat_mod)
    4.16 +  finally show ?thesis .
    4.17  qed
    4.18  
    4.19  lemma even_of_nat [simp]: