This AFP entry defines a probabilistic while operator based on
sub-probability mass functions and formalises zero-one laws and variant
rules for probabilistic loop termination. As applications, we
implement probabilistic algorithms for the Bernoulli, geometric and
arbitrary uniform distributions that only use fair coin flips, and
prove them correct and terminating with probability 1.BSD License
Added a proof that probabilistic conditioning can be implemented by repeated sampling.