# HG changeset patch
# User haftmann
# Date 1414257628 -7200
# Node ID fa5b67fb70adeeaba4e844de1e3d434ab109d68b
# Parent  e7d2b46520e057a56ff02fcbf06d3c71d5dda8df
more simp rules;
slight proof tuning

diff -r e7d2b46520e0 -r fa5b67fb70ad src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Oct 26 15:57:10 2014 +0100
+++ b/src/HOL/Divides.thy	Sat Oct 25 19:20:28 2014 +0200
@@ -321,7 +321,7 @@
   also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
     by (simp only: mod_mult_self1)
   also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
-    by (simp only: ac_simps ac_simps)
+    by (simp only: ac_simps)
   also have "\<dots> = a mod c"
     by (simp only: mod_div_equality)
   finally show ?thesis .
@@ -509,7 +509,7 @@
 
 class semiring_div_parity = semiring_div + semiring_numeral +
   assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
-  assumes one_mod_two_eq_one: "1 mod 2 = 1"
+  assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
   assumes zero_not_eq_two: "0 \<noteq> 2"
 begin
 
@@ -519,15 +519,7 @@
   shows P
   using assms parity by blast
 
-lemma not_mod_2_eq_0_eq_1 [simp]:
-  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
-  by (cases a rule: parity_cases) simp_all
-
-lemma not_mod_2_eq_1_eq_0 [simp]:
-  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
-  by (cases a rule: parity_cases) simp_all
-
-lemma one_div_two_eq_zero [simp]: -- \<open>FIXME move\<close>
+lemma one_div_two_eq_zero [simp]:
   "1 div 2 = 0"
 proof (cases "2 = 0")
   case True then show ?thesis by simp
@@ -540,6 +532,14 @@
   with False show ?thesis by auto
 qed
 
+lemma not_mod_2_eq_0_eq_1 [simp]:
+  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
+  by (cases a rule: parity_cases) simp_all
+
+lemma not_mod_2_eq_1_eq_0 [simp]:
+  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
+  by (cases a rule: parity_cases) simp_all
+
 subclass semiring_parity
 proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
   fix a b c
@@ -1148,11 +1148,15 @@
 lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
 by (auto simp add: mult.commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
 
+instance nat :: semiring_numeral_div
+  by intro_classes (auto intro: div_positive simp add: mult_div_cancel mod_mult2_eq div_mult2_eq)
+
 
 subsubsection {* Further Facts about Quotient and Remainder *}
 
-lemma div_1 [simp]: "m div Suc 0 = m"
-by (induct m) (simp_all add: div_geq)
+lemma div_1 [simp]:
+  "m div Suc 0 = m"
+  using div_by_1 [of m] by simp
 
 (* Monotonicity of div in first argument *)
 lemma div_le_mono [rule_format (no_asm)]:
@@ -1324,7 +1328,7 @@
     proof (simp, intro allI impI)
       fix i j
       assume "n = k*i + j" "j < k"
-      thus "P j" using not0 P by(simp add:ac_simps ac_simps)
+      thus "P j" using not0 P by (simp add: ac_simps)
     qed
   qed
 next
@@ -1480,7 +1484,6 @@
 lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
 lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
 
-
 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
 apply (induct "m")
 apply (simp_all add: mod_Suc)
@@ -1500,10 +1503,6 @@
   from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp 
 qed
 
-  (* Potential use of algebra : Equality modulo n*)
-lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)"
-by (simp add: ac_simps ac_simps)
-
 lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
 proof -
   have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
@@ -1519,11 +1518,8 @@
 lemma mod_2_not_eq_zero_eq_one_nat:
   fixes n :: nat
   shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
-  by simp
-
-instance nat :: semiring_numeral_div
-  by intro_classes (auto intro: div_positive simp add: mult_div_cancel mod_mult2_eq div_mult2_eq)
-
+  by (fact not_mod_2_eq_0_eq_1)
+  
 lemma even_Suc_div_two [simp]:
   "even n \<Longrightarrow> Suc n div 2 = n div 2"
   using even_succ_div_two [of n] by simp
@@ -2554,6 +2550,12 @@
   using zmod_zdiv_equality[where a="m" and b="n"]
   by (simp add: algebra_simps) (* FIXME: generalize *)
 
+instance int :: semiring_numeral_div
+  by intro_classes (auto intro: zmod_le_nonneg_dividend
+    simp add: zmult_div_cancel
+    pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial
+    zmod_zmult2_eq zdiv_zmult2_eq)
+  
 lemma zdiv_int: "int (a div b) = (int a) div (int b)"
 apply (subst split_div, auto)
 apply (subst split_zdiv, auto)
@@ -2725,12 +2727,6 @@
   "Suc 0 mod numeral v' = nat (1 mod numeral v')"
   by (subst nat_mod_distrib) simp_all
 
-instance int :: semiring_numeral_div
-  by intro_classes (auto intro: zmod_le_nonneg_dividend
-    simp add: zmult_div_cancel
-    pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial
-    zmod_zmult2_eq zdiv_zmult2_eq)
-
 
 subsubsection {* Tools setup *}