[Hol-info] Weakest precondition of While as the least fixpoint

[Piotr T. <pio...@gm...>]

Dear all,

I am still experimenting with programming language semantics using
both HOL Light and HOL4. My question is not specific to any of these
two implementations, but I could not find any better place to ask,
sorry.

I am following the HOL Light tutorial, where the weakest preconditions
`wp`are derived from inductively defined big-step operational
semantics. I want to prove that `wp (While e c) q` is the least fixed
point:

wp (While e c) q = lfp (λw. e AND wp c w OR NOT e AND q)

but I can only prove that the right hand side implies the left hand
side. Can you point me to a proof, ideally in HOL, of the above
equivalence?

The code from HOL Light tutorial is similar to the what Harrison
describes in "Formalizing Dijkstra." He says "We could in fact prove
that `Do gcs` is the least fixpoint," but do not give a proof (page
12). Dijkstra and Scholten give a proof in their "Predicate calculus
and program semantics," but they heavily depend on their own notation
and I found their reasoning difficult to mechanize in HOL. On the
other extreme, HOL mechanizations of the refinement calculus simply
define the weakest precondition for While as the least fixpoint.

-- 
Piotr Trojanek