summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Measurable.thy

changeset 60172 | 423273355b55 |

parent 59361 | fd5da2434be4 |

child 61808 | fc1556774cfe |

1.1 --- a/src/HOL/Probability/Measurable.thy Mon May 04 16:01:36 2015 +0200 1.2 +++ b/src/HOL/Probability/Measurable.thy Mon May 04 17:35:31 2015 +0200 1.3 @@ -7,8 +7,6 @@ 1.4 "~~/src/HOL/Library/Order_Continuity" 1.5 begin 1.6 1.7 -hide_const (open) Order_Continuity.continuous 1.8 - 1.9 subsection {* Measurability prover *} 1.10 1.11 lemma (in algebra) sets_Collect_finite_All: 1.12 @@ -425,7 +423,7 @@ 1.13 lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]: 1.14 fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})" 1.15 assumes "P M" 1.16 - assumes F: "Order_Continuity.continuous F" 1.17 + assumes F: "sup_continuous F" 1.18 assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> A \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)" 1.19 shows "lfp F \<in> measurable M (count_space UNIV)" 1.20 proof - 1.21 @@ -434,13 +432,13 @@ 1.22 then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> measurable M (count_space UNIV)" 1.23 by measurable 1.24 also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = lfp F" 1.25 - by (subst continuous_lfp) (auto intro: F) 1.26 + by (subst sup_continuous_lfp) (auto intro: F) 1.27 finally show ?thesis . 1.28 qed 1.29 1.30 lemma measurable_lfp: 1.31 fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})" 1.32 - assumes F: "Order_Continuity.continuous F" 1.33 + assumes F: "sup_continuous F" 1.34 assumes *: "\<And>A. A \<in> measurable M (count_space UNIV) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)" 1.35 shows "lfp F \<in> measurable M (count_space UNIV)" 1.36 by (coinduction rule: measurable_lfp_coinduct[OF _ F]) (blast intro: *) 1.37 @@ -448,7 +446,7 @@ 1.38 lemma measurable_gfp_coinduct[consumes 1, case_names continuity step]: 1.39 fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})" 1.40 assumes "P M" 1.41 - assumes F: "Order_Continuity.down_continuous F" 1.42 + assumes F: "inf_continuous F" 1.43 assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> A \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)" 1.44 shows "gfp F \<in> measurable M (count_space UNIV)" 1.45 proof - 1.46 @@ -457,13 +455,13 @@ 1.47 then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> measurable M (count_space UNIV)" 1.48 by measurable 1.49 also have "(\<lambda>x. INF i. (F ^^ i) top x) = gfp F" 1.50 - by (subst down_continuous_gfp) (auto intro: F) 1.51 + by (subst inf_continuous_gfp) (auto intro: F) 1.52 finally show ?thesis . 1.53 qed 1.54 1.55 lemma measurable_gfp: 1.56 fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})" 1.57 - assumes F: "Order_Continuity.down_continuous F" 1.58 + assumes F: "inf_continuous F" 1.59 assumes *: "\<And>A. A \<in> measurable M (count_space UNIV) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)" 1.60 shows "gfp F \<in> measurable M (count_space UNIV)" 1.61 by (coinduction rule: measurable_gfp_coinduct[OF _ F]) (blast intro: *) 1.62 @@ -471,7 +469,7 @@ 1.63 lemma measurable_lfp2_coinduct[consumes 1, case_names continuity step]: 1.64 fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})" 1.65 assumes "P M s" 1.66 - assumes F: "Order_Continuity.continuous F" 1.67 + assumes F: "sup_continuous F" 1.68 assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> A t \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A s \<in> measurable M (count_space UNIV)" 1.69 shows "lfp F s \<in> measurable M (count_space UNIV)" 1.70 proof - 1.71 @@ -480,14 +478,14 @@ 1.72 then have "(\<lambda>x. SUP i. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)" 1.73 by measurable 1.74 also have "(\<lambda>x. SUP i. (F ^^ i) bot s x) = lfp F s" 1.75 - by (subst continuous_lfp) (auto simp: F) 1.76 + by (subst sup_continuous_lfp) (auto simp: F) 1.77 finally show ?thesis . 1.78 qed 1.79 1.80 lemma measurable_gfp2_coinduct[consumes 1, case_names continuity step]: 1.81 fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})" 1.82 assumes "P M s" 1.83 - assumes F: "Order_Continuity.down_continuous F" 1.84 + assumes F: "inf_continuous F" 1.85 assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> A t \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A s \<in> measurable M (count_space UNIV)" 1.86 shows "gfp F s \<in> measurable M (count_space UNIV)" 1.87 proof - 1.88 @@ -496,7 +494,7 @@ 1.89 then have "(\<lambda>x. INF i. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)" 1.90 by measurable 1.91 also have "(\<lambda>x. INF i. (F ^^ i) top s x) = gfp F s" 1.92 - by (subst down_continuous_gfp) (auto simp: F) 1.93 + by (subst inf_continuous_gfp) (auto simp: F) 1.94 finally show ?thesis . 1.95 qed 1.96