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. \
|
|
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 |
|