Re: [isabelle] Pending sort hypotheses



> 
> 
>> 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.
> 



Oh, I forgot to say that if i start the first proof with  "proof (unfold_locales, auto simp:sort_constraint_def)", as suggested by Makarius, the exception still raises :


exception TERM raised (line 137 of "more_thm.ML"):
dest_equals
SORT_CONSTRAINT
(?'a∷{finite,perfect_space,real_normed_vector}) 



H.









This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.