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