Twp

[hei411]

This is the branch for including a total wp for the ub logic.

• Add typeclass + notation for twp
• Implement lemmas for total wp type class
• Define total wp instance for ub logic
• Prove a weak adequacy rule (Terminates up to 1 - ep)
• Prove least upper bound property of reals and hence its corollaries
• Implement a ub_lift for total wp.
• prove total_ub_lift lemmas
• Prove stronger adequacy rule (terminate in Phi predicate up to 1 - ep). Assigned to Heili atm
• Prove basic primitive laws for twp
• Prove planner rule for twp
• Implement example of rejection sampler
• Prove termination and probabilities of rejection sampler using adequacy