equal
deleted
inserted
replaced
|
1 (* Title: HOLCF/ex/hoare.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Theory for an example by C.A.R. Hoare |
|
7 |
|
8 p x = if b1(x) |
|
9 then p(g(x)) |
|
10 else x fi |
|
11 |
|
12 q x = if b1(x) orelse b2(x) |
|
13 then q (g(x)) |
|
14 else x fi |
|
15 |
|
16 Prove: for all b1 b2 g . |
|
17 q o p = q |
|
18 |
|
19 In order to get a nice notation we fix the functions b1,b2 and g in the |
|
20 signature of this example |
|
21 |
|
22 *) |
|
23 |
|
24 Hoare = Tr2 + |
|
25 |
|
26 consts |
|
27 b1:: "'a -> tr" |
|
28 b2:: "'a -> tr" |
|
29 g:: "'a -> 'a" |
|
30 p :: "'a -> 'a" |
|
31 q :: "'a -> 'a" |
|
32 |
|
33 rules |
|
34 |
|
35 p_def "p == fix[LAM f. LAM x.\ |
|
36 \ If b1[x] then f[g[x]] else x fi]" |
|
37 |
|
38 q_def "q == fix[LAM f. LAM x.\ |
|
39 \ If b1[x] orelse b2[x] then f[g[x]] else x fi]" |
|
40 |
|
41 |
|
42 end |
|
43 |