Loading theory "HOL-Datatype_Benchmark.Brackin" Loading theory "HOL-Datatype_Benchmark.IsaFoR" Loading theory "HOL-Datatype_Benchmark.Misc_N2M" 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" ### 22.192s elapsed time, 119.516s cpu time, 19.564s 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: 11717 ms ### Normalization & sealing of BNFs: 1454 ms ### Extracted terms & thms: 11 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 12 ms ### Algebra definition & thms: 28 ms ### Proved nonemptiness: 0 ms ### Morphism definition & thms: 34 ms ### Bounds: 1 ms ### min_algs definition & thms: 21 ms ### Minimal algebra definition & thms: 27 ms ### Initiality definition & thms: 170 ms ### THE TYPEDEFs & Rep/Abs thms: 114 ms ### ctor definitions & thms: 18 ms ### fold definitions & thms: 18 ms ### dtor definitions & thms: 16 ms ### induction: 1 ms ### bnf constants for the new datatypes: 283 ms ### map functions for the new datatypes: 3 ms ### set functions for the new datatypes: 12 ms ### helpers for BNF properties: 26 ms ### registered new datatypes as BNFs: 227 ms ### relator induction: 6 ms ### recursor: 49 ms ### FP construction in total: 1086 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 12268 ms ### Construction of BNFs: 5527 ms ### Normalization & sealing of BNFs: 628 ms ### Extracted terms & thms: 3 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 4 ms ### Algebra definition & thms: 25 ms ### Proved nonemptiness: 0 ms ### Morphism definition & thms: 27 ms ### Bounds: 1 ms ### min_algs definition & thms: 13 ms ### Minimal algebra definition & thms: 23 ms ### Initiality definition & thms: 120 ms ### THE TYPEDEFs & Rep/Abs thms: 83 ms ### ctor definitions & thms: 14 ms ### fold definitions & thms: 15 ms ### dtor definitions & thms: 13 ms ### induction: 0 ms ### bnf constants for the new datatypes: 101 ms ### map functions for the new datatypes: 1 ms ### set functions for the new datatypes: 4 ms ### helpers for BNF properties: 9 ms ### registered new datatypes as BNFs: 83 ms ### relator induction: 3 ms ### recursor: 27 ms ### FP construction in total: 581 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 8834 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" ### 129.580s elapsed time, 476.932s cpu time, 43.616s GC time ### Construction of BNFs: 23822 ms ### Normalization & sealing of BNFs: 5078 ms ### Extracted terms & thms: 48 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 35 ms ### Algebra definition & thms: 50 ms ### Proved nonemptiness: 3 ms ### Morphism definition & thms: 97 ms ### Bounds: 813 ms ### min_algs definition & thms: 571 ms ### Minimal algebra definition & thms: 327 ms ### Initiality definition & thms: 1021 ms ### THE TYPEDEFs & Rep/Abs thms: 1029 ms ### ctor definitions & thms: 197 ms ### fold definitions & thms: 253 ms ### dtor definitions & thms: 421 ms ### induction: 16 ms ### bnf constants for the new datatypes: 1634 ms ### map functions for the new datatypes: 13 ms ### set functions for the new datatypes: 47 ms ### helpers for BNF properties: 26 ms ### registered new datatypes as BNFs: 333 ms ### relator induction: 63 ms ### recursor: 688 ms ### FP construction in total: 7694 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 42095 ms ### Construction of BNFs: 55173 ms ### Normalization & sealing of BNFs: 6540 ms ### Extracted terms & thms: 35 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 25 ms ### Algebra definition & thms: 52 ms ### Proved nonemptiness: 2 ms ### Morphism definition & thms: 81 ms ### Bounds: 485 ms ### min_algs definition & thms: 364 ms ### Minimal algebra definition & thms: 227 ms ### Initiality definition & thms: 699 ms ### THE TYPEDEFs & Rep/Abs thms: 821 ms ### ctor definitions & thms: 170 ms ### fold definitions & thms: 187 ms ### dtor definitions & thms: 176 ms ### induction: 8 ms ### bnf constants for the new datatypes: 1518 ms ### map functions for the new datatypes: 11 ms ### set functions for the new datatypes: 209 ms ### helpers for BNF properties: 23 ms ### registered new datatypes as BNFs: 267 ms ### relator induction: 35 ms ### recursor: 393 ms ### FP construction in total: 5799 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 252690 ms ### theory "HOL-Datatype_Benchmark.IsaFoR" ### 520.167s elapsed time, 1480.580s cpu time, 457.708s 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")