# HG changeset patch
# User haftmann
# Date 1508478370 -7200
# Node ID 960509bfd47e388e87495b80cb72544f50a6c4b8
# Parent  d3d508b23d1d06da2d7c87724a98d8523b992c3e
added lemmas and tuned proofs

diff -r d3d508b23d1d -r 960509bfd47e src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Thu Oct 19 17:16:13 2017 +0100
+++ b/src/HOL/Code_Numeral.thy	Fri Oct 20 07:46:10 2017 +0200
@@ -578,16 +578,15 @@
        l'' = l' + l'
      in if j = 0 then l'' else l'' + 1)"
 proof -
-  obtain j where "k = integer_of_int j"
+  obtain j where k: "k = integer_of_int j"
   proof
     show "k = integer_of_int (int_of_integer k)" by simp
   qed
-  moreover have "2 * (j div 2) = j - j mod 2"
-    by (simp add: minus_mod_eq_mult_div [symmetric] mult.commute)
-  ultimately show ?thesis
-    by (auto simp add: split_def Let_def modulo_integer_def nat_of_integer_def not_le
-      nat_add_distrib [symmetric] Suc_nat_eq_nat_zadd1)
-      (auto simp add: mult_2 [symmetric])
+  have *: "nat j mod 2 = nat_of_integer (of_int j mod 2)" if "j \<ge> 0"
+    using that by transfer (simp add: nat_mod_distrib)
+  from k show ?thesis
+    by (auto simp add: split_def Let_def nat_of_integer_def nat_div_distrib mult_2 [symmetric]
+      minus_mod_eq_mult_div [symmetric] *)
 qed
 
 lemma int_of_integer_code [code]:
diff -r d3d508b23d1d -r 960509bfd47e src/HOL/Computational_Algebra/Normalized_Fraction.thy
--- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Thu Oct 19 17:16:13 2017 +0100
+++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Fri Oct 20 07:46:10 2017 +0200
@@ -239,7 +239,6 @@
   
 lemma normalize_quot_eq_0_iff [simp]: "fst (normalize_quot x) = 0 \<longleftrightarrow> fst x = 0 \<or> snd x = 0"
   by (auto simp: normalize_quot_def case_prod_unfold Let_def div_mult_unit2 dvd_div_eq_0_iff)
-  find_theorems "_ div _ = 0"
   
 lemma fst_quot_of_fract_0_imp: "fst (quot_of_fract x) = 0 \<Longrightarrow> snd (quot_of_fract x) = 1"
   by transfer auto
diff -r d3d508b23d1d -r 960509bfd47e src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Oct 19 17:16:13 2017 +0100
+++ b/src/HOL/Divides.thy	Fri Oct 20 07:46:10 2017 +0200
@@ -501,15 +501,13 @@
 
 subsubsection \<open>General Properties of div and mod\<close>
 
-lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
-apply (rule div_int_unique)
-apply (auto simp add: eucl_rel_int_iff)
-done
+lemma div_pos_pos_trivial [simp]:
+  "k div l = 0" if "k \<ge> 0" and "k < l" for k l :: int
+  using that by (auto intro!: div_int_unique [of _ _ _ k] simp add: eucl_rel_int_iff)
 
-lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
-apply (rule div_int_unique)
-apply (auto simp add: eucl_rel_int_iff)
-done
+lemma div_neg_neg_trivial [simp]:
+  "k div l = 0" if "k \<le> 0" and "l < k" for k l :: int
+  using that by (auto intro!: div_int_unique [of _ _ _ k] simp add: eucl_rel_int_iff)
 
 lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
 apply (rule div_int_unique)
@@ -522,15 +520,13 @@
 
 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
 
-lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
-apply (rule_tac q = 0 in mod_int_unique)
-apply (auto simp add: eucl_rel_int_iff)
-done
+lemma mod_pos_pos_trivial [simp]:
+  "k mod l = k" if "k \<ge> 0" and "k < l" for k l :: int
+  using that by (auto intro!: mod_int_unique [of _ _ 0] simp add: eucl_rel_int_iff)
 
-lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
-apply (rule_tac q = 0 in mod_int_unique)
-apply (auto simp add: eucl_rel_int_iff)
-done
+lemma mod_neg_neg_trivial [simp]:
+  "k mod l = k" if "k \<le> 0" and "l < k" for k l :: int
+  using that by (auto intro!: mod_int_unique [of _ _ 0] simp add: eucl_rel_int_iff)
 
 lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
 apply (rule_tac q = "-1" in mod_int_unique)
@@ -775,38 +771,22 @@
 lemma split_pos_lemma:
  "0<k ==>
     P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
-apply (rule iffI, clarify)
- apply (erule_tac P="P x y" for x y in rev_mp)
- apply (subst mod_add_eq [symmetric])
- apply (subst zdiv_zadd1_eq)
- apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
-txt\<open>converse direction\<close>
-apply (drule_tac x = "n div k" in spec)
-apply (drule_tac x = "n mod k" in spec, simp)
-done
+  by auto
 
 lemma split_neg_lemma:
  "k<0 ==>
     P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
-apply (rule iffI, clarify)
- apply (erule_tac P="P x y" for x y in rev_mp)
- apply (subst mod_add_eq [symmetric])
- apply (subst zdiv_zadd1_eq)
- apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
-txt\<open>converse direction\<close>
-apply (drule_tac x = "n div k" in spec)
-apply (drule_tac x = "n mod k" in spec, simp)
-done
+  by auto
 
 lemma split_zdiv:
  "P(n div k :: int) =
   ((k = 0 --> P 0) &
    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
-apply (case_tac "k=0", simp)
+  apply (cases "k = 0")
+  apply simp
 apply (simp only: linorder_neq_iff)
-apply (erule disjE)
- apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]
+ apply (auto simp add: split_pos_lemma [of concl: "%x y. P x"]
                       split_neg_lemma [of concl: "%x y. P x"])
 done
 
@@ -897,14 +877,17 @@
   by (rule pos_zmod_mult_2, simp)
 
 lemma zdiv_eq_0_iff:
- "(i::int) div k = 0 \<longleftrightarrow> k=0 \<or> 0\<le>i \<and> i<k \<or> i\<le>0 \<and> k<i" (is "?L = ?R")
+  "i div k = 0 \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i" (is "?L = ?R")
+  for i k :: int
 proof
   assume ?L
-  have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp
-  with \<open>?L\<close> show ?R by blast
+  moreover have "?L \<longrightarrow> ?R"
+    by (rule split_zdiv [THEN iffD2]) simp
+  ultimately show ?R
+    by blast
 next
-  assume ?R thus ?L
-    by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
+  assume ?R then show ?L
+    by auto
 qed
 
 lemma zmod_trival_iff:
@@ -1004,7 +987,7 @@
 
 instance
   by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
-    pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial zmod_zmult2_eq zdiv_zmult2_eq)
+    pos_imp_zdiv_pos_iff zmod_zmult2_eq zdiv_zmult2_eq)
 
 end
 
diff -r d3d508b23d1d -r 960509bfd47e src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Thu Oct 19 17:16:13 2017 +0100
+++ b/src/HOL/Euclidean_Division.thy	Fri Oct 20 07:46:10 2017 +0200
@@ -128,6 +128,18 @@
 end
 
 class euclidean_ring = idom_modulo + euclidean_semiring
+begin
+
+lemma dvd_diff_commute:
+  "a dvd c - b \<longleftrightarrow> a dvd b - c"
+proof -
+  have "a dvd c - b \<longleftrightarrow> a dvd (c - b) * - 1"
+    by (subst dvd_mult_unit_iff) simp_all
+  then show ?thesis
+    by simp
+qed
+ 
+end
 
 
 subsection \<open>Euclidean (semi)rings with cancel rules\<close>
@@ -711,6 +723,21 @@
     by simp
 qed
 
+lemma div_eq_0_iff:
+  "a div b = 0 \<longleftrightarrow> euclidean_size a < euclidean_size b \<or> b = 0" (is "_ \<longleftrightarrow> ?P")
+  if "division_segment a = division_segment b"
+proof
+  assume ?P
+  with that show "a div b = 0"
+    by (cases "b = 0") (auto intro: div_eqI)
+next
+  assume "a div b = 0"
+  then have "a mod b = a"
+    using div_mult_mod_eq [of a b] by simp
+  with mod_size_less [of b a] show ?P
+    by auto
+qed
+
 end
 
 class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
@@ -954,7 +981,7 @@
 
 lemma div_eq_0_iff:
   "m div n = 0 \<longleftrightarrow> m < n \<or> n = 0" for m n :: nat
-  by (simp add: div_if)
+  by (simp add: div_eq_0_iff)
 
 lemma div_greater_zero_iff:
   "m div n > 0 \<longleftrightarrow> n \<le> m \<and> n > 0" for m n :: nat
diff -r d3d508b23d1d -r 960509bfd47e src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Oct 19 17:16:13 2017 +0100
+++ b/src/HOL/Int.thy	Fri Oct 20 07:46:10 2017 +0200
@@ -552,6 +552,10 @@
 lemma diff_nat_numeral [simp]: "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
   by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
 
+lemma nat_abs_triangle_ineq:
+  "nat \<bar>k + l\<bar> \<le> nat \<bar>k\<bar> + nat \<bar>l\<bar>"
+  by (simp add: nat_add_distrib [symmetric] nat_le_eq_zle abs_triangle_ineq)
+
 lemma nat_of_bool [simp]:
   "nat (of_bool P) = of_bool P"
   by auto
diff -r d3d508b23d1d -r 960509bfd47e src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Thu Oct 19 17:16:13 2017 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Fri Oct 20 07:46:10 2017 +0200
@@ -125,7 +125,6 @@
 lemma Rep_mod: "Rep x mod n = Rep x"
 apply (rule_tac x=x in type_definition.Abs_cases [OF type])
 apply (simp add: type_definition.Abs_inverse [OF type])
-apply (simp add: mod_pos_pos_trivial)
 done
 
 lemmas Rep_simps =
diff -r d3d508b23d1d -r 960509bfd47e src/HOL/Word/Word_Miscellaneous.thy
--- a/src/HOL/Word/Word_Miscellaneous.thy	Thu Oct 19 17:16:13 2017 +0100
+++ b/src/HOL/Word/Word_Miscellaneous.thy	Fri Oct 20 07:46:10 2017 +0200
@@ -276,16 +276,7 @@
 
 lemma mod_power_lem: "a > 1 \<Longrightarrow> a ^ n mod a ^ m = (if m \<le> n then 0 else a ^ n)"
   for a :: int
-  apply clarsimp
-  apply safe
-   apply (simp add: dvd_eq_mod_eq_0 [symmetric])
-   apply (drule le_iff_add [THEN iffD1])
-   apply (force simp: power_add)
-  apply (rule mod_pos_pos_trivial)
-   apply (simp)
-  apply (rule power_strict_increasing)
-   apply auto
-  done
+  by (simp add: mod_eq_0_iff le_imp_power_dvd)
 
 lemma pl_pl_rels: "a + b = c + d \<Longrightarrow> a \<ge> c \<and> b \<le> d \<or> a \<le> c \<and> b \<ge> d"
   for a b c d :: nat