# HG changeset patch
# User haftmann
# Date 1660888152 0
# Node ID 83e4b6a5e7de0b243e91f9392dd530ef77c784b5
# Parent  714fad33252e41c373ac486309cff7c8621dfcc4
streamlined theorems

diff -r 714fad33252e -r 83e4b6a5e7de src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Aug 19 05:49:11 2022 +0000
+++ b/src/HOL/Divides.thy	Fri Aug 19 05:49:12 2022 +0000
@@ -11,112 +11,8 @@
 
 subsection \<open>More on division\<close>
 
-subsubsection \<open>Splitting Rules for div and mod\<close>
-
-text\<open>The proofs of the two lemmas below are essentially identical\<close>
-
-lemma split_pos_lemma:
- "0<k \<Longrightarrow>
-    P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j \<and> j<k \<and> n = k*i + j \<longrightarrow> P i j)"
-  by auto
-
-lemma split_neg_lemma:
- "k<0 \<Longrightarrow>
-    P(n div k :: int)(n mod k) = (\<forall>i j. k<j \<and> j\<le>0 \<and> n = k*i + j \<longrightarrow> P i j)"
-  by auto
-
-lemma split_zdiv:
-  \<open>P (n div k) \<longleftrightarrow>
-    (k = 0 \<longrightarrow> P 0) \<and>
-    (0 < k \<longrightarrow> (\<forall>i j. 0 \<le> j \<and> j < k \<and> n = k * i + j \<longrightarrow> P i)) \<and>
-    (k < 0 \<longrightarrow> (\<forall>i j. k < j \<and> j \<le> 0 \<and> n = k * i + j \<longrightarrow> P i))\<close> for n k :: int
-proof (cases \<open>k = 0\<close>)
-  case True
-  then show ?thesis
-    by simp
-next
-  case False
-  then have \<open>k < 0 \<or> 0 < k\<close>
-    by auto
-  then show ?thesis
-    by (auto simp add: split_pos_lemma [of concl: "\<lambda>x y. P x"] split_neg_lemma [of concl: "\<lambda>x y. P x"])
-qed
-
-lemma split_zmod:
-  \<open>P (n mod k) \<longleftrightarrow>
-    (k = 0 \<longrightarrow> P n) \<and>
-    (0 < k \<longrightarrow> (\<forall>i j. 0 \<le> j \<and> j < k \<and> n = k * i + j \<longrightarrow> P j)) \<and>
-    (k < 0 \<longrightarrow> (\<forall>i j. k < j \<and> j \<le> 0 \<and> n = k * i + j \<longrightarrow> P j))\<close> for n k :: int
-proof (cases \<open>k = 0\<close>)
-  case True
-  then show ?thesis
-    by simp
-next
-  case False
-  then have \<open>k < 0 \<or> 0 < k\<close>
-    by auto
-  then show ?thesis
-    by (auto simp add: split_pos_lemma [of concl: "\<lambda>x y. P y"] split_neg_lemma [of concl: "\<lambda>x y. P y"])
-qed
-
-text \<open>Enable (lin)arith to deal with \<^const>\<open>divide\<close> and \<^const>\<open>modulo\<close>
-  when these are applied to some constant that is of the form
-  \<^term>\<open>numeral k\<close>:\<close>
-declare split_zdiv [of _ _ \<open>numeral n\<close>, linarith_split] for n
-declare split_zdiv [of _ _ \<open>- numeral n\<close>, linarith_split] for n
-declare split_zmod [of _ _ \<open>numeral n\<close>, linarith_split] for n
-declare split_zmod [of _ _ \<open>- numeral n\<close>, linarith_split] for n
-
-lemma half_nonnegative_int_iff [simp]:
-  \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
-  by auto
-
-lemma half_negative_int_iff [simp]:
-  \<open>k div 2 < 0 \<longleftrightarrow> k < 0\<close> for k :: int
-  by auto
-
-lemma zdiv_eq_0_iff:
-  "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
-  moreover have "?L \<longrightarrow> ?R"
-    by (rule split_zdiv [THEN iffD2]) simp
-  ultimately show ?R
-    by blast
-next
-  assume ?R then show ?L
-    by auto
-qed
-
-lemma zmod_trivial_iff:
-  fixes i k :: int
-  shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
-proof -
-  have "i mod k = i \<longleftrightarrow> i div k = 0"
-    using div_mult_mod_eq [of i k] by safe auto
-  with zdiv_eq_0_iff
-  show ?thesis
-    by simp
-qed
-
-
 subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
 
-inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
-  where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
-  | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
-  | eucl_rel_int_remainderI: "sgn r = sgn l \<Longrightarrow> \<bar>r\<bar> < \<bar>l\<bar>
-      \<Longrightarrow> k = q * l + r \<Longrightarrow> eucl_rel_int k l (q, r)"
-
-lemma eucl_rel_int_iff:    
-  "eucl_rel_int k l (q, r) \<longleftrightarrow> 
-    k = l * q + r \<and>
-     (if 0 < l then 0 \<le> r \<and> r < l else if l < 0 then l < r \<and> r \<le> 0 else q = 0)"
-  by (cases "r = 0")
-    (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI
-    simp add: ac_simps sgn_1_pos sgn_1_neg)
-
 lemma unique_quotient_lemma:
   assumes "b * q' + r' \<le> b * q + r" "0 \<le> r'" "r' < b" "r < b" shows "q' \<le> (q::int)"
 proof -
@@ -134,61 +30,6 @@
   "b * q' + r' \<le> b*q + r \<Longrightarrow> r \<le> 0 \<Longrightarrow> b < r \<Longrightarrow> b < r' \<Longrightarrow> q \<le> (q'::int)"
   using unique_quotient_lemma[where b = "-b" and r = "-r'" and r'="-r"] by auto
 
-lemma unique_quotient:
-  "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
-  apply (rule order_antisym)
-   apply (simp_all add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
-     apply (blast intro: order_eq_refl [THEN unique_quotient_lemma] order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
-  done
-
-lemma unique_remainder:
-  assumes "eucl_rel_int a b (q, r)"
-    and "eucl_rel_int a b (q', r')"
-  shows "r = r'"
-proof -
-  have "q = q'"
-    using assms by (blast intro: unique_quotient)
-  then show "r = r'"
-    using assms by (simp add: eucl_rel_int_iff)
-qed
-
-lemma eucl_rel_int:
-  "eucl_rel_int k l (k div l, k mod l)"
-proof (cases k rule: int_cases3)
-  case zero
-  then show ?thesis
-    by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def)
-next
-  case (pos n)
-  then show ?thesis
-    using div_mult_mod_eq [of n]
-    by (cases l rule: int_cases3)
-      (auto simp del: of_nat_mult of_nat_add
-        simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
-        eucl_rel_int_iff divide_int_def modulo_int_def)
-next
-  case (neg n)
-  then show ?thesis
-    using div_mult_mod_eq [of n]
-    by (cases l rule: int_cases3)
-      (auto simp del: of_nat_mult of_nat_add
-        simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
-        eucl_rel_int_iff divide_int_def modulo_int_def)
-qed
-
-lemma divmod_int_unique:
-  assumes "eucl_rel_int k l (q, r)"
-  shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
-  using assms eucl_rel_int [of k l]
-  using unique_quotient [of k l] unique_remainder [of k l]
-  by auto
-
-lemma zminus1_lemma:
-     "eucl_rel_int a b (q, r) ==> b \<noteq> 0
-      ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
-                          if r=0 then 0 else b-r)"
-by (force simp add: eucl_rel_int_iff right_diff_distrib)
-
 lemma zdiv_mono1:
   \<open>a div b \<le> a' div b\<close>
   if \<open>a \<le> a'\<close> \<open>0 < b\<close>
@@ -272,6 +113,72 @@
     by simp
 qed (use assms in auto)
 
+
+subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
+
+inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
+  where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
+  | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
+  | eucl_rel_int_remainderI: "sgn r = sgn l \<Longrightarrow> \<bar>r\<bar> < \<bar>l\<bar>
+      \<Longrightarrow> k = q * l + r \<Longrightarrow> eucl_rel_int k l (q, r)"
+
+lemma eucl_rel_int_iff:    
+  "eucl_rel_int k l (q, r) \<longleftrightarrow> 
+    k = l * q + r \<and>
+     (if 0 < l then 0 \<le> r \<and> r < l else if l < 0 then l < r \<and> r \<le> 0 else q = 0)"
+  by (cases "r = 0")
+    (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI
+    simp add: ac_simps sgn_1_pos sgn_1_neg)
+
+lemma unique_quotient:
+  "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
+  apply (rule order_antisym)
+   apply (simp_all add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
+     apply (blast intro: order_eq_refl [THEN unique_quotient_lemma] order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
+  done
+
+lemma unique_remainder:
+  assumes "eucl_rel_int a b (q, r)"
+    and "eucl_rel_int a b (q', r')"
+  shows "r = r'"
+proof -
+  have "q = q'"
+    using assms by (blast intro: unique_quotient)
+  then show "r = r'"
+    using assms by (simp add: eucl_rel_int_iff)
+qed
+
+lemma eucl_rel_int:
+  "eucl_rel_int k l (k div l, k mod l)"
+proof (cases k rule: int_cases3)
+  case zero
+  then show ?thesis
+    by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def)
+next
+  case (pos n)
+  then show ?thesis
+    using div_mult_mod_eq [of n]
+    by (cases l rule: int_cases3)
+      (auto simp del: of_nat_mult of_nat_add
+        simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
+        eucl_rel_int_iff divide_int_def modulo_int_def)
+next
+  case (neg n)
+  then show ?thesis
+    using div_mult_mod_eq [of n]
+    by (cases l rule: int_cases3)
+      (auto simp del: of_nat_mult of_nat_add
+        simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
+        eucl_rel_int_iff divide_int_def modulo_int_def)
+qed
+
+lemma divmod_int_unique:
+  assumes "eucl_rel_int k l (q, r)"
+  shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
+  using assms eucl_rel_int [of k l]
+  using unique_quotient [of k l] unique_remainder [of k l]
+  by auto
+
 lemma div_pos_geq:
   fixes k l :: int
   assumes "0 < l" and "l \<le> k"
@@ -292,9 +199,6 @@
   with assms show ?thesis by simp
 qed
 
-
-subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
-
 lemma pos_eucl_rel_int_mult_2:
   assumes "0 \<le> b"
   assumes "eucl_rel_int a b (q, r)"
diff -r 714fad33252e -r 83e4b6a5e7de src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Fri Aug 19 05:49:11 2022 +0000
+++ b/src/HOL/Euclidean_Division.thy	Fri Aug 19 05:49:12 2022 +0000
@@ -937,6 +937,14 @@
 
 end
 
+lemma div_nat_eqI:
+  "m div n = q" if "n * q \<le> m" and "m < n * Suc q" for m n q :: nat
+  by (rule div_eqI [of _ "m - n * q"]) (use that in \<open>simp_all add: algebra_simps\<close>)
+
+lemma mod_nat_eqI:
+  "m mod n = r" if "r < n" and "r \<le> m" and "n dvd m - r" for m n r :: nat
+  by (rule mod_eqI [of _ _ "(m - r) div n"]) (use that in \<open>simp_all add: algebra_simps\<close>)
+
 text \<open>Tool support\<close>
 
 ML \<open>
@@ -967,14 +975,6 @@
 simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
   \<open>K Cancel_Div_Mod_Nat.proc\<close>
 
-lemma div_nat_eqI:
-  "m div n = q" if "n * q \<le> m" and "m < n * Suc q" for m n q :: nat
-  by (rule div_eqI [of _ "m - n * q"]) (use that in \<open>simp_all add: algebra_simps\<close>)
-
-lemma mod_nat_eqI:
-  "m mod n = r" if "r < n" and "r \<le> m" and "n dvd m - r" for m n r :: nat
-  by (rule mod_eqI [of _ _ "(m - r) div n"]) (use that in \<open>simp_all add: algebra_simps\<close>)
-
 lemma div_mult_self_is_m [simp]:
   "m * n div n = m" if "n > 0" for m n :: nat
   using that by simp
@@ -1030,6 +1030,41 @@
   and mod_less [simp]: "m mod n = m"
   if "m < n" for m n :: nat
   using that by (auto intro: div_eqI mod_eqI) 
+ 
+lemma split_div:
+  \<open>P (m div n) \<longleftrightarrow>
+    (n = 0 \<longrightarrow> P 0) \<and>
+    (n \<noteq> 0 \<longrightarrow> (\<forall>i j. j < n \<and> m = n * i + j \<longrightarrow> P i))\<close> (is ?div)
+  and split_mod:
+  \<open>Q (m mod n) \<longleftrightarrow>
+    (n = 0 \<longrightarrow> Q m) \<and>
+    (n \<noteq> 0 \<longrightarrow> (\<forall>i j. j < n \<and> m = n * i + j \<longrightarrow> Q j))\<close> (is ?mod)
+  for m n :: nat
+proof -
+  have *: \<open>R (m div n) (m mod n) \<longleftrightarrow>
+    (n = 0 \<longrightarrow> R 0 m) \<and>
+    (n \<noteq> 0 \<longrightarrow> (\<forall>i j. j < n \<and> m = n * i + j \<longrightarrow> R i j))\<close> for R
+    by (cases \<open>n = 0\<close>) auto
+  from * [of \<open>\<lambda>q _. P q\<close>] show ?div .
+  from * [of \<open>\<lambda>_ r. Q r\<close>] show ?mod .
+qed
+
+declare split_div [of _ _ \<open>numeral n\<close>, linarith_split] for n
+declare split_mod [of _ _ \<open>numeral n\<close>, linarith_split] for n
+
+lemma split_div':
+  "P (m div n) \<longleftrightarrow> n = 0 \<and> P 0 \<or> (\<exists>q. (n * q \<le> m \<and> m < n * Suc q) \<and> P q)"
+proof (cases "n = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  then have "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> m div n = q" for q
+    by (auto intro: div_nat_eqI dividend_less_times_div)
+  then show ?thesis
+    by auto
+qed
 
 lemma le_div_geq:
   "m div n = Suc ((m - n) div n)" if "0 < n" and "n \<le> m" for m n :: nat
@@ -1418,71 +1453,6 @@
     by simp
 qed
 
-lemma split_div:
-  "P (m div n) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (n \<noteq> 0 \<longrightarrow>
-     (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P i))"
-     (is "?P = ?Q") for m n :: nat
-proof (cases "n = 0")
-  case True
-  then show ?thesis
-    by simp
-next
-  case False
-  show ?thesis
-  proof
-    assume ?P
-    with False show ?Q
-      by auto
-  next
-    assume ?Q
-    with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P i"
-      by simp
-    with False show ?P
-      by (auto intro: * [of "m mod n"])
-  qed
-qed
-
-lemma split_div':
-  "P (m div n) \<longleftrightarrow> n = 0 \<and> P 0 \<or> (\<exists>q. (n * q \<le> m \<and> m < n * Suc q) \<and> P q)"
-proof (cases "n = 0")
-  case True
-  then show ?thesis
-    by simp
-next
-  case False
-  then have "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> m div n = q" for q
-    by (auto intro: div_nat_eqI dividend_less_times_div)
-  then show ?thesis
-    by auto
-qed
-
-lemma split_mod:
-  "P (m mod n) \<longleftrightarrow> (n = 0 \<longrightarrow> P m) \<and> (n \<noteq> 0 \<longrightarrow>
-     (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P j))"
-     (is "?P \<longleftrightarrow> ?Q") for m n :: nat
-proof (cases "n = 0")
-  case True
-  then show ?thesis
-    by simp
-next
-  case False
-  show ?thesis
-  proof
-    assume ?P
-    with False show ?Q
-      by auto
-  next
-    assume ?Q
-    with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P j"
-      by simp
-    with False show ?P
-      by (auto intro: * [of _ "m div n"])
-  qed
-qed
-
-declare split_div [of _ _ \<open>numeral n\<close>, linarith_split] for n
-declare split_mod [of _ _ \<open>numeral n\<close>, linarith_split] for n
-
 lemma funpow_mod_eq: \<^marker>\<open>contributor \<open>Lars Noschinski\<close>\<close>
   \<open>(f ^^ (m mod n)) x = (f ^^ m) x\<close> if \<open>(f ^^ n) x = x\<close>
 proof -
@@ -2192,6 +2162,64 @@
 qed
 
 
+subsubsection \<open>Splitting Rules for div and mod\<close>
+
+lemma split_zdiv:
+  \<open>P (n div k) \<longleftrightarrow>
+    (k = 0 \<longrightarrow> P 0) \<and>
+    (0 < k \<longrightarrow> (\<forall>i j. 0 \<le> j \<and> j < k \<and> n = k * i + j \<longrightarrow> P i)) \<and>
+    (k < 0 \<longrightarrow> (\<forall>i j. k < j \<and> j \<le> 0 \<and> n = k * i + j \<longrightarrow> P i))\<close> (is ?div)
+  and split_zmod:
+  \<open>Q (n mod k) \<longleftrightarrow>
+    (k = 0 \<longrightarrow> Q n) \<and>
+    (0 < k \<longrightarrow> (\<forall>i j. 0 \<le> j \<and> j < k \<and> n = k * i + j \<longrightarrow> Q j)) \<and>
+    (k < 0 \<longrightarrow> (\<forall>i j. k < j \<and> j \<le> 0 \<and> n = k * i + j \<longrightarrow> Q j))\<close> (is ?mod)
+  for n k :: int
+proof -
+  have *: \<open>R (n div k) (n mod k) \<longleftrightarrow>
+    (k = 0 \<longrightarrow> R 0 n) \<and>
+    (0 < k \<longrightarrow> (\<forall>i j. 0 \<le> j \<and> j < k \<and> n = k * i + j \<longrightarrow> R i j)) \<and>
+    (k < 0 \<longrightarrow> (\<forall>i j. k < j \<and> j \<le> 0 \<and> n = k * i + j \<longrightarrow> R i j))\<close> for R
+    by (cases \<open>k = 0\<close>)
+      (auto simp add: linorder_class.neq_iff)
+  from * [of \<open>\<lambda>q _. P q\<close>] show ?div .
+  from * [of \<open>\<lambda>_ r. Q r\<close>] show ?mod .
+qed
+ 
+text \<open>Enable (lin)arith to deal with \<^const>\<open>divide\<close> and \<^const>\<open>modulo\<close>
+  when these are applied to some constant that is of the form
+  \<^term>\<open>numeral k\<close>:\<close>
+declare split_zdiv [of _ _ \<open>numeral n\<close>, linarith_split] for n
+declare split_zdiv [of _ _ \<open>- numeral n\<close>, linarith_split] for n
+declare split_zmod [of _ _ \<open>numeral n\<close>, linarith_split] for n
+declare split_zmod [of _ _ \<open>- numeral n\<close>, linarith_split] for n
+
+lemma zdiv_eq_0_iff:
+  "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
+  moreover have "?L \<longrightarrow> ?R"
+    by (rule split_zdiv [THEN iffD2]) simp
+  ultimately show ?R
+    by blast
+next
+  assume ?R then show ?L
+    by auto
+qed
+
+lemma zmod_trivial_iff:
+  fixes i k :: int
+  shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
+proof -
+  have "i mod k = i \<longleftrightarrow> i div k = 0"
+    using div_mult_mod_eq [of i k] by safe auto
+  with zdiv_eq_0_iff
+  show ?thesis
+    by simp
+qed
+
+
 subsubsection \<open>Algebraic rewrites\<close>
 
 lemma zdiv_zmult2_eq:
@@ -2230,6 +2258,14 @@
     using mod_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
 qed
 
+lemma half_nonnegative_int_iff [simp]:
+  \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
+  by auto
+
+lemma half_negative_int_iff [simp]:
+  \<open>k div 2 < 0 \<longleftrightarrow> k < 0\<close> for k :: int
+  by auto
+
 
 subsubsection \<open>Distributive laws for conversions.\<close>