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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
244
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
     1
Proves about loops and tail-recursive functions
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
     2
===============================================
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
     3
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
     4
Problem A
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
     5
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
     6
P = while B1       do S od
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
     7
Q = while B1 or B2 do S od
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
     8
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
     9
Prove P;Q = Q    (provided B1, B2 have no side effects)
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    10
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    11
------
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    12
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    13
Looking at the denotational semantics of while, we get
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    14
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    15
Problem B
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    16
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    17
[|B1|]:State->Bool
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    18
[|B2|]:State->Bool
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    19
[|S |]:State->State
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    20
f     :State->State
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    21
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    22
p = fix LAM f.LAM x. if [| B1 |] x                  then f([| S |] x) else x fi
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    23
q = fix LAM f.LAM x. if [| B1 |] x orelse [|b2 |] x then f([| S |] x) else x fi
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    24
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    25
Prove q o p = q          rsp.       ALL x.q(p(x))=q(x)
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    26
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    27
Remark: 1. Bool is the three-valued domain {UU,FF,TT} since tests B1 and B2 may
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    28
           not terminate.
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    29
        2. orelse is the sequential or like in ML
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    30
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    31
----------
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    32
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    33
If we abstract over the structure of stores we get
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    34
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    35
Problem C
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    36
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    37
b1:'a -> Bool
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    38
b2:'a -> Bool
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    39
g :'a ->'a
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    40
h :'a ->'a
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    41
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    42
p = fix LAM h.LAM x. if b1(x)              then h(g(x)) else x fi
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    43
q = fix LAM h.LAM x. if b1(x) orelse b2(x) then h(g(x)) else x fi
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    44
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    45
where g is an abstraction of [| S |]
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    46
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    47
Prove q o p = q 
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    48
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    49
Remark: there are no restrictions wrt. definedness or strictness for any of 
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    50
        the involved functions.
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    51
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    52
----------
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    53
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    54
In a functional programming language the problem reads as follows:
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    55
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    56
p(x) = if b1(x) 
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    57
         then p(g(x))
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    58
         else x fi
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    59
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    60
q(x) = if b1(x) orelse b2(x) 
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    61
         then q(g(x))
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    62
         else x fi
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    63
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    64
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    65
Prove:  q o p = q
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    66
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    67
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    68
-------------
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    69
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    70
In you like to test the problem in ML (bad guy) you have to introduce 
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    71
formal parameters for b1,b2 and g.
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    72
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    73
fun p b1 g x = if b1(x) 
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    74
         then p b1 g (g(x))
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    75
         else x;
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    76
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    77
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    78
fun q b1 b2 g x = if b1(x) orelse b2(x) 
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    79
         then q b1 b2 g (g(x))
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    80
         else x;
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    81
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    82
Prove: for all b1 b2 g . 
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    83
            (q b1 b2 g) o (p b1 g) = (q b1 b2 g)
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    84
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    85
===========
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    86
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    87
It took 4 person-days to formulate and prove the problem C in the
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    88
Isabelle logic HOLCF. The formalisation was done by conservative extension and
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    89
all proof principles where derived from pure HOLCF.
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    90
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    91
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    92
    
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    93
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    94
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    95
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    96
929fc2c63bd0 HOLCF examples
nipkow
parents:
diff changeset
    97