author  wenzelm 
Wed, 26 Jul 2006 00:44:44 +0200  
changeset 20207  4c57e850e8d5 
parent 16417  9bc16273c2d4 
child 33695  bec342db1bf4 
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 

16417  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  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  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  27 
 App__ 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3" 
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  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  36 
 Conveyed__ 'a "('a, 'b, 'c) TY2" 
37 
 Possesses__ 'a "('a, 'b, 'c) TY2" 

38 
 Received__ 'a "('a, 'b, 'c) TY2" 

39 
 Recognizes__ 'a "('a, 'b, 'c) TY2" 

40 
 NeverMalFromSelf__ 'a 'b "('a, 'b, 'c) TY2" 

41 
 Sends__ 'a "('a, 'b, 'c) TY2" 'b 

42 
 SharedSecret__ 'a "('a, 'b, 'c) TY2" 'b 

43 
 Believes__ 'a "('a, 'b, 'c) TY3" 

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 