|
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. \ |
|
32 \ ccase(h, <red.lr,<lw,lb>>, \ |
|
33 \ <lr,<white.lw,lb>>, \ |
|
34 \ <lr,<lw,blue.lb>>)))) \ |
|
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 |