src/HOL/Datatype_Benchmark/Brackin.thy
author wenzelm
Thu May 24 17:25:53 2012 +0200 (2012-05-24)
changeset 47988 e4b69e10b990
parent 45860 93eda35a8377
child 51699 0539e75b4170
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Datatype_Benchmark/Brackin.thy
     2 
     3 A couple from Steve Brackin's work.
     4 *)
     5 
     6 theory Brackin imports Main begin
     7 
     8 datatype   T = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
     9                 X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
    10                 X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
    11                 X32 | X33 | X34
    12 
    13 datatype  
    14   ('a, 'b, 'c) TY1 =
    15       NoF__
    16     | Fk__ 'a "('a, 'b, 'c) TY2"
    17 and
    18   ('a, 'b, 'c) TY2 =
    19       Ta__ bool
    20     | Td__ bool
    21     | Tf__ "('a, 'b, 'c) TY1"
    22     | Tk__ bool
    23     | Tp__ bool
    24     | App__ 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
    25     | Pair__ "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
    26 and
    27   ('a, 'b, 'c) TY3 =
    28       NoS__
    29     | Fresh__ "('a, 'b, 'c) TY2"
    30     | Trustworthy__ 'a
    31     | PrivateKey__ 'a 'b 'c
    32     | PublicKey__ 'a 'b 'c
    33     | Conveyed__ 'a "('a, 'b, 'c) TY2"
    34     | Possesses__ 'a "('a, 'b, 'c) TY2"
    35     | Received__ 'a "('a, 'b, 'c) TY2"
    36     | Recognizes__ 'a "('a, 'b, 'c) TY2"
    37     | NeverMalFromSelf__ 'a 'b "('a, 'b, 'c) TY2"
    38     | Sends__ 'a "('a, 'b, 'c) TY2" 'b
    39     | SharedSecret__ 'a "('a, 'b, 'c) TY2" 'b
    40     | Believes__ 'a "('a, 'b, 'c) TY3"
    41     | And__ "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
    42 
    43 end