src/CCL/ex/flag.thy
 author clasohm Tue, 22 Mar 1994 12:43:51 +0100 changeset 290 37d580c16af5 parent 0 a5a9c433f639 permissions -rw-r--r--
changed "." to "\$" and added parentheses to eliminate ambiguity
```
(*  Title: 	CCL/ex/flag.thy
ID:         \$Id\$
Author: 	Martin Coen, Cambridge University Computer Laboratory
Copyright   1993  University of Cambridge

Dutch national flag program - except that the point of Dijkstra's example was to use
arrays and this uses lists.

*)

Flag = List +

consts

Colour             :: "i set"
red, white, blue   :: "i"
ccase              :: "[i,i,i,i]=>i"
flag               :: "i"

rules

Colour_def  "Colour == Unit + Unit + Unit"
red_def        "red == inl(one)"
white_def    "white == inr(inl(one))"
blue_def     "blue == inr(inr(one))"

ccase_def   "ccase(c,r,w,b) == when(c,%x.r,%wb.when(wb,%x.w,%x.b))"

flag_def    "flag == lam l.letrec \
\      flagx l be lcase(l,<[],<[],[]>>, \
\                       %h t. split(flagx(t),%lr p.split(p,%lw lb. \
\                            ccase(h, <red\$lr,<lw,lb>>, \
\                                     <lr,<white\$lw,lb>>, \
\                                     <lr,<lw,blue\$lb>>)))) \
\      in flagx(l)"

Flag_def
"Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour). \
\                    x = <lr,<lw,lb>> --> \
\                  (ALL c:Colour.(c mem lr = true --> c=red) & \
\                                (c mem lw = true --> c=white) & \
\                                (c mem lb = true --> c=blue)) & \
\                  Perm(l,lr @ lw @ lb)"

end

```