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