Loading theory "HOL-Datatype_Benchmark.Brackin" Loading theory "HOL-Datatype_Benchmark.Misc_N2M" Loading theory "HOL-Datatype_Benchmark.IsaFoR" locale misc consts f_tl :: "'a \ 'a tr li \ nat" f_t :: "'a \ 'a tr \ nat" consts f_tl2 :: "(('a, 'a) t, 'a) l \ nat" f_t2 :: "('a, 'a) t \ nat" consts g_tla :: "(('a, 'b) t, 'a) l \ nat" g_tlb :: "(('a, 'b) t, 'b) l \ nat" g_t :: "('a, 'b) t \ nat" ### Defined types not fully mutually recursive ### Alternative specification: ### datatype t1 = \ ### datatype t2 = \ consts h1_tl1 :: "(nat, 'a) t1 l1 \ nat" h1_natl1 :: "(nat \ (nat, 'a) t1) l1 \ nat" h1_t1 :: "(nat, 'a) t1 \ nat" locale mplicated consts fG :: "'a G \ 'a G" fK :: "('a G, 'a G N) K \ ('a G, 'a G N) K" fL :: "('a G, 'a G N) L \ ('a G, 'a G N) L" fM :: "'a G M \ 'a G M" locale complicated fG \ fG.rec_n2m_G (\x. CG (map_G0 id snd (map_L snd snd) x)) (\w. CM (map_M0 snd snd w)) (\y. CK (map_K0 snd snd y)) (\z. CL (map_L0 (map_N snd) snd z)) fK \ fK.rec_n2m_G_G_N_K (\x. CG (map_G0 id snd (map_L snd snd) x)) (\w. CM (map_M0 snd snd w)) (\y. CK (map_K0 snd snd y)) (\z. CL (map_L0 (map_N snd) snd z)) fL \ fL.rec_n2m_G_G_N_L (\x. CG (map_G0 id snd (map_L snd snd) x)) (\w. CM (map_M0 snd snd w)) (\y. CK (map_K0 snd snd y)) (\z. CL (map_L0 (map_N snd) snd z)) fM \ fM.rec_n2m_G_M (\x. CG (map_G0 id snd (map_L snd snd) x)) (\w. CM (map_M0 snd snd w)) (\y. CK (map_K0 snd snd y)) (\z. CL (map_L0 (map_N snd) snd z)) fG (CG ?x) = CG (map_G0 id fK (map_L fM fG) ?x) fK (CK ?y) = CK (map_K0 fG fL ?y) fL (CL ?z) = CL (map_L0 (map_N fG) fK ?z) fM (CM ?w) = CM (map_M0 fG fM ?w) ### theory "HOL-Datatype_Benchmark.Brackin" ### 21.773s elapsed time, 116.952s cpu time, 16.132s GC time consts fG :: "'a G \ 'a G" fK :: "('a G, 'a G N) K \ ('a G, 'a G N) K" fL :: "('a G, 'a G N) L \ ('a G, 'a G N) L" fM :: "'a G M \ 'a G M" fG \ fG.corec_n2m_G (\x. map_G0 id Inr (map_L Inr Inr) (un_CG x)) (\w. map_M0 Inr Inr (un_CM w)) (\y. map_K0 Inr Inr (un_CK y)) (\z. map_L0 (map_N Inr) Inr (un_CL z)) fK \ fK.corec_n2m_G_G_N_K (\x. map_G0 id Inr (map_L Inr Inr) (un_CG x)) (\w. map_M0 Inr Inr (un_CM w)) (\y. map_K0 Inr Inr (un_CK y)) (\z. map_L0 (map_N Inr) Inr (un_CL z)) fL \ fL.corec_n2m_G_G_N_L (\x. map_G0 id Inr (map_L Inr Inr) (un_CG x)) (\w. map_M0 Inr Inr (un_CM w)) (\y. map_K0 Inr Inr (un_CK y)) (\z. map_L0 (map_N Inr) Inr (un_CL z)) fM \ fM.corec_n2m_G_M (\x. map_G0 id Inr (map_L Inr Inr) (un_CG x)) (\w. map_M0 Inr Inr (un_CM w)) (\y. map_K0 Inr Inr (un_CK y)) (\z. map_L0 (map_N Inr) Inr (un_CL z)) un_CG (fG ?x) = map_G0 id fK (map_L fM fG) (un_CG ?x) un_CK (fK ?y) = map_K0 fG fL (un_CK ?y) un_CL (fL ?z) = map_L0 (map_N fG) fK (un_CL ?z) un_CM (fM ?w) = map_M0 fG fM (un_CM ?w) ### Construction of BNFs: 12407 ms ### Normalization & sealing of BNFs: 1277 ms ### Extracted terms & thms: 12 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 7 ms ### Algebra definition & thms: 18 ms ### Proved nonemptiness: 0 ms ### Morphism definition & thms: 24 ms ### Bounds: 1 ms ### min_algs definition & thms: 17 ms ### Minimal algebra definition & thms: 25 ms ### Initiality definition & thms: 186 ms ### THE TYPEDEFs & Rep/Abs thms: 170 ms ### ctor definitions & thms: 24 ms ### fold definitions & thms: 22 ms ### dtor definitions & thms: 31 ms ### induction: 2 ms ### bnf constants for the new datatypes: 335 ms ### map functions for the new datatypes: 3 ms ### set functions for the new datatypes: 21 ms ### helpers for BNF properties: 29 ms ### registered new datatypes as BNFs: 261 ms ### relator induction: 7 ms ### recursor: 53 ms ### FP construction in total: 1260 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 12386 ms ### Construction of BNFs: 5289 ms ### Normalization & sealing of BNFs: 623 ms ### Extracted terms & thms: 3 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 3 ms ### Algebra definition & thms: 13 ms ### Proved nonemptiness: 0 ms ### Morphism definition & thms: 16 ms ### Bounds: 1 ms ### min_algs definition & thms: 16 ms ### Minimal algebra definition & thms: 26 ms ### Initiality definition & thms: 121 ms ### THE TYPEDEFs & Rep/Abs thms: 73 ms ### ctor definitions & thms: 12 ms ### fold definitions & thms: 14 ms ### dtor definitions & thms: 22 ms ### induction: 1 ms ### bnf constants for the new datatypes: 121 ms ### map functions for the new datatypes: 1 ms ### set functions for the new datatypes: 4 ms ### helpers for BNF properties: 8 ms ### registered new datatypes as BNFs: 108 ms ### relator induction: 4 ms ### recursor: 38 ms ### FP construction in total: 614 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 8517 ms Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" ### theory "HOL-Datatype_Benchmark.Misc_N2M" ### 130.031s elapsed time, 476.620s cpu time, 46.384s GC time ### Construction of BNFs: 24153 ms ### Normalization & sealing of BNFs: 4699 ms ### Extracted terms & thms: 46 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 209 ms ### Algebra definition & thms: 46 ms ### Proved nonemptiness: 3 ms ### Morphism definition & thms: 77 ms ### Bounds: 474 ms ### min_algs definition & thms: 505 ms ### Minimal algebra definition & thms: 289 ms ### Initiality definition & thms: 926 ms ### THE TYPEDEFs & Rep/Abs thms: 908 ms ### ctor definitions & thms: 181 ms ### fold definitions & thms: 233 ms ### dtor definitions & thms: 411 ms ### induction: 13 ms ### bnf constants for the new datatypes: 1620 ms ### map functions for the new datatypes: 13 ms ### set functions for the new datatypes: 55 ms ### helpers for BNF properties: 39 ms ### registered new datatypes as BNFs: 386 ms ### relator induction: 60 ms ### recursor: 735 ms ### FP construction in total: 7242 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 41406 ms ### Construction of BNFs: 44126 ms ### Normalization & sealing of BNFs: 6599 ms ### Extracted terms & thms: 30 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 91 ms ### Algebra definition & thms: 64 ms ### Proved nonemptiness: 2 ms ### Morphism definition & thms: 76 ms ### Bounds: 525 ms ### min_algs definition & thms: 328 ms ### Minimal algebra definition & thms: 333 ms ### Initiality definition & thms: 942 ms ### THE TYPEDEFs & Rep/Abs thms: 1318 ms ### ctor definitions & thms: 261 ms ### fold definitions & thms: 231 ms ### dtor definitions & thms: 387 ms ### induction: 15 ms ### bnf constants for the new datatypes: 2403 ms ### map functions for the new datatypes: 12 ms ### set functions for the new datatypes: 118 ms ### helpers for BNF properties: 172 ms ### registered new datatypes as BNFs: 7067 ms ### relator induction: 58 ms ### recursor: 490 ms ### FP construction in total: 14934 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 252933 ms ### theory "HOL-Datatype_Benchmark.IsaFoR" ### 517.586s elapsed time, 1478.444s cpu time, 462.184s GC time *** Malformed global fact "Misc_N2M.linorder_class.f1_t.n2m_t_ctor_fold_dict" *** Illegal fixed variable: "s1" *** At command "primrec" (line 164 of "~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy")