summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/HOLCF/ex/hoare.txt

author | wenzelm |

Sat, 07 Apr 2012 16:41:59 +0200 | |

changeset 47389 | e8552cba702d |

parent 40774 | 0437dbc127b3 |

permissions | -rw-r--r-- |

explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
tuned;

Proves about loops and tail-recursive functions =============================================== Problem A P = while B1 do S od Q = while B1 or B2 do S od Prove P;Q = Q (provided B1, B2 have no side effects) ------ Looking at the denotational semantics of while, we get Problem B [|B1|]:State->Bool [|B2|]:State->Bool [|S |]:State->State f :State->State p = fix LAM f.LAM x. if [| B1 |] x then f([| S |] x) else x fi q = fix LAM f.LAM x. if [| B1 |] x orelse [|b2 |] x then f([| S |] x) else x fi Prove q o p = q rsp. ALL x.q(p(x))=q(x) Remark: 1. Bool is the three-valued domain {UU,FF,TT} since tests B1 and B2 may not terminate. 2. orelse is the sequential or like in ML ---------- If we abstract over the structure of stores we get Problem C b1:'a -> Bool b2:'a -> Bool g :'a ->'a h :'a ->'a p = fix LAM h.LAM x. if b1(x) then h(g(x)) else x fi q = fix LAM h.LAM x. if b1(x) orelse b2(x) then h(g(x)) else x fi where g is an abstraction of [| S |] Prove q o p = q Remark: there are no restrictions wrt. definedness or strictness for any of the involved functions. ---------- In a functional programming language the problem reads as follows: p(x) = if b1(x) then p(g(x)) else x fi q(x) = if b1(x) orelse b2(x) then q(g(x)) else x fi Prove: q o p = q ------------- In you like to test the problem in ML (bad guy) you have to introduce formal parameters for b1,b2 and g. fun p b1 g x = if b1(x) then p b1 g (g(x)) else x; fun q b1 b2 g x = if b1(x) orelse b2(x) then q b1 b2 g (g(x)) else x; Prove: for all b1 b2 g . (q b1 b2 g) o (p b1 g) = (q b1 b2 g) =========== It took 4 person-days to formulate and prove the problem C in the Isabelle logic HOLCF. The formalisation was done by conservative extension and all proof principles where derived from pure HOLCF.