author  blanchet 
Wed, 21 Aug 2013 09:25:40 +0200  
changeset 53123  00d922eba913 
parent 53122  bc87b7af4767 
child 53134  4f8e156d2f19 
permissions  rwrr 
53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52844
diff
changeset

1 
(* Title: HOL/BNF/Examples/Misc_Datatype.thy 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

2 
Author: Dmitriy Traytel, TU Muenchen 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

3 
Author: Andrei Popescu, TU Muenchen 
51744  4 
Author: Jasmin Blanchette, TU Muenchen 
5 
Copyright 2012, 2013 

48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

6 

53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52844
diff
changeset

7 
Miscellaneous datatype definitions. 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

8 
*) 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

9 

53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52844
diff
changeset

10 
header {* Miscellaneous Datatype Definitions *} 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

11 

53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52844
diff
changeset

12 
theory Misc_Datatype 
49509
163914705f8d
renamed toplevel theory from "Codatatype" to "BNF"
blanchet
parents:
49463
diff
changeset

13 
imports "../BNF" 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

14 
begin 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

15 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

16 
datatype_new simple = X1  X2  X3  X4 
49157  17 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

18 
datatype_new simple' = X1' unit  X2' unit  X3' unit  X4' unit 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

19 

52323  20 
datatype_new simple'' = X1'' nat int  X2'' 
21 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

22 
datatype_new 'a mylist = MyNil  MyCons 'a "'a mylist" 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

23 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

24 
datatype_new ('b, 'c, 'd, 'e) some_passive = 
49157  25 
SP1 "('b, 'c, 'd, 'e) some_passive"  SP2 'b  SP3 'c  SP4 'd  SP5 'e 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

26 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

27 
datatype_new hfset = HFset "hfset fset" 
49601  28 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

29 
datatype_new lambda = 
49157  30 
Var string  
31 
App lambda lambda  

32 
Abs string lambda  

33 
Let "(string \<times> lambda) fset" lambda 

48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

34 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

35 
datatype_new 'a par_lambda = 
49157  36 
PVar 'a  
37 
PApp "'a par_lambda" "'a par_lambda"  

38 
PAbs 'a "'a par_lambda"  

39 
PLet "('a \<times> 'a par_lambda) fset" "'a par_lambda" 

48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

40 

7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

41 
(* 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

42 
('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

43 
('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

44 
*) 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

45 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

46 
datatype_new 'a I1 = I11 'a "'a I1"  I12 'a "'a I2" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

47 
and 'a I2 = I21  I22 "'a I1" "'a I2" 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

48 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

49 
datatype_new 'a tree = TEmpty  TNode 'a "'a forest" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

50 
and 'a forest = FNil  FCons "'a tree" "'a forest" 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

51 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

52 
datatype_new 'a tree' = TEmpty'  TNode' "'a branch" "'a branch" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

53 
and 'a branch = Branch 'a "'a tree'" 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

54 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

55 
datatype_new ('a, 'b) exp = Term "('a, 'b) trm"  Sum "('a, 'b) trm" "('a, 'b) exp" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

56 
and ('a, 'b) trm = Factor "('a, 'b) factor"  Prod "('a, 'b) factor" "('a, 'b) trm" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

57 
and ('a, 'b) factor = C 'a  V 'b  Paren "('a, 'b) exp" 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

58 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

59 
datatype_new ('a, 'b, 'c) some_killing = 
49157  60 
SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" 
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

61 
and ('a, 'b, 'c) in_here = 
49157  62 
IH1 'b 'a  IH2 'c 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

63 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

64 
datatype_new 'b nofail1 = NF11 "'b nofail1" 'b  NF12 'b 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

65 
datatype_new 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

66 
datatype_new 'b nofail3 = NF3 'b "('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

67 
datatype_new 'b nofail4 = NF4 "('b nofail4 \<times> ('b nofail4 \<times> 'b \<times> 'b nofail4 \<times> 'b) fset) list" 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

68 

7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

69 
(* 
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

70 
datatype_new 'b fail = F "'b fail" 'b "'b fail" "'b list" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

71 
datatype_new 'b fail = F "'b fail" 'b "'b fail" 'b 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

72 
datatype_new 'b fail = F1 "'b fail" 'b  F2 "'b fail" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

73 
datatype_new 'b fail = F "'b fail" 'b 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

74 
*) 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

75 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

76 
datatype_new l1 = L1 "l2 list" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

77 
and l2 = L21 "l1 fset"  L22 l2 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

78 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

79 
datatype_new kk1 = KK1 kk2 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

80 
and kk2 = KK2 kk3 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

81 
and kk3 = KK3 "kk1 list" 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

82 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

83 
datatype_new t1 = T11 t3  T12 t2 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

84 
and t2 = T2 t1 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

85 
and t3 = T3 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

86 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

87 
datatype_new t1' = T11' t2'  T12' t3' 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

88 
and t2' = T2' t1' 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

89 
and t3' = T3' 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

90 

7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

91 
(* 
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

92 
datatype_new fail1 = F1 fail2 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

93 
and fail2 = F2 fail3 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

94 
and fail3 = F3 fail1 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

95 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

96 
datatype_new fail1 = F1 "fail2 list" fail2 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

97 
and fail2 = F2 "fail2 fset" fail3 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

98 
and fail3 = F3 fail1 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

99 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

100 
datatype_new fail1 = F1 "fail2 list" fail2 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

101 
and fail2 = F2 "fail1 fset" fail1 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

102 
*) 
49157  103 

49162  104 
(* SLOW 
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

105 
datatype_new ('a, 'c) D1 = A1 "('a, 'c) D2"  B1 "'a list" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

106 
and ('a, 'c) D2 = A2 "('a, 'c) D3"  B2 "'c list" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

107 
and ('a, 'c) D3 = A3 "('a, 'c) D3"  B3 "('a, 'c) D4"  C3 "('a, 'c) D4" "('a, 'c) D5" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

108 
and ('a, 'c) D4 = A4 "('a, 'c) D5"  B4 "'a list list list" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

109 
and ('a, 'c) D5 = A5 "('a, 'c) D6" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

110 
and ('a, 'c) D6 = A6 "('a, 'c) D7" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

111 
and ('a, 'c) D7 = A7 "('a, 'c) D8" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

112 
and ('a, 'c) D8 = A8 "('a, 'c) D1 list" 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

113 

7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

114 
(*time comparison*) 
49157  115 
datatype ('a, 'c) D1' = A1' "('a, 'c) D2'"  B1' "'a list" 
116 
and ('a, 'c) D2' = A2' "('a, 'c) D3'"  B2' "'c list" 

117 
and ('a, 'c) D3' = A3' "('a, 'c) D3'"  B3' "('a, 'c) D4'"  C3' "('a, 'c) D4'" "('a, 'c) D5'" 

118 
and ('a, 'c) D4' = A4' "('a, 'c) D5'"  B4' "'a list list list" 

119 
and ('a, 'c) D5' = A5' "('a, 'c) D6'" 

120 
and ('a, 'c) D6' = A6' "('a, 'c) D7'" 

121 
and ('a, 'c) D7' = A7' "('a, 'c) D8'" 

122 
and ('a, 'c) D8' = A8' "('a, 'c) D1' list" 

49162  123 
*) 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

124 

7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

125 
(* fail: 
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

126 
datatype_new tt1 = TT11 tt2 tt3  TT12 tt2 tt4 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

127 
and tt2 = TT2 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

128 
and tt3 = TT3 tt4 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

129 
and tt4 = TT4 tt1 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

130 
*) 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

131 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

132 
datatype_new k1 = K11 k2 k3  K12 k2 k4 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

133 
and k2 = K2 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

134 
and k3 = K3 k4 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

135 
and k4 = K4 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

136 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

137 
datatype_new tt1 = TT11 tt3 tt2  TT12 tt2 tt4 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

138 
and tt2 = TT2 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

139 
and tt3 = TT3 tt1 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

140 
and tt4 = TT4 
49157  141 

49162  142 
(* SLOW 
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

143 
datatype_new s1 = S11 s2 s3 s4  S12 s3  S13 s2 s6  S14 s4 s2  S15 s2 s2 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

144 
and s2 = S21 s7 s5  S22 s5 s4 s6 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

145 
and s3 = S31 s1 s7 s2  S32 s3 s3  S33 s4 s5 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

146 
and s4 = S4 s5 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

147 
and s5 = S5 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

148 
and s6 = S61 s6  S62 s1 s2  S63 s6 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

149 
and s7 = S71 s8  S72 s5 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

150 
and s8 = S8 nat 
49162  151 
*) 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

152 

52813  153 
datatype_new 'a deadbar = DeadBar "'a \<Rightarrow> 'a" 
154 
datatype_new 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option" 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

155 
datatype_new ('a, 'b) bar = Bar "'b \<Rightarrow> 'a" 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

156 
datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a" 
53123  157 
datatype_new 'a deadfoo = DeadFoo "'a \<Rightarrow> 'a + 'a" 
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49166
diff
changeset

158 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

159 
datatype_new 'a dead_foo = A 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

160 
datatype_new ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo" 
49186
4b5fa9d5e330
handle type constructors not known to be a BNF using the DEADID BNF
traytel
parents:
49185
diff
changeset

161 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

162 
datatype_new d1 = D 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

163 
datatype_new d1' = is_D: D 
51744  164 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

165 
datatype_new d2 = D nat 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

166 
datatype_new d2' = is_D: D nat 
51744  167 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

168 
datatype_new d3 = D  E 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

169 
datatype_new d3' = D  is_E: E 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

170 
datatype_new d3'' = is_D: D  E 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

171 
datatype_new d3''' = is_D: D  is_E: E 
51744  172 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

173 
datatype_new d4 = D nat  E 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

174 
datatype_new d4' = D nat  is_E: E 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

175 
datatype_new d4'' = is_D: D nat  E 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

176 
datatype_new d4''' = is_D: D nat  is_E: E 
51744  177 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

178 
datatype_new d5 = D nat  E int 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

179 
datatype_new d5' = D nat  is_E: E int 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

180 
datatype_new d5'' = is_D: D nat  E int 
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51744
diff
changeset

181 
datatype_new d5''' = is_D: D nat  is_E: E int 
51744  182 

48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

183 
end 