author | nipkow |
Thu, 26 Nov 1998 12:18:08 +0100 | |
changeset 5974 | 6acf3ff0f486 |
parent 2380 | 90280b3a538b |
child 10835 | f4745d77e620 |
permissions | -rw-r--r-- |
1479 | 1 |
(* Title: HOLCF/ex/hoare.thy |
244 | 2 |
ID: $Id$ |
1479 | 3 |
Author: Franz Regensburger |
4 |
Copyright 1993 Technische Universitaet Muenchen |
|
244 | 5 |
|
6 |
Theory for an example by C.A.R. Hoare |
|
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 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
35 |
p_def "p == fix`(LAM f. LAM x. |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
36 |
If b1`x then f`(g`x) else x fi)" |
244 | 37 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
38 |
q_def "q == fix`(LAM f. LAM x. |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
39 |
If b1`x orelse b2`x then f`(g`x) else x fi)" |
244 | 40 |
|
41 |
end |
|
42 |