Loading theory "HOL-Library.Cancellation" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Library.Permutations" via "HOL-Library.Multiset") Loading theory "HOL-Library.Disjoint_Sets" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Library.Permutations") Loading theory "HOL-Library.FuncSet" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product") Loading theory "HOL-Library.Infinite_Set" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Affine" via "HOL-Analysis.Linear_Algebra") Loading theory "HOL-Library.Nat_Bijection" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product" via "HOL-Library.Countable_Set" via "HOL-Library.Countable") Loading theory "HOL-Library.Old_Datatype" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product" via "HOL-Library.Countable_Set" via "HOL-Library.Countable") Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "size_list size <*mlex*> {}" ### theory "HOL-Library.Disjoint_Sets" ### 0.430s elapsed time, 2.592s cpu time, 0.000s GC time Loading theory "HOL-Library.Phantom_Type" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product" via "HOL-Library.Numeral_Type" via "HOL-Library.Cardinality") ### theory "HOL-Library.Infinite_Set" ### 0.471s elapsed time, 2.824s cpu time, 0.000s GC time Loading theory "HOL-Library.Product_Plus" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Affine" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space" via "HOL-Analysis.Product_Vector") signature CANCEL = sig val proc: Proof.context -> cterm -> thm option end functor Cancel_Fun (Data: CANCEL_NUMERALS_DATA): CANCEL ### theory "HOL-Library.Nat_Bijection" ### 0.518s elapsed time, 3.116s cpu time, 0.000s GC time Loading theory "HOL-Library.Set_Algebras" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex") signature CANCEL_DATA = sig val dest_coeff: term -> int * term val dest_sum: term -> term list val find_first_coeff: term -> term list -> int * term list val mk_coeff: int * term -> term val mk_sum: typ -> term list -> term val norm_ss1: simpset val norm_ss2: simpset val norm_tac: Proof.context -> tactic val numeral_simp_tac: Proof.context -> tactic val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option val simplify_meta_eq: Proof.context -> thm -> thm val trans_tac: Proof.context -> thm option -> tactic end structure Cancel_Data: CANCEL_DATA ### theory "HOL-Library.Product_Plus" ### 0.148s elapsed time, 0.876s cpu time, 0.000s GC time Loading theory "HOL-Library.Product_Order" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Lebesgue_Measure" via "HOL-Analysis.Finite_Product_Measure" via "HOL-Analysis.Binary_Product_Measure" via "HOL-Analysis.Nonnegative_Lebesgue_Integration" via "HOL-Analysis.Borel_Space" via "HOL-Analysis.Ordered_Euclidean_Space") signature CANCEL_SIMPROCS = sig val diff_cancel: Proof.context -> cterm -> thm option val eq_cancel: Proof.context -> cterm -> thm option val less_cancel: Proof.context -> cterm -> thm option val less_eq_cancel: Proof.context -> cterm -> thm option end structure Cancel_Simprocs: CANCEL_SIMPROCS ### theory "HOL-Library.Cancellation" ### 0.814s elapsed time, 4.808s cpu time, 0.444s GC time Loading theory "HOL-Library.Multiset" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Library.Permutations") ### theory "HOL-Library.FuncSet" ### 0.807s elapsed time, 4.744s cpu time, 0.444s GC time Loading theory "HOL-Analysis.Metric_Arith" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Elementary_Normed_Spaces" via "HOL-Analysis.Elementary_Metric_Spaces") signature OLD_DATATYPE = sig val check_specs: spec list -> theory -> spec list * Proof.context type config = {quiet: bool, strict: bool} val default_config: config type descr = (int * (string * dtyp list * (string * dtyp list) list)) list val distinct_lemma: thm datatype dtyp = DtRec of int | DtTFree of string * sort | DtType of string * dtyp list type info = {case_cong: thm, case_cong_weak: thm, case_name: string, case_rewrites: thm list, descr: descr, distinct: thm list, exhaust: thm, index: int, induct: thm, inducts: thm list, inject: thm list, nchotomy: thm, rec_names: string list, rec_rewrites: thm list, split: thm, split_asm: thm} val read_specs: spec_cmd list -> theory -> spec list * Proof.context type spec = (binding * (string * sort) list * mixfix) * (binding * typ list * mixfix) list type spec_cmd = (binding * (string * string option) list * mixfix) * (binding * string list * mixfix) list end structure Old_Datatype: OLD_DATATYPE ### theory "HOL-Library.Old_Datatype" ### 0.822s elapsed time, 4.840s cpu time, 0.444s GC time Loading theory "HOL-Library.Countable" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product" via "HOL-Library.Countable_Set") ### theory "HOL-Library.Set_Algebras" ### 0.421s elapsed time, 2.440s cpu time, 0.444s GC time Loading theory "HOL-Analysis.Inner_Product" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Affine" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space") ### theory "HOL-Library.Product_Order" ### 0.320s elapsed time, 1.848s cpu time, 0.444s GC time Loading theory "HOL-Analysis.L2_Norm" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Affine" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space") ### theory "HOL-Analysis.L2_Norm" ### 0.108s elapsed time, 0.656s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Operator_Norm" (required by "HOL-Analysis.Analysis") ### theory "HOL-Analysis.Operator_Norm" ### 0.120s elapsed time, 0.716s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Poly_Roots" (required by "HOL-Analysis.Analysis") ### theory "HOL-Library.Phantom_Type" ### 0.771s elapsed time, 4.544s cpu time, 0.444s GC time Loading theory "HOL-Library.Cardinality" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product" via "HOL-Library.Numeral_Type") ### Additional type variable(s) in locale specification "CARD_1": 'a ### Additional type variable(s) in locale specification "countable": 'a ### theory "HOL-Analysis.Poly_Roots" ### 0.116s elapsed time, 0.708s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Product_Vector" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Affine" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space") ### Additional type variable(s) in locale specification "card2": 'a signature METRIC_ARITH = sig val metric_arith_tac: Proof.context -> int -> tactic val trace: bool Config.T end structure MetricArith: METRIC_ARITH ### Partially applied constant "Multiset.inf_subset_mset" on left hand side of equation, in theorem: ### semilattice_inf.Inf_fin (\#) (set (?x # ?xs)) \ fold (\#) ?xs ?x ### theory "HOL-Analysis.Metric_Arith" ### 0.681s elapsed time, 4.116s cpu time, 0.000s GC time Loading theory "HOL-Library.Discrete" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests") ### Partially applied constant "Multiset.sup_subset_mset" on left hand side of equation, in theorem: ### semilattice_sup.Sup_fin (\#) (set (?x # ?xs)) \ fold (\#) ?xs ?x Proofs for inductive predicate(s) "finite_item" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### Rewrite rule not in simpset: ### Wellfounded.accp log_rel ?n1 \ ### log ?n1 \ if ?n1 < 2 then 0 else Suc (log (?n1 div 2)) Found termination order: "size <*mlex*> {}" ### theory "HOL-Library.Discrete" ### 0.254s elapsed time, 1.492s cpu time, 0.000s GC time Loading theory "HOL-Library.Indicator_Function" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Connected" via "HOL-Analysis.Abstract_Topology_2") Found termination order: "(\p. size (fst p)) <*mlex*> {}" val old_countable_datatype_tac = fn: Proof.context -> int -> tactic ### ML warning (line 93 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Pattern is not exhaustive. ### ML warning (line 139 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Pattern is not exhaustive. ### ML warning (line 143 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Matches are not exhaustive. ### ML warning (line 145 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Matches are not exhaustive. ### ML warning (line 156 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Pattern is not exhaustive. signature BNF_LFP_COUNTABLE = sig val countable_datatype_tac: Proof.context -> tactic val derive_encode_injectives_thms: Proof.context -> string list -> thm list end structure BNF_LFP_Countable: BNF_LFP_COUNTABLE signature MULTISET_SIMPROCS = sig val subset_cancel_msets: Proof.context -> cterm -> thm option val subseteq_cancel_msets: Proof.context -> cterm -> thm option end structure Multiset_Simprocs: MULTISET_SIMPROCS val countable_datatype_tac = fn: Proof.context -> thm -> thm Seq.seq val countable_tac = fn: Proof.context -> int -> tactic ### Code generator: dropping subsumed code equation ### List.coset [] \ set [] \ False ### theory "HOL-Library.Indicator_Function" ### 0.703s elapsed time, 3.912s cpu time, 0.928s GC time Loading theory "HOL-Library.Liminf_Limsup" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests" via "HOL-Library.Extended_Real") ### theory "HOL-Analysis.Inner_Product" ### 1.525s elapsed time, 8.832s cpu time, 0.928s GC time Loading theory "HOL-Library.Nonpos_Ints" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Harmonic_Numbers" via "HOL-Analysis.Complex_Transcendental" via "HOL-Analysis.Complex_Analysis_Basics") ### theory "HOL-Library.Countable" ### 1.782s elapsed time, 10.388s cpu time, 0.928s GC time Loading theory "HOL-Library.Countable_Set" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product") ### theory "HOL-Library.Cardinality" ### 1.433s elapsed time, 8.284s cpu time, 0.928s GC time Loading theory "HOL-Library.Numeral_Type" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product") ### theory "HOL-Analysis.Product_Vector" ### 1.390s elapsed time, 8.020s cpu time, 0.928s GC time Loading theory "HOL-Analysis.Euclidean_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Affine" via "HOL-Analysis.Linear_Algebra") ### theory "HOL-Library.Nonpos_Ints" ### 0.232s elapsed time, 1.404s cpu time, 0.000s GC time Loading theory "HOL-Library.Periodic_Fun" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Harmonic_Numbers" via "HOL-Analysis.Complex_Transcendental") ### theory "HOL-Library.Periodic_Fun" ### 0.164s elapsed time, 0.992s cpu time, 0.000s GC time Loading theory "HOL-Library.Sum_of_Squares" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Norm_Arith") ### Rule already declared as safe introduction (intro!) ### True ### Ignoring duplicate introduction (intro) ### True ### theory "HOL-Library.Liminf_Limsup" ### 0.624s elapsed time, 3.788s cpu time, 0.000s GC time ### theory "HOL-Library.Countable_Set" ### 0.492s elapsed time, 2.992s cpu time, 0.000s GC time Loading theory "HOL-Library.Countable_Complete_Lattices" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests" via "HOL-Library.Extended_Real" via "HOL-Library.Extended_Nat" via "HOL-Library.Order_Continuity") Loading theory "HOL-Library.Set_Idioms" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Connected" via "HOL-Analysis.Abstract_Topology_2" via "HOL-Analysis.Elementary_Topology") ### theory "HOL-Library.Set_Idioms" ### 0.275s elapsed time, 1.656s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Abstract_Topology" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Connected" via "HOL-Analysis.Abstract_Topology_2") ### theory "HOL-Library.Numeral_Type" ### 0.830s elapsed time, 5.024s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Continuum_Not_Denumerable" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Homeomorphism" via "HOL-Analysis.Homotopy") ### theory "HOL-Analysis.Continuum_Not_Denumerable" ### 0.427s elapsed time, 2.480s cpu time, 0.676s GC time Loading theory "HOL-Analysis.Elementary_Topology" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Connected" via "HOL-Analysis.Abstract_Topology_2") Proofs for inductive predicate(s) "pw_leq" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "HOL-Analysis.Euclidean_Space" ### 2.131s elapsed time, 12.780s cpu time, 0.676s GC time Loading theory "HOL-Analysis.Finite_Cartesian_Product" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space") Found termination order: "(\p. length (fst p)) <*mlex*> {}" ### ML warning (line 379 of "~~/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML"): ### Pattern is not exhaustive. signature FUNC = sig exception DUP of key exception SAME exception UNDEF of key val apply: 'a table -> key -> 'a val applyd: 'a table -> (key -> 'a) -> key -> 'a val choose: 'a table -> key * 'a val combine: ('a -> 'a -> 'a) -> ('a -> bool) -> 'a table -> 'a table -> 'a table val cons_list: key * 'a -> 'a list table -> 'a list table val default: key * 'a -> 'a table -> 'a table val defined: 'a table -> key -> bool val delete: key -> 'a table -> 'a table val delete_safe: key -> 'a table -> 'a table val dest: 'a table -> (key * 'a) list val dest_list: 'a list table -> (key * 'a) list val dom: 'a table -> key list val empty: 'a table val exists: (key * 'a -> bool) -> 'a table -> bool val fold: (key * 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b val fold_rev: (key * 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b val forall: (key * 'a -> bool) -> 'a table -> bool val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table val insert_set: key -> set -> set val is_empty: 'a table -> bool val is_single: 'a table -> bool val join: (key -> 'a * 'a -> 'a) -> 'a table * 'a table -> 'a table type key val keys: 'a table -> key list val lookup: 'a table -> key -> 'a option val lookup_key: 'a table -> key -> (key * 'a) option val lookup_list: 'a list table -> key -> 'a list val make: (key * 'a) list -> 'a table val make_list: (key * 'a) list -> 'a list table val make_set: key list -> set val map: (key -> 'a -> 'b) -> 'a table -> 'b table val map_default: key * 'a -> ('a -> 'a) -> 'a table -> 'a table val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table val max: 'a table -> (key * 'a) option val member: ('a * 'b -> bool) -> 'b table -> key * 'a -> bool val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table val merge_list: ('a * 'a -> bool) -> 'a list table * 'a list table -> 'a list table val min: 'a table -> (key * 'a) option val onefunc: key * 'a -> 'a table val remove: ('a * 'b -> bool) -> key * 'a -> 'b table -> 'b table val remove_list: ('a * 'b -> bool) -> key * 'a -> 'b list table -> 'b list table val remove_set: key -> set -> set type set = unit table type 'a table val tryapplyd: 'a table -> key -> 'a -> 'a val update: key * 'a -> 'a table -> 'a table val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table val update_new: key * 'a -> 'a table -> 'a table val updatep: (key * 'a -> bool) -> key * 'a -> 'a table -> 'a table end functor FuncFun (Key: KEY): FUNC signature REAL_ARITH = sig type cert_conv = cterm -> thm * pss_tree val cterm_of_rat: Rat.rat -> cterm val dest_ratconst: cterm -> Rat.rat val gen_gen_real_arith: Proof.context -> (Rat.rat -> cterm) * conv * conv * conv * conv * conv * conv * conv * conv * conv * prover -> cert_conv val gen_prover_real_arith: Proof.context -> prover -> cert_conv val gen_real_arith: Proof.context -> (Rat.rat -> cterm) * conv * conv * conv * conv * conv * conv * conv * prover -> cert_conv val is_ratconst: cterm -> bool datatype positivstellensatz = Axiom_eq of int | Axiom_le of int | Axiom_lt of int | Eqmul of FuncUtil.poly * positivstellensatz | Product of positivstellensatz * positivstellensatz | Rational_eq of Rat.rat | Rational_le of Rat.rat | Rational_lt of Rat.rat | Square of FuncUtil.poly | Sum of positivstellensatz * positivstellensatz type prover = tree_choice list -> (thm list * thm list * thm list -> positivstellensatz -> thm) -> thm list * thm list * thm list -> thm * pss_tree datatype pss_tree = Branch of pss_tree * pss_tree | Cert of positivstellensatz | Trivial val real_linear_prover: (thm list * thm list * thm list -> positivstellensatz -> thm) -> thm list * thm list * thm list -> thm * pss_tree datatype tree_choice = Left | Right end structure FuncUtil: sig structure Ctermfunc: FUNC structure Intfunc: FUNC structure Intpairfunc: FUNC structure Monomialfunc: FUNC structure Ratfunc: FUNC structure Symfunc: FUNC structure Termfunc: FUNC val dest_monomial: 'a Ctermfunc.table -> (cterm * 'a) list type monomial = int Ctermfunc.table val monomial_ord: int Ctermfunc.table * int Ctermfunc.table -> order val monomial_order: int Ctermfunc.table * int Ctermfunc.table -> order type poly = Rat.rat Monomialfunc.table end structure RealArith: REAL_ARITH Proofs for inductive predicate(s) "pred_mset" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "HOL-Library.Countable_Complete_Lattices" ### 2.620s elapsed time, 15.584s cpu time, 1.332s GC time Loading theory "HOL-Analysis.Linear_Algebra" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Affine") signature POSITIVSTELLENSATZ_TOOLS = sig val print_cert: RealArith.pss_tree -> string val read_cert: Proof.context -> string -> RealArith.pss_tree end structure Positivstellensatz_Tools: POSITIVSTELLENSATZ_TOOLS Proofs for inductive predicate(s) "rel_mset'" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "HOL-Library.Multiset" ### 4.983s elapsed time, 29.500s cpu time, 2.260s GC time Loading theory "HOL-Computational_Algebra.Factorial_Ring" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Jordan_Curve" via "HOL-Analysis.Arcwise_Connected" via "HOL-Computational_Algebra.Primes" via "HOL-Computational_Algebra.Euclidean_Algorithm") signature SUM_OF_SQUARES = sig exception Failure of string val debug: bool Config.T val debug_message: Proof.context -> (unit -> string) -> unit datatype proof_method = Certificate of RealArith.pss_tree | Prover of string -> string val sos_tac: (RealArith.pss_tree -> unit) -> proof_method -> Proof.context -> int -> tactic val trace: bool Config.T val trace_message: Proof.context -> (unit -> string) -> unit end structure Sum_of_Squares: SUM_OF_SQUARES ### theory "HOL-Analysis.Elementary_Topology" ### 2.434s elapsed time, 14.452s cpu time, 1.272s GC time Loading theory "HOL-Library.Permutations" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants") signature SOS_WRAPPER = sig val sos_tac: Proof.context -> string option -> int -> tactic end structure SOS_Wrapper: SOS_WRAPPER ### theory "HOL-Library.Sum_of_Squares" ### 3.506s elapsed time, 20.828s cpu time, 1.948s GC time Loading theory "HOL-Library.Order_Continuity" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests" via "HOL-Library.Extended_Real" via "HOL-Library.Extended_Nat") Proofs for inductive predicate(s) "swapidseq" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "generate_topology_on" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "HOL-Analysis.Abstract_Topology" ### 3.551s elapsed time, 21.120s cpu time, 1.948s GC time Loading theory "HOL-Analysis.Abstract_Limits" (required by "HOL-Analysis.Analysis") ### theory "HOL-Analysis.Finite_Cartesian_Product" ### 2.073s elapsed time, 12.424s cpu time, 0.616s GC time Loading theory "HOL-Analysis.Abstract_Topology_2" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Connected") ### theory "HOL-Analysis.Linear_Algebra" ### 1.317s elapsed time, 7.860s cpu time, 0.616s GC time Loading theory "HOL-Analysis.Affine" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex") ### theory "HOL-Library.Order_Continuity" ### 0.691s elapsed time, 4.192s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Cartesian_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants") Found termination order: "(\p. size_list size (fst p)) <*mlex*> {}" ### theory "HOL-Library.Permutations" ### 2.099s elapsed time, 10.644s cpu time, 5.108s GC time Loading theory "HOL-Library.Extended_Nat" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests" via "HOL-Library.Extended_Real") ### theory "HOL-Analysis.Abstract_Limits" ### 1.518s elapsed time, 7.116s cpu time, 5.108s GC time Loading theory "HOL-Analysis.Norm_Arith" (required by "HOL-Analysis.Analysis") Proofs for inductive predicate(s) "rec_set_enat" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the simplification rules ... ### theory "HOL-Analysis.Affine" ### 1.841s elapsed time, 8.996s cpu time, 5.108s GC time Loading theory "HOL-Analysis.Convex" (required by "HOL-Analysis.Analysis") ### No equation for constructor "Extended_Nat.infinity_class.infinity" ### in definition of function "the_enat" ### ML warning (line 103 of "~~/src/HOL/Analysis/normarith.ML"): ### Matches are not exhaustive. ### ML warning (line 347 of "~~/src/HOL/Analysis/normarith.ML"): ### Value identifier (instantiate_cterm') has not been referenced. signature NORM_ARITH = sig val norm_arith: Proof.context -> conv val norm_arith_tac: Proof.context -> int -> tactic end structure NormArith: NORM_ARITH ### theory "HOL-Analysis.Norm_Arith" ### 0.584s elapsed time, 3.428s cpu time, 0.408s GC time structure Cancel_Enat_Common: sig val dest_sum: term -> term list val dest_summing: term * term list -> term list val find_first: term -> term list -> term list val find_first_t: term list -> term -> term list -> term list val mk_eq: term * term -> term val mk_sum: typ -> term list -> term val norm_ss: simpset val norm_tac: Proof.context -> tactic val simplify_meta_eq: Proof.context -> thm -> thm -> thm val trans_tac: Proof.context -> thm option -> tactic end structure Eq_Enat_Cancel: sig val proc: Proof.context -> term -> thm option end structure Le_Enat_Cancel: sig val proc: Proof.context -> term -> thm option end structure Less_Enat_Cancel: sig val proc: Proof.context -> term -> thm option end ### theory "HOL-Library.Extended_Nat" ### 1.000s elapsed time, 5.936s cpu time, 0.408s GC time Loading theory "HOL-Library.Extended_Real" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests") ### theory "HOL-Analysis.Cartesian_Space" ### 2.664s elapsed time, 13.884s cpu time, 5.516s GC time Loading theory "HOL-Analysis.Determinants" (required by "HOL-Analysis.Analysis") ### theory "HOL-Analysis.Abstract_Topology_2" ### 3.138s elapsed time, 16.672s cpu time, 5.516s GC time Loading theory "HOL-Analysis.Connected" (required by "HOL-Analysis.Analysis") Loading theory "HOL-Analysis.Elementary_Metric_Spaces" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Elementary_Normed_Spaces") ### theory "HOL-Analysis.Convex" ### 1.499s elapsed time, 8.888s cpu time, 0.648s GC time ### theory "HOL-Analysis.Connected" ### 0.474s elapsed time, 2.828s cpu time, 0.648s GC time Loading theory "HOL-Analysis.Function_Topology" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function") Found termination order: "{}" ### theory "HOL-Analysis.Determinants" ### 1.056s elapsed time, 6.276s cpu time, 0.648s GC time ### theory "HOL-Analysis.Function_Topology" ### 0.866s elapsed time, 5.244s cpu time, 0.656s GC time Loading theory "HOL-Analysis.Product_Topology" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Weierstrass_Theorems" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.T1_Spaces") ### theory "HOL-Analysis.Product_Topology" ### 0.331s elapsed time, 2.020s cpu time, 0.000s GC time Loading theory "HOL-Analysis.T1_Spaces" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Weierstrass_Theorems" via "HOL-Analysis.Path_Connected") ### theory "HOL-Analysis.T1_Spaces" ### 0.332s elapsed time, 2.024s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Lindelof_Spaces" (required by "HOL-Analysis.Analysis") ### theory "HOL-Analysis.Lindelof_Spaces" ### 0.120s elapsed time, 0.728s cpu time, 0.000s GC time ### theory "HOL-Analysis.Elementary_Metric_Spaces" ### 2.335s elapsed time, 14.140s cpu time, 1.172s GC time Loading theory "HOL-Analysis.Elementary_Normed_Spaces" (required by "HOL-Analysis.Analysis") Loading theory "HOL-Analysis.Function_Metric" (required by "HOL-Analysis.Analysis") ### theory "HOL-Analysis.Function_Metric" ### 0.384s elapsed time, 2.348s cpu time, 0.000s GC time ### theory "HOL-Library.Extended_Real" ### 3.697s elapsed time, 22.240s cpu time, 1.820s GC time Loading theory "HOL-Library.Extended_Nonnegative_Real" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests" via "HOL-Analysis.Extended_Real_Limits") structure Cancel_Ennreal_Common: sig val dest_sum: term -> term list val dest_summing: term * term list -> term list val find_first: term -> term list -> term list val find_first_t: term list -> term -> term list -> term list val mk_eq: term * term -> term val mk_sum: typ -> term list -> term val norm_ss: simpset val norm_tac: Proof.context -> tactic val simplify_meta_eq: Proof.context -> thm -> thm -> thm val trans_tac: Proof.context -> thm option -> tactic end structure Eq_Ennreal_Cancel: sig val proc: Proof.context -> term -> thm option end structure Le_Ennreal_Cancel: sig val proc: Proof.context -> term -> thm option end structure Less_Ennreal_Cancel: sig val proc: Proof.context -> term -> thm option end ### theory "HOL-Analysis.Elementary_Normed_Spaces" ### 1.607s elapsed time, 9.688s cpu time, 0.508s GC time Loading theory "HOL-Analysis.Topology_Euclidean_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex_Euclidean_Space") ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Ignoring duplicate rewrite rule: ### f (0::'a) \ 0::'b ### Ignoring duplicate rewrite rule: ### f (0::'a) \ 0::'b ### theory "HOL-Library.Extended_Nonnegative_Real" ### 1.920s elapsed time, 11.524s cpu time, 0.952s GC time Loading theory "HOL-Analysis.Sigma_Algebra" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Lebesgue_Measure" via "HOL-Analysis.Finite_Product_Measure" via "HOL-Analysis.Binary_Product_Measure" via "HOL-Analysis.Nonnegative_Lebesgue_Integration" via "HOL-Analysis.Measure_Space" via "HOL-Analysis.Measurable") Proofs for inductive predicate(s) "sigma_setsp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "HOL-Computational_Algebra.Factorial_Ring" ### 10.616s elapsed time, 61.608s cpu time, 9.416s GC time Loading theory "HOL-Computational_Algebra.Euclidean_Algorithm" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Jordan_Curve" via "HOL-Analysis.Arcwise_Connected" via "HOL-Computational_Algebra.Primes") Proofs for inductive predicate(s) "smallest_ccdi_setsp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "HOL-Analysis.Topology_Euclidean_Space" ### 2.649s elapsed time, 15.976s cpu time, 0.956s GC time Loading theory "HOL-Analysis.Convex_Euclidean_Space" (required by "HOL-Analysis.Analysis") Loading theory "HOL-Analysis.Extended_Real_Limits" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests") Loading theory "HOL-Analysis.Line_Segment" (required by "HOL-Analysis.Analysis") Loading theory "HOL-Analysis.Tagged_Division" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Henstock_Kurzweil_Integration") ### theory "HOL-Analysis.Sigma_Algebra" ### 2.641s elapsed time, 15.916s cpu time, 1.088s GC time Loading theory "HOL-Analysis.Measurable" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Lebesgue_Measure" via "HOL-Analysis.Finite_Product_Measure" via "HOL-Analysis.Binary_Product_Measure" via "HOL-Analysis.Nonnegative_Lebesgue_Integration" via "HOL-Analysis.Measure_Space") signature MEASURABLE = sig val add_del_cong_thm: bool -> thm -> Context.generic -> Context.generic val add_local_cong: thm -> Proof.context -> Proof.context val add_preprocessor: string -> preprocessor -> Context.generic -> Context.generic val cong_thm_attr: attribute context_parser val del_preprocessor: string -> Context.generic -> Context.generic val dest_thm_attr: attribute context_parser val get_all: Context.generic -> thm list val get_cong: Context.generic -> thm list val get_dest: Context.generic -> thm list datatype level = Concrete | Generic val measurable_tac: Proof.context -> thm list -> tactic val measurable_thm_attr: bool * (bool * level) -> attribute val prepare_facts: Proof.context -> thm list -> thm list * Proof.context type preprocessor = thm -> Proof.context -> thm list * Proof.context val simproc: Proof.context -> cterm -> thm option end structure Measurable: MEASURABLE ### theory "HOL-Analysis.Extended_Real_Limits" ### 1.286s elapsed time, 7.776s cpu time, 0.576s GC time Loading theory "HOL-Analysis.Summation_Tests" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit") ### theory "HOL-Analysis.Convex_Euclidean_Space" ### 1.321s elapsed time, 7.988s cpu time, 0.576s GC time Loading theory "HOL-Analysis.Ordered_Euclidean_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Lebesgue_Measure" via "HOL-Analysis.Finite_Product_Measure" via "HOL-Analysis.Binary_Product_Measure" via "HOL-Analysis.Nonnegative_Lebesgue_Integration" via "HOL-Analysis.Borel_Space") ### theory "HOL-Analysis.Line_Segment" ### 1.269s elapsed time, 7.684s cpu time, 0.576s GC time Loading theory "HOL-Analysis.Starlike" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Weierstrass_Theorems" via "HOL-Analysis.Path_Connected") ### theory "HOL-Analysis.Measurable" ### 0.678s elapsed time, 4.136s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Measure_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Lebesgue_Measure" via "HOL-Analysis.Finite_Product_Measure" via "HOL-Analysis.Binary_Product_Measure" via "HOL-Analysis.Nonnegative_Lebesgue_Integration") ### theory "HOL-Analysis.Tagged_Division" ### 1.289s elapsed time, 7.776s cpu time, 0.816s GC time ### theory "HOL-Analysis.Summation_Tests" ### 1.204s elapsed time, 7.232s cpu time, 0.816s GC time Loading theory "HOL-Analysis.Uniform_Limit" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function") Proofs for inductive predicate(s) "less_eq_measure" ### theory "HOL-Analysis.Uniform_Limit" ### 2.517s elapsed time, 13.108s cpu time, 8.300s GC time Loading theory "HOL-Analysis.Bounded_Continuous_Function" (required by "HOL-Analysis.Analysis") Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Loading theory "HOL-Analysis.Bounded_Linear_Function" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative") ### theory "HOL-Analysis.Starlike" ### 4.087s elapsed time, 22.552s cpu time, 9.676s GC time Loading theory "HOL-Analysis.Continuous_Extension" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Equivalence_Measurable_On_Borel") ### theory "HOL-Analysis.Measure_Space" ### 4.246s elapsed time, 23.520s cpu time, 9.676s GC time Loading theory "HOL-Analysis.Caratheodory" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Lebesgue_Measure") ### theory "HOL-Analysis.Bounded_Continuous_Function" ### 0.712s elapsed time, 4.308s cpu time, 0.560s GC time Loading theory "HOL-Analysis.Path_Connected" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Weierstrass_Theorems") ### theory "HOL-Analysis.Continuous_Extension" ### 0.242s elapsed time, 1.468s cpu time, 0.000s GC time ### theory "HOL-Analysis.Caratheodory" ### 0.415s elapsed time, 2.508s cpu time, 0.000s GC time ### theory "HOL-Analysis.Ordered_Euclidean_Space" ### 6.221s elapsed time, 35.336s cpu time, 10.520s GC time ### theory "HOL-Analysis.Bounded_Linear_Function" ### 2.702s elapsed time, 16.236s cpu time, 1.404s GC time Loading theory "HOL-Analysis.Derivative" (required by "HOL-Analysis.Analysis") ### Introduced fixed type variable(s): 'd, 'e, 'f in "f__" or "g__" ### Introduced fixed type variable(s): 'h in "A__" ### theory "HOL-Analysis.Path_Connected" ### 2.481s elapsed time, 14.912s cpu time, 0.844s GC time Loading theory "HOL-Analysis.Homotopy" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Homeomorphism") Loading theory "HOL-Analysis.Locally" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Abstract_Euclidean_Space") ### Ignoring duplicate rewrite rule: ### ?a1 * ?b1 \ (0::?'a1) \ ### (0::?'a1) \ ?a1 \ ?b1 \ (0::?'a1) \ ?a1 \ (0::?'a1) \ (0::?'a1) \ ?b1 ### theory "HOL-Analysis.Locally" ### 0.234s elapsed time, 1.412s cpu time, 0.000s GC time ### Introduced fixed type variable(s): 'a in "P__" ### theory "HOL-Analysis.Derivative" ### 2.582s elapsed time, 15.664s cpu time, 1.432s GC time Loading theory "HOL-Analysis.Borel_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Lebesgue_Measure" via "HOL-Analysis.Finite_Product_Measure" via "HOL-Analysis.Binary_Product_Measure" via "HOL-Analysis.Nonnegative_Lebesgue_Integration") Loading theory "HOL-Analysis.Cartesian_Euclidean_Space" (required by "HOL-Analysis.Analysis") Loading theory "HOL-Analysis.Complex_Analysis_Basics" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Harmonic_Numbers" via "HOL-Analysis.Complex_Transcendental") Loading theory "HOL-Analysis.Lipschitz" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Multivariate_Analysis") ### theory "HOL-Analysis.Cartesian_Euclidean_Space" ### 0.414s elapsed time, 2.512s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Cross3" (required by "HOL-Analysis.Analysis") ### theory "HOL-Analysis.Lipschitz" ### 0.621s elapsed time, 3.768s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Polytope" (required by "HOL-Analysis.Analysis") ### theory "HOL-Analysis.Homotopy" ### 2.803s elapsed time, 17.000s cpu time, 1.432s GC time Loading theory "HOL-Analysis.Homeomorphism" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration") ### theory "HOL-Analysis.Complex_Analysis_Basics" ### 1.353s elapsed time, 8.180s cpu time, 0.972s GC time Loading theory "HOL-Analysis.Complex_Transcendental" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Harmonic_Numbers") ### theory "HOL-Analysis.Homeomorphism" ### 0.807s elapsed time, 4.876s cpu time, 0.972s GC time Loading theory "HOL-Analysis.Brouwer_Fixpoint" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Fashoda_Theorem") ### theory "HOL-Analysis.Polytope" ### 2.080s elapsed time, 12.580s cpu time, 1.892s GC time Loading theory "HOL-Analysis.Abstract_Euclidean_Space" (required by "HOL-Analysis.Analysis") Proofs for inductive predicate(s) "ksimplex" Proving monotonicity ... ### theory "HOL-Analysis.Borel_Space" ### 2.824s elapsed time, 17.092s cpu time, 1.892s GC time Proving the introduction rules ... Loading theory "HOL-Analysis.Nonnegative_Lebesgue_Integration" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Lebesgue_Measure" via "HOL-Analysis.Finite_Product_Measure" via "HOL-Analysis.Binary_Product_Measure") Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "HOL-Computational_Algebra.Euclidean_Algorithm" ### 14.272s elapsed time, 84.188s cpu time, 14.420s GC time Loading theory "HOL-Computational_Algebra.Primes" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Jordan_Curve" via "HOL-Analysis.Arcwise_Connected") ### theory "HOL-Analysis.Abstract_Euclidean_Space" ### 0.381s elapsed time, 2.316s cpu time, 0.000s GC time Loading theory "HOL-Computational_Algebra.Formal_Power_Series" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.FPS_Convergence") ### theory "HOL-Analysis.Brouwer_Fixpoint" ### 1.687s elapsed time, 10.220s cpu time, 0.920s GC time Loading theory "HOL-Analysis.Regularity" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Lebesgue_Measure") ### theory "HOL-Computational_Algebra.Primes" ### 0.313s elapsed time, 1.900s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Arcwise_Connected" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Jordan_Curve") ### theory "HOL-Analysis.Complex_Transcendental" ### 2.202s elapsed time, 13.348s cpu time, 0.920s GC time Loading theory "HOL-Analysis.Generalised_Binomial_Theorem" (required by "HOL-Analysis.Analysis") ### theory "HOL-Analysis.Generalised_Binomial_Theorem" ### 2.364s elapsed time, 11.692s cpu time, 10.780s GC time Loading theory "HOL-Analysis.Harmonic_Numbers" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function") *** Interrupt