Admin/Benchmarks/HOL-datatype/Brackin.thy
author wenzelm
Wed, 26 Jul 2006 00:44:44 +0200
changeset 20207 4c57e850e8d5
parent 16417 9bc16273c2d4
child 33695 bec342db1bf4
permissions -rw-r--r--
added Pure/subgoal.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
     1
(*  Title:      Admin/Benchmarks/HOL-datatype/Brackin.thy
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
     2
    ID:         $Id$
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
     3
*)
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
     4
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 7373
diff changeset
     5
theory Brackin imports Main begin
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
     6
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
     7
(* ------------------------------------------------------------------------- *)
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
     8
(* A couple from Steve Brackin's work.                                       *)
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
     9
(* ------------------------------------------------------------------------- *)
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    10
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    11
datatype   T = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    12
                X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    13
                X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    14
                X32 | X33 | X34
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    15
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    16
datatype  
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    17
  ('a, 'b, 'c) TY1 =
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    18
      NoF__
7373
776d888472aa better timing information;
wenzelm
parents: 7013
diff changeset
    19
    | Fk__ 'a "('a, 'b, 'c) TY2"
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    20
and
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    21
  ('a, 'b, 'c) TY2 =
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    22
      Ta__ bool
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    23
    | Td__ bool
7373
776d888472aa better timing information;
wenzelm
parents: 7013
diff changeset
    24
    | Tf__ "('a, 'b, 'c) TY1"
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    25
    | Tk__ bool
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    26
    | Tp__ bool
7373
776d888472aa better timing information;
wenzelm
parents: 7013
diff changeset
    27
    | App__ 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
776d888472aa better timing information;
wenzelm
parents: 7013
diff changeset
    28
    | Pair__ "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    29
and
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    30
  ('a, 'b, 'c) TY3 =
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    31
      NoS__
7373
776d888472aa better timing information;
wenzelm
parents: 7013
diff changeset
    32
    | Fresh__ "('a, 'b, 'c) TY2"
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    33
    | Trustworthy__ 'a
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    34
    | PrivateKey__ 'a 'b 'c
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    35
    | PublicKey__ 'a 'b 'c
7373
776d888472aa better timing information;
wenzelm
parents: 7013
diff changeset
    36
    | Conveyed__ 'a "('a, 'b, 'c) TY2"
776d888472aa better timing information;
wenzelm
parents: 7013
diff changeset
    37
    | Possesses__ 'a "('a, 'b, 'c) TY2"
776d888472aa better timing information;
wenzelm
parents: 7013
diff changeset
    38
    | Received__ 'a "('a, 'b, 'c) TY2"
776d888472aa better timing information;
wenzelm
parents: 7013
diff changeset
    39
    | Recognizes__ 'a "('a, 'b, 'c) TY2"
776d888472aa better timing information;
wenzelm
parents: 7013
diff changeset
    40
    | NeverMalFromSelf__ 'a 'b "('a, 'b, 'c) TY2"
776d888472aa better timing information;
wenzelm
parents: 7013
diff changeset
    41
    | Sends__ 'a "('a, 'b, 'c) TY2" 'b
776d888472aa better timing information;
wenzelm
parents: 7013
diff changeset
    42
    | SharedSecret__ 'a "('a, 'b, 'c) TY2" 'b
776d888472aa better timing information;
wenzelm
parents: 7013
diff changeset
    43
    | Believes__ 'a "('a, 'b, 'c) TY3"
776d888472aa better timing information;
wenzelm
parents: 7013
diff changeset
    44
    | And__ "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
7013
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    45
8a7fb425e04a Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff changeset
    46
end