--- a/src/HOL/Divides.thy Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/Divides.thy Sun Aug 21 06:18:23 2022 +0000
@@ -541,439 +541,6 @@
qed
-subsection \<open>Numeral division with a pragmatic type class\<close>
-
-text \<open>
- The following type class contains everything necessary to formulate
- a division algorithm in ring structures with numerals, restricted
- to its positive segments.
-\<close>
-
-class unique_euclidean_semiring_with_nat_division = unique_euclidean_semiring_with_nat +
- fixes divmod :: \<open>num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a\<close>
- and divmod_step :: \<open>'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a\<close> \<comment> \<open>
- These are conceptually definitions but force generated code
- to be monomorphic wrt. particular instances of this class which
- yields a significant speedup.\<close>
- assumes divmod_def: \<open>divmod m n = (numeral m div numeral n, numeral m mod numeral n)\<close>
- and divmod_step_def [simp]: \<open>divmod_step l (q, r) =
- (if euclidean_size l \<le> euclidean_size r then (2 * q + 1, r - l)
- else (2 * q, r))\<close> \<comment> \<open>
- This is a formulation of one step (referring to one digit position)
- in school-method division: compare the dividend at the current
- digit position with the remainder from previous division steps
- and evaluate accordingly.\<close>
-begin
-
-lemma fst_divmod:
- \<open>fst (divmod m n) = numeral m div numeral n\<close>
- by (simp add: divmod_def)
-
-lemma snd_divmod:
- \<open>snd (divmod m n) = numeral m mod numeral n\<close>
- by (simp add: divmod_def)
-
-text \<open>
- Following a formulation of school-method division.
- If the divisor is smaller than the dividend, terminate.
- If not, shift the dividend to the right until termination
- occurs and then reiterate single division steps in the
- opposite direction.
-\<close>
-
-lemma divmod_divmod_step:
- \<open>divmod m n = (if m < n then (0, numeral m)
- else divmod_step (numeral n) (divmod m (Num.Bit0 n)))\<close>
-proof (cases \<open>m < n\<close>)
- case True
- then show ?thesis
- by (simp add: prod_eq_iff fst_divmod snd_divmod flip: of_nat_numeral of_nat_div of_nat_mod)
-next
- case False
- define r s t where \<open>r = (numeral m :: nat)\<close> \<open>s = (numeral n :: nat)\<close> \<open>t = 2 * s\<close>
- then have *: \<open>numeral m = of_nat r\<close> \<open>numeral n = of_nat s\<close> \<open>numeral (num.Bit0 n) = of_nat t\<close>
- and \<open>\<not> s \<le> r mod s\<close>
- by (simp_all add: not_le)
- have t: \<open>2 * (r div t) = r div s - r div s mod 2\<close>
- \<open>r mod t = s * (r div s mod 2) + r mod s\<close>
- by (simp add: Rings.minus_mod_eq_mult_div Groups.mult.commute [of 2] Euclidean_Division.div_mult2_eq \<open>t = 2 * s\<close>)
- (use mod_mult2_eq [of r s 2] in \<open>simp add: ac_simps \<open>t = 2 * s\<close>\<close>)
- have rs: \<open>r div s mod 2 = 0 \<or> r div s mod 2 = Suc 0\<close>
- by auto
- from \<open>\<not> s \<le> r mod s\<close> have \<open>s \<le> r mod t \<Longrightarrow>
- r div s = Suc (2 * (r div t)) \<and>
- r mod s = r mod t - s\<close>
- using rs
- by (auto simp add: t)
- moreover have \<open>r mod t < s \<Longrightarrow>
- r div s = 2 * (r div t) \<and>
- r mod s = r mod t\<close>
- using rs
- by (auto simp add: t)
- ultimately show ?thesis
- by (simp add: divmod_def prod_eq_iff split_def Let_def
- not_less mod_eq_0_iff_dvd Rings.mod_eq_0_iff_dvd False not_le *)
- (simp add: flip: of_nat_numeral of_nat_mult add.commute [of 1] of_nat_div of_nat_mod of_nat_Suc of_nat_diff)
-qed
-
-text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
-
-lemma divmod_trivial [simp]:
- "divmod m Num.One = (numeral m, 0)"
- "divmod num.One (num.Bit0 n) = (0, Numeral1)"
- "divmod num.One (num.Bit1 n) = (0, Numeral1)"
- using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
-
-text \<open>Division by an even number is a right-shift\<close>
-
-lemma divmod_cancel [simp]:
- \<open>divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))\<close> (is ?P)
- \<open>divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))\<close> (is ?Q)
-proof -
- define r s where \<open>r = (numeral m :: nat)\<close> \<open>s = (numeral n :: nat)\<close>
- then have *: \<open>numeral m = of_nat r\<close> \<open>numeral n = of_nat s\<close>
- \<open>numeral (num.Bit0 m) = of_nat (2 * r)\<close> \<open>numeral (num.Bit0 n) = of_nat (2 * s)\<close>
- \<open>numeral (num.Bit1 m) = of_nat (Suc (2 * r))\<close>
- by simp_all
- show ?P and ?Q
- by (simp_all add: divmod_def *)
- (simp_all flip: of_nat_numeral of_nat_div of_nat_mod of_nat_mult add.commute [of 1] of_nat_Suc
- add: Euclidean_Division.mod_mult_mult1 div_mult2_eq [of _ 2] mod_mult2_eq [of _ 2])
-qed
-
-text \<open>The really hard work\<close>
-
-lemma divmod_steps [simp]:
- "divmod (num.Bit0 m) (num.Bit1 n) =
- (if m \<le> n then (0, numeral (num.Bit0 m))
- else divmod_step (numeral (num.Bit1 n))
- (divmod (num.Bit0 m)
- (num.Bit0 (num.Bit1 n))))"
- "divmod (num.Bit1 m) (num.Bit1 n) =
- (if m < n then (0, numeral (num.Bit1 m))
- else divmod_step (numeral (num.Bit1 n))
- (divmod (num.Bit1 m)
- (num.Bit0 (num.Bit1 n))))"
- by (simp_all add: divmod_divmod_step)
-
-lemmas divmod_algorithm_code = divmod_trivial divmod_cancel divmod_steps
-
-text \<open>Special case: divisibility\<close>
-
-definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
-where
- "divides_aux qr \<longleftrightarrow> snd qr = 0"
-
-lemma divides_aux_eq [simp]:
- "divides_aux (q, r) \<longleftrightarrow> r = 0"
- by (simp add: divides_aux_def)
-
-lemma dvd_numeral_simp [simp]:
- "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
- by (simp add: divmod_def mod_eq_0_iff_dvd)
-
-text \<open>Generic computation of quotient and remainder\<close>
-
-lemma numeral_div_numeral [simp]:
- "numeral k div numeral l = fst (divmod k l)"
- by (simp add: fst_divmod)
-
-lemma numeral_mod_numeral [simp]:
- "numeral k mod numeral l = snd (divmod k l)"
- by (simp add: snd_divmod)
-
-lemma one_div_numeral [simp]:
- "1 div numeral n = fst (divmod num.One n)"
- by (simp add: fst_divmod)
-
-lemma one_mod_numeral [simp]:
- "1 mod numeral n = snd (divmod num.One n)"
- by (simp add: snd_divmod)
-
-text \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
-
-lemma cong_exp_iff_simps:
- "numeral n mod numeral Num.One = 0
- \<longleftrightarrow> True"
- "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
- \<longleftrightarrow> numeral n mod numeral q = 0"
- "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
- \<longleftrightarrow> False"
- "numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
- \<longleftrightarrow> True"
- "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
- \<longleftrightarrow> True"
- "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
- \<longleftrightarrow> False"
- "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
- \<longleftrightarrow> (numeral n mod numeral q) = 0"
- "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
- \<longleftrightarrow> False"
- "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
- \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
- "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
- \<longleftrightarrow> False"
- "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
- \<longleftrightarrow> (numeral m mod numeral q) = 0"
- "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
- \<longleftrightarrow> False"
- "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
- \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
- by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])
-
-end
-
-instantiation nat :: unique_euclidean_semiring_with_nat_division
-begin
-
-definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
-where
- divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
-
-definition divmod_step_nat :: "nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
-where
- "divmod_step_nat l qr = (let (q, r) = qr
- in if r \<ge> l then (2 * q + 1, r - l)
- else (2 * q, r))"
-
-instance
- by standard (simp_all add: divmod'_nat_def divmod_step_nat_def)
-
-end
-
-declare divmod_algorithm_code [where ?'a = nat, code]
-
-lemma Suc_0_div_numeral [simp]:
- fixes k l :: num
- shows "Suc 0 div numeral k = fst (divmod Num.One k)"
- by (simp_all add: fst_divmod)
-
-lemma Suc_0_mod_numeral [simp]:
- fixes k l :: num
- shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
- by (simp_all add: snd_divmod)
-
-instantiation int :: unique_euclidean_semiring_with_nat_division
-begin
-
-definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
-where
- "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
-
-definition divmod_step_int :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
-where
- "divmod_step_int l qr = (let (q, r) = qr
- in if \<bar>l\<bar> \<le> \<bar>r\<bar> then (2 * q + 1, r - l)
- else (2 * q, r))"
-
-instance
- by standard (auto simp add: divmod_int_def divmod_step_int_def)
-
-end
-
-declare divmod_algorithm_code [where ?'a = int, code]
-
-context
-begin
-
-qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
-where
- "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
-
-qualified lemma adjust_div_eq [simp, code]:
- "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
- by (simp add: adjust_div_def)
-
-qualified definition adjust_mod :: "num \<Rightarrow> int \<Rightarrow> int"
-where
- [simp]: "adjust_mod l r = (if r = 0 then 0 else numeral l - r)"
-
-lemma minus_numeral_div_numeral [simp]:
- "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
-proof -
- have "int (fst (divmod m n)) = fst (divmod m n)"
- by (simp only: fst_divmod divide_int_def) auto
- then show ?thesis
- by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
-qed
-
-lemma minus_numeral_mod_numeral [simp]:
- "- numeral m mod numeral n = adjust_mod n (snd (divmod m n) :: int)"
-proof (cases "snd (divmod m n) = (0::int)")
- case True
- then show ?thesis
- by (simp add: mod_eq_0_iff_dvd divides_aux_def)
-next
- case False
- then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
- by (simp only: snd_divmod modulo_int_def) auto
- then show ?thesis
- by (simp add: divides_aux_def adjust_div_def)
- (simp add: divides_aux_def modulo_int_def)
-qed
-
-lemma numeral_div_minus_numeral [simp]:
- "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
-proof -
- have "int (fst (divmod m n)) = fst (divmod m n)"
- by (simp only: fst_divmod divide_int_def) auto
- then show ?thesis
- by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
-qed
-
-lemma numeral_mod_minus_numeral [simp]:
- "numeral m mod - numeral n = - adjust_mod n (snd (divmod m n) :: int)"
-proof (cases "snd (divmod m n) = (0::int)")
- case True
- then show ?thesis
- by (simp add: mod_eq_0_iff_dvd divides_aux_def)
-next
- case False
- then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
- by (simp only: snd_divmod modulo_int_def) auto
- then show ?thesis
- by (simp add: divides_aux_def adjust_div_def)
- (simp add: divides_aux_def modulo_int_def)
-qed
-
-lemma minus_one_div_numeral [simp]:
- "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
- using minus_numeral_div_numeral [of Num.One n] by simp
-
-lemma minus_one_mod_numeral [simp]:
- "- 1 mod numeral n = adjust_mod n (snd (divmod Num.One n) :: int)"
- using minus_numeral_mod_numeral [of Num.One n] by simp
-
-lemma one_div_minus_numeral [simp]:
- "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
- using numeral_div_minus_numeral [of Num.One n] by simp
-
-lemma one_mod_minus_numeral [simp]:
- "1 mod - numeral n = - adjust_mod n (snd (divmod Num.One n) :: int)"
- using numeral_mod_minus_numeral [of Num.One n] by simp
-
-end
-
-lemma divmod_BitM_2_eq [simp]:
- \<open>divmod (Num.BitM m) (Num.Bit0 Num.One) = (numeral m - 1, (1 :: int))\<close>
- by (cases m) simp_all
-
-lemma div_positive_int:
- "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
- using that by (simp add: nonneg1_imp_zdiv_pos_iff)
-
-
-subsubsection \<open>Dedicated simproc for calculation\<close>
-
-lemma euclidean_size_nat_less_eq_iff:
- \<open>euclidean_size m \<le> euclidean_size n \<longleftrightarrow> m \<le> n\<close> for m n :: nat
- by simp
-
-lemma euclidean_size_int_less_eq_iff:
- \<open>euclidean_size k \<le> euclidean_size l \<longleftrightarrow> \<bar>k\<bar> \<le> \<bar>l\<bar>\<close> for k l :: int
- by auto
-
-text \<open>
- There is space for improvement here: the calculation itself
- could be carried out outside the logic, and a generic simproc
- (simplifier setup) for generic calculation would be helpful.
-\<close>
-
-simproc_setup numeral_divmod
- ("0 div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" |
- "0 div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" |
- "0 div - 1 :: int" | "0 mod - 1 :: int" |
- "0 div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" |
- "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
- "1 div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" |
- "1 div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" |
- "1 div - 1 :: int" | "1 mod - 1 :: int" |
- "1 div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" |
- "1 div - numeral b :: int" |"1 mod - numeral b :: int" |
- "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
- "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
- "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
- "numeral a div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" |
- "numeral a div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" |
- "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
- "numeral a div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" |
- "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
- "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
- "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
- "- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" |
- "- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" |
- "- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") =
-\<open> let
- val if_cong = the (Code.get_case_cong \<^theory> \<^const_name>\<open>If\<close>);
- fun successful_rewrite ctxt ct =
- let
- val thm = Simplifier.rewrite ctxt ct
- in if Thm.is_reflexive thm then NONE else SOME thm end;
- in fn phi =>
- let
- val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
- one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
- one_div_minus_numeral one_mod_minus_numeral
- numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
- numeral_div_minus_numeral numeral_mod_minus_numeral
- div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
- numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
- divmod_cancel divmod_steps divmod_step_def fst_conv snd_conv numeral_One
- case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
- minus_minus numeral_times_numeral mult_zero_right mult_1_right
- euclidean_size_nat_less_eq_iff euclidean_size_int_less_eq_iff diff_nat_numeral nat_numeral}
- @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
- fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
- (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps)
- in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
- end
-\<close>
-
-
-subsubsection \<open>Code generation\<close>
-
-definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
- where "divmod_nat m n = (m div n, m mod n)"
-
-lemma fst_divmod_nat [simp]:
- "fst (divmod_nat m n) = m div n"
- by (simp add: divmod_nat_def)
-
-lemma snd_divmod_nat [simp]:
- "snd (divmod_nat m n) = m mod n"
- by (simp add: divmod_nat_def)
-
-lemma divmod_nat_if [code]:
- "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
- let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
- by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
-
-lemma [code]:
- "m div n = fst (divmod_nat m n)"
- "m mod n = snd (divmod_nat m n)"
- by simp_all
-
-lemma [code]:
- fixes k :: int
- shows
- "k div 0 = 0"
- "k mod 0 = k"
- "0 div k = 0"
- "0 mod k = 0"
- "k div Int.Pos Num.One = k"
- "k mod Int.Pos Num.One = 0"
- "k div Int.Neg Num.One = - k"
- "k mod Int.Neg Num.One = 0"
- "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
- "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
- "Int.Neg m div Int.Pos n = - (Divides.adjust_div (divmod m n) :: int)"
- "Int.Neg m mod Int.Pos n = Divides.adjust_mod n (snd (divmod m n) :: int)"
- "Int.Pos m div Int.Neg n = - (Divides.adjust_div (divmod m n) :: int)"
- "Int.Pos m mod Int.Neg n = - Divides.adjust_mod n (snd (divmod m n) :: int)"
- "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
- "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
- by simp_all
-
code_identifier
code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
@@ -1090,4 +657,8 @@
lemma zmod_eq_0D [dest!]: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: int
using that by auto
+lemma div_positive_int:
+ "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
+ using that by (simp add: nonneg1_imp_zdiv_pos_iff)
+
end