src/HOL/Probability/Independent_Family.thy
 changeset 46731 5302e932d1e5 parent 45777 c36637603821 child 47694 05663f75964c
```     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Tue Feb 28 20:20:09 2012 +0100
1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Tue Feb 28 21:53:36 2012 +0100
1.3 @@ -142,7 +142,7 @@
1.4    with indep have "indep_sets F J"
1.5      by (subst (asm) indep_sets_finite_index_sets) auto
1.6    { fix J K assume "indep_sets F K"
1.7 -    let "?G S i" = "if i \<in> S then ?F i else F i"
1.8 +    let ?G = "\<lambda>S i. if i \<in> S then ?F i else F i"
1.9      assume "finite J" "J \<subseteq> K"
1.10      then have "indep_sets (?G J) K"
1.11      proof induct
1.12 @@ -384,7 +384,7 @@
1.13    assumes disjoint: "disjoint_family_on I J"
1.14    shows "indep_sets (\<lambda>j. sigma_sets (space M) (\<Union>i\<in>I j. E i)) J"
1.15  proof -
1.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) }"
1.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) }"
1.18
1.19    from indep have E: "\<And>j i. j \<in> J \<Longrightarrow> i \<in> I j \<Longrightarrow> E i \<subseteq> events"
1.20      unfolding indep_sets_def by auto
1.21 @@ -447,7 +447,7 @@
1.22            with * L_inj show "k = j" by auto
1.23          qed (insert *, simp) }
1.24        note k_simp[simp] = this
1.25 -      let "?E' l" = "E' (k l) l"
1.26 +      let ?E' = "\<lambda>l. E' (k l) l"
1.27        have "prob (\<Inter>j\<in>K. A j) = prob (\<Inter>l\<in>(\<Union>k\<in>K. L k). ?E' l)"
1.28          by (auto simp: A intro!: arg_cong[where f=prob])
1.29        also have "\<dots> = (\<Prod>l\<in>(\<Union>k\<in>K. L k). prob (?E' l))"
1.30 @@ -658,7 +658,7 @@
1.31      fix i show "Int_stable \<lparr>space = space M, sets = {F i}\<rparr>"
1.32        unfolding Int_stable_def by simp
1.33    qed
1.34 -  let "?Q n" = "\<Union>i\<in>{n..}. F i"
1.35 +  let ?Q = "\<lambda>n. \<Union>i\<in>{n..}. F i"
1.36    show "(\<Inter>n. \<Union>m\<in>{n..}. F m) \<in> terminal_events (\<lambda>i. sigma_sets (space M) {F i})"
1.37      unfolding terminal_events_def
1.38    proof
1.39 @@ -691,7 +691,7 @@
1.40    proof (rule indep_setsI[OF F(1)])
1.41      fix A J assume J: "J \<noteq> {}" "J \<subseteq> I" "finite J"
1.42      assume A: "\<forall>j\<in>J. A j \<in> F j"
1.43 -    let "?A j" = "if j \<in> J then A j else space M"
1.44 +    let ?A = "\<lambda>j. if j \<in> J then A j else space M"
1.45      have "prob (\<Inter>j\<in>I. ?A j) = prob (\<Inter>j\<in>J. A j)"
1.46        using subset_trans[OF F(1) space_closed] J A
1.47        by (auto intro!: arg_cong[where f=prob] split: split_if_asm) blast
```