# HG changeset patch
# User wenzelm
# Date 1330462416 -3600
# Node ID 5302e932d1e510811e96f157e0508281a26f3f40
# Parent  e3b99d0231bc2773a73155a8f4118c186cc887a0
avoid undeclared variables in let bindings;
tuned proofs;

diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/Binary_Product_Measure.thy
--- 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>"
diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/Borel_Space.thy
--- 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)
diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/Caratheodory.thy
--- 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))"
 proof (simp add: countably_subadditive_def, safe)
   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"
diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/Complete_Measure.thy
--- 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'])
diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/Conditional_Probability.thy
--- 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
diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/Finite_Product_Measure.thy
--- 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
diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/Independent_Family.thy
--- 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
diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/Infinite_Product_Measure.thy
--- 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)"
diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/Information.thy
--- 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]
diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/Lebesgue_Integration.thy
--- 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"
     by (simp add: AE_all_countable)
   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)"
diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/Lebesgue_Measure.thy
--- 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]
     by (simp add: lborel_def lebesgue_def)
diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/Measure.thy
--- 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)"
     using insert by (simp add: measure_subadditive)
   also have "\<dots> \<le> (\<Sum>i\<in>insert i I. \<mu> (A i))"
@@ -458,7 +458,7 @@
     by (simp add:  disjoint_family_disjointed comp_def)
   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})"
diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/Probability_Measure.thy
--- 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"
diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/Radon_Nikodym.thy
--- 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
-                       borel_measurable_ereal_times ereal_add_nonneg_nonneg)
+      by (auto intro!: ereal_add_nonneg_nonneg)
     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"
diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/Sigma_Algebra.thy
--- 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
diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/ex/Dining_Cryptographers.thy
--- 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)
diff -r e3b99d0231bc -r 5302e932d1e5 src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- 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)}))"