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" ### 19.024s elapsed time, 102.364s cpu time, 14.532s 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: 10150 ms ### Normalization & sealing of BNFs: 913 ms ### Extracted terms & thms: 9 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 5 ms ### Algebra definition & thms: 12 ms ### Proved nonemptiness: 0 ms ### Morphism definition & thms: 215 ms ### Bounds: 1 ms ### min_algs definition & thms: 13 ms ### Minimal algebra definition & thms: 18 ms ### Initiality definition & thms: 133 ms ### THE TYPEDEFs & Rep/Abs thms: 84 ms ### ctor definitions & thms: 13 ms ### fold definitions & thms: 13 ms ### dtor definitions & thms: 11 ms ### induction: 1 ms ### bnf constants for the new datatypes: 186 ms ### map functions for the new datatypes: 2 ms ### set functions for the new datatypes: 21 ms ### helpers for BNF properties: 28 ms ### registered new datatypes as BNFs: 238 ms ### relator induction: 6 ms ### recursor: 55 ms ### FP construction in total: 1074 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 9770 ms ### Construction of BNFs: 4495 ms ### Normalization & sealing of BNFs: 489 ms ### Extracted terms & thms: 2 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 4 ms ### Algebra definition & thms: 22 ms ### Proved nonemptiness: 0 ms ### Morphism definition & thms: 24 ms ### Bounds: 1 ms ### min_algs definition & thms: 13 ms ### Minimal algebra definition & thms: 20 ms ### Initiality definition & thms: 97 ms ### THE TYPEDEFs & Rep/Abs thms: 58 ms ### ctor definitions & thms: 9 ms ### fold definitions & thms: 10 ms ### dtor definitions & thms: 9 ms ### induction: 1 ms ### bnf constants for the new datatypes: 115 ms ### map functions for the new datatypes: 1 ms ### set functions for the new datatypes: 4 ms ### helpers for BNF properties: 7 ms ### registered new datatypes as BNFs: 94 ms ### relator induction: 3 ms ### recursor: 26 ms ### FP construction in total: 530 ms class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" ### Constructors, discriminators, selectors, etc., for the new datatype: 7178 ms Found termination order: "{}" ### theory "HOL-Datatype_Benchmark.Misc_N2M" ### 99.670s elapsed time, 375.424s cpu time, 33.032s GC time Found termination order: "{}" Found termination order: "{}" ### Construction of BNFs: 19334 ms ### Normalization & sealing of BNFs: 3462 ms ### Extracted terms & thms: 38 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 26 ms ### Algebra definition & thms: 34 ms ### Proved nonemptiness: 3 ms ### Morphism definition & thms: 67 ms ### Bounds: 399 ms ### min_algs definition & thms: 383 ms ### Minimal algebra definition & thms: 233 ms ### Initiality definition & thms: 765 ms ### THE TYPEDEFs & Rep/Abs thms: 819 ms ### ctor definitions & thms: 117 ms ### fold definitions & thms: 161 ms ### dtor definitions & thms: 166 ms ### induction: 13 ms ### bnf constants for the new datatypes: 1110 ms ### map functions for the new datatypes: 11 ms ### set functions for the new datatypes: 41 ms ### helpers for BNF properties: 24 ms ### registered new datatypes as BNFs: 410 ms ### relator induction: 60 ms ### recursor: 472 ms ### FP construction in total: 5363 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 33717 ms ### Construction of BNFs: 42164 ms ### Normalization & sealing of BNFs: 4156 ms ### Extracted terms & thms: 24 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 19 ms ### Algebra definition & thms: 172 ms ### Proved nonemptiness: 2 ms ### Morphism definition & thms: 72 ms ### Bounds: 320 ms ### min_algs definition & thms: 169 ms ### Minimal algebra definition & thms: 170 ms ### Initiality definition & thms: 616 ms ### THE TYPEDEFs & Rep/Abs thms: 568 ms ### ctor definitions & thms: 106 ms ### fold definitions & thms: 124 ms ### dtor definitions & thms: 124 ms ### induction: 8 ms ### bnf constants for the new datatypes: 1089 ms ### map functions for the new datatypes: 8 ms ### set functions for the new datatypes: 26 ms ### helpers for BNF properties: 17 ms ### registered new datatypes as BNFs: 237 ms ### relator induction: 30 ms ### recursor: 392 ms ### FP construction in total: 4303 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 200529 ms ### theory "HOL-Datatype_Benchmark.IsaFoR" ### 414.033s elapsed time, 1205.684s cpu time, 351.020s 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")