[isabelle] Pending sort hypotheses



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} 


Does anyone have any idea on how to solve this issue ?

Thanks in advance,
Henri.









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