author bulwahn Wed Apr 06 13:08:44 2011 +0200 (2011-04-06) changeset 42259 5ff3a11e18ca parent 42258 79cb339d8989 parent 42257 08d717c82828 child 42260 4ea47da3d19b
merged
```     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Apr 06 10:58:18 2011 +0200
1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Apr 06 13:08:44 2011 +0200
1.3 @@ -319,7 +319,7 @@
1.4  translations
1.5    "PIP x:I. M" == "CONST Pi\<^isub>P I (%x. M)"
1.6
1.7 -sublocale product_prob_space \<subseteq> G: algebra generator
1.8 +sublocale product_prob_space \<subseteq> G!: algebra generator
1.9  proof
1.10    let ?G = generator
1.11    show "sets ?G \<subseteq> Pow (space ?G)"
1.12 @@ -738,19 +738,19 @@
1.13      done
1.14  qed
1.15
1.16 -sublocale product_prob_space \<subseteq> measure_space "Pi\<^isub>P I M"
1.17 +sublocale product_prob_space \<subseteq> P: measure_space "Pi\<^isub>P I M"
1.18    using infprod_spec by auto
1.19
1.20  lemma (in product_prob_space) measure_infprod_emb:
1.21    assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)"
1.22 -  shows "measure (Pi\<^isub>P I M) (emb I J X) = measure (Pi\<^isub>M J M) X"
1.23 +  shows "\<mu> (emb I J X) = measure (Pi\<^isub>M J M) X"
1.24  proof -
1.25    have "emb I J X \<in> sets generator"
1.26      using assms by (rule generatorI')
1.27    with \<mu>G_eq[OF assms] infprod_spec show ?thesis by auto
1.28  qed
1.29
1.30 -sublocale product_prob_space \<subseteq> prob_space "Pi\<^isub>P I M"
1.31 +sublocale product_prob_space \<subseteq> P: prob_space "Pi\<^isub>P I M"
1.32  proof
1.33    obtain i where "i \<in> I" using I_not_empty by auto
1.34    interpret i: finite_product_sigma_finite M "{i}" by default auto
1.35 @@ -758,11 +758,11 @@
1.36    have "?X \<in> sets (Pi\<^isub>M {i} M)"
1.37      by auto
1.38    from measure_infprod_emb[OF _ _ _ this] `i \<in> I`
1.39 -  have "measure (Pi\<^isub>P I M) (emb I {i} ?X) = measure (M i) (space (M i))"
1.40 +  have "\<mu> (emb I {i} ?X) = measure (M i) (space (M i))"
1.42    also have "emb I {i} ?X = space (Pi\<^isub>P I M)"
1.43      using `i \<in> I` by (auto simp: emb_def infprod_algebra_def generator_def)
1.44 -  finally show "measure (Pi\<^isub>P I M) (space (Pi\<^isub>P I M)) = 1"
1.45 +  finally show "\<mu> (space (Pi\<^isub>P I M)) = 1"
1.46      using M.measure_space_1 by simp
1.47  qed
1.48
1.49 @@ -784,4 +784,199 @@
1.50      unfolding infprod_algebra_def by auto
1.51  qed
1.52
1.53 +lemma (in product_prob_space) emb_in_infprod_algebra[intro]:
1.54 +  fixes J assumes J: "finite J" "J \<subseteq> I" and X: "X \<in> sets (Pi\<^isub>M J M)"
1.55 +  shows "emb I J X \<in> sets (\<Pi>\<^isub>P i\<in>I. M i)"
1.56 +proof cases
1.57 +  assume "J = {}"
1.58 +  with X have "emb I J X = space (\<Pi>\<^isub>P i\<in>I. M i) \<or> emb I J X = {}"
1.59 +    by (auto simp: emb_def infprod_algebra_def generator_def
1.60 +                   product_algebra_def product_algebra_generator_def image_constant sigma_def)
1.61 +  then show ?thesis by auto
1.62 +next
1.63 +  assume "J \<noteq> {}"
1.64 +  show ?thesis unfolding infprod_algebra_def
1.65 +    by simp (intro in_sigma generatorI'  `J \<noteq> {}` J X)
1.66 +qed
1.67 +
1.68 +lemma (in product_prob_space) finite_measure_infprod_emb:
1.69 +  assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)"
1.70 +  shows "\<mu>' (emb I J X) = finite_measure.\<mu>' (Pi\<^isub>M J M) X"
1.71 +proof -
1.72 +  interpret J: finite_product_prob_space M J by default fact+
1.73 +  from assms have "emb I J X \<in> sets (Pi\<^isub>P I M)" by auto
1.74 +  with assms show "\<mu>' (emb I J X) = J.\<mu>' X"
1.75 +    unfolding \<mu>'_def J.\<mu>'_def
1.76 +    unfolding measure_infprod_emb[OF assms]
1.77 +    by auto
1.78 +qed
1.79 +
1.80 +lemma (in finite_product_prob_space) finite_measure_times:
1.81 +  assumes "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)"
1.82 +  shows "\<mu>' (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu>' i (A i))"
1.83 +  using assms
1.84 +  unfolding \<mu>'_def M.\<mu>'_def
1.85 +  by (subst measure_times[OF assms])
1.86 +     (auto simp: finite_measure_eq M.finite_measure_eq setprod_extreal)
1.87 +
1.88 +lemma (in product_prob_space) finite_measure_infprod_emb_Pi:
1.89 +  assumes J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> X j \<in> sets (M j)"
1.90 +  shows "\<mu>' (emb I J (Pi\<^isub>E J X)) = (\<Prod>j\<in>J. M.\<mu>' j (X j))"
1.91 +proof cases
1.92 +  assume "J = {}"
1.93 +  then have "emb I J (Pi\<^isub>E J X) = space infprod_algebra"
1.94 +    by (auto simp: infprod_algebra_def generator_def sigma_def emb_def)
1.95 +  then show ?thesis using `J = {}` prob_space by simp
1.96 +next
1.97 +  assume "J \<noteq> {}"
1.98 +  interpret J: finite_product_prob_space M J by default fact+
1.99 +  have "(\<Prod>i\<in>J. M.\<mu>' i (X i)) = J.\<mu>' (Pi\<^isub>E J X)"
1.100 +    using J `J \<noteq> {}` by (subst J.finite_measure_times) auto
1.101 +  also have "\<dots> = \<mu>' (emb I J (Pi\<^isub>E J X))"
1.102 +    using J `J \<noteq> {}` by (intro finite_measure_infprod_emb[symmetric]) auto
1.103 +  finally show ?thesis by simp
1.104 +qed
1.105 +
1.106 +lemma sigma_sets_mono: assumes "A \<subseteq> sigma_sets X B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
1.107 +proof
1.108 +  fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
1.109 +    by induct (insert `A \<subseteq> sigma_sets X B`, auto intro: sigma_sets.intros)
1.110 +qed
1.111 +
1.112 +lemma sigma_sets_mono': assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
1.113 +proof
1.114 +  fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
1.115 +    by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros)
1.116 +qed
1.117 +
1.118 +lemma sigma_sets_subseteq: "A \<subseteq> sigma_sets X A"
1.119 +  by (auto intro: sigma_sets.Basic)
1.120 +
1.121 +lemma (in product_prob_space) infprod_algebra_alt:
1.122 +  "Pi\<^isub>P I M = sigma \<lparr> space = space (Pi\<^isub>P I M),
1.123 +    sets = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i))),
1.124 +    measure = measure (Pi\<^isub>P I M) \<rparr>"
1.125 +  (is "_ = sigma \<lparr> space = ?O, sets = ?M, measure = ?m \<rparr>")
1.126 +proof (rule measure_space.equality)
1.127 +  let ?G = "\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^isub>M J M)"
1.128 +  have "sigma_sets ?O ?M = sigma_sets ?O ?G"
1.129 +  proof (intro equalityI sigma_sets_mono UN_least)
1.130 +    fix J assume J: "J \<in> {J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}"
1.131 +    have "emb I J ` Pi\<^isub>E J ` (\<Pi> i\<in>J. sets (M i)) \<subseteq> emb I J ` sets (Pi\<^isub>M J M)" by auto
1.132 +    also have "\<dots> \<subseteq> ?G" using J by (rule UN_upper)
1.133 +    also have "\<dots> \<subseteq> sigma_sets ?O ?G" by (rule sigma_sets_subseteq)
1.134 +    finally show "emb I J ` Pi\<^isub>E J ` (\<Pi> i\<in>J. sets (M i)) \<subseteq> sigma_sets ?O ?G" .
1.135 +    have "emb I J ` sets (Pi\<^isub>M J M) = emb I J ` sigma_sets (space (Pi\<^isub>M J M)) (Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
1.136 +      by (simp add: sets_sigma product_algebra_generator_def product_algebra_def)
1.137 +    also have "\<dots> = sigma_sets (space (Pi\<^isub>M I M)) (emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
1.138 +      using J M.sets_into_space
1.139 +      by (auto simp: emb_def_raw intro!: sigma_sets_vimage[symmetric]) blast
1.140 +    also have "\<dots> \<subseteq> sigma_sets (space (Pi\<^isub>M I M)) ?M"
1.141 +      using J by (intro sigma_sets_mono') auto
1.142 +    finally show "emb I J ` sets (Pi\<^isub>M J M) \<subseteq> sigma_sets ?O ?M"
1.143 +      by (simp add: infprod_algebra_def generator_def)
1.144 +  qed
1.145 +  then show "sets (Pi\<^isub>P I M) = sets (sigma \<lparr> space = ?O, sets = ?M, measure = ?m \<rparr>)"
1.146 +    by (simp_all add: infprod_algebra_def generator_def sets_sigma)
1.147 +qed simp_all
1.148 +
1.149 +lemma (in product_prob_space) infprod_algebra_alt2:
1.150 +  "Pi\<^isub>P I M = sigma \<lparr> space = space (Pi\<^isub>P I M),
1.151 +    sets = (\<Union>i\<in>I. (\<lambda>A. (\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M)) ` sets (M i)),
1.152 +    measure = measure (Pi\<^isub>P I M) \<rparr>"
1.153 +  (is "_ = ?S")
1.154 +proof (rule measure_space.equality)
1.155 +  let "sigma \<lparr> space = ?O, sets = ?A, \<dots> = _ \<rparr>" = ?S
1.156 +  let ?G = "(\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
1.157 +  have "sets (Pi\<^isub>P I M) = sigma_sets ?O ?G"
1.158 +    by (subst infprod_algebra_alt) (simp add: sets_sigma)
1.159 +  also have "\<dots> = sigma_sets ?O ?A"
1.160 +  proof (intro equalityI sigma_sets_mono subsetI)
1.161 +    interpret A: sigma_algebra ?S
1.162 +      by (rule sigma_algebra_sigma) auto
1.163 +    fix A assume "A \<in> ?G"
1.164 +    then obtain J B where "finite J" "J \<noteq> {}" "J \<subseteq> I" "A = emb I J (Pi\<^isub>E J B)"
1.165 +        and B: "\<And>i. i \<in> J \<Longrightarrow> B i \<in> sets (M i)"
1.166 +      by auto
1.167 +    then have A: "A = (\<Inter>j\<in>J. (\<lambda>x. x j) -` (B j) \<inter> space (Pi\<^isub>P I M))"
1.168 +      by (auto simp: emb_def infprod_algebra_def generator_def Pi_iff)
1.169 +    { fix j assume "j\<in>J"
1.170 +      with `J \<subseteq> I` have "j \<in> I" by auto
1.171 +      with `j \<in> J` B have "(\<lambda>x. x j) -` (B j) \<inter> space (Pi\<^isub>P I M) \<in> sets ?S"
1.172 +        by (auto simp: sets_sigma intro: sigma_sets.Basic) }
1.173 +    with `finite J` `J \<noteq> {}` have "A \<in> sets ?S"
1.174 +      unfolding A by (intro A.finite_INT) auto
1.175 +    then show "A \<in> sigma_sets ?O ?A" by (simp add: sets_sigma)
1.176 +  next
1.177 +    fix A assume "A \<in> ?A"
1.178 +    then obtain i B where i: "i \<in> I" "B \<in> sets (M i)"
1.179 +        and "A = (\<lambda>x. x i) -` B \<inter> space (Pi\<^isub>P I M)"
1.180 +      by auto
1.181 +    then have "A = emb I {i} (Pi\<^isub>E {i} (\<lambda>_. B))"
1.182 +      by (auto simp: emb_def infprod_algebra_def generator_def Pi_iff)
1.183 +    with i show "A \<in> sigma_sets ?O ?G"
1.184 +      by (intro sigma_sets.Basic UN_I[where a="{i}"]) auto
1.185 +  qed
1.186 +  finally show "sets (Pi\<^isub>P I M) = sets ?S"
1.187 +    by (simp add: sets_sigma)
1.188 +qed simp_all
1.189 +
1.190 +lemma (in product_prob_space) measurable_into_infprod_algebra:
1.191 +  assumes "sigma_algebra N"
1.192 +  assumes f: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. f x i) \<in> measurable N (M i)"
1.193 +  assumes ext: "\<And>x. x \<in> space N \<Longrightarrow> f x \<in> extensional I"
1.194 +  shows "f \<in> measurable N (Pi\<^isub>P I M)"
1.195 +proof -
1.196 +  interpret N: sigma_algebra N by fact
1.197 +  have f_in: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. f x i) \<in> space N \<rightarrow> space (M i)"
1.198 +    using f by (auto simp: measurable_def)
1.199 +  { fix i A assume i: "i \<in> I" "A \<in> sets (M i)"
1.200 +    then have "f -` (\<lambda>x. x i) -` A \<inter> f -` space infprod_algebra \<inter> space N = (\<lambda>x. f x i) -` A \<inter> space N"
1.201 +      using f_in ext by (auto simp: infprod_algebra_def generator_def)
1.202 +    also have "\<dots> \<in> sets N"
1.203 +      by (rule measurable_sets f i)+
1.204 +    finally have "f -` (\<lambda>x. x i) -` A \<inter> f -` space infprod_algebra \<inter> space N \<in> sets N" . }
1.205 +  with f_in ext show ?thesis
1.206 +    by (subst infprod_algebra_alt2)
1.207 +       (auto intro!: N.measurable_sigma simp: Pi_iff infprod_algebra_def generator_def)
1.208 +qed
1.209 +
1.210 +subsection {* Sequence space *}
1.211 +
1.212 +locale sequence_space = product_prob_space M "UNIV :: nat set" for M
1.213 +
1.214 +lemma (in sequence_space) infprod_in_sets[intro]:
1.215 +  fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)"
1.216 +  shows "Pi UNIV E \<in> sets (Pi\<^isub>P UNIV M)"
1.217 +proof -
1.218 +  have "Pi UNIV E = (\<Inter>i. emb UNIV {..i} (\<Pi>\<^isub>E j\<in>{..i}. E j))"
1.219 +    using E E[THEN M.sets_into_space]
1.220 +    by (auto simp: emb_def Pi_iff extensional_def) blast
1.221 +  with E show ?thesis
1.222 +    by (auto intro: emb_in_infprod_algebra)
1.223 +qed
1.224 +
1.225 +lemma (in sequence_space) measure_infprod:
1.226 +  fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)"
1.227 +  shows "(\<lambda>n. \<Prod>i\<le>n. M.\<mu>' i (E i)) ----> \<mu>' (Pi UNIV E)"
1.228 +proof -
1.229 +  let "?E n" = "emb UNIV {..n} (Pi\<^isub>E {.. n} E)"
1.230 +  { fix n :: nat
1.231 +    interpret n: finite_product_prob_space M "{..n}" by default auto
1.232 +    have "(\<Prod>i\<le>n. M.\<mu>' i (E i)) = n.\<mu>' (Pi\<^isub>E {.. n} E)"
1.233 +      using E by (subst n.finite_measure_times) auto
1.234 +    also have "\<dots> = \<mu>' (?E n)"
1.235 +      using E by (intro finite_measure_infprod_emb[symmetric]) auto
1.236 +    finally have "(\<Prod>i\<le>n. M.\<mu>' i (E i)) = \<mu>' (?E n)" . }
1.237 +  moreover have "Pi UNIV E = (\<Inter>n. ?E n)"
1.238 +    using E E[THEN M.sets_into_space]
1.239 +    by (auto simp: emb_def extensional_def Pi_iff) blast
1.240 +  moreover have "range ?E \<subseteq> sets (Pi\<^isub>P UNIV M)"
1.241 +    using E by auto
1.242 +  moreover have "decseq ?E"
1.243 +    by (auto simp: emb_def Pi_iff decseq_def)
1.244 +  ultimately show ?thesis
1.245 +    by (simp add: finite_continuity_from_above)
1.246 +qed
1.247 +
1.248  end
1.249 \ No newline at end of file
```
```     2.1 --- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Wed Apr 06 10:58:18 2011 +0200
2.2 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Wed Apr 06 13:08:44 2011 +0200
2.3 @@ -95,11 +95,11 @@
2.4  lemma zero_notin_Suc_image[simp]: "0 \<notin> Suc ` A"
2.5    by auto
2.6
2.7 -definition extensional :: "'b \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) set" where
2.8 -  "extensional d A = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = d}"
2.9 +definition extensionalD :: "'b \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) set" where
2.10 +  "extensionalD d A = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = d}"
2.11
2.12 -lemma extensional_empty[simp]: "extensional d {} = {\<lambda>x. d}"
2.13 -  unfolding extensional_def by (simp add: set_eq_iff fun_eq_iff)
2.14 +lemma extensionalD_empty[simp]: "extensionalD d {} = {\<lambda>x. d}"
2.15 +  unfolding extensionalD_def by (simp add: set_eq_iff fun_eq_iff)
2.16
2.17  lemma funset_eq_UN_fun_upd_I:
2.18    assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
2.19 @@ -121,16 +121,16 @@
2.20    from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
2.21  qed
2.22
2.23 -lemma extensional_insert[simp]:
2.24 +lemma extensionalD_insert[simp]:
2.25    assumes "a \<notin> A"
2.26 -  shows "extensional d (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional d A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
2.27 +  shows "extensionalD d (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensionalD d A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
2.28    apply (rule funset_eq_UN_fun_upd_I)
2.29    using assms
2.30 -  by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def)
2.31 +  by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensionalD_def)
2.32
2.33 -lemma finite_extensional_funcset[simp, intro]:
2.34 +lemma finite_extensionalD_funcset[simp, intro]:
2.35    assumes "finite A" "finite B"
2.36 -  shows "finite (extensional d A \<inter> (A \<rightarrow> B))"
2.37 +  shows "finite (extensionalD d A \<inter> (A \<rightarrow> B))"
2.38    using assms by induct auto
2.39
2.40  lemma fun_upd_eq_iff: "f(a := b) = g(a := b') \<longleftrightarrow> b = b' \<and> f(a := d) = g(a := d)"
2.41 @@ -138,27 +138,27 @@
2.42
2.43  lemma card_funcset:
2.44    assumes "finite A" "finite B"
2.45 -  shows "card (extensional d A \<inter> (A \<rightarrow> B)) = card B ^ card A"
2.46 +  shows "card (extensionalD d A \<inter> (A \<rightarrow> B)) = card B ^ card A"
2.47  using `finite A` proof induct
2.48 -  case (insert a A) thus ?case unfolding extensional_insert[OF `a \<notin> A`]
2.49 +  case (insert a A) thus ?case unfolding extensionalD_insert[OF `a \<notin> A`]
2.50    proof (subst card_UN_disjoint, safe, simp_all)
2.51 -    show "finite (extensional d A \<inter> (A \<rightarrow> B))" "\<And>f. finite (fun_upd f a ` B)"
2.52 +    show "finite (extensionalD d A \<inter> (A \<rightarrow> B))" "\<And>f. finite (fun_upd f a ` B)"
2.53        using `finite B` `finite A` by simp_all
2.54    next
2.55      fix f g b b' assume "f \<noteq> g" and eq: "f(a := b) = g(a := b')" and
2.56 -      ext: "f \<in> extensional d A" "g \<in> extensional d A"
2.57 +      ext: "f \<in> extensionalD d A" "g \<in> extensionalD d A"
2.58      have "f a = d" "g a = d"
2.59 -      using ext `a \<notin> A` by (auto simp add: extensional_def)
2.60 +      using ext `a \<notin> A` by (auto simp add: extensionalD_def)
2.61      with `f \<noteq> g` eq show False unfolding fun_upd_eq_iff[of _ _ b _ _ d]
2.62        by (auto simp: fun_upd_idem fun_upd_eq_iff)
2.63    next
2.64 -    { fix f assume "f \<in> extensional d A \<inter> (A \<rightarrow> B)"
2.65 +    { fix f assume "f \<in> extensionalD d A \<inter> (A \<rightarrow> B)"
2.66        have "card (fun_upd f a ` B) = card B"
2.67        proof (auto intro!: card_image inj_onI)
2.68          fix b b' assume "f(a := b) = f(a := b')"
2.69          from fun_upd_eq_iff[THEN iffD1, OF this] show "b = b'" by simp
2.70        qed }
2.71 -    then show "(\<Sum>i\<in>extensional d A \<inter> (A \<rightarrow> B). card (fun_upd i a ` B)) = card B * card B ^ card A"
2.72 +    then show "(\<Sum>i\<in>extensionalD d A \<inter> (A \<rightarrow> B). card (fun_upd i a ` B)) = card B * card B ^ card A"
2.73        using insert by simp
2.74    qed
2.75  qed simp
2.76 @@ -301,11 +301,11 @@
2.77
2.78  lemma card_T_bound: "card ((t\<circ>OB)`msgs) \<le> (n+1)^card observations"
2.79  proof -
2.80 -  have "(t\<circ>OB)`msgs \<subseteq> extensional 0 observations \<inter> (observations \<rightarrow> {.. n})"
2.81 -    unfolding observations_def extensional_def OB_def msgs_def
2.82 +  have "(t\<circ>OB)`msgs \<subseteq> extensionalD 0 observations \<inter> (observations \<rightarrow> {.. n})"
2.83 +    unfolding observations_def extensionalD_def OB_def msgs_def
2.84      by (auto simp add: t_def comp_def image_iff)
2.85 -  with finite_extensional_funcset
2.86 -  have "card ((t\<circ>OB)`msgs) \<le> card (extensional 0 observations \<inter> (observations \<rightarrow> {.. n}))"
2.87 +  with finite_extensionalD_funcset
2.88 +  have "card ((t\<circ>OB)`msgs) \<le> card (extensionalD 0 observations \<inter> (observations \<rightarrow> {.. n}))"
2.89      by (rule card_mono) auto
2.90    also have "\<dots> = (n + 1) ^ card observations"
2.91      by (subst card_funcset) auto
```