merged
authorpaulson
Sun, 16 Mar 2025 17:02:41 +0000
changeset 82293 3fb2525699e6
parent 82289 26fbbf43863b (diff)
parent 82292 5d91cca0aaf3 (current diff)
child 82296 4dd01eb1e0cb
child 82302 19ada02fa486
merged
--- a/NEWS	Sun Mar 16 17:02:27 2025 +0000
+++ b/NEWS	Sun Mar 16 17:02:41 2025 +0000
@@ -28,13 +28,19 @@
       antisymp_equality[simp] ~> antisymp_on_equality[simp]
       transp_equality[simp] ~> transp_on_equality[simp]
   - Added lemmas.
+      antisymp_on_bot[simp]
+      asymp_on_bot[simp]
+      irreflp_on_bot[simp]
+      left_unique_bot[simp]
       left_unique_iff_Uniq
       reflp_on_refl_on_eq[pred_set_conv]
+      symp_on_bot[simp]
       symp_on_equality[simp]
       totalp_on_mono[mono]
       totalp_on_mono_strong
       totalp_on_mono_stronger
       totalp_on_mono_stronger_alt
+      transp_on_bot[simp]
 
 * Theory "HOL.Wellfounded":
   - Added lemmas.
@@ -80,6 +86,8 @@
       set_mset_sum_list[simp]
       size_mset_sum_mset_conv[simp]
 
+* Removed theory "HOL-Library.Divides" (finally).
+
 
 
 New in Isabelle2025 (March 2025)
--- a/src/HOL/Bit_Operations.thy	Sun Mar 16 17:02:27 2025 +0000
+++ b/src/HOL/Bit_Operations.thy	Sun Mar 16 17:02:41 2025 +0000
@@ -338,6 +338,57 @@
   \<open>bit (a mod 2) n \<longleftrightarrow> n = 0 \<and> odd a\<close>
   by (simp add: mod_2_eq_odd bit_simps)
 
+lemma stable_index:
+  obtains m where \<open>possible_bit TYPE('a) m\<close>
+    \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> m \<Longrightarrow> bit a n \<longleftrightarrow> bit a m\<close>
+proof -
+  have \<open>\<exists>m. possible_bit TYPE('a) m \<and> (\<forall>n\<ge>m. possible_bit TYPE('a) n \<longrightarrow> bit a n \<longleftrightarrow> bit a m)\<close>
+  proof (induction a rule: bit_induct)
+    case (stable a)
+    show ?case
+      by (rule exI [of _ \<open>0::nat\<close>]) (simp add: stable_imp_bit_iff_odd stable)
+  next
+    case (rec a b)
+    then obtain m where \<open>possible_bit TYPE('a) m\<close>
+       and hyp: \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> m \<Longrightarrow> bit a n \<longleftrightarrow> bit a m\<close>
+      by blast
+    show ?case
+    proof (cases \<open>possible_bit TYPE('a) (Suc m)\<close>)
+      case True
+      moreover have \<open>bit (of_bool b + 2 * a) n \<longleftrightarrow> bit (of_bool b + 2 * a) (Suc m)\<close>
+        if \<open>possible_bit TYPE('a) n\<close> \<open>Suc m \<le> n\<close> for n
+        using hyp [of \<open>n - 1\<close>] possible_bit_less_imp [of n \<open>n - 1\<close>] rec.hyps that
+        by (cases n) (simp_all add: bit_Suc)
+      ultimately show ?thesis
+        by blast
+    next
+      case False
+      have \<open>bit (of_bool b + 2 * a) n \<longleftrightarrow> bit (of_bool b + 2 * a) m\<close>
+        if \<open>possible_bit TYPE('a) n\<close> \<open>m \<le> n\<close> for n
+      proof (cases \<open>m = n\<close>)
+        case True
+        then show ?thesis
+          by simp
+      next
+        case False
+        with \<open>m \<le> n\<close> have \<open>m < n\<close>
+          by simp
+        with \<open>\<not> possible_bit TYPE('a) (Suc m)\<close>
+        have \<open>\<not> possible_bit TYPE('a) n\<close> using possible_bit_less_imp [of n \<open>Suc m\<close>]
+          by auto
+        with \<open>possible_bit TYPE('a) n\<close>
+        show ?thesis
+          by simp
+      qed
+      with \<open>possible_bit TYPE('a) m\<close> show ?thesis
+        by blast
+    qed
+  qed
+  with that show thesis
+    by blast
+qed
+
+
 end
 
 lemma nat_bit_induct [case_names zero even odd]:
@@ -1105,6 +1156,20 @@
   qed
 qed
 
+lemma impossible_bit_imp_take_bit_eq_self:
+  \<open>take_bit n a = a\<close> if \<open>\<not> possible_bit TYPE('a) n\<close>
+proof -
+  have \<open>drop_bit n a = 0\<close>
+  proof (rule bit_eqI)
+    fix m
+    show \<open>bit (drop_bit n a) m \<longleftrightarrow> bit 0 m\<close>
+      using possible_bit_less_imp [of \<open>n + m\<close> n] that
+      by (auto simp add: bit_simps dest: bit_imp_possible_bit)
+  qed
+  then show ?thesis
+    by (simp add: take_bit_eq_self_iff_drop_bit_eq_0)
+qed
+
 lemma drop_bit_exp_eq:
   \<open>drop_bit m (2 ^ n) = of_bool (m \<le> n \<and> possible_bit TYPE('a) n) * 2 ^ (n - m)\<close>
   by (auto simp: bit_eq_iff bit_simps)
@@ -1486,6 +1551,11 @@
   \<open>take_bit m (NOT (mask n)) = 0\<close> if \<open>n \<ge> m\<close>
   by (rule bit_eqI) (use that in \<open>simp add: bit_take_bit_iff bit_not_iff bit_mask_iff\<close>)
 
+lemma mask_eq_minus_one_if_not_possible_bit:
+  \<open>mask n = - 1\<close> if \<open>\<not> possible_bit TYPE('a) n\<close>
+  using that mask_eq_take_bit_minus_one [of n] impossible_bit_imp_take_bit_eq_self [of n \<open>- 1\<close>]
+  by simp
+
 lemma unset_bit_eq_and_not:
   \<open>unset_bit n a = a AND NOT (push_bit n 1)\<close>
   by (rule bit_eqI) (auto simp: bit_simps)
--- a/src/HOL/Library/Divides.thy	Sun Mar 16 17:02:27 2025 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-(*  Title:      HOL/Library/Divides.thy
-*)
-
-section \<open>Misc lemmas on division, to be sorted out finally\<close>
-
-theory Divides
-imports Main
-begin
-
-class unique_euclidean_semiring_numeral = linordered_euclidean_semiring + discrete_linordered_semidom +
-  assumes div_less [no_atp]: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
-    and mod_less [no_atp]: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
-    and div_positive [no_atp]: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
-    and mod_less_eq_dividend [no_atp]: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
-    and pos_mod_bound [no_atp]: "0 < b \<Longrightarrow> a mod b < b"
-    and pos_mod_sign [no_atp]: "0 < b \<Longrightarrow> 0 \<le> a mod b"
-    and mod_mult2_eq [no_atp]: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
-    and div_mult2_eq [no_atp]: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
-
-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
-
-context unique_euclidean_semiring_numeral
-begin
-
-context
-begin
-
-qualified lemma discrete [no_atp]:
-  "a < b \<longleftrightarrow> a + 1 \<le> b"
-  by (fact less_iff_succ_less_eq)
-
-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")
-proof -
-  from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
-    by (auto intro: trans)
-  with \<open>0 < b\<close> have "0 < a div b" by (auto intro: div_positive)
-  then have [simp]: "1 \<le> a div b" by (simp add: discrete)
-  with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
-  define w where "w = a div b mod 2"
-  then have w_exhaust: "w = 0 \<or> w = 1" by auto
-  have mod_w: "a mod (2 * b) = a mod b + b * w"
-    by (simp add: w_def mod_mult2_eq ac_simps)
-  from assms w_exhaust have "w = 1"
-    using mod_less by (auto simp add: mod_w)
-  with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
-  have "2 * (a div (2 * b)) = a div b - w"
-    by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
-  with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
-  then show ?P and ?Q
-    by (simp_all add: div mod add_implies_diff [symmetric])
-qed
-
-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")
-proof -
-  define w where "w = a div b mod 2"
-  then have w_exhaust: "w = 0 \<or> w = 1" by auto
-  have mod_w: "a mod (2 * b) = a mod b + b * w"
-    by (simp add: w_def mod_mult2_eq ac_simps)
-  moreover have "b \<le> a mod b + b"
-  proof -
-    from \<open>0 < b\<close> pos_mod_sign have "0 \<le> a mod b" by blast
-    then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
-    then show ?thesis by simp
-  qed
-  moreover note assms w_exhaust
-  ultimately have "w = 0" by auto
-  with mod_w have mod: "a mod (2 * b) = a mod b" by simp
-  have "2 * (a div (2 * b)) = a div b - w"
-    by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
-  with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
-  then show ?P and ?Q
-    by (simp_all add: div mod)
-qed
-
-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")
-  case True
-  thus ?thesis using assms using divmod_digit_0(2)[of m x] by auto
-next
-  case False
-  hence *: "x mod (2 * m) - m = x mod m"
-    using assms by (intro divmod_digit_1) auto
-  hence "x mod (2 * m) = x mod m + m"
-    by (subst * [symmetric], subst le_add_diff_inverse2) (use False in auto)
-  thus ?thesis by simp
-qed
-
-end
-
-end
-
-instance nat :: unique_euclidean_semiring_numeral
-  by standard
-    (auto simp add: div_greater_zero_iff div_mult2_eq mod_mult2_eq)
-
-instance int :: unique_euclidean_semiring_numeral
-  by standard (auto intro: zmod_le_nonneg_dividend simp add:
-    pos_imp_zdiv_pos_iff zmod_zmult2_eq zdiv_zmult2_eq)
-
-context
-begin
-
-qualified lemma zmod_eq_0D: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: int
-  using that by auto
-
-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>)
-
-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>)
-
-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)
-
-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
-
-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
-
-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)
-
-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
-
-end
--- a/src/HOL/ROOT	Sun Mar 16 17:02:27 2025 +0000
+++ b/src/HOL/ROOT	Sun Mar 16 17:02:41 2025 +0000
@@ -96,8 +96,6 @@
     Old_Recdef
     Realizers
     Refute
-    (*transitional theories*)
-    Divides
   document_files "root.bib" "root.tex"
 
 session "HOL-Analysis" (main timing) in Analysis = HOL +
--- a/src/HOL/Relation.thy	Sun Mar 16 17:02:27 2025 +0000
+++ b/src/HOL/Relation.thy	Sun Mar 16 17:02:41 2025 +0000
@@ -316,6 +316,9 @@
 lemma irreflpD: "irreflp R \<Longrightarrow> \<not> R x x"
   by (rule irreflD[to_pred])
 
+lemma irreflp_on_bot[simp]: "irreflp_on A \<bottom>"
+  by (simp add: irreflp_on_def)
+
 lemma irrefl_on_distinct [code]: "irrefl_on A r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<noteq> b)"
   by (auto simp add: irrefl_on_def)
 
@@ -382,6 +385,9 @@
 lemma asympD: "asymp R \<Longrightarrow> R x y \<Longrightarrow> \<not> R y x"
   by (rule asymD[to_pred])
 
+lemma asymp_on_bot[simp]: "asymp_on A \<bottom>"
+  by (simp add: asymp_on_def)
+
 lemma asym_iff: "asym r \<longleftrightarrow> (\<forall>x y. (x,y) \<in> r \<longrightarrow> (y,x) \<notin> r)"
   by (blast dest: asymD)
 
@@ -434,6 +440,9 @@
 
 lemmas symp_sym_eq = symp_on_sym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
 
+lemma symp_on_bot[simp]: "symp_on A \<bottom>"
+  by (simp add: symp_on_def)
+
 lemma sym_on_subset: "sym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> sym_on B r"
   by (auto simp: sym_on_def)
 
@@ -533,6 +542,9 @@
 
 lemmas antisymp_antisym_eq = antisymp_on_antisym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
 
+lemma antisymp_on_bot[simp]: "antisymp_on A \<bottom>"
+  by (simp add: antisymp_on_def)
+
 lemma antisym_on_subset: "antisym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> antisym_on B r"
   by (auto simp: antisym_on_def)
 
@@ -723,8 +735,11 @@
 lemma trans_empty [simp]: "trans {}"
   by (blast intro: transI)
 
+lemma transp_on_bot[simp]: "transp_on A \<bottom>"
+  by (simp add: transp_on_def)
+
 lemma transp_empty [simp]: "transp (\<lambda>x y. False)"
-  using trans_empty[to_pred] by (simp add: bot_fun_def)
+  using transp_on_bot unfolding bot_fun_def bot_bool_def .
 
 lemma trans_singleton [simp]: "trans {(a, a)}"
   by (blast intro: transI)
@@ -886,6 +901,9 @@
 lemma left_unique_iff_Uniq: "left_unique r \<longleftrightarrow> (\<forall>y. \<exists>\<^sub>\<le>\<^sub>1x. r x y)"
   unfolding Uniq_def left_unique_def by blast
 
+lemma left_unique_bot[simp]: "left_unique \<bottom>"
+  by (simp add: left_unique_def)
+
 
 subsubsection \<open>Right uniqueness\<close>