author  berghofe 
Fri, 16 Jul 1999 12:02:06 +0200  
changeset 7013  8a7fb425e04a 
child 7373  776d888472aa 
permissions  rwrr 
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

1 
(* Title: Admin/Benchmarks/HOLdatatype/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 

8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

5 
Brackin = Main + 
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__ 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

19 
 Fk__ 'a (('a, 'b, 'c) TY2) 
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 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

24 
 Tf__ (('a, 'b, 'c) TY1) 
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 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

27 
 App__ 'a (('a, 'b, 'c) TY1) (('a, 'b, 'c) TY2) (('a, 'b, 'c) TY3) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

28 
 Pair__ (('a, 'b, 'c) TY2) (('a, 'b, 'c) TY2) 
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__ 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

32 
 Fresh__ (('a, 'b, 'c) TY2) 
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 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

36 
 Conveyed__ 'a (('a, 'b, 'c) TY2) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

37 
 Possesses__ 'a (('a, 'b, 'c) TY2) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

38 
 Received__ 'a (('a, 'b, 'c) TY2) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

39 
 Recognizes__ 'a (('a, 'b, 'c) TY2) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

40 
 NeverMalFromSelf__ 'a 'b (('a, 'b, 'c) TY2) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

41 
 Sends__ 'a (('a, 'b, 'c) TY2) 'b 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

42 
 SharedSecret__ 'a (('a, 'b, 'c) TY2) 'b 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

43 
 Believes__ 'a (('a, 'b, 'c) TY3) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

44 
 And__ (('a, 'b, 'c) TY3) (('a, 'b, 'c) TY3) 
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 