regression tests for n2m
authortraytel
Fri Sep 19 10:00:34 2014 +0200 (2014-09-19)
changeset 583859cbef70cff8e
parent 58384 00aaaa7bd752
child 58386 6999f55645ea
regression tests for n2m
src/HOL/Datatype_Examples/Misc_N2M.thy
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Datatype_Examples/Misc_N2M.thy	Fri Sep 19 10:00:34 2014 +0200
     1.3 @@ -0,0 +1,469 @@
     1.4 +(*  Title:      HOL/Datatype_Examples/Misc_N2M.thy
     1.5 +    Author:     Dmitriy Traytel, TU Muenchen
     1.6 +    Copyright   2014
     1.7 +
     1.8 +Miscellaneous datatype definitions.
     1.9 +*)
    1.10 +
    1.11 +header \<open>Miscellaneous Tests for the Nested-to-Mutual Reduction\<close>
    1.12 +
    1.13 +theory Misc_N2M
    1.14 +imports "~~/src/HOL/Library/BNF_Axiomatization"
    1.15 +begin
    1.16 +
    1.17 +locale misc
    1.18 +begin
    1.19 +
    1.20 +datatype 'a li = Ni | Co 'a "'a li"
    1.21 +datatype 'a tr = Tr "'a \<Rightarrow> 'a tr li"
    1.22 +
    1.23 +primrec (nonexhaustive)
    1.24 +  f_tl :: "'a \<Rightarrow> 'a tr li \<Rightarrow> nat" and
    1.25 +  f_t :: "'a \<Rightarrow> 'a tr \<Rightarrow> nat"
    1.26 +where
    1.27 +  "f_tl _ Ni = 0" |
    1.28 +  "f_t a (Tr ts) = 1 + f_tl a (ts a)"
    1.29 +
    1.30 +datatype ('a, 'b) l = N | C 'a 'b "('a, 'b) l"
    1.31 +datatype ('a, 'b) t = T "(('a, 'b) t, 'a) l" "(('a, 'b) t, 'b) l"
    1.32 +
    1.33 +primrec (nonexhaustive)
    1.34 +  f_tl2 :: "(('a, 'a) t, 'a) l \<Rightarrow> nat" and
    1.35 +  f_t2 :: "('a, 'a) t \<Rightarrow> nat"
    1.36 +where
    1.37 +  "f_tl2 N = 0" |
    1.38 +  "f_t2 (T ts us) = f_tl2 ts + f_tl2 us"
    1.39 +
    1.40 +primrec  (nonexhaustive)
    1.41 +  g_tla :: "(('a, 'b) t, 'a) l \<Rightarrow> nat" and
    1.42 +  g_tlb :: "(('a, 'b) t, 'b) l \<Rightarrow> nat" and
    1.43 +  g_t :: "('a, 'b) t \<Rightarrow> nat"
    1.44 +where
    1.45 +  "g_tla N = 0" |
    1.46 +  "g_tlb N = 1" |
    1.47 +  "g_t (T ts us) = g_tla ts + g_tlb us"
    1.48 +
    1.49 +
    1.50 +datatype
    1.51 +  'a l1 = N1 | C1 'a "'a l1"
    1.52 +
    1.53 +datatype
    1.54 +  ('a, 'b) t1 = T1 'a 'b "('a, 'b) t1 l1" "(nat \<times> ('a, 'b) t1) l1" and
    1.55 +  ('a, 'b) t2 = T2 "('a, 'b) t1"
    1.56 +
    1.57 +primrec
    1.58 +  h1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
    1.59 +  h1_natl1 :: "(nat \<times> (nat, 'a) t1) l1 \<Rightarrow> nat" and
    1.60 +  h1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat"
    1.61 +where
    1.62 +  "h1_tl1 N1 = 0" |
    1.63 +  "h1_tl1 (C1 t ts) = h1_t1 t + h1_tl1 ts" |
    1.64 +  "h1_natl1 N1 = Suc 0" |
    1.65 +  "h1_natl1 (C1 n ts) = fst n + h1_natl1 ts" |
    1.66 +  "h1_t1 (T1 n _ ts _) = n + h1_tl1 ts"
    1.67 +
    1.68 +end
    1.69 +
    1.70 +
    1.71 +bnf_axiomatization ('a, 'b) M0 [wits: "('a, 'b) M0"]
    1.72 +bnf_axiomatization ('a, 'b) N0 [wits: "('a, 'b) N0"]
    1.73 +bnf_axiomatization ('a, 'b) K0 [wits: "('a, 'b) K0"]
    1.74 +bnf_axiomatization ('a, 'b) L0 [wits: "('a, 'b) L0"]
    1.75 +bnf_axiomatization ('a, 'b, 'c) G0 [wits: "('a, 'b, 'c) G0"]
    1.76 +
    1.77 +locale (*co*)mplicated
    1.78 +begin
    1.79 +
    1.80 +datatype 'a M = CM "('a, 'a M) M0"
    1.81 +datatype 'a N = CN "('a N, 'a) N0"
    1.82 +datatype ('a, 'b) K = CK "('a, ('a, 'b) L) K0"
    1.83 +         and ('a, 'b) L = CL "('b, ('a, 'b) K) L0"
    1.84 +datatype 'a G = CG "('a, ('a G, 'a G N) K, ('a G M, 'a G) L) G0"
    1.85 +
    1.86 +primrec
    1.87 +    fG :: "'a G \<Rightarrow> 'a G"
    1.88 +and fK :: "('a G, 'a G N) K \<Rightarrow> ('a G, 'a G N) K"
    1.89 +and fL :: "('a G, 'a G N) L \<Rightarrow> ('a G, 'a G N) L"
    1.90 +and fM :: "'a G M \<Rightarrow> 'a G M" where
    1.91 +  "fG (CG x) = CG (map_G0 id fK (map_L fM fG) x)"
    1.92 +| "fK (CK y) = CK (map_K0 fG fL y)"
    1.93 +| "fL (CL z) = CL (map_L0 (map_N fG) fK z)"
    1.94 +| "fM (CM w) = CM (map_M0 fG fM w)"
    1.95 +thm fG_def fK_def fL_def fM_def fG.simps fK.simps fL.simps fM.simps
    1.96 +
    1.97 +end
    1.98 +
    1.99 +locale complicated
   1.100 +begin
   1.101 +
   1.102 +codatatype 'a M = CM "('a, 'a M) M0"
   1.103 +codatatype 'a N = CN "('a N, 'a) N0"
   1.104 +codatatype ('a, 'b) K = CK "('a, ('a, 'b) L) K0"
   1.105 +         and ('a, 'b) L = CL "('b, ('a, 'b) K) L0"
   1.106 +codatatype 'a G = CG "('a, ('a G, 'a G N) K, ('a G M, 'a G) L) G0"
   1.107 +
   1.108 +primcorec
   1.109 +    fG :: "'a G \<Rightarrow> 'a G"
   1.110 +and fK :: "('a G, 'a G N) K \<Rightarrow> ('a G, 'a G N) K"
   1.111 +and fL :: "('a G, 'a G N) L \<Rightarrow> ('a G, 'a G N) L"
   1.112 +and fM :: "'a G M \<Rightarrow> 'a G M" where
   1.113 +  "fG x = CG (map_G0 id fK (map_L fM fG) (un_CG x))"
   1.114 +| "fK y = CK (map_K0 fG fL (un_CK y))"
   1.115 +| "fL z = CL (map_L0 (map_N fG) fK (un_CL z))"
   1.116 +| "fM w = CM (map_M0 fG fM (un_CM w))"
   1.117 +thm fG_def fK_def fL_def fM_def fG.simps fK.simps fL.simps fM.simps
   1.118 +
   1.119 +end
   1.120 +
   1.121 +datatype ('a, 'b) F1 = F1 'a 'b
   1.122 +datatype F2 = F2 "((unit, nat) F1, F2) F1" | F2'
   1.123 +datatype 'a kk1 = K1 'a | K2 "'a kk2" and 'a kk2 = K3 "'a kk1"
   1.124 +datatype 'a ll1 = L1 'a | L2 "'a ll2 kk2" and 'a ll2 = L3 "'a ll1"
   1.125 +
   1.126 +datatype_compat F1
   1.127 +datatype_compat F2
   1.128 +datatype_compat kk1 kk2
   1.129 +datatype_compat ll1 ll2
   1.130 +
   1.131 +
   1.132 +
   1.133 +section \<open>Deep Nesting\<close>
   1.134 +
   1.135 +datatype 'a tree = Empty | Node 'a "'a tree list"
   1.136 +datatype_compat tree
   1.137 +
   1.138 +datatype 'a ttree = TEmpty | TNode 'a "'a ttree list tree"
   1.139 +datatype_compat ttree
   1.140 +
   1.141 +datatype 'a tttree = TEmpty | TNode 'a "'a tttree list ttree list tree"
   1.142 +datatype_compat tttree
   1.143 +(*
   1.144 +datatype 'a ttttree = TEmpty | TNode 'a "'a ttttree list tttree list ttree list tree"
   1.145 +datatype_compat ttttree
   1.146 +*)
   1.147 +
   1.148 +datatype ('a,'b)complex = 
   1.149 +  C1 nat "'a ttree" 
   1.150 +| C2 "('a,'b)complex list tree tree" 'b "('a,'b)complex" "('a,'b)complex2 ttree list"
   1.151 +and ('a,'b)complex2 = D1 "('a,'b)complex ttree"
   1.152 +datatype_compat complex complex2
   1.153 +
   1.154 +datatype 'a F = F1 'a | F2 "'a F"
   1.155 +datatype 'a G = G1 'a | G2 "'a G F"
   1.156 +datatype H = H1 | H2 "H G"
   1.157 +
   1.158 +datatype_compat F
   1.159 +datatype_compat G
   1.160 +datatype_compat H
   1.161 +
   1.162 +section \<open>Primrec cache\<close>
   1.163 +
   1.164 +datatype 'a l = N | C 'a "'a l"
   1.165 +datatype ('a, 'b) t = T 'a 'b "('a, 'b) t l"
   1.166 +
   1.167 +context linorder
   1.168 +begin
   1.169 +
   1.170 +(* slow *)
   1.171 +primrec
   1.172 +  f1_tl :: "(nat, 'a) t l \<Rightarrow> nat" and
   1.173 +  f1_t :: "(nat, 'a) t \<Rightarrow> nat"
   1.174 +where
   1.175 +  "f1_tl N = 0" |
   1.176 +  "f1_tl (C t ts) = f1_t t + f1_tl ts" |
   1.177 +  "f1_t (T n _ ts) = n + f1_tl ts"
   1.178 +
   1.179 +(* should be fast *)
   1.180 +primrec
   1.181 +  f2_t :: "(nat, 'b) t \<Rightarrow> nat" and
   1.182 +  f2_tl :: "(nat, 'b) t l \<Rightarrow> nat"
   1.183 +where
   1.184 +  "f2_tl N = 0" |
   1.185 +  "f2_tl (C t ts) = f2_t t + f2_tl ts" |
   1.186 +  "f2_t (T n _ ts) = n + f2_tl ts"
   1.187 +
   1.188 +end
   1.189 +
   1.190 +(* should be fast *)
   1.191 +primrec
   1.192 +  g1_t :: "('a, int) t \<Rightarrow> nat" and
   1.193 +  g1_tl :: "('a, int) t l \<Rightarrow> nat"
   1.194 +where
   1.195 +  "g1_t (T _ _ ts) = g1_tl ts" |
   1.196 +  "g1_tl N = 0" |
   1.197 +  "g1_tl (C _ ts) = g1_tl ts"
   1.198 +
   1.199 +(* should be fast *)
   1.200 +primrec
   1.201 +  g2_t :: "(int, int) t \<Rightarrow> nat" and
   1.202 +  g2_tl :: "(int, int) t l \<Rightarrow> nat"
   1.203 +where
   1.204 +  "g2_t (T _ _ ts) = g2_tl ts" |
   1.205 +  "g2_tl N = 0" |
   1.206 +  "g2_tl (C _ ts) = g2_tl ts"
   1.207 +
   1.208 +
   1.209 +datatype
   1.210 +  'a l1 = N1 | C1 'a "'a l2" and
   1.211 +  'a l2 = N2 | C2 'a "'a l1"
   1.212 +
   1.213 +primrec
   1.214 +  sum_l1 :: "'a::{zero,plus} l1 \<Rightarrow> 'a" and
   1.215 +  sum_l2 :: "'a::{zero,plus} l2 \<Rightarrow> 'a"
   1.216 +where
   1.217 +  "sum_l1 N1 = 0" |
   1.218 +  "sum_l1 (C1 n ns) = n + sum_l2 ns" |
   1.219 +  "sum_l2 N2 = 0" |
   1.220 +  "sum_l2 (C2 n ns) = n + sum_l1 ns"
   1.221 +
   1.222 +datatype
   1.223 +  ('a, 'b) t1 = T1 'a 'b "('a, 'b) t1 l1" and
   1.224 +  ('a, 'b) t2 = T2 "('a, 'b) t1"
   1.225 +
   1.226 +(* slow *)
   1.227 +primrec
   1.228 +  h1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
   1.229 +  h1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
   1.230 +  h1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat"
   1.231 +where
   1.232 +  "h1_tl1 N1 = 0" |
   1.233 +  "h1_tl1 (C1 t ts) = h1_t1 t + h1_tl2 ts" |
   1.234 +  "h1_tl2 N2 = 0" |
   1.235 +  "h1_tl2 (C2 t ts) = h1_t1 t + h1_tl1 ts" |
   1.236 +  "h1_t1 (T1 n _ ts) = n + h1_tl1 ts"
   1.237 +
   1.238 +(* should be fast *)
   1.239 +primrec
   1.240 +  h2_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
   1.241 +  h2_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
   1.242 +  h2_t1 :: "(nat, 'a) t1 \<Rightarrow> nat"
   1.243 +where
   1.244 +  "h2_tl1 N1 = 0" |
   1.245 +  "h2_tl1 (C1 t ts) = h2_t1 t + h2_tl2 ts" |
   1.246 +  "h2_tl2 N2 = 0" |
   1.247 +  "h2_tl2 (C2 t ts) = h2_t1 t + h2_tl1 ts" |
   1.248 +  "h2_t1 (T1 n _ ts) = n + h2_tl1 ts"
   1.249 +
   1.250 +(* should be fast *)
   1.251 +primrec
   1.252 +  h3_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
   1.253 +  h3_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
   1.254 +  h3_t1 :: "(nat, 'a) t1 \<Rightarrow> nat"
   1.255 +where
   1.256 +  "h3_tl1 N1 = 0" |
   1.257 +  "h3_tl1 (C1 t ts) = h3_t1 t + h3_tl2 ts" |
   1.258 +  "h3_tl2 N2 = 0" |
   1.259 +  "h3_tl2 (C2 t ts) = h3_t1 t + h3_tl1 ts" |
   1.260 +  "h3_t1 (T1 n _ ts) = n + h3_tl1 ts"
   1.261 +
   1.262 +(* should be fast *)
   1.263 +primrec
   1.264 +  i1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
   1.265 +  i1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
   1.266 +  i1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat" and
   1.267 +  i1_t2 :: "(nat, 'a) t2 \<Rightarrow> nat"
   1.268 +where
   1.269 +  "i1_tl1 N1 = 0" |
   1.270 +  "i1_tl1 (C1 t ts) = i1_t1 t + i1_tl2 ts" |
   1.271 +  "i1_tl2 N2 = 0" |
   1.272 +  "i1_tl2 (C2 t ts) = i1_t1 t + i1_tl1 ts" |
   1.273 +  "i1_t1 (T1 n _ ts) = n + i1_tl1 ts" |
   1.274 +  "i1_t2 (T2 t) = i1_t1 t"
   1.275 +
   1.276 +(* should be fast *)
   1.277 +primrec
   1.278 +  j1_t2 :: "(nat, 'a) t2 \<Rightarrow> nat" and
   1.279 +  j1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat" and
   1.280 +  j1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
   1.281 +  j1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat"
   1.282 +where
   1.283 +  "j1_tl1 N1 = 0" |
   1.284 +  "j1_tl1 (C1 t ts) = j1_t1 t + j1_tl2 ts" |
   1.285 +  "j1_tl2 N2 = 0" |
   1.286 +  "j1_tl2 (C2 t ts) = j1_t1 t + j1_tl1 ts" |
   1.287 +  "j1_t1 (T1 n _ ts) = n + j1_tl1 ts" |
   1.288 +  "j1_t2 (T2 t) = j1_t1 t"
   1.289 +
   1.290 +
   1.291 +datatype 'a l3 = N3 | C3 'a "'a l3"
   1.292 +datatype 'a l4 = N4 | C4 'a "'a l4"
   1.293 +datatype ('a, 'b) t3 = T3 'a 'b "('a, 'b) t3 l3" "('a, 'b) t3 l4"
   1.294 +
   1.295 +(* slow *)
   1.296 +primrec
   1.297 +  k1_tl3 :: "(nat, 'a) t3 l3 \<Rightarrow> nat" and
   1.298 +  k1_tl4 :: "(nat, 'a) t3 l4 \<Rightarrow> nat" and
   1.299 +  k1_t3 :: "(nat, 'a) t3 \<Rightarrow> nat"
   1.300 +where
   1.301 +  "k1_tl3 N3 = 0" |
   1.302 +  "k1_tl3 (C3 t ts) = k1_t3 t + k1_tl3 ts" |
   1.303 +  "k1_tl4 N4 = 0" |
   1.304 +  "k1_tl4 (C4 t ts) = k1_t3 t + k1_tl4 ts" |
   1.305 +  "k1_t3 (T3 n _ ts us) = n + k1_tl3 ts + k1_tl4 us"
   1.306 +
   1.307 +(* should be fast *)
   1.308 +primrec
   1.309 +  k2_tl4 :: "(nat, int) t3 l4 \<Rightarrow> nat" and
   1.310 +  k2_tl3 :: "(nat, int) t3 l3 \<Rightarrow> nat" and
   1.311 +  k2_t3 :: "(nat, int) t3 \<Rightarrow> nat"
   1.312 +where
   1.313 +  "k2_tl4 N4 = 0" |
   1.314 +  "k2_tl4 (C4 t ts) = k2_t3 t + k2_tl4 ts" |
   1.315 +  "k2_tl3 N3 = 0" |
   1.316 +  "k2_tl3 (C3 t ts) = k2_t3 t + k2_tl3 ts" |
   1.317 +  "k2_t3 (T3 n _ ts us) = n + k2_tl3 ts + k2_tl4 us"
   1.318 +
   1.319 +
   1.320 +datatype ('a, 'b) l5 = N5 | C5 'a 'b "('a, 'b) l5"
   1.321 +datatype ('a, 'b) l6 = N6 | C6 'a 'b "('a, 'b) l6"
   1.322 +datatype ('a, 'b, 'c) t4 = T4 'a 'b "(('a, 'b, 'c) t4, 'b) l5" "(('a, 'b, 'c) t4, 'c) l6"
   1.323 +
   1.324 +(* slow *)
   1.325 +primrec
   1.326 +  l1_tl5 :: "((nat, 'a, 'b) t4, 'a) l5 \<Rightarrow> nat" and
   1.327 +  l1_tl6 :: "((nat, 'a, 'b) t4, 'b) l6 \<Rightarrow> nat" and
   1.328 +  l1_t4 :: "(nat, 'a, 'b) t4 \<Rightarrow> nat"
   1.329 +where
   1.330 +  "l1_tl5 N5 = 0" |
   1.331 +  "l1_tl5 (C5 t _ ts) = l1_t4 t + l1_tl5 ts" |
   1.332 +  "l1_tl6 N6 = 0" |
   1.333 +  "l1_tl6 (C6 t _ ts) = l1_t4 t + l1_tl6 ts" |
   1.334 +  "l1_t4 (T4 n _ ts us) = n + l1_tl5 ts + l1_tl6 us"
   1.335 +
   1.336 +
   1.337 +
   1.338 +section \<open>Primcorec Cache\<close>
   1.339 +
   1.340 +codatatype 'a col = N | C 'a "'a col"
   1.341 +codatatype ('a, 'b) cot = T 'a 'b "('a, 'b) cot col"
   1.342 +
   1.343 +context linorder
   1.344 +begin
   1.345 +
   1.346 +(* slow *)
   1.347 +primcorec
   1.348 +  f1_cotcol :: "nat \<Rightarrow> (nat, 'a) cot col" and
   1.349 +  f1_cot :: "nat \<Rightarrow> (nat, 'a) cot"
   1.350 +where
   1.351 +  "n = 0 \<Longrightarrow> f1_cotcol n = N" |
   1.352 +  "_ \<Longrightarrow> f1_cotcol n = C (f1_cot n) (f1_cotcol n)" |
   1.353 +  "f1_cot n = T n undefined (f1_cotcol n)"
   1.354 +
   1.355 +(* should be fast *)
   1.356 +primcorec
   1.357 +  f2_cotcol :: "nat \<Rightarrow> (nat, 'b) cot col" and
   1.358 +  f2_cot :: "nat \<Rightarrow> (nat, 'b) cot"
   1.359 +where
   1.360 +  "n = 0 \<Longrightarrow> f2_cotcol n = N" |
   1.361 +  "_ \<Longrightarrow> f2_cotcol n = C (f2_cot n) (f2_cotcol n)" |
   1.362 +  "f2_cot n = T n undefined (f2_cotcol n)"
   1.363 +
   1.364 +end
   1.365 +
   1.366 +(* should be fast *)
   1.367 +primcorec
   1.368 +  g1_cot :: "int \<Rightarrow> (int, 'a) cot" and
   1.369 +  g1_cotcol :: "int \<Rightarrow> (int, 'a) cot col"
   1.370 +where
   1.371 +  "g1_cot n = T n undefined (g1_cotcol n)" |
   1.372 +  "n = 0 \<Longrightarrow> g1_cotcol n = N" |
   1.373 +  "_ \<Longrightarrow> g1_cotcol n = C (g1_cot n) (g1_cotcol n)"
   1.374 +
   1.375 +(* should be fast *)
   1.376 +primcorec
   1.377 +  g2_cot :: "int \<Rightarrow> (int, int) cot" and
   1.378 +  g2_cotcol :: "int \<Rightarrow> (int, int) cot col"
   1.379 +where
   1.380 +  "g2_cot n = T n undefined (g2_cotcol n)" |
   1.381 +  "n = 0 \<Longrightarrow> g2_cotcol n = N" |
   1.382 +  "_ \<Longrightarrow> g2_cotcol n = C (g2_cot n) (g2_cotcol n)"
   1.383 +
   1.384 +
   1.385 +codatatype
   1.386 +  'a col1 = N1 | C1 'a "'a col2" and
   1.387 +  'a col2 = N2 | C2 'a "'a col1"
   1.388 +
   1.389 +codatatype
   1.390 +  ('a, 'b) cot1 = T1 'a 'b "('a, 'b) cot1 col1" and
   1.391 +  ('a, 'b) cot2 = T2 "('a, 'b) cot1"
   1.392 +
   1.393 +(* slow *)
   1.394 +primcorec
   1.395 +  h1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
   1.396 +  h1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
   1.397 +  h1_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1"
   1.398 +where
   1.399 +  "h1_cotcol1 n = C1 (h1_cot1 n) (h1_cotcol2 n)" |
   1.400 +  "h1_cotcol2 n = C2 (h1_cot1 n) (h1_cotcol1 n)" |
   1.401 +  "h1_cot1 n = T1 n undefined (h1_cotcol1 n)"
   1.402 +
   1.403 +(* should be fast *)
   1.404 +primcorec
   1.405 +  h2_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
   1.406 +  h2_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
   1.407 +  h2_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1"
   1.408 +where
   1.409 +  "h2_cotcol1 n = C1 (h2_cot1 n) (h2_cotcol2 n)" |
   1.410 +  "h2_cotcol2 n = C2 (h2_cot1 n) (h2_cotcol1 n)" |
   1.411 +  "h2_cot1 n = T1 n undefined (h2_cotcol1 n)"
   1.412 +
   1.413 +(* should be fast *)
   1.414 +primcorec
   1.415 +  h3_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
   1.416 +  h3_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
   1.417 +  h3_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1"
   1.418 +where
   1.419 +  "h3_cotcol1 n = C1 (h3_cot1 n) (h3_cotcol2 n)" |
   1.420 +  "h3_cotcol2 n = C2 (h3_cot1 n) (h3_cotcol1 n)" |
   1.421 +  "h3_cot1 n = T1 n undefined (h3_cotcol1 n)"
   1.422 +
   1.423 +(* should be fast *)
   1.424 +primcorec
   1.425 +  i1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
   1.426 +  i1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
   1.427 +  i1_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1" and
   1.428 +  i1_cot2 :: "nat \<Rightarrow> (nat, 'a) cot2"
   1.429 +where
   1.430 +  "i1_cotcol1 n = C1 (i1_cot1 n) (i1_cotcol2 n)" |
   1.431 +  "i1_cotcol2 n = C2 (i1_cot1 n) (i1_cotcol1 n)" |
   1.432 +  "i1_cot1 n = T1 n undefined (i1_cotcol1 n)" |
   1.433 +  "i1_cot2 n = T2 (i1_cot1 n)"
   1.434 +
   1.435 +(* should be fast *)
   1.436 +primcorec
   1.437 +  j1_cot2 :: "nat \<Rightarrow> (nat, 'a) cot2" and
   1.438 +  j1_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1" and
   1.439 +  j1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
   1.440 +  j1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2"
   1.441 +where
   1.442 +  "j1_cotcol1 n = C1 (j1_cot1 n) (j1_cotcol2 n)" |
   1.443 +  "j1_cotcol2 n = C2 (j1_cot1 n) (j1_cotcol1 n)" |
   1.444 +  "j1_cot1 n = T1 n undefined (j1_cotcol1 n)" |
   1.445 +  "j1_cot2 n = T2 (j1_cot1 n)"
   1.446 +
   1.447 +
   1.448 +codatatype 'a col3 = N3 | C3 'a "'a col3"
   1.449 +codatatype 'a col4 = N4 | C4 'a "'a col4"
   1.450 +codatatype ('a, 'b) cot3 = T3 'a 'b "('a, 'b) cot3 col3" "('a, 'b) cot3 col4"
   1.451 +
   1.452 +(* slow *)
   1.453 +primcorec
   1.454 +  k1_cotcol3 :: "nat \<Rightarrow> (nat, 'a) cot3 col3" and
   1.455 +  k1_cotcol4 :: "nat \<Rightarrow> (nat, 'a) cot3 col4" and
   1.456 +  k1_cot3 :: "nat \<Rightarrow> (nat, 'a) cot3"
   1.457 +where
   1.458 +  "k1_cotcol3 n = C3 (k1_cot3 n) (k1_cotcol3 n)" |
   1.459 +  "k1_cotcol4 n = C4 (k1_cot3 n) (k1_cotcol4 n)" |
   1.460 +  "k1_cot3 n = T3 n undefined (k1_cotcol3 n) (k1_cotcol4 n)"
   1.461 +
   1.462 +(* should be fast *)
   1.463 +primcorec
   1.464 +  k2_cotcol4 :: "nat \<Rightarrow> (nat, 'a) cot3 col4" and
   1.465 +  k2_cotcol3 :: "nat \<Rightarrow> (nat, 'a) cot3 col3" and
   1.466 +  k2_cot3 :: "nat \<Rightarrow> (nat, 'a) cot3"
   1.467 +where
   1.468 +  "k2_cotcol4 n = C4 (k2_cot3 n) (k2_cotcol4 n)" |
   1.469 +  "k2_cotcol3 n = C3 (k2_cot3 n) (k2_cotcol3 n)" |
   1.470 +  "k2_cot3 n = T3 n undefined (k2_cotcol3 n) (k2_cotcol4 n)"
   1.471 +
   1.472 +end
     2.1 --- a/src/HOL/ROOT	Fri Sep 19 08:26:03 2014 +0200
     2.2 +++ b/src/HOL/ROOT	Fri Sep 19 10:00:34 2014 +0200
     2.3 @@ -755,6 +755,7 @@
     2.4      Stream_Processor
     2.5      Misc_Codatatype
     2.6      Misc_Datatype
     2.7 +    Misc_N2M
     2.8      Misc_Primcorec
     2.9      Misc_Primrec
    2.10    theories [condition = ISABELLE_FULL_TEST, timing]