--- 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)"
--- 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>