author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 12036 | 49f6c49454c2 |
child 17291 | 94f6113fe9ed |
permissions | -rw-r--r-- |
1479 | 1 |
(* Title: HOLCF/ex/hoare.thy |
244 | 2 |
ID: $Id$ |
1479 | 3 |
Author: Franz Regensburger |
244 | 4 |
|
12036 | 5 |
Theory for an example by C.A.R. Hoare |
244 | 6 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
7 |
p x = if b1 x |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
8 |
then p (g x) |
244 | 9 |
else x fi |
10 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
11 |
q x = if b1 x orelse b2 x |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
12 |
then q (g x) |
244 | 13 |
else x fi |
14 |
||
15 |
Prove: for all b1 b2 g . |
|
16 |
q o p = q |
|
17 |
||
18 |
In order to get a nice notation we fix the functions b1,b2 and g in the |
|
19 |
signature of this example |
|
20 |
||
21 |
*) |
|
22 |
||
2380
90280b3a538b
Dummy change to document the change in revision 1.5:
sandnerr
parents:
2379
diff
changeset
|
23 |
Hoare = HOLCF + |
244 | 24 |
|
25 |
consts |
|
1479 | 26 |
b1:: "'a -> tr" |
27 |
b2:: "'a -> tr" |
|
28 |
g:: "'a -> 'a" |
|
29 |
p :: "'a -> 'a" |
|
30 |
q :: "'a -> 'a" |
|
244 | 31 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
32 |
defs |
244 | 33 |
|
10835 | 34 |
p_def "p == fix$(LAM f. LAM x. |
35 |
If b1$x then f$(g$x) else x fi)" |
|
244 | 36 |
|
10835 | 37 |
q_def "q == fix$(LAM f. LAM x. |
38 |
If b1$x orelse b2$x then f$(g$x) else x fi)" |
|
244 | 39 |
|
40 |
end |
|
41 |