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 ### theory "HOL-Datatype_Benchmark.Brackin" ### 20.637s elapsed time, 111.360s cpu time, 17.640s 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" 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) 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: 10609 ms ### Normalization & sealing of BNFs: 1022 ms ### Extracted terms & thms: 9 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 6 ms ### Algebra definition & thms: 232 ms ### Proved nonemptiness: 0 ms ### Morphism definition & thms: 20 ms ### Bounds: 1 ms ### min_algs definition & thms: 14 ms ### Minimal algebra definition & thms: 18 ms ### Initiality definition & thms: 138 ms ### THE TYPEDEFs & Rep/Abs thms: 89 ms ### ctor definitions & thms: 14 ms ### fold definitions & thms: 15 ms ### dtor definitions & thms: 31 ms ### induction: 3 ms ### bnf constants for the new datatypes: 240 ms ### map functions for the new datatypes: 2 ms ### set functions for the new datatypes: 20 ms ### helpers for BNF properties: 27 ms ### registered new datatypes as BNFs: 250 ms ### relator induction: 6 ms ### recursor: 66 ms ### FP construction in total: 1209 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 10785 ms ### Construction of BNFs: 4673 ms ### Normalization & sealing of BNFs: 527 ms ### Extracted terms & thms: 3 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 5 ms ### Algebra definition & thms: 22 ms ### Proved nonemptiness: 0 ms ### Morphism definition & thms: 24 ms ### Bounds: 1 ms ### min_algs definition & thms: 14 ms ### Minimal algebra definition & thms: 20 ms ### Initiality definition & thms: 99 ms ### THE TYPEDEFs & Rep/Abs thms: 62 ms ### ctor definitions & thms: 11 ms ### fold definitions & thms: 11 ms ### dtor definitions & thms: 9 ms ### induction: 0 ms ### bnf constants for the new datatypes: 66 ms ### map functions for the new datatypes: 1 ms ### set functions for the new datatypes: 3 ms ### helpers for BNF properties: 9 ms ### registered new datatypes as BNFs: 61 ms ### relator induction: 3 ms ### recursor: 22 ms ### FP construction in total: 456 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 7504 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" ### 117.516s elapsed time, 436.940s cpu time, 39.716s GC time ### Construction of BNFs: 21203 ms ### Normalization & sealing of BNFs: 3492 ms ### Extracted terms & thms: 38 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 26 ms ### Algebra definition & thms: 36 ms ### Proved nonemptiness: 3 ms ### Morphism definition & thms: 74 ms ### Bounds: 405 ms ### min_algs definition & thms: 371 ms ### Minimal algebra definition & thms: 234 ms ### Initiality definition & thms: 956 ms ### THE TYPEDEFs & Rep/Abs thms: 724 ms ### ctor definitions & thms: 130 ms ### fold definitions & thms: 173 ms ### dtor definitions & thms: 164 ms ### induction: 16 ms ### bnf constants for the new datatypes: 1323 ms ### map functions for the new datatypes: 11 ms ### set functions for the new datatypes: 48 ms ### helpers for BNF properties: 27 ms ### registered new datatypes as BNFs: 302 ms ### relator induction: 53 ms ### recursor: 471 ms ### FP construction in total: 5597 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 33832 ms ### Construction of BNFs: 41783 ms ### Normalization & sealing of BNFs: 4259 ms ### Extracted terms & thms: 24 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 18 ms ### Algebra definition & thms: 36 ms ### Proved nonemptiness: 1 ms ### Morphism definition & thms: 58 ms ### Bounds: 309 ms ### min_algs definition & thms: 159 ms ### Minimal algebra definition & thms: 157 ms ### Initiality definition & thms: 670 ms ### THE TYPEDEFs & Rep/Abs thms: 571 ms ### ctor definitions & thms: 104 ms ### fold definitions & thms: 129 ms ### dtor definitions & thms: 124 ms ### induction: 8 ms ### bnf constants for the new datatypes: 938 ms ### map functions for the new datatypes: 7 ms ### set functions for the new datatypes: 45 ms ### helpers for BNF properties: 28 ms ### registered new datatypes as BNFs: 342 ms ### relator induction: 31 ms ### recursor: 313 ms ### FP construction in total: 4084 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 203804 ms ### theory "HOL-Datatype_Benchmark.IsaFoR" ### 428.133s elapsed time, 1253.076s cpu time, 364.048s 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")