src/HOL/Divides.thy
changeset 58786 fa5b67fb70ad
parent 58778 e29cae8eab1f
child 58834 773b378d9313
     1.1 --- a/src/HOL/Divides.thy	Sun Oct 26 15:57:10 2014 +0100
     1.2 +++ b/src/HOL/Divides.thy	Sat Oct 25 19:20:28 2014 +0200
     1.3 @@ -321,7 +321,7 @@
     1.4    also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
     1.5      by (simp only: mod_mult_self1)
     1.6    also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
     1.7 -    by (simp only: ac_simps ac_simps)
     1.8 +    by (simp only: ac_simps)
     1.9    also have "\<dots> = a mod c"
    1.10      by (simp only: mod_div_equality)
    1.11    finally show ?thesis .
    1.12 @@ -509,7 +509,7 @@
    1.13  
    1.14  class semiring_div_parity = semiring_div + semiring_numeral +
    1.15    assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
    1.16 -  assumes one_mod_two_eq_one: "1 mod 2 = 1"
    1.17 +  assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
    1.18    assumes zero_not_eq_two: "0 \<noteq> 2"
    1.19  begin
    1.20  
    1.21 @@ -519,15 +519,7 @@
    1.22    shows P
    1.23    using assms parity by blast
    1.24  
    1.25 -lemma not_mod_2_eq_0_eq_1 [simp]:
    1.26 -  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
    1.27 -  by (cases a rule: parity_cases) simp_all
    1.28 -
    1.29 -lemma not_mod_2_eq_1_eq_0 [simp]:
    1.30 -  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
    1.31 -  by (cases a rule: parity_cases) simp_all
    1.32 -
    1.33 -lemma one_div_two_eq_zero [simp]: -- \<open>FIXME move\<close>
    1.34 +lemma one_div_two_eq_zero [simp]:
    1.35    "1 div 2 = 0"
    1.36  proof (cases "2 = 0")
    1.37    case True then show ?thesis by simp
    1.38 @@ -540,6 +532,14 @@
    1.39    with False show ?thesis by auto
    1.40  qed
    1.41  
    1.42 +lemma not_mod_2_eq_0_eq_1 [simp]:
    1.43 +  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
    1.44 +  by (cases a rule: parity_cases) simp_all
    1.45 +
    1.46 +lemma not_mod_2_eq_1_eq_0 [simp]:
    1.47 +  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
    1.48 +  by (cases a rule: parity_cases) simp_all
    1.49 +
    1.50  subclass semiring_parity
    1.51  proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
    1.52    fix a b c
    1.53 @@ -1148,11 +1148,15 @@
    1.54  lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
    1.55  by (auto simp add: mult.commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
    1.56  
    1.57 +instance nat :: semiring_numeral_div
    1.58 +  by intro_classes (auto intro: div_positive simp add: mult_div_cancel mod_mult2_eq div_mult2_eq)
    1.59 +
    1.60  
    1.61  subsubsection {* Further Facts about Quotient and Remainder *}
    1.62  
    1.63 -lemma div_1 [simp]: "m div Suc 0 = m"
    1.64 -by (induct m) (simp_all add: div_geq)
    1.65 +lemma div_1 [simp]:
    1.66 +  "m div Suc 0 = m"
    1.67 +  using div_by_1 [of m] by simp
    1.68  
    1.69  (* Monotonicity of div in first argument *)
    1.70  lemma div_le_mono [rule_format (no_asm)]:
    1.71 @@ -1324,7 +1328,7 @@
    1.72      proof (simp, intro allI impI)
    1.73        fix i j
    1.74        assume "n = k*i + j" "j < k"
    1.75 -      thus "P j" using not0 P by(simp add:ac_simps ac_simps)
    1.76 +      thus "P j" using not0 P by (simp add: ac_simps)
    1.77      qed
    1.78    qed
    1.79  next
    1.80 @@ -1480,7 +1484,6 @@
    1.81  lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
    1.82  lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
    1.83  
    1.84 -
    1.85  lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
    1.86  apply (induct "m")
    1.87  apply (simp_all add: mod_Suc)
    1.88 @@ -1500,10 +1503,6 @@
    1.89    from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp 
    1.90  qed
    1.91  
    1.92 -  (* Potential use of algebra : Equality modulo n*)
    1.93 -lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)"
    1.94 -by (simp add: ac_simps ac_simps)
    1.95 -
    1.96  lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
    1.97  proof -
    1.98    have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
    1.99 @@ -1519,11 +1518,8 @@
   1.100  lemma mod_2_not_eq_zero_eq_one_nat:
   1.101    fixes n :: nat
   1.102    shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
   1.103 -  by simp
   1.104 -
   1.105 -instance nat :: semiring_numeral_div
   1.106 -  by intro_classes (auto intro: div_positive simp add: mult_div_cancel mod_mult2_eq div_mult2_eq)
   1.107 -
   1.108 +  by (fact not_mod_2_eq_0_eq_1)
   1.109 +  
   1.110  lemma even_Suc_div_two [simp]:
   1.111    "even n \<Longrightarrow> Suc n div 2 = n div 2"
   1.112    using even_succ_div_two [of n] by simp
   1.113 @@ -2554,6 +2550,12 @@
   1.114    using zmod_zdiv_equality[where a="m" and b="n"]
   1.115    by (simp add: algebra_simps) (* FIXME: generalize *)
   1.116  
   1.117 +instance int :: semiring_numeral_div
   1.118 +  by intro_classes (auto intro: zmod_le_nonneg_dividend
   1.119 +    simp add: zmult_div_cancel
   1.120 +    pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial
   1.121 +    zmod_zmult2_eq zdiv_zmult2_eq)
   1.122 +  
   1.123  lemma zdiv_int: "int (a div b) = (int a) div (int b)"
   1.124  apply (subst split_div, auto)
   1.125  apply (subst split_zdiv, auto)
   1.126 @@ -2725,12 +2727,6 @@
   1.127    "Suc 0 mod numeral v' = nat (1 mod numeral v')"
   1.128    by (subst nat_mod_distrib) simp_all
   1.129  
   1.130 -instance int :: semiring_numeral_div
   1.131 -  by intro_classes (auto intro: zmod_le_nonneg_dividend
   1.132 -    simp add: zmult_div_cancel
   1.133 -    pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial
   1.134 -    zmod_zmult2_eq zdiv_zmult2_eq)
   1.135 -
   1.136  
   1.137  subsubsection {* Tools setup *}
   1.138