author | wenzelm |
Fri, 10 Oct 1997 17:10:12 +0200 | |
changeset 3837 | d7f033c74b38 |
parent 290 | 37d580c16af5 |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: CCL/ex/flag.thy |
2 |
ID: $Id$ |
|
3 |
Author: Martin Coen, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
Dutch national flag program - except that the point of Dijkstra's example was to use |
|
7 |
arrays and this uses lists. |
|
8 |
||
9 |
*) |
|
10 |
||
11 |
Flag = List + |
|
12 |
||
13 |
consts |
|
14 |
||
15 |
Colour :: "i set" |
|
16 |
red, white, blue :: "i" |
|
17 |
ccase :: "[i,i,i,i]=>i" |
|
18 |
flag :: "i" |
|
19 |
||
20 |
rules |
|
21 |
||
22 |
Colour_def "Colour == Unit + Unit + Unit" |
|
23 |
red_def "red == inl(one)" |
|
24 |
white_def "white == inr(inl(one))" |
|
25 |
blue_def "blue == inr(inr(one))" |
|
26 |
||
27 |
ccase_def "ccase(c,r,w,b) == when(c,%x.r,%wb.when(wb,%x.w,%x.b))" |
|
28 |
||
29 |
flag_def "flag == lam l.letrec \ |
|
30 |
\ flagx l be lcase(l,<[],<[],[]>>, \ |
|
31 |
\ %h t. split(flagx(t),%lr p.split(p,%lw lb. \ |
|
290
37d580c16af5
changed "." to "$" and added parentheses to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
32 |
\ ccase(h, <red$lr,<lw,lb>>, \ |
37d580c16af5
changed "." to "$" and added parentheses to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
33 |
\ <lr,<white$lw,lb>>, \ |
37d580c16af5
changed "." to "$" and added parentheses to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
34 |
\ <lr,<lw,blue$lb>>)))) \ |
0 | 35 |
\ in flagx(l)" |
36 |
||
37 |
Flag_def |
|
38 |
"Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour). \ |
|
39 |
\ x = <lr,<lw,lb>> --> \ |
|
40 |
\ (ALL c:Colour.(c mem lr = true --> c=red) & \ |
|
41 |
\ (c mem lw = true --> c=white) & \ |
|
42 |
\ (c mem lb = true --> c=blue)) & \ |
|
43 |
\ Perm(l,lr @ lw @ lb)" |
|
44 |
||
45 |
end |
|
46 |
||
47 |
||
48 |