Hallo, I just had a strange build failure with HOL-Probability. I executed
manuel@colosson ~/.i/etc> isabelle-dev build -d '$AFP' Random_BSTs Euler_MacLaurin Bertrands_Postulate and HOL-Probability failed to build: Building HOL-Probability ... HOL-Probability FAILED (see also /home/manuel/.isabelle/heaps/polyml-5.6_x86-linux/log/HOL-Probability) (full console output and build log attached). There is absolutely nothing in the build log that indicates an error to me. Also, I built HOL-Probability (without -b) a few minutes before that and it went through fine, and when I built it again a few minutes after the failure, it also worked fine. For completeness, the tests were executed on an up-to-date Arch Linux with 32 GB of RAM and a completely fresh Isabelle installation; i.e. no settings were modified except that AFP was registered as a component. In particular, it ran in 32 bit mode. Cheers, Manuel
Building Landau_Analysis ... Finished Landau_Analysis (0:00:29 elapsed time, 0:01:07 cpu time, factor 2.31) Building HOL-Number_Theory ... Finished HOL-Number_Theory (0:01:09 elapsed time, 0:03:57 cpu time, factor 3.43) Building Lehmer ... Finished Lehmer (0:00:20 elapsed time, 0:00:38 cpu time, factor 1.90) Building Pratt_Certificate ... Finished Pratt_Certificate (0:00:25 elapsed time, 0:01:05 cpu time, factor 2.57) Building HOL-Probability ... HOL-Probability FAILED (see also /home/manuel/.isabelle/heaps/polyml-5.6_x86-linux/log/HOL-Probability) ### ("\<^const>Fun.comp" ("_position" f) ("_position" X)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### inverse ?a1 \<equiv> (1::?'a1) / ?a1 ### Ignoring duplicate rewrite rule: ### inverse ?a1 ^ ?n1 \<equiv> inverse (?a1 ^ ?n1) ### Ignoring duplicate rewrite rule: ### ((1::?'a1) / ?a1) ^ ?n1 \<equiv> (1::?'a1) / ?a1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### (?a1 / ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 / ?b1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### frontier {..?a1} \<equiv> {?a1} ### Ambiguous input (line 1868 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.mutual_information_Pow" ("_position" X) ### ("_position" Z)) ### ("\<^const>Groups.minus_class.minus" ### ("\<^const>local.entropy_Pow" ("_position" X)) ### ("\<^const>local.entropy_Pow" ### ("\<^const>HOL.disj" ("_position" X) ("_position" Z)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.mutual_information_Pow" ("_position" X) ### ("_position" Z)) ### ("\<^const>Groups.minus_class.minus" ### ("\<^const>local.entropy_Pow" ("_position" X)) ### ("\<^const>local.conditional_entropy_Pow" ("_position" X) ### ("_position" Z))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. Quick_Sort_Cost CANCELLED Running Bertrands_Postulate ... ^[^EFinished Bertrands_Postulate (0:01:15 elapsed time, 0:02:46 cpu time, factor 2.21) Running Euler_MacLaurin ... Finished Euler_MacLaurin (0:00:16 elapsed time, 0:00:32 cpu time, factor 1.95) Random_BSTs CANCELLED Unfinished session(s): HOL-Probability, Quick_Sort_Cost, Random_BSTs 0:05:30 elapsed time, 0:14:56 cpu time, factor 2.71
Loading theory "HOL-Probability.Fin_Map" (required by "Probability" via "HOL-Probability.Projective_Limit") Loading theory "HOL-Probability.Discrete_Topology" (required by "Probability") Loading theory "HOL-Probability.Probability_Measure" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions" via "HOL-Probability.Weak_Convergence" via "HOL-Probability.Distribution_Functions") Loading theory "HOL-Probability.Essential_Supremum" (required by "Probability") Loading theory "HOL-Probability.Stopping_Time" (required by "Probability") locale prob_space = fixes M :: "'a measure" assumes "prob_space M" instantiation discrete :: (type) metric_space dist_discrete == dist :: 'a discrete \<Rightarrow> 'a discrete \<Rightarrow> real uniformity_discrete == uniformity :: ('a discrete \<times> 'a discrete) filter open_discrete == open :: 'a discrete set \<Rightarrow> bool locale filtration = fixes \<Omega> :: "'a set" and F :: "'t \<Rightarrow> 'a measure" assumes "filtration \<Omega> F" ### theory "HOL-Probability.Discrete_Topology" ### 0.310s elapsed time, 1.793s cpu time, 0.063s GC time ### theory "HOL-Probability.Essential_Supremum" ### 0.315s elapsed time, 1.837s cpu time, 0.063s GC time ### theory "HOL-Probability.Stopping_Time" ### 0.374s elapsed time, 2.227s cpu time, 0.147s GC time ### Rule already declared as introduction (intro) ### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g locale pair_prob_space = fixes M1 :: "'a measure" and M2 :: "'b measure" assumes "pair_prob_space M1 M2" ### Rule already declared as introduction (intro) ### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g instantiation fmap :: (type, topological_space) topological_space open_fmap == open :: ('a \<Rightarrow>\<^sub>F 'b) set \<Rightarrow> bool locale product_prob_space = fixes M :: "'i \<Rightarrow> 'a measure" and I :: "'i set" assumes "product_prob_space M" instantiation fmap :: (type, metric_space) dist dist_fmap == dist :: 'a \<Rightarrow>\<^sub>F 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>F 'b \<Rightarrow> real instantiation fmap :: (type, metric_space) uniformity_dist uniformity_fmap == uniformity :: ('a \<Rightarrow>\<^sub>F 'b \<times> 'a \<Rightarrow>\<^sub>F 'b) filter ### Rule already declared as introduction (intro) ### ((\<lambda>x. x) \<longlongrightarrow> ?a) (at ?a within ?s) instantiation fmap :: (type, metric_space) metric_space locale finite_product_prob_space = fixes M :: "'a \<Rightarrow> 'b measure" and I :: "'a set" assumes "finite_product_prob_space M I" instantiation fmap :: (countable, second_countable_topology) second_countable_topology ### Ignoring duplicate rewrite rule: ### \<Prod>_\<in>?A1. (1::?'a1) \<equiv> 1::?'a1 ### Rule already declared as introduction (intro) ### \<lbrakk>?a \<in> sets ?M; ?b \<in> sets ?M\<rbrakk> ### \<Longrightarrow> ?a \<inter> ?b \<in> sets ?M locale function_to_finmap = fixes J :: "'a set" and f :: "'a \<Rightarrow> 'b" and f' :: "'b \<Rightarrow> 'a" assumes "function_to_finmap J f f'" ### theory "HOL-Probability.Fin_Map" ### 1.297s elapsed time, 9.027s cpu time, 0.513s GC time ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### theory "HOL-Probability.Probability_Measure" ### 1.579s elapsed time, 11.077s cpu time, 0.603s GC time Loading theory "HOL-Probability.Conditional_Expectation" (required by "Probability") Loading theory "HOL-Probability.Distribution_Functions" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions" via "HOL-Probability.Weak_Convergence") Loading theory "HOL-Probability.Giry_Monad" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions" via "HOL-Probability.Independent_Family" via "HOL-Probability.Infinite_Product_Measure" via "HOL-Probability.Projective_Family") locale finite_borel_measure = fixes M :: "real measure" assumes "finite_borel_measure M" locale real_distribution = fixes M :: "real measure" assumes "real_distribution M" locale sigma_finite_subalgebra = fixes M :: "'a measure" and F :: "'a measure" assumes "sigma_finite_subalgebra M F" ### theory "HOL-Probability.Distribution_Functions" ### 0.364s elapsed time, 2.607s cpu time, 0.173s GC time Loading theory "HOL-Probability.Weak_Convergence" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions") locale finite_measure_subalgebra = fixes M :: "'a measure" and F :: "'a measure" assumes "finite_measure_subalgebra M F" locale sigma_finite_subalgebra = fixes M :: "'a measure" and F :: "'a measure" assumes "sigma_finite_subalgebra M F" ### Metis: Unused theorems: "Set.in_mono" locale sigma_finite_subalgebra = fixes M :: "'a measure" and F :: "'a measure" assumes "sigma_finite_subalgebra M F" locale right_continuous_mono = fixes f :: "real \<Rightarrow> real" and a :: "real" and b :: "real" assumes "right_continuous_mono f a b" locale cdf_distribution = fixes M :: "real measure" assumes "cdf_distribution M" locale subprob_space = fixes M :: "'a measure" assumes "subprob_space M" ### theory "HOL-Probability.Conditional_Expectation" ### 0.691s elapsed time, 4.937s cpu time, 0.307s GC time ### theory "HOL-Probability.Weak_Convergence" ### 0.375s elapsed time, 2.697s cpu time, 0.133s GC time Loading theory "HOL-Probability.Helly_Selection" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy") locale pair_subprob_space = fixes M1 :: "'a measure" and M2 :: "'b measure" assumes "pair_subprob_space M1 M2" val subprob_cong = fn: thm -> Proof.context -> 'a list * Proof.context ### theory "HOL-Probability.Giry_Monad" ### 1.618s elapsed time, 11.497s cpu time, 0.707s GC time Loading theory "HOL-Probability.Probability_Mass_Function" (required by "Probability" via "HOL-Probability.PMF_Impl") Loading theory "HOL-Probability.Projective_Family" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions" via "HOL-Probability.Independent_Family" via "HOL-Probability.Infinite_Product_Measure") ### theory "HOL-Probability.Helly_Selection" ### 1.089s elapsed time, 7.730s cpu time, 0.550s GC time ### Rule already declared as introduction (intro) ### (\<And>x. x \<in> space ?M \<Longrightarrow> ?P x) \<Longrightarrow> ### almost_everywhere ?M ?P locale projective_family = fixes I :: "'i set" and P :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" and M :: "'i \<Rightarrow> 'a measure" assumes "projective_family I P M" locale pmf_as_measure ### Generation of a parametrized correspondence relation failed. ### Reason: No relator for the type "Sigma_Algebra.measure" found. Proofs for inductive predicate(s) "generatorp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... locale Ionescu_Tulcea = fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a measure" and M :: "nat \<Rightarrow> 'a measure" assumes "Ionescu_Tulcea P M" consts C :: "nat \<Rightarrow> nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) measure" ### theory "HOL-Probability.Projective_Family" ### 0.815s elapsed time, 5.310s cpu time, 0.367s GC time Loading theory "HOL-Probability.Infinite_Product_Measure" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions" via "HOL-Probability.Independent_Family") locale pmf_as_function Proofs for inductive predicate(s) "rel_pmf" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... consts replicate_pmf :: "nat \<Rightarrow> 'a pmf \<Rightarrow> 'a list pmf" ### theory "HOL-Probability.Probability_Mass_Function" ### 1.643s elapsed time, 9.960s cpu time, 0.720s GC time Loading theory "HOL-Probability.PMF_Impl" (required by "Probability") locale sequence_space = fixes M :: "'a measure" assumes "sequence_space M" ### theory "HOL-Probability.Infinite_Product_Measure" ### 0.935s elapsed time, 5.257s cpu time, 0.400s GC time Loading theory "HOL-Probability.Random_Permutations" (required by "Probability") Loading theory "HOL-Probability.SPMF" (required by "Probability") Loading theory "HOL-Probability.Independent_Family" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions") ### theory "HOL-Probability.Random_Permutations" ### 0.871s elapsed time, 4.960s cpu time, 0.440s GC time Loading theory "HOL-Probability.Projective_Limit" (required by "Probability") instantiation pmf :: (equal) equal equal_pmf == equal_class.equal :: 'a pmf \<Rightarrow> 'a pmf \<Rightarrow> bool Loading theory "HOL-Probability.Stream_Space" (required by "Probability") ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True instantiation pmf :: (random) random random_pmf == random_class.random :: natural \<Rightarrow> natural \<times> natural \<Rightarrow> ('a pmf \<times> (unit \<Rightarrow> term)) \<times> natural \<times> natural ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True Proofs for inductive predicate(s) "ord_option" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... instantiation pmf :: (full_exhaustive) full_exhaustive full_exhaustive_pmf == full_exhaustive_class.full_exhaustive :: ('a pmf \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option ### theory "HOL-Probability.Independent_Family" ### 1.091s elapsed time, 6.890s cpu time, 0.660s GC time Loading theory "HOL-Probability.Convolution" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions" via "HOL-Probability.Distributions") ### theory "HOL-Probability.PMF_Impl" ### 1.783s elapsed time, 10.740s cpu time, 0.927s GC time Loading theory "HOL-Probability.Information" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions" via "HOL-Probability.Distributions") ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True consts sstart :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a stream set" consts scylinder :: "'a set \<Rightarrow> 'a set list \<Rightarrow> 'a stream set" locale finmap_seqs_into_compact = fixes K :: "nat \<Rightarrow> (nat \<Rightarrow>\<^sub>F 'a) set" and f :: "nat \<Rightarrow> nat \<Rightarrow>\<^sub>F 'a" and M :: "'b" assumes "finmap_seqs_into_compact K f" ### theory "HOL-Probability.Stream_Space" ### 1.039s elapsed time, 6.530s cpu time, 0.670s GC time locale polish_projective = fixes I :: "'i set" and P :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" assumes "polish_projective I P" ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True locale information_space = fixes M :: "'a measure" and b :: "real" assumes "information_space M b" locale information_space = fixes M :: "'a measure" and b :: "real" assumes "information_space M b" ### Ambiguous input (line 61 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" log) ### ("_cargs" ("_position" b) ### ("\<^const>Fields.inverse_class.inverse_divide" ("_position" A) ### ("_position" B)))) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ### ("\<^const>Groups.zero_class.zero") ### ("\<^const>Groups.times_class.times" ("_position" A) ### ("_position" B))) ### ("\<^const>Groups.minus_class.minus" ### ("_applC" ("_position" log) ### ("_cargs" ("_position" b) ### ("\<^const>Groups.abs_class.abs" ("_position" A)))) ### ("_applC" ("_position" log) ### ("_cargs" ("_position" b) ### ("\<^const>Groups.abs_class.abs" ("_position" B))))) ### ("_applC" ("_position" log) ### ("_cargs" ("_position" b) ("\<^const>Groups.zero_class.zero")))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" log) ### ("_cargs" ("_position" b) ### ("\<^const>Fields.inverse_class.inverse_divide" ("_position" A) ### ("_position" B)))) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ### ("\<^const>Groups.zero_class.zero") ### ("\<^const>Groups.times_class.times" ("_position" A) ### ("_position" B))) ### ("_applC" ("_position" log) ### ("_cargs" ("_position" b) ### ("\<^const>Groups.abs_class.abs" ### ("_applC" ("_position" A) ### ("_cargs" ### ("\<^const>Groups.abs_class.abs" ### ("\<^const>Groups.uminus_class.uminus" ### ("_applC" ("_position" log) ("_position" b)))) ### ("_position" B)))))) ### ("_applC" ("_position" log) ### ("_cargs" ("_position" b) ("\<^const>Groups.zero_class.zero")))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### theory "HOL-Probability.Convolution" ### 0.359s elapsed time, 2.133s cpu time, 0.230s GC time locale polish_product_prob_space = fixes I :: "'i set" assumes "polish_product_prob_space TYPE('a) TYPE('i)" locale ord_spmf_syntax ### theory "HOL-Probability.Projective_Limit" ### 1.547s elapsed time, 8.750s cpu time, 0.943s GC time ### Additional type variable(s) in locale specification "rel_spmf_characterisation": 'a, 'b locale rel_spmf_characterisation = assumes "rel_spmf_characterisation TYPE('a) TYPE('b)" ### Ambiguous input (line 947 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>Pure.eq" ### ("\<^fixed>conditional_mutual_information_Pow" ("_position" X) ### ("_position" Y) ("_position" Z)) ### ("_applC" ("_position" conditional_mutual_information) ### ("_cargs" ("_position" b) ### ("_cargs" ### ("_applC" ("_position" count_space) ### ("\<^const>Set.image" ("_position" X) ### ("_applC" ("_position" space) ("_position" M)))) ### ("_cargs" ### ("_applC" ("_position" count_space) ### ("\<^const>Set.image" ("_position" Y) ### ("_applC" ("_position" space) ("_position" M)))) ### ("_cargs" ### ("_applC" ("_position" count_space) ### ("\<^const>Set.image" ("_position" Z) ### ("_applC" ("_position" space) ("_position" M)))) ### ("_cargs" ("_position" X) ### ("_cargs" ("_position" Y) ("_position" Z))))))))) ### ("\<^const>Pure.eq" ### ("\<^const>local.mutual_information_Pow" ("_position" X) ### ("\<^const>HOL.disj" ("_position" Y) ("_position" Z))) ### ("_applC" ("_position" conditional_mutual_information) ### ("_cargs" ("_position" b) ### ("_cargs" ### ("_applC" ("_position" count_space) ### ("\<^const>Set.image" ("_position" X) ### ("_applC" ("_position" space) ("_position" M)))) ### ("_cargs" ### ("_applC" ("_position" count_space) ### ("\<^const>Set.image" ("_position" Y) ### ("_applC" ("_position" space) ("_position" M)))) ### ("_cargs" ### ("_applC" ("_position" count_space) ### ("\<^const>Set.image" ("_position" Z) ### ("_applC" ("_position" space) ("_position" M)))) ### ("_cargs" ("_position" X) ### ("_cargs" ("_position" Y) ("_position" Z))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ambiguous input (line 1440 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.conditional_mutual_information_Pow" ("_position" X) ### ("_position" Y) ("_position" Z)) ### ("_sum" ### ("_pattern" ("_position" x) ### ("_patterns" ("_position" y) ("_position" z))) ### ("\<^const>Set.image" ### ("_lambda" ("_position" x) ### ("_tuple" ("_applC" ("_position" X) ("_position" x)) ### ("_tuple_args" ("_applC" ("_position" Y) ("_position" x)) ### ("_tuple_arg" ("_applC" ("_position" Z) ("_position" x)))))) ### ("_applC" ("_position" space) ("_position" M))) ### ("\<^const>Groups.times_class.times" ### ("_applC" ("_position" Pxyz) ### ("_tuple" ("_position" x) ### ("_tuple_args" ("_position" y) ("_tuple_arg" ("_position" z))))) ### ("_applC" ("_position" log) ### ("_cargs" ("_position" b) ### ("\<^const>Fields.inverse_class.inverse_divide" ### ("_applC" ("_position" Pxyz) ### ("_tuple" ("_position" x) ### ("_tuple_args" ("_position" y) ### ("_tuple_arg" ("_position" z))))) ### ("\<^const>Groups.times_class.times" ### ("_applC" ("_position" Pxz) ### ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z)))) ### ("\<^const>Fields.inverse_class.inverse_divide" ### ("_applC" ("_position" Pyz) ### ("_tuple" ("_position" y) ### ("_tuple_arg" ("_position" z)))) ### ("_applC" ("_position" Pz) ("_position" z))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.mutual_information_Pow" ("_position" X) ### ("\<^const>HOL.disj" ("_position" Y) ("_position" Z))) ### ("_sum" ### ("_pattern" ("_position" x) ### ("_patterns" ("_position" y) ("_position" z))) ### ("\<^const>Set.image" ### ("_lambda" ("_position" x) ### ("_tuple" ("_applC" ("_position" X) ("_position" x)) ### ("_tuple_args" ("_applC" ("_position" Y) ("_position" x)) ### ("_tuple_arg" ("_applC" ("_position" Z) ("_position" x)))))) ### ("_applC" ("_position" space) ("_position" M))) ### ("\<^const>Groups.times_class.times" ### ("_applC" ("_position" Pxyz) ### ("_tuple" ("_position" x) ### ("_tuple_args" ("_position" y) ("_tuple_arg" ("_position" z))))) ### ("_applC" ("_position" log) ### ("_cargs" ("_position" b) ### ("\<^const>Fields.inverse_class.inverse_divide" ### ("_applC" ("_position" Pxyz) ### ("_tuple" ("_position" x) ### ("_tuple_args" ("_position" y) ### ("_tuple_arg" ("_position" z))))) ### ("\<^const>Groups.times_class.times" ### ("_applC" ("_position" Pxz) ### ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z)))) ### ("\<^const>Fields.inverse_class.inverse_divide" ### ("_applC" ("_position" Pyz) ### ("_tuple" ("_position" y) ### ("_tuple_arg" ("_position" z)))) ### ("_applC" ("_position" Pz) ("_position" z))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1487 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less_eq" ### ("\<^const>Groups.zero_class.zero") ### ("\<^const>local.mutual_information_Pow" ("_position" X) ### ("\<^const>HOL.disj" ("_position" Y) ("_position" Z))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less_eq" ### ("\<^const>Groups.zero_class.zero") ### ("\<^const>local.conditional_mutual_information_Pow" ("_position" X) ### ("_position" Y) ("_position" Z)))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1524 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>Pure.eq" ### ("\<^fixed>conditional_entropy_Pow" ("_position" X) ("_position" Y)) ### ("_applC" ("_position" conditional_entropy) ### ("_cargs" ("_position" b) ### ("_cargs" ### ("_applC" ("_position" count_space) ### ("\<^const>Set.image" ("_position" X) ### ("_applC" ("_position" space) ("_position" M)))) ### ("_cargs" ### ("_applC" ("_position" count_space) ### ("\<^const>Set.image" ("_position" Y) ### ("_applC" ("_position" space) ("_position" M)))) ### ("_cargs" ("_position" X) ("_position" Y))))))) ### ("\<^const>Pure.eq" ### ("\<^const>local.entropy_Pow" ### ("\<^const>HOL.disj" ("_position" X) ("_position" Y))) ### ("_applC" ("_position" conditional_entropy) ### ("_cargs" ("_position" b) ### ("_cargs" ### ("_applC" ("_position" count_space) ### ("\<^const>Set.image" ("_position" X) ### ("_applC" ("_position" space) ("_position" M)))) ### ("_cargs" ### ("_applC" ("_position" count_space) ### ("\<^const>Set.image" ("_position" Y) ### ("_applC" ("_position" space) ("_position" M)))) ### ("_cargs" ("_position" X) ("_position" Y))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1626 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.conditional_entropy_Pow" ("_position" X) ### ("_position" Y)) ### ("\<^const>Groups.minus_class.minus" ### ("_applC" ("_position" entropy) ### ("_cargs" ("_position" b) ### ("_cargs" ### ("\<^const>Binary_Product_Measure.pair_measure" ### ("_applC" ("_position" count_space) ### ("\<^const>Set.image" ("_position" X) ### ("_applC" ("_position" space) ("_position" M)))) ### ("_applC" ("_position" count_space) ### ("\<^const>Set.image" ("_position" Y) ### ("_applC" ("_position" space) ("_position" M))))) ### ("_lambda" ("_position" x) ### ("_tuple" ("_applC" ("_position" X) ("_position" x)) ### ("_tuple_arg" ### ("_applC" ("_position" Y) ("_position" x)))))))) ### ("\<^const>local.entropy_Pow" ("_position" Y))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.entropy_Pow" ### ("\<^const>HOL.disj" ("_position" X) ("_position" Y))) ### ("\<^const>Groups.minus_class.minus" ### ("_applC" ("_position" entropy) ### ("_cargs" ("_position" b) ### ("_cargs" ### ("\<^const>Binary_Product_Measure.pair_measure" ### ("_applC" ("_position" count_space) ### ("\<^const>Set.image" ("_position" X) ### ("_applC" ("_position" space) ("_position" M)))) ### ("_applC" ("_position" count_space) ### ("\<^const>Set.image" ("_position" Y) ### ("_applC" ("_position" space) ("_position" M))))) ### ("_lambda" ("_position" x) ### ("_tuple" ("_applC" ("_position" X) ("_position" x)) ### ("_tuple_arg" ### ("_applC" ("_position" Y) ("_position" x)))))))) ### ("\<^const>local.entropy_Pow" ("_position" Y))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1640 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.conditional_entropy_Pow" ("_position" X) ### ("_position" Y)) ### ("\<^const>Groups.uminus_class.uminus" ### ("_sum" ("_pattern" ("_position" x) ("_position" y)) ### ("\<^const>Set.image" ### ("_lambda" ("_position" x) ### ("_tuple" ("_applC" ("_position" X) ("_position" x)) ### ("_tuple_arg" ("_applC" ("_position" Y) ("_position" x))))) ### ("_applC" ("_position" space) ("_position" M))) ### ("\<^const>Groups.times_class.times" ### ("_applC" ("_position" Pxy) ### ("_tuple" ("_position" x) ("_tuple_arg" ("_position" y)))) ### ("_applC" ("_position" log) ### ("_cargs" ("_position" b) ### ("\<^const>Fields.inverse_class.inverse_divide" ### ("_applC" ("_position" Pxy) ### ("_tuple" ("_position" x) ("_tuple_arg" ("_position" y)))) ### ("_applC" ("_position" Py) ("_position" y)))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.entropy_Pow" ### ("\<^const>HOL.disj" ("_position" X) ("_position" Y))) ### ("\<^const>Groups.uminus_class.uminus" ### ("_sum" ("_pattern" ("_position" x) ("_position" y)) ### ("\<^const>Set.image" ### ("_lambda" ("_position" x) ### ("_tuple" ("_applC" ("_position" X) ("_position" x)) ### ("_tuple_arg" ("_applC" ("_position" Y) ("_position" x))))) ### ("_applC" ("_position" space) ("_position" M))) ### ("\<^const>Groups.times_class.times" ### ("_applC" ("_position" Pxy) ### ("_tuple" ("_position" x) ("_tuple_arg" ("_position" y)))) ### ("_applC" ("_position" log) ### ("_cargs" ("_position" b) ### ("\<^const>Fields.inverse_class.inverse_divide" ### ("_applC" ("_position" Pxy) ### ("_tuple" ("_position" x) ("_tuple_arg" ("_position" y)))) ### ("_applC" ("_position" Py) ("_position" y)))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1667 of "~~/src/HOL/Probability/Information.thy") produces 4 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.conditional_mutual_information_Pow" ("_position" X) ### ("_position" X) ("_position" Y)) ### ("\<^const>local.entropy_Pow" ### ("\<^const>HOL.disj" ("_position" X) ("_position" Y))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.mutual_information_Pow" ("_position" X) ### ("\<^const>HOL.disj" ("_position" X) ("_position" Y))) ### ("\<^const>local.entropy_Pow" ### ("\<^const>HOL.disj" ("_position" X) ("_position" Y))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.conditional_mutual_information_Pow" ("_position" X) ### ("_position" X) ("_position" Y)) ### ("\<^const>local.conditional_entropy_Pow" ("_position" X) ### ("_position" Y)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.mutual_information_Pow" ("_position" X) ### ("\<^const>HOL.disj" ("_position" X) ("_position" Y))) ### ("\<^const>local.conditional_entropy_Pow" ("_position" X) ### ("_position" Y)))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### theory "HOL-Probability.SPMF" ### 3.140s elapsed time, 14.943s cpu time, 1.740s GC time ### Ambiguous input (line 1709 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less_eq" ### ("\<^const>Groups.zero_class.zero") ### ("\<^const>local.entropy_Pow" ### ("\<^const>HOL.disj" ("_position" X) ("_position" Y))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less_eq" ### ("\<^const>Groups.zero_class.zero") ### ("\<^const>local.conditional_entropy_Pow" ("_position" X) ### ("_position" Y)))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ambiguous input (line 1816 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.mutual_information_Pow" ("_position" X) ### ("_position" Y)) ### ("\<^const>Groups.minus_class.minus" ### ("\<^const>local.entropy_Pow" ("_position" X)) ### ("\<^const>local.entropy_Pow" ### ("\<^const>HOL.disj" ("_position" X) ("_position" Y)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.mutual_information_Pow" ("_position" X) ### ("_position" Y)) ### ("\<^const>Groups.minus_class.minus" ### ("\<^const>local.entropy_Pow" ("_position" X)) ### ("\<^const>local.conditional_entropy_Pow" ("_position" X) ### ("_position" Y))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1865 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less_eq" ### ("\<^const>local.conditional_entropy_Pow" ("_position" X) ### ("_position" Z)) ### ("\<^const>local.entropy_Pow" ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less_eq" ### ("\<^const>local.entropy_Pow" ### ("\<^const>HOL.disj" ("_position" X) ("_position" Z))) ### ("\<^const>local.entropy_Pow" ("_position" X)))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1894 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.entropy_Pow" ### ("_lambda" ("_position" x) ### ("_tuple" ("_applC" ("_position" X) ("_position" x)) ### ("_tuple_arg" ("_applC" ("_position" Y) ("_position" x)))))) ### ("\<^const>Groups.plus_class.plus" ### ("\<^const>local.entropy_Pow" ("_position" X)) ### ("\<^const>local.entropy_Pow" ### ("\<^const>HOL.disj" ("_position" Y) ("_position" X)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.entropy_Pow" ### ("_lambda" ("_position" x) ### ("_tuple" ("_applC" ("_position" X) ("_position" x)) ### ("_tuple_arg" ("_applC" ("_position" Y) ("_position" x)))))) ### ("\<^const>Groups.plus_class.plus" ### ("\<^const>local.entropy_Pow" ("_position" X)) ### ("\<^const>local.conditional_entropy_Pow" ("_position" Y) ### ("_position" X))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1919 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("\<^const>local.entropy_Pow" ("_position" X)) ### ("\<^const>Groups.plus_class.plus" ### ("\<^const>local.entropy_Pow" ### ("\<^const>Fun.comp" ("_position" f) ("_position" X))) ### ("\<^const>local.entropy_Pow" ### ("\<^const>HOL.disj" ("_position" X) ### ("\<^const>Fun.comp" ("_position" f) ("_position" X))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("\<^const>local.entropy_Pow" ("_position" X)) ### ("\<^const>Groups.plus_class.plus" ### ("\<^const>local.entropy_Pow" ### ("\<^const>Fun.comp" ("_position" f) ("_position" X))) ### ("\<^const>local.conditional_entropy_Pow" ("_position" X) ### ("\<^const>Fun.comp" ("_position" f) ("_position" X)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### theory "HOL-Probability.Information" ### 2.267s elapsed time, 8.447s cpu time, 1.123s GC time Loading theory "HOL-Probability.Distributions" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy" via "HOL-Probability.Characteristic_Functions") ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Rule already declared as introduction (intro) ### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### set_pmf (map_pmf ?f1 ?M1) \<equiv> ?f1 ` set_pmf ?M1 ### Ignoring duplicate rewrite rule: ### \<lbrakk>\<And>i. 0 \<le> ?f1 i; ### (\<Sum>i. ennreal (?f1 i)) \<noteq> top\<rbrakk> ### \<Longrightarrow> \<Sum>i. ennreal (?f1 i) \<equiv> ennreal (\<Sum>i. ?f1 i) ### Rule already declared as introduction (intro) ### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g ### theory "HOL-Probability.Distributions" ### 1.507s elapsed time, 7.600s cpu time, 0.710s GC time Loading theory "HOL-Probability.Characteristic_Functions" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy") Loading theory "HOL-Probability.Sinc_Integral" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem" via "HOL-Probability.Levy") ### Ignoring duplicate rewrite rule: ### (\<And>x. ### x \<in> set ?xs1 \<Longrightarrow> 0 \<le> ?f1 x) \<Longrightarrow> ### \<Sum>x\<leftarrow>?xs1. ennreal (?f1 x) \<equiv> ### ennreal (sum_list (map ?f1 ?xs1)) ### theory "HOL-Probability.Sinc_Integral" ### 0.460s elapsed time, 2.760s cpu time, 0.277s GC time ### Rule already declared as introduction (intro) ### (\<And>x. x \<in> space ?M \<Longrightarrow> ?P x) \<Longrightarrow> ### almost_everywhere ?M ?P ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### theory "HOL-Probability.Characteristic_Functions" ### 1.534s elapsed time, 9.127s cpu time, 0.883s GC time Loading theory "HOL-Probability.Levy" (required by "Probability" via "HOL-Probability.Central_Limit_Theorem") ### Ignoring duplicate safe introduction (intro!) ### (\<And>i. {x \<in> space ?M. ?P i x} \<in> sets ?M) \<Longrightarrow> ### {x \<in> space ?M. \<forall>i. ?P i x} \<in> sets ?M ### Rule already declared as introduction (intro) ### \<lbrakk>?a \<in> sets ?M; ?b \<in> sets ?M\<rbrakk> ### \<Longrightarrow> ?a \<inter> ?b \<in> sets ?M ### theory "HOL-Probability.Levy" ### 1.710s elapsed time, 8.160s cpu time, 1.170s GC time Loading theory "HOL-Probability.Central_Limit_Theorem" (required by "Probability") ### theory "HOL-Probability.Central_Limit_Theorem" ### 0.867s elapsed time, 2.913s cpu time, 0.533s GC time Loading theory "Probability" ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?I; ?I \<noteq> {}; ### \<And>i. i \<in> ?I \<Longrightarrow> ?A i \<in> sets ?M\<rbrakk> ### \<Longrightarrow> (\<Inter>i\<in>?I. ?A i) \<in> sets ?M ### Ignoring duplicate rewrite rule: ### (\<And>x. ### x \<in> space ?M1 \<Longrightarrow> 0 \<le> ?f1 x) \<Longrightarrow> ### (\<lambda>x. ennreal (?f1 x)) \<in> borel_measurable ?M1 \<equiv> ### ?f1 \<in> borel_measurable ?M1 ### Ignoring duplicate rewrite rule: ### (\<And>x. ### x \<in> space ?M1 \<Longrightarrow> 0 \<le> ?f1 x) \<Longrightarrow> ### (\<lambda>x. ennreal (?f1 x)) \<in> borel_measurable ?M1 \<equiv> ### ?f1 \<in> borel_measurable ?M1 ### Rule already declared as introduction (intro) ### \<lbrakk>?a \<in> sets ?M; ?b \<in> sets ?M\<rbrakk> ### \<Longrightarrow> ?a \<inter> ?b \<in> sets ?M ### theory "Probability" ### 3.800s elapsed time, 16.140s cpu time, 3.853s GC time ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### of_nat (Suc ?m1) \<equiv> (1::?'a1) + of_nat ?m1 ### Ignoring duplicate rewrite rule: ### of_nat (Suc ?m1) \<equiv> (1::?'a1) + of_nat ?m1 ### Ignoring duplicate rewrite rule: ### of_nat (Suc ?m1) \<equiv> (1::?'a1) + of_nat ?m1 ### Ignoring duplicate rewrite rule: ### inverse ?a1 \<equiv> (1::?'a1) / ?a1 ### Ignoring duplicate rewrite rule: ### inverse ?a1 ^ ?n1 \<equiv> inverse (?a1 ^ ?n1) ### Ignoring duplicate rewrite rule: ### ((1::?'a1) / ?a1) ^ ?n1 \<equiv> (1::?'a1) / ?a1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### (?a1 / ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 / ?b1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### of_nat (Suc ?m1) \<equiv> (1::?'a1) + of_nat ?m1 ### Ignoring duplicate rewrite rule: ### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T) ### Rule already declared as introduction (intro) ### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> ### open (\<Union>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk> ### \<Longrightarrow> open (\<Inter>?S) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk> ### \<Longrightarrow> open (\<Inter>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; closed ?T\<rbrakk> ### \<Longrightarrow> closed (?S \<union> ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; closed ?T\<rbrakk> ### \<Longrightarrow> closed (?S \<inter> ?T) ### Rule already declared as introduction (intro) ### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow> ### closed (\<Inter>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter>?K) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk> ### \<Longrightarrow> closed (\<Union>?S) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk> ### \<Longrightarrow> closed (\<Union>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T) ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \<Longrightarrow> open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \<Longrightarrow> closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Rule already declared as introduction (intro) ### (\<And>i. continuous_on UNIV (\<lambda>x. ?f x i)) \<Longrightarrow> ### continuous_on UNIV ?f ### Ignoring duplicate rewrite rule: ### of_nat (?m1 * ?n1) \<equiv> of_nat ?m1 * of_nat ?n1 ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ambiguous input (line 1069 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_DDDOT") ### ("_nn_integral" ("_position" x) ### ("\<^const>Groups.times_class.times" ### ("_applC" ("_position" ennreal) ### ("_applC" ("_position" Pyz) ("_position" x))) ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Binary_Product_Measure.pair_measure" ("_position" T) ### ("_position" P))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_DDDOT") ### ("\<^const>Binary_Product_Measure.pair_measure" ### ("_nn_integral" ("_position" x) ### ("\<^const>Groups.times_class.times" ### ("_applC" ("_position" ennreal) ### ("_applC" ("_position" Pyz) ("_position" x))) ### ("\<^const>Groups.one_class.one")) ### ("_position" T)) ### ("_position" P)))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Introduced fixed type variable(s): 'c in "Sa__" or "Xa__" ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ambiguous input (line 1322 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_DDDOT") ### ("_nn_integral" ("_pattern" ("_position" y) ("_position" z)) ### ("_nn_integral" ("_position" x) ### ("\<^const>Groups.times_class.times" ### ("_applC" ("_position" ennreal) ### ("_applC" ("_position" Pxz) ### ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))))) ### ("_applC" ("_position" ennreal) ### ("\<^const>Fields.inverse_class.inverse_divide" ### ("_applC" ("_position" Pyz) ### ("_tuple" ("_position" y) ("_tuple_arg" ("_position" z)))) ### ("_applC" ("_position" Pz) ("_position" z))))) ### ("_position" S)) ### ("\<^const>Binary_Product_Measure.pair_measure" ("_position" T) ### ("_position" P))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_DDDOT") ### ("\<^const>Binary_Product_Measure.pair_measure" ### ("_nn_integral" ("_pattern" ("_position" y) ("_position" z)) ### ("_nn_integral" ("_position" x) ### ("\<^const>Groups.times_class.times" ### ("_applC" ("_position" ennreal) ### ("_applC" ("_position" Pxz) ### ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))))) ### ("_applC" ("_position" ennreal) ### ("\<^const>Fields.inverse_class.inverse_divide" ### ("_applC" ("_position" Pyz) ### ("_tuple" ("_position" y) ("_tuple_arg" ("_position" z)))) ### ("_applC" ("_position" Pz) ("_position" z))))) ### ("_position" S)) ### ("_position" T)) ### ("_position" P)))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ambiguous input (line 1326 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_DDDOT") ### ("_nn_integral" ("_position" x) ### ("\<^const>Groups.times_class.times" ### ("_applC" ("_position" ennreal) ### ("_applC" ("_position" Pyz) ("_position" x))) ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Binary_Product_Measure.pair_measure" ("_position" T) ### ("_position" P))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_DDDOT") ### ("\<^const>Binary_Product_Measure.pair_measure" ### ("_nn_integral" ("_position" x) ### ("\<^const>Groups.times_class.times" ### ("_applC" ("_position" ennreal) ### ("_applC" ("_position" Pyz) ("_position" x))) ### ("\<^const>Groups.one_class.one")) ### ("_position" T)) ### ("_position" P)))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### ((\<lambda>x. x) \<longlongrightarrow> ?a1) (at ?a1 within ?s1) \<equiv> ### True ### Ignoring duplicate rewrite rule: ### ((\<lambda>x. ?k1) \<longlongrightarrow> ?k1) ?F1 \<equiv> True ### Ignoring duplicate rewrite rule: ### (?f1 \<longlongrightarrow> ?x1) ?F1 \<Longrightarrow> ### ((\<lambda>x. ereal (?f1 x)) \<longlongrightarrow> ereal ?x1) ?F1 \<equiv> ### True ### Ignoring duplicate rewrite rule: ### (?f1 \<longlongrightarrow> ?x1) ?F1 \<Longrightarrow> ### ((\<lambda>x. - ?f1 x) \<longlongrightarrow> - ?x1) ?F1 \<equiv> True ### Ignoring duplicate rewrite rule: ### \<lbrakk>\<bar>?c1\<bar> \<noteq> \<infinity>; ### (?f1 \<longlongrightarrow> ?x1) ?F1\<rbrakk> ### \<Longrightarrow> ((\<lambda>x. ?c1 * ?f1 x) \<longlongrightarrow> ### ?c1 * ?x1) ### ?F1 \<equiv> ### True ### Ignoring duplicate rewrite rule: ### \<lbrakk>?x1 \<noteq> 0; (?f1 \<longlongrightarrow> ?x1) ?F1\<rbrakk> ### \<Longrightarrow> ((\<lambda>x. ?c1 * ?f1 x) \<longlongrightarrow> ### ?c1 * ?x1) ### ?F1 \<equiv> ### True ### Ignoring duplicate rewrite rule: ### \<lbrakk>?y1 \<noteq> - \<infinity>; ?x1 \<noteq> - \<infinity>; ### (?f1 \<longlongrightarrow> ?x1) ?F1\<rbrakk> ### \<Longrightarrow> ((\<lambda>x. ?f1 x + ?y1) \<longlongrightarrow> ### ?x1 + ?y1) ### ?F1 \<equiv> ### True ### Ignoring duplicate rewrite rule: ### \<lbrakk>\<bar>?y1\<bar> \<noteq> \<infinity>; ### (?f1 \<longlongrightarrow> ?x1) ?F1\<rbrakk> ### \<Longrightarrow> ((\<lambda>x. ?f1 x + ?y1) \<longlongrightarrow> ### ?x1 + ?y1) ### ?F1 \<equiv> ### True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Rule already declared as introduction (intro) ### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Rule already declared as introduction (intro) ### \<lbrakk>integrable ?M ?f; integrable ?M ?g\<rbrakk> ### \<Longrightarrow> integrable ?M (\<lambda>x. ?f x + ?g x) ### Rule already declared as introduction (intro) ### integrable ?M ?f \<Longrightarrow> ### integrable ?M (\<lambda>x. \<bar>?f x\<bar>) ### Rule already declared as introduction (intro) ### (?c \<noteq> (0::?'b) \<Longrightarrow> integrable ?M ?f) \<Longrightarrow> ### integrable ?M (\<lambda>x. ?c * ?f x) ### Rule already declared as introduction (intro) ### \<lbrakk>integrable ?M ?f; integrable ?M ?g\<rbrakk> ### \<Longrightarrow> integrable ?M (\<lambda>x. ?f x - ?g x) ### Rule already declared as introduction (intro) ### integrable M ?f \<Longrightarrow> integrable M (real_cond_exp M F ?f) ### Rule already declared as introduction (intro) ### ?A ` ?X \<subseteq> sets ?M \<Longrightarrow> ### (\<Union>x\<in>?X. ?A x) \<in> sets ?M ### Rule already declared as introduction (intro) ### integrable M ?f \<Longrightarrow> integrable M (real_cond_exp M F ?f) ### Rule already declared as introduction (intro) ### integrable M ?f \<Longrightarrow> ### integral\<^sup>L M (real_cond_exp M F ?f) = integral\<^sup>L M ?f ### Rule already declared as introduction (intro) ### integrable M ?f \<Longrightarrow> integrable M (real_cond_exp M F ?f) ### Rule already declared as introduction (intro) ### integrable M ?f \<Longrightarrow> ### integral\<^sup>L M (real_cond_exp M F ?f) = integral\<^sup>L M ?f ### Rule already declared as introduction (intro) ### \<lbrakk>integrable ?M ?f; integrable ?M ?g\<rbrakk> ### \<Longrightarrow> integrable ?M (\<lambda>x. ?f x + ?g x) ### Rule already declared as introduction (intro) ### integrable ?M ?f \<Longrightarrow> ### integrable ?M (\<lambda>x. \<bar>?f x\<bar>) ### Rule already declared as introduction (intro) ### integrable M ?f \<Longrightarrow> integrable M (real_cond_exp M F ?f) ### Rule already declared as introduction (intro) ### integrable M ?f \<Longrightarrow> ### integral\<^sup>L M (real_cond_exp M F ?f) = integral\<^sup>L M ?f ### Rule already declared as introduction (intro) ### (\<And>x. x \<in> space ?M \<Longrightarrow> ?P x) \<Longrightarrow> ### almost_everywhere ?M ?P ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> enn2real ?x1 \<equiv> True ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?I; ?I \<noteq> {}; ### \<And>i. i \<in> ?I \<Longrightarrow> ?A i \<in> sets ?M\<rbrakk> ### \<Longrightarrow> (\<Inter>i\<in>?I. ?A i) \<in> sets ?M ### Ignoring duplicate rewrite rule: ### 0 \<le> enn2real ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> enn2real ?x1 \<equiv> True ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?I; ?I \<noteq> {}; ### \<And>i. ### i \<in> ?I \<Longrightarrow> ### ?A i \<in> sigma_sets (space M) (\<Union>i\<in>I j. E i)\<rbrakk> ### \<Longrightarrow> (\<Inter>i\<in>?I. ?A i) ### \<in> sigma_sets (space M) (\<Union>i\<in>I j. E i) ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Rule already declared as introduction (intro) ### \<lbrakk>integrable ?M ?f; integrable ?M ?g\<rbrakk> ### \<Longrightarrow> integrable ?M (\<lambda>x. ?f x + ?g x) ### Rule already declared as introduction (intro) ### integrable ?M ?f \<Longrightarrow> ### integrable ?M (\<lambda>x. \<bar>?f x\<bar>) ### Rule already declared as introduction (intro) ### (?c \<noteq> (0::?'b) \<Longrightarrow> integrable ?M ?f) \<Longrightarrow> ### integrable ?M (\<lambda>x. ?c * ?f x) ### Rule already declared as introduction (intro) ### \<lbrakk>integrable ?M ?f; integrable ?M ?g\<rbrakk> ### \<Longrightarrow> integrable ?M (\<lambda>x. ?f x - ?g x) ### Rule already declared as introduction (intro) ### integrable M ?f \<Longrightarrow> integrable M (real_cond_exp M F ?f) ### Rule already declared as introduction (intro) ### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g ### Rule already declared as introduction (intro) ### \<lbrakk>?a \<in> sets ?M; ?b \<in> sets ?M\<rbrakk> ### \<Longrightarrow> ?a - ?b \<in> sets ?M ### Ignoring duplicate rewrite rule: ### \<Prod>_\<in>?A1. (1::?'a1) \<equiv> 1::?'a1 ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ambiguous input (line 1097 of "~~/src/HOL/Probability/Information.thy") produces 3 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Binary_Product_Measure.pair_measure" ### ("_nn_integral" ("_position" x) ### ("_applC" ("_position" ennreal) ### ("_applC" ("_position" Pxyz) ("_position" x))) ### ("\<^const>Binary_Product_Measure.pair_measure" ("_position" S) ### ("_position" T))) ### ("_position" P)) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_nn_integral" ("_position" x) ### ("_applC" ("_position" ennreal) ### ("_applC" ("_position" Pxyz) ("_position" x))) ### ("\<^const>Binary_Product_Measure.pair_measure" ("_position" S) ### ("\<^const>Binary_Product_Measure.pair_measure" ("_position" T) ### ("_position" P)))) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Binary_Product_Measure.pair_measure" ### ("_nn_integral" ("_position" x) ### ("_applC" ("_position" ennreal) ### ("_applC" ("_position" Pxyz) ("_position" x))) ### ("_position" S)) ### ("\<^const>Binary_Product_Measure.pair_measure" ("_position" T) ### ("_position" P))) ### ("\<^const>Groups.zero_class.zero"))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Rule already declared as introduction (intro) ### (\<And>x. x \<in> space ?M \<Longrightarrow> ?P x) \<Longrightarrow> ### almost_everywhere ?M ?P ### Ignoring duplicate rewrite rule: ### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T) ### Rule already declared as introduction (intro) ### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> ### open (\<Union>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk> ### \<Longrightarrow> open (\<Inter>?S) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk> ### \<Longrightarrow> open (\<Inter>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; closed ?T\<rbrakk> ### \<Longrightarrow> closed (?S \<union> ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; closed ?T\<rbrakk> ### \<Longrightarrow> closed (?S \<inter> ?T) ### Rule already declared as introduction (intro) ### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow> ### closed (\<Inter>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter>?K) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk> ### \<Longrightarrow> closed (\<Union>?S) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk> ### \<Longrightarrow> closed (\<Union>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T) ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \<Longrightarrow> open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \<Longrightarrow> closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Rule already declared as introduction (intro) ### (\<And>i. continuous_on UNIV (\<lambda>x. ?f x i)) \<Longrightarrow> ### continuous_on UNIV ?f ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T) ### Rule already declared as introduction (intro) ### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> ### open (\<Union>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk> ### \<Longrightarrow> open (\<Inter>?S) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk> ### \<Longrightarrow> open (\<Inter>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; closed ?T\<rbrakk> ### \<Longrightarrow> closed (?S \<union> ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; closed ?T\<rbrakk> ### \<Longrightarrow> closed (?S \<inter> ?T) ### Rule already declared as introduction (intro) ### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow> ### closed (\<Inter>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter>?K) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk> ### \<Longrightarrow> closed (\<Union>?S) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk> ### \<Longrightarrow> closed (\<Union>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T) ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \<Longrightarrow> open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \<Longrightarrow> closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Rule already declared as introduction (intro) ### (\<And>i. continuous_on UNIV (\<lambda>x. ?f x i)) \<Longrightarrow> ### continuous_on UNIV ?f ### Ambiguous input (line 1358 of "~~/src/HOL/Probability/Information.thy") produces 3 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Binary_Product_Measure.pair_measure" ### ("_nn_integral" ("_position" x) ### ("_applC" ("_position" ennreal) ### ("_applC" ("_position" Pxyz) ("_position" x))) ### ("\<^const>Binary_Product_Measure.pair_measure" ("_position" S) ### ("_position" T))) ### ("_position" P)) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_nn_integral" ("_position" x) ### ("_applC" ("_position" ennreal) ### ("_applC" ("_position" Pxyz) ("_position" x))) ### ("\<^const>Binary_Product_Measure.pair_measure" ("_position" S) ### ("\<^const>Binary_Product_Measure.pair_measure" ("_position" T) ### ("_position" P)))) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Binary_Product_Measure.pair_measure" ### ("_nn_integral" ("_position" x) ### ("_applC" ("_position" ennreal) ### ("_applC" ("_position" Pxyz) ("_position" x))) ### ("_position" S)) ### ("\<^const>Binary_Product_Measure.pair_measure" ("_position" T) ### ("_position" P))) ### ("\<^const>Groups.zero_class.zero"))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ignoring duplicate rewrite rule: ### (\<And>x. ### x \<in> space ?M1 \<Longrightarrow> 0 \<le> ?f1 x) \<Longrightarrow> ### 0 \<le> integral\<^sup>L ?M1 ?f1 \<equiv> True ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T) ### Rule already declared as introduction (intro) ### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> ### open (\<Union>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk> ### \<Longrightarrow> open (\<Inter>?S) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk> ### \<Longrightarrow> open (\<Inter>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; closed ?T\<rbrakk> ### \<Longrightarrow> closed (?S \<union> ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; closed ?T\<rbrakk> ### \<Longrightarrow> closed (?S \<inter> ?T) ### Rule already declared as introduction (intro) ### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow> ### closed (\<Inter>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter>?K) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk> ### \<Longrightarrow> closed (\<Union>?S) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk> ### \<Longrightarrow> closed (\<Union>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T) ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \<Longrightarrow> open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \<Longrightarrow> closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Rule already declared as introduction (intro) ### (\<And>i. continuous_on UNIV (\<lambda>x. ?f x i)) \<Longrightarrow> ### continuous_on UNIV ?f ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T) ### Rule already declared as introduction (intro) ### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> ### open (\<Union>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk> ### \<Longrightarrow> open (\<Inter>?S) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk> ### \<Longrightarrow> open (\<Inter>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; closed ?T\<rbrakk> ### \<Longrightarrow> closed (?S \<union> ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; closed ?T\<rbrakk> ### \<Longrightarrow> closed (?S \<inter> ?T) ### Rule already declared as introduction (intro) ### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow> ### closed (\<Inter>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter>?K) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk> ### \<Longrightarrow> closed (\<Union>?S) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk> ### \<Longrightarrow> closed (\<Union>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T) ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \<Longrightarrow> open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \<Longrightarrow> closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Rule already declared as introduction (intro) ### (\<And>i. continuous_on UNIV (\<lambda>x. ?f x i)) \<Longrightarrow> ### continuous_on UNIV ?f ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T) ### Rule already declared as introduction (intro) ### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> ### open (\<Union>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk> ### \<Longrightarrow> open (\<Inter>?S) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk> ### \<Longrightarrow> open (\<Inter>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; closed ?T\<rbrakk> ### \<Longrightarrow> closed (?S \<union> ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; closed ?T\<rbrakk> ### \<Longrightarrow> closed (?S \<inter> ?T) ### Rule already declared as introduction (intro) ### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow> ### closed (\<Inter>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter>?K) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk> ### \<Longrightarrow> closed (\<Union>?S) ### Rule already declared as introduction (intro) ### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk> ### \<Longrightarrow> closed (\<Union>x\<in>?A. ?B x) ### Rule already declared as introduction (intro) ### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T) ### Rule already declared as introduction (intro) ### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \<Longrightarrow> open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \<Longrightarrow> closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Rule already declared as introduction (intro) ### (\<And>i. continuous_on UNIV (\<lambda>x. ?f x i)) \<Longrightarrow> ### continuous_on UNIV ?f ### Rule already declared as introduction (intro) ### ((\<lambda>x. x) \<longlongrightarrow> ?a) (at ?a within ?s) ### Rule already declared as introduction (intro) ### ((\<lambda>x. ?k) \<longlongrightarrow> ?k) ?F ### Rule already declared as introduction (intro) ### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow> ### ((\<lambda>x. ereal (?f x)) \<longlongrightarrow> ereal ?x) ?F ### Rule already declared as introduction (intro) ### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow> ### ((\<lambda>x. - ?f x) \<longlongrightarrow> - ?x) ?F ### Rule already declared as introduction (intro) ### \<lbrakk>\<bar>?c\<bar> \<noteq> \<infinity>; ### (?f \<longlongrightarrow> ?x) ?F\<rbrakk> ### \<Longrightarrow> ((\<lambda>x. ?c * ?f x) \<longlongrightarrow> ?c * ?x) ?F ### Rule already declared as introduction (intro) ### \<lbrakk>?x \<noteq> 0; (?f \<longlongrightarrow> ?x) ?F\<rbrakk> ### \<Longrightarrow> ((\<lambda>x. ?c * ?f x) \<longlongrightarrow> ?c * ?x) ?F ### Rule already declared as introduction (intro) ### \<lbrakk>?y \<noteq> - \<infinity>; ?x \<noteq> - \<infinity>; ### (?f \<longlongrightarrow> ?x) ?F\<rbrakk> ### \<Longrightarrow> ((\<lambda>x. ?f x + ?y) \<longlongrightarrow> ?x + ?y) ?F ### Rule already declared as introduction (intro) ### \<lbrakk>\<bar>?y\<bar> \<noteq> \<infinity>; ### (?f \<longlongrightarrow> ?x) ?F\<rbrakk> ### \<Longrightarrow> ((\<lambda>x. ?f x + ?y) \<longlongrightarrow> ?x + ?y) ?F ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### of_real (?x1 * ?y1) \<equiv> of_real ?x1 * of_real ?y1 ### Ignoring duplicate rewrite rule: ### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True ### Rule already declared as introduction (intro) ### ((\<lambda>x. x) \<longlongrightarrow> ?a) (at ?a within ?s) ### Rule already declared as introduction (intro) ### ((\<lambda>x. ?k) \<longlongrightarrow> ?k) ?F ### Rule already declared as introduction (intro) ### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow> ### ((\<lambda>x. ereal (?f x)) \<longlongrightarrow> ereal ?x) ?F ### Rule already declared as introduction (intro) ### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow> ### ((\<lambda>x. - ?f x) \<longlongrightarrow> - ?x) ?F ### Rule already declared as introduction (intro) ### \<lbrakk>\<bar>?c\<bar> \<noteq> \<infinity>; ### (?f \<longlongrightarrow> ?x) ?F\<rbrakk> ### \<Longrightarrow> ((\<lambda>x. ?c * ?f x) \<longlongrightarrow> ?c * ?x) ?F ### Rule already declared as introduction (intro) ### \<lbrakk>?x \<noteq> 0; (?f \<longlongrightarrow> ?x) ?F\<rbrakk> ### \<Longrightarrow> ((\<lambda>x. ?c * ?f x) \<longlongrightarrow> ?c * ?x) ?F ### Rule already declared as introduction (intro) ### \<lbrakk>?y \<noteq> - \<infinity>; ?x \<noteq> - \<infinity>; ### (?f \<longlongrightarrow> ?x) ?F\<rbrakk> ### \<Longrightarrow> ((\<lambda>x. ?f x + ?y) \<longlongrightarrow> ?x + ?y) ?F ### Rule already declared as introduction (intro) ### \<lbrakk>\<bar>?y\<bar> \<noteq> \<infinity>; ### (?f \<longlongrightarrow> ?x) ?F\<rbrakk> ### \<Longrightarrow> ((\<lambda>x. ?f x + ?y) \<longlongrightarrow> ?x + ?y) ?F ### Ignoring duplicate rewrite rule: ### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True ### Rule already declared as introduction (intro) ### (\<And>x. x \<in> space ?M \<Longrightarrow> ?P x) \<Longrightarrow> ### almost_everywhere ?M ?P ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Rule already declared as introduction (intro) ### \<lbrakk>?A ` ?X ### \<subseteq> sigma_sets (space M) ### (\<Union>i\<in>{j..}. sigma_sets (space M) {F i}); ### ?X \<noteq> {}\<rbrakk> ### \<Longrightarrow> (\<Inter>i\<in>?X. ?A i) ### \<in> sigma_sets (space M) ### (\<Union>i\<in>{j..}. sigma_sets (space M) {F i}) ### Rule already declared as introduction (intro) ### ?A ` ?X ### \<subseteq> sigma_sets (space M) ### (\<Union>i\<in>{j..}. ### sigma_sets (space M) {F i}) \<Longrightarrow> ### (\<Union>x\<in>?X. ?A x) ### \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i}) ### Rule already declared as introduction (intro) ### ?a \<in> ?A \<Longrightarrow> ?a \<in> sigma_sets ?sp ?A ### Rule already declared as introduction (intro) ### \<lbrakk>?P ?x; ?x \<in> ?A\<rbrakk> ### \<Longrightarrow> \<exists>x\<in>?A. ?P x ### Rule already declared as introduction (intro) ### ?a \<in> ?A \<Longrightarrow> ?a \<in> sigma_sets ?sp ?A ### Rule already declared as introduction (intro) ### \<lbrakk>?b = ?f ?x; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?b \<in> ?f ` ?A ### Rule already declared as introduction (intro) ### \<lbrakk>?A \<in> sets ?M; emeasure ?M ?A < \<infinity>\<rbrakk> ### \<Longrightarrow> integrable ?M (indicator ?A) ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Rule already declared as introduction (intro) ### \<lbrakk>?b = ?f ?x; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?b \<in> ?f ` ?A ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> pmf ?p1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ambiguous input (line 1939 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("\<^const>local.entropy_Pow" ("_position" X)) ### ("\<^const>Groups.plus_class.plus" ### ("\<^const>local.entropy_Pow" ### ("\<^const>Fun.comp" ("_position" f) ("_position" X))) ### ("\<^const>local.entropy_Pow" ### ("\<^const>HOL.disj" ("_position" X) ### ("\<^const>Fun.comp" ("_position" f) ("_position" X))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("\<^const>local.entropy_Pow" ("_position" X)) ### ("\<^const>Groups.plus_class.plus" ### ("\<^const>local.entropy_Pow" ### ("\<^const>Fun.comp" ("_position" f) ("_position" X))) ### ("\<^const>local.conditional_entropy_Pow" ("_position" X) ### ("\<^const>Fun.comp" ("_position" f) ("_position" X)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### inverse ?a1 \<equiv> (1::?'a1) / ?a1 ### Ignoring duplicate rewrite rule: ### inverse ?a1 ^ ?n1 \<equiv> inverse (?a1 ^ ?n1) ### Ignoring duplicate rewrite rule: ### ((1::?'a1) / ?a1) ^ ?n1 \<equiv> (1::?'a1) / ?a1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### (?a1 / ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 / ?b1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True ### Ignoring duplicate rewrite rule: ### frontier {..?a1} \<equiv> {?a1} ### Ambiguous input (line 1868 of "~~/src/HOL/Probability/Information.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.mutual_information_Pow" ("_position" X) ### ("_position" Z)) ### ("\<^const>Groups.minus_class.minus" ### ("\<^const>local.entropy_Pow" ("_position" X)) ### ("\<^const>local.entropy_Pow" ### ("\<^const>HOL.disj" ("_position" X) ("_position" Z)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>local.mutual_information_Pow" ("_position" X) ### ("_position" Z)) ### ("\<^const>Groups.minus_class.minus" ### ("\<^const>local.entropy_Pow" ("_position" X)) ### ("\<^const>local.conditional_entropy_Pow" ("_position" X) ### ("_position" Z))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input.
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev