--- 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>