11 |
11 |
12 theory Misc_Datatype |
12 theory Misc_Datatype |
13 imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/FSet" |
13 imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/FSet" |
14 begin |
14 begin |
15 |
15 |
16 datatype_new (discs_sels) simple = X1 | X2 | X3 | X4 |
16 datatype (discs_sels) simple = X1 | X2 | X3 | X4 |
17 |
17 |
18 datatype_new (discs_sels) simple' = X1' unit | X2' unit | X3' unit | X4' unit |
18 datatype (discs_sels) simple' = X1' unit | X2' unit | X3' unit | X4' unit |
19 |
19 |
20 datatype_new (discs_sels) simple'' = X1'' nat int | X2'' |
20 datatype (discs_sels) simple'' = X1'' nat int | X2'' |
21 |
21 |
22 datatype_new (discs_sels) 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist") |
22 datatype (discs_sels) 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist") |
23 |
23 |
24 datatype_new (discs_sels) ('b, 'c :: ord, 'd, 'e) some_passive = |
24 datatype (discs_sels) ('b, 'c :: ord, 'd, 'e) some_passive = |
25 SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e |
25 SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e |
26 |
26 |
27 datatype_new (discs_sels) hfset = HFset "hfset fset" |
27 datatype (discs_sels) hfset = HFset "hfset fset" |
28 |
28 |
29 datatype_new (discs_sels) lambda = |
29 datatype (discs_sels) lambda = |
30 Var string | |
30 Var string | |
31 App lambda lambda | |
31 App lambda lambda | |
32 Abs string lambda | |
32 Abs string lambda | |
33 Let "(string \<times> lambda) fset" lambda |
33 Let "(string \<times> lambda) fset" lambda |
34 |
34 |
35 datatype_new (discs_sels) 'a par_lambda = |
35 datatype (discs_sels) 'a par_lambda = |
36 PVar 'a | |
36 PVar 'a | |
37 PApp "'a par_lambda" "'a par_lambda" | |
37 PApp "'a par_lambda" "'a par_lambda" | |
38 PAbs 'a "'a par_lambda" | |
38 PAbs 'a "'a par_lambda" | |
39 PLet "('a \<times> 'a par_lambda) fset" "'a par_lambda" |
39 PLet "('a \<times> 'a par_lambda) fset" "'a par_lambda" |
40 |
40 |
41 (* |
41 (* |
42 ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2 |
42 ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2 |
43 ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 |
43 ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 |
44 *) |
44 *) |
45 |
45 |
46 datatype_new (discs_sels) 'a I1 = I11 'a "'a I1" | I12 'a "'a I2" |
46 datatype (discs_sels) 'a I1 = I11 'a "'a I1" | I12 'a "'a I2" |
47 and 'a I2 = I21 | I22 "'a I1" "'a I2" |
47 and 'a I2 = I21 | I22 "'a I1" "'a I2" |
48 |
48 |
49 datatype_new (discs_sels) 'a tree = TEmpty | TNode 'a "'a forest" |
49 datatype (discs_sels) 'a tree = TEmpty | TNode 'a "'a forest" |
50 and 'a forest = FNil | FCons "'a tree" "'a forest" |
50 and 'a forest = FNil | FCons "'a tree" "'a forest" |
51 |
51 |
52 datatype_new (discs_sels) 'a tree' = TEmpty' | TNode' "'a branch" "'a branch" |
52 datatype (discs_sels) 'a tree' = TEmpty' | TNode' "'a branch" "'a branch" |
53 and 'a branch = Branch 'a "'a tree'" |
53 and 'a branch = Branch 'a "'a tree'" |
54 |
54 |
55 datatype_new (discs_sels) 'a bin_rose_tree = BRTree 'a "'a bin_rose_tree mylist" "'a bin_rose_tree mylist" |
55 datatype (discs_sels) 'a bin_rose_tree = BRTree 'a "'a bin_rose_tree mylist" "'a bin_rose_tree mylist" |
56 |
56 |
57 datatype_new (discs_sels) ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" |
57 datatype (discs_sels) ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" |
58 and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" |
58 and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" |
59 and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" |
59 and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" |
60 |
60 |
61 datatype_new (discs_sels) 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree" |
61 datatype (discs_sels) 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree" |
62 |
62 |
63 datatype_new (discs_sels) ('a, 'b, 'c) some_killing = |
63 datatype (discs_sels) ('a, 'b, 'c) some_killing = |
64 SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" |
64 SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" |
65 and ('a, 'b, 'c) in_here = |
65 and ('a, 'b, 'c) in_here = |
66 IH1 'b 'a | IH2 'c |
66 IH1 'b 'a | IH2 'c |
67 |
67 |
68 datatype_new (discs_sels) 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b |
68 datatype (discs_sels) 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b |
69 datatype_new (discs_sels) 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list" |
69 datatype (discs_sels) 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list" |
70 datatype_new (discs_sels) 'b nofail3 = NF3 'b "('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset" |
70 datatype (discs_sels) 'b nofail3 = NF3 'b "('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset" |
71 datatype_new (discs_sels) 'b nofail4 = NF4 "('b nofail4 \<times> ('b nofail4 \<times> 'b \<times> 'b nofail4 \<times> 'b) fset) list" |
71 datatype (discs_sels) 'b nofail4 = NF4 "('b nofail4 \<times> ('b nofail4 \<times> 'b \<times> 'b nofail4 \<times> 'b) fset) list" |
72 |
72 |
73 (* |
73 (* |
74 datatype_new (discs_sels) 'b fail = F "'b fail" 'b "'b fail" "'b list" |
74 datatype (discs_sels) 'b fail = F "'b fail" 'b "'b fail" "'b list" |
75 datatype_new (discs_sels) 'b fail = F "'b fail" 'b "'b fail" 'b |
75 datatype (discs_sels) 'b fail = F "'b fail" 'b "'b fail" 'b |
76 datatype_new (discs_sels) 'b fail = F1 "'b fail" 'b | F2 "'b fail" |
76 datatype (discs_sels) 'b fail = F1 "'b fail" 'b | F2 "'b fail" |
77 datatype_new (discs_sels) 'b fail = F "'b fail" 'b |
77 datatype (discs_sels) 'b fail = F "'b fail" 'b |
78 *) |
78 *) |
79 |
79 |
80 datatype_new (discs_sels) l1 = L1 "l2 list" |
80 datatype (discs_sels) l1 = L1 "l2 list" |
81 and l2 = L21 "l1 fset" | L22 l2 |
81 and l2 = L21 "l1 fset" | L22 l2 |
82 |
82 |
83 datatype_new (discs_sels) kk1 = KK1 kk2 |
83 datatype (discs_sels) kk1 = KK1 kk2 |
84 and kk2 = KK2 kk3 |
84 and kk2 = KK2 kk3 |
85 and kk3 = KK3 "kk1 list" |
85 and kk3 = KK3 "kk1 list" |
86 |
86 |
87 datatype_new (discs_sels) t1 = T11 t3 | T12 t2 |
87 datatype (discs_sels) t1 = T11 t3 | T12 t2 |
88 and t2 = T2 t1 |
88 and t2 = T2 t1 |
89 and t3 = T3 |
89 and t3 = T3 |
90 |
90 |
91 datatype_new (discs_sels) t1' = T11' t2' | T12' t3' |
91 datatype (discs_sels) t1' = T11' t2' | T12' t3' |
92 and t2' = T2' t1' |
92 and t2' = T2' t1' |
93 and t3' = T3' |
93 and t3' = T3' |
94 |
94 |
95 (* |
95 (* |
96 datatype_new (discs_sels) fail1 = F1 fail2 |
96 datatype (discs_sels) fail1 = F1 fail2 |
97 and fail2 = F2 fail3 |
97 and fail2 = F2 fail3 |
98 and fail3 = F3 fail1 |
98 and fail3 = F3 fail1 |
99 |
99 |
100 datatype_new (discs_sels) fail1 = F1 "fail2 list" fail2 |
100 datatype (discs_sels) fail1 = F1 "fail2 list" fail2 |
101 and fail2 = F2 "fail2 fset" fail3 |
101 and fail2 = F2 "fail2 fset" fail3 |
102 and fail3 = F3 fail1 |
102 and fail3 = F3 fail1 |
103 |
103 |
104 datatype_new (discs_sels) fail1 = F1 "fail2 list" fail2 |
104 datatype (discs_sels) fail1 = F1 "fail2 list" fail2 |
105 and fail2 = F2 "fail1 fset" fail1 |
105 and fail2 = F2 "fail1 fset" fail1 |
106 *) |
106 *) |
107 |
107 |
108 (* SLOW |
108 (* SLOW |
109 datatype_new (discs_sels) ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list" |
109 datatype (discs_sels) ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list" |
110 and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list" |
110 and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list" |
111 and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5" |
111 and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5" |
112 and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list" |
112 and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list" |
113 and ('a, 'c) D5 = A5 "('a, 'c) D6" |
113 and ('a, 'c) D5 = A5 "('a, 'c) D6" |
114 and ('a, 'c) D6 = A6 "('a, 'c) D7" |
114 and ('a, 'c) D6 = A6 "('a, 'c) D7" |
115 and ('a, 'c) D7 = A7 "('a, 'c) D8" |
115 and ('a, 'c) D7 = A7 "('a, 'c) D8" |
116 and ('a, 'c) D8 = A8 "('a, 'c) D1 list" |
116 and ('a, 'c) D8 = A8 "('a, 'c) D1 list" |
117 *) |
117 *) |
118 |
118 |
119 (* fail: |
119 (* fail: |
120 datatype_new (discs_sels) tt1 = TT11 tt2 tt3 | TT12 tt2 tt4 |
120 datatype (discs_sels) tt1 = TT11 tt2 tt3 | TT12 tt2 tt4 |
121 and tt2 = TT2 |
121 and tt2 = TT2 |
122 and tt3 = TT3 tt4 |
122 and tt3 = TT3 tt4 |
123 and tt4 = TT4 tt1 |
123 and tt4 = TT4 tt1 |
124 *) |
124 *) |
125 |
125 |
126 datatype_new (discs_sels) k1 = K11 k2 k3 | K12 k2 k4 |
126 datatype (discs_sels) k1 = K11 k2 k3 | K12 k2 k4 |
127 and k2 = K2 |
127 and k2 = K2 |
128 and k3 = K3 k4 |
128 and k3 = K3 k4 |
129 and k4 = K4 |
129 and k4 = K4 |
130 |
130 |
131 datatype_new (discs_sels) tt1 = TT11 tt3 tt2 | TT12 tt2 tt4 |
131 datatype (discs_sels) tt1 = TT11 tt3 tt2 | TT12 tt2 tt4 |
132 and tt2 = TT2 |
132 and tt2 = TT2 |
133 and tt3 = TT3 tt1 |
133 and tt3 = TT3 tt1 |
134 and tt4 = TT4 |
134 and tt4 = TT4 |
135 |
135 |
136 (* SLOW |
136 (* SLOW |
137 datatype_new (discs_sels) s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2 |
137 datatype (discs_sels) s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2 |
138 and s2 = S21 s7 s5 | S22 s5 s4 s6 |
138 and s2 = S21 s7 s5 | S22 s5 s4 s6 |
139 and s3 = S31 s1 s7 s2 | S32 s3 s3 | S33 s4 s5 |
139 and s3 = S31 s1 s7 s2 | S32 s3 s3 | S33 s4 s5 |
140 and s4 = S4 s5 |
140 and s4 = S4 s5 |
141 and s5 = S5 |
141 and s5 = S5 |
142 and s6 = S61 s6 | S62 s1 s2 | S63 s6 |
142 and s6 = S61 s6 | S62 s1 s2 | S63 s6 |
143 and s7 = S71 s8 | S72 s5 |
143 and s7 = S71 s8 | S72 s5 |
144 and s8 = S8 nat |
144 and s8 = S8 nat |
145 *) |
145 *) |
146 |
146 |
147 datatype_new (discs_sels) 'a deadbar = DeadBar "'a \<Rightarrow> 'a" |
147 datatype (discs_sels) 'a deadbar = DeadBar "'a \<Rightarrow> 'a" |
148 datatype_new (discs_sels) 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option" |
148 datatype (discs_sels) 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option" |
149 datatype_new (discs_sels) ('a, 'b) bar = Bar "'b \<Rightarrow> 'a" |
149 datatype (discs_sels) ('a, 'b) bar = Bar "'b \<Rightarrow> 'a" |
150 datatype_new (discs_sels) ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a" |
150 datatype (discs_sels) ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a" |
151 datatype_new (discs_sels) 'a deadfoo = DeadFoo "'a \<Rightarrow> 'a + 'a" |
151 datatype (discs_sels) 'a deadfoo = DeadFoo "'a \<Rightarrow> 'a + 'a" |
152 |
152 |
153 datatype_new (discs_sels) 'a dead_foo = A |
153 datatype (discs_sels) 'a dead_foo = A |
154 datatype_new (discs_sels) ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo" |
154 datatype (discs_sels) ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo" |
155 |
155 |
156 datatype_new (discs_sels) d1 = D |
156 datatype (discs_sels) d1 = D |
157 datatype_new (discs_sels) d1' = is_D: D |
157 datatype (discs_sels) d1' = is_D: D |
158 |
158 |
159 datatype_new (discs_sels) d2 = D nat |
159 datatype (discs_sels) d2 = D nat |
160 datatype_new (discs_sels) d2' = is_D: D nat |
160 datatype (discs_sels) d2' = is_D: D nat |
161 |
161 |
162 datatype_new (discs_sels) d3 = D | E |
162 datatype (discs_sels) d3 = D | E |
163 datatype_new (discs_sels) d3' = D | is_E: E |
163 datatype (discs_sels) d3' = D | is_E: E |
164 datatype_new (discs_sels) d3'' = is_D: D | E |
164 datatype (discs_sels) d3'' = is_D: D | E |
165 datatype_new (discs_sels) d3''' = is_D: D | is_E: E |
165 datatype (discs_sels) d3''' = is_D: D | is_E: E |
166 |
166 |
167 datatype_new (discs_sels) d4 = D nat | E |
167 datatype (discs_sels) d4 = D nat | E |
168 datatype_new (discs_sels) d4' = D nat | is_E: E |
168 datatype (discs_sels) d4' = D nat | is_E: E |
169 datatype_new (discs_sels) d4'' = is_D: D nat | E |
169 datatype (discs_sels) d4'' = is_D: D nat | E |
170 datatype_new (discs_sels) d4''' = is_D: D nat | is_E: E |
170 datatype (discs_sels) d4''' = is_D: D nat | is_E: E |
171 |
171 |
172 datatype_new (discs_sels) d5 = D nat | E int |
172 datatype (discs_sels) d5 = D nat | E int |
173 datatype_new (discs_sels) d5' = D nat | is_E: E int |
173 datatype (discs_sels) d5' = D nat | is_E: E int |
174 datatype_new (discs_sels) d5'' = is_D: D nat | E int |
174 datatype (discs_sels) d5'' = is_D: D nat | E int |
175 datatype_new (discs_sels) d5''' = is_D: D nat | is_E: E int |
175 datatype (discs_sels) d5''' = is_D: D nat | is_E: E int |
176 |
176 |
177 instance simple :: countable |
177 instance simple :: countable |
178 by countable_datatype |
178 by countable_datatype |
179 |
179 |
180 instance simple'' :: countable |
180 instance simple'' :: countable |