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" ### 17.434s elapsed time, 94.924s cpu time, 12.928s 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: 9994 ms ### Normalization & sealing of BNFs: 1122 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: 17 ms ### Bounds: 1 ms ### min_algs definition & thms: 12 ms ### Minimal algebra definition & thms: 17 ms ### Initiality definition & thms: 128 ms ### THE TYPEDEFs & Rep/Abs thms: 200 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: 201 ms ### map functions for the new datatypes: 2 ms ### set functions for the new datatypes: 11 ms ### helpers for BNF properties: 15 ms ### registered new datatypes as BNFs: 196 ms ### relator induction: 5 ms ### recursor: 36 ms ### FP construction in total: 915 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 10138 ms ### Construction of BNFs: 4616 ms ### Normalization & sealing of BNFs: 490 ms ### Extracted terms & thms: 2 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 4 ms ### Algebra definition & thms: 21 ms ### Proved nonemptiness: 0 ms ### Morphism definition & thms: 23 ms ### Bounds: 1 ms ### min_algs definition & thms: 12 ms ### Minimal algebra definition & thms: 20 ms ### Initiality definition & thms: 93 ms ### THE TYPEDEFs & Rep/Abs thms: 56 ms ### ctor definitions & thms: 9 ms ### fold definitions & thms: 10 ms ### dtor definitions & thms: 9 ms ### induction: 0 ms ### bnf constants for the new datatypes: 63 ms ### map functions for the new datatypes: 1 ms ### set functions for the new datatypes: 3 ms ### helpers for BNF properties: 8 ms ### registered new datatypes as BNFs: 82 ms ### relator induction: 3 ms ### recursor: 26 ms ### FP construction in total: 455 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 7495 ms Found termination order: "{}" Found termination order: "{}" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" Found termination order: "{}" ### theory "HOL-Datatype_Benchmark.Misc_N2M" ### 101.324s elapsed time, 376.980s cpu time, 34.868s GC time ### Construction of BNFs: 20309 ms ### Normalization & sealing of BNFs: 4107 ms ### Extracted terms & thms: 43 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 28 ms ### Algebra definition & thms: 37 ms ### Proved nonemptiness: 3 ms ### Morphism definition & thms: 74 ms ### Bounds: 467 ms ### min_algs definition & thms: 523 ms ### Minimal algebra definition & thms: 332 ms ### Initiality definition & thms: 1008 ms ### THE TYPEDEFs & Rep/Abs thms: 920 ms ### ctor definitions & thms: 116 ms ### fold definitions & thms: 153 ms ### dtor definitions & thms: 2924 ms ### induction: 35 ms ### bnf constants for the new datatypes: 1361 ms ### map functions for the new datatypes: 18 ms ### set functions for the new datatypes: 62 ms ### helpers for BNF properties: 81 ms ### registered new datatypes as BNFs: 341 ms ### relator induction: 85 ms ### recursor: 665 ms ### FP construction in total: 9288 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 35331 ms ### Construction of BNFs: 33309 ms ### Normalization & sealing of BNFs: 4218 ms ### Extracted terms & thms: 26 ms ### Checked nonemptiness: 0 ms ### Derived simple theorems: 20 ms ### Algebra definition & thms: 37 ms ### Proved nonemptiness: 2 ms ### Morphism definition & thms: 57 ms ### Bounds: 308 ms ### min_algs definition & thms: 166 ms ### Minimal algebra definition & thms: 159 ms ### Initiality definition & thms: 527 ms ### THE TYPEDEFs & Rep/Abs thms: 678 ms ### ctor definitions & thms: 97 ms ### fold definitions & thms: 116 ms ### dtor definitions & thms: 143 ms ### induction: 8 ms ### bnf constants for the new datatypes: 945 ms ### map functions for the new datatypes: 7 ms ### set functions for the new datatypes: 27 ms ### helpers for BNF properties: 32 ms ### registered new datatypes as BNFs: 365 ms ### relator induction: 31 ms ### recursor: 299 ms ### FP construction in total: 4059 ms ### Constructors, discriminators, selectors, etc., for the new datatype: 199121 ms ### theory "HOL-Datatype_Benchmark.IsaFoR" ### 409.480s elapsed time, 1202.740s cpu time, 349.276s 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")