*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Pending sort hypotheses*From*: Henri DEBRAT <Henri.Debrat at loria.fr>*Date*: Tue, 3 Jul 2012 18:53:43 +0200*Cc*: Johannes Hölzl <hoelzl at in.tum.de>*In-reply-to*: <1341258546.2104.13.camel@vogelfrei>*References*: <C889C598-FE01-49FD-8D17-50FEA8F7B266@loria.fr> <1341258546.2104.13.camel@vogelfrei>

> 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 a lot, Johannes. The code you provide me with does work, thanks a lot. You are right, I had some axiomatic constraints on p so that it is in ] 0 ; 1[ I just forgot to say it. Yet, some great mystery lies here concerning sort_constraint and the exception it raises. In case it might be an interesting issue to solve, I copy here two piece of code. They look pretty similar, however, the first goes fine while the second raise the famous sort_constraint error. typedecl Proc arities Proc :: finite axiomatization bp::real where bpdef:"bp > 0 ∧ bp < 1" definition "bernoulli ≡ point_measure (UNIV :: bool set) (% True => ereal bp | False => 1 - ereal bp)" **** CODE WHICH FAILS AT THE LAST "QED" (sort_constraint error): interpretation rs:product_prob_space "(λi::nat × Proc. bernoulli)" "UNIV::(nat × Proc) set" where "SORT_CONSTRAINT('a::{finite,perfect_space,real_normed_vector} )" proof(unfold_locales, auto) have "UNIV = { True, False }" by auto thus "emeasure bernoulli (space bernoulli) = 1" using space_point_measure finite_UNIV by (blast dest:emeasure_point_measure_finite) next have "UNIV = { True, False }" by auto thus "emeasure bernoulli (space bernoulli) = ∞ ⟹ False" using finite_UNIV space_point_measure by (blast dest:emeasure_point_measure_finite) next have "UNIV = { True, False }" by auto moreover obtain A where "A = (λi::nat. if i = 0 then space bernoulli else {})" by auto hence "range A ⊆ sets bernoulli" and "(⋃x::nat. A x) = space bernoulli" by auto ultimately show "∃A. range A ⊆ sets bernoulli ∧ (⋃x::nat. A x) = space bernoulli ∧ (∀i. emeasure bernoulli (A i) ≠ ∞)" using finite_UNIV by (blast dest:emeasure_point_measure_finite) qed *** CODE WHICH ENDS FINE (thanks to Johannes) : interpretation rs:product_prob_space "(λi. bernoulli)" "UNIV::(nat × Proc) set" proof(unfold_locales, auto) from bpdef show "emeasure bernoulli (space bernoulli) = 1" by (auto simp: UNIV_bool one_ereal_def bernoulli_def space_point_measure emeasure_point_measure_finite split: bool.split) next from bpdef show "emeasure bernoulli (space bernoulli) = ∞ ⟹ False" by (auto simp: UNIV_bool one_ereal_def bernoulli_def space_point_measure emeasure_point_measure_finite split: bool.split) next obtain A where Adef:"A = (λi::nat. if i = 0 then space bernoulli else {})" by auto hence "range A ⊆ sets bernoulli" and "(⋃x::nat. A x) = space bernoulli" by auto moreover from Adef bpdef have "∀i. emeasure bernoulli (A i) ≠ ∞" by(auto simp: UNIV_bool one_ereal_def bernoulli_def space_point_measure emeasure_point_measure_finite split: bool.split) ultimately show "∃A. range A ⊆ sets bernoulli ∧ (⋃x::nat. A x) = space bernoulli ∧ (∀i. emeasure bernoulli (A i) ≠ ∞)" by auto qed I hope this might be useful. H.

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

**Re: [isabelle] Pending sort hypotheses***From:*Lars Noschinski

**References**:**Re: [isabelle] Pending sort hypotheses***From:*Johannes Hölzl

- Previous by Date: [isabelle] New AFP entry: Logical Relations for PCF
- Next by Date: Re: [isabelle] Pending sort hypotheses
- 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