src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (23 months ago)
changeset 66924 b4d4027f743b
parent 66453 cc19f7ca2ed6
permissions -rw-r--r--
more permissive;
     1 (*  Title:      Benchmarks/Datatype_Benchmark/Misc_N2M.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Copyright   2014
     4 
     5 Miscellaneous tests for the nested-to-mutual reduction.
     6 *)
     7 
     8 section \<open>Miscellaneous Tests for the Nested-to-Mutual Reduction\<close>
     9 
    10 theory Misc_N2M
    11 imports "HOL-Library.BNF_Axiomatization"
    12 begin
    13 
    14 declare [[typedef_overloaded]]
    15 
    16 
    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"
   105        and ('a, 'b) L = CL "('b, ('a, 'b) K) L0"
   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 
   132 subsection \<open>Deep Nesting\<close>
   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 
   155 
   156 subsection \<open>Primrec cache\<close>
   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 
   172 (* should hit cache *)
   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 
   183 (* should hit cache *)
   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 
   192 (* should hit cache *)
   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 
   230 (* should hit cache *)
   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 
   242 (* should hit cache *)
   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 
   254 (* should hit cache *)
   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 
   268 (* should hit cache *)
   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 
   298 (* should hit cache *)
   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 
   327 subsection \<open>Primcorec Cache\<close>
   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 
   343 (* should hit cache *)
   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 
   354 (* should hit cache *)
   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 
   363 (* should hit cache *)
   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 
   390 (* should hit cache *)
   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 
   400 (* should hit cache *)
   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 
   410 (* should hit cache *)
   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 
   422 (* should hit cache *)
   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 
   448 (* should hit cache *)
   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 
   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 
   464 end