author | immler |
Tue, 18 Mar 2014 10:12:57 +0100 | |
changeset 56188 | 0268784f60da |
parent 56045 | 1ca060139a59 |
child 56993 | e5366291d6aa |
permissions | -rw-r--r-- |
50530 | 1 |
(* Title: HOL/Probability/Measurable.thy |
50387 | 2 |
Author: Johannes Hölzl <hoelzl@in.tum.de> |
3 |
*) |
|
4 |
theory Measurable |
|
56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
5 |
imports |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
6 |
Sigma_Algebra |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
7 |
"~~/src/HOL/Library/Order_Continuity" |
50387 | 8 |
begin |
9 |
||
56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
10 |
hide_const (open) Order_Continuity.continuous |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
11 |
|
50387 | 12 |
subsection {* Measurability prover *} |
13 |
||
14 |
lemma (in algebra) sets_Collect_finite_All: |
|
15 |
assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" |
|
16 |
shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M" |
|
17 |
proof - |
|
18 |
have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (if S = {} then \<Omega> else \<Inter>i\<in>S. {x\<in>\<Omega>. P i x})" |
|
19 |
by auto |
|
20 |
with assms show ?thesis by (auto intro!: sets_Collect_finite_All') |
|
21 |
qed |
|
22 |
||
23 |
abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))" |
|
24 |
||
25 |
lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M" |
|
26 |
proof |
|
27 |
assume "pred M P" |
|
28 |
then have "P -` {True} \<inter> space M \<in> sets M" |
|
29 |
by (auto simp: measurable_count_space_eq2) |
|
30 |
also have "P -` {True} \<inter> space M = {x\<in>space M. P x}" by auto |
|
31 |
finally show "{x\<in>space M. P x} \<in> sets M" . |
|
32 |
next |
|
33 |
assume P: "{x\<in>space M. P x} \<in> sets M" |
|
34 |
moreover |
|
35 |
{ fix X |
|
36 |
have "X \<in> Pow (UNIV :: bool set)" by simp |
|
37 |
then have "P -` X \<inter> space M = {x\<in>space M. ((X = {True} \<longrightarrow> P x) \<and> (X = {False} \<longrightarrow> \<not> P x) \<and> X \<noteq> {})}" |
|
38 |
unfolding UNIV_bool Pow_insert Pow_empty by auto |
|
39 |
then have "P -` X \<inter> space M \<in> sets M" |
|
40 |
by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) } |
|
41 |
then show "pred M P" |
|
42 |
by (auto simp: measurable_def) |
|
43 |
qed |
|
44 |
||
45 |
lemma pred_sets1: "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> f \<in> measurable N M \<Longrightarrow> pred N (\<lambda>x. P (f x))" |
|
46 |
by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def) |
|
47 |
||
48 |
lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)" |
|
49 |
by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric]) |
|
50 |
||
51 |
ML_file "measurable.ML" |
|
52 |
||
53043
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
53 |
attribute_setup measurable = {* |
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
54 |
Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false -- |
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
55 |
Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete)) |
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
56 |
(false, Measurable.Concrete) >> (Thm.declaration_attribute o Measurable.add_thm)) |
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
57 |
*} "declaration of measurability theorems" |
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
58 |
|
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
59 |
attribute_setup measurable_dest = {* |
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
60 |
Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_dest)) |
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
61 |
*} "add dest rule for measurability prover" |
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
62 |
|
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
63 |
attribute_setup measurable_app = {* |
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
64 |
Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_app)) |
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
65 |
*} "add application rule for measurability prover" |
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
66 |
|
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
67 |
method_setup measurable = {* |
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
68 |
Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => Measurable.measurable_tac ctxt facts))) |
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
69 |
*} "measurability prover" |
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
50530
diff
changeset
|
70 |
|
50387 | 71 |
simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *} |
72 |
||
73 |
declare |
|
74 |
measurable_compose_rev[measurable_dest] |
|
75 |
pred_sets1[measurable_dest] |
|
76 |
pred_sets2[measurable_dest] |
|
77 |
sets.sets_into_space[measurable_dest] |
|
78 |
||
79 |
declare |
|
80 |
sets.top[measurable] |
|
81 |
sets.empty_sets[measurable (raw)] |
|
82 |
sets.Un[measurable (raw)] |
|
83 |
sets.Diff[measurable (raw)] |
|
84 |
||
85 |
declare |
|
86 |
measurable_count_space[measurable (raw)] |
|
87 |
measurable_ident[measurable (raw)] |
|
88 |
measurable_ident_sets[measurable (raw)] |
|
89 |
measurable_const[measurable (raw)] |
|
90 |
measurable_If[measurable (raw)] |
|
91 |
measurable_comp[measurable (raw)] |
|
92 |
measurable_sets[measurable (raw)] |
|
93 |
||
94 |
lemma predE[measurable (raw)]: |
|
95 |
"pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M" |
|
96 |
unfolding pred_def . |
|
97 |
||
98 |
lemma pred_intros_imp'[measurable (raw)]: |
|
99 |
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)" |
|
100 |
by (cases K) auto |
|
101 |
||
102 |
lemma pred_intros_conj1'[measurable (raw)]: |
|
103 |
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)" |
|
104 |
by (cases K) auto |
|
105 |
||
106 |
lemma pred_intros_conj2'[measurable (raw)]: |
|
107 |
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)" |
|
108 |
by (cases K) auto |
|
109 |
||
110 |
lemma pred_intros_disj1'[measurable (raw)]: |
|
111 |
"(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)" |
|
112 |
by (cases K) auto |
|
113 |
||
114 |
lemma pred_intros_disj2'[measurable (raw)]: |
|
115 |
"(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)" |
|
116 |
by (cases K) auto |
|
117 |
||
118 |
lemma pred_intros_logic[measurable (raw)]: |
|
119 |
"pred M (\<lambda>x. x \<in> space M)" |
|
120 |
"pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)" |
|
121 |
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)" |
|
122 |
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)" |
|
123 |
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)" |
|
124 |
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)" |
|
125 |
"pred M (\<lambda>x. f x \<in> UNIV)" |
|
126 |
"pred M (\<lambda>x. f x \<in> {})" |
|
127 |
"pred M (\<lambda>x. P' (f x) x) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {y. P' y x})" |
|
128 |
"pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))" |
|
129 |
"pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) - (B x))" |
|
130 |
"pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<inter> (B x))" |
|
131 |
"pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<union> (B x))" |
|
132 |
"pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))" |
|
133 |
by (auto simp: iff_conv_conj_imp pred_def) |
|
134 |
||
135 |
lemma pred_intros_countable[measurable (raw)]: |
|
136 |
fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool" |
|
137 |
shows |
|
138 |
"(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)" |
|
139 |
"(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)" |
|
140 |
by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def) |
|
141 |
||
142 |
lemma pred_intros_countable_bounded[measurable (raw)]: |
|
143 |
fixes X :: "'i :: countable set" |
|
144 |
shows |
|
145 |
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>X. N x i))" |
|
146 |
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>X. N x i))" |
|
147 |
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>X. P x i)" |
|
148 |
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>X. P x i)" |
|
149 |
by (auto simp: Bex_def Ball_def) |
|
150 |
||
151 |
lemma pred_intros_finite[measurable (raw)]: |
|
152 |
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>I. N x i))" |
|
153 |
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>I. N x i))" |
|
154 |
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>I. P x i)" |
|
155 |
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>I. P x i)" |
|
156 |
by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def) |
|
157 |
||
158 |
lemma countable_Un_Int[measurable (raw)]: |
|
159 |
"(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M" |
|
160 |
"I \<noteq> {} \<Longrightarrow> (\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Inter>i\<in>I. N i) \<in> sets M" |
|
161 |
by auto |
|
162 |
||
163 |
declare |
|
164 |
finite_UN[measurable (raw)] |
|
165 |
finite_INT[measurable (raw)] |
|
166 |
||
167 |
lemma sets_Int_pred[measurable (raw)]: |
|
168 |
assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)" |
|
169 |
shows "A \<inter> B \<in> sets M" |
|
170 |
proof - |
|
171 |
have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto |
|
172 |
also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B" |
|
173 |
using space by auto |
|
174 |
finally show ?thesis . |
|
175 |
qed |
|
176 |
||
177 |
lemma [measurable (raw generic)]: |
|
178 |
assumes f: "f \<in> measurable M N" and c: "c \<in> space N \<Longrightarrow> {c} \<in> sets N" |
|
179 |
shows pred_eq_const1: "pred M (\<lambda>x. f x = c)" |
|
180 |
and pred_eq_const2: "pred M (\<lambda>x. c = f x)" |
|
181 |
proof - |
|
182 |
show "pred M (\<lambda>x. f x = c)" |
|
183 |
proof cases |
|
184 |
assume "c \<in> space N" |
|
185 |
with measurable_sets[OF f c] show ?thesis |
|
186 |
by (auto simp: Int_def conj_commute pred_def) |
|
187 |
next |
|
188 |
assume "c \<notin> space N" |
|
189 |
with f[THEN measurable_space] have "{x \<in> space M. f x = c} = {}" by auto |
|
190 |
then show ?thesis by (auto simp: pred_def cong: conj_cong) |
|
191 |
qed |
|
192 |
then show "pred M (\<lambda>x. c = f x)" |
|
193 |
by (simp add: eq_commute) |
|
194 |
qed |
|
195 |
||
196 |
lemma pred_le_const[measurable (raw generic)]: |
|
197 |
assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)" |
|
198 |
using measurable_sets[OF f c] |
|
199 |
by (auto simp: Int_def conj_commute eq_commute pred_def) |
|
200 |
||
201 |
lemma pred_const_le[measurable (raw generic)]: |
|
202 |
assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)" |
|
203 |
using measurable_sets[OF f c] |
|
204 |
by (auto simp: Int_def conj_commute eq_commute pred_def) |
|
205 |
||
206 |
lemma pred_less_const[measurable (raw generic)]: |
|
207 |
assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)" |
|
208 |
using measurable_sets[OF f c] |
|
209 |
by (auto simp: Int_def conj_commute eq_commute pred_def) |
|
210 |
||
211 |
lemma pred_const_less[measurable (raw generic)]: |
|
212 |
assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)" |
|
213 |
using measurable_sets[OF f c] |
|
214 |
by (auto simp: Int_def conj_commute eq_commute pred_def) |
|
215 |
||
216 |
declare |
|
217 |
sets.Int[measurable (raw)] |
|
218 |
||
219 |
lemma pred_in_If[measurable (raw)]: |
|
220 |
"(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow> |
|
221 |
pred M (\<lambda>x. x \<in> (if P then A x else B x))" |
|
222 |
by auto |
|
223 |
||
224 |
lemma sets_range[measurable_dest]: |
|
225 |
"A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M" |
|
226 |
by auto |
|
227 |
||
228 |
lemma pred_sets_range[measurable_dest]: |
|
229 |
"A ` I \<subseteq> sets N \<Longrightarrow> i \<in> I \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)" |
|
230 |
using pred_sets2[OF sets_range] by auto |
|
231 |
||
232 |
lemma sets_All[measurable_dest]: |
|
233 |
"\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)" |
|
234 |
by auto |
|
235 |
||
236 |
lemma pred_sets_All[measurable_dest]: |
|
237 |
"\<forall>i. A i \<in> sets (N i) \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)" |
|
238 |
using pred_sets2[OF sets_All, of A N f] by auto |
|
239 |
||
240 |
lemma sets_Ball[measurable_dest]: |
|
241 |
"\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)" |
|
242 |
by auto |
|
243 |
||
244 |
lemma pred_sets_Ball[measurable_dest]: |
|
245 |
"\<forall>i\<in>I. A i \<in> sets (N i) \<Longrightarrow> i\<in>I \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)" |
|
246 |
using pred_sets2[OF sets_Ball, of _ _ _ f] by auto |
|
247 |
||
248 |
lemma measurable_finite[measurable (raw)]: |
|
249 |
fixes S :: "'a \<Rightarrow> nat set" |
|
250 |
assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M" |
|
251 |
shows "pred M (\<lambda>x. finite (S x))" |
|
252 |
unfolding finite_nat_set_iff_bounded by (simp add: Ball_def) |
|
253 |
||
254 |
lemma measurable_Least[measurable]: |
|
255 |
assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q |
|
256 |
shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)" |
|
257 |
unfolding measurable_def by (safe intro!: sets_Least) simp_all |
|
258 |
||
259 |
lemma measurable_count_space_insert[measurable (raw)]: |
|
260 |
"s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)" |
|
261 |
by simp |
|
262 |
||
56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
263 |
subsection {* Measurability for (co)inductive predicates *} |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
264 |
|
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
265 |
lemma measurable_lfp: |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
266 |
assumes "Order_Continuity.continuous F" |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
267 |
assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)" |
56045 | 268 |
shows "pred M (lfp F)" |
56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
269 |
proof - |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
270 |
{ fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. False) x)" |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
271 |
by (induct i) (auto intro!: *) } |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
272 |
then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x)" |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
273 |
by measurable |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
274 |
also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x) = (SUP i. (F ^^ i) bot)" |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
275 |
by (auto simp add: bot_fun_def) |
56045 | 276 |
also have "\<dots> = lfp F" |
277 |
by (rule continuous_lfp[symmetric]) fact |
|
56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
278 |
finally show ?thesis . |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
279 |
qed |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
280 |
|
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
281 |
lemma measurable_gfp: |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
282 |
assumes "Order_Continuity.down_continuous F" |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
283 |
assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)" |
56045 | 284 |
shows "pred M (gfp F)" |
56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
285 |
proof - |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
286 |
{ fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. True) x)" |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
287 |
by (induct i) (auto intro!: *) } |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
288 |
then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x)" |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
289 |
by measurable |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
290 |
also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x) = (INF i. (F ^^ i) top)" |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
291 |
by (auto simp add: top_fun_def) |
56045 | 292 |
also have "\<dots> = gfp F" |
293 |
by (rule down_continuous_gfp[symmetric]) fact |
|
56021
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
294 |
finally show ?thesis . |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
295 |
qed |
e0c9d76c2a6d
add measurability rule for (co)inductive predicates
hoelzl
parents:
53043
diff
changeset
|
296 |
|
50387 | 297 |
hide_const (open) pred |
298 |
||
299 |
end |