src/CCL/ex/flag.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 290 37d580c16af5
permissions -rw-r--r--
tidying
     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