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