--- a/NEWS Wed Apr 15 15:10:01 2015 +0200
+++ b/NEWS Wed Apr 15 16:48:24 2015 +0200
@@ -77,6 +77,9 @@
* Old graph browser (Java/AWT 1.1) is superseded by improved graphview
panel, which also produces PDF output without external tools.
+* Improved scheduling for asynchronous print commands (e.g. provers
+managed by the Sledgehammer panel) wrt. ongoing document processing.
+
*** Document preparation ***
--- a/etc/options Wed Apr 15 15:10:01 2015 +0200
+++ b/etc/options Wed Apr 15 16:48:24 2015 +0200
@@ -101,6 +101,9 @@
public option ML_exception_trace : bool = false
-- "ML exception trace for toplevel command execution"
+public option ML_statistics : bool = true
+ -- "ML runtime system statistics"
+
section "Editor Reactivity"
--- a/src/HOL/Complete_Partial_Order.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Complete_Partial_Order.thy Wed Apr 15 16:48:24 2015 +0200
@@ -53,6 +53,20 @@
lemma chain_empty: "chain ord {}"
by(simp add: chain_def)
+lemma chain_equality: "chain op = A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)"
+by(auto simp add: chain_def)
+
+lemma chain_subset:
+ "\<lbrakk> chain ord A; B \<subseteq> A \<rbrakk>
+ \<Longrightarrow> chain ord B"
+by(rule chainI)(blast dest: chainD)
+
+lemma chain_imageI:
+ assumes chain: "chain le_a Y"
+ and mono: "\<And>x y. \<lbrakk> x \<in> Y; y \<in> Y; le_a x y \<rbrakk> \<Longrightarrow> le_b (f x) (f y)"
+ shows "chain le_b (f ` Y)"
+by(blast intro: chainI dest: chainD[OF chain] mono)
+
subsection {* Chain-complete partial orders *}
text {*
@@ -65,6 +79,12 @@
assumes ccpo_Sup_least: "\<lbrakk>chain (op \<le>) A; \<And>x. x \<in> A \<Longrightarrow> x \<le> z\<rbrakk> \<Longrightarrow> Sup A \<le> z"
begin
+lemma chain_singleton: "Complete_Partial_Order.chain op \<le> {x}"
+by(rule chainI) simp
+
+lemma ccpo_Sup_singleton [simp]: "\<Squnion>{x} = x"
+by(rule antisym)(auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)
+
subsection {* Transfinite iteration of a function *}
inductive_set iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set"
--- a/src/HOL/Extraction.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Extraction.thy Wed Apr 15 16:48:24 2015 +0200
@@ -31,7 +31,8 @@
induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
induct_atomize induct_atomize' induct_rulify induct_rulify'
induct_rulify_fallback induct_trueI
- True_implies_equals TrueE
+ True_implies_equals implies_True_equals TrueE
+ False_implies_equals
lemmas [extraction_expand_def] =
HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def
--- a/src/HOL/Library/Countable_Set.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Library/Countable_Set.thy Wed Apr 15 16:48:24 2015 +0200
@@ -247,6 +247,13 @@
shows "countable ((X ^^ i) `` Y)"
using Y by (induct i arbitrary: Y) (auto simp: relcomp_Image Image_X)
+lemma countable_funpow:
+ fixes f :: "'a set \<Rightarrow> 'a set"
+ assumes "\<And>A. countable A \<Longrightarrow> countable (f A)"
+ and "countable A"
+ shows "countable ((f ^^ n) A)"
+by(induction n)(simp_all add: assms)
+
lemma countable_rtrancl:
"(\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)) \<Longrightarrow> countable Y \<Longrightarrow> countable (X^* `` Y)"
unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow)
@@ -276,6 +283,9 @@
"countable T \<Longrightarrow> countable {A. finite A \<and> A \<subseteq> T}"
unfolding Collect_finite_subset_eq_lists by auto
+lemma countable_set_option [simp]: "countable (set_option x)"
+by(cases x) auto
+
subsection {* Misc lemmas *}
lemma countable_all:
--- a/src/HOL/Library/Countable_Set_Type.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Library/Countable_Set_Type.thy Wed Apr 15 16:48:24 2015 +0200
@@ -341,7 +341,30 @@
lemmas cin_mono = in_mono[Transfer.transferred]
lemmas cLeast_mono = Least_mono[Transfer.transferred]
lemmas cequalityI = equalityI[Transfer.transferred]
-
+lemmas cUnion_cimage_eq [simp] = Union_image_eq[Transfer.transferred]
+lemmas cUN_iff [simp] = UN_iff[Transfer.transferred]
+lemmas cUN_I [intro] = UN_I[Transfer.transferred]
+lemmas cUN_E [elim!] = UN_E[Transfer.transferred]
+lemmas cimage_eq_cUN = image_eq_UN[Transfer.transferred]
+lemmas cUN_upper = UN_upper[Transfer.transferred]
+lemmas cUN_least = UN_least[Transfer.transferred]
+lemmas cUN_cinsert_distrib = UN_insert_distrib[Transfer.transferred]
+lemmas cUN_empty [simp] = UN_empty[Transfer.transferred]
+lemmas cUN_empty2 [simp] = UN_empty2[Transfer.transferred]
+lemmas cUN_absorb = UN_absorb[Transfer.transferred]
+lemmas cUN_cinsert [simp] = UN_insert[Transfer.transferred]
+lemmas cUN_cUn [simp] = UN_Un[Transfer.transferred]
+lemmas cUN_cUN_flatten = UN_UN_flatten[Transfer.transferred]
+lemmas cUN_csubset_iff = UN_subset_iff[Transfer.transferred]
+lemmas cUN_constant [simp] = UN_constant[Transfer.transferred]
+lemmas cimage_cUnion = image_Union[Transfer.transferred]
+lemmas cUNION_cempty_conv [simp] = UNION_empty_conv[Transfer.transferred]
+lemmas cBall_cUN = ball_UN[Transfer.transferred]
+lemmas cBex_cUN = bex_UN[Transfer.transferred]
+lemmas cUn_eq_cUN = Un_eq_UN[Transfer.transferred]
+lemmas cUN_mono = UN_mono[Transfer.transferred]
+lemmas cimage_cUN = image_UN[Transfer.transferred]
+lemmas cUN_csingleton [simp] = UN_singleton[Transfer.transferred]
subsection {* Additional lemmas*}
@@ -395,6 +418,11 @@
apply (rule equal_intr_rule)
by (transfer, simp)+
+subsubsection {* @{const cUnion} *}
+
+lemma cUNION_cimage: "cUNION (cimage f A) g = cUNION A (g \<circ> f)"
+including cset.lifting by transfer auto
+
subsection {* Setup for Lifting/Transfer *}
@@ -415,6 +443,14 @@
(\<forall>t. cin t b \<longrightarrow> (\<exists>u. cin u a \<and> R u t))"
by transfer(auto simp add: rel_set_def)
+lemma rel_cset_cUNION:
+ "\<lbrakk> rel_cset Q A B; rel_fun Q (rel_cset R) f g \<rbrakk>
+ \<Longrightarrow> rel_cset R (cUNION A f) (cUNION B g)"
+unfolding rel_fun_def by transfer(erule rel_set_UNION, simp add: rel_fun_def)
+
+lemma rel_cset_csingle_iff [simp]: "rel_cset R (csingle x) (csingle y) \<longleftrightarrow> R x y"
+by transfer(auto simp add: rel_set_def)
+
subsubsection {* Transfer rules for the Transfer package *}
text {* Unconditional transfer rules *}
--- a/src/HOL/Library/Extended_Real.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy Wed Apr 15 16:48:24 2015 +0200
@@ -298,6 +298,10 @@
end
+lemma ereal_0_plus [simp]: "ereal 0 + x = x"
+ and plus_ereal_0 [simp]: "x + ereal 0 = x"
+by(simp_all add: zero_ereal_def[symmetric])
+
instance ereal :: numeral ..
lemma real_of_ereal_0[simp]: "real (0::ereal) = 0"
@@ -1286,6 +1290,9 @@
shows "real (a - b) = (if \<bar>a\<bar> = \<infinity> \<or> \<bar>b\<bar> = \<infinity> then 0 else real a - real b)"
by (cases rule: ereal2_cases[of a b]) auto
+lemma real_of_ereal_minus': "\<bar>x\<bar> = \<infinity> \<longleftrightarrow> \<bar>y\<bar> = \<infinity> \<Longrightarrow> real x - real y = real (x - y :: ereal)"
+by(subst real_of_ereal_minus) auto
+
lemma ereal_diff_positive:
fixes a b :: ereal shows "a \<le> b \<Longrightarrow> 0 \<le> b - a"
by (cases rule: ereal2_cases[of a b]) auto
@@ -1428,6 +1435,14 @@
shows "0 < inverse x \<longleftrightarrow> x \<noteq> \<infinity> \<and> 0 \<le> x"
by (cases x) auto
+lemma ereal_inverse_le_0_iff:
+ fixes x :: ereal
+ shows "inverse x \<le> 0 \<longleftrightarrow> x < 0 \<or> x = \<infinity>"
+ by(cases x) auto
+
+lemma ereal_divide_eq_0_iff: "x / y = 0 \<longleftrightarrow> x = 0 \<or> \<bar>y :: ereal\<bar> = \<infinity>"
+by(cases x y rule: ereal2_cases) simp_all
+
lemma ereal_mult_less_right:
fixes a b c :: ereal
assumes "b * a < c * a"
@@ -1971,7 +1986,7 @@
assumes f: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" and c: "0 \<le> c"
shows "(SUP i:I. c * f i) = c * (SUP i:I. f i)"
proof cases
- assume "(SUP i:I. f i) = 0"
+ assume "(SUP i: I. f i) = 0"
moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = 0"
by (metis SUP_upper f antisym)
ultimately show ?thesis
@@ -2646,6 +2661,38 @@
finally show "(SUP P:?F. ?INF P f + (SUP P:?F. ?INF P g)) \<le> (SUP P:?F. INF x:Collect P. f x + g x)" .
qed
+lemma Sup_ereal_mult_right':
+ assumes nonempty: "Y \<noteq> {}"
+ and x: "x \<ge> 0"
+ shows "(SUP i:Y. f i) * ereal x = (SUP i:Y. f i * ereal x)" (is "?lhs = ?rhs")
+proof(cases "x = 0")
+ case True thus ?thesis by(auto simp add: nonempty zero_ereal_def[symmetric])
+next
+ case False
+ show ?thesis
+ proof(rule antisym)
+ show "?rhs \<le> ?lhs"
+ by(rule SUP_least)(simp add: ereal_mult_right_mono SUP_upper x)
+ next
+ have "?lhs / ereal x = (SUP i:Y. f i) * (ereal x / ereal x)" by(simp only: ereal_times_divide_eq)
+ also have "\<dots> = (SUP i:Y. f i)" using False by simp
+ also have "\<dots> \<le> ?rhs / x"
+ proof(rule SUP_least)
+ fix i
+ assume "i \<in> Y"
+ have "f i = f i * (ereal x / ereal x)" using False by simp
+ also have "\<dots> = f i * x / x" by(simp only: ereal_times_divide_eq)
+ also from \<open>i \<in> Y\<close> have "f i * x \<le> ?rhs" by(rule SUP_upper)
+ hence "f i * x / x \<le> ?rhs / x" using x False by simp
+ finally show "f i \<le> ?rhs / x" .
+ qed
+ finally have "(?lhs / x) * x \<le> (?rhs / x) * x"
+ by(rule ereal_mult_right_mono)(simp add: x)
+ also have "\<dots> = ?rhs" using False ereal_divide_eq mult.commute by force
+ also have "(?lhs / x) * x = ?lhs" using False ereal_divide_eq mult.commute by force
+ finally show "?lhs \<le> ?rhs" .
+ qed
+qed
subsubsection {* Tests for code generator *}
--- a/src/HOL/Library/document/root.tex Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Library/document/root.tex Wed Apr 15 16:48:24 2015 +0200
@@ -2,7 +2,7 @@
\usepackage{ifthen}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
-\usepackage{isabelle,isabellesym,amssymb,stmaryrd,textcomp}
+\usepackage{isabelle,isabellesym,amssymb,stmaryrd,textcomp,wasysym}
\usepackage{pdfsetup}
\urlstyle{rm}
--- a/src/HOL/Lifting_Set.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Lifting_Set.thy Wed Apr 15 16:48:24 2015 +0200
@@ -281,4 +281,9 @@
lemmas setsum_parametric = setsum.F_parametric
lemmas setprod_parametric = setprod.F_parametric
+lemma rel_set_UNION:
+ assumes [transfer_rule]: "rel_set Q A B" "rel_fun Q (rel_set R) f g"
+ shows "rel_set R (UNION A f) (UNION B g)"
+by transfer_prover
+
end
--- a/src/HOL/Map.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Map.thy Wed Apr 15 16:48:24 2015 +0200
@@ -641,6 +641,8 @@
ultimately show ?case by (simp only: map_of.simps ran_map_upd) simp
qed
+lemma ran_map_option: "ran (\<lambda>x. map_option f (m x)) = f ` ran m"
+by(auto simp add: ran_def)
subsection {* @{text "map_le"} *}
--- a/src/HOL/Partial_Function.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Partial_Function.thy Wed Apr 15 16:48:24 2015 +0200
@@ -12,6 +12,40 @@
named_theorems partial_function_mono "monotonicity rules for partial function definitions"
ML_file "Tools/Function/partial_function.ML"
+lemma (in ccpo) in_chain_finite:
+ assumes "Complete_Partial_Order.chain op \<le> A" "finite A" "A \<noteq> {}"
+ shows "\<Squnion>A \<in> A"
+using assms(2,1,3)
+proof induction
+ case empty thus ?case by simp
+next
+ case (insert x A)
+ note chain = `Complete_Partial_Order.chain op \<le> (insert x A)`
+ show ?case
+ proof(cases "A = {}")
+ case True thus ?thesis by simp
+ next
+ case False
+ from chain have chain': "Complete_Partial_Order.chain op \<le> A"
+ by(rule chain_subset) blast
+ hence "\<Squnion>A \<in> A" using False by(rule insert.IH)
+ show ?thesis
+ proof(cases "x \<le> \<Squnion>A")
+ case True
+ have "\<Squnion>insert x A \<le> \<Squnion>A" using chain
+ by(rule ccpo_Sup_least)(auto simp add: True intro: ccpo_Sup_upper[OF chain'])
+ hence "\<Squnion>insert x A = \<Squnion>A"
+ by(rule antisym)(blast intro: ccpo_Sup_upper[OF chain] ccpo_Sup_least[OF chain'])
+ with `\<Squnion>A \<in> A` show ?thesis by simp
+ next
+ case False
+ with chainD[OF chain, of x "\<Squnion>A"] `\<Squnion>A \<in> A`
+ have "\<Squnion>insert x A = x"
+ by(auto intro: antisym ccpo_Sup_least[OF chain] order_trans[OF ccpo_Sup_upper[OF chain']] ccpo_Sup_upper[OF chain])
+ thus ?thesis by simp
+ qed
+ qed
+qed
subsection {* Axiomatic setup *}
--- a/src/HOL/Probability/Binary_Product_Measure.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Wed Apr 15 16:48:24 2015 +0200
@@ -1056,6 +1056,13 @@
finally show ?thesis .
qed
+lemma measurable_pair_measure_countable1:
+ assumes "countable A"
+ and [measurable]: "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N K"
+ shows "f \<in> measurable (count_space A \<Otimes>\<^sub>M N) K"
+using _ _ assms(1)
+by(rule measurable_compose_countable'[where f="\<lambda>a b. f (a, snd b)" and g=fst and I=A, simplified])simp_all
+
subsection {* Product of Borel spaces *}
lemma borel_Times:
--- a/src/HOL/Probability/Bochner_Integration.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy Wed Apr 15 16:48:24 2015 +0200
@@ -1875,6 +1875,15 @@
qed
qed (simp add: integrable_restrict_space)
+lemma integral_empty:
+ assumes "space M = {}"
+ shows "integral\<^sup>L M f = 0"
+proof -
+ have "(\<integral> x. f x \<partial>M) = (\<integral> x. 0 \<partial>M)"
+ by(rule integral_cong)(simp_all add: assms)
+ thus ?thesis by simp
+qed
+
subsection {* Measure spaces with an associated density *}
lemma integrable_density:
--- a/src/HOL/Probability/Embed_Measure.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Probability/Embed_Measure.thy Wed Apr 15 16:48:24 2015 +0200
@@ -110,13 +110,18 @@
"inj f \<Longrightarrow> embed_measure M f = distr M (embed_measure M f) f"
by (rule embed_measure_eq_distr') (auto intro!: inj_onI dest: injD)
+lemma nn_integral_embed_measure':
+ "inj_on f (space M) \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
+ nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
+ apply (subst embed_measure_eq_distr', simp)
+ apply (subst nn_integral_distr)
+ apply (simp_all add: measurable_embed_measure2')
+ done
+
lemma nn_integral_embed_measure:
"inj f \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
- apply (subst embed_measure_eq_distr, simp)
- apply (subst nn_integral_distr)
- apply (simp_all add: measurable_embed_measure2)
- done
+ by(erule nn_integral_embed_measure'[OF subset_inj_on]) simp
lemma emeasure_embed_measure':
assumes "inj_on f (space M)" "A \<in> sets (embed_measure M f)"
@@ -167,18 +172,21 @@
qed
qed
-lemma embed_measure_count_space:
- "inj f \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
+lemma embed_measure_count_space':
+ "inj_on f A \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
apply (subst distr_bij_count_space[of f A "f`A", symmetric])
apply (simp add: inj_on_def bij_betw_def)
- apply (subst embed_measure_eq_distr)
+ apply (subst embed_measure_eq_distr')
apply simp
- apply (auto intro!: measure_eqI imageI simp: sets_embed_measure subset_image_iff)
- apply blast
+ apply(auto 4 3 intro!: measure_eqI imageI simp add: sets_embed_measure' subset_image_iff)
apply (subst (1 2) emeasure_distr)
- apply (auto simp: space_embed_measure sets_embed_measure)
+ apply (auto simp: space_embed_measure sets_embed_measure')
done
+lemma embed_measure_count_space:
+ "inj f \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
+ by(rule embed_measure_count_space')(erule subset_inj_on, simp)
+
lemma sets_embed_measure_alt:
"inj f \<Longrightarrow> sets (embed_measure M f) = (op`f) ` sets M"
by (auto simp: sets_embed_measure)
@@ -340,4 +348,33 @@
shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
using assms by (intro AE_embed_measure') (auto intro!: inj_onI dest: injD)
+lemma nn_integral_monotone_convergence_SUP_countable:
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ereal"
+ assumes nonempty: "Y \<noteq> {}"
+ and chain: "Complete_Partial_Order.chain op \<le> (f ` Y)"
+ and countable: "countable B"
+ shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space B) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space B))"
+ (is "?lhs = ?rhs")
+proof -
+ let ?f = "(\<lambda>i x. f i (from_nat_into B x) * indicator (to_nat_on B ` B) x)"
+ have "?lhs = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B"
+ by(rule nn_integral_cong)(simp add: countable)
+ also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B x)) \<partial>count_space (to_nat_on B ` B)"
+ by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
+ also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. ?f i x) \<partial>count_space UNIV"
+ by(simp add: nn_integral_count_space_indicator ereal_indicator[symmetric] Sup_ereal_mult_right' nonempty)
+ also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)" using nonempty
+ proof(rule nn_integral_monotone_convergence_SUP_nat)
+ show "Complete_Partial_Order.chain op \<le> (?f ` Y)"
+ by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD)
+ qed
+ also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"
+ by(simp add: nn_integral_count_space_indicator)
+ also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \<partial>count_space B)"
+ by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
+ also have "\<dots> = ?rhs"
+ by(intro arg_cong2[where f="SUPREMUM"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)
+ finally show ?thesis .
+qed
+
end
--- a/src/HOL/Probability/Giry_Monad.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy Wed Apr 15 16:48:24 2015 +0200
@@ -38,6 +38,12 @@
sublocale prob_space \<subseteq> subprob_space
by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty)
+lemma subprob_space_sigma [simp]: "\<Omega> \<noteq> {} \<Longrightarrow> subprob_space (sigma \<Omega> X)"
+by(rule subprob_spaceI)(simp_all add: emeasure_sigma space_measure_of_conv)
+
+lemma subprob_space_null_measure: "space M \<noteq> {} \<Longrightarrow> subprob_space (null_measure M)"
+by(simp add: null_measure_def)
+
lemma (in subprob_space) subprob_space_distr:
assumes f: "f \<in> measurable M M'" and "space M' \<noteq> {}" shows "subprob_space (distr M M' f)"
proof (rule subprob_spaceI)
@@ -324,6 +330,35 @@
finally show ?thesis .
qed
+lemma integral_measurable_subprob_algebra:
+ fixes f :: "_ \<Rightarrow> real"
+ assumes f_measurable [measurable]: "f \<in> borel_measurable N"
+ and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> \<bar>f x\<bar> \<le> B"
+ shows "(\<lambda>M. integral\<^sup>L M f) \<in> borel_measurable (subprob_algebra N)"
+proof -
+ note [measurable] = nn_integral_measurable_subprob_algebra
+ have "?thesis \<longleftrightarrow> (\<lambda>M. real (\<integral>\<^sup>+ x. f x \<partial>M) - real (\<integral>\<^sup>+ x. - f x \<partial>M)) \<in> borel_measurable (subprob_algebra N)"
+ proof(rule measurable_cong)
+ fix M
+ assume "M \<in> space (subprob_algebra N)"
+ hence "subprob_space M" and M [measurable_cong]: "sets M = sets N"
+ by(simp_all add: space_subprob_algebra)
+ interpret subprob_space M by fact
+ have "(\<integral>\<^sup>+ x. ereal \<bar>f x\<bar> \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal B \<partial>M)"
+ by(rule nn_integral_mono)(simp add: sets_eq_imp_space_eq[OF M] f_bounded)
+ also have "\<dots> = max B 0 * emeasure M (space M)" by(simp add: nn_integral_const_If max_def)
+ also have "\<dots> \<le> ereal (max B 0) * 1"
+ by(rule ereal_mult_left_mono)(simp_all add: emeasure_space_le_1 zero_ereal_def)
+ finally have "(\<integral>\<^sup>+ x. ereal \<bar>f x\<bar> \<partial>M) \<noteq> \<infinity>" by(auto simp add: max_def)
+ then have "integrable M f" using f_measurable
+ by(auto intro: integrableI_bounded)
+ thus "(\<integral> x. f x \<partial>M) = real (\<integral>\<^sup>+ x. f x \<partial>M) - real (\<integral>\<^sup>+ x. - f x \<partial>M)"
+ by(simp add: real_lebesgue_integral_def)
+ qed
+ also have "\<dots>" by measurable
+ finally show ?thesis .
+qed
+
(* TODO: Rename. This name is too general -- Manuel *)
lemma measurable_pair_measure:
assumes f: "f \<in> measurable M (subprob_algebra N)"
@@ -796,6 +831,163 @@
apply (auto simp: f)
done
+lemma measurable_join1:
+ "\<lbrakk> f \<in> measurable N K; sets M = sets (subprob_algebra N) \<rbrakk>
+ \<Longrightarrow> f \<in> measurable (join M) K"
+by(simp add: measurable_def)
+
+lemma
+ fixes f :: "_ \<Rightarrow> real"
+ assumes f_measurable [measurable]: "f \<in> borel_measurable N"
+ and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> \<bar>f x\<bar> \<le> B"
+ and M [measurable_cong]: "sets M = sets (subprob_algebra N)"
+ and fin: "finite_measure M"
+ and M_bounded: "AE M' in M. emeasure M' (space M') \<le> ereal B'"
+ shows integrable_join: "integrable (join M) f" (is ?integrable)
+ and integral_join: "integral\<^sup>L (join M) f = \<integral> M'. integral\<^sup>L M' f \<partial>M" (is ?integral)
+proof(case_tac [!] "space N = {}")
+ assume *: "space N = {}"
+ show ?integrable
+ using M * by(simp add: real_integrable_def measurable_def nn_integral_empty)
+ have "(\<integral> M'. integral\<^sup>L M' f \<partial>M) = (\<integral> M'. 0 \<partial>M)"
+ proof(rule integral_cong)
+ fix M'
+ assume "M' \<in> space M"
+ with sets_eq_imp_space_eq[OF M] have "space M' = space N"
+ by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
+ with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: integral_empty)
+ qed simp
+ then show ?integral
+ using M * by(simp add: integral_empty)
+next
+ assume *: "space N \<noteq> {}"
+
+ from * have B [simp]: "0 \<le> B" by(auto dest: f_bounded)
+
+ have [measurable]: "f \<in> borel_measurable (join M)" using f_measurable M
+ by(rule measurable_join1)
+
+ { fix f M'
+ assume [measurable]: "f \<in> borel_measurable N"
+ and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> f x \<le> B"
+ and "M' \<in> space M" "emeasure M' (space M') \<le> ereal B'"
+ have "AE x in M'. ereal (f x) \<le> ereal B"
+ proof(rule AE_I2)
+ fix x
+ assume "x \<in> space M'"
+ with \<open>M' \<in> space M\<close> sets_eq_imp_space_eq[OF M]
+ have "x \<in> space N" by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
+ from f_bounded[OF this] show "ereal (f x) \<le> ereal B" by simp
+ qed
+ then have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> (\<integral>\<^sup>+ x. ereal B \<partial>M')"
+ by(rule nn_integral_mono_AE)
+ also have "\<dots> = ereal B * emeasure M' (space M')" by(simp)
+ also have "\<dots> \<le> ereal B * ereal B'" by(rule ereal_mult_left_mono)(fact, simp)
+ also have "\<dots> \<le> ereal B * ereal \<bar>B'\<bar>" by(rule ereal_mult_left_mono)(simp_all)
+ finally have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)" by simp }
+ note bounded1 = this
+
+ have bounded:
+ "\<And>f. \<lbrakk> f \<in> borel_measurable N; \<And>x. x \<in> space N \<Longrightarrow> f x \<le> B \<rbrakk>
+ \<Longrightarrow> (\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) \<noteq> \<infinity>"
+ proof -
+ fix f
+ assume [measurable]: "f \<in> borel_measurable N"
+ and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> f x \<le> B"
+ have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. ereal (f x) \<partial>M' \<partial>M)"
+ by(rule nn_integral_join[OF _ M]) simp
+ also have "\<dots> \<le> \<integral>\<^sup>+ M'. B * \<bar>B'\<bar> \<partial>M"
+ using bounded1[OF \<open>f \<in> borel_measurable N\<close> f_bounded]
+ by(rule nn_integral_mono_AE[OF AE_mp[OF M_bounded AE_I2], rule_format])
+ also have "\<dots> = B * \<bar>B'\<bar> * emeasure M (space M)" by simp
+ also have "\<dots> < \<infinity>" by(simp add: finite_measure.finite_emeasure_space[OF fin])
+ finally show "?thesis f" by simp
+ qed
+ have f_pos: "(\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) \<noteq> \<infinity>"
+ and f_neg: "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>join M) \<noteq> \<infinity>"
+ using f_bounded by(auto del: notI intro!: bounded simp add: abs_le_iff)
+
+ show ?integrable using f_pos f_neg by(simp add: real_integrable_def)
+
+ note [measurable] = nn_integral_measurable_subprob_algebra
+
+ have "(\<integral>\<^sup>+ x. f x \<partial>join M) = (\<integral>\<^sup>+ x. max 0 (f x) \<partial>join M)"
+ by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)
+ also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. max 0 (f x) \<partial>M' \<partial>M"
+ by(simp add: nn_integral_join[OF _ M])
+ also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M"
+ by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)
+ finally have int_f: "(\<integral>\<^sup>+ x. f x \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)" .
+
+ have "(\<integral>\<^sup>+ x. - f x \<partial>join M) = (\<integral>\<^sup>+ x. max 0 (- f x) \<partial>join M)"
+ by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)
+ also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. max 0 (- f x) \<partial>M' \<partial>M"
+ by(simp add: nn_integral_join[OF _ M])
+ also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M"
+ by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)
+ finally have int_mf: "(\<integral>\<^sup>+ x. - f x \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M)" .
+
+ have f_pos1:
+ "\<And>M'. \<lbrakk> M' \<in> space M; emeasure M' (space M') \<le> ereal B' \<rbrakk>
+ \<Longrightarrow> (\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)"
+ using f_measurable by(auto intro!: bounded1 dest: f_bounded)
+ have "AE M' in M. (\<integral>\<^sup>+ x. f x \<partial>M') \<noteq> \<infinity>"
+ using M_bounded by(rule AE_mp[OF _ AE_I2])(auto dest: f_pos1)
+ hence [simp]: "(\<integral>\<^sup>+ M'. ereal (real (\<integral>\<^sup>+ x. f x \<partial>M')) \<partial>M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"
+ by(rule nn_integral_cong_AE[OF AE_mp])(simp add: ereal_real nn_integral_nonneg)
+ from f_pos have [simp]: "integrable M (\<lambda>M'. real (\<integral>\<^sup>+ x. f x \<partial>M'))"
+ by(simp add: int_f real_integrable_def nn_integral_nonneg real_of_ereal[symmetric] nn_integral_0_iff_AE[THEN iffD2] del: real_of_ereal)
+
+ have f_neg1:
+ "\<And>M'. \<lbrakk> M' \<in> space M; emeasure M' (space M') \<le> ereal B' \<rbrakk>
+ \<Longrightarrow> (\<integral>\<^sup>+ x. ereal (- f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)"
+ using f_measurable by(auto intro!: bounded1 dest: f_bounded)
+ have "AE M' in M. (\<integral>\<^sup>+ x. - f x \<partial>M') \<noteq> \<infinity>"
+ using M_bounded by(rule AE_mp[OF _ AE_I2])(auto dest: f_neg1)
+ hence [simp]: "(\<integral>\<^sup>+ M'. ereal (real (\<integral>\<^sup>+ x. - f x \<partial>M')) \<partial>M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M)"
+ by(rule nn_integral_cong_AE[OF AE_mp])(simp add: ereal_real nn_integral_nonneg)
+ from f_neg have [simp]: "integrable M (\<lambda>M'. real (\<integral>\<^sup>+ x. - f x \<partial>M'))"
+ by(simp add: int_mf real_integrable_def nn_integral_nonneg real_of_ereal[symmetric] nn_integral_0_iff_AE[THEN iffD2] del: real_of_ereal)
+
+ from \<open>?integrable\<close>
+ have "ereal (\<integral> x. f x \<partial>join M) = (\<integral>\<^sup>+ x. f x \<partial>join M) - (\<integral>\<^sup>+ x. - f x \<partial>join M)"
+ by(simp add: real_lebesgue_integral_def ereal_minus(1)[symmetric] ereal_real nn_integral_nonneg f_pos f_neg del: ereal_minus(1))
+ also note int_f
+ also note int_mf
+ also have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M) =
+ ((\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)) -
+ ((\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M))"
+ by(subst (7 11) nn_integral_0_iff_AE[THEN iffD2])(simp_all add: nn_integral_nonneg)
+ also have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) = \<integral> M'. real (\<integral>\<^sup>+ x. f x \<partial>M') \<partial>M"
+ using f_pos
+ by(simp add: real_lebesgue_integral_def)(simp add: ereal_minus(1)[symmetric] ereal_real int_f nn_integral_nonneg nn_integral_0_iff_AE[THEN iffD2] real_of_ereal_pos zero_ereal_def[symmetric])
+ also have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M) = \<integral> M'. real (\<integral>\<^sup>+ x. - f x \<partial>M') \<partial>M"
+ using f_neg
+ by(simp add: real_lebesgue_integral_def)(simp add: ereal_minus(1)[symmetric] ereal_real int_mf nn_integral_nonneg nn_integral_0_iff_AE[THEN iffD2] real_of_ereal_pos zero_ereal_def[symmetric])
+ also note ereal_minus(1)
+ also have "(\<integral> M'. real (\<integral>\<^sup>+ x. f x \<partial>M') \<partial>M) - (\<integral> M'. real (\<integral>\<^sup>+ x. - f x \<partial>M') \<partial>M) =
+ \<integral>M'. real (\<integral>\<^sup>+ x. f x \<partial>M') - real (\<integral>\<^sup>+ x. - f x \<partial>M') \<partial>M"
+ by simp
+ also have "\<dots> = \<integral>M'. \<integral> x. f x \<partial>M' \<partial>M" using _ _ M_bounded
+ proof(rule integral_cong_AE[OF _ _ AE_mp[OF _ AE_I2], rule_format])
+ show "(\<lambda>M'. integral\<^sup>L M' f) \<in> borel_measurable M"
+ by measurable(simp add: integral_measurable_subprob_algebra[OF _ f_bounded])
+
+ fix M'
+ assume "M' \<in> space M" "emeasure M' (space M') \<le> B'"
+ then interpret finite_measure M' by(auto intro: finite_measureI)
+
+ from \<open>M' \<in> space M\<close> sets_eq_imp_space_eq[OF M]
+ have [measurable_cong]: "sets M' = sets N" by(simp add: space_subprob_algebra)
+ hence [simp]: "space M' = space N" by(rule sets_eq_imp_space_eq)
+ have "integrable M' f"
+ by(rule integrable_const_bound[where B=B])(auto simp add: f_bounded)
+ then show "real (\<integral>\<^sup>+ x. f x \<partial>M') - real (\<integral>\<^sup>+ x. - f x \<partial>M') = \<integral> x. f x \<partial>M'"
+ by(simp add: real_lebesgue_integral_def)
+ qed simp_all
+ finally show ?integral by simp
+qed
+
lemma join_assoc:
assumes M[measurable_cong]: "sets M = sets (subprob_algebra (subprob_algebra N))"
shows "join (distr M (subprob_algebra N) join) = join (join M)"
@@ -998,6 +1190,32 @@
by (simp add: space_subprob_algebra)
qed
+lemma
+ fixes f :: "_ \<Rightarrow> real"
+ assumes f_measurable [measurable]: "f \<in> borel_measurable K"
+ and f_bounded: "\<And>x. x \<in> space K \<Longrightarrow> \<bar>f x\<bar> \<le> B"
+ and N [measurable]: "N \<in> measurable M (subprob_algebra K)"
+ and fin: "finite_measure M"
+ and M_bounded: "AE x in M. emeasure (N x) (space (N x)) \<le> ereal B'"
+ shows integrable_bind: "integrable (bind M N) f" (is ?integrable)
+ and integral_bind: "integral\<^sup>L (bind M N) f = \<integral> x. integral\<^sup>L (N x) f \<partial>M" (is ?integral)
+proof(case_tac [!] "space M = {}")
+ assume [simp]: "space M \<noteq> {}"
+ interpret finite_measure M by(rule fin)
+
+ have "integrable (join (distr M (subprob_algebra K) N)) f"
+ using f_measurable f_bounded
+ by(rule integrable_join[where B'=B'])(simp_all add: finite_measure_distr AE_distr_iff M_bounded)
+ then show ?integrable by(simp add: bind_nonempty''[where N=K])
+
+ have "integral\<^sup>L (join (distr M (subprob_algebra K) N)) f = \<integral> M'. integral\<^sup>L M' f \<partial>distr M (subprob_algebra K) N"
+ using f_measurable f_bounded
+ by(rule integral_join[where B'=B'])(simp_all add: finite_measure_distr AE_distr_iff M_bounded)
+ also have "\<dots> = \<integral> x. integral\<^sup>L (N x) f \<partial>M"
+ by(rule integral_distr)(simp_all add: integral_measurable_subprob_algebra[OF _ f_bounded])
+ finally show ?integral by(simp add: bind_nonempty''[where N=K])
+qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite integral_empty)
+
lemma (in prob_space) prob_space_bind:
assumes ae: "AE x in M. prob_space (N x)"
and N[measurable]: "N \<in> measurable M (subprob_algebra S)"
@@ -1142,6 +1360,38 @@
done
qed
+lemma bind_restrict_space:
+ assumes A: "A \<inter> space M \<noteq> {}" "A \<inter> space M \<in> sets M"
+ and f: "f \<in> measurable (restrict_space M A) (subprob_algebra N)"
+ shows "restrict_space M A \<guillemotright>= f = M \<guillemotright>= (\<lambda>x. if x \<in> A then f x else null_measure (f (SOME x. x \<in> A \<and> x \<in> space M)))"
+ (is "?lhs = ?rhs" is "_ = M \<guillemotright>= ?f")
+proof -
+ let ?P = "\<lambda>x. x \<in> A \<and> x \<in> space M"
+ let ?x = "Eps ?P"
+ let ?c = "null_measure (f ?x)"
+ from A have "?P ?x" by-(rule someI_ex, blast)
+ hence "?x \<in> space (restrict_space M A)" by(simp add: space_restrict_space)
+ with f have "f ?x \<in> space (subprob_algebra N)" by(rule measurable_space)
+ hence sps: "subprob_space (f ?x)"
+ and sets: "sets (f ?x) = sets N"
+ by(simp_all add: space_subprob_algebra)
+ have "space (f ?x) \<noteq> {}" using sps by(rule subprob_space.subprob_not_empty)
+ moreover have "sets ?c = sets N" by(simp add: null_measure_def)(simp add: sets)
+ ultimately have c: "?c \<in> space (subprob_algebra N)"
+ by(simp add: space_subprob_algebra subprob_space_null_measure)
+ from f A c have f': "?f \<in> measurable M (subprob_algebra N)"
+ by(simp add: measurable_restrict_space_iff)
+
+ from A have [simp]: "space M \<noteq> {}" by blast
+
+ have "?lhs = join (distr (restrict_space M A) (subprob_algebra N) f)"
+ using assms by(simp add: space_restrict_space bind_nonempty'')
+ also have "\<dots> = join (distr M (subprob_algebra N) ?f)"
+ by(rule measure_eqI)(auto simp add: emeasure_join nn_integral_distr nn_integral_restrict_space f f' A intro: nn_integral_cong)
+ also have "\<dots> = ?rhs" using f' by(simp add: bind_nonempty'')
+ finally show ?thesis .
+qed
+
lemma bind_const': "\<lbrakk>prob_space M; subprob_space N\<rbrakk> \<Longrightarrow> M \<guillemotright>= (\<lambda>x. N) = N"
by (intro measure_eqI)
(simp_all add: space_subprob_algebra prob_space.not_empty emeasure_bind_const_prob_space)
--- a/src/HOL/Probability/Measure_Space.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Probability/Measure_Space.thy Wed Apr 15 16:48:24 2015 +0200
@@ -1650,7 +1650,6 @@
with f show "emeasure (distr M M' f) (space (distr M M' f)) \<noteq> \<infinity>" by (auto simp: emeasure_distr)
qed
-
subsection {* Counting space *}
lemma strict_monoI_Suc:
@@ -1882,6 +1881,40 @@
by (cases "finite X") (auto simp add: emeasure_restrict_space)
qed
+lemma sigma_finite_measure_restrict_space:
+ assumes "sigma_finite_measure M"
+ and A: "A \<in> sets M"
+ shows "sigma_finite_measure (restrict_space M A)"
+proof -
+ interpret sigma_finite_measure M by fact
+ from sigma_finite_countable obtain C
+ where C: "countable C" "C \<subseteq> sets M" "(\<Union>C) = space M" "\<forall>a\<in>C. emeasure M a \<noteq> \<infinity>"
+ by blast
+ let ?C = "op \<inter> A ` C"
+ from C have "countable ?C" "?C \<subseteq> sets (restrict_space M A)" "(\<Union>?C) = space (restrict_space M A)"
+ by(auto simp add: sets_restrict_space space_restrict_space)
+ moreover {
+ fix a
+ assume "a \<in> ?C"
+ then obtain a' where "a = A \<inter> a'" "a' \<in> C" ..
+ then have "emeasure (restrict_space M A) a \<le> emeasure M a'"
+ using A C by(auto simp add: emeasure_restrict_space intro: emeasure_mono)
+ also have "\<dots> < \<infinity>" using C(4)[rule_format, of a'] \<open>a' \<in> C\<close> by simp
+ finally have "emeasure (restrict_space M A) a \<noteq> \<infinity>" by simp }
+ ultimately show ?thesis
+ by unfold_locales (rule exI conjI|assumption|blast)+
+qed
+
+lemma finite_measure_restrict_space:
+ assumes "finite_measure M"
+ and A: "A \<in> sets M"
+ shows "finite_measure (restrict_space M A)"
+proof -
+ interpret finite_measure M by fact
+ show ?thesis
+ by(rule finite_measureI)(simp add: emeasure_restrict_space A space_restrict_space)
+qed
+
lemma restrict_distr:
assumes [measurable]: "f \<in> measurable M N"
assumes [simp]: "\<Omega> \<inter> space N \<in> sets N" and restrict: "f \<in> space M \<rightarrow> \<Omega>"
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Wed Apr 15 16:48:24 2015 +0200
@@ -758,6 +758,9 @@
lemma nn_integral_le_0[simp]: "integral\<^sup>N M f \<le> 0 \<longleftrightarrow> integral\<^sup>N M f = 0"
using nn_integral_nonneg[of M f] by auto
+lemma nn_integral_not_less_0 [simp]: "\<not> nn_integral M f < 0"
+by(simp add: not_less nn_integral_nonneg)
+
lemma nn_integral_not_MInfty[simp]: "integral\<^sup>N M f \<noteq> -\<infinity>"
using nn_integral_nonneg[of M f] by auto
@@ -1648,6 +1651,15 @@
subsection {* Integral under concrete measures *}
+lemma nn_integral_empty:
+ assumes "space M = {}"
+ shows "nn_integral M f = 0"
+proof -
+ have "(\<integral>\<^sup>+ x. f x \<partial>M) = (\<integral>\<^sup>+ x. 0 \<partial>M)"
+ by(rule nn_integral_cong)(simp add: assms)
+ thus ?thesis by simp
+qed
+
subsubsection {* Distributions *}
lemma nn_integral_distr':
@@ -1854,6 +1866,143 @@
finally show "emeasure M A = emeasure N A" ..
qed simp
+lemma nn_integral_monotone_convergence_SUP_nat':
+ fixes f :: "'a \<Rightarrow> nat \<Rightarrow> ereal"
+ assumes chain: "Complete_Partial_Order.chain op \<le> (f ` Y)"
+ and nonempty: "Y \<noteq> {}"
+ and nonneg: "\<And>i n. i \<in> Y \<Longrightarrow> f i n \<ge> 0"
+ shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space UNIV) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space UNIV))"
+ (is "?lhs = ?rhs" is "integral\<^sup>N ?M _ = _")
+proof (rule order_class.order.antisym)
+ show "?rhs \<le> ?lhs"
+ by (auto intro!: SUP_least SUP_upper nn_integral_mono)
+next
+ have "\<And>x. \<exists>g. incseq g \<and> range g \<subseteq> (\<lambda>i. f i x) ` Y \<and> (SUP i:Y. f i x) = (SUP i. g i)"
+ unfolding Sup_class.SUP_def by(rule Sup_countable_SUP[unfolded Sup_class.SUP_def])(simp add: nonempty)
+ then obtain g where incseq: "\<And>x. incseq (g x)"
+ and range: "\<And>x. range (g x) \<subseteq> (\<lambda>i. f i x) ` Y"
+ and sup: "\<And>x. (SUP i:Y. f i x) = (SUP i. g x i)" by moura
+ from incseq have incseq': "incseq (\<lambda>i x. g x i)"
+ by(blast intro: incseq_SucI le_funI dest: incseq_SucD)
+
+ have "?lhs = \<integral>\<^sup>+ x. (SUP i. g x i) \<partial>?M" by(simp add: sup)
+ also have "\<dots> = (SUP i. \<integral>\<^sup>+ x. g x i \<partial>?M)" using incseq'
+ by(rule nn_integral_monotone_convergence_SUP) simp
+ also have "\<dots> \<le> (SUP i:Y. \<integral>\<^sup>+ x. f i x \<partial>?M)"
+ proof(rule SUP_least)
+ fix n
+ have "\<And>x. \<exists>i. g x n = f i x \<and> i \<in> Y" using range by blast
+ then obtain I where I: "\<And>x. g x n = f (I x) x" "\<And>x. I x \<in> Y" by moura
+
+ { fix x
+ from range[of x] obtain i where "i \<in> Y" "g x n = f i x" by auto
+ hence "g x n \<ge> 0" using nonneg[of i x] by simp }
+ note nonneg_g = this
+ then have "(\<integral>\<^sup>+ x. g x n \<partial>count_space UNIV) = (\<Sum>x. g x n)"
+ by(rule nn_integral_count_space_nat)
+ also have "\<dots> = (SUP m. \<Sum>x<m. g x n)" using nonneg_g
+ by(rule suminf_ereal_eq_SUP)
+ also have "\<dots> \<le> (SUP i:Y. \<integral>\<^sup>+ x. f i x \<partial>?M)"
+ proof(rule SUP_mono)
+ fix m
+ show "\<exists>m'\<in>Y. (\<Sum>x<m. g x n) \<le> (\<integral>\<^sup>+ x. f m' x \<partial>?M)"
+ proof(cases "m > 0")
+ case False
+ thus ?thesis using nonempty by(auto simp add: nn_integral_nonneg)
+ next
+ case True
+ let ?Y = "I ` {..<m}"
+ have "f ` ?Y \<subseteq> f ` Y" using I by auto
+ with chain have chain': "Complete_Partial_Order.chain op \<le> (f ` ?Y)" by(rule chain_subset)
+ hence "Sup (f ` ?Y) \<in> f ` ?Y"
+ by(rule ccpo_class.in_chain_finite)(auto simp add: True lessThan_empty_iff)
+ then obtain m' where "m' < m" and m': "(SUP i:?Y. f i) = f (I m')" by auto
+ have "I m' \<in> Y" using I by blast
+ have "(\<Sum>x<m. g x n) \<le> (\<Sum>x<m. f (I m') x)"
+ proof(rule setsum_mono)
+ fix x
+ assume "x \<in> {..<m}"
+ hence "x < m" by simp
+ have "g x n = f (I x) x" by(simp add: I)
+ also have "\<dots> \<le> (SUP i:?Y. f i) x" unfolding SUP_def Sup_fun_def image_image
+ using \<open>x \<in> {..<m}\<close> by(rule Sup_upper[OF imageI])
+ also have "\<dots> = f (I m') x" unfolding m' by simp
+ finally show "g x n \<le> f (I m') x" .
+ qed
+ also have "\<dots> \<le> (SUP m. (\<Sum>x<m. f (I m') x))"
+ by(rule SUP_upper) simp
+ also have "\<dots> = (\<Sum>x. f (I m') x)"
+ by(rule suminf_ereal_eq_SUP[symmetric])(simp add: nonneg \<open>I m' \<in> Y\<close>)
+ also have "\<dots> = (\<integral>\<^sup>+ x. f (I m') x \<partial>?M)"
+ by(rule nn_integral_count_space_nat[symmetric])(simp add: nonneg \<open>I m' \<in> Y\<close>)
+ finally show ?thesis using \<open>I m' \<in> Y\<close> by blast
+ qed
+ qed
+ finally show "(\<integral>\<^sup>+ x. g x n \<partial>count_space UNIV) \<le> \<dots>" .
+ qed
+ finally show "?lhs \<le> ?rhs" .
+qed
+
+lemma nn_integral_monotone_convergence_SUP_nat:
+ fixes f :: "'a \<Rightarrow> nat \<Rightarrow> ereal"
+ assumes nonempty: "Y \<noteq> {}"
+ and chain: "Complete_Partial_Order.chain op \<le> (f ` Y)"
+ shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space UNIV) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space UNIV))"
+ (is "?lhs = ?rhs")
+proof -
+ let ?f = "\<lambda>i x. max 0 (f i x)"
+ have chain': "Complete_Partial_Order.chain op \<le> (?f ` Y)"
+ proof(rule chainI)
+ fix g h
+ assume "g \<in> ?f ` Y" "h \<in> ?f ` Y"
+ then obtain g' h' where gh: "g' \<in> Y" "h' \<in> Y" "g = ?f g'" "h = ?f h'" by blast
+ hence "f g' \<in> f ` Y" "f h' \<in> f ` Y" by blast+
+ with chain have "f g' \<le> f h' \<or> f h' \<le> f g'" by(rule chainD)
+ thus "g \<le> h \<or> h \<le> g"
+ proof
+ assume "f g' \<le> f h'"
+ hence "g \<le> h" using gh order_trans by(auto simp add: le_fun_def max_def)
+ thus ?thesis ..
+ next
+ assume "f h' \<le> f g'"
+ hence "h \<le> g" using gh order_trans by(auto simp add: le_fun_def max_def)
+ thus ?thesis ..
+ qed
+ qed
+ have "?lhs = (\<integral>\<^sup>+ x. max 0 (SUP i:Y. f i x) \<partial>count_space UNIV)"
+ by(simp add: nn_integral_max_0)
+ also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i:Y. ?f i x) \<partial>count_space UNIV)"
+ proof(rule nn_integral_cong)
+ fix x
+ have "max 0 (SUP i:Y. f i x) \<le> (SUP i:Y. ?f i x)"
+ proof(cases "0 \<le> (SUP i:Y. f i x)")
+ case True
+ have "(SUP i:Y. f i x) \<le> (SUP i:Y. ?f i x)" by(rule SUP_mono)(auto intro: rev_bexI)
+ with True show ?thesis by simp
+ next
+ case False
+ have "0 \<le> (SUP i:Y. ?f i x)" using nonempty by(auto intro: SUP_upper2)
+ thus ?thesis using False by simp
+ qed
+ moreover have "\<dots> \<le> max 0 (SUP i:Y. f i x)"
+ proof(cases "(SUP i:Y. f i x) \<ge> 0")
+ case True
+ show ?thesis
+ by(rule SUP_least)(auto simp add: True max_def intro: SUP_upper)
+ next
+ case False
+ hence "(SUP i:Y. f i x) \<le> 0" by simp
+ hence less: "\<forall>i\<in>Y. f i x \<le> 0" by(simp add: SUP_le_iff)
+ show ?thesis by(rule SUP_least)(auto simp add: max_def less intro: SUP_upper)
+ qed
+ ultimately show "\<dots> = (SUP i:Y. ?f i x)" by(rule order.antisym)
+ qed
+ also have "\<dots> = (SUP i:Y. (\<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV))"
+ using chain' nonempty by(rule nn_integral_monotone_convergence_SUP_nat') simp
+ also have "\<dots> = ?rhs" by(simp add: nn_integral_max_0)
+ finally show ?thesis .
+qed
+
subsubsection {* Measures with Restricted Space *}
lemma simple_function_iff_borel_measurable:
--- a/src/HOL/Probability/Probability_Mass_Function.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Wed Apr 15 16:48:24 2015 +0200
@@ -224,6 +224,9 @@
shows "emeasure M {x} = pmf M x"
by transfer (simp add: finite_measure.emeasure_eq_measure[OF prob_space.finite_measure])
+lemma measure_pmf_single: "measure (measure_pmf M) {x} = pmf M x"
+using emeasure_pmf_single[of M x] by(simp add: measure_pmf.emeasure_eq_measure)
+
lemma emeasure_measure_pmf_finite: "finite S \<Longrightarrow> emeasure (measure_pmf M) S = (\<Sum>s\<in>S. pmf M s)"
by (subst emeasure_eq_setsum_singleton) (auto simp: emeasure_pmf_single)
@@ -510,13 +513,13 @@
finally show ?thesis .
qed
-lemma map_return_pmf: "map_pmf f (return_pmf x) = return_pmf (f x)"
+lemma map_return_pmf [simp]: "map_pmf f (return_pmf x) = return_pmf (f x)"
by transfer (simp add: distr_return)
lemma map_pmf_const[simp]: "map_pmf (\<lambda>_. c) M = return_pmf c"
by transfer (auto simp: prob_space.distr_const)
-lemma pmf_return: "pmf (return_pmf x) y = indicator {y} x"
+lemma pmf_return [simp]: "pmf (return_pmf x) y = indicator {y} x"
by transfer (simp add: measure_return)
lemma nn_integral_return_pmf[simp]: "0 \<le> f x \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>return_pmf x) = f x"
@@ -592,7 +595,7 @@
then show "emeasure ?L X = emeasure ?R X"
apply (simp add: emeasure_bind[OF _ M' X])
apply (simp add: nn_integral_bind[where B="count_space UNIV"] pair_pmf_def measure_pmf_bind[of A]
- nn_integral_measure_pmf_finite emeasure_nonneg pmf_return one_ereal_def[symmetric])
+ nn_integral_measure_pmf_finite emeasure_nonneg one_ereal_def[symmetric])
apply (subst emeasure_bind[OF _ _ X])
apply measurable
apply (subst emeasure_bind[OF _ _ X])
@@ -624,6 +627,16 @@
by (auto simp: pmf.rep_eq map_pmf_rep_eq measure_distr AE_measure_pmf_iff inj_onD
intro!: measure_pmf.finite_measure_eq_AE)
+lemma pmf_map_inj': "inj f \<Longrightarrow> pmf (map_pmf f M) (f x) = pmf M x"
+apply(cases "x \<in> set_pmf M")
+ apply(simp add: pmf_map_inj[OF subset_inj_on])
+apply(simp add: pmf_eq_0_set_pmf[symmetric])
+apply(auto simp add: pmf_eq_0_set_pmf dest: injD)
+done
+
+lemma pmf_map_outside: "x \<notin> f ` set_pmf M \<Longrightarrow> pmf (map_pmf f M) x = 0"
+unfolding pmf_eq_0_set_pmf by simp
+
subsection \<open> PMFs as function \<close>
context
@@ -651,6 +664,9 @@
by transfer (simp add: measure_def emeasure_density nonneg max_def)
qed
+lemma set_embed_pmf: "set_pmf embed_pmf = {x. f x \<noteq> 0}"
+by(auto simp add: set_pmf_eq assms pmf_embed_pmf)
+
end
lemma embed_pmf_transfer:
@@ -700,6 +716,9 @@
end
+lemma nn_integral_measure_pmf: "(\<integral>\<^sup>+ x. f x \<partial>measure_pmf p) = \<integral>\<^sup>+ x. ereal (pmf p x) * f x \<partial>count_space UNIV"
+by(simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg)
+
locale pmf_as_function
begin
@@ -896,11 +915,11 @@
then show "\<And>x y. (x, y) \<in> set_pmf ?pq \<Longrightarrow> R x y"
by auto
show "map_pmf fst ?pq = p"
- by (simp add: map_bind_pmf map_return_pmf bind_return_pmf')
+ by (simp add: map_bind_pmf bind_return_pmf')
show "map_pmf snd ?pq = q"
using R eq
- apply (simp add: bind_cond_pmf_cancel map_bind_pmf map_return_pmf bind_return_pmf')
+ apply (simp add: bind_cond_pmf_cancel map_bind_pmf bind_return_pmf')
apply (rule bind_cond_pmf_cancel)
apply (auto simp: rel_set_def)
done
@@ -1064,10 +1083,10 @@
by blast
next
have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {yz. fst yz = y}))"
- by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_return_pmf map_pmf_comp)
+ by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_pmf_comp)
then show "map_pmf snd pr = r"
unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute)
- qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf map_pmf_def[symmetric] p map_pmf_comp) }
+ qed (simp add: pr_def map_bind_pmf split_beta map_pmf_def[symmetric] p map_pmf_comp) }
then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
by(auto simp add: le_fun_def)
qed (fact natLeq_card_order natLeq_cinfinite)+
@@ -1420,8 +1439,59 @@
lemma emeasure_pmf_of_set[simp]: "emeasure pmf_of_set S = 1"
by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff)
+lemma nn_integral_pmf_of_set':
+ "(\<And>x. x \<in> S \<Longrightarrow> f x \<ge> 0) \<Longrightarrow> nn_integral (measure_pmf pmf_of_set) f = setsum f S / card S"
+apply(subst nn_integral_measure_pmf_finite, simp_all add: S_finite)
+apply(simp add: setsum_ereal_left_distrib[symmetric])
+apply(subst ereal_divide', simp add: S_not_empty S_finite)
+apply(simp add: ereal_times_divide_eq one_ereal_def[symmetric])
+done
+
+lemma nn_integral_pmf_of_set:
+ "nn_integral (measure_pmf pmf_of_set) f = setsum (max 0 \<circ> f) S / card S"
+apply(subst nn_integral_max_0[symmetric])
+apply(subst nn_integral_pmf_of_set')
+apply simp_all
+done
+
+lemma integral_pmf_of_set:
+ "integral\<^sup>L (measure_pmf pmf_of_set) f = setsum f S / card S"
+apply(simp add: real_lebesgue_integral_def integrable_measure_pmf_finite nn_integral_pmf_of_set S_finite)
+apply(subst real_of_ereal_minus')
+ apply(simp add: ereal_max_0 S_finite del: ereal_max)
+apply(simp add: ereal_max_0 S_finite S_not_empty del: ereal_max)
+apply(simp add: field_simps S_finite S_not_empty)
+apply(subst setsum.distrib[symmetric])
+apply(rule setsum.cong; simp_all)
+done
+
end
+lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x"
+by(rule pmf_eqI)(simp add: indicator_def)
+
+lemma map_pmf_of_set_inj:
+ assumes f: "inj_on f A"
+ and [simp]: "A \<noteq> {}" "finite A"
+ shows "map_pmf f (pmf_of_set A) = pmf_of_set (f ` A)" (is "?lhs = ?rhs")
+proof(rule pmf_eqI)
+ fix i
+ show "pmf ?lhs i = pmf ?rhs i"
+ proof(cases "i \<in> f ` A")
+ case True
+ then obtain i' where "i = f i'" "i' \<in> A" by auto
+ thus ?thesis using f by(simp add: card_image pmf_map_inj)
+ next
+ case False
+ hence "pmf ?lhs i = 0" by(simp add: pmf_eq_0_set_pmf set_map_pmf)
+ moreover have "pmf ?rhs i = 0" using False by simp
+ ultimately show ?thesis by simp
+ qed
+qed
+
+lemma bernoulli_pmf_half_conv_pmf_of_set: "bernoulli_pmf (1 / 2) = pmf_of_set UNIV"
+by(rule pmf_eqI) simp_all
+
subsubsection \<open> Poisson Distribution \<close>
context
--- a/src/HOL/Probability/Sigma_Algebra.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Apr 15 16:48:24 2015 +0200
@@ -2361,6 +2361,10 @@
by simp
qed
+lemma sets_restrict_space_count_space :
+ "sets (restrict_space (count_space A) B) = sets (count_space (A \<inter> B))"
+by(auto simp add: sets_restrict_space)
+
lemma sets_restrict_UNIV[simp]: "sets (restrict_space M UNIV) = sets M"
by (auto simp add: sets_restrict_space)
--- a/src/HOL/Product_Type.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Product_Type.thy Wed Apr 15 16:48:24 2015 +0200
@@ -1224,6 +1224,18 @@
using * eq[symmetric] by auto
qed simp_all
+lemma inj_on_apfst [simp]: "inj_on (apfst f) (A \<times> UNIV) \<longleftrightarrow> inj_on f A"
+by(auto simp add: inj_on_def)
+
+lemma inj_apfst [simp]: "inj (apfst f) \<longleftrightarrow> inj f"
+using inj_on_apfst[of f UNIV] by simp
+
+lemma inj_on_apsnd [simp]: "inj_on (apsnd f) (UNIV \<times> A) \<longleftrightarrow> inj_on f A"
+by(auto simp add: inj_on_def)
+
+lemma inj_apsnd [simp]: "inj (apsnd f) \<longleftrightarrow> inj f"
+using inj_on_apsnd[of f UNIV] by simp
+
definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
[code_abbrev]: "product A B = A \<times> B"
--- a/src/HOL/Relation.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Relation.thy Wed Apr 15 16:48:24 2015 +0200
@@ -216,6 +216,8 @@
"refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)"
by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
+lemma reflp_equality [simp]: "reflp op ="
+by(simp add: reflp_def)
subsubsection {* Irreflexivity *}
@@ -357,6 +359,8 @@
lemma antisym_empty [simp]: "antisym {}"
by (unfold antisym_def) blast
+lemma antisymP_equality [simp]: "antisymP op ="
+by(auto intro: antisymI)
subsubsection {* Transitivity *}
--- a/src/HOL/Set.thy Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Set.thy Wed Apr 15 16:48:24 2015 +0200
@@ -647,7 +647,6 @@
lemma empty_not_UNIV[simp]: "{} \<noteq> UNIV"
by blast
-
subsubsection {* The Powerset operator -- Pow *}
definition Pow :: "'a set => 'a set set" where
@@ -846,6 +845,9 @@
assume ?R thus ?L by (auto split: if_splits)
qed
+lemma insert_UNIV: "insert x UNIV = UNIV"
+by auto
+
subsubsection {* Singletons, using insert *}
lemma singletonI [intro!]: "a : {a}"
@@ -1884,6 +1886,8 @@
lemma bind_const: "Set.bind A (\<lambda>_. B) = (if A = {} then {} else B)"
by (auto simp add: bind_def)
+lemma bind_singleton_conv_image: "Set.bind A (\<lambda>x. {f x}) = f ` A"
+ by(auto simp add: bind_def)
subsubsection {* Operations for execution *}
--- a/src/HOL/Tools/etc/options Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/Tools/etc/options Wed Apr 15 16:48:24 2015 +0200
@@ -26,11 +26,11 @@
section "Miscellaneous Tools"
-public option sledgehammer_provers : string = "e spass remote_vampire"
- -- "ATPs for Sledgehammer (separated by blanks)"
+public option sledgehammer_provers : string = "cvc4 remote_vampire z3 spass e"
+ -- "provers for Sledgehammer (separated by blanks)"
public option sledgehammer_timeout : int = 30
- -- "ATPs will be interrupted after this time (in seconds)"
+ -- "provers will be interrupted after this time (in seconds)"
public option MaSh : string = "sml"
-- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"
--- a/src/HOL/ex/document/root.tex Wed Apr 15 15:10:01 2015 +0200
+++ b/src/HOL/ex/document/root.tex Wed Apr 15 16:48:24 2015 +0200
@@ -4,6 +4,7 @@
\usepackage[english]{babel}
\usepackage{textcomp}
\usepackage{amssymb}
+\usepackage{wasysym}
\usepackage{pdfsetup}
\urlstyle{rm}
--- a/src/Pure/Isar/outer_syntax.ML Wed Apr 15 15:10:01 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Wed Apr 15 16:48:24 2015 +0200
@@ -177,22 +177,18 @@
| SOME (Command {command_parser = Limited_Parser parse, ...}) =>
before_command :|-- (fn limited =>
Parse.!!! (command_tags |-- parse limited)) >> (fn f => f tr0)
- | NONE =>
- Scan.succeed
- (tr0 |> Toplevel.imperative (fn () => err_command "Undefined command " name [pos])))
+ | NONE => Scan.fail_with (fn _ => fn _ => err_command "Undefined command " name [pos]))
end);
val parse_cmt = Parse.$$$ "--" -- Parse.!!! Parse.document_source;
-in
-
fun commands_source thy =
Token.source_proper #>
Source.source Token.stopper (Scan.bulk (parse_cmt >> K NONE || Parse.not_eof >> SOME)) #>
Source.map_filter I #>
Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy) xs));
-end;
+in
fun parse thy pos str =
Source.of_string str
@@ -206,6 +202,8 @@
|> commands_source thy
|> Source.exhaust;
+end;
+
(* parse spans *)
--- a/src/Pure/Isar/toplevel.ML Wed Apr 15 15:10:01 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Apr 15 16:48:24 2015 +0200
@@ -31,7 +31,7 @@
val empty: transition
val name_of: transition -> string
val pos_of: transition -> Position.T
- val type_error: transition -> state -> string
+ val type_error: transition -> string
val name: string -> transition -> transition
val position: Position.T -> transition -> transition
val init_theory: (unit -> theory) -> transition -> transition
@@ -309,11 +309,12 @@
fun name_of (Transition {name, ...}) = name;
fun pos_of (Transition {pos, ...}) = pos;
-fun command_msg msg tr = msg ^ "command " ^ quote (name_of tr) ^ Position.here (pos_of tr);
-fun at_command tr = command_msg "At " tr;
+fun command_msg msg tr =
+ msg ^ "command " ^ quote (Markup.markup Markup.keyword1 (name_of tr)) ^
+ Position.here (pos_of tr);
-fun type_error tr state =
- command_msg "Illegal application of " tr ^ " " ^ str_of_state state;
+fun at_command tr = command_msg "At " tr;
+fun type_error tr = command_msg "Bad context for " tr;
(* modify transitions *)
@@ -569,9 +570,7 @@
val timing_props =
Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
val _ = Timing.protocol_message timing_props timing_result;
- in
- (result, Option.map (fn UNDEF => ERROR (type_error tr state) | exn => exn) opt_err)
- end);
+ in (result, Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn) opt_err) end);
in
--- a/src/Pure/PIDE/command.ML Wed Apr 15 15:10:01 2015 +0200
+++ b/src/Pure/PIDE/command.ML Wed Apr 15 16:48:24 2015 +0200
@@ -170,7 +170,7 @@
in
(case res of
NONE => st0
- | SOME st => (Output.error_message (Toplevel.type_error tr st0 ^ " -- using reset state"); st))
+ | SOME st => (Output.error_message (Toplevel.type_error tr ^ " -- using reset state"); st))
end) ();
fun run keywords int tr st =
--- a/src/Pure/PIDE/protocol.ML Wed Apr 15 15:10:01 2015 +0200
+++ b/src/Pure/PIDE/protocol.ML Wed Apr 15 16:48:24 2015 +0200
@@ -16,7 +16,7 @@
(fn [options_yxml] =>
let val options = Options.decode (YXML.parse_body options_yxml) in
Options.set_default options;
- Future.ML_statistics := true;
+ Future.ML_statistics := Options.bool options "ML_statistics";
Multithreading.trace := Options.int options "threads_trace";
Multithreading.max_threads_update (Options.int options "threads");
Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
--- a/src/Pure/PIDE/session.scala Wed Apr 15 15:10:01 2015 +0200
+++ b/src/Pure/PIDE/session.scala Wed Apr 15 16:48:24 2015 +0200
@@ -624,11 +624,6 @@
def update_options(options: Options)
{ manager.send_wait(Update_Options(options)) }
- def init_options(options: Options)
- {
- update_options(options)
- }
-
def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
{ manager.send(Session.Dialog_Result(id, serial, result)) }
--- a/src/Pure/Thy/present.scala Wed Apr 15 15:10:01 2015 +0200
+++ b/src/Pure/Thy/present.scala Wed Apr 15 16:48:24 2015 +0200
@@ -12,6 +12,32 @@
object Present
{
+ /* session graph */
+
+ def session_graph(
+ parent_session: String,
+ parent_loaded: String => Boolean,
+ deps: List[Thy_Info.Dep]): Graph_Display.Graph =
+ {
+ val parent_session_node =
+ Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
+
+ def node(name: Document.Node.Name): Graph_Display.Node =
+ if (parent_loaded(name.theory)) parent_session_node
+ else Graph_Display.Node(name.theory, "theory." + name.theory)
+
+ (Graph_Display.empty_graph /: deps) {
+ case (g, dep) =>
+ if (parent_loaded(dep.name.theory)) g
+ else {
+ val a = node(dep.name)
+ val bs = dep.header.imports.map({ case (name, _) => node(name) })
+ ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
+ }
+ }
+ }
+
+
/* maintain chapter index -- NOT thread-safe */
private val index_path = Path.basic("index.html")
@@ -48,4 +74,3 @@
File.write(dir + index_path, HTML.chapter_index(chapter, sessions))
}
}
-
--- a/src/Pure/Thy/thy_info.scala Wed Apr 15 15:10:01 2015 +0200
+++ b/src/Pure/Thy/thy_info.scala Wed Apr 15 16:48:24 2015 +0200
@@ -7,6 +7,15 @@
package isabelle
+object Thy_Info
+{
+ /* dependencies */
+
+ sealed case class Dep(
+ name: Document.Node.Name,
+ header: Document.Node.Header)
+}
+
class Thy_Info(resources: Resources)
{
/* messages */
@@ -24,29 +33,18 @@
/* dependencies */
- sealed case class Dep(
- name: Document.Node.Name,
- header: Document.Node.Header)
- {
- def loaded_files(syntax: Prover.Syntax): List[String] =
- {
- val string = resources.with_thy_reader(name, reader => Symbol.decode(reader.source.toString))
- resources.loaded_files(syntax, string)
- }
- }
-
object Dependencies
{
val empty = new Dependencies(Nil, Nil, Multi_Map.empty, Multi_Map.empty)
}
final class Dependencies private(
- rev_deps: List[Dep],
+ rev_deps: List[Thy_Info.Dep],
val keywords: Thy_Header.Keywords,
val seen_names: Multi_Map[String, Document.Node.Name],
val seen_positions: Multi_Map[String, Position.T])
{
- def :: (dep: Dep): Dependencies =
+ def :: (dep: Thy_Info.Dep): Dependencies =
new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords,
seen_names, seen_positions)
@@ -58,7 +56,7 @@
seen_positions + (name.theory -> pos))
}
- def deps: List[Dep] = rev_deps.reverse
+ def deps: List[Thy_Info.Dep] = rev_deps.reverse
def errors: List[String] =
{
@@ -84,33 +82,16 @@
def loaded_files: List[Path] =
{
- val dep_files =
- Par_List.map(
- (dep: Dep) =>
- dep.loaded_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a)),
- rev_deps)
+ def loaded(dep: Thy_Info.Dep): List[Path] =
+ {
+ val string = resources.with_thy_reader(dep.name,
+ reader => Symbol.decode(reader.source.toString))
+ resources.loaded_files(syntax, string).
+ map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
+ }
+ val dep_files = Par_List.map(loaded _, rev_deps)
((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
}
-
- def deps_graph(parent_session: String, parent_loaded: String => Boolean): Graph_Display.Graph =
- {
- val parent_session_node =
- Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
-
- def node(name: Document.Node.Name): Graph_Display.Node =
- if (parent_loaded(name.theory)) parent_session_node
- else Graph_Display.Node(name.theory, "theory." + name.theory)
-
- (Graph_Display.empty_graph /: rev_deps) {
- case (g, dep) =>
- if (parent_loaded(dep.name.theory)) g
- else {
- val a = node(dep.name)
- val bs = dep.header.imports.map({ case (name, _) => node(name) })
- ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
- }
- }
- }
}
private def require_thys(session: String, initiators: List[Document.Node.Name],
@@ -136,11 +117,12 @@
val header =
try { resources.check_thy(session, name, Token.Pos.file(name.node)).cat_errors(message) }
catch { case ERROR(msg) => cat_error(msg, message) }
- Dep(name, header) :: require_thys(session, name :: initiators, required1, header.imports)
+ Thy_Info.Dep(name, header) ::
+ require_thys(session, name :: initiators, required1, header.imports)
}
catch {
case e: Throwable =>
- Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1
+ Thy_Info.Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1
}
}
}
--- a/src/Pure/Tools/build.scala Wed Apr 15 15:10:01 2015 +0200
+++ b/src/Pure/Tools/build.scala Wed Apr 15 16:48:24 2015 +0200
@@ -512,7 +512,8 @@
val sources = all_files.map(p => (p, SHA1.digest(p.file)))
- val session_graph = thy_deps.deps_graph(info.parent getOrElse "", loaded_theories0)
+ val session_graph =
+ Present.session_graph(info.parent getOrElse "", loaded_theories0, thy_deps.deps)
val content =
Session_Content(loaded_theories, known_theories, keywords, syntax,
--- a/src/Tools/jEdit/src/isabelle.scala Wed Apr 15 15:10:01 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Wed Apr 15 16:48:24 2015 +0200
@@ -173,17 +173,14 @@
private val CONTINUOUS_CHECKING = "editor_continuous_checking"
def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
-
- def continuous_checking_=(b: Boolean)
- {
- GUI_Thread.require {}
-
- if (continuous_checking != b) {
- PIDE.options.bool(CONTINUOUS_CHECKING) = b
- PIDE.options_changed()
- PIDE.editor.flush()
+ def continuous_checking_=(b: Boolean): Unit =
+ GUI_Thread.require {
+ if (continuous_checking != b) {
+ PIDE.options.bool(CONTINUOUS_CHECKING) = b
+ PIDE.options_changed()
+ PIDE.editor.flush()
+ }
}
- }
def set_continuous_checking() { continuous_checking = true }
def reset_continuous_checking() { continuous_checking = false }
@@ -198,6 +195,28 @@
}
+ /* ML statistics */
+
+ private val ML_STATISTICS = "ML_statistics"
+
+ def ml_statistics: Boolean = PIDE.options.bool(ML_STATISTICS)
+ def ml_statistics_=(b: Boolean): Unit =
+ GUI_Thread.require {
+ if (ml_statistics != b) {
+ PIDE.options.bool(ML_STATISTICS) = b
+ PIDE.session.update_options(PIDE.options.value)
+ }
+ }
+
+ class ML_Stats extends CheckBox("ML statistics")
+ {
+ tooltip = "Enable ML runtime system statistics"
+ reactions += { case ButtonClicked(_) => ml_statistics = selected }
+ def load() { selected = ml_statistics }
+ load()
+ }
+
+
/* required document nodes */
private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
--- a/src/Tools/jEdit/src/monitor_dockable.scala Wed Apr 15 15:10:01 2015 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Wed Apr 15 16:48:24 2015 +0200
@@ -44,6 +44,8 @@
/* controls */
+ private val ml_stats = new Isabelle.ML_Stats
+
private val select_data = new ComboBox[String](
ML_Statistics.standard_fields.map(_._1))
{
@@ -65,7 +67,8 @@
}
}
- private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(select_data, reset_data)
+ private val controls =
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(ml_stats, select_data, reset_data)
/* layout */
@@ -77,13 +80,24 @@
/* main */
private val main =
- Session.Consumer[Session.Statistics](getClass.getName) {
- case stats =>
+ Session.Consumer[Any](getClass.getName) {
+ case stats: Session.Statistics =>
rev_stats.change(stats.props :: _)
delay_update.invoke()
+
+ case _: Session.Global_Options =>
+ GUI_Thread.later { ml_stats.load() }
}
- override def init() { PIDE.session.statistics += main }
- override def exit() { PIDE.session.statistics -= main }
+ override def init()
+ {
+ PIDE.session.statistics += main
+ PIDE.session.global_options += main
+ }
+
+ override def exit()
+ {
+ PIDE.session.statistics -= main
+ PIDE.session.global_options -= main
+ }
}
-
--- a/src/Tools/jEdit/src/plugin.scala Wed Apr 15 15:10:01 2015 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Wed Apr 15 16:48:24 2015 +0200
@@ -261,7 +261,7 @@
}
case Session.Ready =>
- PIDE.session.init_options(PIDE.options.value)
+ PIDE.session.update_options(PIDE.options.value)
PIDE.init_models()
if (!Isabelle.continuous_checking) {
--- a/src/Tools/jEdit/src/protocol_dockable.scala Wed Apr 15 15:10:01 2015 +0200
+++ b/src/Tools/jEdit/src/protocol_dockable.scala Wed Apr 15 16:48:24 2015 +0200
@@ -9,6 +9,8 @@
import isabelle._
+import java.awt.BorderLayout
+
import scala.swing.{TextArea, ScrollPane}
import org.gjt.sp.jedit.View
@@ -16,21 +18,47 @@
class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
{
+ /* controls */
+
+ private val ml_stats = new Isabelle.ML_Stats
+
+ private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(ml_stats)
+
+
+ /* text area */
+
private val text_area = new TextArea
+
+
+ /* layout */
+
set_content(new ScrollPane(text_area))
+ add(controls.peer, BorderLayout.NORTH)
/* main */
private val main =
- Session.Consumer[Prover.Message](getClass.getName) {
+ Session.Consumer[Any](getClass.getName) {
case input: Prover.Input =>
GUI_Thread.later { text_area.append(input.toString + "\n\n") }
case output: Prover.Output =>
GUI_Thread.later { text_area.append(output.message.toString + "\n\n") }
+
+ case _: Session.Global_Options =>
+ GUI_Thread.later { ml_stats.load() }
}
- override def init() { PIDE.session.all_messages += main }
- override def exit() { PIDE.session.all_messages -= main }
+ override def init()
+ {
+ PIDE.session.all_messages += main
+ PIDE.session.global_options += main
+ }
+
+ override def exit()
+ {
+ PIDE.session.all_messages -= main
+ PIDE.session.global_options -= main
+ }
}