src/HOL/Datatype_Examples/Brackin.thy
author wenzelm
Sat Jul 18 22:58:50 2015 +0200 (2015-07-18)
changeset 60758 d8d85a8172b5
parent 58330 a016c42d136d
permissions -rw-r--r--
isabelle update_cartouches;
     1 (*  Title:      HOL/Datatype_Examples/Brackin.thy
     2 
     3 A couple of datatypes from Steve Brackin's work.
     4 *)
     5 
     6 theory Brackin imports Main begin
     7 
     8 datatype T =
     9     X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
    10     X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
    11     X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
    12     X32 | X33 | X34
    13 
    14 datatype ('a, 'b, 'c) TY1 =
    15       NoF
    16     | Fk 'a "('a, 'b, 'c) TY2"
    17 and ('a, 'b, 'c) TY2 =
    18       Ta bool
    19     | Td bool
    20     | Tf "('a, 'b, 'c) TY1"
    21     | Tk bool
    22     | Tp bool
    23     | App 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
    24     | Pair "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
    25 and ('a, 'b, 'c) TY3 =
    26       NoS
    27     | Fresh "('a, 'b, 'c) TY2"
    28     | Trustworthy 'a
    29     | PrivateKey 'a 'b 'c
    30     | PublicKey 'a 'b 'c
    31     | Conveyed 'a "('a, 'b, 'c) TY2"
    32     | Possesses 'a "('a, 'b, 'c) TY2"
    33     | Received 'a "('a, 'b, 'c) TY2"
    34     | Recognizes 'a "('a, 'b, 'c) TY2"
    35     | NeverMalFromSelf 'a 'b "('a, 'b, 'c) TY2"
    36     | Sends 'a "('a, 'b, 'c) TY2" 'b
    37     | SharedSecret 'a "('a, 'b, 'c) TY2" 'b
    38     | Believes 'a "('a, 'b, 'c) TY3"
    39     | And "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
    40 
    41 end