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