|
1474
|
1 |
(* Title: CCL/ex/flag.thy
|
|
0
|
2 |
ID: $Id$
|
|
1474
|
3 |
Author: Martin Coen, Cambridge University Computer Laboratory
|
|
0
|
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 |
|
|
1149
|
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.
|
|
|
32 |
ccase(h, <red$lr,<lw,lb>>,
|
|
|
33 |
<lr,<white$lw,lb>>,
|
|
|
34 |
<lr,<lw,blue$lb>>))))
|
|
|
35 |
in flagx(l)"
|
|
0
|
36 |
|
|
|
37 |
Flag_def
|
|
1149
|
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)"
|
|
0
|
44 |
|
|
|
45 |
end
|
|
|
46 |
|
|
|
47 |
|
|
|
48 |
|