src/HOL/Probability/Information.thy

 
 theory Information
 imports
   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 +
   fixes b :: real assumes b_gt_1: "1 < b"

   ultimately have int: "integrable (S \<Otimes>\<^sub>M T) f"
   proof (rule integrable_cong_AE_imp)
     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
   proof (intro ST.KL_density_density_nonneg)
     show "prob_space (density (S \<Otimes>\<^sub>M T) (\<lambda>x. ennreal (Pxy x))) "

       unfolding real_integrable_def
       using fin neg by (auto simp: split_beta')
     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) 
   qed (auto simp: b_gt_1 minus_log_convex)
   also have "\<dots> = conditional_mutual_information b S T P X Y Z"

        apply simp
       apply (force simp: space_pair_measure) 
      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
 
 lemma (in information_space)

   moreover have "(\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z)))) \<in> borel_measurable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)"
     using Pxyz Px Pyz by simp
   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))"]
     using finite_entropy_integrable_transform[OF Fx Pxyz Pxyz_nn, of fst]
     using finite_entropy_integrable_transform[OF Fz Pxyz Pxyz_nn, of "snd \<circ> snd"]

     using Pxyz Px Pz
     by auto
   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)
     apply (subst Bochner_Integration.integral_diff[symmetric])
       apply (auto intro!: integral_cong_AE simp: split_beta' simp del: Bochner_Integration.integral_diff)

       unfolding real_integrable_def
       using fin neg by (auto simp: split_beta')
     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"
     unfolding \<open>?eq\<close>
     using Pz_nn Pxz_nn Pyz_nn Pxyz_nn

     apply simp
     apply simp
     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
 
 lemma (in information_space) conditional_mutual_information_eq: