# HG changeset patch
# User haftmann
# Date 1694846324 0
# Node ID 18ea58bdcf77b0929faea2a123fd136668dce4c4
# Parent  d52934f126d4596fc2ae15f0fde8e95194671a5b
reduced prominence of lemma names

diff -r d52934f126d4 -r 18ea58bdcf77 src/HOL/Code_Numeral.thy
--- 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>
diff -r d52934f126d4 -r 18ea58bdcf77 src/HOL/Divides.thy
--- 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
 
diff -r d52934f126d4 -r 18ea58bdcf77 src/HOL/Real.thy
--- 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"