author | wenzelm |
Sat, 03 Nov 2001 18:41:28 +0100 | |
changeset 12036 | 49f6c49454c2 |
parent 10835 | f4745d77e620 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
1479 | 1 |
(* Title: HOLCF/ex/hoare.thy |
244 | 2 |
ID: $Id$ |
1479 | 3 |
Author: Franz Regensburger |
12036 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
244 | 5 |
|
12036 | 6 |
Theory for an example by C.A.R. Hoare |
244 | 7 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
8 |
p x = if b1 x |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
9 |
then p (g x) |
244 | 10 |
else x fi |
11 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
12 |
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
|
13 |
then q (g x) |
244 | 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 |
||
2380
90280b3a538b
Dummy change to document the change in revision 1.5:
sandnerr
parents:
2379
diff
changeset
|
24 |
Hoare = HOLCF + |
244 | 25 |
|
26 |
consts |
|
1479 | 27 |
b1:: "'a -> tr" |
28 |
b2:: "'a -> tr" |
|
29 |
g:: "'a -> 'a" |
|
30 |
p :: "'a -> 'a" |
|
31 |
q :: "'a -> 'a" |
|
244 | 32 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
33 |
defs |
244 | 34 |
|
10835 | 35 |
p_def "p == fix$(LAM f. LAM x. |
36 |
If b1$x then f$(g$x) else x fi)" |
|
244 | 37 |
|
10835 | 38 |
q_def "q == fix$(LAM f. LAM x. |
39 |
If b1$x orelse b2$x then f$(g$x) else x fi)" |
|
244 | 40 |
|
41 |
end |
|
42 |