src/HOL/Datatype_Examples/Misc_N2M.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58396 7b60e4e74430
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 (*  Title:      HOL/Datatype_Examples/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 header \<open>Miscellaneous Tests for the Nested-to-Mutual Reduction\<close>
     9 
    10 theory Misc_N2M
    11 imports "~~/src/HOL/Library/BNF_Axiomatization"
    12 begin
    13 
    14 locale misc
    15 begin
    16 
    17 datatype 'a li = Ni | Co 'a "'a li"
    18 datatype 'a tr = Tr "'a \<Rightarrow> 'a tr li"
    19 
    20 primrec (nonexhaustive)
    21   f_tl :: "'a \<Rightarrow> 'a tr li \<Rightarrow> nat" and
    22   f_t :: "'a \<Rightarrow> 'a tr \<Rightarrow> nat"
    23 where
    24   "f_tl _ Ni = 0" |
    25   "f_t a (Tr ts) = 1 + f_tl a (ts a)"
    26 
    27 datatype ('a, 'b) l = N | C 'a 'b "('a, 'b) l"
    28 datatype ('a, 'b) t = T "(('a, 'b) t, 'a) l" "(('a, 'b) t, 'b) l"
    29 
    30 primrec (nonexhaustive)
    31   f_tl2 :: "(('a, 'a) t, 'a) l \<Rightarrow> nat" and
    32   f_t2 :: "('a, 'a) t \<Rightarrow> nat"
    33 where
    34   "f_tl2 N = 0" |
    35   "f_t2 (T ts us) = f_tl2 ts + f_tl2 us"
    36 
    37 primrec  (nonexhaustive)
    38   g_tla :: "(('a, 'b) t, 'a) l \<Rightarrow> nat" and
    39   g_tlb :: "(('a, 'b) t, 'b) l \<Rightarrow> nat" and
    40   g_t :: "('a, 'b) t \<Rightarrow> nat"
    41 where
    42   "g_tla N = 0" |
    43   "g_tlb N = 1" |
    44   "g_t (T ts us) = g_tla ts + g_tlb us"
    45 
    46 
    47 datatype
    48   'a l1 = N1 | C1 'a "'a l1"
    49 
    50 datatype
    51   ('a, 'b) t1 = T1 'a 'b "('a, 'b) t1 l1" "(nat \<times> ('a, 'b) t1) l1" and
    52   ('a, 'b) t2 = T2 "('a, 'b) t1"
    53 
    54 primrec
    55   h1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
    56   h1_natl1 :: "(nat \<times> (nat, 'a) t1) l1 \<Rightarrow> nat" and
    57   h1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat"
    58 where
    59   "h1_tl1 N1 = 0" |
    60   "h1_tl1 (C1 t ts) = h1_t1 t + h1_tl1 ts" |
    61   "h1_natl1 N1 = Suc 0" |
    62   "h1_natl1 (C1 n ts) = fst n + h1_natl1 ts" |
    63   "h1_t1 (T1 n _ ts _) = n + h1_tl1 ts"
    64 
    65 end
    66 
    67 
    68 bnf_axiomatization ('a, 'b) M0 [wits: "('a, 'b) M0"]
    69 bnf_axiomatization ('a, 'b) N0 [wits: "('a, 'b) N0"]
    70 bnf_axiomatization ('a, 'b) K0 [wits: "('a, 'b) K0"]
    71 bnf_axiomatization ('a, 'b) L0 [wits: "('a, 'b) L0"]
    72 bnf_axiomatization ('a, 'b, 'c) G0 [wits: "('a, 'b, 'c) G0"]
    73 
    74 locale (*co*)mplicated
    75 begin
    76 
    77 datatype 'a M = CM "('a, 'a M) M0"
    78 datatype 'a N = CN "('a N, 'a) N0"
    79 datatype ('a, 'b) K = CK "('a, ('a, 'b) L) K0"
    80          and ('a, 'b) L = CL "('b, ('a, 'b) K) L0"
    81 datatype 'a G = CG "('a, ('a G, 'a G N) K, ('a G M, 'a G) L) G0"
    82 
    83 primrec
    84     fG :: "'a G \<Rightarrow> 'a G"
    85 and fK :: "('a G, 'a G N) K \<Rightarrow> ('a G, 'a G N) K"
    86 and fL :: "('a G, 'a G N) L \<Rightarrow> ('a G, 'a G N) L"
    87 and fM :: "'a G M \<Rightarrow> 'a G M" where
    88   "fG (CG x) = CG (map_G0 id fK (map_L fM fG) x)"
    89 | "fK (CK y) = CK (map_K0 fG fL y)"
    90 | "fL (CL z) = CL (map_L0 (map_N fG) fK z)"
    91 | "fM (CM w) = CM (map_M0 fG fM w)"
    92 thm fG_def fK_def fL_def fM_def fG.simps fK.simps fL.simps fM.simps
    93 
    94 end
    95 
    96 locale complicated
    97 begin
    98 
    99 codatatype 'a M = CM "('a, 'a M) M0"
   100 codatatype 'a N = CN "('a N, 'a) N0"
   101 codatatype ('a, 'b) K = CK "('a, ('a, 'b) L) K0"
   102          and ('a, 'b) L = CL "('b, ('a, 'b) K) L0"
   103 codatatype 'a G = CG "('a, ('a G, 'a G N) K, ('a G M, 'a G) L) G0"
   104 
   105 primcorec
   106     fG :: "'a G \<Rightarrow> 'a G"
   107 and fK :: "('a G, 'a G N) K \<Rightarrow> ('a G, 'a G N) K"
   108 and fL :: "('a G, 'a G N) L \<Rightarrow> ('a G, 'a G N) L"
   109 and fM :: "'a G M \<Rightarrow> 'a G M" where
   110   "fG x = CG (map_G0 id fK (map_L fM fG) (un_CG x))"
   111 | "fK y = CK (map_K0 fG fL (un_CK y))"
   112 | "fL z = CL (map_L0 (map_N fG) fK (un_CL z))"
   113 | "fM w = CM (map_M0 fG fM (un_CM w))"
   114 thm fG_def fK_def fL_def fM_def fG.simps fK.simps fL.simps fM.simps
   115 
   116 end
   117 
   118 datatype ('a, 'b) F1 = F1 'a 'b
   119 datatype F2 = F2 "((unit, nat) F1, F2) F1" | F2'
   120 datatype 'a kk1 = K1 'a | K2 "'a kk2" and 'a kk2 = K3 "'a kk1"
   121 datatype 'a ll1 = L1 'a | L2 "'a ll2 kk2" and 'a ll2 = L3 "'a ll1"
   122 
   123 datatype_compat F1
   124 datatype_compat F2
   125 datatype_compat kk1 kk2
   126 datatype_compat ll1 ll2
   127 
   128 
   129 subsection \<open>Deep Nesting\<close>
   130 
   131 datatype 'a tree = Empty | Node 'a "'a tree list"
   132 datatype_compat tree
   133 
   134 datatype 'a ttree = TEmpty | TNode 'a "'a ttree list tree"
   135 datatype_compat ttree
   136 
   137 datatype 'a tttree = TEmpty | TNode 'a "'a tttree list ttree list tree"
   138 datatype_compat tttree
   139 (*
   140 datatype 'a ttttree = TEmpty | TNode 'a "'a ttttree list tttree list ttree list tree"
   141 datatype_compat ttttree
   142 *)
   143 
   144 datatype ('a,'b)complex = 
   145   C1 nat "'a ttree" 
   146 | C2 "('a,'b)complex list tree tree" 'b "('a,'b)complex" "('a,'b)complex2 ttree list"
   147 and ('a,'b)complex2 = D1 "('a,'b)complex ttree"
   148 datatype_compat complex complex2
   149 
   150 datatype 'a F = F1 'a | F2 "'a F"
   151 datatype 'a G = G1 'a | G2 "'a G F"
   152 datatype H = H1 | H2 "H G"
   153 
   154 datatype_compat F
   155 datatype_compat G
   156 datatype_compat H
   157 
   158 
   159 subsection \<open>Primrec cache\<close>
   160 
   161 datatype 'a l = N | C 'a "'a l"
   162 datatype ('a, 'b) t = T 'a 'b "('a, 'b) t l"
   163 
   164 context linorder
   165 begin
   166 
   167 (* slow *)
   168 primrec
   169   f1_tl :: "(nat, 'a) t l \<Rightarrow> nat" and
   170   f1_t :: "(nat, 'a) t \<Rightarrow> nat"
   171 where
   172   "f1_tl N = 0" |
   173   "f1_tl (C t ts) = f1_t t + f1_tl ts" |
   174   "f1_t (T n _ ts) = n + f1_tl ts"
   175 
   176 (* should be fast *)
   177 primrec
   178   f2_t :: "(nat, 'b) t \<Rightarrow> nat" and
   179   f2_tl :: "(nat, 'b) t l \<Rightarrow> nat"
   180 where
   181   "f2_tl N = 0" |
   182   "f2_tl (C t ts) = f2_t t + f2_tl ts" |
   183   "f2_t (T n _ ts) = n + f2_tl ts"
   184 
   185 end
   186 
   187 (* should be fast *)
   188 primrec
   189   g1_t :: "('a, int) t \<Rightarrow> nat" and
   190   g1_tl :: "('a, int) t l \<Rightarrow> nat"
   191 where
   192   "g1_t (T _ _ ts) = g1_tl ts" |
   193   "g1_tl N = 0" |
   194   "g1_tl (C _ ts) = g1_tl ts"
   195 
   196 (* should be fast *)
   197 primrec
   198   g2_t :: "(int, int) t \<Rightarrow> nat" and
   199   g2_tl :: "(int, int) t l \<Rightarrow> nat"
   200 where
   201   "g2_t (T _ _ ts) = g2_tl ts" |
   202   "g2_tl N = 0" |
   203   "g2_tl (C _ ts) = g2_tl ts"
   204 
   205 
   206 datatype
   207   'a l1 = N1 | C1 'a "'a l2" and
   208   'a l2 = N2 | C2 'a "'a l1"
   209 
   210 primrec
   211   sum_l1 :: "'a::{zero,plus} l1 \<Rightarrow> 'a" and
   212   sum_l2 :: "'a::{zero,plus} l2 \<Rightarrow> 'a"
   213 where
   214   "sum_l1 N1 = 0" |
   215   "sum_l1 (C1 n ns) = n + sum_l2 ns" |
   216   "sum_l2 N2 = 0" |
   217   "sum_l2 (C2 n ns) = n + sum_l1 ns"
   218 
   219 datatype
   220   ('a, 'b) t1 = T1 'a 'b "('a, 'b) t1 l1" and
   221   ('a, 'b) t2 = T2 "('a, 'b) t1"
   222 
   223 (* slow *)
   224 primrec
   225   h1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
   226   h1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
   227   h1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat"
   228 where
   229   "h1_tl1 N1 = 0" |
   230   "h1_tl1 (C1 t ts) = h1_t1 t + h1_tl2 ts" |
   231   "h1_tl2 N2 = 0" |
   232   "h1_tl2 (C2 t ts) = h1_t1 t + h1_tl1 ts" |
   233   "h1_t1 (T1 n _ ts) = n + h1_tl1 ts"
   234 
   235 (* should be fast *)
   236 primrec
   237   h2_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
   238   h2_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
   239   h2_t1 :: "(nat, 'a) t1 \<Rightarrow> nat"
   240 where
   241   "h2_tl1 N1 = 0" |
   242   "h2_tl1 (C1 t ts) = h2_t1 t + h2_tl2 ts" |
   243   "h2_tl2 N2 = 0" |
   244   "h2_tl2 (C2 t ts) = h2_t1 t + h2_tl1 ts" |
   245   "h2_t1 (T1 n _ ts) = n + h2_tl1 ts"
   246 
   247 (* should be fast *)
   248 primrec
   249   h3_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
   250   h3_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
   251   h3_t1 :: "(nat, 'a) t1 \<Rightarrow> nat"
   252 where
   253   "h3_tl1 N1 = 0" |
   254   "h3_tl1 (C1 t ts) = h3_t1 t + h3_tl2 ts" |
   255   "h3_tl2 N2 = 0" |
   256   "h3_tl2 (C2 t ts) = h3_t1 t + h3_tl1 ts" |
   257   "h3_t1 (T1 n _ ts) = n + h3_tl1 ts"
   258 
   259 (* should be fast *)
   260 primrec
   261   i1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
   262   i1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
   263   i1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat" and
   264   i1_t2 :: "(nat, 'a) t2 \<Rightarrow> nat"
   265 where
   266   "i1_tl1 N1 = 0" |
   267   "i1_tl1 (C1 t ts) = i1_t1 t + i1_tl2 ts" |
   268   "i1_tl2 N2 = 0" |
   269   "i1_tl2 (C2 t ts) = i1_t1 t + i1_tl1 ts" |
   270   "i1_t1 (T1 n _ ts) = n + i1_tl1 ts" |
   271   "i1_t2 (T2 t) = i1_t1 t"
   272 
   273 (* should be fast *)
   274 primrec
   275   j1_t2 :: "(nat, 'a) t2 \<Rightarrow> nat" and
   276   j1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat" and
   277   j1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
   278   j1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat"
   279 where
   280   "j1_tl1 N1 = 0" |
   281   "j1_tl1 (C1 t ts) = j1_t1 t + j1_tl2 ts" |
   282   "j1_tl2 N2 = 0" |
   283   "j1_tl2 (C2 t ts) = j1_t1 t + j1_tl1 ts" |
   284   "j1_t1 (T1 n _ ts) = n + j1_tl1 ts" |
   285   "j1_t2 (T2 t) = j1_t1 t"
   286 
   287 
   288 datatype 'a l3 = N3 | C3 'a "'a l3"
   289 datatype 'a l4 = N4 | C4 'a "'a l4"
   290 datatype ('a, 'b) t3 = T3 'a 'b "('a, 'b) t3 l3" "('a, 'b) t3 l4"
   291 
   292 (* slow *)
   293 primrec
   294   k1_tl3 :: "(nat, 'a) t3 l3 \<Rightarrow> nat" and
   295   k1_tl4 :: "(nat, 'a) t3 l4 \<Rightarrow> nat" and
   296   k1_t3 :: "(nat, 'a) t3 \<Rightarrow> nat"
   297 where
   298   "k1_tl3 N3 = 0" |
   299   "k1_tl3 (C3 t ts) = k1_t3 t + k1_tl3 ts" |
   300   "k1_tl4 N4 = 0" |
   301   "k1_tl4 (C4 t ts) = k1_t3 t + k1_tl4 ts" |
   302   "k1_t3 (T3 n _ ts us) = n + k1_tl3 ts + k1_tl4 us"
   303 
   304 (* should be fast *)
   305 primrec
   306   k2_tl4 :: "(nat, int) t3 l4 \<Rightarrow> nat" and
   307   k2_tl3 :: "(nat, int) t3 l3 \<Rightarrow> nat" and
   308   k2_t3 :: "(nat, int) t3 \<Rightarrow> nat"
   309 where
   310   "k2_tl4 N4 = 0" |
   311   "k2_tl4 (C4 t ts) = k2_t3 t + k2_tl4 ts" |
   312   "k2_tl3 N3 = 0" |
   313   "k2_tl3 (C3 t ts) = k2_t3 t + k2_tl3 ts" |
   314   "k2_t3 (T3 n _ ts us) = n + k2_tl3 ts + k2_tl4 us"
   315 
   316 
   317 datatype ('a, 'b) l5 = N5 | C5 'a 'b "('a, 'b) l5"
   318 datatype ('a, 'b) l6 = N6 | C6 'a 'b "('a, 'b) l6"
   319 datatype ('a, 'b, 'c) t4 = T4 'a 'b "(('a, 'b, 'c) t4, 'b) l5" "(('a, 'b, 'c) t4, 'c) l6"
   320 
   321 (* slow *)
   322 primrec
   323   l1_tl5 :: "((nat, 'a, 'b) t4, 'a) l5 \<Rightarrow> nat" and
   324   l1_tl6 :: "((nat, 'a, 'b) t4, 'b) l6 \<Rightarrow> nat" and
   325   l1_t4 :: "(nat, 'a, 'b) t4 \<Rightarrow> nat"
   326 where
   327   "l1_tl5 N5 = 0" |
   328   "l1_tl5 (C5 t _ ts) = l1_t4 t + l1_tl5 ts" |
   329   "l1_tl6 N6 = 0" |
   330   "l1_tl6 (C6 t _ ts) = l1_t4 t + l1_tl6 ts" |
   331   "l1_t4 (T4 n _ ts us) = n + l1_tl5 ts + l1_tl6 us"
   332 
   333 
   334 subsection \<open>Primcorec Cache\<close>
   335 
   336 codatatype 'a col = N | C 'a "'a col"
   337 codatatype ('a, 'b) cot = T 'a 'b "('a, 'b) cot col"
   338 
   339 context linorder
   340 begin
   341 
   342 (* slow *)
   343 primcorec
   344   f1_cotcol :: "nat \<Rightarrow> (nat, 'a) cot col" and
   345   f1_cot :: "nat \<Rightarrow> (nat, 'a) cot"
   346 where
   347   "n = 0 \<Longrightarrow> f1_cotcol n = N" |
   348   "_ \<Longrightarrow> f1_cotcol n = C (f1_cot n) (f1_cotcol n)" |
   349   "f1_cot n = T n undefined (f1_cotcol n)"
   350 
   351 (* should be fast *)
   352 primcorec
   353   f2_cotcol :: "nat \<Rightarrow> (nat, 'b) cot col" and
   354   f2_cot :: "nat \<Rightarrow> (nat, 'b) cot"
   355 where
   356   "n = 0 \<Longrightarrow> f2_cotcol n = N" |
   357   "_ \<Longrightarrow> f2_cotcol n = C (f2_cot n) (f2_cotcol n)" |
   358   "f2_cot n = T n undefined (f2_cotcol n)"
   359 
   360 end
   361 
   362 (* should be fast *)
   363 primcorec
   364   g1_cot :: "int \<Rightarrow> (int, 'a) cot" and
   365   g1_cotcol :: "int \<Rightarrow> (int, 'a) cot col"
   366 where
   367   "g1_cot n = T n undefined (g1_cotcol n)" |
   368   "n = 0 \<Longrightarrow> g1_cotcol n = N" |
   369   "_ \<Longrightarrow> g1_cotcol n = C (g1_cot n) (g1_cotcol n)"
   370 
   371 (* should be fast *)
   372 primcorec
   373   g2_cot :: "int \<Rightarrow> (int, int) cot" and
   374   g2_cotcol :: "int \<Rightarrow> (int, int) cot col"
   375 where
   376   "g2_cot n = T n undefined (g2_cotcol n)" |
   377   "n = 0 \<Longrightarrow> g2_cotcol n = N" |
   378   "_ \<Longrightarrow> g2_cotcol n = C (g2_cot n) (g2_cotcol n)"
   379 
   380 
   381 codatatype
   382   'a col1 = N1 | C1 'a "'a col2" and
   383   'a col2 = N2 | C2 'a "'a col1"
   384 
   385 codatatype
   386   ('a, 'b) cot1 = T1 'a 'b "('a, 'b) cot1 col1" and
   387   ('a, 'b) cot2 = T2 "('a, 'b) cot1"
   388 
   389 (* slow *)
   390 primcorec
   391   h1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
   392   h1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
   393   h1_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1"
   394 where
   395   "h1_cotcol1 n = C1 (h1_cot1 n) (h1_cotcol2 n)" |
   396   "h1_cotcol2 n = C2 (h1_cot1 n) (h1_cotcol1 n)" |
   397   "h1_cot1 n = T1 n undefined (h1_cotcol1 n)"
   398 
   399 (* should be fast *)
   400 primcorec
   401   h2_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
   402   h2_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
   403   h2_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1"
   404 where
   405   "h2_cotcol1 n = C1 (h2_cot1 n) (h2_cotcol2 n)" |
   406   "h2_cotcol2 n = C2 (h2_cot1 n) (h2_cotcol1 n)" |
   407   "h2_cot1 n = T1 n undefined (h2_cotcol1 n)"
   408 
   409 (* should be fast *)
   410 primcorec
   411   h3_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
   412   h3_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
   413   h3_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1"
   414 where
   415   "h3_cotcol1 n = C1 (h3_cot1 n) (h3_cotcol2 n)" |
   416   "h3_cotcol2 n = C2 (h3_cot1 n) (h3_cotcol1 n)" |
   417   "h3_cot1 n = T1 n undefined (h3_cotcol1 n)"
   418 
   419 (* should be fast *)
   420 primcorec
   421   i1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
   422   i1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
   423   i1_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1" and
   424   i1_cot2 :: "nat \<Rightarrow> (nat, 'a) cot2"
   425 where
   426   "i1_cotcol1 n = C1 (i1_cot1 n) (i1_cotcol2 n)" |
   427   "i1_cotcol2 n = C2 (i1_cot1 n) (i1_cotcol1 n)" |
   428   "i1_cot1 n = T1 n undefined (i1_cotcol1 n)" |
   429   "i1_cot2 n = T2 (i1_cot1 n)"
   430 
   431 (* should be fast *)
   432 primcorec
   433   j1_cot2 :: "nat \<Rightarrow> (nat, 'a) cot2" and
   434   j1_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1" and
   435   j1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
   436   j1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2"
   437 where
   438   "j1_cotcol1 n = C1 (j1_cot1 n) (j1_cotcol2 n)" |
   439   "j1_cotcol2 n = C2 (j1_cot1 n) (j1_cotcol1 n)" |
   440   "j1_cot1 n = T1 n undefined (j1_cotcol1 n)" |
   441   "j1_cot2 n = T2 (j1_cot1 n)"
   442 
   443 
   444 codatatype 'a col3 = N3 | C3 'a "'a col3"
   445 codatatype 'a col4 = N4 | C4 'a "'a col4"
   446 codatatype ('a, 'b) cot3 = T3 'a 'b "('a, 'b) cot3 col3" "('a, 'b) cot3 col4"
   447 
   448 (* slow *)
   449 primcorec
   450   k1_cotcol3 :: "nat \<Rightarrow> (nat, 'a) cot3 col3" and
   451   k1_cotcol4 :: "nat \<Rightarrow> (nat, 'a) cot3 col4" and
   452   k1_cot3 :: "nat \<Rightarrow> (nat, 'a) cot3"
   453 where
   454   "k1_cotcol3 n = C3 (k1_cot3 n) (k1_cotcol3 n)" |
   455   "k1_cotcol4 n = C4 (k1_cot3 n) (k1_cotcol4 n)" |
   456   "k1_cot3 n = T3 n undefined (k1_cotcol3 n) (k1_cotcol4 n)"
   457 
   458 (* should be fast *)
   459 primcorec
   460   k2_cotcol4 :: "nat \<Rightarrow> (nat, 'a) cot3 col4" and
   461   k2_cotcol3 :: "nat \<Rightarrow> (nat, 'a) cot3 col3" and
   462   k2_cot3 :: "nat \<Rightarrow> (nat, 'a) cot3"
   463 where
   464   "k2_cotcol4 n = C4 (k2_cot3 n) (k2_cotcol4 n)" |
   465   "k2_cotcol3 n = C3 (k2_cot3 n) (k2_cotcol3 n)" |
   466   "k2_cot3 n = T3 n undefined (k2_cotcol3 n) (k2_cotcol4 n)"
   467 
   468 end