author wenzelm Tue, 28 Feb 2012 21:53:36 +0100 changeset 46731 5302e932d1e5 parent 46730 e3b99d0231bc child 46735 c8ec1958f822
avoid undeclared variables in let bindings; tuned proofs;
```--- a/src/HOL/Probability/Binary_Product_Measure.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -170,7 +170,7 @@
assumes Q: "Q \<in> sets P"
shows "(\<lambda>(x,y). (y, x)) -` Q \<in> sets (M2 \<Otimes>\<^isub>M M1)" (is "_ \<in> sets ?Q")
proof -
-  let "?f Q" = "(\<lambda>(x,y). (y, x)) -` Q \<inter> space M2 \<times> space M1"
+  let ?f = "\<lambda>Q. (\<lambda>(x,y). (y, x)) -` Q \<inter> space M2 \<times> space M1"
have *: "(\<lambda>(x,y). (y, x)) -` Q = ?f Q"
using sets_into_space[OF Q] by (auto simp: space_pair_measure)
have "sets (M2 \<Otimes>\<^isub>M M1) = sets (sigma (pair_measure_generator M2 M1))"
@@ -325,7 +325,7 @@
have M1: "sigma_finite_measure M1" by default
from M2.disjoint_sigma_finite guess F .. note F = this
then have F_sets: "\<And>i. F i \<in> sets M2" by auto
-  let "?C x i" = "F i \<inter> Pair x -` Q"
+  let ?C = "\<lambda>x i. F i \<inter> Pair x -` Q"
{ fix i
let ?R = "M2.restricted_space (F i)"
have [simp]: "space M1 \<times> F i \<inter> space M1 \<times> space M2 = space M1 \<times> F i"
@@ -607,8 +607,8 @@
proof -
have f_borel: "f \<in> borel_measurable P"
using f(1) by (rule borel_measurable_simple_function)
-  let "?F z" = "f -` {z} \<inter> space P"
-  let "?F' x z" = "Pair x -` ?F z"
+  let ?F = "\<lambda>z. f -` {z} \<inter> space P"
+  let ?F' = "\<lambda>x z. Pair x -` ?F z"
{ fix x assume "x \<in> space M1"
have [simp]: "\<And>z y. indicator (?F z) (x, y) = indicator (?F' x z) y"
by (auto simp: indicator_def)
@@ -819,7 +819,7 @@
shows "M1.almost_everywhere (\<lambda>x. integrable M2 (\<lambda> y. f (x, y)))" (is "?AE")
and "(\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>L P f" (is "?INT")
proof -
-  let "?pf x" = "ereal (f x)" and "?nf x" = "ereal (- f x)"
+  let ?pf = "\<lambda>x. ereal (f x)" and ?nf = "\<lambda>x. ereal (- f x)"
have
borel: "?nf \<in> borel_measurable P""?pf \<in> borel_measurable P" and
int: "integral\<^isup>P P ?nf \<noteq> \<infinity>" "integral\<^isup>P P ?pf \<noteq> \<infinity>"```
```--- a/src/HOL/Probability/Borel_Space.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -521,7 +521,8 @@
finally show "{x. x\$\$i \<le> a} \<in> sets ?SIGMA"
apply (simp only:)
apply (safe intro!: countable_UN Diff)
-      by (auto simp: sets_sigma intro!: sigma_sets.Basic)
+      apply (auto simp: sets_sigma intro!: sigma_sets.Basic)
+      done
next
fix a i assume "\<not> i < DIM('a)"
then show "{x. x\$\$i \<le> a} \<in> sets ?SIGMA"
@@ -556,7 +557,8 @@
finally show "{x. a \<le> x\$\$i} \<in> sets ?SIGMA"
apply (simp only:)
apply (safe intro!: countable_UN Diff)
-      by (auto simp: sets_sigma intro!: sigma_sets.Basic)
+      apply (auto simp: sets_sigma intro!: sigma_sets.Basic)
+      done
next
fix a i assume "\<not> i < DIM('a)"
then show "{x. a \<le> x\$\$i} \<in> sets ?SIGMA"
@@ -653,7 +655,8 @@
have "M \<in> sets ?SIGMA"
apply (subst open_UNION[OF `open M`])
apply (safe intro!: countable_UN)
-        by (auto simp add: sigma_def intro!: sigma_sets.Basic) }
+        apply (auto simp add: sigma_def intro!: sigma_sets.Basic)
+        done }
then show ?thesis
unfolding borel_def by (intro sets_sigma_subset) auto
qed
@@ -1156,7 +1159,7 @@
assume *: "(\<lambda>x. real (f x)) \<in> borel_measurable M" "f -` {\<infinity>} \<inter> space M \<in> sets M" "f -` {-\<infinity>} \<inter> space M \<in> sets M"
have "f -` {\<infinity>} \<inter> space M = {x\<in>space M. f x = \<infinity>}" "f -` {-\<infinity>} \<inter> space M = {x\<in>space M. f x = -\<infinity>}" by auto
with * have **: "{x\<in>space M. f x = \<infinity>} \<in> sets M" "{x\<in>space M. f x = -\<infinity>} \<in> sets M" by simp_all
-  let "?f x" = "if f x = \<infinity> then \<infinity> else if f x = -\<infinity> then -\<infinity> else ereal (real (f x))"
+  let ?f = "\<lambda>x. if f x = \<infinity> then \<infinity> else if f x = -\<infinity> then -\<infinity> else ereal (real (f x))"
have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto
also have "?f = f" by (auto simp: fun_eq_iff ereal_real)
finally show "f \<in> borel_measurable M" .
@@ -1469,7 +1472,7 @@
shows "u' \<in> borel_measurable M"
proof -
have "\<And>x. x \<in> space M \<Longrightarrow> liminf (\<lambda>n. ereal (u n x)) = ereal (u' x)"
-    using u' by (simp add: lim_imp_Liminf trivial_limit_sequentially lim_ereal)
+    using u' by (simp add: lim_imp_Liminf)
moreover from u have "(\<lambda>x. liminf (\<lambda>n. ereal (u n x))) \<in> borel_measurable M"
by auto
ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff)```
```--- a/src/HOL/Probability/Caratheodory.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/Caratheodory.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -223,7 +223,7 @@
by (metis Diff_Un Un compl_sets lambda_system_sets xl yl)
moreover
have "x \<union> y = space M - ((space M - x) \<inter> (space M - y))"
-    by auto  (metis subsetD lambda_system_sets sets_into_space xl yl)+
+    by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+
ultimately show ?thesis
by (metis lambda_system_Compl lambda_system_Int xl yl)
qed
@@ -666,7 +666,7 @@
(\<lambda>x. Inf (measure_set M f x))"
fix A :: "nat \<Rightarrow> 'a set"
-  let "?outer B" = "Inf (measure_set M f B)"
+  let ?outer = "\<lambda>B. Inf (measure_set M f B)"
assume A: "range A \<subseteq> Pow (space M)"
and disj: "disjoint_family A"
and sb: "(\<Union>i. A i) \<subseteq> space M"```
```--- a/src/HOL/Probability/Complete_Measure.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/Complete_Measure.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -203,7 +203,7 @@
assumes f: "simple_function completion f"
shows "\<exists>f'. simple_function M f' \<and> (AE x. f x = f' x)"
proof -
-  let "?F x" = "f -` {x} \<inter> space M"
+  let ?F = "\<lambda>x. f -` {x} \<inter> space M"
have F: "\<And>x. ?F x \<in> sets completion" and fin: "finite (f`space M)"
using completion.simple_functionD[OF f]
completion.simple_functionD[OF f] by simp_all
@@ -211,7 +211,8 @@
using F null_part by auto
from choice[OF this] obtain N where
N: "\<And>x. null_part (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets" by auto
-  let ?N = "\<Union>x\<in>f`space M. N x" let "?f' x" = "if x \<in> ?N then undefined else f x"
+  let ?N = "\<Union>x\<in>f`space M. N x"
+  let ?f' = "\<lambda>x. if x \<in> ?N then undefined else f x"
have sets: "?N \<in> null_sets" using N fin by (intro nullsets.finite_UN) auto
show ?thesis unfolding simple_function_def
proof (safe intro!: exI[of _ ?f'])```
```--- a/src/HOL/Probability/Conditional_Probability.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/Conditional_Probability.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -25,8 +25,8 @@
interpret P: prob_space N
using prob_space_subalgebra[OF N] .

-  let "?f A" = "\<lambda>x. X x * indicator A x"
-  let "?Q A" = "integral\<^isup>P M (?f A)"
+  let ?f = "\<lambda>A x. X x * indicator A x"
+  let ?Q = "\<lambda>A. integral\<^isup>P M (?f A)"

from measure_space_density[OF borel]
have Q: "measure_space (N\<lparr> measure := ?Q \<rparr>)"
@@ -146,7 +146,7 @@
by auto
from factorize_measurable_function_pos[OF assms(1,2) this] guess n .. note n = this
from factorize_measurable_function_pos[OF assms Z] guess p .. note p = this
-  let "?g x" = "p x - n x"
+  let ?g = "\<lambda>x. p x - n x"
show "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x)"
proof (intro bexI ballI)
show "?g \<in> borel_measurable M'" using p n by auto```
```--- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -627,7 +627,7 @@
by (intro P.measure_space_vimage[OF I']) (auto simp add: measure_preserving_def)
show ?case
proof (intro exI[of _ ?\<nu>] conjI ballI)
-    let "?m A" = "measure (Pi\<^isub>M I M\<lparr>measure := \<nu>\<rparr> \<Otimes>\<^isub>M M i) (?h -` A \<inter> space P.P)"
+    let ?m = "\<lambda>A. measure (Pi\<^isub>M I M\<lparr>measure := \<nu>\<rparr> \<Otimes>\<^isub>M M i) (?h -` A \<inter> space P.P)"
{ fix A assume A: "A \<in> (\<Pi> i\<in>insert i I. sets (M i))"
then have *: "?h -` Pi\<^isub>E (insert i I) A \<inter> space P.P = Pi\<^isub>E I A \<times> A i"
using `i \<notin> I` M.sets_into_space by (auto simp: space_pair_measure space_product_algebra) blast
@@ -648,7 +648,7 @@
"(\<Union>k. \<Pi>\<^isub>E j \<in> insert i I. F j k) = space I'.G"
"\<And>k. \<And>j. j \<in> insert i I \<Longrightarrow> \<mu> j (F j k) \<noteq> \<infinity>"
by blast+
-      let "?F k" = "\<Pi>\<^isub>E j \<in> insert i I. F j k"
+      let ?F = "\<lambda>k. \<Pi>\<^isub>E j \<in> insert i I. F j k"
show "\<exists>F::nat \<Rightarrow> ('i \<Rightarrow> 'a) set. range F \<subseteq> sets I'.P \<and>
(\<Union>i. F i) = (\<Pi>\<^isub>E i\<in>insert i I. space (M i)) \<and> (\<forall>i. ?m (F i) \<noteq> \<infinity>)"
proof (intro exI[of _ ?F] conjI allI)
@@ -727,7 +727,7 @@
interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
interpret P: pair_sigma_finite I.P J.P by default
let ?g = "\<lambda>(x,y). merge I x J y"
-  let "?X S" = "?g -` S \<inter> space P.P"
+  let ?X = "\<lambda>S. ?g -` S \<inter> space P.P"
from IJ.sigma_finite_pairs obtain F where
F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
"incseq (\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k)"
@@ -839,7 +839,7 @@
unfolding product_positive_integral_fold[OF IJ, unfolded insert, simplified, OF f]
proof (rule I.positive_integral_cong, subst product_positive_integral_singleton)
fix x assume x: "x \<in> space I.P"
-    let "?f y" = "f (restrict (x(i := y)) (insert i I))"
+    let ?f = "\<lambda>y. f (restrict (x(i := y)) (insert i I))"
have f'_eq: "\<And>y. ?f y = f (x(i := y))"
using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
show "?f \<in> borel_measurable (M i)" unfolding f'_eq
@@ -930,7 +930,7 @@
unfolding product_integral_fold[OF IJ, simplified, OF f]
proof (rule I.integral_cong, subst product_integral_singleton)
fix x assume x: "x \<in> space I.P"
-    let "?f y" = "f (restrict (x(i := y)) (insert i I))"
+    let ?f = "\<lambda>y. f (restrict (x(i := y)) (insert i I))"
have f'_eq: "\<And>y. ?f y = f (x(i := y))"
using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
have f: "f \<in> borel_measurable I'.P" using f unfolding integrable_def by auto```
```--- a/src/HOL/Probability/Independent_Family.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/Independent_Family.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -142,7 +142,7 @@
with indep have "indep_sets F J"
by (subst (asm) indep_sets_finite_index_sets) auto
{ fix J K assume "indep_sets F K"
-    let "?G S i" = "if i \<in> S then ?F i else F i"
+    let ?G = "\<lambda>S i. if i \<in> S then ?F i else F i"
assume "finite J" "J \<subseteq> K"
then have "indep_sets (?G J) K"
proof induct
@@ -384,7 +384,7 @@
assumes disjoint: "disjoint_family_on I J"
shows "indep_sets (\<lambda>j. sigma_sets (space M) (\<Union>i\<in>I j. E i)) J"
proof -
-  let "?E j" = "{\<Inter>k\<in>K. E' k| E' K. finite K \<and> K \<noteq> {} \<and> K \<subseteq> I j \<and> (\<forall>k\<in>K. E' k \<in> E k) }"
+  let ?E = "\<lambda>j. {\<Inter>k\<in>K. E' k| E' K. finite K \<and> K \<noteq> {} \<and> K \<subseteq> I j \<and> (\<forall>k\<in>K. E' k \<in> E k) }"

from indep have E: "\<And>j i. j \<in> J \<Longrightarrow> i \<in> I j \<Longrightarrow> E i \<subseteq> events"
unfolding indep_sets_def by auto
@@ -447,7 +447,7 @@
with * L_inj show "k = j" by auto
qed (insert *, simp) }
note k_simp[simp] = this
-      let "?E' l" = "E' (k l) l"
+      let ?E' = "\<lambda>l. E' (k l) l"
have "prob (\<Inter>j\<in>K. A j) = prob (\<Inter>l\<in>(\<Union>k\<in>K. L k). ?E' l)"
by (auto simp: A intro!: arg_cong[where f=prob])
also have "\<dots> = (\<Prod>l\<in>(\<Union>k\<in>K. L k). prob (?E' l))"
@@ -658,7 +658,7 @@
fix i show "Int_stable \<lparr>space = space M, sets = {F i}\<rparr>"
unfolding Int_stable_def by simp
qed
-  let "?Q n" = "\<Union>i\<in>{n..}. F i"
+  let ?Q = "\<lambda>n. \<Union>i\<in>{n..}. F i"
show "(\<Inter>n. \<Union>m\<in>{n..}. F m) \<in> terminal_events (\<lambda>i. sigma_sets (space M) {F i})"
unfolding terminal_events_def
proof
@@ -691,7 +691,7 @@
proof (rule indep_setsI[OF F(1)])
fix A J assume J: "J \<noteq> {}" "J \<subseteq> I" "finite J"
assume A: "\<forall>j\<in>J. A j \<in> F j"
-    let "?A j" = "if j \<in> J then A j else space M"
+    let ?A = "\<lambda>j. if j \<in> J then A j else space M"
have "prob (\<Inter>j\<in>I. ?A j) = prob (\<Inter>j\<in>J. A j)"
using subset_trans[OF F(1) space_closed] J A
by (auto intro!: arg_cong[where f=prob] split: split_if_asm) blast```
```--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -52,7 +52,7 @@
from J.sigma_finite_pairs guess F .. note F = this
then have [simp,intro]: "\<And>k i. k \<in> J \<Longrightarrow> F k i \<in> sets (M k)"
by auto
-  let "?F i" = "\<Pi>\<^isub>E k\<in>J. F k i"
+  let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. F k i"
let ?J = "product_algebra_generator J M \<lparr> measure := measure (Pi\<^isub>M J M) \<rparr>"
have "?R \<in> measure_preserving (\<Pi>\<^isub>M i\<in>K. M i) (sigma ?J)"
proof (rule K.measure_preserving_Int_stable)
@@ -448,7 +448,7 @@
"K - J \<noteq> {}" "K - J \<subseteq> I" "\<mu>G Z = measure (Pi\<^isub>M K M) X"
by (auto simp: subset_insertI)

-    let "?M y" = "merge J y (K - J) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M)"
+    let ?M = "\<lambda>y. merge J y (K - J) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M)"
{ fix y assume y: "y \<in> space (Pi\<^isub>M J M)"
note * = merge_emb[OF `K \<subseteq> I` `J \<subseteq> I` y, of X]
moreover
@@ -487,7 +487,7 @@
by (intro KmJ.measure_le_1 merge_in_G(2)[OF x]) }
note le_1 = this

-    let "?q y" = "\<mu>G (merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M))"
+    let ?q = "\<lambda>y. \<mu>G (merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M))"
have "?q \<in> borel_measurable (Pi\<^isub>M J M)"
unfolding `Z = emb I K X` using J K merge_in_G(3)
by (simp add: merge_in_G  \<mu>G_eq measure_fold_measurable
@@ -536,15 +536,15 @@
using \<mu>G_spec[of "J 0" "A 0" "X 0"] J A_eq
by (auto intro!: INF_lower2[of 0] J.measure_le_1)

-      let "?M K Z y" = "merge K y (I - K) -` Z \<inter> space (Pi\<^isub>M I M)"
+      let ?M = "\<lambda>K Z y. merge K y (I - K) -` Z \<inter> space (Pi\<^isub>M I M)"

{ fix Z k assume Z: "range Z \<subseteq> sets ?G" "decseq Z" "\<forall>n. ?a / 2^k \<le> \<mu>G (Z n)"
then have Z_sets: "\<And>n. Z n \<in> sets ?G" by auto
fix J' assume J': "J' \<noteq> {}" "finite J'" "J' \<subseteq> I"
interpret J': finite_product_prob_space M J' by default fact+

-        let "?q n y" = "\<mu>G (?M J' (Z n) y)"
-        let "?Q n" = "?q n -` {?a / 2^(k+1) ..} \<inter> space (Pi\<^isub>M J' M)"
+        let ?q = "\<lambda>n y. \<mu>G (?M J' (Z n) y)"
+        let ?Q = "\<lambda>n. ?q n -` {?a / 2^(k+1) ..} \<inter> space (Pi\<^isub>M J' M)"
{ fix n
have "?q n \<in> borel_measurable (Pi\<^isub>M J' M)"
using Z J' by (intro fold(1)) auto
@@ -599,13 +599,14 @@
then have "\<exists>w\<in>space (Pi\<^isub>M J' M). \<forall>n. ?a / 2 ^ (k + 1) \<le> ?q n w" by auto }
note Ex_w = this

-      let "?q k n y" = "\<mu>G (?M (J k) (A n) y)"
+      let ?q = "\<lambda>k n y. \<mu>G (?M (J k) (A n) y)"

have "\<forall>n. ?a / 2 ^ 0 \<le> \<mu>G (A n)" by (auto intro: INF_lower)
from Ex_w[OF A(1,2) this J(1-3), of 0] guess w0 .. note w0 = this

-      let "?P k wk w" =
-        "w \<in> space (Pi\<^isub>M (J (Suc k)) M) \<and> restrict w (J k) = wk \<and> (\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> ?q (Suc k) n w)"
+      let ?P =
+        "\<lambda>k wk w. w \<in> space (Pi\<^isub>M (J (Suc k)) M) \<and> restrict w (J k) = wk \<and>
+          (\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> ?q (Suc k) n w)"
def w \<equiv> "nat_rec w0 (\<lambda>k wk. Eps (?P k wk))"

{ fix k have w: "w k \<in> space (Pi\<^isub>M (J k) M) \<and>
@@ -1015,7 +1016,7 @@
fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)"
shows "(\<lambda>n. \<Prod>i\<le>n. M.\<mu>' i (E i)) ----> \<mu>' (Pi UNIV E)"
proof -
-  let "?E n" = "emb UNIV {..n} (Pi\<^isub>E {.. n} E)"
+  let ?E = "\<lambda>n. emb UNIV {..n} (Pi\<^isub>E {.. n} E)"
{ fix n :: nat
interpret n: finite_product_prob_space M "{..n}" by default auto
have "(\<Prod>i\<le>n. M.\<mu>' i (E i)) = n.\<mu>' (Pi\<^isub>E {.. n} E)"```
```--- a/src/HOL/Probability/Information.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/Information.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -748,8 +748,8 @@
proof -
interpret MX: finite_prob_space "MX\<lparr>measure := ereal\<circ>distribution X\<rparr>"
using MX by (rule distribution_finite_prob_space)
-  let "?X x" = "distribution X {x}"
-  let "?XX x y" = "joint_distribution X X {(x, y)}"
+  let ?X = "\<lambda>x. distribution X {x}"
+  let ?XX = "\<lambda>x y. joint_distribution X X {(x, y)}"

{ fix x y :: 'c
{ assume "x \<noteq> y"
@@ -803,7 +803,7 @@
assumes X: "simple_function M X"
shows "\<H>(X) \<le> log b (card (X ` space M \<inter> {x. distribution X {x} \<noteq> 0}))"
proof -
-  let "?p x" = "distribution X {x}"
+  let ?p = "\<lambda>x. distribution X {x}"
have "\<H>(X) = (\<Sum>x\<in>X`space M. ?p x * log b (1 / ?p x))"
unfolding entropy_eq[OF X] setsum_negf[symmetric]
by (auto intro!: setsum_cong simp: log_simps)
@@ -1117,10 +1117,10 @@
proof -
interpret MX: finite_sigma_algebra MX using MX by simp
interpret MZ: finite_sigma_algebra MZ using MZ by simp
-  let "?XXZ x y z" = "joint_distribution X (\<lambda>x. (X x, Z x)) {(x, y, z)}"
-  let "?XZ x z" = "joint_distribution X Z {(x, z)}"
-  let "?Z z" = "distribution Z {z}"
-  let "?f x y z" = "log b (?XXZ x y z * ?Z z / (?XZ x z * ?XZ y z))"
+  let ?XXZ = "\<lambda>x y z. joint_distribution X (\<lambda>x. (X x, Z x)) {(x, y, z)}"
+  let ?XZ = "\<lambda>x z. joint_distribution X Z {(x, z)}"
+  let ?Z = "\<lambda>z. distribution Z {z}"
+  let ?f = "\<lambda>x y z. log b (?XXZ x y z * ?Z z / (?XZ x z * ?XZ y z))"
{ fix x z have "?XXZ x x z = ?XZ x z"
unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>']) }
note this[simp]
@@ -1183,9 +1183,9 @@
assumes X: "simple_function M X" and Z: "simple_function M Z"
shows  "\<I>(X ; Z) = \<H>(X) - \<H>(X | Z)"
proof -
-  let "?XZ x z" = "joint_distribution X Z {(x, z)}"
-  let "?Z z" = "distribution Z {z}"
-  let "?X x" = "distribution X {x}"
+  let ?XZ = "\<lambda>x z. joint_distribution X Z {(x, z)}"
+  let ?Z = "\<lambda>z. distribution Z {z}"
+  let ?X = "\<lambda>x. distribution X {x}"
note fX = X[THEN simple_function_imp_finite_random_variable]
note fZ = Z[THEN simple_function_imp_finite_random_variable]
note finite_distribution_order[OF fX fZ, simp]
@@ -1214,9 +1214,9 @@
assumes X: "simple_function M X" and Y: "simple_function M Y"
shows  "\<H>(\<lambda>x. (X x, Y x)) = \<H>(X) + \<H>(Y|X)"
proof -
-  let "?XY x y" = "joint_distribution X Y {(x, y)}"
-  let "?Y y" = "distribution Y {y}"
-  let "?X x" = "distribution X {x}"
+  let ?XY = "\<lambda>x y. joint_distribution X Y {(x, y)}"
+  let ?Y = "\<lambda>y. distribution Y {y}"
+  let ?X = "\<lambda>x. distribution X {x}"
note fX = X[THEN simple_function_imp_finite_random_variable]
note fY = Y[THEN simple_function_imp_finite_random_variable]
note finite_distribution_order[OF fX fY, simp]
@@ -1352,9 +1352,9 @@
assumes svi: "subvimage (space M) X P"
shows "\<H>(X) = \<H>(P) + \<H>(X|P)"
proof -
-  let "?XP x p" = "joint_distribution X P {(x, p)}"
-  let "?X x" = "distribution X {x}"
-  let "?P p" = "distribution P {p}"
+  let ?XP = "\<lambda>x p. joint_distribution X P {(x, p)}"
+  let ?X = "\<lambda>x. distribution X {x}"
+  let ?P = "\<lambda>p. distribution P {p}"
note fX = sf(1)[THEN simple_function_imp_finite_random_variable]
note fP = sf(2)[THEN simple_function_imp_finite_random_variable]
note finite_distribution_order[OF fX fP, simp]```
```--- a/src/HOL/Probability/Lebesgue_Integration.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -331,7 +331,7 @@
"\<And>i x. real (f x i) = (if real i \<le> u x then i * 2 ^ i else real (natfloor (real (u x) * 2 ^ i)))"
unfolding f_def by auto

-  let "?g j x" = "real (f x j) / 2^j :: ereal"
+  let ?g = "\<lambda>j x. real (f x j) / 2^j :: ereal"
show ?thesis
proof (intro exI[of _ ?g] conjI allI ballI)
fix i
@@ -567,7 +567,7 @@
shows "integral\<^isup>S M f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. the_elem (f`A) * \<mu> A)"
(is "_ = setsum _ (?p ` space M)")
proof-
-  let "?sub x" = "?p ` (f -` {x} \<inter> space M)"
+  let ?sub = "\<lambda>x. ?p ` (f -` {x} \<inter> space M)"
let ?SIGMA = "Sigma (f`space M) ?sub"

have [intro]:
@@ -659,7 +659,7 @@
and mono: "AE x. f x \<le> g x"
shows "integral\<^isup>S M f \<le> integral\<^isup>S M g"
proof -
-  let "?S x" = "(g -` {g x} \<inter> space M) \<inter> (f -` {f x} \<inter> space M)"
+  let ?S = "\<lambda>x. (g -` {g x} \<inter> space M) \<inter> (f -` {f x} \<inter> space M)"
have *: "\<And>x. g -` {g x} \<inter> f -` {f x} \<inter> space M = ?S x"
"\<And>x. f -` {f x} \<inter> g -` {g x} \<inter> space M = ?S x" by auto
show ?thesis
@@ -899,7 +899,7 @@
let ?G = "{x \<in> space M. \<not> g x \<noteq> \<infinity>}"
note gM = g(1)[THEN borel_measurable_simple_function]
have \<mu>G_pos: "0 \<le> \<mu> ?G" using gM by auto
-  let "?g y x" = "if g x = \<infinity> then y else max 0 (g x)"
+  let ?g = "\<lambda>y x. if g x = \<infinity> then y else max 0 (g x)"
from g gM have g_in_A: "\<And>y. 0 \<le> y \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> ?g y \<in> ?A"
apply (safe intro!: simple_function_max simple_function_If)
apply (force simp: max_def le_fun_def split: split_if_asm)+
@@ -941,7 +941,7 @@
fix n assume n: "simple_function M n" "n \<le> max 0 \<circ> u"
from ae[THEN AE_E] guess N . note N = this
then have ae_N: "AE x. x \<notin> N" by (auto intro: AE_not_in)
-  let "?n x" = "n x * indicator (space M - N) x"
+  let ?n = "\<lambda>x. n x * indicator (space M - N) x"
have "AE x. n x \<le> ?n x" "simple_function M ?n"
using n N ae_N by auto
moreover
@@ -974,7 +974,7 @@
lemma (in measure_space) positive_integral_eq_simple_integral:
assumes f: "simple_function M f" "\<And>x. 0 \<le> f x" shows "integral\<^isup>P M f = integral\<^isup>S M f"
proof -
-  let "?f x" = "f x * indicator (space M) x"
+  let ?f = "\<lambda>x. f x * indicator (space M) x"
have f': "simple_function M ?f" using f by auto
with f(2) have [simp]: "max 0 \<circ> ?f = ?f"
by (auto simp: fun_eq_iff max_def split: split_indicator)
@@ -1010,11 +1010,11 @@
using u(3) by auto
fix a :: ereal assume "0 < a" "a < 1"
hence "a \<noteq> 0" by auto
-  let "?B i" = "{x \<in> space M. a * u x \<le> f i x}"
+  let ?B = "\<lambda>i. {x \<in> space M. a * u x \<le> f i x}"
have B: "\<And>i. ?B i \<in> sets M"
using f `simple_function M u` by (auto simp: borel_measurable_simple_function)

-  let "?uB i x" = "u x * indicator (?B i) x"
+  let ?uB = "\<lambda>i x. u x * indicator (?B i) x"

{ fix i have "?B i \<subseteq> ?B (Suc i)"
proof safe
@@ -1027,7 +1027,7 @@

note B_u = Int[OF u(1)[THEN simple_functionD(2)] B]

-  let "?B' i n" = "(u -` {i} \<inter> space M) \<inter> ?B n"
+  let ?B' = "\<lambda>i n. (u -` {i} \<inter> space M) \<inter> ?B n"
have measure_conv: "\<And>i. \<mu> (u -` {i} \<inter> space M) = (SUP n. \<mu> (?B' i n))"
proof -
fix i
@@ -1126,7 +1126,7 @@
from f have "AE x. \<forall>i. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x"
from this[THEN AE_E] guess N . note N = this
-  let "?f i x" = "if x \<in> space M - N then f i x else 0"
+  let ?f = "\<lambda>i x. if x \<in> space M - N then f i x else 0"
have f_eq: "AE x. \<forall>i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ N])
then have "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) = (\<integral>\<^isup>+ x. (SUP i. ?f i x) \<partial>M)"
by (auto intro!: positive_integral_cong_AE)
@@ -1202,7 +1202,7 @@
interpret T: measure_space M' by (rule measure_space_vimage[OF T])
from T.borel_measurable_implies_simple_function_sequence'[OF f]
guess f' . note f' = this
-  let "?f i x" = "f' i (T x)"
+  let ?f = "\<lambda>i x. f' i (T x)"
have inc: "incseq ?f" using f' by (force simp: le_fun_def incseq_def)
have sup: "\<And>x. (SUP i. ?f i x) = max 0 (f (T x))"
using f'(4) .
@@ -1225,7 +1225,7 @@
note u = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess v .
note v = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
-  let "?L' i x" = "a * u i x + v i x"
+  let ?L' = "\<lambda>i x. a * u i x + v i x"

have "?L \<in> borel_measurable M" using assms by auto
from borel_measurable_implies_simple_function_sequence'[OF this] guess l .
@@ -1494,7 +1494,7 @@
from G(4) g(2) have G_M': "AE x in M'. (SUP i. G i x) = g x"
by (auto intro!: ac split: split_max)
{ fix i
-    let "?I y x" = "indicator (G i -` {y} \<inter> space M) x"
+    let ?I = "\<lambda>y x. indicator (G i -` {y} \<inter> space M) x"
{ fix x assume *: "x \<in> space M" "0 \<le> f x" "0 \<le> g x"
then have [simp]: "G i ` space M \<inter> {y. G i x = y \<and> x \<in> space M} = {G i x}" by auto
from * G' G have "(\<Sum>y\<in>G i`space M. y * (f x * ?I y x)) = f x * (\<Sum>y\<in>G i`space M. (y * ?I y x))"
@@ -1546,7 +1546,7 @@
then have "0 \<le> r" by (auto simp add: ereal_zero_less_0_iff) }
note gt_1 = this
assume *: "integral\<^isup>P M u = 0"
-    let "?M n" = "{x \<in> space M. 1 \<le> real (n::nat) * u x}"
+    let ?M = "\<lambda>n. {x \<in> space M. 1 \<le> real (n::nat) * u x}"
have "0 = (SUP n. \<mu> (?M n \<inter> ?A))"
proof -
{ fix n :: nat
@@ -1618,7 +1618,7 @@
proof -
interpret R: measure_space ?R
by (rule restricted_measure_space) fact
-  let "?I g x" = "g x * indicator A x :: ereal"
+  let ?I = "\<lambda>g x. g x * indicator A x :: ereal"
show ?thesis
unfolding positive_integral_def
unfolding simple_function_restricted[OF A]
@@ -1846,10 +1846,10 @@
and f_def: "\<And>x. f x = u x - v x" and pos: "\<And>x. 0 \<le> u x" "\<And>x. 0 \<le> v x"
shows "integrable M f" and "integral\<^isup>L M f = integral\<^isup>L M u - integral\<^isup>L M v"
proof -
-  let "?f x" = "max 0 (ereal (f x))"
-  let "?mf x" = "max 0 (ereal (- f x))"
-  let "?u x" = "max 0 (ereal (u x))"
-  let "?v x" = "max 0 (ereal (v x))"
+  let ?f = "\<lambda>x. max 0 (ereal (f x))"
+  let ?mf = "\<lambda>x. max 0 (ereal (- f x))"
+  let ?u = "\<lambda>x. max 0 (ereal (u x))"
+  let ?v = "\<lambda>x. max 0 (ereal (v x))"

from borel_measurable_diff[of u v] integrable
have f_borel: "?f \<in> borel_measurable M" and
@@ -1886,12 +1886,12 @@
shows "integrable M (\<lambda>t. a * f t + g t)"
and "(\<integral> t. a * f t + g t \<partial>M) = a * integral\<^isup>L M f + integral\<^isup>L M g" (is ?EQ)
proof -
-  let "?f x" = "max 0 (ereal (f x))"
-  let "?g x" = "max 0 (ereal (g x))"
-  let "?mf x" = "max 0 (ereal (- f x))"
-  let "?mg x" = "max 0 (ereal (- g x))"
-  let "?p t" = "max 0 (a * f t) + max 0 (g t)"
-  let "?n t" = "max 0 (- (a * f t)) + max 0 (- g t)"
+  let ?f = "\<lambda>x. max 0 (ereal (f x))"
+  let ?g = "\<lambda>x. max 0 (ereal (g x))"
+  let ?mf = "\<lambda>x. max 0 (ereal (- f x))"
+  let ?mg = "\<lambda>x. max 0 (ereal (- g x))"
+  let ?p = "\<lambda>t. max 0 (a * f t) + max 0 (g t)"
+  let ?n = "\<lambda>t. max 0 (- (a * f t)) + max 0 (- g t)"

from assms have linear:
"(\<integral>\<^isup>+ x. ereal a * ?f x + ?g x \<partial>M) = ereal a * integral\<^isup>P M ?f + integral\<^isup>P M ?g"
@@ -2353,7 +2353,7 @@
show "\<bar>u' x\<bar> \<le> w x" using u'_bound[OF x] .
qed

-  let "?diff n x" = "2 * w x - \<bar>u n x - u' x\<bar>"
+  let ?diff = "\<lambda>n x. 2 * w x - \<bar>u n x - u' x\<bar>"
have diff: "\<And>n. integrable M (\<lambda>x. \<bar>u n x - u' x\<bar>)"
using w u `integrable M u'`
by (auto intro!: integral_add integral_diff integral_cmult integrable_abs)
@@ -2468,7 +2468,7 @@
from bchoice[OF this]
obtain w where w: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. \<bar>f i x\<bar>) sums w x" by auto

-  let "?w y" = "if y \<in> space M then w y else 0"
+  let ?w = "\<lambda>y. if y \<in> space M then w y else 0"

obtain x where abs_sum: "(\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M)) sums x"
using sums unfolding summable_def ..
@@ -2484,8 +2484,8 @@

have 3: "integrable M ?w"
proof (rule integral_monotone_convergence(1))
-    let "?F n y" = "(\<Sum>i = 0..<n. \<bar>f i y\<bar>)"
-    let "?w' n y" = "if y \<in> space M then ?F n y else 0"
+    let ?F = "\<lambda>n y. (\<Sum>i = 0..<n. \<bar>f i y\<bar>)"
+    let ?w' = "\<lambda>n y. if y \<in> space M then ?F n y else 0"
have "\<And>n. integrable M (?F n)"
using borel by (auto intro!: integral_setsum integrable_abs)
thus "\<And>n. integrable M (?w' n)" by (simp cong: integrable_cong)
@@ -2522,8 +2522,8 @@
shows "integrable M f"
and "(\<lambda>r. enum r * real (\<mu> (f -` {enum r} \<inter> space M))) sums integral\<^isup>L M f" (is ?sums)
proof -
-  let "?A r" = "f -` {enum r} \<inter> space M"
-  let "?F r x" = "enum r * indicator (?A r) x"
+  let ?A = "\<lambda>r. f -` {enum r} \<inter> space M"
+  let ?F = "\<lambda>r x. enum r * indicator (?A r) x"
have enum_eq: "\<And>r. enum r * real (\<mu> (?A r)) = integral\<^isup>L M (?F r)"
using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator)

@@ -2579,8 +2579,8 @@
and "(\<integral>x. f x \<partial>M) =
(\<Sum> r \<in> f`space M. r * real (\<mu> (f -` {r} \<inter> space M)))" (is "?integral")
proof -
-  let "?A r" = "f -` {r} \<inter> space M"
-  let "?S x" = "\<Sum>r\<in>f`space M. r * indicator (?A r) x"
+  let ?A = "\<lambda>r. f -` {r} \<inter> space M"
+  let ?S = "\<lambda>x. \<Sum>r\<in>f`space M. r * indicator (?A r) x"

{ fix x assume "x \<in> space M"
have "f x = (\<Sum>r\<in>f`space M. if x \<in> ?A r then r else 0)"```
```--- a/src/HOL/Probability/Lebesgue_Measure.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -133,8 +133,8 @@
fix A :: "nat \<Rightarrow> 'b set" assume rA: "range A \<subseteq> sets lebesgue" "disjoint_family A"
then have A[simp, intro]: "\<And>i n. (indicator (A i) :: _ \<Rightarrow> real) integrable_on cube n"
by (auto dest: lebesgueD)
-    let "?m n i" = "integral (cube n) (indicator (A i) :: _\<Rightarrow>real)"
-    let "?M n I" = "integral (cube n) (indicator (\<Union>i\<in>I. A i) :: _\<Rightarrow>real)"
+    let ?m = "\<lambda>n i. integral (cube n) (indicator (A i) :: _\<Rightarrow>real)"
+    let ?M = "\<lambda>n I. integral (cube n) (indicator (\<Union>i\<in>I. A i) :: _\<Rightarrow>real)"
have nn[simp, intro]: "\<And>i n. 0 \<le> ?m n i" by (auto intro!: integral_nonneg)
assume "(\<Union>i. A i) \<in> sets lebesgue"
then have UN_A[simp, intro]: "\<And>i n. (indicator (\<Union>i. A i) :: _ \<Rightarrow> real) integrable_on cube n"
@@ -560,8 +560,8 @@
shows "((\<lambda>x. real (f x)) has_integral (real (integral\<^isup>S lebesgue f))) UNIV"
unfolding simple_integral_def space_lebesgue
proof (subst lebesgue_simple_function_indicator)
-  let "?M x" = "lebesgue.\<mu> (f -` {x} \<inter> UNIV)"
-  let "?F x" = "indicator (f -` {x})"
+  let ?M = "\<lambda>x. lebesgue.\<mu> (f -` {x} \<inter> UNIV)"
+  let ?F = "\<lambda>x. indicator (f -` {x})"
{ fix x y assume "y \<in> range f"
from subsetD[OF f' this] have "y * ?F y x = ereal (real y * ?F y x)"
by (cases rule: ereal2_cases[of y "?F y x"])
@@ -637,7 +637,7 @@
guess u . note u = this
have SUP_eq: "\<And>x. (SUP i. u i x) = f x"
using u(4) f(2)[THEN subsetD] by (auto split: split_max)
-  let "?u i x" = "real (u i x)"
+  let ?u = "\<lambda>i x. real (u i x)"
note u_eq = lebesgue.positive_integral_eq_simple_integral[OF u(1,5), symmetric]
{ fix i
note u_eq
@@ -986,7 +986,7 @@
(is "_ = ?\<nu> X")
proof -
let ?E = "\<lparr>space = UNIV, sets = range (\<lambda>(a,b). {a::real .. b})\<rparr> :: real algebra"
-  let "?M \<nu>" = "\<lparr>space = space ?E, sets = sets (sigma ?E), measure = \<nu>\<rparr> :: real measure_space"
+  let ?M = "\<lambda>\<nu>. \<lparr>space = space ?E, sets = sets (sigma ?E), measure = \<nu>\<rparr> :: real measure_space"
have *: "?M (measure lebesgue) = lborel"
unfolding borel_eq_atLeastAtMost[symmetric]
```--- a/src/HOL/Probability/Measure.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/Measure.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -439,7 +439,7 @@
shows "\<mu> (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. \<mu> (A i))"
using assms proof induct
case (insert i I)
-  then have "(\<Union>i\<in>I. A i) \<in> sets M" by (auto intro: finite_UN)
+  then have "(\<Union>i\<in>I. A i) \<in> sets M" by auto
then have "\<mu> (\<Union>i\<in>insert i I. A i) \<le> \<mu> (A i) + \<mu> (\<Union>i\<in>I. A i)"
also have "\<dots> \<le> (\<Sum>i\<in>insert i I. \<mu> (A i))"
@@ -458,7 +458,7 @@
also have "\<dots> \<le> (\<Sum>i. \<mu> (f i))"
using range_disjointed_sets[OF assms] assms
-    by (auto intro!: suminf_le_pos measure_mono positive_measure disjointed_subset)
+    by (auto intro!: suminf_le_pos measure_mono disjointed_subset)
finally show ?thesis .
qed

@@ -509,7 +509,7 @@
assumes "X \<in> sets (sigma E)"
shows "\<mu> X = \<nu> X"
proof -
-  let "?D F" = "{D. D \<in> sets (sigma E) \<and> \<mu> (F \<inter> D) = \<nu> (F \<inter> D)}"
+  let ?D = "\<lambda>F. {D. D \<in> sets (sigma E) \<and> \<mu> (F \<inter> D) = \<nu> (F \<inter> D)}"
interpret M: measure_space ?M
where "space ?M = space E" and "sets ?M = sets (sigma E)" and "measure ?M = \<mu>" by (simp_all add: M)
interpret N: measure_space ?N
@@ -559,7 +559,7 @@
have "\<And>D. D \<in> sets (sigma E) \<Longrightarrow> \<mu> (F \<inter> D) = \<nu> (F \<inter> D)"
by (subst (asm) *) auto }
note * = this
-  let "?A i" = "A i \<inter> X"
+  let ?A = "\<lambda>i. A i \<inter> X"
have A': "range ?A \<subseteq> sets (sigma E)" "incseq ?A"
using A(1,2) `X \<in> sets (sigma E)` by (auto simp: incseq_def)
{ fix i have "\<mu> (?A i) = \<nu> (?A i)"
@@ -1015,7 +1015,7 @@
proof (rule measure_unique_Int_stable[OF E A(1,2,3) _ _ eq _ X])
interpret M: measure_space M by fact
interpret N: measure_space N by fact
-  let "?T X" = "T -` X \<inter> space N"
+  let ?T = "\<lambda>X. T -` X \<inter> space N"
show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = measure M\<rparr>"
by (rule M.measure_space_cong) (auto simp: M)
show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = \<lambda>X. measure N (?T X)\<rparr>" (is "measure_space ?E")
@@ -1397,7 +1397,7 @@

lemma (in finite_measure_space) sum_over_space: "(\<Sum>x\<in>space M. \<mu> {x}) = \<mu> (space M)"
using measure_setsum[of "space M" "\<lambda>i. {i}"]
-  by (simp add: sets_eq_Pow disjoint_family_on_def finite_space)
+  by (simp add: disjoint_family_on_def finite_space)

lemma (in finite_measure_space) finite_measure_singleton:
assumes A: "A \<subseteq> space M" shows "\<mu>' A = (\<Sum>x\<in>A. \<mu>' {x})"```
```--- a/src/HOL/Probability/Probability_Measure.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -380,7 +380,7 @@
assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q"
shows "q (expectation X) \<le> expectation (\<lambda>x. q (X x))"
proof -
-  let "?F x" = "Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I))"
+  let ?F = "\<lambda>x. Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I))"
from not_empty X(2) have "I \<noteq> {}" by auto

from I have "open I" by auto
@@ -741,7 +741,7 @@
proof (subst finite_measure_finite_Union[symmetric])
interpret MX: finite_sigma_algebra MX using X by auto
show "finite (space MX)" using MX.finite_space .
-  let "?d i" = "(\<lambda>x. (X x, Y x)) -` ({i} \<times> B) \<inter> space M"
+  let ?d = "\<lambda>i. (\<lambda>x. (X x, Y x)) -` ({i} \<times> B) \<inter> space M"
{ fix i assume "i \<in> space MX"
moreover have "?d i = (X -` {i} \<inter> space M) \<inter> (Y -` B \<inter> space M)" by auto
ultimately show "?d i \<in> events"```
```--- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -17,7 +17,7 @@
measure: "\<And>i. \<mu> (A i) \<noteq> \<infinity>" and
disjoint: "disjoint_family A"
using disjoint_sigma_finite by auto
-  let "?B i" = "2^Suc i * \<mu> (A i)"
+  let ?B = "\<lambda>i. 2^Suc i * \<mu> (A i)"
have "\<forall>i. \<exists>x. 0 < x \<and> x < inverse (?B i)"
proof
fix i have Ai: "A i \<in> sets M" using range by auto
@@ -28,7 +28,7 @@
from choice[OF this] obtain n where n: "\<And>i. 0 < n i"
"\<And>i. n i < inverse (2^Suc i * \<mu> (A i))" by auto
{ fix i have "0 \<le> n i" using n(1)[of i] by auto } note pos = this
-  let "?h x" = "\<Sum>i. n i * indicator (A i) x"
+  let ?h = "\<lambda>x. \<Sum>i. n i * indicator (A i) x"
show ?thesis
proof (safe intro!: bexI[of _ ?h] del: notI)
have "\<And>i. A i \<in> sets M"
@@ -132,8 +132,8 @@
(\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> - e < \<mu>' B - finite_measure.\<mu>' (M\<lparr>measure := \<nu>\<rparr>) B)"
proof -
interpret M': finite_measure "M\<lparr>measure := \<nu>\<rparr>" by fact
-  let "?d A" = "\<mu>' A - M'.\<mu>' A"
-  let "?A A" = "if (\<forall>B\<in>sets M. B \<subseteq> space M - A \<longrightarrow> -e < ?d B)
+  let ?d = "\<lambda>A. \<mu>' A - M'.\<mu>' A"
+  let ?A = "\<lambda>A. if (\<forall>B\<in>sets M. B \<subseteq> space M - A \<longrightarrow> -e < ?d B)
then {}
else (SOME B. B \<in> sets M \<and> B \<subseteq> space M - A \<and> ?d B \<le> -e)"
def A \<equiv> "\<lambda>n. ((\<lambda>B. B \<union> ?A B) ^^ n) {}"
@@ -247,9 +247,9 @@
proof -
interpret M': finite_measure ?M' where
"space ?M' = space M" and "sets ?M' = sets M" and "measure ?M' = \<nu>" by fact auto
-  let "?d A" = "\<mu>' A - M'.\<mu>' A"
-  let "?P A B n" = "A \<in> sets M \<and> A \<subseteq> B \<and> ?d B \<le> ?d A \<and> (\<forall>C\<in>sets M. C \<subseteq> A \<longrightarrow> - 1 / real (Suc n) < ?d C)"
-  let "?r S" = "restricted_space S"
+  let ?d = "\<lambda>A. \<mu>' A - M'.\<mu>' A"
+  let ?P = "\<lambda>A B n. A \<in> sets M \<and> A \<subseteq> B \<and> ?d B \<le> ?d A \<and> (\<forall>C\<in>sets M. C \<subseteq> A \<longrightarrow> - 1 / real (Suc n) < ?d C)"
+  let ?r = "\<lambda>S. restricted_space S"
{ fix S n assume S: "S \<in> sets M"
note r = M'.restricted_finite_measure[of S] restricted_finite_measure[OF S] S
then have "finite_measure (?r S)" "0 < 1 / real (Suc n)"
@@ -342,7 +342,7 @@
(\<integral>\<^isup>+x. g x * indicator (?A \<inter> A) x \<partial>M) +
(\<integral>\<^isup>+x. f x * indicator ((space M - ?A) \<inter> A) x \<partial>M)"
using f g sets unfolding G_def
-        by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator)
+        by (auto cong: positive_integral_cong intro!: positive_integral_add)
also have "\<dots> \<le> \<nu> (?A \<inter> A) + \<nu> ((space M - ?A) \<inter> A)"
using f g sets unfolding G_def by (auto intro!: add_mono)
also have "\<dots> = \<nu> A"
@@ -388,9 +388,9 @@
qed
from choice[OF this] obtain gs where "\<And>i. gs i \<in> G" "\<And>n. integral\<^isup>P M (gs n) = ys n" by auto
hence y_eq: "?y = (SUP i. integral\<^isup>P M (gs i))" using ys by auto
-  let "?g i x" = "Max ((\<lambda>n. gs n x) ` {..i})"
+  let ?g = "\<lambda>i x. Max ((\<lambda>n. gs n x) ` {..i})"
def f \<equiv> "\<lambda>x. SUP i. ?g i x"
-  let "?F A x" = "f x * indicator A x"
+  let ?F = "\<lambda>A x. f x * indicator A x"
have gs_not_empty: "\<And>i x. (\<lambda>n. gs n x) ` {..i} \<noteq> {}" by auto
{ fix i have "?g i \<in> G"
proof (induct i)
@@ -420,7 +420,7 @@
have "\<And>x. 0 \<le> f x"
unfolding f_def using `\<And>i. gs i \<in> G`
by (auto intro!: SUP_upper2 Max_ge_iff[THEN iffD2] simp: G_def)
-  let "?t A" = "\<nu> A - (\<integral>\<^isup>+x. ?F A x \<partial>M)"
+  let ?t = "\<lambda>A. \<nu> A - (\<integral>\<^isup>+x. ?F A x \<partial>M)"
let ?M = "M\<lparr> measure := ?t\<rparr>"
interpret M: sigma_algebra ?M
by (intro sigma_algebra_cong) auto
@@ -522,7 +522,7 @@
using M'.finite_measure b finite_measure M.positive_measure[OF B(1)]
by (cases rule: ereal2_cases[of "?t B" "b * \<mu> B"]) auto }
note bM_le_t = this
-    let "?f0 x" = "f x + b * indicator A0 x"
+    let ?f0 = "\<lambda>x. f x + b * indicator A0 x"
{ fix A assume A: "A \<in> sets M"
hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
have "(\<integral>\<^isup>+x. ?f0 x  * indicator A x \<partial>M) =
@@ -550,8 +550,7 @@
by (cases "\<integral>\<^isup>+x. ?F A x \<partial>M", cases "\<nu> A") auto
finally have "(\<integral>\<^isup>+x. ?f0 x * indicator A x \<partial>M) \<le> \<nu> A" . }
hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G` unfolding G_def
-      by (auto intro!: borel_measurable_indicator borel_measurable_ereal_add
have real: "?t (space M) \<noteq> \<infinity>" "?t A0 \<noteq> \<infinity>"
"b * \<mu> (space M) \<noteq> \<infinity>" "b * \<mu> A0 \<noteq> \<infinity>"
using `A0 \<in> sets M` b
@@ -633,7 +632,7 @@
have "{} \<in> ?Q" using v.empty_measure by auto
then have Q_not_empty: "?Q \<noteq> {}" by blast
have "?a \<le> \<mu> (space M)" using sets_into_space
-    by (auto intro!: SUP_least measure_mono top)
+    by (auto intro!: SUP_least measure_mono)
then have "?a \<noteq> \<infinity>" using finite_measure_of_space
by auto
from SUPR_countable_SUPR[OF Q_not_empty, of \<mu>]
@@ -643,7 +642,7 @@
from choice[OF this] obtain Q' where Q': "\<And>i. Q'' i = \<mu> (Q' i)" "\<And>i. Q' i \<in> ?Q"
by auto
then have a_Lim: "?a = (SUP i::nat. \<mu> (Q' i))" using a by simp
-  let "?O n" = "\<Union>i\<le>n. Q' i"
+  let ?O = "\<lambda>n. \<Union>i\<le>n. Q' i"
have Union: "(SUP i. \<mu> (?O i)) = \<mu> (\<Union>i. ?O i)"
proof (rule continuity_from_below[of ?O])
show "range ?O \<subseteq> sets M" using Q' by (auto intro!: finite_UN)
@@ -675,7 +674,7 @@
using O_in_G[of i] by (auto intro!: exI[of _ "?O i"])
qed
qed
-  let "?O_0" = "(\<Union>i. ?O i)"
+  let ?O_0 = "(\<Union>i. ?O i)"
have "?O_0 \<in> sets M" using Q' by auto
def Q \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> Q' 0 | Suc n \<Rightarrow> ?O (Suc n) - ?O n"
{ fix i have "Q i \<in> sets M" unfolding Q_def using Q'[of 0] by (cases i) (auto intro: O_sets) }
@@ -710,10 +709,9 @@
fix i have "?O i \<union> A \<in> ?Q"
proof (safe del: notI)
show "?O i \<union> A \<in> sets M" using O_sets A by auto
-              from O_in_G[of i]
-              moreover have "\<nu> (?O i \<union> A) \<le> \<nu> (?O i) + \<nu> A"
+              from O_in_G[of i] have "\<nu> (?O i \<union> A) \<le> \<nu> (?O i) + \<nu> A"
using v.measure_subadditive[of "?O i" A] A O_sets by auto
-              ultimately show "\<nu> (?O i \<union> A) \<noteq> \<infinity>"
+              with O_in_G[of i] show "\<nu> (?O i \<union> A) \<noteq> \<infinity>"
using `\<nu> A \<noteq> \<infinity>` by auto
qed
then show "\<mu> (?O i \<union> A) \<le> ?a" by (rule SUP_upper)
@@ -800,7 +798,7 @@
and f: "\<And>A i. A \<in> sets M \<Longrightarrow>
\<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f i x * indicator (Q i \<inter> A) x \<partial>M)"
by auto
-  let "?f x" = "(\<Sum>i. f i x * indicator (Q i) x) + \<infinity> * indicator Q0 x"
+  let ?f = "\<lambda>x. (\<Sum>i. f i x * indicator (Q i) x) + \<infinity> * indicator Q0 x"
show ?thesis
proof (safe intro!: bexI[of _ ?f])
show "?f \<in> borel_measurable M" using Q0 borel Q_sets
@@ -850,7 +848,7 @@
nn: "\<And>x. 0 \<le> h x" and
pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
"\<And>x. x \<in> space M \<Longrightarrow> h x < \<infinity>" by auto
-  let "?T A" = "(\<integral>\<^isup>+x. h x * indicator A x \<partial>M)"
+  let ?T = "\<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x \<partial>M)"
let ?MT = "M\<lparr> measure := ?T \<rparr>"
interpret T: finite_measure ?MT
where "space ?MT = space M" and "sets ?MT = sets M" and "measure ?MT = ?T"
@@ -872,7 +870,7 @@
show ?thesis
proof (safe intro!: bexI[of _ "\<lambda>x. h x * f x"])
show "(\<lambda>x. h x * f x) \<in> borel_measurable M"
-      using borel f_borel by (auto intro: borel_measurable_ereal_times)
+      using borel f_borel by auto
show "\<And>x. 0 \<le> h x * f x" using nn f_borel by auto
fix A assume "A \<in> sets M"
then show "\<nu> A = (\<integral>\<^isup>+x. h x * f x * indicator A x \<partial>M)"
@@ -933,8 +931,8 @@
(is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
shows "AE x. f x = f' x"
proof -
-  let "?\<nu> A" = "?P f A" and "?\<nu>' A" = "?P f' A"
-  let "?f A x" = "f x * indicator A x" and "?f' A x" = "f' x * indicator A x"
+  let ?\<nu> = "\<lambda>A. ?P f A" and ?\<nu>' = "\<lambda>A. ?P f' A"
+  let ?f = "\<lambda>A x. f x * indicator A x" and ?f' = "\<lambda>A x. f' x * indicator A x"
interpret M: measure_space "M\<lparr> measure := ?\<nu>\<rparr>"
using borel(1) pos(1) by (rule measure_space_density) simp
have ac: "absolutely_continuous ?\<nu>"
@@ -957,7 +955,7 @@
proof (rule AE_I')
{ fix f :: "'a \<Rightarrow> ereal" assume borel: "f \<in> borel_measurable M"
and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)"
-      let "?A i" = "Q0 \<inter> {x \<in> space M. f x < (i::nat)}"
+      let ?A = "\<lambda>i. Q0 \<inter> {x \<in> space M. f x < (i::nat)}"
have "(\<Union>i. ?A i) \<in> null_sets"
proof (rule null_sets_UN)
fix i ::nat have "?A i \<in> sets M"
@@ -1079,7 +1077,7 @@
apply (rule_tac Int)
by (cases i) (auto intro: measurable_sets[OF f(1)]) }
note A_in_sets = this
-  let "?A n" = "case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
+  let ?A = "\<lambda>n. case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
show "sigma_finite_measure ?N"
proof (default, intro exI conjI subsetI allI)
fix x assume "x \<in> range ?A"```
```--- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -214,7 +214,7 @@
then have "(\<Union>i. A i) = (\<Union>s\<in>sets M \<inter> range A. s)"
by auto
also have "(\<Union>s\<in>sets M \<inter> range A. s) \<in> sets M"
-    using `finite (sets M)` by (auto intro: finite_UN)
+    using `finite (sets M)` by auto
finally show "(\<Union>i. A i) \<in> sets M" .
qed

@@ -243,7 +243,7 @@
assumes "A`X \<subseteq> sets M"
shows  "(\<Union>x\<in>X. A x) \<in> sets M"
proof -
-  let "?A i" = "if i \<in> X then A i else {}"
+  let ?A = "\<lambda>i. if i \<in> X then A i else {}"
from assms have "range ?A \<subseteq> sets M" by auto
with countable_nat_UN[of "?A \<circ> from_nat"] countable_UN_eq[of ?A M]
have "(\<Union>x. ?A x) \<in> sets M" by auto
@@ -1563,7 +1563,7 @@
unfolding sigma_algebra_eq_Int_stable Int_stable_def
proof (intro ballI)
fix A B assume "A \<in> sets (dynkin M)" "B \<in> sets (dynkin M)"
-    let "?D E" = "\<lparr> space = space M,
+    let ?D = "\<lambda>E. \<lparr> space = space M,
sets = {Q. Q \<subseteq> space M \<and> Q \<inter> E \<in> sets (dynkin M)} \<rparr>"
have "sets M \<subseteq> sets (?D B)"
proof
@@ -1637,7 +1637,7 @@
next
fix S assume "S \<subseteq> space (image_space X)"
then obtain S' where "S = X`S'" "S'\<in>sets M"
-    by (auto simp: subset_image_iff sets_eq_Pow image_space_def)
+    by (auto simp: subset_image_iff image_space_def)
then show "S \<in> sets (image_space X)"
by (auto simp: image_space_def)
qed```
```--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -82,7 +82,7 @@
assumes "dc \<in> dining_cryptographers"
shows "result dc \<longleftrightarrow> (payer dc \<noteq> None)"
proof -
-  let "?XOR f l" = "foldl (op \<noteq>) False (map f [0..<l])"
+  let ?XOR = "\<lambda>f l. foldl (op \<noteq>) False (map f [0..<l])"

have foldl_coin:
"\<not> ?XOR (\<lambda>c. coin dc c \<noteq> coin dc (c + 1)) n"
@@ -306,8 +306,8 @@
assumes "xs \<in> inversion ` dc_crypto"
shows "card {dc \<in> dc_crypto. inversion dc = xs} = 2 * n"
proof -
-  let "?set i" = "{dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs}"
-  let "?sets" = "{?set i | i. i < n}"
+  let ?set = "\<lambda>i. {dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs}"
+  let ?sets = "{?set i | i. i < n}"

have [simp]: "length xs = n" using assms
by (auto simp: dc_crypto inversion_def_raw)```
```--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Tue Feb 28 21:53:36 2012 +0100
@@ -333,7 +333,7 @@
using `K k \<noteq> 0` by auto }
note t_eq_imp = this

-  let "?S obs" = "t -`{t obs} \<inter> OB`msgs"
+  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 *: "((\<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
@@ -378,8 +378,8 @@
finally have "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(fst | OB) {(k, obs)}" . }
note CP_T_eq_CP_O = this

-  let "?H obs" = "(\<Sum>k\<in>keys. \<P>(fst|OB) {(k, obs)} * log b (\<P>(fst|OB) {(k, obs)})) :: real"
-  let "?Ht obs" = "(\<Sum>k\<in>keys. \<P>(fst|t\<circ>OB) {(k, obs)} * log b (\<P>(fst|t\<circ>OB) {(k, obs)})) :: real"
+  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 = (\<Sum>k\<in>keys. \<P>(fst|t\<circ>OB) {(k, t obs)} * log b (\<P>(fst|t\<circ>OB) {(k, t obs)}))"```