--- a/src/HOL/Library/Float.thy Tue Jan 14 18:46:58 2025 +0000
+++ b/src/HOL/Library/Float.thy Tue Jan 14 21:50:44 2025 +0000
@@ -113,7 +113,7 @@
by (cases x rule: linorder_cases[of 0]) auto
lemma sgn_of_float[simp]: "x \<in> float \<Longrightarrow> sgn x \<in> float"
- by (cases x rule: linorder_cases[of 0]) (auto intro!: uminus_float)
+ by (simp add: sgn_real_def)
lemma div_power_2_float[simp]: "x \<in> float \<Longrightarrow> x / 2^d \<in> float"
by (simp add: float_def) (metis of_int_diff of_int_of_nat_eq powr_diff powr_realpow zero_less_numeral times_divide_eq_right)
@@ -144,8 +144,8 @@
from assms obtain m e :: int where "a = m * 2 powr e"
by (auto simp: float_def)
then show ?thesis
- by (auto intro!: floatI[where m="m^b" and e = "e*b"]
- simp: power_mult_distrib powr_realpow[symmetric] powr_powr)
+ by (intro floatI[where m="m^b" and e = "e*b"])
+ (auto simp: powr_powr power_mult_distrib simp flip: powr_realpow)
qed
lift_definition Float :: "int \<Rightarrow> int \<Rightarrow> float" is "\<lambda>(m::int) (e::int). m * 2 powr e"
@@ -383,11 +383,10 @@
by (auto simp: float_def)
with \<open>x \<noteq> 0\<close> int_cancel_factors[of 2 m] obtain k i where "m = k * 2 ^ i" "\<not> 2 dvd k"
by auto
- with \<open>\<not> 2 dvd k\<close> x show ?thesis
- apply (rule_tac exI[of _ "k"])
- apply (rule_tac exI[of _ "e + int i"])
- apply (simp add: powr_add powr_realpow)
- done
+ with \<open>\<not> 2 dvd k\<close> x have "x = real_of_int k * 2 powr real_of_int (e + int i) \<and> odd k"
+ by (simp add: powr_add powr_realpow)
+ then show ?thesis
+ by blast
qed
with that show thesis by blast
qed
@@ -799,7 +798,7 @@
apply (metis (no_types, opaque_lifting) Float.rep_eq
add.inverse_inverse compute_real_of_float diff_minus_eq_add
floor_divide_of_int_eq int_of_reals(1) linorder_not_le
- minus_add_distrib of_int_eq_numeral_power_cancel_iff )
+ minus_add_distrib of_int_eq_numeral_power_cancel_iff)
done
next
case False
@@ -1190,7 +1189,7 @@
using logless flogless \<open>x > 0\<close> \<open>y > 0\<close>
by (auto intro!: floor_mono)
finally show ?thesis
- by (auto simp flip: powr_realpow simp: powr_diff assms of_nat_diff)
+ by (auto simp flip: powr_realpow simp: powr_diff assms)
qed
ultimately show ?thesis
by (metis dual_order.trans truncate_down)
@@ -1264,11 +1263,9 @@
note powr_strict = powr_less_cancel_iff[symmetric, OF \<open>1 < p\<close>, THEN iffD2]
have "floor ?r = (if i \<ge> j * p powr (?fl i - ?fl j) then 0 else -1)" (is "_ = ?if")
using assms
- by (linarith |
- auto
- intro!: floor_eq2
- intro: powr_strict powr
- simp: powr_diff powr_add field_split_simps algebra_simps)+
+ apply simp
+ by (smt (verit, ccfv_SIG) floor_less_iff floor_uminus_of_int le_log_iff mult_powr_eq
+ of_int_1 real_of_int_floor_add_one_gt zero_le_floor)
finally
show ?thesis by simp
qed
@@ -2164,7 +2161,7 @@
by transfer (simp add: truncate_down_nonneg)
lemma rapprox_rat: "real_of_int x / real_of_int y \<le> real_of_float (rapprox_rat prec x y)"
- by transfer (simp add: truncate_up)
+ by (simp add: rapprox_rat.rep_eq truncate_up)
lemma rapprox_rat_le1:
assumes "0 \<le> x" "0 < y" "x \<le> y"
@@ -2232,7 +2229,7 @@
by transfer (rule real_divl_pos_less1_bound)
lemma float_divr: "real_of_float x / real_of_float y \<le> real_of_float (float_divr prec x y)"
- by transfer (rule real_divr)
+ by (simp add: float_divr.rep_eq real_divr)
lemma real_divr_pos_less1_lower_bound:
assumes "0 < x"
--- a/src/HOL/Library/Signed_Division.thy Tue Jan 14 18:46:58 2025 +0000
+++ b/src/HOL/Library/Signed_Division.thy Tue Jan 14 21:50:44 2025 +0000
@@ -104,8 +104,7 @@
"(a :: int) sdiv 1 = a"
"(a :: int) sdiv 0 = 0"
"(a :: int) sdiv -1 = -a"
- apply (auto simp: signed_divide_int_def sgn_if)
- done
+ by (auto simp: signed_divide_int_def sgn_if)
lemma smod_int_mod_0 [simp]:
"x smod (0 :: int) = x"
@@ -120,33 +119,26 @@
by (auto simp: signed_divide_int_def sgn_div_eq_sgn_mult sgn_mult)
lemma int_sdiv_same_is_1 [simp]:
- "a \<noteq> 0 \<Longrightarrow> ((a :: int) sdiv b = a) = (b = 1)"
- apply (rule iffI)
- apply (clarsimp simp: signed_divide_int_def)
- apply (subgoal_tac "b > 0")
- apply (case_tac "a > 0")
- apply (clarsimp simp: sgn_if)
- apply (simp_all add: not_less algebra_split_simps sgn_if split: if_splits)
- using int_div_less_self [of a b] apply linarith
- apply (metis add.commute add.inverse_inverse group_cancel.rule0 int_div_less_self linorder_neqE_linordered_idom neg_0_le_iff_le not_less verit_comp_simplify1(1) zless_imp_add1_zle)
- apply (metis div_minus_right neg_imp_zdiv_neg_iff neg_le_0_iff_le not_less order.not_eq_order_implies_strict)
- apply (metis abs_le_zero_iff abs_of_nonneg neg_imp_zdiv_nonneg_iff order.not_eq_order_implies_strict)
- done
+ assumes "a \<noteq> 0"
+ shows "((a :: int) sdiv b = a) = (b = 1)"
+proof -
+ have "b = 1" if "a sdiv b = a"
+ proof -
+ have "b>0"
+ by (smt (verit, ccfv_threshold) assms mult_cancel_left2 sgn_if sgn_mult
+ sgn_sdiv_eq_sgn_mult that)
+ then show ?thesis
+ by (smt (verit) assms dvd_eq_mod_eq_0 int_div_less_self of_bool_eq(1,2) sgn_if
+ signed_divide_int_eq_divide_int that zdiv_zminus1_eq_if)
+ qed
+ then show ?thesis
+ by auto
+qed
lemma int_sdiv_negated_is_minus1 [simp]:
"a \<noteq> 0 \<Longrightarrow> ((a :: int) sdiv b = - a) = (b = -1)"
- apply (clarsimp simp: signed_divide_int_def)
- apply (rule iffI)
- apply (subgoal_tac "b < 0")
- apply (case_tac "a > 0")
- apply (clarsimp simp: sgn_if algebra_split_simps not_less)
- apply (case_tac "sgn (a * b) = -1")
- apply (simp_all add: not_less algebra_split_simps sgn_if split: if_splits)
- apply (metis add.inverse_inverse int_div_less_self int_one_le_iff_zero_less less_le neg_0_less_iff_less)
- apply (metis add.inverse_inverse div_minus_right int_div_less_self int_one_le_iff_zero_less less_le neg_0_less_iff_less)
- apply (metis less_le neg_less_0_iff_less not_less pos_imp_zdiv_neg_iff)
- apply (metis div_minus_right dual_order.eq_iff neg_imp_zdiv_nonneg_iff neg_less_0_iff_less)
- done
+ using int_sdiv_same_is_1 [of _ "-b"]
+ using signed_divide_int_def by fastforce
lemma sdiv_int_range:
\<open>a sdiv b \<in> {- \<bar>a\<bar>..\<bar>a\<bar>}\<close> for a b :: int
@@ -178,9 +170,8 @@
"\<lbrakk> 0 \<le> a; b < 0 \<rbrakk> \<Longrightarrow> 0 \<le> (a :: int) smod b"
"\<lbrakk> a \<le> 0; b < 0 \<rbrakk> \<Longrightarrow> (a :: int) smod b \<le> 0"
"\<lbrakk> a \<le> 0; b < 0 \<rbrakk> \<Longrightarrow> b \<le> (a :: int) smod b"
- apply (insert smod_int_range [where a=a and b=b])
- apply (auto simp: add1_zle_eq smod_int_alt_def sgn_if)
- done
+ using smod_int_range [where a=a and b=b]
+ by (auto simp: add1_zle_eq smod_int_alt_def sgn_if)
lemma smod_mod_positive:
"\<lbrakk> 0 \<le> (a :: int); 0 \<le> b \<rbrakk> \<Longrightarrow> a smod b = a mod b"