author  nipkow 
Tue, 05 Nov 2019 14:57:41 +0100  
changeset 71033  c1b63124245c 
parent 66453  cc19f7ca2ed6 
permissions  rwrr 
62286
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build a" by default;
wenzelm
parents:
61260
diff
changeset

1 
(* Title: Benchmarks/Datatype_Benchmark/Misc_N2M.thy 
58385  2 
Author: Dmitriy Traytel, TU Muenchen 
3 
Copyright 2014 

4 

58396  5 
Miscellaneous tests for the nestedtomutual reduction. 
58385  6 
*) 
7 

58889  8 
section \<open>Miscellaneous Tests for the NestedtoMutual Reduction\<close> 
58385  9 

10 
theory Misc_N2M 

66453
cc19f7ca2ed6
sessionqualified theory imports: isabelle imports U i d '~~/src/Benchmarks' a;
wenzelm
parents:
62688
diff
changeset

11 
imports "HOLLibrary.BNF_Axiomatization" 
58385  12 
begin 
13 

61260  14 
declare [[typedef_overloaded]] 
15 

16 

58385  17 
locale misc 
18 
begin 

19 

20 
datatype 'a li = Ni  Co 'a "'a li" 

21 
datatype 'a tr = Tr "'a \<Rightarrow> 'a tr li" 

22 

23 
primrec (nonexhaustive) 

24 
f_tl :: "'a \<Rightarrow> 'a tr li \<Rightarrow> nat" and 

25 
f_t :: "'a \<Rightarrow> 'a tr \<Rightarrow> nat" 

26 
where 

27 
"f_tl _ Ni = 0"  

28 
"f_t a (Tr ts) = 1 + f_tl a (ts a)" 

29 

30 
datatype ('a, 'b) l = N  C 'a 'b "('a, 'b) l" 

31 
datatype ('a, 'b) t = T "(('a, 'b) t, 'a) l" "(('a, 'b) t, 'b) l" 

32 

33 
primrec (nonexhaustive) 

34 
f_tl2 :: "(('a, 'a) t, 'a) l \<Rightarrow> nat" and 

35 
f_t2 :: "('a, 'a) t \<Rightarrow> nat" 

36 
where 

37 
"f_tl2 N = 0"  

38 
"f_t2 (T ts us) = f_tl2 ts + f_tl2 us" 

39 

40 
primrec (nonexhaustive) 

41 
g_tla :: "(('a, 'b) t, 'a) l \<Rightarrow> nat" and 

42 
g_tlb :: "(('a, 'b) t, 'b) l \<Rightarrow> nat" and 

43 
g_t :: "('a, 'b) t \<Rightarrow> nat" 

44 
where 

45 
"g_tla N = 0"  

46 
"g_tlb N = 1"  

47 
"g_t (T ts us) = g_tla ts + g_tlb us" 

48 

49 

50 
datatype 

51 
'a l1 = N1  C1 'a "'a l1" 

52 

53 
datatype 

54 
('a, 'b) t1 = T1 'a 'b "('a, 'b) t1 l1" "(nat \<times> ('a, 'b) t1) l1" and 

55 
('a, 'b) t2 = T2 "('a, 'b) t1" 

56 

57 
primrec 

58 
h1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and 

59 
h1_natl1 :: "(nat \<times> (nat, 'a) t1) l1 \<Rightarrow> nat" and 

60 
h1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat" 

61 
where 

62 
"h1_tl1 N1 = 0"  

63 
"h1_tl1 (C1 t ts) = h1_t1 t + h1_tl1 ts"  

64 
"h1_natl1 N1 = Suc 0"  

65 
"h1_natl1 (C1 n ts) = fst n + h1_natl1 ts"  

66 
"h1_t1 (T1 n _ ts _) = n + h1_tl1 ts" 

67 

68 
end 

69 

70 

71 
bnf_axiomatization ('a, 'b) M0 [wits: "('a, 'b) M0"] 

72 
bnf_axiomatization ('a, 'b) N0 [wits: "('a, 'b) N0"] 

73 
bnf_axiomatization ('a, 'b) K0 [wits: "('a, 'b) K0"] 

74 
bnf_axiomatization ('a, 'b) L0 [wits: "('a, 'b) L0"] 

75 
bnf_axiomatization ('a, 'b, 'c) G0 [wits: "('a, 'b, 'c) G0"] 

76 

77 
locale (*co*)mplicated 

78 
begin 

79 

80 
datatype 'a M = CM "('a, 'a M) M0" 

81 
datatype 'a N = CN "('a N, 'a) N0" 

82 
datatype ('a, 'b) K = CK "('a, ('a, 'b) L) K0" 

83 
and ('a, 'b) L = CL "('b, ('a, 'b) K) L0" 

84 
datatype 'a G = CG "('a, ('a G, 'a G N) K, ('a G M, 'a G) L) G0" 

85 

86 
primrec 

87 
fG :: "'a G \<Rightarrow> 'a G" 

88 
and fK :: "('a G, 'a G N) K \<Rightarrow> ('a G, 'a G N) K" 

89 
and fL :: "('a G, 'a G N) L \<Rightarrow> ('a G, 'a G N) L" 

90 
and fM :: "'a G M \<Rightarrow> 'a G M" where 

91 
"fG (CG x) = CG (map_G0 id fK (map_L fM fG) x)" 

92 
 "fK (CK y) = CK (map_K0 fG fL y)" 

93 
 "fL (CL z) = CL (map_L0 (map_N fG) fK z)" 

94 
 "fM (CM w) = CM (map_M0 fG fM w)" 

95 
thm fG_def fK_def fL_def fM_def fG.simps fK.simps fL.simps fM.simps 

96 

97 
end 

98 

99 
locale complicated 

100 
begin 

101 

102 
codatatype 'a M = CM "('a, 'a M) M0" 

103 
codatatype 'a N = CN "('a N, 'a) N0" 

104 
codatatype ('a, 'b) K = CK "('a, ('a, 'b) L) K0" 

62688  105 
and ('a, 'b) L = CL "('b, ('a, 'b) K) L0" 
58385  106 
codatatype 'a G = CG "('a, ('a G, 'a G N) K, ('a G M, 'a G) L) G0" 
107 

108 
primcorec 

109 
fG :: "'a G \<Rightarrow> 'a G" 

110 
and fK :: "('a G, 'a G N) K \<Rightarrow> ('a G, 'a G N) K" 

111 
and fL :: "('a G, 'a G N) L \<Rightarrow> ('a G, 'a G N) L" 

112 
and fM :: "'a G M \<Rightarrow> 'a G M" where 

113 
"fG x = CG (map_G0 id fK (map_L fM fG) (un_CG x))" 

114 
 "fK y = CK (map_K0 fG fL (un_CK y))" 

115 
 "fL z = CL (map_L0 (map_N fG) fK (un_CL z))" 

116 
 "fM w = CM (map_M0 fG fM (un_CM w))" 

117 
thm fG_def fK_def fL_def fM_def fG.simps fK.simps fL.simps fM.simps 

118 

119 
end 

120 

121 
datatype ('a, 'b) F1 = F1 'a 'b 

122 
datatype F2 = F2 "((unit, nat) F1, F2) F1"  F2' 

123 
datatype 'a kk1 = K1 'a  K2 "'a kk2" and 'a kk2 = K3 "'a kk1" 

124 
datatype 'a ll1 = L1 'a  L2 "'a ll2 kk2" and 'a ll2 = L3 "'a ll1" 

125 

126 
datatype_compat F1 

127 
datatype_compat F2 

128 
datatype_compat kk1 kk2 

129 
datatype_compat ll1 ll2 

130 

131 

58396  132 
subsection \<open>Deep Nesting\<close> 
58385  133 

134 
datatype 'a tree = Empty  Node 'a "'a tree list" 

135 
datatype_compat tree 

136 

137 
datatype 'a ttree = TEmpty  TNode 'a "'a ttree list tree" 

138 
datatype_compat ttree 

139 

140 
datatype 'a tttree = TEmpty  TNode 'a "'a tttree list ttree list tree" 

141 
datatype_compat tttree 

142 
(* 

143 
datatype 'a ttttree = TEmpty  TNode 'a "'a ttttree list tttree list ttree list tree" 

144 
datatype_compat ttttree 

145 
*) 

146 

147 
datatype 'a F = F1 'a  F2 "'a F" 

148 
datatype 'a G = G1 'a  G2 "'a G F" 

149 
datatype H = H1  H2 "H G" 

150 

151 
datatype_compat F 

152 
datatype_compat G 

153 
datatype_compat H 

154 

58396  155 

156 
subsection \<open>Primrec cache\<close> 

58385  157 

158 
datatype 'a l = N  C 'a "'a l" 

159 
datatype ('a, 'b) t = T 'a 'b "('a, 'b) t l" 

160 

161 
context linorder 

162 
begin 

163 

164 
primrec 

165 
f1_tl :: "(nat, 'a) t l \<Rightarrow> nat" and 

166 
f1_t :: "(nat, 'a) t \<Rightarrow> nat" 

167 
where 

168 
"f1_tl N = 0"  

169 
"f1_tl (C t ts) = f1_t t + f1_tl ts"  

170 
"f1_t (T n _ ts) = n + f1_tl ts" 

171 

62688  172 
(* should hit cache *) 
58385  173 
primrec 
174 
f2_t :: "(nat, 'b) t \<Rightarrow> nat" and 

175 
f2_tl :: "(nat, 'b) t l \<Rightarrow> nat" 

176 
where 

177 
"f2_tl N = 0"  

178 
"f2_tl (C t ts) = f2_t t + f2_tl ts"  

179 
"f2_t (T n _ ts) = n + f2_tl ts" 

180 

181 
end 

182 

62688  183 
(* should hit cache *) 
58385  184 
primrec 
185 
g1_t :: "('a, int) t \<Rightarrow> nat" and 

186 
g1_tl :: "('a, int) t l \<Rightarrow> nat" 

187 
where 

188 
"g1_t (T _ _ ts) = g1_tl ts"  

189 
"g1_tl N = 0"  

190 
"g1_tl (C _ ts) = g1_tl ts" 

191 

62688  192 
(* should hit cache *) 
58385  193 
primrec 
194 
g2_t :: "(int, int) t \<Rightarrow> nat" and 

195 
g2_tl :: "(int, int) t l \<Rightarrow> nat" 

196 
where 

197 
"g2_t (T _ _ ts) = g2_tl ts"  

198 
"g2_tl N = 0"  

199 
"g2_tl (C _ ts) = g2_tl ts" 

200 

201 

202 
datatype 

203 
'a l1 = N1  C1 'a "'a l2" and 

204 
'a l2 = N2  C2 'a "'a l1" 

205 

206 
primrec 

207 
sum_l1 :: "'a::{zero,plus} l1 \<Rightarrow> 'a" and 

208 
sum_l2 :: "'a::{zero,plus} l2 \<Rightarrow> 'a" 

209 
where 

210 
"sum_l1 N1 = 0"  

211 
"sum_l1 (C1 n ns) = n + sum_l2 ns"  

212 
"sum_l2 N2 = 0"  

213 
"sum_l2 (C2 n ns) = n + sum_l1 ns" 

214 

215 
datatype 

216 
('a, 'b) t1 = T1 'a 'b "('a, 'b) t1 l1" and 

217 
('a, 'b) t2 = T2 "('a, 'b) t1" 

218 

219 
primrec 

220 
h1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and 

221 
h1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and 

222 
h1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat" 

223 
where 

224 
"h1_tl1 N1 = 0"  

225 
"h1_tl1 (C1 t ts) = h1_t1 t + h1_tl2 ts"  

226 
"h1_tl2 N2 = 0"  

227 
"h1_tl2 (C2 t ts) = h1_t1 t + h1_tl1 ts"  

228 
"h1_t1 (T1 n _ ts) = n + h1_tl1 ts" 

229 

62688  230 
(* should hit cache *) 
58385  231 
primrec 
232 
h2_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and 

233 
h2_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and 

234 
h2_t1 :: "(nat, 'a) t1 \<Rightarrow> nat" 

235 
where 

236 
"h2_tl1 N1 = 0"  

237 
"h2_tl1 (C1 t ts) = h2_t1 t + h2_tl2 ts"  

238 
"h2_tl2 N2 = 0"  

239 
"h2_tl2 (C2 t ts) = h2_t1 t + h2_tl1 ts"  

240 
"h2_t1 (T1 n _ ts) = n + h2_tl1 ts" 

241 

62688  242 
(* should hit cache *) 
58385  243 
primrec 
244 
h3_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and 

245 
h3_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and 

246 
h3_t1 :: "(nat, 'a) t1 \<Rightarrow> nat" 

247 
where 

248 
"h3_tl1 N1 = 0"  

249 
"h3_tl1 (C1 t ts) = h3_t1 t + h3_tl2 ts"  

250 
"h3_tl2 N2 = 0"  

251 
"h3_tl2 (C2 t ts) = h3_t1 t + h3_tl1 ts"  

252 
"h3_t1 (T1 n _ ts) = n + h3_tl1 ts" 

253 

62688  254 
(* should hit cache *) 
58385  255 
primrec 
256 
i1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and 

257 
i1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and 

258 
i1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat" and 

259 
i1_t2 :: "(nat, 'a) t2 \<Rightarrow> nat" 

260 
where 

261 
"i1_tl1 N1 = 0"  

262 
"i1_tl1 (C1 t ts) = i1_t1 t + i1_tl2 ts"  

263 
"i1_tl2 N2 = 0"  

264 
"i1_tl2 (C2 t ts) = i1_t1 t + i1_tl1 ts"  

265 
"i1_t1 (T1 n _ ts) = n + i1_tl1 ts"  

266 
"i1_t2 (T2 t) = i1_t1 t" 

267 

62688  268 
(* should hit cache *) 
58385  269 
primrec 
270 
j1_t2 :: "(nat, 'a) t2 \<Rightarrow> nat" and 

271 
j1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat" and 

272 
j1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and 

273 
j1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" 

274 
where 

275 
"j1_tl1 N1 = 0"  

276 
"j1_tl1 (C1 t ts) = j1_t1 t + j1_tl2 ts"  

277 
"j1_tl2 N2 = 0"  

278 
"j1_tl2 (C2 t ts) = j1_t1 t + j1_tl1 ts"  

279 
"j1_t1 (T1 n _ ts) = n + j1_tl1 ts"  

280 
"j1_t2 (T2 t) = j1_t1 t" 

281 

282 

283 
datatype 'a l3 = N3  C3 'a "'a l3" 

284 
datatype 'a l4 = N4  C4 'a "'a l4" 

285 
datatype ('a, 'b) t3 = T3 'a 'b "('a, 'b) t3 l3" "('a, 'b) t3 l4" 

286 

287 
primrec 

288 
k1_tl3 :: "(nat, 'a) t3 l3 \<Rightarrow> nat" and 

289 
k1_tl4 :: "(nat, 'a) t3 l4 \<Rightarrow> nat" and 

290 
k1_t3 :: "(nat, 'a) t3 \<Rightarrow> nat" 

291 
where 

292 
"k1_tl3 N3 = 0"  

293 
"k1_tl3 (C3 t ts) = k1_t3 t + k1_tl3 ts"  

294 
"k1_tl4 N4 = 0"  

295 
"k1_tl4 (C4 t ts) = k1_t3 t + k1_tl4 ts"  

296 
"k1_t3 (T3 n _ ts us) = n + k1_tl3 ts + k1_tl4 us" 

297 

62688  298 
(* should hit cache *) 
58385  299 
primrec 
300 
k2_tl4 :: "(nat, int) t3 l4 \<Rightarrow> nat" and 

301 
k2_tl3 :: "(nat, int) t3 l3 \<Rightarrow> nat" and 

302 
k2_t3 :: "(nat, int) t3 \<Rightarrow> nat" 

303 
where 

304 
"k2_tl4 N4 = 0"  

305 
"k2_tl4 (C4 t ts) = k2_t3 t + k2_tl4 ts"  

306 
"k2_tl3 N3 = 0"  

307 
"k2_tl3 (C3 t ts) = k2_t3 t + k2_tl3 ts"  

308 
"k2_t3 (T3 n _ ts us) = n + k2_tl3 ts + k2_tl4 us" 

309 

310 

311 
datatype ('a, 'b) l5 = N5  C5 'a 'b "('a, 'b) l5" 

312 
datatype ('a, 'b) l6 = N6  C6 'a 'b "('a, 'b) l6" 

313 
datatype ('a, 'b, 'c) t4 = T4 'a 'b "(('a, 'b, 'c) t4, 'b) l5" "(('a, 'b, 'c) t4, 'c) l6" 

314 

315 
primrec 

316 
l1_tl5 :: "((nat, 'a, 'b) t4, 'a) l5 \<Rightarrow> nat" and 

317 
l1_tl6 :: "((nat, 'a, 'b) t4, 'b) l6 \<Rightarrow> nat" and 

318 
l1_t4 :: "(nat, 'a, 'b) t4 \<Rightarrow> nat" 

319 
where 

320 
"l1_tl5 N5 = 0"  

321 
"l1_tl5 (C5 t _ ts) = l1_t4 t + l1_tl5 ts"  

322 
"l1_tl6 N6 = 0"  

323 
"l1_tl6 (C6 t _ ts) = l1_t4 t + l1_tl6 ts"  

324 
"l1_t4 (T4 n _ ts us) = n + l1_tl5 ts + l1_tl6 us" 

325 

326 

58396  327 
subsection \<open>Primcorec Cache\<close> 
58385  328 

329 
codatatype 'a col = N  C 'a "'a col" 

330 
codatatype ('a, 'b) cot = T 'a 'b "('a, 'b) cot col" 

331 

332 
context linorder 

333 
begin 

334 

335 
primcorec 

336 
f1_cotcol :: "nat \<Rightarrow> (nat, 'a) cot col" and 

337 
f1_cot :: "nat \<Rightarrow> (nat, 'a) cot" 

338 
where 

339 
"n = 0 \<Longrightarrow> f1_cotcol n = N"  

340 
"_ \<Longrightarrow> f1_cotcol n = C (f1_cot n) (f1_cotcol n)"  

341 
"f1_cot n = T n undefined (f1_cotcol n)" 

342 

62688  343 
(* should hit cache *) 
58385  344 
primcorec 
345 
f2_cotcol :: "nat \<Rightarrow> (nat, 'b) cot col" and 

346 
f2_cot :: "nat \<Rightarrow> (nat, 'b) cot" 

347 
where 

348 
"n = 0 \<Longrightarrow> f2_cotcol n = N"  

349 
"_ \<Longrightarrow> f2_cotcol n = C (f2_cot n) (f2_cotcol n)"  

350 
"f2_cot n = T n undefined (f2_cotcol n)" 

351 

352 
end 

353 

62688  354 
(* should hit cache *) 
58385  355 
primcorec 
356 
g1_cot :: "int \<Rightarrow> (int, 'a) cot" and 

357 
g1_cotcol :: "int \<Rightarrow> (int, 'a) cot col" 

358 
where 

359 
"g1_cot n = T n undefined (g1_cotcol n)"  

360 
"n = 0 \<Longrightarrow> g1_cotcol n = N"  

361 
"_ \<Longrightarrow> g1_cotcol n = C (g1_cot n) (g1_cotcol n)" 

362 

62688  363 
(* should hit cache *) 
58385  364 
primcorec 
365 
g2_cot :: "int \<Rightarrow> (int, int) cot" and 

366 
g2_cotcol :: "int \<Rightarrow> (int, int) cot col" 

367 
where 

368 
"g2_cot n = T n undefined (g2_cotcol n)"  

369 
"n = 0 \<Longrightarrow> g2_cotcol n = N"  

370 
"_ \<Longrightarrow> g2_cotcol n = C (g2_cot n) (g2_cotcol n)" 

371 

372 

373 
codatatype 

374 
'a col1 = N1  C1 'a "'a col2" and 

375 
'a col2 = N2  C2 'a "'a col1" 

376 

377 
codatatype 

378 
('a, 'b) cot1 = T1 'a 'b "('a, 'b) cot1 col1" and 

379 
('a, 'b) cot2 = T2 "('a, 'b) cot1" 

380 

381 
primcorec 

382 
h1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and 

383 
h1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and 

384 
h1_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1" 

385 
where 

386 
"h1_cotcol1 n = C1 (h1_cot1 n) (h1_cotcol2 n)"  

387 
"h1_cotcol2 n = C2 (h1_cot1 n) (h1_cotcol1 n)"  

388 
"h1_cot1 n = T1 n undefined (h1_cotcol1 n)" 

389 

62688  390 
(* should hit cache *) 
58385  391 
primcorec 
392 
h2_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and 

393 
h2_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and 

394 
h2_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1" 

395 
where 

396 
"h2_cotcol1 n = C1 (h2_cot1 n) (h2_cotcol2 n)"  

397 
"h2_cotcol2 n = C2 (h2_cot1 n) (h2_cotcol1 n)"  

398 
"h2_cot1 n = T1 n undefined (h2_cotcol1 n)" 

399 

62688  400 
(* should hit cache *) 
58385  401 
primcorec 
402 
h3_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and 

403 
h3_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and 

404 
h3_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1" 

405 
where 

406 
"h3_cotcol1 n = C1 (h3_cot1 n) (h3_cotcol2 n)"  

407 
"h3_cotcol2 n = C2 (h3_cot1 n) (h3_cotcol1 n)"  

408 
"h3_cot1 n = T1 n undefined (h3_cotcol1 n)" 

409 

62688  410 
(* should hit cache *) 
58385  411 
primcorec 
412 
i1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and 

413 
i1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and 

414 
i1_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1" and 

415 
i1_cot2 :: "nat \<Rightarrow> (nat, 'a) cot2" 

416 
where 

417 
"i1_cotcol1 n = C1 (i1_cot1 n) (i1_cotcol2 n)"  

418 
"i1_cotcol2 n = C2 (i1_cot1 n) (i1_cotcol1 n)"  

419 
"i1_cot1 n = T1 n undefined (i1_cotcol1 n)"  

420 
"i1_cot2 n = T2 (i1_cot1 n)" 

421 

62688  422 
(* should hit cache *) 
58385  423 
primcorec 
424 
j1_cot2 :: "nat \<Rightarrow> (nat, 'a) cot2" and 

425 
j1_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1" and 

426 
j1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and 

427 
j1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" 

428 
where 

429 
"j1_cotcol1 n = C1 (j1_cot1 n) (j1_cotcol2 n)"  

430 
"j1_cotcol2 n = C2 (j1_cot1 n) (j1_cotcol1 n)"  

431 
"j1_cot1 n = T1 n undefined (j1_cotcol1 n)"  

432 
"j1_cot2 n = T2 (j1_cot1 n)" 

433 

434 

435 
codatatype 'a col3 = N3  C3 'a "'a col3" 

436 
codatatype 'a col4 = N4  C4 'a "'a col4" 

437 
codatatype ('a, 'b) cot3 = T3 'a 'b "('a, 'b) cot3 col3" "('a, 'b) cot3 col4" 

438 

439 
primcorec 

440 
k1_cotcol3 :: "nat \<Rightarrow> (nat, 'a) cot3 col3" and 

441 
k1_cotcol4 :: "nat \<Rightarrow> (nat, 'a) cot3 col4" and 

442 
k1_cot3 :: "nat \<Rightarrow> (nat, 'a) cot3" 

443 
where 

444 
"k1_cotcol3 n = C3 (k1_cot3 n) (k1_cotcol3 n)"  

445 
"k1_cotcol4 n = C4 (k1_cot3 n) (k1_cotcol4 n)"  

446 
"k1_cot3 n = T3 n undefined (k1_cotcol3 n) (k1_cotcol4 n)" 

447 

62688  448 
(* should hit cache *) 
58385  449 
primcorec 
450 
k2_cotcol4 :: "nat \<Rightarrow> (nat, 'a) cot3 col4" and 

451 
k2_cotcol3 :: "nat \<Rightarrow> (nat, 'a) cot3 col3" and 

452 
k2_cot3 :: "nat \<Rightarrow> (nat, 'a) cot3" 

453 
where 

454 
"k2_cotcol4 n = C4 (k2_cot3 n) (k2_cotcol4 n)"  

455 
"k2_cotcol3 n = C3 (k2_cot3 n) (k2_cotcol3 n)"  

456 
"k2_cot3 n = T3 n undefined (k2_cotcol3 n) (k2_cotcol4 n)" 

457 

62688  458 
datatype ('a,'b)complex = 
459 
C1 nat "'a ttree" 

460 
 C2 "('a,'b)complex list tree tree" 'b "('a,'b)complex" "('a,'b)complex2 ttree list" 

461 
and ('a,'b)complex2 = D1 "('a,'b)complex ttree" 

462 
datatype_compat complex complex2 

463 

58385  464 
end 