# HG changeset patch
# User wenzelm
# Date 1729113182 -7200
# Node ID cf2c039671789508f4e00fe01efba8f4e7ba40db
# Parent  8e7bd056675995282f51427f52b820981cded778
tuned proofs;

diff -r 8e7bd0566759 -r cf2c03967178 src/HOL/Probability/ex/Dining_Cryptographers.thy
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Wed Oct 16 22:07:04 2024 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Wed Oct 16 23:13:02 2024 +0200
@@ -124,32 +124,31 @@
   hence "length ys = n" by (simp add: dc_crypto)
   have [simp]: "length xs = n" using xs_inv[symmetric] by (simp add: inversion_def)
 
-  { fix b
-    have "inj_on (\<lambda>x. inversion (Some i, x)) {ys. ys ! 0 = b \<and> length ys = length xs}"
-    proof (rule inj_onI)
-      fix x y
-      assume "x \<in> {ys. ys ! 0 = b \<and> length ys = length xs}"
-        and "y \<in> {ys. ys ! 0 = b \<and> length ys = length xs}"
-        and inv: "inversion (Some i, x) = inversion (Some i, y)"
-      hence [simp]: "x ! 0 = y ! 0" "length y = n" "length x = n"
-        using \<open>length xs = n\<close> by simp_all
-      have *: "\<And>j. j < n \<Longrightarrow>
-        (x ! j = x ! (Suc j mod n)) = (y ! j = y ! (Suc j mod n))"
-        using inv unfolding inversion_def map_eq_conv payer_def coin_def
-        by fastforce
-      show "x = y"
-      proof (rule nth_equalityI, simp)
-        fix j assume "j < length x" hence "j < n" using \<open>length xs = n\<close> by simp
-        thus "x ! j = y ! j"
-        proof (induct j)
-          case (Suc j)
-          hence "j < n" by simp
-          with Suc show ?case using *[OF \<open>j < n\<close>]
-            by (cases "y ! j") simp_all
-        qed simp
-      qed
-    qed }
-  note inj_inv = this
+  have inj_inv: "inj_on (\<lambda>x. inversion (Some i, x)) {ys. ys ! 0 = b \<and> length ys = length xs}"
+    for b
+  proof (rule inj_onI)
+    fix x y
+    assume "x \<in> {ys. ys ! 0 = b \<and> length ys = length xs}"
+      and "y \<in> {ys. ys ! 0 = b \<and> length ys = length xs}"
+      and inv: "inversion (Some i, x) = inversion (Some i, y)"
+    hence [simp]: "x ! 0 = y ! 0" "length y = n" "length x = n"
+      using \<open>length xs = n\<close> by simp_all
+    have *: "\<And>j. j < n \<Longrightarrow>
+      (x ! j = x ! (Suc j mod n)) = (y ! j = y ! (Suc j mod n))"
+      using inv unfolding inversion_def map_eq_conv payer_def coin_def
+      by fastforce
+    show "x = y"
+    proof (rule nth_equalityI, simp)
+      fix j assume "j < length x" hence "j < n" using \<open>length xs = n\<close> by simp
+      thus "x ! j = y ! j"
+      proof (induct j)
+        case (Suc j)
+        hence "j < n" by simp
+        with Suc show ?case using *[OF \<open>j < n\<close>]
+          by (cases "y ! j") simp_all
+      qed simp
+    qed
+  qed
 
   txt \<open>
     We now construct the possible inversions for \<^term>\<open>xs\<close> when the payer is
@@ -162,16 +161,20 @@
 
   have "\<And>l. l < max i j \<Longrightarrow> Suc l mod n = Suc l"
     using \<open>i < n\<close> \<open>j < n\<close> by auto
-  { fix l assume "l < n"
-    hence "(((l < min i j \<or> l = min i j) \<or> (min i j < l \<and> l < max i j)) \<or> l = max i j) \<or> max i j < l" by auto
-    hence "((i = l) = (zs ! l = zs ! (Suc l mod n))) = ((j = l) = (ys ! l = ys ! (Suc l mod n)))"
-    apply - proof ((erule disjE)+)
-      assume "l < min i j"
+  have "((i = l) = (zs ! l = zs ! (Suc l mod n))) = ((j = l) = (ys ! l = ys ! (Suc l mod n)))"
+    if "l < n" for l
+  proof -
+    from that consider "l < min i j" | "l = min i j" | "min i j < l" "l < max i j"
+      | "l = max i j" | "max i j < l"
+      by linarith
+    thus ?thesis
+    proof cases
+      case 1
       hence "l \<noteq> i" and "l \<noteq> j" and "zs ! l = ys ! l" and
         "zs ! (Suc l mod n) = ys ! (Suc l mod n)" using \<open>i < n\<close> \<open>j < n\<close> unfolding zs_def by auto
       thus ?thesis by simp
     next
-      assume "l = min i j"
+      case 2
       show ?thesis
       proof (cases rule: linorder_cases)
         assume "i < j"
@@ -192,13 +195,13 @@
         thus ?thesis by simp
       qed
     next
-      assume "min i j < l \<and> l < max i j"
+      case 3
       hence "i \<noteq> l" and "j \<noteq> l" and "zs ! l = (\<not> ys ! l)"
         "zs ! (Suc l mod n) = (\<not> ys ! (Suc l mod n))"
         using \<open>i < n\<close> \<open>j < n\<close> by (auto simp: zs_def)
       thus ?thesis by simp
     next
-      assume "l = max i j"
+      case 4
       show ?thesis
       proof (cases rule: linorder_cases)
         assume "i < j"
@@ -223,14 +226,15 @@
         thus ?thesis by simp
       qed
     next
-      assume "max i j < l"
+      case 5
       hence "j \<noteq> l" and "i \<noteq> l" by simp_all
       have "zs ! (Suc l mod n) = ys ! (Suc l mod n)"
         using \<open>l < n\<close> \<open>max i j < l\<close> by (cases "Suc l = n") (auto simp add: zs_def)
       moreover have "zs ! l = ys ! l"
         using \<open>l < n\<close> \<open>max i j < l\<close> by (auto simp add: zs_def)
       ultimately show ?thesis using \<open>j \<noteq> l\<close> \<open>i \<noteq> l\<close> by auto
-    qed }
+    qed
+  qed
   hence zs: "inversion (Some i, zs) = xs"
     by (simp add: xs_inv[symmetric] inversion_def coin_def payer_def)
   moreover
@@ -297,15 +301,12 @@
   have card_double: "2 * card ?sets = card (\<Union>?sets)"
   proof (rule card_partition)
     show "finite ?sets" by simp
-    { fix i assume "i < n"
-      have "?set i \<subseteq> dc_crypto" by auto
-      have "finite (?set i)" using finite_dc_crypto by auto }
+    have "finite (?set i)" for i
+      using finite_dc_crypto by auto
     thus "finite (\<Union>?sets)" by auto
-
   next
     fix c assume "c \<in> ?sets"
     thus "card c = 2" using card_payer_and_inversion[OF assms] by auto
-
   next
     fix x y assume "x \<in> ?sets" and "y \<in> ?sets" "x \<noteq> y"
     then obtain i j where xy: "x = ?set i" "y = ?set j" by auto
@@ -315,17 +316,20 @@
 
   have sets: "?sets = ?set ` {..< n}"
     unfolding image_def by auto
-  { fix i j :: nat assume asm: "i \<noteq> j" "i < n" "j < n"
-    { assume iasm: "?set i = {}"
+  have "?set i \<noteq> ?set j" if asm: "i \<noteq> j" "i < n" "j < n" for i j
+  proof -
+    have False if iasm: "?set i = {}"
+    proof -
       have "card (?set i) = 2"
         using card_payer_and_inversion[OF assms \<open>i < n\<close>] by auto
-      hence "False"
-        using iasm by auto }
+      thus ?thesis using iasm by auto
+    qed
     then obtain c where ci: "c \<in> ?set i" by blast
     hence cj: "c \<notin> ?set j" using asm by auto
-    { assume "?set i = ?set j"
-      hence "False" using ci cj by auto }
-    hence "?set i \<noteq> ?set j" by auto }
+    have False if "?set i = ?set j"
+      using that ci cj by auto
+    thus ?thesis by auto
+  qed
   hence "inj_on ?set {..< n}" unfolding inj_on_def by auto
   from card_image[OF this]
   have "card (?set ` {..< n}) = n" by auto
@@ -345,16 +349,13 @@
   let ?P = "{inversion -` {x} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto}"
   have "\<Union>?P = dc_crypto" by auto
 
-  { fix a b assume *: "(a, b) \<in> dc_crypto"
-    have inv_SOME: "inversion (SOME x. inversion x = inversion (a, b) \<and> x \<in> dc_crypto) = inversion (a, b)"
-      apply (rule someI2)
-      by (auto simp: *) }
-  note inv_SOME = this
+  have inv_SOME: "inversion (SOME x. inversion x = inversion (a, b) \<and> x \<in> dc_crypto) = inversion (a, b)"
+    if "(a, b) \<in> dc_crypto" for a b
+    by (rule someI2) (auto simp: that)
 
-  { fix a b assume *: "(a, b) \<in> dc_crypto"
-    have "(SOME x. inversion x = inversion (a, b) \<and> x \<in> dc_crypto) \<in> dc_crypto"
-      by (rule someI2) (auto simp: *) }
-  note SOME_inv_dc = this
+  have SOME_inv_dc: "(SOME x. inversion x = inversion (a, b) \<and> x \<in> dc_crypto) \<in> dc_crypto"
+    if "(a, b) \<in> dc_crypto" for a b
+    by (rule someI2) (auto simp: that)
 
   have "bij_betw (\<lambda>s. inversion (SOME x. x \<in> s \<and> x \<in> dc_crypto))
     {inversion -` {x} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto}
@@ -373,13 +374,11 @@
     have "?P = (\<lambda>x. inversion -` {x} \<inter> dc_crypto) ` (inversion ` dc_crypto)"
       by auto
     thus "finite ?P" using finite_dc_crypto by auto
-
   next
     fix c assume "c \<in> {inversion -` {x} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto}"
     then obtain x where "c = inversion -` {x} \<inter> dc_crypto" and x: "x \<in> inversion ` dc_crypto" by auto
     hence "c = {dc \<in> dc_crypto. inversion dc = x}" by auto
     thus "card c = 2 * n" using card_inversion[OF x] by simp
-
   next
     fix x y assume "x \<in> ?P" "y \<in> ?P" and "x \<noteq> y"
     then obtain i j where
diff -r 8e7bd0566759 -r cf2c03967178 src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Wed Oct 16 22:07:04 2024 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Wed Oct 16 23:13:02 2024 +0200
@@ -69,12 +69,12 @@
     with \<open>f \<noteq> g\<close> eq show False unfolding fun_upd_eq_iff[of _ _ b _ _ d]
       by (auto simp: fun_upd_idem fun_upd_eq_iff)
   next
-    { fix f assume "f \<in> extensionalD d A \<inter> (A \<rightarrow> B)"
-      have "card (fun_upd f a ` B) = card B"
-      proof (auto intro!: card_image inj_onI)
-        fix b b' assume "f(a := b) = f(a := b')"
-        from fun_upd_eq_iff[THEN iffD1, OF this] show "b = b'" by simp
-      qed }
+    have "card (fun_upd f a ` B) = card B"
+      if "f \<in> extensionalD d A \<inter> (A \<rightarrow> B)" for f
+    proof (auto intro!: card_image inj_onI)
+      fix b b' assume "f(a := b) = f(a := b')"
+      from fun_upd_eq_iff[THEN iffD1, OF this] show "b = b'" by simp
+    qed
     then show "(\<Sum>i\<in>extensionalD d A \<inter> (A \<rightarrow> B). card (fun_upd i a ` B)) = card B * card B ^ card A"
       using insert by simp
   qed
@@ -170,9 +170,9 @@
   qed
   then show "sum P msgs = 1"
     unfolding msgs_def P_def by simp
-  fix x
-  have "\<And> A f. 0 \<le> (\<Prod>x\<in>A. M (f x))" by (auto simp: prod_nonneg)
-  then show "0 \<le> P x"
+  have "0 \<le> (\<Prod>x\<in>A. M (f x))" for A f
+    by (auto simp: prod_nonneg)
+  then show "0 \<le> P x" for x
     unfolding P_def by (auto split: prod.split simp: zero_le_mult_iff)
 qed auto
 
@@ -333,40 +333,45 @@
 proof -
   txt \<open>Lemma 2\<close>
 
-  { fix k obs obs'
-    assume "k \<in> keys" "K k \<noteq> 0" and obs': "obs' \<in> OB ` msgs" and obs: "obs \<in> OB ` msgs"
-    assume "t obs = t obs'"
-    from t_eq_imp_bij_func[OF this]
+  have t_eq_imp: "(\<P>(OB ; fst) {(obs, k)}) = (\<P>(OB ; fst) {(obs', k)})"
+    if "k \<in> keys" "K k \<noteq> 0" and obs': "obs' \<in> OB ` msgs" and obs: "obs \<in> OB ` msgs"
+      and eq: "t obs = t obs'"
+    for k obs obs'
+  proof -
+    from t_eq_imp_bij_func[OF eq]
     obtain t_f where "bij_betw t_f {..<n} {..<n}" and
       obs_t_f: "\<And>i. i<n \<Longrightarrow> obs!i = obs' ! t_f i"
       using obs obs' unfolding OB_def msgs_def by auto
     then have t_f: "inj_on t_f {..<n}" "{..<n} = t_f`{..<n}" unfolding bij_betw_def by auto
 
-    { fix obs assume "obs \<in> OB`msgs"
-      then have **: "\<And>ms. length ms = n \<Longrightarrow> OB (k, ms) = obs \<longleftrightarrow> (\<forall>i<n. observe k (ms!i) = obs ! i)"
+    have *: "(\<P>(OB ; fst) {(obs, k)}) / K k =
+            (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)"
+      if "obs \<in> OB`msgs" for obs
+    proof -
+      from that have **: "length ms = n \<Longrightarrow> OB (k, ms) = obs \<longleftrightarrow> (\<forall>i<n. observe k (ms!i) = obs ! i)"
+        for ms
         unfolding OB_def msgs_def by (simp add: image_iff list_eq_iff_nth_eq)
-
       have "(\<P>(OB ; fst) {(obs, k)}) / K k =
           p ({k}\<times>{ms. (k,ms) \<in> msgs \<and> OB (k,ms) = obs}) / K k"
-        apply (simp add: \<mu>'_eq) by (auto intro!: arg_cong[where f=p])
-      also have "\<dots> =
-          (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)"
+        by (simp add: \<mu>'_eq) (auto intro!: arg_cong[where f=p])
+      also have "\<dots> = (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)"
         unfolding P_def using \<open>K k \<noteq> 0\<close> \<open>k \<in> keys\<close>
         apply (simp add: sum.cartesian_product' sum_divide_distrib msgs_def ** cong: conj_cong)
         apply (subst prod_sum_distrib_lists[OF M.finite_space]) ..
-      finally have "(\<P>(OB ; fst) {(obs, k)}) / K k =
-            (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)" . }
-    note * = this
+      finally show ?thesis .
+    qed
 
     have "(\<P>(OB ; fst) {(obs, k)}) / K k = (\<P>(OB ; fst) {(obs', k)}) / K k"
       unfolding *[OF obs] *[OF obs']
       using t_f(1) obs_t_f by (subst (2) t_f(2)) (simp add: prod.reindex)
-    then have "(\<P>(OB ; fst) {(obs, k)}) = (\<P>(OB ; fst) {(obs', k)})"
-      using \<open>K k \<noteq> 0\<close> by auto }
-  note t_eq_imp = this
+    then show ?thesis using \<open>K k \<noteq> 0\<close> by auto
+  qed
 
   let ?S = "\<lambda>obs. t -`{t obs} \<inter> OB`msgs"
-  { fix k obs assume "k \<in> keys" "K k \<noteq> 0" and obs: "obs \<in> OB`msgs"
+  have P_t_eq_P_OB: "\<P>(t\<circ>OB ; fst) {(t obs, k)} = real (card (?S obs)) * \<P>(OB ; fst) {(obs, k)}"
+    if "k \<in> keys" "K k \<noteq> 0" and obs: "obs \<in> OB`msgs"
+    for k obs
+  proof -
     have *: "((\<lambda>x. (t (OB x), fst x)) -` {(t obs, k)} \<inter> msgs) =
       (\<Union>obs'\<in>?S obs. ((\<lambda>x. (OB x, fst x)) -` {(obs', k)} \<inter> msgs))" by auto
     have df: "disjoint_family_on (\<lambda>obs'. (\<lambda>x. (OB x, fst x)) -` {(obs', k)} \<inter> msgs) (?S obs)"
@@ -377,17 +382,18 @@
       by (auto simp add: * intro!: sum_nonneg)
     also have "(\<Sum>obs'\<in>?S obs. \<P>(OB ; fst) {(obs', k)}) = real (card (?S obs)) * \<P>(OB ; fst) {(obs, k)}"
       by (simp add: t_eq_imp[OF \<open>k \<in> keys\<close> \<open>K k \<noteq> 0\<close> obs])
-    finally have "\<P>(t\<circ>OB ; fst) {(t obs, k)} = real (card (?S obs)) * \<P>(OB ; fst) {(obs, k)}" .}
-  note P_t_eq_P_OB = this
+    finally show ?thesis .
+  qed
 
-  { fix k obs assume "k \<in> keys" and obs: "obs \<in> OB`msgs"
-    have "\<P>(t\<circ>OB | fst) {(t obs, k)} =
-      real (card (t -` {t obs} \<inter> OB ` msgs)) * \<P>(OB | fst) {(obs, k)}"
-      using \<P>_k[OF \<open>k \<in> keys\<close>] P_t_eq_P_OB[OF \<open>k \<in> keys\<close> _ obs] by auto }
-  note CP_t_K = this
+  have CP_t_K: "\<P>(t\<circ>OB | fst) {(t obs, k)} =
+    real (card (t -` {t obs} \<inter> OB ` msgs)) * \<P>(OB | fst) {(obs, k)}"
+    if k: "k \<in> keys" and obs: "obs \<in> OB`msgs" for k obs
+    using \<P>_k[OF k] P_t_eq_P_OB[OF k _ obs] by auto
 
-  { fix k obs assume "k \<in> keys" and obs: "obs \<in> OB`msgs"
-    then have "t -`{t obs} \<inter> OB`msgs \<noteq> {}" (is "?S \<noteq> {}") by auto
+  have CP_T_eq_CP_O: "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(fst | OB) {(k, obs)}"
+    if "k \<in> keys" and obs: "obs \<in> OB`msgs" for k obs
+  proof -
+    from that have "t -`{t obs} \<inter> OB`msgs \<noteq> {}" (is "?S \<noteq> {}") by auto
     then have "real (card ?S) \<noteq> 0" by auto
 
     have "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(t\<circ>OB | fst) {(t obs, k)} * \<P>(fst) {k} / \<P>(t\<circ>OB) {t obs}"
@@ -411,31 +417,33 @@
       by (auto intro!: sum.cong simp: prob_conj_imp1 vimage_def)
     also have "\<P>(OB | fst) {(obs, k)} * \<P>(fst) {k} / \<P>(OB) {obs} = \<P>(fst | OB) {(k, obs)}"
       by (auto simp: vimage_def conj_commute prob_conj_imp2)
-    finally have "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(fst | OB) {(k, obs)}" . }
-  note CP_T_eq_CP_O = this
+    finally show ?thesis .
+  qed
 
   let ?H = "\<lambda>obs. (\<Sum>k\<in>keys. \<P>(fst|OB) {(k, obs)} * log b (\<P>(fst|OB) {(k, obs)})) :: real"
   let ?Ht = "\<lambda>obs. (\<Sum>k\<in>keys. \<P>(fst|t\<circ>OB) {(k, obs)} * log b (\<P>(fst|t\<circ>OB) {(k, obs)})) :: real"
 
-  { fix obs assume obs: "obs \<in> OB`msgs"
+  have *: "?H obs = ?Ht (t obs)" if obs: "obs \<in> OB`msgs" for obs
+  proof -
     have "?H obs = (\<Sum>k\<in>keys. \<P>(fst|t\<circ>OB) {(k, t obs)} * log b (\<P>(fst|t\<circ>OB) {(k, t obs)}))"
       using CP_T_eq_CP_O[OF _ obs]
       by simp
-    then have "?H obs = ?Ht (t obs)" . }
-  note * = this
+    then show ?thesis .
+  qed
 
   have **: "\<And>x f A. (\<Sum>y\<in>t-`{x}\<inter>A. f y (t y)) = (\<Sum>y\<in>t-`{x}\<inter>A. f y x)" by auto
 
-  { fix x
+  have P_t_sum_P_O: "\<P>(t\<circ>OB) {t (OB x)} = (\<Sum>obs\<in>?S (OB x). \<P>(OB) {obs})" for x
+  proof -
     have *: "(\<lambda>x. t (OB x)) -` {t (OB x)} \<inter> msgs =
       (\<Union>obs\<in>?S (OB x). OB -` {obs} \<inter> msgs)" by auto
     have df: "disjoint_family_on (\<lambda>obs. OB -` {obs} \<inter> msgs) (?S (OB x))"
       unfolding disjoint_family_on_def by auto
-    have "\<P>(t\<circ>OB) {t (OB x)} = (\<Sum>obs\<in>?S (OB x). \<P>(OB) {obs})"
+    show ?thesis
       unfolding comp_def
       using finite_measure_finite_Union[OF _ _ df]
-      by (force simp add: * intro!: sum_nonneg) }
-  note P_t_sum_P_O = this
+      by (force simp add: * intro!: sum_nonneg)
+  qed
 
   txt \<open>Lemma 3\<close>
   have "\<H>(fst | OB) = -(\<Sum>obs\<in>OB`msgs. \<P>(OB) {obs} * ?Ht (t obs))"
diff -r 8e7bd0566759 -r cf2c03967178 src/HOL/Probability/ex/Measure_Not_CCC.thy
--- a/src/HOL/Probability/ex/Measure_Not_CCC.thy	Wed Oct 16 22:07:04 2024 +0200
+++ b/src/HOL/Probability/ex/Measure_Not_CCC.thy	Wed Oct 16 23:13:02 2024 +0200
@@ -44,28 +44,30 @@
   proof induction
     case (Union F)
     moreover
-    { fix i assume "countable (UNIV - F i)"
-      then have "countable (UNIV - (\<Union>i. F i))"
-        by (rule countable_subset[rotated]) auto }
+    have "countable (UNIV - (\<Union>i. F i))" if "countable (UNIV - F i)" for i
+      using that by (rule countable_subset[rotated]) auto
     ultimately show "countable (\<Union>i. F i) \<or> countable (UNIV - (\<Union>i. F i))"
       by blast
   qed (auto simp: Diff_Diff_Int)
 next
   assume "countable A \<or> countable (UNIV - A)"
   moreover
-  { fix A :: "real set" assume A: "countable A"
+  have A: "A \<in> COCOUNT" if "countable A" for A :: "real set"
+  proof -
     have "A = (\<Union>a\<in>A. {a})"
       by auto
     also have "\<dots> \<in> COCOUNT"
-      by (intro sets.countable_UN' A) (auto simp: COCOUNT_def) 
-    finally have "A \<in> COCOUNT" . }
-  note A = this
+      by (intro sets.countable_UN' that) (auto simp: COCOUNT_def) 
+    finally show ?thesis .
+  qed
   note A[of A]
   moreover
-  { assume "countable (UNIV - A)"
-    with A have "space COCOUNT - (UNIV - A) \<in> COCOUNT" by simp
-    then have "A \<in> COCOUNT"
-      by (auto simp: COCOUNT_def Diff_Diff_Int) }
+  have "A \<in> COCOUNT" if "countable (UNIV - A)"
+  proof -
+    from A that have "space COCOUNT - (UNIV - A) \<in> COCOUNT" by simp
+    then show ?thesis
+      by (auto simp: COCOUNT_def Diff_Diff_Int)
+  qed
   ultimately show "A \<in> COCOUNT" 
     by blast
 qed
@@ -121,12 +123,14 @@
 
 lemma space_EXP: "space EXP = measurable COCOUNT BOOL"
 proof -
-  { fix f 
+  have "f \<in> space EXP \<longleftrightarrow> f \<in> measurable COCOUNT BOOL" for f
+  proof -
     have "f \<in> space EXP \<longleftrightarrow> (\<lambda>(a, b). f b) \<in> measurable (POW \<Otimes>\<^sub>M COCOUNT) BOOL"
       using eq[of "\<lambda>x. f"] by (simp add: measurable_const_iff)
     also have "\<dots> \<longleftrightarrow> f \<in> measurable COCOUNT BOOL"
       by auto
-    finally have "f \<in> space EXP \<longleftrightarrow> f \<in> measurable COCOUNT BOOL" . }
+    finally show ?thesis .
+  qed
   then show ?thesis by auto
 qed