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.7 -hide_const (open) Order_Continuity.continuous
1.8 -
1.9  subsection {* Measurability prover *}
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.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.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.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