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 in advance,
> Henri.











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