1(* Title: Benchmarks/Datatype_Benchmark/Misc_N2M.thy 2 Author: Dmitriy Traytel, TU Muenchen 3 Copyright 2014 4 5Miscellaneous tests for the nested-to-mutual reduction. 6*) 7 8section \<open>Miscellaneous Tests for the Nested-to-Mutual Reduction\<close> 9 10theory Misc_N2M 11imports "HOL-Library.BNF_Axiomatization" 12begin 13 14declare [[typedef_overloaded]] 15 16 17locale misc 18begin 19 20datatype 'a li = Ni | Co 'a "'a li" 21datatype 'a tr = Tr "'a \<Rightarrow> 'a tr li" 22 23primrec (nonexhaustive) 24 f_tl :: "'a \<Rightarrow> 'a tr li \<Rightarrow> nat" and 25 f_t :: "'a \<Rightarrow> 'a tr \<Rightarrow> nat" 26where 27 "f_tl _ Ni = 0" | 28 "f_t a (Tr ts) = 1 + f_tl a (ts a)" 29 30datatype ('a, 'b) l = N | C 'a 'b "('a, 'b) l" 31datatype ('a, 'b) t = T "(('a, 'b) t, 'a) l" "(('a, 'b) t, 'b) l" 32 33primrec (nonexhaustive) 34 f_tl2 :: "(('a, 'a) t, 'a) l \<Rightarrow> nat" and 35 f_t2 :: "('a, 'a) t \<Rightarrow> nat" 36where 37 "f_tl2 N = 0" | 38 "f_t2 (T ts us) = f_tl2 ts + f_tl2 us" 39 40primrec (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" 44where 45 "g_tla N = 0" | 46 "g_tlb N = 1" | 47 "g_t (T ts us) = g_tla ts + g_tlb us" 48 49 50datatype 51 'a l1 = N1 | C1 'a "'a l1" 52 53datatype 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 57primrec 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" 61where 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 68end 69 70 71bnf_axiomatization ('a, 'b) M0 [wits: "('a, 'b) M0"] 72bnf_axiomatization ('a, 'b) N0 [wits: "('a, 'b) N0"] 73bnf_axiomatization ('a, 'b) K0 [wits: "('a, 'b) K0"] 74bnf_axiomatization ('a, 'b) L0 [wits: "('a, 'b) L0"] 75bnf_axiomatization ('a, 'b, 'c) G0 [wits: "('a, 'b, 'c) G0"] 76 77locale (*co*)mplicated 78begin 79 80datatype 'a M = CM "('a, 'a M) M0" 81datatype 'a N = CN "('a N, 'a) N0" 82datatype ('a, 'b) K = CK "('a, ('a, 'b) L) K0" 83 and ('a, 'b) L = CL "('b, ('a, 'b) K) L0" 84datatype 'a G = CG "('a, ('a G, 'a G N) K, ('a G M, 'a G) L) G0" 85 86primrec 87 fG :: "'a G \<Rightarrow> 'a G" 88and fK :: "('a G, 'a G N) K \<Rightarrow> ('a G, 'a G N) K" 89and fL :: "('a G, 'a G N) L \<Rightarrow> ('a G, 'a G N) L" 90and 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)" 95thm fG_def fK_def fL_def fM_def fG.simps fK.simps fL.simps fM.simps 96 97end 98 99locale complicated 100begin 101 102codatatype 'a M = CM "('a, 'a M) M0" 103codatatype 'a N = CN "('a N, 'a) N0" 104codatatype ('a, 'b) K = CK "('a, ('a, 'b) L) K0" 105 and ('a, 'b) L = CL "('b, ('a, 'b) K) L0" 106codatatype 'a G = CG "('a, ('a G, 'a G N) K, ('a G M, 'a G) L) G0" 107 108primcorec 109 fG :: "'a G \<Rightarrow> 'a G" 110and fK :: "('a G, 'a G N) K \<Rightarrow> ('a G, 'a G N) K" 111and fL :: "('a G, 'a G N) L \<Rightarrow> ('a G, 'a G N) L" 112and 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))" 117thm fG_def fK_def fL_def fM_def fG.simps fK.simps fL.simps fM.simps 118 119end 120 121datatype ('a, 'b) F1 = F1 'a 'b 122datatype F2 = F2 "((unit, nat) F1, F2) F1" | F2' 123datatype 'a kk1 = K1 'a | K2 "'a kk2" and 'a kk2 = K3 "'a kk1" 124datatype 'a ll1 = L1 'a | L2 "'a ll2 kk2" and 'a ll2 = L3 "'a ll1" 125 126datatype_compat F1 127datatype_compat F2 128datatype_compat kk1 kk2 129datatype_compat ll1 ll2 130 131 132subsection \<open>Deep Nesting\<close> 133 134datatype 'a tree = Empty | Node 'a "'a tree list" 135datatype_compat tree 136 137datatype 'a ttree = TEmpty | TNode 'a "'a ttree list tree" 138datatype_compat ttree 139 140datatype 'a tttree = TEmpty | TNode 'a "'a tttree list ttree list tree" 141datatype_compat tttree 142(* 143datatype 'a ttttree = TEmpty | TNode 'a "'a ttttree list tttree list ttree list tree" 144datatype_compat ttttree 145*) 146 147datatype 'a F = F1 'a | F2 "'a F" 148datatype 'a G = G1 'a | G2 "'a G F" 149datatype H = H1 | H2 "H G" 150 151datatype_compat F 152datatype_compat G 153datatype_compat H 154 155 156subsection \<open>Primrec cache\<close> 157 158datatype 'a l = N | C 'a "'a l" 159datatype ('a, 'b) t = T 'a 'b "('a, 'b) t l" 160 161context linorder 162begin 163 164primrec 165 f1_tl :: "(nat, 'a) t l \<Rightarrow> nat" and 166 f1_t :: "(nat, 'a) t \<Rightarrow> nat" 167where 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 *) 173primrec 174 f2_t :: "(nat, 'b) t \<Rightarrow> nat" and 175 f2_tl :: "(nat, 'b) t l \<Rightarrow> nat" 176where 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 181end 182 183(* should hit cache *) 184primrec 185 g1_t :: "('a, int) t \<Rightarrow> nat" and 186 g1_tl :: "('a, int) t l \<Rightarrow> nat" 187where 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 *) 193primrec 194 g2_t :: "(int, int) t \<Rightarrow> nat" and 195 g2_tl :: "(int, int) t l \<Rightarrow> nat" 196where 197 "g2_t (T _ _ ts) = g2_tl ts" | 198 "g2_tl N = 0" | 199 "g2_tl (C _ ts) = g2_tl ts" 200 201 202datatype 203 'a l1 = N1 | C1 'a "'a l2" and 204 'a l2 = N2 | C2 'a "'a l1" 205 206primrec 207 sum_l1 :: "'a::{zero,plus} l1 \<Rightarrow> 'a" and 208 sum_l2 :: "'a::{zero,plus} l2 \<Rightarrow> 'a" 209where 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 215datatype 216 ('a, 'b) t1 = T1 'a 'b "('a, 'b) t1 l1" and 217 ('a, 'b) t2 = T2 "('a, 'b) t1" 218 219primrec 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" 223where 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 *) 231primrec 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" 235where 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 *) 243primrec 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" 247where 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 *) 255primrec 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" 260where 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 *) 269primrec 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" 274where 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 283datatype 'a l3 = N3 | C3 'a "'a l3" 284datatype 'a l4 = N4 | C4 'a "'a l4" 285datatype ('a, 'b) t3 = T3 'a 'b "('a, 'b) t3 l3" "('a, 'b) t3 l4" 286 287primrec 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" 291where 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 *) 299primrec 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" 303where 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 311datatype ('a, 'b) l5 = N5 | C5 'a 'b "('a, 'b) l5" 312datatype ('a, 'b) l6 = N6 | C6 'a 'b "('a, 'b) l6" 313datatype ('a, 'b, 'c) t4 = T4 'a 'b "(('a, 'b, 'c) t4, 'b) l5" "(('a, 'b, 'c) t4, 'c) l6" 314 315primrec 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" 319where 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 327subsection \<open>Primcorec Cache\<close> 328 329codatatype 'a col = N | C 'a "'a col" 330codatatype ('a, 'b) cot = T 'a 'b "('a, 'b) cot col" 331 332context linorder 333begin 334 335primcorec 336 f1_cotcol :: "nat \<Rightarrow> (nat, 'a) cot col" and 337 f1_cot :: "nat \<Rightarrow> (nat, 'a) cot" 338where 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 *) 344primcorec 345 f2_cotcol :: "nat \<Rightarrow> (nat, 'b) cot col" and 346 f2_cot :: "nat \<Rightarrow> (nat, 'b) cot" 347where 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 352end 353 354(* should hit cache *) 355primcorec 356 g1_cot :: "int \<Rightarrow> (int, 'a) cot" and 357 g1_cotcol :: "int \<Rightarrow> (int, 'a) cot col" 358where 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 *) 364primcorec 365 g2_cot :: "int \<Rightarrow> (int, int) cot" and 366 g2_cotcol :: "int \<Rightarrow> (int, int) cot col" 367where 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 373codatatype 374 'a col1 = N1 | C1 'a "'a col2" and 375 'a col2 = N2 | C2 'a "'a col1" 376 377codatatype 378 ('a, 'b) cot1 = T1 'a 'b "('a, 'b) cot1 col1" and 379 ('a, 'b) cot2 = T2 "('a, 'b) cot1" 380 381primcorec 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" 385where 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 *) 391primcorec 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" 395where 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 *) 401primcorec 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" 405where 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 *) 411primcorec 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" 416where 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 *) 423primcorec 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" 428where 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 435codatatype 'a col3 = N3 | C3 'a "'a col3" 436codatatype 'a col4 = N4 | C4 'a "'a col4" 437codatatype ('a, 'b) cot3 = T3 'a 'b "('a, 'b) cot3 col3" "('a, 'b) cot3 col4" 438 439primcorec 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" 443where 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 *) 449primcorec 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" 453where 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 458datatype ('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" 461and ('a,'b)complex2 = D1 "('a,'b)complex ttree" 462datatype_compat complex complex2 463 464end 465