more symbols via abbrevs;
authorwenzelm
Tue Jan 17 11:26:21 2017 +0100 (2017-01-17)
changeset 649106108dddad9f0
parent 64909 8007f10195af
child 64911 f0e07600de47
more symbols via abbrevs;
src/HOL/Analysis/Finite_Product_Measure.thy
src/HOL/Analysis/Function_Topology.thy
src/HOL/Analysis/Tagged_Division.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Library/FuncSet.thy
src/HOL/Probability/Infinite_Product_Measure.thy
     1.1 --- a/src/HOL/Analysis/Finite_Product_Measure.thy	Mon Jan 16 21:53:44 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Tue Jan 17 11:26:21 2017 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Binary_Product_Measure
     1.5  begin
     1.6  
     1.7 -lemma PiE_choice: "(\<exists>f\<in>PiE I F. \<forall>i\<in>I. P i (f i)) \<longleftrightarrow> (\<forall>i\<in>I. \<exists>x\<in>F i. P i x)"
     1.8 +lemma PiE_choice: "(\<exists>f\<in>Pi\<^sub>E I F. \<forall>i\<in>I. P i (f i)) \<longleftrightarrow> (\<forall>i\<in>I. \<exists>x\<in>F i. P i x)"
     1.9    by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1])
    1.10       (force intro: exI[of _ "restrict f I" for f])
    1.11  
    1.12 @@ -61,7 +61,7 @@
    1.13  
    1.14  lemma PiE_cancel_merge[simp]:
    1.15    "I \<inter> J = {} \<Longrightarrow>
    1.16 -    merge I J (x, y) \<in> PiE (I \<union> J) B \<longleftrightarrow> x \<in> Pi I B \<and> y \<in> Pi J B"
    1.17 +    merge I J (x, y) \<in> Pi\<^sub>E (I \<union> J) B \<longleftrightarrow> x \<in> Pi I B \<and> y \<in> Pi J B"
    1.18    by (auto simp: PiE_def restrict_Pi_cancel)
    1.19  
    1.20  lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I {i} (x,y) = restrict (x(i := y i)) (insert i I)"
    1.21 @@ -114,7 +114,7 @@
    1.22  subsubsection \<open>Products\<close>
    1.23  
    1.24  definition prod_emb where
    1.25 -  "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (PIE i:I. space (M i))"
    1.26 +  "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (\<Pi>\<^sub>E i\<in>I. space (M i))"
    1.27  
    1.28  lemma prod_emb_iff:
    1.29    "f \<in> prod_emb I M K X \<longleftrightarrow> f \<in> extensional I \<and> (restrict f K \<in> X) \<and> (\<forall>i\<in>I. f i \<in> space (M i))"
    1.30 @@ -216,7 +216,7 @@
    1.31  proof (intro iffI set_eqI)
    1.32    fix A assume "A \<in> ?L"
    1.33    then obtain J E where J: "J \<noteq> {} \<or> I = {}" "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
    1.34 -    and A: "A = prod_emb I M J (PIE j:J. E j)"
    1.35 +    and A: "A = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
    1.36      by (auto simp: prod_algebra_def)
    1.37    let ?A = "\<Pi>\<^sub>E i\<in>I. if i \<in> J then E i else space (M i)"
    1.38    have A: "A = ?A"
    1.39 @@ -234,7 +234,7 @@
    1.40  
    1.41  lemma prod_algebraI:
    1.42    "finite J \<Longrightarrow> (J \<noteq> {} \<or> I = {}) \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i))
    1.43 -    \<Longrightarrow> prod_emb I M J (PIE j:J. E j) \<in> prod_algebra I M"
    1.44 +    \<Longrightarrow> prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) \<in> prod_algebra I M"
    1.45    by (auto simp: prod_algebra_def)
    1.46  
    1.47  lemma prod_algebraI_finite:
    1.48 @@ -250,7 +250,7 @@
    1.49  
    1.50  lemma prod_algebraE:
    1.51    assumes A: "A \<in> prod_algebra I M"
    1.52 -  obtains J E where "A = prod_emb I M J (PIE j:J. E j)"
    1.53 +  obtains J E where "A = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
    1.54      "finite J" "J \<noteq> {} \<or> I = {}" "J \<subseteq> I" "\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i)"
    1.55    using A by (auto simp: prod_algebra_def)
    1.56  
    1.57 @@ -459,9 +459,9 @@
    1.58          by (auto simp: PiE_def Pi_def)
    1.59        then obtain s where s: "\<And>i. i \<in> j \<Longrightarrow> s i \<in> S i" "\<And>i. i \<in> j \<Longrightarrow> x i \<in> s i"
    1.60          by metis
    1.61 -      with \<open>x i \<in> A\<close> have "\<exists>n\<in>PiE (j-{i}) S. \<forall>i\<in>j. x i \<in> A' n i"
    1.62 +      with \<open>x i \<in> A\<close> have "\<exists>n\<in>Pi\<^sub>E (j-{i}) S. \<forall>i\<in>j. x i \<in> A' n i"
    1.63          by (intro bexI[of _ "restrict (s(i := A)) (j-{i})"]) (auto simp: A'_def split: if_splits) }
    1.64 -    then have "Z = (\<Union>n\<in>PiE (j-{i}) S. {f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A' n i})"
    1.65 +    then have "Z = (\<Union>n\<in>Pi\<^sub>E (j-{i}) S. {f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A' n i})"
    1.66        unfolding Z_def
    1.67        by (auto simp add: set_eq_iff ball_conj_distrib \<open>i\<in>j\<close> A'_i dest: bspec[OF _ \<open>i\<in>j\<close>]
    1.68                 cong: conj_cong)
    1.69 @@ -509,10 +509,10 @@
    1.70  
    1.71  lemma sets_PiM_I:
    1.72    assumes "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
    1.73 -  shows "prod_emb I M J (PIE j:J. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)"
    1.74 +  shows "prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)"
    1.75  proof cases
    1.76    assume "J = {}"
    1.77 -  then have "prod_emb I M J (PIE j:J. E j) = (PIE j:I. space (M j))"
    1.78 +  then have "prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) = (\<Pi>\<^sub>E j\<in>I. space (M j))"
    1.79      by (auto simp: prod_emb_def)
    1.80    then show ?thesis
    1.81      by (auto simp add: sets_PiM intro!: sigma_sets_top)
    1.82 @@ -576,7 +576,7 @@
    1.83  
    1.84  lemma sets_PiM_I_finite[measurable]:
    1.85    assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
    1.86 -  shows "(PIE j:I. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)"
    1.87 +  shows "(\<Pi>\<^sub>E j\<in>I. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)"
    1.88    using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] \<open>finite I\<close> sets by auto
    1.89  
    1.90  lemma measurable_component_singleton[measurable (raw)]:
    1.91 @@ -741,7 +741,7 @@
    1.92    assumes I: "countable I" and E: "\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i)" shows "Pi\<^sub>E I E \<in> sets (Pi\<^sub>M I M)"
    1.93  proof cases
    1.94    assume "I \<noteq> {}"
    1.95 -  then have "PiE I E = (\<Inter>i\<in>I. prod_emb I M {i} (PiE {i} E))"
    1.96 +  then have "Pi\<^sub>E I E = (\<Inter>i\<in>I. prod_emb I M {i} (Pi\<^sub>E {i} E))"
    1.97      using E[THEN sets.sets_into_space] by (auto simp: PiE_iff prod_emb_def fun_eq_iff)
    1.98    also have "\<dots> \<in> sets (PiM I M)"
    1.99      using I \<open>I \<noteq> {}\<close> by (safe intro!: sets.countable_INT' measurable_prod_emb sets_PiM_I_finite E)
   1.100 @@ -793,7 +793,7 @@
   1.101    show "range A \<subseteq> prod_algebra I M" "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))" "\<And>i. P (A i) \<noteq> \<infinity>"
   1.102      unfolding space_PiM[symmetric] by fact+
   1.103    fix X assume "X \<in> prod_algebra I M"
   1.104 -  then obtain J E where X: "X = prod_emb I M J (PIE j:J. E j)"
   1.105 +  then obtain J E where X: "X = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
   1.106      and J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)"
   1.107      by (force elim!: prod_algebraE)
   1.108    then show "emeasure P X = emeasure Q X"
   1.109 @@ -822,7 +822,7 @@
   1.110      by (auto simp: space_PiM)
   1.111  next
   1.112    fix X assume X: "X \<in> prod_algebra I M"
   1.113 -  then obtain J E where X: "X = prod_emb I M J (PIE j:J. E j)"
   1.114 +  then obtain J E where X: "X = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
   1.115      and J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)"
   1.116      by (force elim!: prod_algebraE)
   1.117    then show "emeasure P X = emeasure Q X"
   1.118 @@ -976,10 +976,10 @@
   1.119      "\<And>j f. f \<in> F j \<Longrightarrow> emeasure (M j) f \<noteq> \<infinity>" and
   1.120      in_space: "\<And>j. space (M j) = (\<Union>F j)"
   1.121      using sigma_finite_countable by (metis subset_eq)
   1.122 -  moreover have "(\<Union>(PiE I ` PiE I F)) = space (Pi\<^sub>M I M)"
   1.123 +  moreover have "(\<Union>(Pi\<^sub>E I ` Pi\<^sub>E I F)) = space (Pi\<^sub>M I M)"
   1.124      using in_space by (auto simp: space_PiM PiE_iff intro!: PiE_choice[THEN iffD2])
   1.125    ultimately show "\<exists>A. countable A \<and> A \<subseteq> sets (Pi\<^sub>M I M) \<and> \<Union>A = space (Pi\<^sub>M I M) \<and> (\<forall>a\<in>A. emeasure (Pi\<^sub>M I M) a \<noteq> \<infinity>)"
   1.126 -    by (intro exI[of _ "PiE I ` PiE I F"])
   1.127 +    by (intro exI[of _ "Pi\<^sub>E I ` Pi\<^sub>E I F"])
   1.128         (auto intro!: countable_PiE sets_PiM_I_finite
   1.129               simp: PiE_iff emeasure_PiM finite_index ennreal_prod_eq_top)
   1.130  qed
   1.131 @@ -1003,7 +1003,7 @@
   1.132    interpret I: finite_product_sigma_finite M I by standard fact
   1.133    interpret J: finite_product_sigma_finite M J by standard fact
   1.134    fix A assume A: "\<And>i. i \<in> I \<union> J \<Longrightarrow> A i \<in> sets (M i)"
   1.135 -  have *: "(merge I J -` Pi\<^sub>E (I \<union> J) A \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)) = PiE I A \<times> PiE J A"
   1.136 +  have *: "(merge I J -` Pi\<^sub>E (I \<union> J) A \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)) = Pi\<^sub>E I A \<times> Pi\<^sub>E J A"
   1.137      using A[THEN sets.sets_into_space] by (auto simp: space_PiM space_pair_measure)
   1.138    from A fin show "emeasure (distr (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M) (merge I J)) (Pi\<^sub>E (I \<union> J) A) =
   1.139        (\<Prod>i\<in>I \<union> J. emeasure (M i) (A i))"
     2.1 --- a/src/HOL/Analysis/Function_Topology.thy	Mon Jan 16 21:53:44 2017 +0100
     2.2 +++ b/src/HOL/Analysis/Function_Topology.thy	Tue Jan 17 11:26:21 2017 +0100
     2.3 @@ -17,7 +17,7 @@
     2.4  to each factor is continuous.
     2.5  
     2.6  To form a product of objects in Isabelle/HOL, all these objects should be subsets of a common type
     2.7 -'a. The product is then @{term "PiE I X"}, the set of elements from 'i to 'a such that the $i$-th
     2.8 +'a. The product is then @{term "Pi\<^sub>E I X"}, the set of elements from 'i to 'a such that the $i$-th
     2.9  coordinate belongs to $X\;i$ for all $i \in I$.
    2.10  
    2.11  Hence, to form a product of topological spaces, all these spaces should be subsets of a common type.
    2.12 @@ -696,7 +696,7 @@
    2.13  lemma product_topology_countable_basis:
    2.14    shows "\<exists>K::(('a::countable \<Rightarrow> 'b::second_countable_topology) set set).
    2.15            topological_basis K \<and> countable K \<and>
    2.16 -          (\<forall>k\<in>K. \<exists>X. (k = PiE UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV})"
    2.17 +          (\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV})"
    2.18  proof -
    2.19    obtain B::"'b set set" where B: "countable B \<and> topological_basis B"
    2.20      using ex_countable_basis by auto
    2.21 @@ -708,7 +708,7 @@
    2.22      using that unfolding B2_def using B topological_basis_open by auto
    2.23  
    2.24    define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i::'a. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
    2.25 -  have i: "\<forall>k\<in>K. \<exists>X. (k = PiE UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
    2.26 +  have i: "\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
    2.27      unfolding K_def using `\<And>U. U \<in> B2 \<Longrightarrow> open U` by auto
    2.28  
    2.29    have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
    2.30 @@ -1335,11 +1335,11 @@
    2.31    "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
    2.32  proof
    2.33    obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
    2.34 -            "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = PiE UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
    2.35 +            "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
    2.36      using product_topology_countable_basis by fast
    2.37    have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
    2.38    proof -
    2.39 -    obtain X where H: "k = PiE UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
    2.40 +    obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
    2.41        using K(3)[OF `k \<in> K`] by blast
    2.42      show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
    2.43    qed
     3.1 --- a/src/HOL/Analysis/Tagged_Division.thy	Mon Jan 16 21:53:44 2017 +0100
     3.2 +++ b/src/HOL/Analysis/Tagged_Division.thy	Tue Jan 17 11:26:21 2017 +0100
     3.3 @@ -2539,7 +2539,7 @@
     3.4    let ?K0 = "\<lambda>(n, f::'a\<Rightarrow>nat).
     3.5                      cbox (\<Sum>i \<in> Basis. (a \<bullet> i + (f i / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
     3.6                           (\<Sum>i \<in> Basis. (a \<bullet> i + ((f i + 1) / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)"
     3.7 -  let ?D0 = "?K0 ` (SIGMA n:UNIV. PiE Basis (\<lambda>i::'a. lessThan (2^n)))"
     3.8 +  let ?D0 = "?K0 ` (SIGMA n:UNIV. Pi\<^sub>E Basis (\<lambda>i::'a. lessThan (2^n)))"
     3.9    obtain \<D>0 where count: "countable \<D>0"
    3.10               and sub: "\<Union>\<D>0 \<subseteq> cbox a b"
    3.11               and int:  "\<And>K. K \<in> \<D>0 \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
    3.12 @@ -2698,7 +2698,7 @@
    3.13      proof (rule finite_subset)
    3.14        let ?B = "(\<lambda>(n, f::'a\<Rightarrow>nat). cbox (\<Sum>i\<in>Basis. (a \<bullet> i + (f i) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
    3.15                                          (\<Sum>i\<in>Basis. (a \<bullet> i + ((f i) + 1) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i))
    3.16 -                ` (SIGMA m:atMost n. PiE Basis (\<lambda>i::'a. lessThan (2^m)))"
    3.17 +                ` (SIGMA m:atMost n. Pi\<^sub>E Basis (\<lambda>i::'a. lessThan (2^m)))"
    3.18        have "?K0(m,g) \<in> ?B" if "g \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ m}" "?K0(n,f) \<subseteq> ?K0(m,g)" for m g
    3.19        proof -
    3.20          have dd: "w / m \<le> v / n \<and> (v+1) / n \<le> (w+1) / m
     4.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Jan 16 21:53:44 2017 +0100
     4.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jan 17 11:26:21 2017 +0100
     4.3 @@ -89,7 +89,7 @@
     4.4    done
     4.5  
     4.6  lemma countable_PiE:
     4.7 -  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
     4.8 +  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)"
     4.9    by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
    4.10  
    4.11  lemma continuous_on_cases:
    4.12 @@ -2173,7 +2173,7 @@
    4.13  
    4.14  lemma interior_complement: "interior (- S) = - closure S"
    4.15    by (simp add: closure_interior)
    4.16 -   
    4.17 +
    4.18  lemma interior_diff: "interior(S - T) = interior S - closure T"
    4.19    by (simp add: Diff_eq interior_complement)
    4.20  
    4.21 @@ -5348,7 +5348,7 @@
    4.22    show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
    4.23      using l r by fast
    4.24  qed
    4.25 -  
    4.26 +
    4.27  subsubsection \<open>Intersecting chains of compact sets\<close>
    4.28  
    4.29  proposition bounded_closed_chain:
    4.30 @@ -10727,8 +10727,8 @@
    4.31    qed
    4.32    from X0(1,2) this show ?thesis ..
    4.33  qed
    4.34 -  
    4.35 -  
    4.36 +
    4.37 +
    4.38  subsection\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
    4.39  
    4.40  text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
     5.1 --- a/src/HOL/Library/FuncSet.thy	Mon Jan 16 21:53:44 2017 +0100
     5.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Jan 17 11:26:21 2017 +0100
     5.3 @@ -5,7 +5,9 @@
     5.4  section \<open>Pi and Function Sets\<close>
     5.5  
     5.6  theory FuncSet
     5.7 -imports Hilbert_Choice Main
     5.8 +  imports Hilbert_Choice Main
     5.9 +  abbrevs PiE = "Pi\<^sub>E"
    5.10 +    PIE = "\<Pi>\<^sub>E"
    5.11  begin
    5.12  
    5.13  definition Pi :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set"
    5.14 @@ -360,10 +362,10 @@
    5.15  lemma extensional_funcset_def: "extensional_funcset S T = (S \<rightarrow> T) \<inter> extensional S"
    5.16    by (simp add: PiE_def)
    5.17  
    5.18 -lemma PiE_empty_domain[simp]: "PiE {} T = {\<lambda>x. undefined}"
    5.19 +lemma PiE_empty_domain[simp]: "Pi\<^sub>E {} T = {\<lambda>x. undefined}"
    5.20    unfolding PiE_def by simp
    5.21  
    5.22 -lemma PiE_UNIV_domain: "PiE UNIV T = Pi UNIV T"
    5.23 +lemma PiE_UNIV_domain: "Pi\<^sub>E UNIV T = Pi UNIV T"
    5.24    unfolding PiE_def by simp
    5.25  
    5.26  lemma PiE_empty_range[simp]: "i \<in> I \<Longrightarrow> F i = {} \<Longrightarrow> (\<Pi>\<^sub>E i\<in>I. F i) = {}"
    5.27 @@ -386,29 +388,29 @@
    5.28    qed
    5.29  qed (auto simp: PiE_def)
    5.30  
    5.31 -lemma PiE_arb: "f \<in> PiE S T \<Longrightarrow> x \<notin> S \<Longrightarrow> f x = undefined"
    5.32 +lemma PiE_arb: "f \<in> Pi\<^sub>E S T \<Longrightarrow> x \<notin> S \<Longrightarrow> f x = undefined"
    5.33    unfolding PiE_def by auto (auto dest!: extensional_arb)
    5.34  
    5.35 -lemma PiE_mem: "f \<in> PiE S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T x"
    5.36 +lemma PiE_mem: "f \<in> Pi\<^sub>E S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T x"
    5.37    unfolding PiE_def by auto
    5.38  
    5.39 -lemma PiE_fun_upd: "y \<in> T x \<Longrightarrow> f \<in> PiE S T \<Longrightarrow> f(x := y) \<in> PiE (insert x S) T"
    5.40 +lemma PiE_fun_upd: "y \<in> T x \<Longrightarrow> f \<in> Pi\<^sub>E S T \<Longrightarrow> f(x := y) \<in> Pi\<^sub>E (insert x S) T"
    5.41    unfolding PiE_def extensional_def by auto
    5.42  
    5.43 -lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> PiE (insert x S) T \<Longrightarrow> f(x := undefined) \<in> PiE S T"
    5.44 +lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> Pi\<^sub>E (insert x S) T \<Longrightarrow> f(x := undefined) \<in> Pi\<^sub>E S T"
    5.45    unfolding PiE_def extensional_def by auto
    5.46  
    5.47 -lemma PiE_insert_eq: "PiE (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
    5.48 +lemma PiE_insert_eq: "Pi\<^sub>E (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)"
    5.49  proof -
    5.50    {
    5.51 -    fix f assume "f \<in> PiE (insert x S) T" "x \<notin> S"
    5.52 -    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
    5.53 +    fix f assume "f \<in> Pi\<^sub>E (insert x S) T" "x \<notin> S"
    5.54 +    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)"
    5.55        by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
    5.56    }
    5.57    moreover
    5.58    {
    5.59 -    fix f assume "f \<in> PiE (insert x S) T" "x \<in> S"
    5.60 -    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
    5.61 +    fix f assume "f \<in> Pi\<^sub>E (insert x S) T" "x \<in> S"
    5.62 +    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)"
    5.63        by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb)
    5.64    }
    5.65    ultimately show ?thesis
    5.66 @@ -422,25 +424,25 @@
    5.67    unfolding PiE_def by (auto simp: Pi_cong)
    5.68  
    5.69  lemma PiE_E [elim]:
    5.70 -  assumes "f \<in> PiE A B"
    5.71 +  assumes "f \<in> Pi\<^sub>E A B"
    5.72    obtains "x \<in> A" and "f x \<in> B x"
    5.73      | "x \<notin> A" and "f x = undefined"
    5.74    using assms by (auto simp: Pi_def PiE_def extensional_def)
    5.75  
    5.76  lemma PiE_I[intro!]:
    5.77 -  "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> (\<And>x. x \<notin> A \<Longrightarrow> f x = undefined) \<Longrightarrow> f \<in> PiE A B"
    5.78 +  "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> (\<And>x. x \<notin> A \<Longrightarrow> f x = undefined) \<Longrightarrow> f \<in> Pi\<^sub>E A B"
    5.79    by (simp add: PiE_def extensional_def)
    5.80  
    5.81 -lemma PiE_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> PiE A B \<subseteq> PiE A C"
    5.82 +lemma PiE_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> Pi\<^sub>E A B \<subseteq> Pi\<^sub>E A C"
    5.83    by auto
    5.84  
    5.85 -lemma PiE_iff: "f \<in> PiE I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I"
    5.86 +lemma PiE_iff: "f \<in> Pi\<^sub>E I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I"
    5.87    by (simp add: PiE_def Pi_iff)
    5.88  
    5.89 -lemma PiE_restrict[simp]:  "f \<in> PiE A B \<Longrightarrow> restrict f A = f"
    5.90 +lemma PiE_restrict[simp]:  "f \<in> Pi\<^sub>E A B \<Longrightarrow> restrict f A = f"
    5.91    by (simp add: extensional_restrict PiE_def)
    5.92  
    5.93 -lemma restrict_PiE[simp]: "restrict f I \<in> PiE I S \<longleftrightarrow> f \<in> Pi I S"
    5.94 +lemma restrict_PiE[simp]: "restrict f I \<in> Pi\<^sub>E I S \<longleftrightarrow> f \<in> Pi I S"
    5.95    by (auto simp: PiE_iff)
    5.96  
    5.97  lemma PiE_eq_subset:
     6.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Mon Jan 16 21:53:44 2017 +0100
     6.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Jan 17 11:26:21 2017 +0100
     6.3 @@ -14,7 +14,7 @@
     6.4  proof (rule PiM_eqI)
     6.5    fix X assume X: "\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)"
     6.6    { fix J X assume J: "J \<noteq> {} \<or> I = {}" "finite J" "J \<subseteq> I" and X: "\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)"
     6.7 -    have "emeasure (PiM I M) (emb I J (PiE J X)) = (\<Prod>i\<in>J. M i (X i))"
     6.8 +    have "emeasure (PiM I M) (emb I J (Pi\<^sub>E J X)) = (\<Prod>i\<in>J. M i (X i))"
     6.9      proof (subst emeasure_extend_measure_Pair[OF PiM_def, where \<mu>'=lim], goal_cases)
    6.10        case 1 then show ?case
    6.11          by (simp add: M.emeasure_space_1 emeasure_PiM Pi_iff sets_PiM_I_finite emeasure_lim_emb)
    6.12 @@ -28,7 +28,7 @@
    6.13        add: M.emeasure_space_1 sets_lim[symmetric] emeasure_countably_additive emeasure_positive) }
    6.14    note * = this
    6.15  
    6.16 -  have "emeasure (PiM I M) (emb I J (PiE J X)) = (\<Prod>i\<in>J. M i (X i))"
    6.17 +  have "emeasure (PiM I M) (emb I J (Pi\<^sub>E J X)) = (\<Prod>i\<in>J. M i (X i))"
    6.18    proof (cases "J \<noteq> {} \<or> I = {}")
    6.19      case False
    6.20      then obtain i where i: "J = {}" "i \<in> I" by auto
    6.21 @@ -340,8 +340,8 @@
    6.22    have "\<And>j x. j \<in> J \<Longrightarrow> x \<in> E j \<Longrightarrow> x \<in> space M"
    6.23      using J(3)[THEN sets.sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
    6.24    with J have "?f -` ?X \<inter> space (S \<Otimes>\<^sub>M S) =
    6.25 -    (prod_emb ?I ?M (J \<inter> {..<i}) (PIE j:J \<inter> {..<i}. E j)) \<times>
    6.26 -    (prod_emb ?I ?M ((op + i) -` J) (PIE j:(op + i) -` J. E (i + j)))" (is "_ = ?E \<times> ?F")
    6.27 +    (prod_emb ?I ?M (J \<inter> {..<i}) (\<Pi>\<^sub>E j\<in>J \<inter> {..<i}. E j)) \<times>
    6.28 +    (prod_emb ?I ?M ((op + i) -` J) (\<Pi>\<^sub>E j\<in>(op + i) -` J. E (i + j)))" (is "_ = ?E \<times> ?F")
    6.29     by (auto simp: space_pair_measure space_PiM prod_emb_def all_conj_distrib PiE_iff
    6.30                 split: split_comb_seq split_comb_seq_asm)
    6.31    then have "emeasure ?D ?X = emeasure (S \<Otimes>\<^sub>M S) (?E \<times> ?F)"
    6.32 @@ -368,11 +368,11 @@
    6.33    let "distr _ _ ?f" = "?D"
    6.34  
    6.35    fix J E assume J: "finite J" "J \<subseteq> ?I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets M"
    6.36 -  let ?X = "prod_emb ?I ?M J (PIE j:J. E j)"
    6.37 +  let ?X = "prod_emb ?I ?M J (\<Pi>\<^sub>E j\<in>J. E j)"
    6.38    have "\<And>j x. j \<in> J \<Longrightarrow> x \<in> E j \<Longrightarrow> x \<in> space M"
    6.39      using J(3)[THEN sets.sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
    6.40    with J have "?f -` ?X \<inter> space (M \<Otimes>\<^sub>M S) = (if 0 \<in> J then E 0 else space M) \<times>
    6.41 -    (prod_emb ?I ?M (Suc -` J) (PIE j:Suc -` J. E (Suc j)))" (is "_ = ?E \<times> ?F")
    6.42 +    (prod_emb ?I ?M (Suc -` J) (\<Pi>\<^sub>E j\<in>Suc -` J. E (Suc j)))" (is "_ = ?E \<times> ?F")
    6.43     by (auto simp: space_pair_measure space_PiM PiE_iff prod_emb_def all_conj_distrib
    6.44        split: nat.split nat.split_asm)
    6.45    then have "emeasure ?D ?X = emeasure (M \<Otimes>\<^sub>M S) (?E \<times> ?F)"