*To*: Henri DEBRAT <Henri.Debrat at loria.fr>*Subject*: Re: [isabelle] Pending sort hypotheses*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Mon, 02 Jul 2012 21:49:06 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <C889C598-FE01-49FD-8D17-50FEA8F7B266@loria.fr>*Organization*: TU München*References*: <C889C598-FE01-49FD-8D17-50FEA8F7B266@loria.fr>

Am Donnerstag, den 28.06.2012, 12:40 +0200 schrieb Henri DEBRAT: > Hi all, > > I am trying to define a randomized algorithm in order to prove it is correct. On this purpose, I defined following objects: > > > "bernoulli p ≡ point_measure (UNIV :: bool set) (% True => p | False => 1 - p)" > > > interpretation rs:product_prob_space "(λi. bernoulli p)" "UNIV::(nat × Proc) set" for p > proof (unfold_locales, auto) > have "(UNIV :: bool set) = { True, False }" by auto > thus "emeasure (bernoulli p) (space (bernoulli p)) = ∞ ⟹ False" > using emeasure_point_measure_finite finite_UNIV > proof (unfold bernoulli_def, blast) qed > ... > > > > Proof goes fine (just ends with "no subgoals") but at "qed" I obtain the following error: > > Pending sort hypotheses: > {finite,perfect_space,real_normed_vector} Huh, where does this come from? There should be no additional sort constraint. > > Does anyone have any idea on how to solve this issue ? The interpretation as you try it will unfortunately not work. You need to clamp the probability p between 0 and 1: definition clamp :: "real ⇒ real" where "clamp p = min 0 (max 1 p)" definition "bernoulli p ≡ point_measure (UNIV :: bool set) (% True => ereal (clamp p) | False => 1 - ereal (clamp p))" Important note: If p is a real the following proofs are much simpler! The next is: For product_prob_space you just need to show that "bernoulli p" is a probabilty space. This does work directly with unfold_locales, but with prob_spaceI which is a default rule. This is a little ugly but saves a couple of sublocales in the probability theory. interpretation rs: product_prob_space "(λi. bernoulli p)" "UNIV::(nat × nat) set" for p :: real proof - have "emeasure (bernoulli p) (space (bernoulli p)) = (∑i∈UNIV. case i of True => clamp p | False => 1 - clamp p)" by (simp add: bernoulli_def space_point_measure emeasure_point_measure_finite clamp_def max_def min_def split: bool.split) also have "… = 1" by (simp add: UNIV_bool one_ereal_def) finally interpret prob_space "bernoulli p" by rule -- {* Here prob_spaceI is applied *} show "product_prob_space (λi. bernoulli p)" .. -- {* This is also unfold_locales, but this time the interpret from above is used *} qed Maybe even better is: interpretation bernoulli: "bernoulli p" for p :: real proof - have "emeasure (bernoulli p) (space (bernoulli p)) = (∑i∈UNIV. case i of True => clamp p | False => 1 - clamp p)" by (simp add: bernoulli_def space_point_measure emeasure_point_measure_finite clamp_def max_def min_def split: bool.split) also have "… = 1" by (simp add: UNIV_bool one_ereal_def) finally show "prob_space (bernoulli p)" by rule -- {* Here prob_spaceI is applied *} qed interpretation rs: product_prob_space "(λi. bernoulli p)" "UNIV::(nat × nat) set" for p :: real .. > Thanks in advance, > Henri.

**Follow-Ups**:**Re: [isabelle] Pending sort hypotheses***From:*Henri DEBRAT

- Previous by Date: Re: [isabelle] Pending sort hypotheses
- Next by Date: [isabelle] ON Isabelle/SMT counter_example
- Previous by Thread: Re: [isabelle] Pending sort hypotheses
- Next by Thread: Re: [isabelle] Pending sort hypotheses
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list