src/CCL/ex/Flag.thy
author clasohm
Wed, 21 Jun 1995 15:01:07 +0200
changeset 1149 5750eba8820d
parent 290 37d580c16af5
child 1474 3f7d67927fe2
permissions -rw-r--r--
removed \...\ inside strings
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	CCL/ex/flag.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Martin Coen, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Dutch national flag program - except that the point of Dijkstra's example was to use 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
arrays and this uses lists.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
Flag = List + 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
consts
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  Colour             :: "i set"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  red, white, blue   :: "i"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  ccase              :: "[i,i,i,i]=>i"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  flag               :: "i"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  Colour_def  "Colour == Unit + Unit + Unit"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
  red_def        "red == inl(one)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  white_def    "white == inr(inl(one))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  blue_def     "blue == inr(inr(one))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  ccase_def   "ccase(c,r,w,b) == when(c,%x.r,%wb.when(wb,%x.w,%x.b))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
1149
5750eba8820d removed \...\ inside strings
clasohm
parents: 290
diff changeset
    29
  flag_def    "flag == lam l.letrec 
5750eba8820d removed \...\ inside strings
clasohm
parents: 290
diff changeset
    30
      flagx l be lcase(l,<[],<[],[]>>, 
5750eba8820d removed \...\ inside strings
clasohm
parents: 290
diff changeset
    31
                       %h t. split(flagx(t),%lr p.split(p,%lw lb. 
5750eba8820d removed \...\ inside strings
clasohm
parents: 290
diff changeset
    32
                            ccase(h, <red$lr,<lw,lb>>, 
5750eba8820d removed \...\ inside strings
clasohm
parents: 290
diff changeset
    33
                                     <lr,<white$lw,lb>>, 
5750eba8820d removed \...\ inside strings
clasohm
parents: 290
diff changeset
    34
                                     <lr,<lw,blue$lb>>)))) 
5750eba8820d removed \...\ inside strings
clasohm
parents: 290
diff changeset
    35
      in flagx(l)"    
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
  Flag_def
1149
5750eba8820d removed \...\ inside strings
clasohm
parents: 290
diff changeset
    38
     "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour). 
5750eba8820d removed \...\ inside strings
clasohm
parents: 290
diff changeset
    39
                    x = <lr,<lw,lb>> --> 
5750eba8820d removed \...\ inside strings
clasohm
parents: 290
diff changeset
    40
                  (ALL c:Colour.(c mem lr = true --> c=red) & 
5750eba8820d removed \...\ inside strings
clasohm
parents: 290
diff changeset
    41
                                (c mem lw = true --> c=white) & 
5750eba8820d removed \...\ inside strings
clasohm
parents: 290
diff changeset
    42
                                (c mem lb = true --> c=blue)) & 
5750eba8820d removed \...\ inside strings
clasohm
parents: 290
diff changeset
    43
                  Perm(l,lr @ lw @ lb)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48