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.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.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