avoid undeclared variables in let bindings;
authorwenzelm
Tue Feb 28 21:53:36 2012 +0100 (2012-02-28)
changeset 467315302e932d1e5
parent 46730 e3b99d0231bc
child 46735 c8ec1958f822
avoid undeclared variables in let bindings;
tuned proofs;
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Complete_Measure.thy
src/HOL/Probability/Conditional_Probability.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Independent_Family.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Measure.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Probability/ex/Dining_Cryptographers.thy
src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
     1.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Tue Feb 28 20:20:09 2012 +0100
     1.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue Feb 28 21:53:36 2012 +0100
     1.3 @@ -170,7 +170,7 @@
     1.4    assumes Q: "Q \<in> sets P"
     1.5    shows "(\<lambda>(x,y). (y, x)) -` Q \<in> sets (M2 \<Otimes>\<^isub>M M1)" (is "_ \<in> sets ?Q")
     1.6  proof -
     1.7 -  let "?f Q" = "(\<lambda>(x,y). (y, x)) -` Q \<inter> space M2 \<times> space M1"
     1.8 +  let ?f = "\<lambda>Q. (\<lambda>(x,y). (y, x)) -` Q \<inter> space M2 \<times> space M1"
     1.9    have *: "(\<lambda>(x,y). (y, x)) -` Q = ?f Q"
    1.10      using sets_into_space[OF Q] by (auto simp: space_pair_measure)
    1.11    have "sets (M2 \<Otimes>\<^isub>M M1) = sets (sigma (pair_measure_generator M2 M1))"
    1.12 @@ -325,7 +325,7 @@
    1.13    have M1: "sigma_finite_measure M1" by default
    1.14    from M2.disjoint_sigma_finite guess F .. note F = this
    1.15    then have F_sets: "\<And>i. F i \<in> sets M2" by auto
    1.16 -  let "?C x i" = "F i \<inter> Pair x -` Q"
    1.17 +  let ?C = "\<lambda>x i. F i \<inter> Pair x -` Q"
    1.18    { fix i
    1.19      let ?R = "M2.restricted_space (F i)"
    1.20      have [simp]: "space M1 \<times> F i \<inter> space M1 \<times> space M2 = space M1 \<times> F i"
    1.21 @@ -607,8 +607,8 @@
    1.22  proof -
    1.23    have f_borel: "f \<in> borel_measurable P"
    1.24      using f(1) by (rule borel_measurable_simple_function)
    1.25 -  let "?F z" = "f -` {z} \<inter> space P"
    1.26 -  let "?F' x z" = "Pair x -` ?F z"
    1.27 +  let ?F = "\<lambda>z. f -` {z} \<inter> space P"
    1.28 +  let ?F' = "\<lambda>x z. Pair x -` ?F z"
    1.29    { fix x assume "x \<in> space M1"
    1.30      have [simp]: "\<And>z y. indicator (?F z) (x, y) = indicator (?F' x z) y"
    1.31        by (auto simp: indicator_def)
    1.32 @@ -819,7 +819,7 @@
    1.33    shows "M1.almost_everywhere (\<lambda>x. integrable M2 (\<lambda> y. f (x, y)))" (is "?AE")
    1.34      and "(\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>L P f" (is "?INT")
    1.35  proof -
    1.36 -  let "?pf x" = "ereal (f x)" and "?nf x" = "ereal (- f x)"
    1.37 +  let ?pf = "\<lambda>x. ereal (f x)" and ?nf = "\<lambda>x. ereal (- f x)"
    1.38    have
    1.39      borel: "?nf \<in> borel_measurable P""?pf \<in> borel_measurable P" and
    1.40      int: "integral\<^isup>P P ?nf \<noteq> \<infinity>" "integral\<^isup>P P ?pf \<noteq> \<infinity>"
     2.1 --- a/src/HOL/Probability/Borel_Space.thy	Tue Feb 28 20:20:09 2012 +0100
     2.2 +++ b/src/HOL/Probability/Borel_Space.thy	Tue Feb 28 21:53:36 2012 +0100
     2.3 @@ -521,7 +521,8 @@
     2.4      finally show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
     2.5        apply (simp only:)
     2.6        apply (safe intro!: countable_UN Diff)
     2.7 -      by (auto simp: sets_sigma intro!: sigma_sets.Basic)
     2.8 +      apply (auto simp: sets_sigma intro!: sigma_sets.Basic)
     2.9 +      done
    2.10    next
    2.11      fix a i assume "\<not> i < DIM('a)"
    2.12      then show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
    2.13 @@ -556,7 +557,8 @@
    2.14      finally show "{x. a \<le> x$$i} \<in> sets ?SIGMA"
    2.15        apply (simp only:)
    2.16        apply (safe intro!: countable_UN Diff)
    2.17 -      by (auto simp: sets_sigma intro!: sigma_sets.Basic)
    2.18 +      apply (auto simp: sets_sigma intro!: sigma_sets.Basic)
    2.19 +      done
    2.20    next
    2.21      fix a i assume "\<not> i < DIM('a)"
    2.22      then show "{x. a \<le> x$$i} \<in> sets ?SIGMA"
    2.23 @@ -653,7 +655,8 @@
    2.24        have "M \<in> sets ?SIGMA"
    2.25          apply (subst open_UNION[OF `open M`])
    2.26          apply (safe intro!: countable_UN)
    2.27 -        by (auto simp add: sigma_def intro!: sigma_sets.Basic) }
    2.28 +        apply (auto simp add: sigma_def intro!: sigma_sets.Basic)
    2.29 +        done }
    2.30      then show ?thesis
    2.31        unfolding borel_def by (intro sets_sigma_subset) auto
    2.32    qed
    2.33 @@ -1156,7 +1159,7 @@
    2.34    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"
    2.35    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
    2.36    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
    2.37 -  let "?f x" = "if f x = \<infinity> then \<infinity> else if f x = -\<infinity> then -\<infinity> else ereal (real (f x))"
    2.38 +  let ?f = "\<lambda>x. if f x = \<infinity> then \<infinity> else if f x = -\<infinity> then -\<infinity> else ereal (real (f x))"
    2.39    have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto
    2.40    also have "?f = f" by (auto simp: fun_eq_iff ereal_real)
    2.41    finally show "f \<in> borel_measurable M" .
    2.42 @@ -1469,7 +1472,7 @@
    2.43    shows "u' \<in> borel_measurable M"
    2.44  proof -
    2.45    have "\<And>x. x \<in> space M \<Longrightarrow> liminf (\<lambda>n. ereal (u n x)) = ereal (u' x)"
    2.46 -    using u' by (simp add: lim_imp_Liminf trivial_limit_sequentially lim_ereal)
    2.47 +    using u' by (simp add: lim_imp_Liminf)
    2.48    moreover from u have "(\<lambda>x. liminf (\<lambda>n. ereal (u n x))) \<in> borel_measurable M"
    2.49      by auto
    2.50    ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff)
     3.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue Feb 28 20:20:09 2012 +0100
     3.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Feb 28 21:53:36 2012 +0100
     3.3 @@ -223,7 +223,7 @@
     3.4      by (metis Diff_Un Un compl_sets lambda_system_sets xl yl)
     3.5    moreover
     3.6    have "x \<union> y = space M - ((space M - x) \<inter> (space M - y))"
     3.7 -    by auto  (metis subsetD lambda_system_sets sets_into_space xl yl)+
     3.8 +    by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+
     3.9    ultimately show ?thesis
    3.10      by (metis lambda_system_Compl lambda_system_Int xl yl)
    3.11  qed
    3.12 @@ -666,7 +666,7 @@
    3.13                    (\<lambda>x. Inf (measure_set M f x))"
    3.14  proof (simp add: countably_subadditive_def, safe)
    3.15    fix A :: "nat \<Rightarrow> 'a set"
    3.16 -  let "?outer B" = "Inf (measure_set M f B)"
    3.17 +  let ?outer = "\<lambda>B. Inf (measure_set M f B)"
    3.18    assume A: "range A \<subseteq> Pow (space M)"
    3.19       and disj: "disjoint_family A"
    3.20       and sb: "(\<Union>i. A i) \<subseteq> space M"
     4.1 --- a/src/HOL/Probability/Complete_Measure.thy	Tue Feb 28 20:20:09 2012 +0100
     4.2 +++ b/src/HOL/Probability/Complete_Measure.thy	Tue Feb 28 21:53:36 2012 +0100
     4.3 @@ -203,7 +203,7 @@
     4.4    assumes f: "simple_function completion f"
     4.5    shows "\<exists>f'. simple_function M f' \<and> (AE x. f x = f' x)"
     4.6  proof -
     4.7 -  let "?F x" = "f -` {x} \<inter> space M"
     4.8 +  let ?F = "\<lambda>x. f -` {x} \<inter> space M"
     4.9    have F: "\<And>x. ?F x \<in> sets completion" and fin: "finite (f`space M)"
    4.10      using completion.simple_functionD[OF f]
    4.11        completion.simple_functionD[OF f] by simp_all
    4.12 @@ -211,7 +211,8 @@
    4.13      using F null_part by auto
    4.14    from choice[OF this] obtain N where
    4.15      N: "\<And>x. null_part (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets" by auto
    4.16 -  let ?N = "\<Union>x\<in>f`space M. N x" let "?f' x" = "if x \<in> ?N then undefined else f x"
    4.17 +  let ?N = "\<Union>x\<in>f`space M. N x"
    4.18 +  let ?f' = "\<lambda>x. if x \<in> ?N then undefined else f x"
    4.19    have sets: "?N \<in> null_sets" using N fin by (intro nullsets.finite_UN) auto
    4.20    show ?thesis unfolding simple_function_def
    4.21    proof (safe intro!: exI[of _ ?f'])
     5.1 --- a/src/HOL/Probability/Conditional_Probability.thy	Tue Feb 28 20:20:09 2012 +0100
     5.2 +++ b/src/HOL/Probability/Conditional_Probability.thy	Tue Feb 28 21:53:36 2012 +0100
     5.3 @@ -25,8 +25,8 @@
     5.4    interpret P: prob_space N
     5.5      using prob_space_subalgebra[OF N] .
     5.6  
     5.7 -  let "?f A" = "\<lambda>x. X x * indicator A x"
     5.8 -  let "?Q A" = "integral\<^isup>P M (?f A)"
     5.9 +  let ?f = "\<lambda>A x. X x * indicator A x"
    5.10 +  let ?Q = "\<lambda>A. integral\<^isup>P M (?f A)"
    5.11  
    5.12    from measure_space_density[OF borel]
    5.13    have Q: "measure_space (N\<lparr> measure := ?Q \<rparr>)"
    5.14 @@ -146,7 +146,7 @@
    5.15      by auto
    5.16    from factorize_measurable_function_pos[OF assms(1,2) this] guess n .. note n = this
    5.17    from factorize_measurable_function_pos[OF assms Z] guess p .. note p = this
    5.18 -  let "?g x" = "p x - n x"
    5.19 +  let ?g = "\<lambda>x. p x - n x"
    5.20    show "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x)"
    5.21    proof (intro bexI ballI)
    5.22      show "?g \<in> borel_measurable M'" using p n by auto
     6.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Feb 28 20:20:09 2012 +0100
     6.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Feb 28 21:53:36 2012 +0100
     6.3 @@ -627,7 +627,7 @@
     6.4      by (intro P.measure_space_vimage[OF I']) (auto simp add: measure_preserving_def)
     6.5    show ?case
     6.6    proof (intro exI[of _ ?\<nu>] conjI ballI)
     6.7 -    let "?m A" = "measure (Pi\<^isub>M I M\<lparr>measure := \<nu>\<rparr> \<Otimes>\<^isub>M M i) (?h -` A \<inter> space P.P)"
     6.8 +    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)"
     6.9      { fix A assume A: "A \<in> (\<Pi> i\<in>insert i I. sets (M i))"
    6.10        then have *: "?h -` Pi\<^isub>E (insert i I) A \<inter> space P.P = Pi\<^isub>E I A \<times> A i"
    6.11          using `i \<notin> I` M.sets_into_space by (auto simp: space_pair_measure space_product_algebra) blast
    6.12 @@ -648,7 +648,7 @@
    6.13          "(\<Union>k. \<Pi>\<^isub>E j \<in> insert i I. F j k) = space I'.G"
    6.14          "\<And>k. \<And>j. j \<in> insert i I \<Longrightarrow> \<mu> j (F j k) \<noteq> \<infinity>"
    6.15          by blast+
    6.16 -      let "?F k" = "\<Pi>\<^isub>E j \<in> insert i I. F j k"
    6.17 +      let ?F = "\<lambda>k. \<Pi>\<^isub>E j \<in> insert i I. F j k"
    6.18        show "\<exists>F::nat \<Rightarrow> ('i \<Rightarrow> 'a) set. range F \<subseteq> sets I'.P \<and>
    6.19            (\<Union>i. F i) = (\<Pi>\<^isub>E i\<in>insert i I. space (M i)) \<and> (\<forall>i. ?m (F i) \<noteq> \<infinity>)"
    6.20        proof (intro exI[of _ ?F] conjI allI)
    6.21 @@ -727,7 +727,7 @@
    6.22    interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
    6.23    interpret P: pair_sigma_finite I.P J.P by default
    6.24    let ?g = "\<lambda>(x,y). merge I x J y"
    6.25 -  let "?X S" = "?g -` S \<inter> space P.P"
    6.26 +  let ?X = "\<lambda>S. ?g -` S \<inter> space P.P"
    6.27    from IJ.sigma_finite_pairs obtain F where
    6.28      F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
    6.29         "incseq (\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k)"
    6.30 @@ -839,7 +839,7 @@
    6.31      unfolding product_positive_integral_fold[OF IJ, unfolded insert, simplified, OF f]
    6.32    proof (rule I.positive_integral_cong, subst product_positive_integral_singleton)
    6.33      fix x assume x: "x \<in> space I.P"
    6.34 -    let "?f y" = "f (restrict (x(i := y)) (insert i I))"
    6.35 +    let ?f = "\<lambda>y. f (restrict (x(i := y)) (insert i I))"
    6.36      have f'_eq: "\<And>y. ?f y = f (x(i := y))"
    6.37        using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
    6.38      show "?f \<in> borel_measurable (M i)" unfolding f'_eq
    6.39 @@ -930,7 +930,7 @@
    6.40      unfolding product_integral_fold[OF IJ, simplified, OF f]
    6.41    proof (rule I.integral_cong, subst product_integral_singleton)
    6.42      fix x assume x: "x \<in> space I.P"
    6.43 -    let "?f y" = "f (restrict (x(i := y)) (insert i I))"
    6.44 +    let ?f = "\<lambda>y. f (restrict (x(i := y)) (insert i I))"
    6.45      have f'_eq: "\<And>y. ?f y = f (x(i := y))"
    6.46        using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
    6.47      have f: "f \<in> borel_measurable I'.P" using f unfolding integrable_def by auto
     7.1 --- a/src/HOL/Probability/Independent_Family.thy	Tue Feb 28 20:20:09 2012 +0100
     7.2 +++ b/src/HOL/Probability/Independent_Family.thy	Tue Feb 28 21:53:36 2012 +0100
     7.3 @@ -142,7 +142,7 @@
     7.4    with indep have "indep_sets F J"
     7.5      by (subst (asm) indep_sets_finite_index_sets) auto
     7.6    { fix J K assume "indep_sets F K"
     7.7 -    let "?G S i" = "if i \<in> S then ?F i else F i"
     7.8 +    let ?G = "\<lambda>S i. if i \<in> S then ?F i else F i"
     7.9      assume "finite J" "J \<subseteq> K"
    7.10      then have "indep_sets (?G J) K"
    7.11      proof induct
    7.12 @@ -384,7 +384,7 @@
    7.13    assumes disjoint: "disjoint_family_on I J"
    7.14    shows "indep_sets (\<lambda>j. sigma_sets (space M) (\<Union>i\<in>I j. E i)) J"
    7.15  proof -
    7.16 -  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) }"
    7.17 +  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) }"
    7.18  
    7.19    from indep have E: "\<And>j i. j \<in> J \<Longrightarrow> i \<in> I j \<Longrightarrow> E i \<subseteq> events"
    7.20      unfolding indep_sets_def by auto
    7.21 @@ -447,7 +447,7 @@
    7.22            with * L_inj show "k = j" by auto
    7.23          qed (insert *, simp) }
    7.24        note k_simp[simp] = this
    7.25 -      let "?E' l" = "E' (k l) l"
    7.26 +      let ?E' = "\<lambda>l. E' (k l) l"
    7.27        have "prob (\<Inter>j\<in>K. A j) = prob (\<Inter>l\<in>(\<Union>k\<in>K. L k). ?E' l)"
    7.28          by (auto simp: A intro!: arg_cong[where f=prob])
    7.29        also have "\<dots> = (\<Prod>l\<in>(\<Union>k\<in>K. L k). prob (?E' l))"
    7.30 @@ -658,7 +658,7 @@
    7.31      fix i show "Int_stable \<lparr>space = space M, sets = {F i}\<rparr>"
    7.32        unfolding Int_stable_def by simp
    7.33    qed
    7.34 -  let "?Q n" = "\<Union>i\<in>{n..}. F i"
    7.35 +  let ?Q = "\<lambda>n. \<Union>i\<in>{n..}. F i"
    7.36    show "(\<Inter>n. \<Union>m\<in>{n..}. F m) \<in> terminal_events (\<lambda>i. sigma_sets (space M) {F i})"
    7.37      unfolding terminal_events_def
    7.38    proof
    7.39 @@ -691,7 +691,7 @@
    7.40    proof (rule indep_setsI[OF F(1)])
    7.41      fix A J assume J: "J \<noteq> {}" "J \<subseteq> I" "finite J"
    7.42      assume A: "\<forall>j\<in>J. A j \<in> F j"
    7.43 -    let "?A j" = "if j \<in> J then A j else space M"
    7.44 +    let ?A = "\<lambda>j. if j \<in> J then A j else space M"
    7.45      have "prob (\<Inter>j\<in>I. ?A j) = prob (\<Inter>j\<in>J. A j)"
    7.46        using subset_trans[OF F(1) space_closed] J A
    7.47        by (auto intro!: arg_cong[where f=prob] split: split_if_asm) blast
     8.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Feb 28 20:20:09 2012 +0100
     8.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Feb 28 21:53:36 2012 +0100
     8.3 @@ -52,7 +52,7 @@
     8.4    from J.sigma_finite_pairs guess F .. note F = this
     8.5    then have [simp,intro]: "\<And>k i. k \<in> J \<Longrightarrow> F k i \<in> sets (M k)"
     8.6      by auto
     8.7 -  let "?F i" = "\<Pi>\<^isub>E k\<in>J. F k i"
     8.8 +  let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. F k i"
     8.9    let ?J = "product_algebra_generator J M \<lparr> measure := measure (Pi\<^isub>M J M) \<rparr>"
    8.10    have "?R \<in> measure_preserving (\<Pi>\<^isub>M i\<in>K. M i) (sigma ?J)"
    8.11    proof (rule K.measure_preserving_Int_stable)
    8.12 @@ -448,7 +448,7 @@
    8.13        "K - J \<noteq> {}" "K - J \<subseteq> I" "\<mu>G Z = measure (Pi\<^isub>M K M) X"
    8.14        by (auto simp: subset_insertI)
    8.15  
    8.16 -    let "?M y" = "merge J y (K - J) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M)"
    8.17 +    let ?M = "\<lambda>y. merge J y (K - J) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M)"
    8.18      { fix y assume y: "y \<in> space (Pi\<^isub>M J M)"
    8.19        note * = merge_emb[OF `K \<subseteq> I` `J \<subseteq> I` y, of X]
    8.20        moreover
    8.21 @@ -487,7 +487,7 @@
    8.22          by (intro KmJ.measure_le_1 merge_in_G(2)[OF x]) }
    8.23      note le_1 = this
    8.24  
    8.25 -    let "?q y" = "\<mu>G (merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M))"
    8.26 +    let ?q = "\<lambda>y. \<mu>G (merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M))"
    8.27      have "?q \<in> borel_measurable (Pi\<^isub>M J M)"
    8.28        unfolding `Z = emb I K X` using J K merge_in_G(3)
    8.29        by (simp add: merge_in_G  \<mu>G_eq measure_fold_measurable
    8.30 @@ -536,15 +536,15 @@
    8.31          using \<mu>G_spec[of "J 0" "A 0" "X 0"] J A_eq
    8.32          by (auto intro!: INF_lower2[of 0] J.measure_le_1)
    8.33  
    8.34 -      let "?M K Z y" = "merge K y (I - K) -` Z \<inter> space (Pi\<^isub>M I M)"
    8.35 +      let ?M = "\<lambda>K Z y. merge K y (I - K) -` Z \<inter> space (Pi\<^isub>M I M)"
    8.36  
    8.37        { fix Z k assume Z: "range Z \<subseteq> sets ?G" "decseq Z" "\<forall>n. ?a / 2^k \<le> \<mu>G (Z n)"
    8.38          then have Z_sets: "\<And>n. Z n \<in> sets ?G" by auto
    8.39          fix J' assume J': "J' \<noteq> {}" "finite J'" "J' \<subseteq> I"
    8.40          interpret J': finite_product_prob_space M J' by default fact+
    8.41  
    8.42 -        let "?q n y" = "\<mu>G (?M J' (Z n) y)"
    8.43 -        let "?Q n" = "?q n -` {?a / 2^(k+1) ..} \<inter> space (Pi\<^isub>M J' M)"
    8.44 +        let ?q = "\<lambda>n y. \<mu>G (?M J' (Z n) y)"
    8.45 +        let ?Q = "\<lambda>n. ?q n -` {?a / 2^(k+1) ..} \<inter> space (Pi\<^isub>M J' M)"
    8.46          { fix n
    8.47            have "?q n \<in> borel_measurable (Pi\<^isub>M J' M)"
    8.48              using Z J' by (intro fold(1)) auto
    8.49 @@ -599,13 +599,14 @@
    8.50          then have "\<exists>w\<in>space (Pi\<^isub>M J' M). \<forall>n. ?a / 2 ^ (k + 1) \<le> ?q n w" by auto }
    8.51        note Ex_w = this
    8.52  
    8.53 -      let "?q k n y" = "\<mu>G (?M (J k) (A n) y)"
    8.54 +      let ?q = "\<lambda>k n y. \<mu>G (?M (J k) (A n) y)"
    8.55  
    8.56        have "\<forall>n. ?a / 2 ^ 0 \<le> \<mu>G (A n)" by (auto intro: INF_lower)
    8.57        from Ex_w[OF A(1,2) this J(1-3), of 0] guess w0 .. note w0 = this
    8.58  
    8.59 -      let "?P k wk w" =
    8.60 -        "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)"
    8.61 +      let ?P =
    8.62 +        "\<lambda>k wk w. w \<in> space (Pi\<^isub>M (J (Suc k)) M) \<and> restrict w (J k) = wk \<and>
    8.63 +          (\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> ?q (Suc k) n w)"
    8.64        def w \<equiv> "nat_rec w0 (\<lambda>k wk. Eps (?P k wk))"
    8.65  
    8.66        { fix k have w: "w k \<in> space (Pi\<^isub>M (J k) M) \<and>
    8.67 @@ -1015,7 +1016,7 @@
    8.68    fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)"
    8.69    shows "(\<lambda>n. \<Prod>i\<le>n. M.\<mu>' i (E i)) ----> \<mu>' (Pi UNIV E)"
    8.70  proof -
    8.71 -  let "?E n" = "emb UNIV {..n} (Pi\<^isub>E {.. n} E)"
    8.72 +  let ?E = "\<lambda>n. emb UNIV {..n} (Pi\<^isub>E {.. n} E)"
    8.73    { fix n :: nat
    8.74      interpret n: finite_product_prob_space M "{..n}" by default auto
    8.75      have "(\<Prod>i\<le>n. M.\<mu>' i (E i)) = n.\<mu>' (Pi\<^isub>E {.. n} E)"
     9.1 --- a/src/HOL/Probability/Information.thy	Tue Feb 28 20:20:09 2012 +0100
     9.2 +++ b/src/HOL/Probability/Information.thy	Tue Feb 28 21:53:36 2012 +0100
     9.3 @@ -748,8 +748,8 @@
     9.4  proof -
     9.5    interpret MX: finite_prob_space "MX\<lparr>measure := ereal\<circ>distribution X\<rparr>"
     9.6      using MX by (rule distribution_finite_prob_space)
     9.7 -  let "?X x" = "distribution X {x}"
     9.8 -  let "?XX x y" = "joint_distribution X X {(x, y)}"
     9.9 +  let ?X = "\<lambda>x. distribution X {x}"
    9.10 +  let ?XX = "\<lambda>x y. joint_distribution X X {(x, y)}"
    9.11  
    9.12    { fix x y :: 'c
    9.13      { assume "x \<noteq> y"
    9.14 @@ -803,7 +803,7 @@
    9.15    assumes X: "simple_function M X"
    9.16    shows "\<H>(X) \<le> log b (card (X ` space M \<inter> {x. distribution X {x} \<noteq> 0}))"
    9.17  proof -
    9.18 -  let "?p x" = "distribution X {x}"
    9.19 +  let ?p = "\<lambda>x. distribution X {x}"
    9.20    have "\<H>(X) = (\<Sum>x\<in>X`space M. ?p x * log b (1 / ?p x))"
    9.21      unfolding entropy_eq[OF X] setsum_negf[symmetric]
    9.22      by (auto intro!: setsum_cong simp: log_simps)
    9.23 @@ -1117,10 +1117,10 @@
    9.24  proof -
    9.25    interpret MX: finite_sigma_algebra MX using MX by simp
    9.26    interpret MZ: finite_sigma_algebra MZ using MZ by simp
    9.27 -  let "?XXZ x y z" = "joint_distribution X (\<lambda>x. (X x, Z x)) {(x, y, z)}"
    9.28 -  let "?XZ x z" = "joint_distribution X Z {(x, z)}"
    9.29 -  let "?Z z" = "distribution Z {z}"
    9.30 -  let "?f x y z" = "log b (?XXZ x y z * ?Z z / (?XZ x z * ?XZ y z))"
    9.31 +  let ?XXZ = "\<lambda>x y z. joint_distribution X (\<lambda>x. (X x, Z x)) {(x, y, z)}"
    9.32 +  let ?XZ = "\<lambda>x z. joint_distribution X Z {(x, z)}"
    9.33 +  let ?Z = "\<lambda>z. distribution Z {z}"
    9.34 +  let ?f = "\<lambda>x y z. log b (?XXZ x y z * ?Z z / (?XZ x z * ?XZ y z))"
    9.35    { fix x z have "?XXZ x x z = ?XZ x z"
    9.36        unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>']) }
    9.37    note this[simp]
    9.38 @@ -1183,9 +1183,9 @@
    9.39    assumes X: "simple_function M X" and Z: "simple_function M Z"
    9.40    shows  "\<I>(X ; Z) = \<H>(X) - \<H>(X | Z)"
    9.41  proof -
    9.42 -  let "?XZ x z" = "joint_distribution X Z {(x, z)}"
    9.43 -  let "?Z z" = "distribution Z {z}"
    9.44 -  let "?X x" = "distribution X {x}"
    9.45 +  let ?XZ = "\<lambda>x z. joint_distribution X Z {(x, z)}"
    9.46 +  let ?Z = "\<lambda>z. distribution Z {z}"
    9.47 +  let ?X = "\<lambda>x. distribution X {x}"
    9.48    note fX = X[THEN simple_function_imp_finite_random_variable]
    9.49    note fZ = Z[THEN simple_function_imp_finite_random_variable]
    9.50    note finite_distribution_order[OF fX fZ, simp]
    9.51 @@ -1214,9 +1214,9 @@
    9.52    assumes X: "simple_function M X" and Y: "simple_function M Y"
    9.53    shows  "\<H>(\<lambda>x. (X x, Y x)) = \<H>(X) + \<H>(Y|X)"
    9.54  proof -
    9.55 -  let "?XY x y" = "joint_distribution X Y {(x, y)}"
    9.56 -  let "?Y y" = "distribution Y {y}"
    9.57 -  let "?X x" = "distribution X {x}"
    9.58 +  let ?XY = "\<lambda>x y. joint_distribution X Y {(x, y)}"
    9.59 +  let ?Y = "\<lambda>y. distribution Y {y}"
    9.60 +  let ?X = "\<lambda>x. distribution X {x}"
    9.61    note fX = X[THEN simple_function_imp_finite_random_variable]
    9.62    note fY = Y[THEN simple_function_imp_finite_random_variable]
    9.63    note finite_distribution_order[OF fX fY, simp]
    9.64 @@ -1352,9 +1352,9 @@
    9.65    assumes svi: "subvimage (space M) X P"
    9.66    shows "\<H>(X) = \<H>(P) + \<H>(X|P)"
    9.67  proof -
    9.68 -  let "?XP x p" = "joint_distribution X P {(x, p)}"
    9.69 -  let "?X x" = "distribution X {x}"
    9.70 -  let "?P p" = "distribution P {p}"
    9.71 +  let ?XP = "\<lambda>x p. joint_distribution X P {(x, p)}"
    9.72 +  let ?X = "\<lambda>x. distribution X {x}"
    9.73 +  let ?P = "\<lambda>p. distribution P {p}"
    9.74    note fX = sf(1)[THEN simple_function_imp_finite_random_variable]
    9.75    note fP = sf(2)[THEN simple_function_imp_finite_random_variable]
    9.76    note finite_distribution_order[OF fX fP, simp]
    10.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Tue Feb 28 20:20:09 2012 +0100
    10.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Feb 28 21:53:36 2012 +0100
    10.3 @@ -331,7 +331,7 @@
    10.4      "\<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)))"
    10.5      unfolding f_def by auto
    10.6  
    10.7 -  let "?g j x" = "real (f x j) / 2^j :: ereal"
    10.8 +  let ?g = "\<lambda>j x. real (f x j) / 2^j :: ereal"
    10.9    show ?thesis
   10.10    proof (intro exI[of _ ?g] conjI allI ballI)
   10.11      fix i
   10.12 @@ -567,7 +567,7 @@
   10.13    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)"
   10.14      (is "_ = setsum _ (?p ` space M)")
   10.15  proof-
   10.16 -  let "?sub x" = "?p ` (f -` {x} \<inter> space M)"
   10.17 +  let ?sub = "\<lambda>x. ?p ` (f -` {x} \<inter> space M)"
   10.18    let ?SIGMA = "Sigma (f`space M) ?sub"
   10.19  
   10.20    have [intro]:
   10.21 @@ -659,7 +659,7 @@
   10.22    and mono: "AE x. f x \<le> g x"
   10.23    shows "integral\<^isup>S M f \<le> integral\<^isup>S M g"
   10.24  proof -
   10.25 -  let "?S x" = "(g -` {g x} \<inter> space M) \<inter> (f -` {f x} \<inter> space M)"
   10.26 +  let ?S = "\<lambda>x. (g -` {g x} \<inter> space M) \<inter> (f -` {f x} \<inter> space M)"
   10.27    have *: "\<And>x. g -` {g x} \<inter> f -` {f x} \<inter> space M = ?S x"
   10.28      "\<And>x. f -` {f x} \<inter> g -` {g x} \<inter> space M = ?S x" by auto
   10.29    show ?thesis
   10.30 @@ -899,7 +899,7 @@
   10.31    let ?G = "{x \<in> space M. \<not> g x \<noteq> \<infinity>}"
   10.32    note gM = g(1)[THEN borel_measurable_simple_function]
   10.33    have \<mu>G_pos: "0 \<le> \<mu> ?G" using gM by auto
   10.34 -  let "?g y x" = "if g x = \<infinity> then y else max 0 (g x)"
   10.35 +  let ?g = "\<lambda>y x. if g x = \<infinity> then y else max 0 (g x)"
   10.36    from g gM have g_in_A: "\<And>y. 0 \<le> y \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> ?g y \<in> ?A"
   10.37      apply (safe intro!: simple_function_max simple_function_If)
   10.38      apply (force simp: max_def le_fun_def split: split_if_asm)+
   10.39 @@ -941,7 +941,7 @@
   10.40    fix n assume n: "simple_function M n" "n \<le> max 0 \<circ> u"
   10.41    from ae[THEN AE_E] guess N . note N = this
   10.42    then have ae_N: "AE x. x \<notin> N" by (auto intro: AE_not_in)
   10.43 -  let "?n x" = "n x * indicator (space M - N) x"
   10.44 +  let ?n = "\<lambda>x. n x * indicator (space M - N) x"
   10.45    have "AE x. n x \<le> ?n x" "simple_function M ?n"
   10.46      using n N ae_N by auto
   10.47    moreover
   10.48 @@ -974,7 +974,7 @@
   10.49  lemma (in measure_space) positive_integral_eq_simple_integral:
   10.50    assumes f: "simple_function M f" "\<And>x. 0 \<le> f x" shows "integral\<^isup>P M f = integral\<^isup>S M f"
   10.51  proof -
   10.52 -  let "?f x" = "f x * indicator (space M) x"
   10.53 +  let ?f = "\<lambda>x. f x * indicator (space M) x"
   10.54    have f': "simple_function M ?f" using f by auto
   10.55    with f(2) have [simp]: "max 0 \<circ> ?f = ?f"
   10.56      by (auto simp: fun_eq_iff max_def split: split_indicator)
   10.57 @@ -1010,11 +1010,11 @@
   10.58      using u(3) by auto
   10.59    fix a :: ereal assume "0 < a" "a < 1"
   10.60    hence "a \<noteq> 0" by auto
   10.61 -  let "?B i" = "{x \<in> space M. a * u x \<le> f i x}"
   10.62 +  let ?B = "\<lambda>i. {x \<in> space M. a * u x \<le> f i x}"
   10.63    have B: "\<And>i. ?B i \<in> sets M"
   10.64      using f `simple_function M u` by (auto simp: borel_measurable_simple_function)
   10.65  
   10.66 -  let "?uB i x" = "u x * indicator (?B i) x"
   10.67 +  let ?uB = "\<lambda>i x. u x * indicator (?B i) x"
   10.68  
   10.69    { fix i have "?B i \<subseteq> ?B (Suc i)"
   10.70      proof safe
   10.71 @@ -1027,7 +1027,7 @@
   10.72  
   10.73    note B_u = Int[OF u(1)[THEN simple_functionD(2)] B]
   10.74  
   10.75 -  let "?B' i n" = "(u -` {i} \<inter> space M) \<inter> ?B n"
   10.76 +  let ?B' = "\<lambda>i n. (u -` {i} \<inter> space M) \<inter> ?B n"
   10.77    have measure_conv: "\<And>i. \<mu> (u -` {i} \<inter> space M) = (SUP n. \<mu> (?B' i n))"
   10.78    proof -
   10.79      fix i
   10.80 @@ -1126,7 +1126,7 @@
   10.81    from f have "AE x. \<forall>i. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x"
   10.82      by (simp add: AE_all_countable)
   10.83    from this[THEN AE_E] guess N . note N = this
   10.84 -  let "?f i x" = "if x \<in> space M - N then f i x else 0"
   10.85 +  let ?f = "\<lambda>i x. if x \<in> space M - N then f i x else 0"
   10.86    have f_eq: "AE x. \<forall>i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ N])
   10.87    then have "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) = (\<integral>\<^isup>+ x. (SUP i. ?f i x) \<partial>M)"
   10.88      by (auto intro!: positive_integral_cong_AE)
   10.89 @@ -1202,7 +1202,7 @@
   10.90    interpret T: measure_space M' by (rule measure_space_vimage[OF T])
   10.91    from T.borel_measurable_implies_simple_function_sequence'[OF f]
   10.92    guess f' . note f' = this
   10.93 -  let "?f i x" = "f' i (T x)"
   10.94 +  let ?f = "\<lambda>i x. f' i (T x)"
   10.95    have inc: "incseq ?f" using f' by (force simp: le_fun_def incseq_def)
   10.96    have sup: "\<And>x. (SUP i. ?f i x) = max 0 (f (T x))"
   10.97      using f'(4) .
   10.98 @@ -1225,7 +1225,7 @@
   10.99    note u = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
  10.100    from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess v .
  10.101    note v = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
  10.102 -  let "?L' i x" = "a * u i x + v i x"
  10.103 +  let ?L' = "\<lambda>i x. a * u i x + v i x"
  10.104  
  10.105    have "?L \<in> borel_measurable M" using assms by auto
  10.106    from borel_measurable_implies_simple_function_sequence'[OF this] guess l .
  10.107 @@ -1494,7 +1494,7 @@
  10.108    from G(4) g(2) have G_M': "AE x in M'. (SUP i. G i x) = g x"
  10.109      by (auto intro!: ac split: split_max)
  10.110    { fix i
  10.111 -    let "?I y x" = "indicator (G i -` {y} \<inter> space M) x"
  10.112 +    let ?I = "\<lambda>y x. indicator (G i -` {y} \<inter> space M) x"
  10.113      { fix x assume *: "x \<in> space M" "0 \<le> f x" "0 \<le> g x"
  10.114        then have [simp]: "G i ` space M \<inter> {y. G i x = y \<and> x \<in> space M} = {G i x}" by auto
  10.115        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))"
  10.116 @@ -1546,7 +1546,7 @@
  10.117        then have "0 \<le> r" by (auto simp add: ereal_zero_less_0_iff) }
  10.118      note gt_1 = this
  10.119      assume *: "integral\<^isup>P M u = 0"
  10.120 -    let "?M n" = "{x \<in> space M. 1 \<le> real (n::nat) * u x}"
  10.121 +    let ?M = "\<lambda>n. {x \<in> space M. 1 \<le> real (n::nat) * u x}"
  10.122      have "0 = (SUP n. \<mu> (?M n \<inter> ?A))"
  10.123      proof -
  10.124        { fix n :: nat
  10.125 @@ -1618,7 +1618,7 @@
  10.126  proof -
  10.127    interpret R: measure_space ?R
  10.128      by (rule restricted_measure_space) fact
  10.129 -  let "?I g x" = "g x * indicator A x :: ereal"
  10.130 +  let ?I = "\<lambda>g x. g x * indicator A x :: ereal"
  10.131    show ?thesis
  10.132      unfolding positive_integral_def
  10.133      unfolding simple_function_restricted[OF A]
  10.134 @@ -1846,10 +1846,10 @@
  10.135    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"
  10.136    shows "integrable M f" and "integral\<^isup>L M f = integral\<^isup>L M u - integral\<^isup>L M v"
  10.137  proof -
  10.138 -  let "?f x" = "max 0 (ereal (f x))"
  10.139 -  let "?mf x" = "max 0 (ereal (- f x))"
  10.140 -  let "?u x" = "max 0 (ereal (u x))"
  10.141 -  let "?v x" = "max 0 (ereal (v x))"
  10.142 +  let ?f = "\<lambda>x. max 0 (ereal (f x))"
  10.143 +  let ?mf = "\<lambda>x. max 0 (ereal (- f x))"
  10.144 +  let ?u = "\<lambda>x. max 0 (ereal (u x))"
  10.145 +  let ?v = "\<lambda>x. max 0 (ereal (v x))"
  10.146  
  10.147    from borel_measurable_diff[of u v] integrable
  10.148    have f_borel: "?f \<in> borel_measurable M" and
  10.149 @@ -1886,12 +1886,12 @@
  10.150    shows "integrable M (\<lambda>t. a * f t + g t)"
  10.151    and "(\<integral> t. a * f t + g t \<partial>M) = a * integral\<^isup>L M f + integral\<^isup>L M g" (is ?EQ)
  10.152  proof -
  10.153 -  let "?f x" = "max 0 (ereal (f x))"
  10.154 -  let "?g x" = "max 0 (ereal (g x))"
  10.155 -  let "?mf x" = "max 0 (ereal (- f x))"
  10.156 -  let "?mg x" = "max 0 (ereal (- g x))"
  10.157 -  let "?p t" = "max 0 (a * f t) + max 0 (g t)"
  10.158 -  let "?n t" = "max 0 (- (a * f t)) + max 0 (- g t)"
  10.159 +  let ?f = "\<lambda>x. max 0 (ereal (f x))"
  10.160 +  let ?g = "\<lambda>x. max 0 (ereal (g x))"
  10.161 +  let ?mf = "\<lambda>x. max 0 (ereal (- f x))"
  10.162 +  let ?mg = "\<lambda>x. max 0 (ereal (- g x))"
  10.163 +  let ?p = "\<lambda>t. max 0 (a * f t) + max 0 (g t)"
  10.164 +  let ?n = "\<lambda>t. max 0 (- (a * f t)) + max 0 (- g t)"
  10.165  
  10.166    from assms have linear:
  10.167      "(\<integral>\<^isup>+ x. ereal a * ?f x + ?g x \<partial>M) = ereal a * integral\<^isup>P M ?f + integral\<^isup>P M ?g"
  10.168 @@ -2353,7 +2353,7 @@
  10.169      show "\<bar>u' x\<bar> \<le> w x" using u'_bound[OF x] .
  10.170    qed
  10.171  
  10.172 -  let "?diff n x" = "2 * w x - \<bar>u n x - u' x\<bar>"
  10.173 +  let ?diff = "\<lambda>n x. 2 * w x - \<bar>u n x - u' x\<bar>"
  10.174    have diff: "\<And>n. integrable M (\<lambda>x. \<bar>u n x - u' x\<bar>)"
  10.175      using w u `integrable M u'`
  10.176      by (auto intro!: integral_add integral_diff integral_cmult integrable_abs)
  10.177 @@ -2468,7 +2468,7 @@
  10.178    from bchoice[OF this]
  10.179    obtain w where w: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. \<bar>f i x\<bar>) sums w x" by auto
  10.180  
  10.181 -  let "?w y" = "if y \<in> space M then w y else 0"
  10.182 +  let ?w = "\<lambda>y. if y \<in> space M then w y else 0"
  10.183  
  10.184    obtain x where abs_sum: "(\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M)) sums x"
  10.185      using sums unfolding summable_def ..
  10.186 @@ -2484,8 +2484,8 @@
  10.187  
  10.188    have 3: "integrable M ?w"
  10.189    proof (rule integral_monotone_convergence(1))
  10.190 -    let "?F n y" = "(\<Sum>i = 0..<n. \<bar>f i y\<bar>)"
  10.191 -    let "?w' n y" = "if y \<in> space M then ?F n y else 0"
  10.192 +    let ?F = "\<lambda>n y. (\<Sum>i = 0..<n. \<bar>f i y\<bar>)"
  10.193 +    let ?w' = "\<lambda>n y. if y \<in> space M then ?F n y else 0"
  10.194      have "\<And>n. integrable M (?F n)"
  10.195        using borel by (auto intro!: integral_setsum integrable_abs)
  10.196      thus "\<And>n. integrable M (?w' n)" by (simp cong: integrable_cong)
  10.197 @@ -2522,8 +2522,8 @@
  10.198    shows "integrable M f"
  10.199    and "(\<lambda>r. enum r * real (\<mu> (f -` {enum r} \<inter> space M))) sums integral\<^isup>L M f" (is ?sums)
  10.200  proof -
  10.201 -  let "?A r" = "f -` {enum r} \<inter> space M"
  10.202 -  let "?F r x" = "enum r * indicator (?A r) x"
  10.203 +  let ?A = "\<lambda>r. f -` {enum r} \<inter> space M"
  10.204 +  let ?F = "\<lambda>r x. enum r * indicator (?A r) x"
  10.205    have enum_eq: "\<And>r. enum r * real (\<mu> (?A r)) = integral\<^isup>L M (?F r)"
  10.206      using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator)
  10.207  
  10.208 @@ -2579,8 +2579,8 @@
  10.209    and "(\<integral>x. f x \<partial>M) =
  10.210      (\<Sum> r \<in> f`space M. r * real (\<mu> (f -` {r} \<inter> space M)))" (is "?integral")
  10.211  proof -
  10.212 -  let "?A r" = "f -` {r} \<inter> space M"
  10.213 -  let "?S x" = "\<Sum>r\<in>f`space M. r * indicator (?A r) x"
  10.214 +  let ?A = "\<lambda>r. f -` {r} \<inter> space M"
  10.215 +  let ?S = "\<lambda>x. \<Sum>r\<in>f`space M. r * indicator (?A r) x"
  10.216  
  10.217    { fix x assume "x \<in> space M"
  10.218      have "f x = (\<Sum>r\<in>f`space M. if x \<in> ?A r then r else 0)"
    11.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Tue Feb 28 20:20:09 2012 +0100
    11.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Feb 28 21:53:36 2012 +0100
    11.3 @@ -133,8 +133,8 @@
    11.4      fix A :: "nat \<Rightarrow> 'b set" assume rA: "range A \<subseteq> sets lebesgue" "disjoint_family A"
    11.5      then have A[simp, intro]: "\<And>i n. (indicator (A i) :: _ \<Rightarrow> real) integrable_on cube n"
    11.6        by (auto dest: lebesgueD)
    11.7 -    let "?m n i" = "integral (cube n) (indicator (A i) :: _\<Rightarrow>real)"
    11.8 -    let "?M n I" = "integral (cube n) (indicator (\<Union>i\<in>I. A i) :: _\<Rightarrow>real)"
    11.9 +    let ?m = "\<lambda>n i. integral (cube n) (indicator (A i) :: _\<Rightarrow>real)"
   11.10 +    let ?M = "\<lambda>n I. integral (cube n) (indicator (\<Union>i\<in>I. A i) :: _\<Rightarrow>real)"
   11.11      have nn[simp, intro]: "\<And>i n. 0 \<le> ?m n i" by (auto intro!: integral_nonneg)
   11.12      assume "(\<Union>i. A i) \<in> sets lebesgue"
   11.13      then have UN_A[simp, intro]: "\<And>i n. (indicator (\<Union>i. A i) :: _ \<Rightarrow> real) integrable_on cube n"
   11.14 @@ -560,8 +560,8 @@
   11.15    shows "((\<lambda>x. real (f x)) has_integral (real (integral\<^isup>S lebesgue f))) UNIV"
   11.16    unfolding simple_integral_def space_lebesgue
   11.17  proof (subst lebesgue_simple_function_indicator)
   11.18 -  let "?M x" = "lebesgue.\<mu> (f -` {x} \<inter> UNIV)"
   11.19 -  let "?F x" = "indicator (f -` {x})"
   11.20 +  let ?M = "\<lambda>x. lebesgue.\<mu> (f -` {x} \<inter> UNIV)"
   11.21 +  let ?F = "\<lambda>x. indicator (f -` {x})"
   11.22    { fix x y assume "y \<in> range f"
   11.23      from subsetD[OF f' this] have "y * ?F y x = ereal (real y * ?F y x)"
   11.24        by (cases rule: ereal2_cases[of y "?F y x"])
   11.25 @@ -637,7 +637,7 @@
   11.26    guess u . note u = this
   11.27    have SUP_eq: "\<And>x. (SUP i. u i x) = f x"
   11.28      using u(4) f(2)[THEN subsetD] by (auto split: split_max)
   11.29 -  let "?u i x" = "real (u i x)"
   11.30 +  let ?u = "\<lambda>i x. real (u i x)"
   11.31    note u_eq = lebesgue.positive_integral_eq_simple_integral[OF u(1,5), symmetric]
   11.32    { fix i
   11.33      note u_eq
   11.34 @@ -986,7 +986,7 @@
   11.35      (is "_ = ?\<nu> X")
   11.36  proof -
   11.37    let ?E = "\<lparr>space = UNIV, sets = range (\<lambda>(a,b). {a::real .. b})\<rparr> :: real algebra"
   11.38 -  let "?M \<nu>" = "\<lparr>space = space ?E, sets = sets (sigma ?E), measure = \<nu>\<rparr> :: real measure_space"
   11.39 +  let ?M = "\<lambda>\<nu>. \<lparr>space = space ?E, sets = sets (sigma ?E), measure = \<nu>\<rparr> :: real measure_space"
   11.40    have *: "?M (measure lebesgue) = lborel"
   11.41      unfolding borel_eq_atLeastAtMost[symmetric]
   11.42      by (simp add: lborel_def lebesgue_def)
    12.1 --- a/src/HOL/Probability/Measure.thy	Tue Feb 28 20:20:09 2012 +0100
    12.2 +++ b/src/HOL/Probability/Measure.thy	Tue Feb 28 21:53:36 2012 +0100
    12.3 @@ -439,7 +439,7 @@
    12.4    shows "\<mu> (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. \<mu> (A i))"
    12.5  using assms proof induct
    12.6    case (insert i I)
    12.7 -  then have "(\<Union>i\<in>I. A i) \<in> sets M" by (auto intro: finite_UN)
    12.8 +  then have "(\<Union>i\<in>I. A i) \<in> sets M" by auto
    12.9    then have "\<mu> (\<Union>i\<in>insert i I. A i) \<le> \<mu> (A i) + \<mu> (\<Union>i\<in>I. A i)"
   12.10      using insert by (simp add: measure_subadditive)
   12.11    also have "\<dots> \<le> (\<Sum>i\<in>insert i I. \<mu> (A i))"
   12.12 @@ -458,7 +458,7 @@
   12.13      by (simp add:  disjoint_family_disjointed comp_def)
   12.14    also have "\<dots> \<le> (\<Sum>i. \<mu> (f i))"
   12.15      using range_disjointed_sets[OF assms] assms
   12.16 -    by (auto intro!: suminf_le_pos measure_mono positive_measure disjointed_subset)
   12.17 +    by (auto intro!: suminf_le_pos measure_mono disjointed_subset)
   12.18    finally show ?thesis .
   12.19  qed
   12.20  
   12.21 @@ -509,7 +509,7 @@
   12.22    assumes "X \<in> sets (sigma E)"
   12.23    shows "\<mu> X = \<nu> X"
   12.24  proof -
   12.25 -  let "?D F" = "{D. D \<in> sets (sigma E) \<and> \<mu> (F \<inter> D) = \<nu> (F \<inter> D)}"
   12.26 +  let ?D = "\<lambda>F. {D. D \<in> sets (sigma E) \<and> \<mu> (F \<inter> D) = \<nu> (F \<inter> D)}"
   12.27    interpret M: measure_space ?M
   12.28      where "space ?M = space E" and "sets ?M = sets (sigma E)" and "measure ?M = \<mu>" by (simp_all add: M)
   12.29    interpret N: measure_space ?N
   12.30 @@ -559,7 +559,7 @@
   12.31      have "\<And>D. D \<in> sets (sigma E) \<Longrightarrow> \<mu> (F \<inter> D) = \<nu> (F \<inter> D)"
   12.32        by (subst (asm) *) auto }
   12.33    note * = this
   12.34 -  let "?A i" = "A i \<inter> X"
   12.35 +  let ?A = "\<lambda>i. A i \<inter> X"
   12.36    have A': "range ?A \<subseteq> sets (sigma E)" "incseq ?A"
   12.37      using A(1,2) `X \<in> sets (sigma E)` by (auto simp: incseq_def)
   12.38    { fix i have "\<mu> (?A i) = \<nu> (?A i)"
   12.39 @@ -1015,7 +1015,7 @@
   12.40  proof (rule measure_unique_Int_stable[OF E A(1,2,3) _ _ eq _ X])
   12.41    interpret M: measure_space M by fact
   12.42    interpret N: measure_space N by fact
   12.43 -  let "?T X" = "T -` X \<inter> space N"
   12.44 +  let ?T = "\<lambda>X. T -` X \<inter> space N"
   12.45    show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = measure M\<rparr>"
   12.46      by (rule M.measure_space_cong) (auto simp: M)
   12.47    show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = \<lambda>X. measure N (?T X)\<rparr>" (is "measure_space ?E")
   12.48 @@ -1397,7 +1397,7 @@
   12.49  
   12.50  lemma (in finite_measure_space) sum_over_space: "(\<Sum>x\<in>space M. \<mu> {x}) = \<mu> (space M)"
   12.51    using measure_setsum[of "space M" "\<lambda>i. {i}"]
   12.52 -  by (simp add: sets_eq_Pow disjoint_family_on_def finite_space)
   12.53 +  by (simp add: disjoint_family_on_def finite_space)
   12.54  
   12.55  lemma (in finite_measure_space) finite_measure_singleton:
   12.56    assumes A: "A \<subseteq> space M" shows "\<mu>' A = (\<Sum>x\<in>A. \<mu>' {x})"
    13.1 --- a/src/HOL/Probability/Probability_Measure.thy	Tue Feb 28 20:20:09 2012 +0100
    13.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Tue Feb 28 21:53:36 2012 +0100
    13.3 @@ -380,7 +380,7 @@
    13.4    assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q"
    13.5    shows "q (expectation X) \<le> expectation (\<lambda>x. q (X x))"
    13.6  proof -
    13.7 -  let "?F x" = "Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I))"
    13.8 +  let ?F = "\<lambda>x. Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I))"
    13.9    from not_empty X(2) have "I \<noteq> {}" by auto
   13.10  
   13.11    from I have "open I" by auto
   13.12 @@ -741,7 +741,7 @@
   13.13  proof (subst finite_measure_finite_Union[symmetric])
   13.14    interpret MX: finite_sigma_algebra MX using X by auto
   13.15    show "finite (space MX)" using MX.finite_space .
   13.16 -  let "?d i" = "(\<lambda>x. (X x, Y x)) -` ({i} \<times> B) \<inter> space M"
   13.17 +  let ?d = "\<lambda>i. (\<lambda>x. (X x, Y x)) -` ({i} \<times> B) \<inter> space M"
   13.18    { fix i assume "i \<in> space MX"
   13.19      moreover have "?d i = (X -` {i} \<inter> space M) \<inter> (Y -` B \<inter> space M)" by auto
   13.20      ultimately show "?d i \<in> events"
    14.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Feb 28 20:20:09 2012 +0100
    14.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Feb 28 21:53:36 2012 +0100
    14.3 @@ -17,7 +17,7 @@
    14.4      measure: "\<And>i. \<mu> (A i) \<noteq> \<infinity>" and
    14.5      disjoint: "disjoint_family A"
    14.6      using disjoint_sigma_finite by auto
    14.7 -  let "?B i" = "2^Suc i * \<mu> (A i)"
    14.8 +  let ?B = "\<lambda>i. 2^Suc i * \<mu> (A i)"
    14.9    have "\<forall>i. \<exists>x. 0 < x \<and> x < inverse (?B i)"
   14.10    proof
   14.11      fix i have Ai: "A i \<in> sets M" using range by auto
   14.12 @@ -28,7 +28,7 @@
   14.13    from choice[OF this] obtain n where n: "\<And>i. 0 < n i"
   14.14      "\<And>i. n i < inverse (2^Suc i * \<mu> (A i))" by auto
   14.15    { fix i have "0 \<le> n i" using n(1)[of i] by auto } note pos = this
   14.16 -  let "?h x" = "\<Sum>i. n i * indicator (A i) x"
   14.17 +  let ?h = "\<lambda>x. \<Sum>i. n i * indicator (A i) x"
   14.18    show ?thesis
   14.19    proof (safe intro!: bexI[of _ ?h] del: notI)
   14.20      have "\<And>i. A i \<in> sets M"
   14.21 @@ -132,8 +132,8 @@
   14.22                      (\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> - e < \<mu>' B - finite_measure.\<mu>' (M\<lparr>measure := \<nu>\<rparr>) B)"
   14.23  proof -
   14.24    interpret M': finite_measure "M\<lparr>measure := \<nu>\<rparr>" by fact
   14.25 -  let "?d A" = "\<mu>' A - M'.\<mu>' A"
   14.26 -  let "?A A" = "if (\<forall>B\<in>sets M. B \<subseteq> space M - A \<longrightarrow> -e < ?d B)
   14.27 +  let ?d = "\<lambda>A. \<mu>' A - M'.\<mu>' A"
   14.28 +  let ?A = "\<lambda>A. if (\<forall>B\<in>sets M. B \<subseteq> space M - A \<longrightarrow> -e < ?d B)
   14.29      then {}
   14.30      else (SOME B. B \<in> sets M \<and> B \<subseteq> space M - A \<and> ?d B \<le> -e)"
   14.31    def A \<equiv> "\<lambda>n. ((\<lambda>B. B \<union> ?A B) ^^ n) {}"
   14.32 @@ -247,9 +247,9 @@
   14.33  proof -
   14.34    interpret M': finite_measure ?M' where
   14.35      "space ?M' = space M" and "sets ?M' = sets M" and "measure ?M' = \<nu>" by fact auto
   14.36 -  let "?d A" = "\<mu>' A - M'.\<mu>' A"
   14.37 -  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)"
   14.38 -  let "?r S" = "restricted_space S"
   14.39 +  let ?d = "\<lambda>A. \<mu>' A - M'.\<mu>' A"
   14.40 +  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)"
   14.41 +  let ?r = "\<lambda>S. restricted_space S"
   14.42    { fix S n assume S: "S \<in> sets M"
   14.43      note r = M'.restricted_finite_measure[of S] restricted_finite_measure[OF S] S
   14.44      then have "finite_measure (?r S)" "0 < 1 / real (Suc n)"
   14.45 @@ -342,7 +342,7 @@
   14.46          (\<integral>\<^isup>+x. g x * indicator (?A \<inter> A) x \<partial>M) +
   14.47          (\<integral>\<^isup>+x. f x * indicator ((space M - ?A) \<inter> A) x \<partial>M)"
   14.48          using f g sets unfolding G_def
   14.49 -        by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator)
   14.50 +        by (auto cong: positive_integral_cong intro!: positive_integral_add)
   14.51        also have "\<dots> \<le> \<nu> (?A \<inter> A) + \<nu> ((space M - ?A) \<inter> A)"
   14.52          using f g sets unfolding G_def by (auto intro!: add_mono)
   14.53        also have "\<dots> = \<nu> A"
   14.54 @@ -388,9 +388,9 @@
   14.55    qed
   14.56    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
   14.57    hence y_eq: "?y = (SUP i. integral\<^isup>P M (gs i))" using ys by auto
   14.58 -  let "?g i x" = "Max ((\<lambda>n. gs n x) ` {..i})"
   14.59 +  let ?g = "\<lambda>i x. Max ((\<lambda>n. gs n x) ` {..i})"
   14.60    def f \<equiv> "\<lambda>x. SUP i. ?g i x"
   14.61 -  let "?F A x" = "f x * indicator A x"
   14.62 +  let ?F = "\<lambda>A x. f x * indicator A x"
   14.63    have gs_not_empty: "\<And>i x. (\<lambda>n. gs n x) ` {..i} \<noteq> {}" by auto
   14.64    { fix i have "?g i \<in> G"
   14.65      proof (induct i)
   14.66 @@ -420,7 +420,7 @@
   14.67    have "\<And>x. 0 \<le> f x"
   14.68      unfolding f_def using `\<And>i. gs i \<in> G`
   14.69      by (auto intro!: SUP_upper2 Max_ge_iff[THEN iffD2] simp: G_def)
   14.70 -  let "?t A" = "\<nu> A - (\<integral>\<^isup>+x. ?F A x \<partial>M)"
   14.71 +  let ?t = "\<lambda>A. \<nu> A - (\<integral>\<^isup>+x. ?F A x \<partial>M)"
   14.72    let ?M = "M\<lparr> measure := ?t\<rparr>"
   14.73    interpret M: sigma_algebra ?M
   14.74      by (intro sigma_algebra_cong) auto
   14.75 @@ -522,7 +522,7 @@
   14.76          using M'.finite_measure b finite_measure M.positive_measure[OF B(1)]
   14.77          by (cases rule: ereal2_cases[of "?t B" "b * \<mu> B"]) auto }
   14.78      note bM_le_t = this
   14.79 -    let "?f0 x" = "f x + b * indicator A0 x"
   14.80 +    let ?f0 = "\<lambda>x. f x + b * indicator A0 x"
   14.81      { fix A assume A: "A \<in> sets M"
   14.82        hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
   14.83        have "(\<integral>\<^isup>+x. ?f0 x  * indicator A x \<partial>M) =
   14.84 @@ -550,8 +550,7 @@
   14.85          by (cases "\<integral>\<^isup>+x. ?F A x \<partial>M", cases "\<nu> A") auto
   14.86        finally have "(\<integral>\<^isup>+x. ?f0 x * indicator A x \<partial>M) \<le> \<nu> A" . }
   14.87      hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G` unfolding G_def
   14.88 -      by (auto intro!: borel_measurable_indicator borel_measurable_ereal_add
   14.89 -                       borel_measurable_ereal_times ereal_add_nonneg_nonneg)
   14.90 +      by (auto intro!: ereal_add_nonneg_nonneg)
   14.91      have real: "?t (space M) \<noteq> \<infinity>" "?t A0 \<noteq> \<infinity>"
   14.92        "b * \<mu> (space M) \<noteq> \<infinity>" "b * \<mu> A0 \<noteq> \<infinity>"
   14.93        using `A0 \<in> sets M` b
   14.94 @@ -633,7 +632,7 @@
   14.95    have "{} \<in> ?Q" using v.empty_measure by auto
   14.96    then have Q_not_empty: "?Q \<noteq> {}" by blast
   14.97    have "?a \<le> \<mu> (space M)" using sets_into_space
   14.98 -    by (auto intro!: SUP_least measure_mono top)
   14.99 +    by (auto intro!: SUP_least measure_mono)
  14.100    then have "?a \<noteq> \<infinity>" using finite_measure_of_space
  14.101      by auto
  14.102    from SUPR_countable_SUPR[OF Q_not_empty, of \<mu>]
  14.103 @@ -643,7 +642,7 @@
  14.104    from choice[OF this] obtain Q' where Q': "\<And>i. Q'' i = \<mu> (Q' i)" "\<And>i. Q' i \<in> ?Q"
  14.105      by auto
  14.106    then have a_Lim: "?a = (SUP i::nat. \<mu> (Q' i))" using a by simp
  14.107 -  let "?O n" = "\<Union>i\<le>n. Q' i"
  14.108 +  let ?O = "\<lambda>n. \<Union>i\<le>n. Q' i"
  14.109    have Union: "(SUP i. \<mu> (?O i)) = \<mu> (\<Union>i. ?O i)"
  14.110    proof (rule continuity_from_below[of ?O])
  14.111      show "range ?O \<subseteq> sets M" using Q' by (auto intro!: finite_UN)
  14.112 @@ -675,7 +674,7 @@
  14.113          using O_in_G[of i] by (auto intro!: exI[of _ "?O i"])
  14.114      qed
  14.115    qed
  14.116 -  let "?O_0" = "(\<Union>i. ?O i)"
  14.117 +  let ?O_0 = "(\<Union>i. ?O i)"
  14.118    have "?O_0 \<in> sets M" using Q' by auto
  14.119    def Q \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> Q' 0 | Suc n \<Rightarrow> ?O (Suc n) - ?O n"
  14.120    { fix i have "Q i \<in> sets M" unfolding Q_def using Q'[of 0] by (cases i) (auto intro: O_sets) }
  14.121 @@ -710,10 +709,9 @@
  14.122              fix i have "?O i \<union> A \<in> ?Q"
  14.123              proof (safe del: notI)
  14.124                show "?O i \<union> A \<in> sets M" using O_sets A by auto
  14.125 -              from O_in_G[of i]
  14.126 -              moreover have "\<nu> (?O i \<union> A) \<le> \<nu> (?O i) + \<nu> A"
  14.127 +              from O_in_G[of i] have "\<nu> (?O i \<union> A) \<le> \<nu> (?O i) + \<nu> A"
  14.128                  using v.measure_subadditive[of "?O i" A] A O_sets by auto
  14.129 -              ultimately show "\<nu> (?O i \<union> A) \<noteq> \<infinity>"
  14.130 +              with O_in_G[of i] show "\<nu> (?O i \<union> A) \<noteq> \<infinity>"
  14.131                  using `\<nu> A \<noteq> \<infinity>` by auto
  14.132              qed
  14.133              then show "\<mu> (?O i \<union> A) \<le> ?a" by (rule SUP_upper)
  14.134 @@ -800,7 +798,7 @@
  14.135      and f: "\<And>A i. A \<in> sets M \<Longrightarrow>
  14.136        \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f i x * indicator (Q i \<inter> A) x \<partial>M)"
  14.137      by auto
  14.138 -  let "?f x" = "(\<Sum>i. f i x * indicator (Q i) x) + \<infinity> * indicator Q0 x"
  14.139 +  let ?f = "\<lambda>x. (\<Sum>i. f i x * indicator (Q i) x) + \<infinity> * indicator Q0 x"
  14.140    show ?thesis
  14.141    proof (safe intro!: bexI[of _ ?f])
  14.142      show "?f \<in> borel_measurable M" using Q0 borel Q_sets
  14.143 @@ -850,7 +848,7 @@
  14.144      nn: "\<And>x. 0 \<le> h x" and
  14.145      pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
  14.146      "\<And>x. x \<in> space M \<Longrightarrow> h x < \<infinity>" by auto
  14.147 -  let "?T A" = "(\<integral>\<^isup>+x. h x * indicator A x \<partial>M)"
  14.148 +  let ?T = "\<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x \<partial>M)"
  14.149    let ?MT = "M\<lparr> measure := ?T \<rparr>"
  14.150    interpret T: finite_measure ?MT
  14.151      where "space ?MT = space M" and "sets ?MT = sets M" and "measure ?MT = ?T"
  14.152 @@ -872,7 +870,7 @@
  14.153    show ?thesis
  14.154    proof (safe intro!: bexI[of _ "\<lambda>x. h x * f x"])
  14.155      show "(\<lambda>x. h x * f x) \<in> borel_measurable M"
  14.156 -      using borel f_borel by (auto intro: borel_measurable_ereal_times)
  14.157 +      using borel f_borel by auto
  14.158      show "\<And>x. 0 \<le> h x * f x" using nn f_borel by auto
  14.159      fix A assume "A \<in> sets M"
  14.160      then show "\<nu> A = (\<integral>\<^isup>+x. h x * f x * indicator A x \<partial>M)"
  14.161 @@ -933,8 +931,8 @@
  14.162      (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
  14.163    shows "AE x. f x = f' x"
  14.164  proof -
  14.165 -  let "?\<nu> A" = "?P f A" and "?\<nu>' A" = "?P f' A"
  14.166 -  let "?f A x" = "f x * indicator A x" and "?f' A x" = "f' x * indicator A x"
  14.167 +  let ?\<nu> = "\<lambda>A. ?P f A" and ?\<nu>' = "\<lambda>A. ?P f' A"
  14.168 +  let ?f = "\<lambda>A x. f x * indicator A x" and ?f' = "\<lambda>A x. f' x * indicator A x"
  14.169    interpret M: measure_space "M\<lparr> measure := ?\<nu>\<rparr>"
  14.170      using borel(1) pos(1) by (rule measure_space_density) simp
  14.171    have ac: "absolutely_continuous ?\<nu>"
  14.172 @@ -957,7 +955,7 @@
  14.173    proof (rule AE_I')
  14.174      { fix f :: "'a \<Rightarrow> ereal" assume borel: "f \<in> borel_measurable M"
  14.175          and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)"
  14.176 -      let "?A i" = "Q0 \<inter> {x \<in> space M. f x < (i::nat)}"
  14.177 +      let ?A = "\<lambda>i. Q0 \<inter> {x \<in> space M. f x < (i::nat)}"
  14.178        have "(\<Union>i. ?A i) \<in> null_sets"
  14.179        proof (rule null_sets_UN)
  14.180          fix i ::nat have "?A i \<in> sets M"
  14.181 @@ -1079,7 +1077,7 @@
  14.182      apply (rule_tac Int)
  14.183      by (cases i) (auto intro: measurable_sets[OF f(1)]) }
  14.184    note A_in_sets = this
  14.185 -  let "?A n" = "case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
  14.186 +  let ?A = "\<lambda>n. case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
  14.187    show "sigma_finite_measure ?N"
  14.188    proof (default, intro exI conjI subsetI allI)
  14.189      fix x assume "x \<in> range ?A"
    15.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Feb 28 20:20:09 2012 +0100
    15.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Feb 28 21:53:36 2012 +0100
    15.3 @@ -214,7 +214,7 @@
    15.4    then have "(\<Union>i. A i) = (\<Union>s\<in>sets M \<inter> range A. s)"
    15.5      by auto
    15.6    also have "(\<Union>s\<in>sets M \<inter> range A. s) \<in> sets M"
    15.7 -    using `finite (sets M)` by (auto intro: finite_UN)
    15.8 +    using `finite (sets M)` by auto
    15.9    finally show "(\<Union>i. A i) \<in> sets M" .
   15.10  qed
   15.11  
   15.12 @@ -243,7 +243,7 @@
   15.13    assumes "A`X \<subseteq> sets M"
   15.14    shows  "(\<Union>x\<in>X. A x) \<in> sets M"
   15.15  proof -
   15.16 -  let "?A i" = "if i \<in> X then A i else {}"
   15.17 +  let ?A = "\<lambda>i. if i \<in> X then A i else {}"
   15.18    from assms have "range ?A \<subseteq> sets M" by auto
   15.19    with countable_nat_UN[of "?A \<circ> from_nat"] countable_UN_eq[of ?A M]
   15.20    have "(\<Union>x. ?A x) \<in> sets M" by auto
   15.21 @@ -1563,7 +1563,7 @@
   15.22      unfolding sigma_algebra_eq_Int_stable Int_stable_def
   15.23    proof (intro ballI)
   15.24      fix A B assume "A \<in> sets (dynkin M)" "B \<in> sets (dynkin M)"
   15.25 -    let "?D E" = "\<lparr> space = space M,
   15.26 +    let ?D = "\<lambda>E. \<lparr> space = space M,
   15.27                      sets = {Q. Q \<subseteq> space M \<and> Q \<inter> E \<in> sets (dynkin M)} \<rparr>"
   15.28      have "sets M \<subseteq> sets (?D B)"
   15.29      proof
   15.30 @@ -1637,7 +1637,7 @@
   15.31  next
   15.32    fix S assume "S \<subseteq> space (image_space X)"
   15.33    then obtain S' where "S = X`S'" "S'\<in>sets M"
   15.34 -    by (auto simp: subset_image_iff sets_eq_Pow image_space_def)
   15.35 +    by (auto simp: subset_image_iff image_space_def)
   15.36    then show "S \<in> sets (image_space X)"
   15.37      by (auto simp: image_space_def)
   15.38  qed
    16.1 --- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Tue Feb 28 20:20:09 2012 +0100
    16.2 +++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Tue Feb 28 21:53:36 2012 +0100
    16.3 @@ -82,7 +82,7 @@
    16.4    assumes "dc \<in> dining_cryptographers"
    16.5    shows "result dc \<longleftrightarrow> (payer dc \<noteq> None)"
    16.6  proof -
    16.7 -  let "?XOR f l" = "foldl (op \<noteq>) False (map f [0..<l])"
    16.8 +  let ?XOR = "\<lambda>f l. foldl (op \<noteq>) False (map f [0..<l])"
    16.9  
   16.10    have foldl_coin:
   16.11      "\<not> ?XOR (\<lambda>c. coin dc c \<noteq> coin dc (c + 1)) n"
   16.12 @@ -306,8 +306,8 @@
   16.13    assumes "xs \<in> inversion ` dc_crypto"
   16.14    shows "card {dc \<in> dc_crypto. inversion dc = xs} = 2 * n"
   16.15  proof -
   16.16 -  let "?set i" = "{dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs}"
   16.17 -  let "?sets" = "{?set i | i. i < n}"
   16.18 +  let ?set = "\<lambda>i. {dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs}"
   16.19 +  let ?sets = "{?set i | i. i < n}"
   16.20  
   16.21    have [simp]: "length xs = n" using assms
   16.22      by (auto simp: dc_crypto inversion_def_raw)
    17.1 --- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Tue Feb 28 20:20:09 2012 +0100
    17.2 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Tue Feb 28 21:53:36 2012 +0100
    17.3 @@ -333,7 +333,7 @@
    17.4        using `K k \<noteq> 0` by auto }
    17.5    note t_eq_imp = this
    17.6  
    17.7 -  let "?S obs" = "t -`{t obs} \<inter> OB`msgs"
    17.8 +  let ?S = "\<lambda>obs. t -`{t obs} \<inter> OB`msgs"
    17.9    { fix k obs assume "k \<in> keys" "K k \<noteq> 0" and obs: "obs \<in> OB`msgs"
   17.10      have *: "((\<lambda>x. (t (OB x), fst x)) -` {(t obs, k)} \<inter> msgs) =
   17.11        (\<Union>obs'\<in>?S obs. ((\<lambda>x. (OB x, fst x)) -` {(obs', k)} \<inter> msgs))" by auto
   17.12 @@ -378,8 +378,8 @@
   17.13      finally have "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(fst | OB) {(k, obs)}" . }
   17.14    note CP_T_eq_CP_O = this
   17.15  
   17.16 -  let "?H obs" = "(\<Sum>k\<in>keys. \<P>(fst|OB) {(k, obs)} * log b (\<P>(fst|OB) {(k, obs)})) :: real"
   17.17 -  let "?Ht obs" = "(\<Sum>k\<in>keys. \<P>(fst|t\<circ>OB) {(k, obs)} * log b (\<P>(fst|t\<circ>OB) {(k, obs)})) :: real"
   17.18 +  let ?H = "\<lambda>obs. (\<Sum>k\<in>keys. \<P>(fst|OB) {(k, obs)} * log b (\<P>(fst|OB) {(k, obs)})) :: real"
   17.19 +  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"
   17.20  
   17.21    { fix obs assume obs: "obs \<in> OB`msgs"
   17.22      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)}))"