--- a/src/HOL/Code_Numeral.thy Sat Sep 16 06:38:44 2023 +0000
+++ b/src/HOL/Code_Numeral.thy Sat Sep 16 06:38:44 2023 +0000
@@ -5,7 +5,7 @@
section \<open>Numeric types for code generation onto target language numerals only\<close>
theory Code_Numeral
-imports Divides Lifting Bit_Operations
+imports Lifting Bit_Operations
begin
subsection \<open>Type of target language integers\<close>
--- a/src/HOL/Divides.thy Sat Sep 16 06:38:44 2023 +0000
+++ b/src/HOL/Divides.thy Sat Sep 16 06:38:44 2023 +0000
@@ -18,12 +18,15 @@
and div_mult2_eq [no_atp]: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
assumes discrete [no_atp]: "a < b \<longleftrightarrow> a + 1 \<le> b"
-hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
+hide_fact (open) div_less mod_less div_positive mod_less_eq_dividend pos_mod_bound pos_mod_sign mod_mult2_eq div_mult2_eq discrete
context unique_euclidean_semiring_numeral
begin
-lemma divmod_digit_1 [no_atp]:
+context
+begin
+
+qualified lemma divmod_digit_1 [no_atp]:
assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
and "a mod (2 * b) - b = a mod b" (is "?Q")
@@ -47,7 +50,7 @@
by (simp_all add: div mod add_implies_diff [symmetric])
qed
-lemma divmod_digit_0 [no_atp]:
+qualified lemma divmod_digit_0 [no_atp]:
assumes "0 < b" and "a mod (2 * b) < b"
shows "2 * (a div (2 * b)) = a div b" (is "?P")
and "a mod (2 * b) = a mod b" (is "?Q")
@@ -72,7 +75,7 @@
by (simp_all add: div mod)
qed
-lemma mod_double_modulus [no_atp]:
+qualified lemma mod_double_modulus [no_atp]:
assumes "m > 0" "x \<ge> 0"
shows "x mod (2 * m) = x mod m \<or> x mod (2 * m) = x mod m + m"
proof (cases "x mod (2 * m) < m")
@@ -89,6 +92,8 @@
end
+end
+
instance nat :: unique_euclidean_semiring_numeral
by standard
(auto simp add: div_greater_zero_iff div_mult2_eq mod_mult2_eq)
@@ -97,32 +102,37 @@
by standard (auto intro: zmod_le_nonneg_dividend simp add:
pos_imp_zdiv_pos_iff zmod_zmult2_eq zdiv_zmult2_eq)
+context
+begin
+
(* REVISIT: should this be generalized to all semiring_div types? *)
-lemma zmod_eq_0D [dest!]: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: int
+qualified 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_geq [no_atp]: "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
+qualified lemma div_geq [no_atp]: "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 [no_atp]: "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
+qualified lemma mod_geq [no_atp]: "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_0D [no_atp]: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: nat
+qualified lemma mod_eq_0D [no_atp]: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: nat
using that by (auto simp add: mod_eq_0_iff_dvd)
-lemma pos_mod_conj [no_atp]: "0 < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b" for a b :: int
+qualified lemma pos_mod_conj [no_atp]: "0 < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b" for a b :: int
by simp
-lemma neg_mod_conj [no_atp]: "b < 0 \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b" for a b :: int
+qualified lemma neg_mod_conj [no_atp]: "b < 0 \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b" for a b :: int
by simp
-lemma zmod_eq_0_iff [no_atp]: "m mod d = 0 \<longleftrightarrow> (\<exists>q. m = d * q)" for m d :: int
+qualified lemma zmod_eq_0_iff [no_atp]: "m mod d = 0 \<longleftrightarrow> (\<exists>q. m = d * q)" for m d :: int
by (auto simp add: mod_eq_0_iff_dvd)
-lemma div_positive_int [no_atp]:
+qualified lemma div_positive_int [no_atp]:
"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
+
code_identifier
code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
--- a/src/HOL/Real.thy Sat Sep 16 06:38:44 2023 +0000
+++ b/src/HOL/Real.thy Sat Sep 16 06:38:44 2023 +0000
@@ -1041,10 +1041,17 @@
by simp
lemma nat_less_real_le: "n < m \<longleftrightarrow> real n + 1 \<le> real m"
- by (metis discrete of_nat_1 of_nat_add of_nat_le_iff)
+proof -
+ have \<open>n < m \<longleftrightarrow> Suc n \<le> m\<close>
+ by (simp add: less_eq_Suc_le)
+ also have \<open>\<dots> \<longleftrightarrow> real (Suc n) \<le> real m\<close>
+ by (simp only: of_nat_le_iff)
+ also have \<open>\<dots> \<longleftrightarrow> real n + 1 \<le> real m\<close>
+ by (simp add: ac_simps)
+ finally show ?thesis .
+qed
lemma nat_le_real_less: "n \<le> m \<longleftrightarrow> real n < real m + 1"
- for m n :: nat
by (meson nat_less_real_le not_le)
lemma real_of_nat_div_aux: "real x / real d = real (x div d) + real (x mod d) / real d"