src/CCL/ex/Flag.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CCL/ex/Flag.thy	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,48 @@
+(*  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
+
+
+