--- a/src/CCL/ex/flag.thy Sat Apr 05 16:00:00 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-(* 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
-
-
-