author  haftmann 
Mon, 05 Jul 2010 15:12:20 +0200  
changeset 37715  44b27ea94a16 
parent 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 
33695  2 

3 
A couple from Steve Brackin's work. 

7013
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 

16417  6 
theory Brackin imports Main begin 
7013
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 
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

9 
X12  X13  X14  X15  X16  X17  X18  X19  X20  X21  
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

10 
X22  X23  X24  X25  X26  X27  X28  X29  X30  X31  
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

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

12 

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

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

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

15 
NoF__ 
7373  16 
 Fk__ 'a "('a, 'b, 'c) TY2" 
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

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

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

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

20 
 Td__ bool 
7373  21 
 Tf__ "('a, 'b, 'c) TY1" 
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

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

23 
 Tp__ bool 
7373  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" 

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

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

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

28 
NoS__ 
7373  29 
 Fresh__ "('a, 'b, 'c) TY2" 
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

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

31 
 PrivateKey__ 'a 'b 'c 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

32 
 PublicKey__ 'a 'b 'c 
7373  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" 

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

42 

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

43 
end 