author | oheimb |
Thu, 27 Jun 1996 12:53:08 +0200 | |
changeset 1832 | 79dd1433867c |
parent 1479 | 21eb5e156d91 |
child 2379 | 2e55b396e24c |
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 |
||
24 |
Hoare = Tr2 + |
|
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 |