--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Sun Oct 08 22:28:21 2017 +0200
@@ -15,7 +15,7 @@
definition to_fract :: "'a :: idom \<Rightarrow> 'a fract"
where "to_fract x = Fract x 1"
- \<comment> \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
+ \<comment> \<open>FIXME: more idiomatic name, abbreviation\<close>
lemma to_fract_0 [simp]: "to_fract 0 = 0"
by (simp add: to_fract_def eq_fract Zero_fract_def)
@@ -438,8 +438,8 @@
by (simp add: irreducible_dict)
show "comm_semiring_1.prime_elem times 1 0 = prime_elem"
by (simp add: prime_elem_dict)
- show "class.unique_euclidean_ring divide plus minus (0 :: 'a poly) times 1 modulo
- (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p)
+ show "class.unique_euclidean_ring divide plus minus (0 :: 'a poly) times 1
+ (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p) modulo
(\<lambda>p. if p = 0 then 0 else 2 ^ degree p) uminus top"
proof (standard, fold dvd_dict)
fix p :: "'a poly"
--- a/src/HOL/Divides.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Divides.thy Sun Oct 08 22:28:21 2017 +0200
@@ -9,95 +9,6 @@
imports Parity
begin
-subsection \<open>Parity\<close>
-
-class unique_euclidean_semiring_parity = unique_euclidean_semiring +
- assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
- assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
- assumes zero_not_eq_two: "0 \<noteq> 2"
-begin
-
-lemma parity_cases [case_names even odd]:
- assumes "a mod 2 = 0 \<Longrightarrow> P"
- assumes "a mod 2 = 1 \<Longrightarrow> P"
- shows P
- using assms parity by blast
-
-lemma one_div_two_eq_zero [simp]:
- "1 div 2 = 0"
-proof (cases "2 = 0")
- case True then show ?thesis by simp
-next
- case False
- from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
- with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
- then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
- then have "1 div 2 = 0 \<or> 2 = 0" by simp
- 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)
- show "1 mod 2 = 1"
- by (fact one_mod_two_eq_one)
-next
- fix a b
- assume "a mod 2 = 1"
- moreover assume "b mod 2 = 1"
- ultimately show "(a + b) mod 2 = 0"
- using mod_add_eq [of a 2 b] by simp
-next
- fix a b
- assume "(a * b) mod 2 = 0"
- then have "(a mod 2) * (b mod 2) mod 2 = 0"
- by (simp add: mod_mult_eq)
- then have "(a mod 2) * (b mod 2) = 0"
- by (cases "a mod 2 = 0") simp_all
- then show "a mod 2 = 0 \<or> b mod 2 = 0"
- by (rule divisors_zero)
-next
- fix a
- assume "a mod 2 = 1"
- then have "a = a div 2 * 2 + 1"
- using div_mult_mod_eq [of a 2] by simp
- then show "\<exists>b. a = b + 1" ..
-qed
-
-lemma even_iff_mod_2_eq_zero:
- "even a \<longleftrightarrow> a mod 2 = 0"
- by (fact dvd_eq_mod_eq_0)
-
-lemma odd_iff_mod_2_eq_one:
- "odd a \<longleftrightarrow> a mod 2 = 1"
- by (simp add: even_iff_mod_2_eq_zero)
-
-lemma even_succ_div_two [simp]:
- "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
- by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
-
-lemma odd_succ_div_two [simp]:
- "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
- by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
-
-lemma even_two_times_div_two:
- "even a \<Longrightarrow> 2 * (a div 2) = a"
- by (fact dvd_mult_div_cancel)
-
-lemma odd_two_times_div_two_succ [simp]:
- "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
- using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
-
-end
-
-
subsection \<open>Numeral division with a pragmatic type class\<close>
text \<open>
@@ -382,445 +293,11 @@
end
+hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
+
subsection \<open>Division on @{typ nat}\<close>
-context
-begin
-
-text \<open>
- We define @{const divide} and @{const modulo} on @{typ nat} by means
- of a characteristic relation with two input arguments
- @{term "m::nat"}, @{term "n::nat"} and two output arguments
- @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
-\<close>
-
-inductive eucl_rel_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool"
- where eucl_rel_nat_by0: "eucl_rel_nat m 0 (0, m)"
- | eucl_rel_natI: "r < n \<Longrightarrow> m = q * n + r \<Longrightarrow> eucl_rel_nat m n (q, r)"
-
-text \<open>@{const eucl_rel_nat} is total:\<close>
-
-qualified lemma eucl_rel_nat_ex:
- obtains q r where "eucl_rel_nat m n (q, r)"
-proof (cases "n = 0")
- case True
- with that eucl_rel_nat_by0 show thesis
- by blast
-next
- case False
- have "\<exists>q r. m = q * n + r \<and> r < n"
- proof (induct m)
- case 0 with \<open>n \<noteq> 0\<close>
- have "(0::nat) = 0 * n + 0 \<and> 0 < n" by simp
- then show ?case by blast
- next
- case (Suc m) then obtain q' r'
- where m: "m = q' * n + r'" and n: "r' < n" by auto
- then show ?case proof (cases "Suc r' < n")
- case True
- from m n have "Suc m = q' * n + Suc r'" by simp
- with True show ?thesis by blast
- next
- case False then have "n \<le> Suc r'"
- by (simp add: not_less)
- moreover from n have "Suc r' \<le> n"
- by (simp add: Suc_le_eq)
- ultimately have "n = Suc r'" by auto
- with m have "Suc m = Suc q' * n + 0" by simp
- with \<open>n \<noteq> 0\<close> show ?thesis by blast
- qed
- qed
- with that \<open>n \<noteq> 0\<close> eucl_rel_natI show thesis
- by blast
-qed
-
-text \<open>@{const eucl_rel_nat} is injective:\<close>
-
-qualified lemma eucl_rel_nat_unique_div:
- assumes "eucl_rel_nat m n (q, r)"
- and "eucl_rel_nat m n (q', r')"
- shows "q = q'"
-proof (cases "n = 0")
- case True with assms show ?thesis
- by (auto elim: eucl_rel_nat.cases)
-next
- case False
- have *: "q' \<le> q" if "q' * n + r' = q * n + r" "r < n" for q r q' r' :: nat
- proof (rule ccontr)
- assume "\<not> q' \<le> q"
- then have "q < q'"
- by (simp add: not_le)
- with that show False
- by (auto simp add: less_iff_Suc_add algebra_simps)
- qed
- from \<open>n \<noteq> 0\<close> assms show ?thesis
- by (auto intro: order_antisym elim: eucl_rel_nat.cases dest: * sym split: if_splits)
-qed
-
-qualified lemma eucl_rel_nat_unique_mod:
- assumes "eucl_rel_nat m n (q, r)"
- and "eucl_rel_nat m n (q', r')"
- shows "r = r'"
-proof -
- from assms have "q' = q"
- by (auto intro: eucl_rel_nat_unique_div)
- with assms show ?thesis
- by (auto elim!: eucl_rel_nat.cases)
-qed
-
-text \<open>
- We instantiate divisibility on the natural numbers by
- means of @{const eucl_rel_nat}:
-\<close>
-
-qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
- "divmod_nat m n = (THE qr. eucl_rel_nat m n qr)"
-
-qualified lemma eucl_rel_nat_divmod_nat:
- "eucl_rel_nat m n (divmod_nat m n)"
-proof -
- from eucl_rel_nat_ex
- obtain q r where rel: "eucl_rel_nat m n (q, r)" .
- then show ?thesis
- by (auto simp add: divmod_nat_def intro: theI
- elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
-qed
-
-qualified lemma divmod_nat_unique:
- "divmod_nat m n = (q, r)" if "eucl_rel_nat m n (q, r)"
- using that
- by (auto simp add: divmod_nat_def intro: eucl_rel_nat_divmod_nat elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
-
-qualified lemma divmod_nat_zero:
- "divmod_nat m 0 = (0, m)"
- by (rule divmod_nat_unique) (fact eucl_rel_nat_by0)
-
-qualified lemma divmod_nat_zero_left:
- "divmod_nat 0 n = (0, 0)"
- by (rule divmod_nat_unique)
- (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
-
-qualified lemma divmod_nat_base:
- "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
- by (rule divmod_nat_unique)
- (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
-
-qualified lemma divmod_nat_step:
- assumes "0 < n" and "n \<le> m"
- shows "divmod_nat m n =
- (Suc (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
-proof (rule divmod_nat_unique)
- have "eucl_rel_nat (m - n) n (divmod_nat (m - n) n)"
- by (fact eucl_rel_nat_divmod_nat)
- then show "eucl_rel_nat m n (Suc
- (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
- using assms
- by (auto split: if_splits intro: eucl_rel_natI elim!: eucl_rel_nat.cases simp add: algebra_simps)
-qed
-
-end
-
-instantiation nat :: "{semidom_modulo, normalization_semidom}"
-begin
-
-definition normalize_nat :: "nat \<Rightarrow> nat"
- where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
-
-definition unit_factor_nat :: "nat \<Rightarrow> nat"
- where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
-
-lemma unit_factor_simps [simp]:
- "unit_factor 0 = (0::nat)"
- "unit_factor (Suc n) = 1"
- by (simp_all add: unit_factor_nat_def)
-
-definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
- where div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
-
-definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
- where mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
-
-lemma fst_divmod_nat [simp]:
- "fst (Divides.divmod_nat m n) = m div n"
- by (simp add: div_nat_def)
-
-lemma snd_divmod_nat [simp]:
- "snd (Divides.divmod_nat m n) = m mod n"
- by (simp add: mod_nat_def)
-
-lemma divmod_nat_div_mod:
- "Divides.divmod_nat m n = (m div n, m mod n)"
- by (simp add: prod_eq_iff)
-
-lemma div_nat_unique:
- assumes "eucl_rel_nat m n (q, r)"
- shows "m div n = q"
- using assms
- by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
-
-lemma mod_nat_unique:
- assumes "eucl_rel_nat m n (q, r)"
- shows "m mod n = r"
- using assms
- by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
-
-lemma eucl_rel_nat: "eucl_rel_nat m n (m div n, m mod n)"
- using Divides.eucl_rel_nat_divmod_nat
- by (simp add: divmod_nat_div_mod)
-
-text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
-
-lemma div_less [simp]:
- fixes m n :: nat
- assumes "m < n"
- shows "m div n = 0"
- using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
-
-lemma le_div_geq:
- fixes m n :: nat
- assumes "0 < n" and "n \<le> m"
- shows "m div n = Suc ((m - n) div n)"
- using assms Divides.divmod_nat_step by (simp add: prod_eq_iff)
-
-lemma mod_less [simp]:
- fixes m n :: nat
- assumes "m < n"
- shows "m mod n = m"
- using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
-
-lemma le_mod_geq:
- fixes m n :: nat
- assumes "n \<le> m"
- shows "m mod n = (m - n) mod n"
- using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
-
-lemma mod_less_divisor [simp]:
- fixes m n :: nat
- assumes "n > 0"
- shows "m mod n < n"
- using assms eucl_rel_nat [of m n]
- by (auto elim: eucl_rel_nat.cases)
-
-lemma mod_le_divisor [simp]:
- fixes m n :: nat
- assumes "n > 0"
- shows "m mod n \<le> n"
- using assms eucl_rel_nat [of m n]
- by (auto elim: eucl_rel_nat.cases)
-
-instance proof
- fix m n :: nat
- show "m div n * n + m mod n = m"
- using eucl_rel_nat [of m n]
- by (auto elim: eucl_rel_nat.cases)
-next
- fix n :: nat show "n div 0 = 0"
- by (simp add: div_nat_def Divides.divmod_nat_zero)
-next
- fix m n :: nat
- assume "n \<noteq> 0"
- then show "m * n div n = m"
- by (auto intro!: eucl_rel_natI div_nat_unique [of _ _ _ 0])
-qed (simp_all add: unit_factor_nat_def)
-
-end
-
-text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
-
-lemma (in semiring_modulo) cancel_div_mod_rules:
- "((a div b) * b + a mod b) + c = a + c"
- "(b * (a div b) + a mod b) + c = a + c"
- by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
-
-ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
-
-ML \<open>
-structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
-(
- val div_name = @{const_name divide};
- val mod_name = @{const_name modulo};
- val mk_binop = HOLogic.mk_binop;
- val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
- val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
- fun mk_sum [] = HOLogic.zero
- | mk_sum [t] = t
- | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
- fun dest_sum tm =
- if HOLogic.is_zero tm then []
- else
- (case try HOLogic.dest_Suc tm of
- SOME t => HOLogic.Suc_zero :: dest_sum t
- | NONE =>
- (case try dest_plus tm of
- SOME (t, u) => dest_sum t @ dest_sum u
- | NONE => [tm]));
-
- val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
-
- val prove_eq_sums = Arith_Data.prove_conv2 all_tac
- (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
-)
-\<close>
-
-simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
- \<open>K Cancel_Div_Mod_Nat.proc\<close>
-
-lemma div_by_Suc_0 [simp]:
- "m div Suc 0 = m"
- using div_by_1 [of m] by simp
-
-lemma mod_by_Suc_0 [simp]:
- "m mod Suc 0 = 0"
- using mod_by_1 [of m] by simp
-
-lemma mod_greater_zero_iff_not_dvd:
- fixes m n :: nat
- shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
- by (simp add: dvd_eq_mod_eq_0)
-
-instantiation nat :: unique_euclidean_semiring
-begin
-
-definition [simp]:
- "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
-
-definition [simp]:
- "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
-
-instance proof
- fix n q r :: nat
- assume "euclidean_size r < euclidean_size n"
- then have "n > r"
- by simp_all
- then have "eucl_rel_nat (q * n + r) n (q, r)"
- by (rule eucl_rel_natI) rule
- then show "(q * n + r) div n = q"
- by (rule div_nat_unique)
-qed (use mult_le_mono2 [of 1] in \<open>simp_all\<close>)
-
-end
-
-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 mod_Suc_eq [mod_simps]:
- "Suc (m mod n) mod n = Suc m mod n"
-proof -
- have "(m mod n + 1) mod n = (m + 1) mod n"
- by (simp only: mod_simps)
- then show ?thesis
- by simp
-qed
-
-lemma mod_Suc_Suc_eq [mod_simps]:
- "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
-proof -
- have "(m mod n + 2) mod n = (m + 2) mod n"
- by (simp only: mod_simps)
- then show ?thesis
- by simp
-qed
-
-
-subsubsection \<open>Quotient\<close>
-
-lemma div_geq: "0 < n \<Longrightarrow> \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"
-by (simp add: le_div_geq linorder_not_less)
-
-lemma div_if: "0 < n \<Longrightarrow> m div n = (if m < n then 0 else Suc ((m - n) div n))"
-by (simp add: div_geq)
-
-lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
-by simp
-
-lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
-by simp
-
-lemma div_positive:
- fixes m n :: nat
- assumes "n > 0"
- assumes "m \<ge> n"
- shows "m div n > 0"
-proof -
- from \<open>m \<ge> n\<close> obtain q where "m = n + q"
- by (auto simp add: le_iff_add)
- with \<open>n > 0\<close> show ?thesis by (simp add: div_add_self1)
-qed
-
-lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
- by auto (metis div_positive less_numeral_extra(3) not_less)
-
-
-subsubsection \<open>Remainder\<close>
-
-lemma mod_Suc_le_divisor [simp]:
- "m mod Suc n \<le> n"
- using mod_less_divisor [of "Suc n" m] by arith
-
-lemma mod_less_eq_dividend [simp]:
- fixes m n :: nat
- shows "m mod n \<le> m"
-proof (rule add_leD2)
- from div_mult_mod_eq have "m div n * n + m mod n = m" .
- then show "m div n * n + m mod n \<le> m" by auto
-qed
-
-lemma mod_geq: "\<not> m < (n::nat) \<Longrightarrow> m mod n = (m - n) mod n"
-by (simp add: le_mod_geq linorder_not_less)
-
-lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
-by (simp add: le_mod_geq)
-
-
-subsubsection \<open>Quotient and Remainder\<close>
-
-lemma div_mult1_eq:
- "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
- by (cases "c = 0")
- (auto simp add: algebra_simps distrib_left [symmetric]
- intro!: div_nat_unique [of _ _ _ "(a * (b mod c)) mod c"] eucl_rel_natI)
-
-lemma eucl_rel_nat_add1_eq:
- "eucl_rel_nat a c (aq, ar) \<Longrightarrow> eucl_rel_nat b c (bq, br)
- \<Longrightarrow> eucl_rel_nat (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
- by (auto simp add: split_ifs algebra_simps elim!: eucl_rel_nat.cases intro: eucl_rel_nat_by0 eucl_rel_natI)
-
-(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
-lemma div_add1_eq:
- "(a + b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
-by (blast intro: eucl_rel_nat_add1_eq [THEN div_nat_unique] eucl_rel_nat)
-
-lemma eucl_rel_nat_mult2_eq:
- assumes "eucl_rel_nat a b (q, r)"
- shows "eucl_rel_nat a (b * c) (q div c, b *(q mod c) + r)"
-proof (cases "c = 0")
- case True
- with assms show ?thesis
- by (auto intro: eucl_rel_nat_by0 elim!: eucl_rel_nat.cases simp add: ac_simps)
-next
- case False
- { assume "r < b"
- with False have "b * (q mod c) + r < b * c"
- apply (cut_tac m = q and n = c in mod_less_divisor)
- apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
- apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
- apply (simp add: add_mult_distrib2)
- done
- then have "r + b * (q mod c) < b * c"
- by (simp add: ac_simps)
- } with assms False show ?thesis
- by (auto simp add: algebra_simps add_mult_distrib2 [symmetric] elim!: eucl_rel_nat.cases intro: eucl_rel_nat.intros)
-qed
-
-lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
-by (force simp add: eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN div_nat_unique])
-
-lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
-by (auto simp add: mult.commute eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN mod_nat_unique])
-
instantiation nat :: unique_euclidean_semiring_numeral
begin
@@ -834,370 +311,15 @@
in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
else (2 * q, r))"
-instance
- by standard (auto intro: div_positive simp add: divmod'_nat_def divmod_step_nat_def mod_mult2_eq div_mult2_eq)
+instance by standard
+ (auto simp add: divmod'_nat_def divmod_step_nat_def div_greater_zero_iff div_mult2_eq mod_mult2_eq)
end
declare divmod_algorithm_code [where ?'a = nat, code]
-
-subsubsection \<open>Further Facts about Quotient and Remainder\<close>
-
-lemma div_le_mono:
- fixes m n k :: nat
- assumes "m \<le> n"
- shows "m div k \<le> n div k"
-proof -
- from assms obtain q where "n = m + q"
- by (auto simp add: le_iff_add)
- then show ?thesis
- by (simp add: div_add1_eq [of m q k])
-qed
-
-(* Antimonotonicity of div in second argument *)
-lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
-apply (subgoal_tac "0<n")
- prefer 2 apply simp
-apply (induct_tac k rule: nat_less_induct)
-apply (rename_tac "k")
-apply (case_tac "k<n", simp)
-apply (subgoal_tac "~ (k<m) ")
- prefer 2 apply simp
-apply (simp add: div_geq)
-apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
- prefer 2
- apply (blast intro: div_le_mono diff_le_mono2)
-apply (rule le_trans, simp)
-apply (simp)
-done
-
-lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
-apply (case_tac "n=0", simp)
-apply (subgoal_tac "m div n \<le> m div 1", simp)
-apply (rule div_le_mono2)
-apply (simp_all (no_asm_simp))
-done
-
-(* Similar for "less than" *)
-lemma div_less_dividend [simp]:
- "\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m"
-apply (induct m rule: nat_less_induct)
-apply (rename_tac "m")
-apply (case_tac "m<n", simp)
-apply (subgoal_tac "0<n")
- prefer 2 apply simp
-apply (simp add: div_geq)
-apply (case_tac "n<m")
- apply (subgoal_tac "(m-n) div n < (m-n) ")
- apply (rule impI less_trans_Suc)+
-apply assumption
- apply (simp_all)
-done
-
-text\<open>A fact for the mutilated chess board\<close>
-lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
-apply (case_tac "n=0", simp)
-apply (induct "m" rule: nat_less_induct)
-apply (case_tac "Suc (na) <n")
-(* case Suc(na) < n *)
-apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
-(* case n \<le> Suc(na) *)
-apply (simp add: linorder_not_less le_Suc_eq mod_geq)
-apply (auto simp add: Suc_diff_le le_mod_geq)
-done
-
-lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
-by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
-
-lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
-
-(*Loses information, namely we also have r<d provided d is nonzero*)
-lemma mod_eqD:
- fixes m d r q :: nat
- assumes "m mod d = r"
- shows "\<exists>q. m = r + q * d"
-proof -
- from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
- with assms have "m = r + q * d" by simp
- then show ?thesis ..
-qed
-
-lemma split_div:
- "P(n div k :: nat) =
- ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
- (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
-proof
- assume P: ?P
- show ?Q
- proof (cases)
- assume "k = 0"
- with P show ?Q by simp
- next
- assume not0: "k \<noteq> 0"
- thus ?Q
- proof (simp, intro allI impI)
- fix i j
- assume n: "n = k*i + j" and j: "j < k"
- show "P i"
- proof (cases)
- assume "i = 0"
- with n j P show "P i" by simp
- next
- assume "i \<noteq> 0"
- with not0 n j P show "P i" by(simp add:ac_simps)
- qed
- qed
- qed
-next
- assume Q: ?Q
- show ?P
- proof (cases)
- assume "k = 0"
- with Q show ?P by simp
- next
- assume not0: "k \<noteq> 0"
- with Q have R: ?R by simp
- from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
- show ?P by simp
- qed
-qed
-
-lemma split_div_lemma:
- assumes "0 < n"
- shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m::nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
-proof
- assume ?rhs
- with minus_mod_eq_mult_div [symmetric] have nq: "n * q = m - (m mod n)" by simp
- then have A: "n * q \<le> m" by simp
- have "n - (m mod n) > 0" using mod_less_divisor assms by auto
- then have "m < m + (n - (m mod n))" by simp
- then have "m < n + (m - (m mod n))" by simp
- with nq have "m < n + n * q" by simp
- then have B: "m < n * Suc q" by simp
- from A B show ?lhs ..
-next
- assume P: ?lhs
- then have "eucl_rel_nat m n (q, m - n * q)"
- by (auto intro: eucl_rel_natI simp add: ac_simps)
- then have "m div n = q"
- by (rule div_nat_unique)
- then show ?rhs by simp
-qed
-
-theorem split_div':
- "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
- (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
- apply (cases "0 < n")
- apply (simp only: add: split_div_lemma)
- apply simp_all
- done
-
-lemma split_mod:
- "P(n mod k :: nat) =
- ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
- (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
-proof
- assume P: ?P
- show ?Q
- proof (cases)
- assume "k = 0"
- with P show ?Q by simp
- next
- assume not0: "k \<noteq> 0"
- thus ?Q
- 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)
- qed
- qed
-next
- assume Q: ?Q
- show ?P
- proof (cases)
- assume "k = 0"
- with Q show ?P by simp
- next
- assume not0: "k \<noteq> 0"
- with Q have R: ?R by simp
- from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
- show ?P by simp
- qed
-qed
-
-lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
- apply rule
- apply (cases "b = 0")
- apply simp_all
- apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
- done
-
-lemma (in field_char_0) of_nat_div:
- "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
-proof -
- have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
- unfolding of_nat_add by (cases "n = 0") simp_all
- then show ?thesis
- by simp
-qed
-
-
-subsubsection \<open>An ``induction'' law for modulus arithmetic.\<close>
-
-lemma mod_induct_0:
- assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
- and base: "P i" and i: "i<p"
- shows "P 0"
-proof (rule ccontr)
- assume contra: "\<not>(P 0)"
- from i have p: "0<p" by simp
- have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")
- proof
- fix k
- show "?A k"
- proof (induct k)
- show "?A 0" by simp \<comment> "by contradiction"
- next
- fix n
- assume ih: "?A n"
- show "?A (Suc n)"
- proof (clarsimp)
- assume y: "P (p - Suc n)"
- have n: "Suc n < p"
- proof (rule ccontr)
- assume "\<not>(Suc n < p)"
- hence "p - Suc n = 0"
- by simp
- with y contra show "False"
- by simp
- qed
- hence n2: "Suc (p - Suc n) = p-n" by arith
- from p have "p - Suc n < p" by arith
- with y step have z: "P ((Suc (p - Suc n)) mod p)"
- by blast
- show "False"
- proof (cases "n=0")
- case True
- with z n2 contra show ?thesis by simp
- next
- case False
- with p have "p-n < p" by arith
- with z n2 False ih show ?thesis by simp
- qed
- qed
- qed
- qed
- moreover
- from i obtain k where "0<k \<and> i+k=p"
- by (blast dest: less_imp_add_positive)
- hence "0<k \<and> i=p-k" by auto
- moreover
- note base
- ultimately
- show "False" by blast
-qed
-
-lemma mod_induct:
- assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
- and base: "P i" and i: "i<p" and j: "j<p"
- shows "P j"
-proof -
- have "\<forall>j<p. P j"
- proof
- fix j
- show "j<p \<longrightarrow> P j" (is "?A j")
- proof (induct j)
- from step base i show "?A 0"
- by (auto elim: mod_induct_0)
- next
- fix k
- assume ih: "?A k"
- show "?A (Suc k)"
- proof
- assume suc: "Suc k < p"
- hence k: "k<p" by simp
- with ih have "P k" ..
- with step k have "P (Suc k mod p)"
- by blast
- moreover
- from suc have "Suc k mod p = Suc k"
- by simp
- ultimately
- show "P (Suc k)" by simp
- qed
- qed
- qed
- with j show ?thesis by blast
-qed
-
-lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
- by (simp add: numeral_2_eq_2 le_div_geq)
-
-lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2"
- by (simp add: numeral_2_eq_2 le_mod_geq)
-
-lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
-by (simp add: mult_2 [symmetric])
-
-lemma mod2_gr_0 [simp]: "0 < (m::nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
-proof -
- { fix n :: nat have "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
- moreover have "m mod 2 < 2" by simp
- ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
- then show ?thesis by auto
-qed
-
-text\<open>These lemmas collapse some needless occurrences of Suc:
- at least three Sucs, since two and fewer are rewritten back to Suc again!
- We already have some rules to simplify operands smaller than 3.\<close>
-
-lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
-by (simp add: Suc3_eq_add_3)
-
-lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
-by (simp add: Suc3_eq_add_3)
-
-lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
-by (simp add: Suc3_eq_add_3)
-
-lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
-by (simp add: Suc3_eq_add_3)
-
-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)
-done
-
-declare Suc_times_mod_eq [of "numeral w", simp] for w
-
-lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
-by (simp add: div_le_mono)
-
-lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
-by (cases n) simp_all
-
-lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
-proof -
- from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
- from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp
-qed
-
-lemma mod_mult_self3' [simp]: "Suc (k * n + m) mod n = Suc m mod n"
- using mod_mult_self3 [of k n "Suc m"] by simp
-
-lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
-apply (subst mod_Suc [of m])
-apply (subst mod_Suc [of "m mod n"], simp)
-done
-
-lemma mod_2_not_eq_zero_eq_one_nat:
- fixes n :: nat
- shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
- by (fact not_mod_2_eq_0_eq_1)
+lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
+ by (auto elim: oddE)
lemma even_Suc_div_two [simp]:
"even n \<Longrightarrow> Suc n div 2 = n div 2"
@@ -1245,6 +367,11 @@
qed
qed
+lemma mod_2_not_eq_zero_eq_one_nat:
+ fixes n :: nat
+ shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
+ by (fact not_mod_2_eq_0_eq_1)
+
lemma Suc_0_div_numeral [simp]:
fixes k l :: num
shows "Suc 0 div numeral k = fst (divmod Num.One k)"
@@ -1255,6 +382,27 @@
shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
by (simp_all add: snd_divmod)
+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
+
subsection \<open>Division on @{typ int}\<close>
@@ -2225,7 +1373,7 @@
lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
apply (subgoal_tac "nat x div nat k < nat x")
apply (simp add: nat_div_distrib [symmetric])
-apply (rule Divides.div_less_dividend, simp_all)
+apply (rule div_less_dividend, simp_all)
done
lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
@@ -2258,11 +1406,12 @@
thus ?lhs by simp
qed
+
subsubsection \<open>Dedicated simproc for calculation\<close>
text \<open>
There is space for improvement here: the calculation itself
- could be carried outside the logic, and a generic simproc
+ could be carried out outside the logic, and a generic simproc
(simplifier setup) for generic calculation would be helpful.
\<close>
@@ -2348,4 +1497,39 @@
declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
+
+subsubsection \<open>Lemmas of doubtful value\<close>
+
+lemma mod_mult_self3':
+ "Suc (k * n + m) mod n = Suc m mod n"
+ by (fact Suc_mod_mult_self3)
+
+lemma mod_Suc_eq_Suc_mod:
+ "Suc m mod n = Suc (m mod n) mod n"
+ by (simp add: mod_simps)
+
+lemma div_geq:
+ "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
+ by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>)
+
+lemma mod_geq:
+ "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
+ by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
+
+lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
+ by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
+
+lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
+
+(*Loses information, namely we also have r<d provided d is nonzero*)
+lemma mod_eqD:
+ fixes m d r q :: nat
+ assumes "m mod d = r"
+ shows "\<exists>q. m = r + q * d"
+proof -
+ from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
+ with assms have "m = r + q * d" by simp
+ then show ?thesis ..
+qed
+
end
--- a/src/HOL/Euclidean_Division.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Euclidean_Division.thy Sun Oct 08 22:28:21 2017 +0200
@@ -6,9 +6,19 @@
section \<open>Uniquely determined division in euclidean (semi)rings\<close>
theory Euclidean_Division
- imports Nat_Transfer
+ imports Nat_Transfer Lattices_Big
begin
+subsection \<open>Prelude: simproc for cancelling @{const divide} and @{const modulo}\<close>
+
+lemma (in semiring_modulo) cancel_div_mod_rules:
+ "((a div b) * b + a mod b) + c = a + c"
+ "(b * (a div b) + a mod b) + c = a + c"
+ by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
+
+ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
+
+
subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
class euclidean_semiring = semidom_modulo + normalization_semidom +
@@ -639,4 +649,657 @@
end
+
+subsection \<open>Euclidean division on @{typ nat}\<close>
+
+instantiation nat :: unique_euclidean_semiring
+begin
+
+definition normalize_nat :: "nat \<Rightarrow> nat"
+ where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
+
+definition unit_factor_nat :: "nat \<Rightarrow> nat"
+ where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
+
+lemma unit_factor_simps [simp]:
+ "unit_factor 0 = (0::nat)"
+ "unit_factor (Suc n) = 1"
+ by (simp_all add: unit_factor_nat_def)
+
+definition euclidean_size_nat :: "nat \<Rightarrow> nat"
+ where [simp]: "euclidean_size_nat = id"
+
+definition uniqueness_constraint_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
+ where [simp]: "uniqueness_constraint_nat = \<top>"
+
+definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
+
+definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ where "m mod n = m - (m div n * (n::nat))"
+
+instance proof
+ fix m n :: nat
+ have ex: "\<exists>k. k * n \<le> l" for l :: nat
+ by (rule exI [of _ 0]) simp
+ have fin: "finite {k. k * n \<le> l}" if "n > 0" for l
+ proof -
+ from that have "{k. k * n \<le> l} \<subseteq> {k. k \<le> l}"
+ by (cases n) auto
+ then show ?thesis
+ by (rule finite_subset) simp
+ qed
+ have mult_div_unfold: "n * (m div n) = Max {l. l \<le> m \<and> n dvd l}"
+ proof (cases "n = 0")
+ case True
+ moreover have "{l. l = 0 \<and> l \<le> m} = {0::nat}"
+ by auto
+ ultimately show ?thesis
+ by simp
+ next
+ case False
+ with ex [of m] fin have "n * Max {k. k * n \<le> m} = Max (times n ` {k. k * n \<le> m})"
+ by (auto simp add: nat_mult_max_right intro: hom_Max_commute)
+ also have "times n ` {k. k * n \<le> m} = {l. l \<le> m \<and> n dvd l}"
+ by (auto simp add: ac_simps elim!: dvdE)
+ finally show ?thesis
+ using False by (simp add: divide_nat_def ac_simps)
+ qed
+ show "n div 0 = 0"
+ by (simp add: divide_nat_def)
+ have less_eq: "m div n * n \<le> m"
+ by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI)
+ then show "m div n * n + m mod n = m"
+ by (simp add: modulo_nat_def)
+ assume "n \<noteq> 0"
+ show "m * n div n = m"
+ using \<open>n \<noteq> 0\<close> by (auto simp add: divide_nat_def ac_simps intro: Max_eqI)
+ show "euclidean_size (m mod n) < euclidean_size n"
+ proof -
+ have "m < Suc (m div n) * n"
+ proof (rule ccontr)
+ assume "\<not> m < Suc (m div n) * n"
+ then have "Suc (m div n) * n \<le> m"
+ by (simp add: not_less)
+ moreover from \<open>n \<noteq> 0\<close> have "Max {k. k * n \<le> m} < Suc (m div n)"
+ by (simp add: divide_nat_def)
+ with \<open>n \<noteq> 0\<close> ex fin have "\<And>k. k * n \<le> m \<Longrightarrow> k < Suc (m div n)"
+ by auto
+ ultimately have "Suc (m div n) < Suc (m div n)"
+ by blast
+ then show False
+ by simp
+ qed
+ with \<open>n \<noteq> 0\<close> show ?thesis
+ by (simp add: modulo_nat_def)
+ qed
+ show "euclidean_size m \<le> euclidean_size (m * n)"
+ using \<open>n \<noteq> 0\<close> by (cases n) simp_all
+ fix q r :: nat
+ show "(q * n + r) div n = q" if "euclidean_size r < euclidean_size n"
+ proof -
+ from that have "r < n"
+ by simp
+ have "k \<le> q" if "k * n \<le> q * n + r" for k
+ proof (rule ccontr)
+ assume "\<not> k \<le> q"
+ then have "q < k"
+ by simp
+ then obtain l where "k = Suc (q + l)"
+ by (auto simp add: less_iff_Suc_add)
+ with \<open>r < n\<close> that show False
+ by (simp add: algebra_simps)
+ qed
+ with \<open>n \<noteq> 0\<close> ex fin show ?thesis
+ by (auto simp add: divide_nat_def Max_eq_iff)
+ qed
+qed (simp_all add: unit_factor_nat_def)
+
end
+
+text \<open>Tool support\<close>
+
+ML \<open>
+structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
+(
+ val div_name = @{const_name divide};
+ val mod_name = @{const_name modulo};
+ val mk_binop = HOLogic.mk_binop;
+ val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
+ val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
+ fun mk_sum [] = HOLogic.zero
+ | mk_sum [t] = t
+ | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+ fun dest_sum tm =
+ if HOLogic.is_zero tm then []
+ else
+ (case try HOLogic.dest_Suc tm of
+ SOME t => HOLogic.Suc_zero :: dest_sum t
+ | NONE =>
+ (case try dest_plus tm of
+ SOME (t, u) => dest_sum t @ dest_sum u
+ | NONE => [tm]));
+
+ val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
+
+ val prove_eq_sums = Arith_Data.prove_conv2 all_tac
+ (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
+)
+\<close>
+
+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
+
+lemma div_mult_self1_is_m [simp]:
+ "n * m div n = m" if "n > 0" for m n :: nat
+ using that by simp
+
+lemma mod_less_divisor [simp]:
+ "m mod n < n" if "n > 0" for m n :: nat
+ using mod_size_less [of n m] that by simp
+
+lemma mod_le_divisor [simp]:
+ "m mod n \<le> n" if "n > 0" for m n :: nat
+ using that by (auto simp add: le_less)
+
+lemma div_times_less_eq_dividend [simp]:
+ "m div n * n \<le> m" for m n :: nat
+ by (simp add: minus_mod_eq_div_mult [symmetric])
+
+lemma times_div_less_eq_dividend [simp]:
+ "n * (m div n) \<le> m" for m n :: nat
+ using div_times_less_eq_dividend [of m n]
+ by (simp add: ac_simps)
+
+lemma dividend_less_div_times:
+ "m < n + (m div n) * n" if "0 < n" for m n :: nat
+proof -
+ from that have "m mod n < n"
+ by simp
+ then show ?thesis
+ by (simp add: minus_mod_eq_div_mult [symmetric])
+qed
+
+lemma dividend_less_times_div:
+ "m < n + n * (m div n)" if "0 < n" for m n :: nat
+ using dividend_less_div_times [of n m] that
+ by (simp add: ac_simps)
+
+lemma mod_Suc_le_divisor [simp]:
+ "m mod Suc n \<le> n"
+ using mod_less_divisor [of "Suc n" m] by arith
+
+lemma mod_less_eq_dividend [simp]:
+ "m mod n \<le> m" for m n :: nat
+proof (rule add_leD2)
+ from div_mult_mod_eq have "m div n * n + m mod n = m" .
+ then show "m div n * n + m mod n \<le> m" by auto
+qed
+
+lemma
+ div_less [simp]: "m div n = 0"
+ 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 le_div_geq:
+ "m div n = Suc ((m - n) div n)" if "0 < n" and "n \<le> m" for m n :: nat
+proof -
+ from \<open>n \<le> m\<close> obtain q where "m = n + q"
+ by (auto simp add: le_iff_add)
+ with \<open>0 < n\<close> show ?thesis
+ by (simp add: div_add_self1)
+qed
+
+lemma le_mod_geq:
+ "m mod n = (m - n) mod n" if "n \<le> m" for m n :: nat
+proof -
+ from \<open>n \<le> m\<close> obtain q where "m = n + q"
+ by (auto simp add: le_iff_add)
+ then show ?thesis
+ by simp
+qed
+
+lemma div_if:
+ "m div n = (if m < n \<or> n = 0 then 0 else Suc ((m - n) div n))"
+ by (simp add: le_div_geq)
+
+lemma mod_if:
+ "m mod n = (if m < n then m else (m - n) mod n)" for m n :: nat
+ by (simp add: le_mod_geq)
+
+lemma div_eq_0_iff:
+ "m div n = 0 \<longleftrightarrow> m < n \<or> n = 0" for m n :: nat
+ by (simp add: div_if)
+
+lemma div_greater_zero_iff:
+ "m div n > 0 \<longleftrightarrow> n \<le> m \<and> n > 0" for m n :: nat
+ using div_eq_0_iff [of m n] by auto
+
+lemma mod_greater_zero_iff_not_dvd:
+ "m mod n > 0 \<longleftrightarrow> \<not> n dvd m" for m n :: nat
+ by (simp add: dvd_eq_mod_eq_0)
+
+lemma div_by_Suc_0 [simp]:
+ "m div Suc 0 = m"
+ using div_by_1 [of m] by simp
+
+lemma mod_by_Suc_0 [simp]:
+ "m mod Suc 0 = 0"
+ using mod_by_1 [of m] by simp
+
+lemma div2_Suc_Suc [simp]:
+ "Suc (Suc m) div 2 = Suc (m div 2)"
+ by (simp add: numeral_2_eq_2 le_div_geq)
+
+lemma Suc_n_div_2_gt_zero [simp]:
+ "0 < Suc n div 2" if "n > 0" for n :: nat
+ using that by (cases n) simp_all
+
+lemma div_2_gt_zero [simp]:
+ "0 < n div 2" if "Suc 0 < n" for n :: nat
+ using that Suc_n_div_2_gt_zero [of "n - 1"] by simp
+
+lemma mod2_Suc_Suc [simp]:
+ "Suc (Suc m) mod 2 = m mod 2"
+ by (simp add: numeral_2_eq_2 le_mod_geq)
+
+lemma add_self_div_2 [simp]:
+ "(m + m) div 2 = m" for m :: nat
+ by (simp add: mult_2 [symmetric])
+
+lemma add_self_mod_2 [simp]:
+ "(m + m) mod 2 = 0" for m :: nat
+ by (simp add: mult_2 [symmetric])
+
+lemma mod2_gr_0 [simp]:
+ "0 < m mod 2 \<longleftrightarrow> m mod 2 = 1" for m :: nat
+proof -
+ have "m mod 2 < 2"
+ by (rule mod_less_divisor) simp
+ then have "m mod 2 = 0 \<or> m mod 2 = 1"
+ by arith
+ then show ?thesis
+ by auto
+qed
+
+lemma mod_Suc_eq [mod_simps]:
+ "Suc (m mod n) mod n = Suc m mod n"
+proof -
+ have "(m mod n + 1) mod n = (m + 1) mod n"
+ by (simp only: mod_simps)
+ then show ?thesis
+ by simp
+qed
+
+lemma mod_Suc_Suc_eq [mod_simps]:
+ "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
+proof -
+ have "(m mod n + 2) mod n = (m + 2) mod n"
+ by (simp only: mod_simps)
+ then show ?thesis
+ by simp
+qed
+
+lemma
+ Suc_mod_mult_self1 [simp]: "Suc (m + k * n) mod n = Suc m mod n"
+ and Suc_mod_mult_self2 [simp]: "Suc (m + n * k) mod n = Suc m mod n"
+ and Suc_mod_mult_self3 [simp]: "Suc (k * n + m) mod n = Suc m mod n"
+ and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
+ by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+
+
+lemma div_mult1_eq: -- \<open>TODO: Generalization candidate\<close>
+ "(a * b) div c = a * (b div c) + a * (b mod c) div c" for a b c :: nat
+ apply (cases "c = 0")
+ apply simp
+ apply (rule div_eqI [of _ "(a * (b mod c)) mod c"])
+ apply (auto simp add: algebra_simps distrib_left [symmetric])
+ done
+
+lemma div_add1_eq: -- \<open>NOT suitable for rewriting: the RHS has an instance of the LHS\<close>
+ -- \<open>TODO: Generalization candidate\<close>
+ "(a + b) div c = a div c + b div c + ((a mod c + b mod c) div c)" for a b c :: nat
+ apply (cases "c = 0")
+ apply simp
+ apply (rule div_eqI [of _ "(a mod c + b mod c) mod c"])
+ apply (auto simp add: algebra_simps)
+ done
+
+context
+ fixes m n q :: nat
+begin
+
+private lemma eucl_rel_mult2:
+ "m mod n + n * (m div n mod q) < n * q"
+ if "n > 0" and "q > 0"
+proof -
+ from \<open>n > 0\<close> have "m mod n < n"
+ by (rule mod_less_divisor)
+ from \<open>q > 0\<close> have "m div n mod q < q"
+ by (rule mod_less_divisor)
+ then obtain s where "q = Suc (m div n mod q + s)"
+ by (blast dest: less_imp_Suc_add)
+ moreover have "m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)"
+ using \<open>m mod n < n\<close> by (simp add: add_mult_distrib2)
+ ultimately show ?thesis
+ by simp
+qed
+
+lemma div_mult2_eq:
+ "m div (n * q) = (m div n) div q"
+proof (cases "n = 0 \<or> q = 0")
+ case True
+ then show ?thesis
+ by auto
+next
+ case False
+ with eucl_rel_mult2 show ?thesis
+ by (auto intro: div_eqI [of _ "n * (m div n mod q) + m mod n"]
+ simp add: algebra_simps add_mult_distrib2 [symmetric])
+qed
+
+lemma mod_mult2_eq:
+ "m mod (n * q) = n * (m div n mod q) + m mod n"
+proof (cases "n = 0 \<or> q = 0")
+ case True
+ then show ?thesis
+ by auto
+next
+ case False
+ with eucl_rel_mult2 show ?thesis
+ by (auto intro: mod_eqI [of _ _ "(m div n) div q"]
+ simp add: algebra_simps add_mult_distrib2 [symmetric])
+qed
+
+end
+
+lemma div_le_mono:
+ "m div k \<le> n div k" if "m \<le> n" for m n k :: nat
+proof -
+ from that obtain q where "n = m + q"
+ by (auto simp add: le_iff_add)
+ then show ?thesis
+ by (simp add: div_add1_eq [of m q k])
+qed
+
+text \<open>Antimonotonicity of @{const divide} in second argument\<close>
+
+lemma div_le_mono2:
+ "k div n \<le> k div m" if "0 < m" and "m \<le> n" for m n k :: nat
+using that proof (induct k arbitrary: m rule: less_induct)
+ case (less k)
+ show ?case
+ proof (cases "n \<le> k")
+ case False
+ then show ?thesis
+ by simp
+ next
+ case True
+ have "(k - n) div n \<le> (k - m) div n"
+ using less.prems
+ by (blast intro: div_le_mono diff_le_mono2)
+ also have "\<dots> \<le> (k - m) div m"
+ using \<open>n \<le> k\<close> less.prems less.hyps [of "k - m" m]
+ by simp
+ finally show ?thesis
+ using \<open>n \<le> k\<close> less.prems
+ by (simp add: le_div_geq)
+ qed
+qed
+
+lemma div_le_dividend [simp]:
+ "m div n \<le> m" for m n :: nat
+ using div_le_mono2 [of 1 n m] by (cases "n = 0") simp_all
+
+lemma div_less_dividend [simp]:
+ "m div n < m" if "1 < n" and "0 < m" for m n :: nat
+using that proof (induct m rule: less_induct)
+ case (less m)
+ show ?case
+ proof (cases "n < m")
+ case False
+ with less show ?thesis
+ by (cases "n = m") simp_all
+ next
+ case True
+ then show ?thesis
+ using less.hyps [of "m - n"] less.prems
+ by (simp add: le_div_geq)
+ qed
+qed
+
+lemma div_eq_dividend_iff:
+ "m div n = m \<longleftrightarrow> n = 1" if "m > 0" for m n :: nat
+proof
+ assume "n = 1"
+ then show "m div n = m"
+ by simp
+next
+ assume P: "m div n = m"
+ show "n = 1"
+ proof (rule ccontr)
+ have "n \<noteq> 0"
+ by (rule ccontr) (use that P in auto)
+ moreover assume "n \<noteq> 1"
+ ultimately have "n > 1"
+ by simp
+ with that have "m div n < m"
+ by simp
+ with P show False
+ by simp
+ qed
+qed
+
+lemma less_mult_imp_div_less:
+ "m div n < i" if "m < i * n" for m n i :: nat
+proof -
+ from that have "i * n > 0"
+ by (cases "i * n = 0") simp_all
+ then have "i > 0" and "n > 0"
+ by simp_all
+ have "m div n * n \<le> m"
+ by simp
+ then have "m div n * n < i * n"
+ using that by (rule le_less_trans)
+ with \<open>n > 0\<close> show ?thesis
+ by simp
+qed
+
+text \<open>A fact for the mutilated chess board\<close>
+
+lemma mod_Suc:
+ "Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))" (is "_ = ?rhs")
+proof (cases "n = 0")
+ case True
+ then show ?thesis
+ by simp
+next
+ case False
+ have "Suc m mod n = Suc (m mod n) mod n"
+ by (simp add: mod_simps)
+ also have "\<dots> = ?rhs"
+ using False by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq)
+ finally show ?thesis .
+qed
+
+lemma Suc_times_mod_eq:
+ "Suc (m * n) mod m = 1" if "Suc 0 < m"
+ using that by (simp add: mod_Suc)
+
+lemma Suc_times_numeral_mod_eq [simp]:
+ "Suc (numeral k * n) mod numeral k = 1" if "numeral k \<noteq> (1::nat)"
+ by (rule Suc_times_mod_eq) (use that in simp)
+
+lemma Suc_div_le_mono [simp]:
+ "m div n \<le> Suc m div n"
+ by (simp add: div_le_mono)
+
+text \<open>These lemmas collapse some needless occurrences of Suc:
+ at least three Sucs, since two and fewer are rewritten back to Suc again!
+ We already have some rules to simplify operands smaller than 3.\<close>
+
+lemma div_Suc_eq_div_add3 [simp]:
+ "m div Suc (Suc (Suc n)) = m div (3 + n)"
+ by (simp add: Suc3_eq_add_3)
+
+lemma mod_Suc_eq_mod_add3 [simp]:
+ "m mod Suc (Suc (Suc n)) = m mod (3 + n)"
+ by (simp add: Suc3_eq_add_3)
+
+lemma Suc_div_eq_add3_div:
+ "Suc (Suc (Suc m)) div n = (3 + m) div n"
+ by (simp add: Suc3_eq_add_3)
+
+lemma Suc_mod_eq_add3_mod:
+ "Suc (Suc (Suc m)) mod n = (3 + m) mod n"
+ by (simp add: Suc3_eq_add_3)
+
+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 (in field_char_0) of_nat_div:
+ "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
+proof -
+ have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
+ unfolding of_nat_add by (cases "n = 0") simp_all
+ then show ?thesis
+ by simp
+qed
+
+text \<open>An ``induction'' law for modulus arithmetic.\<close>
+
+lemma mod_induct [consumes 3, case_names step]:
+ "P m" if "P n" and "n < p" and "m < p"
+ and step: "\<And>n. n < p \<Longrightarrow> P n \<Longrightarrow> P (Suc n mod p)"
+using \<open>m < p\<close> proof (induct m)
+ case 0
+ show ?case
+ proof (rule ccontr)
+ assume "\<not> P 0"
+ from \<open>n < p\<close> have "0 < p"
+ by simp
+ from \<open>n < p\<close> obtain m where "0 < m" and "p = n + m"
+ by (blast dest: less_imp_add_positive)
+ with \<open>P n\<close> have "P (p - m)"
+ by simp
+ moreover have "\<not> P (p - m)"
+ using \<open>0 < m\<close> proof (induct m)
+ case 0
+ then show ?case
+ by simp
+ next
+ case (Suc m)
+ show ?case
+ proof
+ assume P: "P (p - Suc m)"
+ with \<open>\<not> P 0\<close> have "Suc m < p"
+ by (auto intro: ccontr)
+ then have "Suc (p - Suc m) = p - m"
+ by arith
+ moreover from \<open>0 < p\<close> have "p - Suc m < p"
+ by arith
+ with P step have "P ((Suc (p - Suc m)) mod p)"
+ by blast
+ ultimately show False
+ using \<open>\<not> P 0\<close> Suc.hyps by (cases "m = 0") simp_all
+ qed
+ qed
+ ultimately show False
+ by blast
+ qed
+next
+ case (Suc m)
+ then have "m < p" and mod: "Suc m mod p = Suc m"
+ by simp_all
+ from \<open>m < p\<close> have "P m"
+ by (rule Suc.hyps)
+ with \<open>m < p\<close> have "P (Suc m mod p)"
+ by (rule step)
+ with mod show ?case
+ 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
+
+
+subsection \<open>Code generation\<close>
+
+code_identifier
+ code_module Euclidean_Division \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
+
+end
--- a/src/HOL/Library/Code_Target_Nat.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Library/Code_Target_Nat.thy Sun Oct 08 22:28:21 2017 +0200
@@ -95,7 +95,7 @@
lemma [code]:
"Divides.divmod_nat m n = (m div n, m mod n)"
- by (fact divmod_nat_div_mod)
+ by (fact divmod_nat_def)
lemma [code]:
"divmod m n = map_prod nat_of_integer nat_of_integer (divmod m n)"
@@ -130,7 +130,7 @@
proof -
from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
show ?thesis
- by (simp add: Let_def divmod_nat_div_mod of_nat_add [symmetric])
+ by (simp add: Let_def divmod_nat_def of_nat_add [symmetric])
(simp add: * mult.commute of_nat_mult add.commute)
qed
--- a/src/HOL/Library/RBT_Impl.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Sun Oct 08 22:28:21 2017 +0200
@@ -1169,7 +1169,7 @@
apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
apfst (Branch B t1 k v) (rbtreeify_f n' kvs'))"
-by (subst rbtreeify_f.simps) (simp only: Let_def divmod_nat_div_mod prod.case)
+by (subst rbtreeify_f.simps) (simp only: Let_def divmod_nat_def prod.case)
lemma rbtreeify_g_code [code]:
"rbtreeify_g n kvs =
@@ -1180,7 +1180,7 @@
apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
apfst (Branch B t1 k v) (rbtreeify_g n' kvs'))"
-by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_div_mod prod.case)
+by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_def prod.case)
lemma Suc_double_half: "Suc (2 * n) div 2 = n"
by simp
--- a/src/HOL/Parity.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Parity.thy Sun Oct 08 22:28:21 2017 +0200
@@ -101,6 +101,92 @@
end
+class unique_euclidean_semiring_parity = unique_euclidean_semiring +
+ assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
+ assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
+ assumes zero_not_eq_two: "0 \<noteq> 2"
+begin
+
+lemma parity_cases [case_names even odd]:
+ assumes "a mod 2 = 0 \<Longrightarrow> P"
+ assumes "a mod 2 = 1 \<Longrightarrow> P"
+ shows P
+ using assms parity by blast
+
+lemma one_div_two_eq_zero [simp]:
+ "1 div 2 = 0"
+proof (cases "2 = 0")
+ case True then show ?thesis by simp
+next
+ case False
+ from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
+ with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
+ then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
+ then have "1 div 2 = 0 \<or> 2 = 0" by simp
+ 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)
+ show "1 mod 2 = 1"
+ by (fact one_mod_two_eq_one)
+next
+ fix a b
+ assume "a mod 2 = 1"
+ moreover assume "b mod 2 = 1"
+ ultimately show "(a + b) mod 2 = 0"
+ using mod_add_eq [of a 2 b] by simp
+next
+ fix a b
+ assume "(a * b) mod 2 = 0"
+ then have "(a mod 2) * (b mod 2) mod 2 = 0"
+ by (simp add: mod_mult_eq)
+ then have "(a mod 2) * (b mod 2) = 0"
+ by (cases "a mod 2 = 0") simp_all
+ then show "a mod 2 = 0 \<or> b mod 2 = 0"
+ by (rule divisors_zero)
+next
+ fix a
+ assume "a mod 2 = 1"
+ then have "a = a div 2 * 2 + 1"
+ using div_mult_mod_eq [of a 2] by simp
+ then show "\<exists>b. a = b + 1" ..
+qed
+
+lemma even_iff_mod_2_eq_zero:
+ "even a \<longleftrightarrow> a mod 2 = 0"
+ by (fact dvd_eq_mod_eq_0)
+
+lemma odd_iff_mod_2_eq_one:
+ "odd a \<longleftrightarrow> a mod 2 = 1"
+ by (simp add: even_iff_mod_2_eq_zero)
+
+lemma even_succ_div_two [simp]:
+ "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
+ by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
+
+lemma odd_succ_div_two [simp]:
+ "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
+ by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
+
+lemma even_two_times_div_two:
+ "even a \<Longrightarrow> 2 * (a div 2) = a"
+ by (fact dvd_mult_div_cancel)
+
+lemma odd_two_times_div_two_succ [simp]:
+ "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
+ using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
+
+end
+
subsection \<open>Instances for @{typ nat} and @{typ int}\<close>
@@ -190,9 +276,6 @@
for k l :: int
using even_abs_add_iff [of l k] by (simp add: ac_simps)
-lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
- by (auto elim: oddE)
-
instance int :: ring_parity
proof
show "\<not> 2 dvd (1 :: int)"
--- a/src/HOL/Rings.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Rings.thy Sun Oct 08 22:28:21 2017 +0200
@@ -1620,6 +1620,10 @@
shows "c dvd a"
using assms dvd_mod_iff [of c b a] by simp
+lemma dvd_minus_mod [simp]:
+ "b dvd a - a mod b"
+ by (simp add: minus_mod_eq_div_mult)
+
end
class idom_modulo = idom + semidom_modulo
--- a/src/HOL/Word/Word.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Word/Word.thy Sun Oct 08 22:28:21 2017 +0200
@@ -2024,7 +2024,7 @@
lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse]
-lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1]
+lemmas thd = times_div_less_eq_dividend
lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle
@@ -3724,7 +3724,7 @@
lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
(* alternative proof of word_rcat_rsplit *)
-lemmas tdle = iffD2 [OF split_div_lemma refl, THEN conjunct1]
+lemmas tdle = times_div_less_eq_dividend
lemmas dtle = xtr4 [OF tdle mult.commute]
lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
@@ -3734,7 +3734,7 @@
apply (simp_all add: word_size
refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
apply safe
- apply (erule xtr7, rule len_gt_0 [THEN dtle])+
+ apply (erule xtr7, rule dtle)+
done
lemma size_word_rsplit_rcat_size:
--- a/src/HOL/Word/Word_Miscellaneous.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy Sun Oct 08 22:28:21 2017 +0200
@@ -304,8 +304,8 @@
lemmas pl_pl_mm' = add.commute [THEN [2] trans, THEN pl_pl_mm]
lemmas dme = div_mult_mod_eq
-lemmas dtle = xtr3 [OF dme [symmetric] le_add1]
-lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle]
+lemmas dtle = div_times_less_eq_dividend
+lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] div_times_less_eq_dividend]
lemma td_gal: "0 < c \<Longrightarrow> a \<ge> b * c \<longleftrightarrow> a div c \<ge> b"
for a b c :: nat
@@ -316,15 +316,13 @@
lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified]
-lemma div_mult_le: "a div b * b \<le> a"
- for a b :: nat
- by (fact dtle)
+lemmas div_mult_le = div_times_less_eq_dividend
-lemmas sdl = split_div_lemma [THEN iffD1, symmetric]
+lemmas sdl = div_nat_eqI
lemma given_quot: "f > 0 \<Longrightarrow> (f * l + (f - 1)) div f = l"
for f l :: nat
- by (rule sdl, assumption) (simp (no_asm))
+ by (rule div_nat_eqI) (simp_all)
lemma given_quot_alt: "f > 0 \<Longrightarrow> (l * f + f - Suc 0) div f = l"
for f l :: nat