Better multiplication and division rules for ln and log

--- a/src/HOL/Analysis/Kronecker_Approximation_Theorem.thy	Sun Jul 07 22:25:34 2024 +0100
+++ b/src/HOL/Analysis/Kronecker_Approximation_Theorem.thy	Mon Jul 08 22:27:50 2024 +0100
@@ -1157,7 +1157,7 @@
     have "ln (real (n + 1) / L) \<le> 0"
       using * eventually_at_top_dense by (intro tendsto_lowerbound [OF 0]) auto
     then have "n+1 \<le> L"
-      by (simp add: ln_div)
+      using \<open>0 < L\<close> by (simp add: ln_div)
     then show ?thesis
       using L_le by linarith
   qed

--- a/src/HOL/Nonstandard_Analysis/HLog.thy	Sun Jul 07 22:25:34 2024 +0100
+++ b/src/HOL/Nonstandard_Analysis/HLog.thy	Mon Jul 08 22:27:50 2024 +0100
@@ -73,7 +73,7 @@
   by transfer simp
 
 lemma hlog_mult:
-  "\<And>a x y. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> (x\<noteq>0 \<longleftrightarrow> y\<noteq>0) \<Longrightarrow> hlog a (x * y) = hlog a x + hlog a y"
+  "\<And>a x y. hlog a (x * y) = (if x\<noteq>0 \<and> y\<noteq>0 then hlog a x + hlog a y else 0)"
   by transfer (rule log_mult)
 
 lemma hlog_as_starfun: "\<And>a x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a x = ( *f* ln) x / ( *f* ln) a"
@@ -111,10 +111,10 @@
 lemma hlog_eq_one [simp]: "\<And>a. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a a = 1"
   by transfer (rule log_eq_one)
 
-lemma hlog_inverse: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> hlog a (inverse x) = - hlog a x"
-  by (rule add_left_cancel [of "hlog a x", THEN iffD1]) (simp add: hlog_mult [symmetric])
+lemma hlog_inverse: "\<And>a x. hlog a (inverse x) = - hlog a x"
+  by transfer (simp add: log_inverse)
 
-lemma hlog_divide: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a (x / y) = hlog a x - hlog a y"
+lemma hlog_divide: "hlog a (x / y) = (if x\<noteq>0 \<and> y\<noteq>0 then hlog a x - hlog a y else 0)"
   by (simp add: hlog_mult hlog_inverse divide_inverse)
 
 lemma hlog_less_cancel_iff [simp]:

--- a/src/HOL/Probability/Information.thy	Sun Jul 07 22:25:34 2024 +0100
+++ b/src/HOL/Probability/Information.thy	Mon Jul 08 22:27:50 2024 +0100
@@ -10,15 +10,6 @@
   Independent_Family
 begin
 
-
-lemma log_mult_nz:
-  "x\<noteq>0 \<Longrightarrow> y\<noteq>0 \<Longrightarrow> log a (x * y) = log a x + log a y"
-  by (simp add: log_def ln_mult divide_inverse distrib_right)
-
-lemma log_divide_nz:
-  "x\<noteq>0 \<Longrightarrow> y\<noteq>0 \<Longrightarrow> log a (x / y) = log a x - log a y"
-  by (simp add: diff_divide_distrib ln_div log_def)
-
 subsection "Information theory"
 
 locale information_space = prob_space +
@@ -554,11 +545,8 @@
     show "AE x in S \<Otimes>\<^sub>M
             T. Pxy x * log b (Pxy x) - Pxy x * log b (Px (fst x)) - Pxy x * log b (Py (snd x)) 
           = f x"
-      using A B unfolding f_def
-
-      apply  (auto simp: f_def field_simps space_pair_measure Px_nn Py_nn Pxy_nn
-          less_le )
-      by (smt (verit, del_insts) AE_I2 distrib_left log_divide log_mult mult_eq_0_iff)
+      using A B 
+      by (auto simp: f_def field_simps space_pair_measure log_mult log_divide)
   qed
 
   show "0 \<le> ?M" unfolding M
@@ -1097,9 +1085,7 @@
     have "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>x. Pxyz x * - log b (?f x))"
       apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
       using ae1 ae2 ae3 ae4 
-      apply (auto simp: log_divide log_mult zero_le_mult_iff zero_less_mult_iff zero_less_divide_iff field_simps
-          less_le space_pair_measure split: prod.split)
-      by (smt (verit, best) AE_I2 fst_conv log_divide mult_cancel_left mult_minus_right snd_conv)
+      by (auto simp: log_mult log_divide field_simps)
     then
     show "integrable ?P (\<lambda>x. - log b (?f x))"
       by (subst integrable_real_density) (auto simp: space_pair_measure) 
@@ -1112,9 +1098,7 @@
      apply simp
     apply (intro integral_cong_AE)
     using ae1 ae2 ae3 ae4
-      apply (auto simp: zero_less_mult_iff zero_less_divide_iff field_simps
-        space_pair_measure less_le split: prod.split)
-      by (smt (verit, best) AE_I2 fst_conv log_divide mult_eq_0_iff mult_minus_right snd_conv)
+    by (auto simp: field_simps log_divide)
   finally show ?nonneg
     by simp
 qed
@@ -1214,10 +1198,7 @@
   ultimately have I1: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z))))"
     apply (rule integrable_cong_AE_imp)
     using ae1 ae4 Px_nn Pyz_nn Pxyz_nn 
-    apply (auto simp: log_divide log_mult field_simps zero_less_mult_iff space_pair_measure less_le
-         split: prod.split)
-    apply (intro AE_I2)
-    by (smt (verit, best) distrib_left divide_eq_0_iff fst_conv log_mult mult.commute nonzero_mult_div_cancel_left snd_conv times_divide_eq_right)
+    by (auto simp: log_divide log_mult field_simps)
   have "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)
     (\<lambda>x. Pxyz x * log b (Pxz (fst x, snd (snd x))) - Pxyz x * log b (Px (fst x)) - Pxyz x * log b (Pz (snd (snd x))))"
     using finite_entropy_integrable_transform[OF Fxz Pxyz Pxyz_nn, of "\<lambda>x. (fst x, snd (snd x))"]
@@ -1230,42 +1211,8 @@
   ultimately have I2: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z)))"
     apply (rule integrable_cong_AE_imp)
     using ae1 ae2 ae3 ae4  Px_nn Pz_nn Pxz_nn Pyz_nn Pxyz_nn
-    apply(auto simp:   field_simps zero_less_mult_iff less_le space_pair_measure split: prod.split)
-    apply (intro AE_I2)
-    apply clarify
-  proof -
-    fix a :: 'c and aa :: 'd and ba :: 'e and x1 :: 'c and ab :: 'd and baa :: 'e
-    assume a1: "Pxz (fst (x1, ab, baa), snd (snd (x1, ab, baa))) = 0 \<longrightarrow> Pxyz (x1, ab, baa) = 0"
-    assume a2: "Pz (snd (snd (x1, ab, baa))) = 0 \<longrightarrow> Pxyz (x1, ab, baa) = 0"
-    assume a3: "Px (fst (x1, ab, baa)) = 0 \<longrightarrow> Pxyz (x1, ab, baa) = 0"
-    have f4: "\<forall>r ra rb. (ra::real) * (rb + r) = rb * ra + ra * r"
-      by (simp add: vector_space_over_itself.scale_right_distrib)
-    have f5: "0 \<noteq> Px x1 \<or> 0 = Pxyz (x1, ab, baa)"
-      using a3 by auto
-    have f6: "0 \<noteq> Pz baa \<or> 0 = Pxyz (x1, ab, baa)"
-      using a2 by force
-    have f7: "\<forall>r. (0::real) = 0 * r"
-      by simp
-    have "0 = Px x1 * Pz baa \<longrightarrow> Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1) + log b (Pz baa) + log b (Pxz (x1, baa) / (Px x1 * Pz baa)))"
-      using f6 f5 by simp
-    moreover
-    { assume "0 \<noteq> Px x1 * Pz baa"
-      moreover
-      { assume "0 \<noteq> Px x1 * Pz baa \<and> 0 \<noteq> Pxyz (x1, ab, baa)"
-        then have "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1 * Pz baa) + log b (Pxz (x1, baa) / (Px x1 * Pz baa))) \<and> 0 \<noteq> Pxz (x1, baa) / (Px x1 * Pz baa)"
-          using a1 by (metis (no_types) divide_eq_0_iff fst_eqD log_mult_nz mult.commute nonzero_eq_divide_eq snd_eqD)
-        moreover
-        { assume "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1) + (log b 0 + log b 0)) \<and> 0 \<noteq> Pxz (x1, baa) / (Px x1 * Pz baa) \<and> Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = log b (Px x1) * Pxyz (x1, ab, baa) + Pxyz (x1, ab, baa) * log b (Pz baa * (Pxz (x1, baa) / (Px x1 * Pz baa)))"
-          then have "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = log b (Px x1) * Pxyz (x1, ab, baa) + (log b (Pz baa) * Pxyz (x1, ab, baa) + Pxyz (x1, ab, baa) * log b (Pxz (x1, baa) / (Px x1 * Pz baa)))"
-            using f7 f4 by (metis (no_types) divide_eq_0_iff log_mult_nz mult.commute) }
-        ultimately have "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1) + log b (Pz baa) + log b (Pxz (x1, baa) / (Px x1 * Pz baa))) \<or> Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = log b (Px x1) * Pxyz (x1, ab, baa) + (log b (Pz baa) * Pxyz (x1, ab, baa) + Pxyz (x1, ab, baa) * log b (Pxz (x1, baa) / (Px x1 * Pz baa)))"
-          using f4 by (simp add: log_mult_nz) }
-      ultimately have "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1) + log b (Pz baa) + log b (Pxz (x1, baa) / (Px x1 * Pz baa))) \<or> Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1) + log b (Pz baa)) + Pxyz (x1, ab, baa) * log b (Pxz (x1, baa) / (Px x1 * Pz baa)) \<or> Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = log b (Px x1) * Pxyz (x1, ab, baa) + (log b (Pz baa) * Pxyz (x1, ab, baa) + Pxyz (x1, ab, baa) * log b (Pxz (x1, baa) / (Px x1 * Pz baa)))"
-        using f7 by (metis (no_types)) }
-    ultimately show "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = log b (Px x1) * Pxyz (x1, ab, baa) + (log b (Pz baa) * Pxyz (x1, ab, baa) + Pxyz (x1, ab, baa) * log b (Pxz (x1, baa) / (Px x1 * Pz baa)))"
-      by argo
-  qed
-
+    apply(auto simp:  field_simps log_divide log_mult)
+    done
   from ae I1 I2 show ?eq
     unfolding conditional_mutual_information_def mi_eq
     apply (subst mutual_information_distr[OF S TP Px Px_nn Pyz Pyz_nn Pxyz Pxyz_nn]; simp add: space_pair_measure)
@@ -1372,14 +1319,8 @@
     have "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>x. Pxyz x * - log b (?f x))"
       apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
       using Pz_nn Pxz_nn Pyz_nn Pxyz_nn ae2 ae3 ae4 
-      apply (auto simp: log_divide_nz log_mult_nz zero_le_mult_iff zero_less_mult_iff
-          zero_less_divide_iff field_simps space_pair_measure less_le split: prod.split)
-    apply (intro AE_I2)
-      apply (auto simp: )
-      by (smt (verit, best) log_divide minus_mult_minus mult_minus_left no_zero_divisors)
-
-    then
-    show "integrable ?P (\<lambda>x. - log b (?f x))"
+      by (auto simp: log_divide field_simps)
+    then show "integrable ?P (\<lambda>x. - log b (?f x))"
       using Pxyz_nn by (auto simp: integrable_real_density)
   qed (auto simp: b_gt_1 minus_log_convex)
   also have "\<dots> = conditional_mutual_information b S T P X Y Z"
@@ -1391,10 +1332,7 @@
     apply simp
     apply (intro integral_cong_AE)
     using ae1 ae2 ae3 ae4 
-    apply (auto simp: log_divide_pos zero_less_mult_iff zero_less_divide_iff
-                      field_simps space_pair_measure less_le integral_cong_AE split: prod.split)
-    apply (intro AE_I2)
-    by (metis divide_divide_eq_right log_recip mult_1 mult_minus_right)
+    by (auto simp: log_divide zero_less_mult_iff field_simps)
   finally show ?nonneg
     by simp
 qed

--- a/src/HOL/Transcendental.thy	Sun Jul 07 22:25:34 2024 +0100
+++ b/src/HOL/Transcendental.thy	Mon Jul 08 22:27:50 2024 +0100
@@ -1626,7 +1626,7 @@
 lemma raw_ln_mult: "x>0 \<Longrightarrow> y>0 \<Longrightarrow> raw_ln_real (x * y) = raw_ln_real x + raw_ln_real y"
   by (metis exp_add exp_ln raw_ln_exp)
 
-lemma ln_mult: "(x\<noteq>0 \<longleftrightarrow> y\<noteq>0) \<Longrightarrow> ln (x * y) = ln x + ln y"
+lemma ln_mult: "ln (x * y) = (if x\<noteq>0 \<and> y\<noteq>0 then ln x + ln y else 0)"
   for x :: real
   by (simp add: ln_real_def abs_mult raw_ln_mult)
 
@@ -1642,7 +1642,7 @@
   for x :: real
   by (smt (verit) inverse_nonzero_iff_nonzero ln_mult ln_one ln_real_def right_inverse)
 
-lemma ln_div: "(x\<noteq>0 \<longleftrightarrow> y\<noteq>0) \<Longrightarrow> ln (x/y) = ln x - ln y"
+lemma ln_div: "ln (x/y) = (if x\<noteq>0 \<and> y\<noteq>0 then ln x - ln y else 0)"
   for x :: real
   by (simp add: divide_inverse ln_inverse ln_mult)
 
@@ -2121,7 +2121,7 @@
 
 corollary ln_diff_le: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x - ln y \<le> (x - y) / y"
   for x :: real
-  by (simp add: ln_div [symmetric] diff_divide_distrib ln_le_minus_one)
+by (metis diff_divide_distrib divide_pos_pos divide_self ln_divide_pos ln_le_minus_one order_less_irrefl)
 
 lemma ln_eq_minus_one:
   fixes x :: real
@@ -2510,7 +2510,7 @@
   by auto
 
 lemma log_mult:
-  "(x\<noteq>0 \<longleftrightarrow> y\<noteq>0) \<Longrightarrow> log a (x * y) = log a x + log a y"
+  "log a (x * y) = (if x\<noteq>0 \<and> y\<noteq>0 then log a x + log a y else 0)"
   by (simp add: log_def ln_mult divide_inverse distrib_right)
 
 lemma log_mult_pos:
@@ -2541,7 +2541,7 @@
   by (simp add: divide_inverse log_inverse)
 
 lemma log_divide:
-  "(x\<noteq>0 \<longleftrightarrow> y\<noteq>0) \<Longrightarrow> log a (x / y) = log a x - log a y"
+  "log a (x / y) = (if x\<noteq>0 \<and> y\<noteq>0 then log a x - log a y else 0)"
   by (simp add: diff_divide_distrib ln_div log_def)
 
 lemma log_divide_pos:
@@ -2839,7 +2839,7 @@
   by (metis ln_powr mult_1 powr_inverse_root powr_one' times_divide_eq_left)
 
 lemma ln_sqrt: "0 \<le> x \<Longrightarrow> ln (sqrt x) = ln x / 2"
-  by (smt (verit) field_sum_of_halves ln_mult real_sqrt_mult_self)
+  by (metis (full_types) divide_inverse inverse_eq_divide ln_powr mult.commute of_nat_numeral pos2 root_powr_inverse sqrt_def)
 
 lemma log_root: "n > 0 \<Longrightarrow> a \<ge> 0 \<Longrightarrow> log b (root n a) =  log b a / n"
   by (simp add: log_def ln_root)