[isabelle-dev] Sporadic build failure of HOL-Probability in 16a8991ab398
Manuel Eberl
eberlm at in.tum.de
Fri Apr 28 08:47:45 CEST 2017
Hallo,
I just had a strange build failure with HOL-Probability. I executed
manuel at 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
-------------- next part --------------
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
-------------- next part --------------
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.
More information about the isabelle-dev
mailing list