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.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Sigma_Algebra" via "HOL-Library.Indicator_Function") ### theory "HOL-Library.Disjoint_Sets" ### 0.278s elapsed time, 0.568s cpu time, 0.000s GC time Loading theory "HOL-Library.FuncSet" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Sigma_Algebra") ### ML warning (line 50 of "~~/src/HOL/Library/Cancellation/cancel.ML"): ### Pattern is not exhaustive. signature CANCEL = sig val proc: Proof.context -> cterm -> thm option end functor Cancel_Fun (Data: CANCEL_NUMERALS_DATA): CANCEL 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 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.768s elapsed time, 1.544s cpu time, 0.000s 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.484s elapsed time, 0.960s cpu time, 0.000s GC time Loading theory "HOL-Library.Infinite_Set" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Sigma_Algebra" via "HOL-Library.Countable_Set") consts enumerate :: "'a set \ nat \ 'a" ### theory "HOL-Library.Infinite_Set" ### 0.432s elapsed time, 0.816s cpu time, 0.240s GC time Loading theory "HOL-Library.Nat_Bijection" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Sigma_Algebra" via "HOL-Library.Countable_Set" via "HOL-Library.Countable") instantiation multiset :: (type) cancel_comm_monoid_add zero_multiset == zero_class.zero :: 'a multiset minus_multiset == minus :: 'a multiset \ 'a multiset \ 'a multiset plus_multiset == plus :: 'a multiset \ 'a multiset \ 'a multiset Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "size_list size <*mlex*> {}" ### theory "HOL-Library.Nat_Bijection" ### 0.474s elapsed time, 0.944s cpu time, 0.000s GC time Loading theory "HOL-Library.Old_Datatype" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Sigma_Algebra" via "HOL-Library.Countable_Set" via "HOL-Library.Countable") ### 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 ### 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 Found termination order: "(\p. size (fst p)) <*mlex*> {}" 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 instantiation multiset :: (type) Inf Inf_multiset == Inf :: 'a multiset set \ 'a multiset 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.597s elapsed time, 1.184s cpu time, 0.000s GC time Loading theory "HOL-Library.Phantom_Type" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Finite_Cartesian_Product" via "HOL-Library.Numeral_Type" via "HOL-Library.Cardinality") instantiation multiset :: (type) Sup Sup_multiset == Sup :: 'a multiset set \ 'a multiset instantiation multiset :: (type) size size_multiset == size :: 'a multiset \ nat locale comp_fun_commute fixes f :: "'a \ 'b \ 'b" assumes "comp_fun_commute f" consts mset :: "'a list \ 'a multiset" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" ### theory "HOL-Library.Phantom_Type" ### 0.789s elapsed time, 1.572s cpu time, 0.000s GC time Loading theory "HOL-Library.Cardinality" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Finite_Cartesian_Product" via "HOL-Library.Numeral_Type") ### Additional type variable(s) in locale specification "card2": 'a locale comm_monoid_mset fixes f :: "'a \ 'a \ 'a" (infixl "\<^bold>*" 70) and z :: "'a" ("\<^bold>1" [] 1000) assumes "comm_monoid_mset (\<^bold>* ) \<^bold>1" class card2 = finite + assumes "two_le_card": "2 \ CARD('a)" class finite_UNIV = type + fixes finite_UNIV :: "('a, bool) phantom" assumes "finite_UNIV": "finite_UNIV = Phantom('a) (finite UNIV)" class card_UNIV = finite_UNIV + fixes card_UNIV :: "('a, nat) phantom" assumes "card_UNIV": "card_UNIV_class.card_UNIV = Phantom('a) CARD('a)" instantiation nat :: card_UNIV card_UNIV_nat == card_UNIV_class.card_UNIV :: (nat, nat) phantom finite_UNIV_nat == finite_UNIV :: (nat, bool) phantom class comm_monoid_add = ab_semigroup_add + monoid_add + assumes "add_0": "\a. (0::'a) + a = a" instantiation int :: card_UNIV card_UNIV_int == card_UNIV_class.card_UNIV :: (int, nat) phantom finite_UNIV_int == finite_UNIV :: (int, bool) phantom instantiation natural :: card_UNIV card_UNIV_natural == card_UNIV_class.card_UNIV :: (natural, nat) phantom finite_UNIV_natural == finite_UNIV :: (natural, bool) phantom class comm_monoid_add = ab_semigroup_add + monoid_add + assumes "add_0": "\a. (0::'a) + a = a" instantiation integer :: card_UNIV card_UNIV_integer == card_UNIV_class.card_UNIV :: (integer, nat) phantom finite_UNIV_integer == finite_UNIV :: (integer, bool) phantom instantiation list :: (type) card_UNIV card_UNIV_list == card_UNIV_class.card_UNIV :: ('a list, nat) phantom finite_UNIV_list == finite_UNIV :: ('a list, bool) phantom instantiation unit :: card_UNIV card_UNIV_unit == card_UNIV_class.card_UNIV :: (unit, nat) phantom finite_UNIV_unit == finite_UNIV :: (unit, bool) phantom instantiation bool :: card_UNIV card_UNIV_bool == card_UNIV_class.card_UNIV :: (bool, nat) phantom finite_UNIV_bool == finite_UNIV :: (bool, bool) phantom class canonically_ordered_monoid_add = ordered_comm_monoid_add + assumes "le_iff_add": "\a b. (a \ b) = (\c. b = a + c)" instantiation char :: card_UNIV card_UNIV_char == card_UNIV_class.card_UNIV :: (char, nat) phantom finite_UNIV_char == finite_UNIV :: (char, bool) phantom instantiation prod :: (finite_UNIV, finite_UNIV) finite_UNIV finite_UNIV_prod == finite_UNIV :: ('a \ 'b, bool) phantom instantiation prod :: (card_UNIV, card_UNIV) card_UNIV card_UNIV_prod == card_UNIV_class.card_UNIV :: ('a \ 'b, nat) phantom instantiation sum :: (finite_UNIV, finite_UNIV) finite_UNIV finite_UNIV_sum == finite_UNIV :: ('a + 'b, bool) phantom instantiation sum :: (card_UNIV, card_UNIV) card_UNIV card_UNIV_sum == card_UNIV_class.card_UNIV :: ('a + 'b, nat) phantom instantiation fun :: (finite_UNIV, card_UNIV) finite_UNIV finite_UNIV_fun == finite_UNIV :: ('a \ 'b, bool) phantom instantiation fun :: (card_UNIV, card_UNIV) card_UNIV card_UNIV_fun == card_UNIV_class.card_UNIV :: ('a \ 'b, nat) phantom instantiation option :: (finite_UNIV) finite_UNIV finite_UNIV_option == finite_UNIV :: ('a option, bool) phantom instantiation option :: (card_UNIV) card_UNIV card_UNIV_option == card_UNIV_class.card_UNIV :: ('a option, nat) phantom instantiation String.literal :: card_UNIV card_UNIV_literal == card_UNIV_class.card_UNIV :: (String.literal, nat) phantom finite_UNIV_literal == finite_UNIV :: (String.literal, bool) phantom instantiation set :: (finite_UNIV) finite_UNIV finite_UNIV_set == finite_UNIV :: ('a set, bool) phantom instantiation set :: (card_UNIV) card_UNIV card_UNIV_set == card_UNIV_class.card_UNIV :: ('a set, nat) phantom instantiation Enum.finite_1 :: card_UNIV card_UNIV_finite_1 == card_UNIV_class.card_UNIV :: (Enum.finite_1, nat) phantom finite_UNIV_finite_1 == finite_UNIV :: (Enum.finite_1, bool) phantom instantiation Enum.finite_2 :: card_UNIV card_UNIV_finite_2 == card_UNIV_class.card_UNIV :: (Enum.finite_2, nat) phantom finite_UNIV_finite_2 == finite_UNIV :: (Enum.finite_2, bool) phantom instantiation Enum.finite_3 :: card_UNIV card_UNIV_finite_3 == card_UNIV_class.card_UNIV :: (Enum.finite_3, nat) phantom finite_UNIV_finite_3 == finite_UNIV :: (Enum.finite_3, bool) phantom instantiation Enum.finite_4 :: card_UNIV card_UNIV_finite_4 == card_UNIV_class.card_UNIV :: (Enum.finite_4, nat) phantom finite_UNIV_finite_4 == finite_UNIV :: (Enum.finite_4, bool) phantom instantiation Enum.finite_5 :: card_UNIV card_UNIV_finite_5 == card_UNIV_class.card_UNIV :: (Enum.finite_5, nat) phantom finite_UNIV_finite_5 == finite_UNIV :: (Enum.finite_5, bool) phantom class comm_monoid_mult = ab_semigroup_mult + monoid_mult + dvd + assumes "mult_1": "\a. (1::'a) * a = a" ### Code generator: dropping subsumed code equation ### List.coset [] \ set [] \ False ### theory "HOL-Library.Cardinality" ### 1.621s elapsed time, 3.188s cpu time, 0.868s GC time Loading theory "HOL-Library.Numeral_Type" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Finite_Cartesian_Product") locale mod_type fixes n :: "int" and Rep :: "'a \ int" and Abs :: "int \ 'a" assumes "mod_type n Rep Abs" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" locale mod_ring fixes n :: "int" and Rep :: "'a \ int" and Abs :: "int \ 'a" assumes "mod_ring n Rep Abs" instantiation num1 :: {comm_monoid_mult,numeral,comm_ring} uminus_num1 == uminus :: num1 \ num1 zero_num1 == zero_class.zero :: num1 minus_num1 == minus :: num1 \ num1 \ num1 plus_num1 == plus :: num1 \ num1 \ num1 one_num1 == one_class.one :: num1 times_num1 == times :: num1 \ num1 \ num1 instantiation bit0 :: (finite) {minus,one,plus,times,uminus,zero} bit1 :: (finite) {minus,one,plus,times,uminus,zero} zero_bit0 == zero_class.zero :: 'a bit0 uminus_bit0 == uminus :: 'a bit0 \ 'a bit0 times_bit0 == times :: 'a bit0 \ 'a bit0 \ 'a bit0 plus_bit0 == plus :: 'a bit0 \ 'a bit0 \ 'a bit0 one_bit0 == one_class.one :: 'a bit0 minus_bit0 == minus :: 'a bit0 \ 'a bit0 \ 'a bit0 zero_bit1 == zero_class.zero :: 'a bit1 uminus_bit1 == uminus :: 'a bit1 \ 'a bit1 times_bit1 == times :: 'a bit1 \ 'a bit1 \ 'a bit1 plus_bit1 == plus :: 'a bit1 \ 'a bit1 \ 'a bit1 one_bit1 == one_class.one :: 'a bit1 minus_bit1 == minus :: 'a bit1 \ 'a bit1 \ 'a bit1 instantiation bit0 :: (finite) linorder bit1 :: (finite) linorder less_eq_bit0 == less_eq :: 'a bit0 \ 'a bit0 \ bool less_bit0 == less :: 'a bit0 \ 'a bit0 \ bool less_eq_bit1 == less_eq :: 'a bit1 \ 'a bit1 \ bool less_bit1 == less :: 'a bit1 \ 'a bit1 \ bool instantiation multiset :: (preorder) order less_eq_multiset == less_eq :: 'a multiset \ 'a multiset \ bool less_multiset == less :: 'a multiset \ 'a multiset \ bool instantiation num0 :: equal equal_num0 == equal_class.equal :: num0 \ num0 \ bool instantiation multiset :: (preorder) ordered_ab_semigroup_add Proofs for inductive predicate(s) "pw_leq" instantiation num1 :: equal equal_num1 == equal_class.equal :: num1 \ num1 \ bool Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... instantiation num1 :: enum enum_num1 == enum_class.enum :: num1 list enum_all_num1 == enum_class.enum_all :: (num1 \ bool) \ bool enum_ex_num1 == enum_class.enum_ex :: (num1 \ bool) \ bool instantiation num0 :: card_UNIV num1 :: card_UNIV card_UNIV_num0 == card_UNIV_class.card_UNIV :: (num0, nat) phantom finite_UNIV_num0 == finite_UNIV :: (num0, bool) phantom card_UNIV_num1 == card_UNIV_class.card_UNIV :: (num1, nat) phantom finite_UNIV_num1 == finite_UNIV :: (num1, bool) phantom instantiation bit0 :: (finite) equal bit1 :: (finite) equal equal_bit0 == equal_class.equal :: 'a bit0 \ 'a bit0 \ bool equal_bit1 == equal_class.equal :: 'a bit1 \ 'a bit1 \ bool instantiation bit0 :: (finite) enum enum_bit0 == enum_class.enum :: 'a bit0 list enum_all_bit0 == enum_class.enum_all :: ('a bit0 \ bool) \ bool enum_ex_bit0 == enum_class.enum_ex :: ('a bit0 \ bool) \ bool instantiation bit1 :: (finite) enum enum_bit1 == enum_class.enum :: 'a bit1 list enum_all_bit1 == enum_class.enum_all :: ('a bit1 \ bool) \ bool enum_ex_bit1 == enum_class.enum_ex :: ('a bit1 \ bool) \ bool instantiation bit0 :: (finite) finite_UNIV bit1 :: (finite) finite_UNIV finite_UNIV_bit0 == finite_UNIV :: ('a bit0, bool) phantom finite_UNIV_bit1 == finite_UNIV :: ('a bit1, bool) phantom instantiation bit0 :: ({card_UNIV,finite}) card_UNIV bit1 :: ({card_UNIV,finite}) card_UNIV card_UNIV_bit0 == card_UNIV_class.card_UNIV :: ('a bit0, nat) phantom card_UNIV_bit1 == card_UNIV_class.card_UNIV :: ('a bit1, nat) phantom Found termination order: "(\p. length (fst p)) <*mlex*> {}" ### theory "HOL-Library.Numeral_Type" ### 1.179s elapsed time, 2.348s cpu time, 0.000s GC time Loading theory "HOL-Library.Product_Plus" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Continuous_Extension" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space" via "HOL-Analysis.Connected" via "HOL-Analysis.Topology_Euclidean_Space" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space" via "HOL-Analysis.Product_Vector") instantiation multiset :: (equal) equal equal_multiset == equal_class.equal :: 'a multiset \ 'a multiset \ bool instantiation prod :: (zero, zero) zero zero_prod == zero_class.zero :: 'a \ 'b instantiation prod :: (plus, plus) plus plus_prod == plus :: 'a \ 'b \ 'a \ 'b \ 'a \ 'b instantiation prod :: (minus, minus) minus minus_prod == minus :: 'a \ 'b \ 'a \ 'b \ 'a \ 'b instantiation prod :: (uminus, uminus) uminus uminus_prod == uminus :: 'a \ 'b \ 'a \ 'b instantiation multiset :: (random) random random_multiset == random_class.random :: natural \ natural \ natural \ ('a multiset \ (unit \ term)) \ natural \ natural ### theory "HOL-Library.Product_Plus" ### 0.149s elapsed time, 0.296s cpu time, 0.000s GC time Loading theory "HOL-Library.Product_Order" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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") instantiation prod :: (ord, ord) ord less_eq_prod == less_eq :: 'a \ 'b \ 'a \ 'b \ bool less_prod == less :: 'a \ 'b \ 'a \ 'b \ bool instantiation prod :: (inf, inf) inf inf_prod == inf :: 'a \ 'b \ 'a \ 'b \ 'a \ 'b instantiation prod :: (sup, sup) sup sup_prod == sup :: 'a \ 'b \ 'a \ 'b \ 'a \ 'b instantiation prod :: (top, top) top top_prod == top :: 'a \ 'b instantiation prod :: (bot, bot) bot bot_prod == bot :: 'a \ 'b instantiation prod :: (Inf, Inf) Inf Inf_prod == Inf :: ('a \ 'b) set \ 'a \ 'b instantiation prod :: (Sup, Sup) Sup Sup_prod == Sup :: ('a \ 'b) set \ 'a \ 'b instantiation multiset :: (full_exhaustive) full_exhaustive full_exhaustive_multiset == full_exhaustive_class.full_exhaustive :: ('a multiset \ (unit \ term) \ (bool \ term list) option) \ natural \ (bool \ term list) option ### theory "HOL-Library.Product_Order" ### 0.361s elapsed time, 0.716s cpu time, 0.000s GC time Loading theory "HOL-Library.Set_Algebras" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Continuous_Extension" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space") instantiation set :: (plus) plus plus_set == plus :: 'a set \ 'a set \ 'a set instantiation set :: (times) times times_set == times :: 'a set \ 'a set \ 'a set Proofs for inductive predicate(s) "pred_mset" Proving monotonicity ... Proving the introduction rules ... instantiation set :: (zero) zero zero_set == zero_class.zero :: 'a set Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... instantiation set :: (one) one one_set == one_class.one :: 'a set 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" ### 5.951s elapsed time, 11.748s cpu time, 1.108s 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") ### theory "HOL-Library.Set_Algebras" ### 0.370s elapsed time, 0.732s cpu time, 0.000s GC time Loading theory "HOL-Library.Permutations" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants") Proofs for inductive predicate(s) "swapidseq" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor + fixes normalize :: "'a \ 'a" assumes "unit_factor_mult_normalize": "\a. unit_factor a * normalize a = a" and "normalize_0": "normalize (0::'a) = (0::'a)" Found termination order: "(\p. size_list size (fst p)) <*mlex*> {}" ### theory "HOL-Library.Permutations" ### 1.642s elapsed time, 3.240s cpu time, 0.804s GC time Loading theory "HOL-Library.Countable" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Sigma_Algebra" via "HOL-Library.Countable_Set") class semiring_gcd = gcd + normalization_semidom + assumes "gcd_dvd1": "\a b. gcd a b dvd a" and "gcd_dvd2": "\a b. gcd a b dvd b" and "gcd_greatest": "\c a b. \c dvd a; c dvd b\ \ c dvd gcd a b" and "normalize_gcd": "\a b. normalize (gcd a b) = gcd a b" and "lcm_gcd": "\a b. lcm a b = normalize (a * b) div gcd a b" ### Additional type variable(s) in locale specification "countable": 'a class countable = type + assumes "ex_inj": "\to_nat. inj to_nat" 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 ... val old_countable_datatype_tac = fn: Proof.context -> int -> tactic class factorial_semiring = normalization_semidom + assumes "prime_factorization_exists": "\x. x \ (0::'a) \ \A. (\x. x \# A \ prime_elem x) \ prod_mset A = normalize x" ### 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 val countable_datatype_tac = fn: Proof.context -> thm -> thm Seq.seq val countable_tac = fn: Proof.context -> int -> tactic class factorial_semiring = normalization_semidom + assumes "prime_factorization_exists": "\x. x \ (0::'a) \ \A. (\x. x \# A \ prime_elem x) \ prod_mset A = normalize x" ### theory "HOL-Library.Countable" ### 1.522s elapsed time, 3.028s cpu time, 0.000s GC time Loading theory "HOL-Library.Countable_Set" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Sigma_Algebra") ### theory "HOL-Library.Countable_Set" ### 0.585s elapsed time, 1.168s cpu time, 0.000s GC time Loading theory "HOL-Library.Countable_Complete_Lattices" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Sigma_Algebra" via "HOL-Library.Extended_Nonnegative_Real" via "HOL-Library.Extended_Real" via "HOL-Library.Extended_Nat" via "HOL-Library.Order_Continuity") class countable_complete_lattice = Inf + Sup + lattice + bot + top + assumes "ccInf_lower": "\A x. \countable A; x \ A\ \ Inf A \ x" assumes "ccInf_greatest": "\A z. \countable A; \x. x \ A \ z \ x\ \ z \ Inf A" assumes "ccSup_upper": "\A x. \countable A; x \ A\ \ x \ Sup A" assumes "ccSup_least": "\A z. \countable A; \x. x \ A \ x \ z\ \ Sup A \ z" assumes "ccInf_empty": "Inf {} = top" assumes "ccSup_empty": "Sup {} = bot" class countable_complete_distrib_lattice = countable_complete_lattice + assumes "sup_ccInf": "\B a. countable B \ sup a (Inf B) = (INF b:B. sup a b)" assumes "inf_ccSup": "\B a. countable B \ inf a (Sup B) = (SUP b:B. inf a b)" class factorial_semiring_gcd = factorial_semiring + Gcd + assumes "gcd_eq_gcd_factorial": "\a b. gcd a b = gcd_factorial a b" and "lcm_eq_lcm_factorial": "\a b. lcm a b = lcm_factorial a b" and "Gcd_eq_Gcd_factorial": "\A. Gcd A = Gcd_factorial A" and "Lcm_eq_Lcm_factorial": "\A. Lcm A = Lcm_factorial A" ### theory "HOL-Library.Countable_Complete_Lattices" ### 2.725s elapsed time, 5.420s cpu time, 0.468s GC time Loading theory "HOL-Analysis.Continuum_Not_Denumerable" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected") ### theory "HOL-Analysis.Continuum_Not_Denumerable" ### 0.382s elapsed time, 0.764s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Infinite_Products" (required by "HOL-Analysis.Analysis") ### theory "HOL-Analysis.Infinite_Products" ### 0.259s elapsed time, 0.520s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Inner_Product" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Continuous_Extension" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space" via "HOL-Analysis.Connected" via "HOL-Analysis.Topology_Euclidean_Space" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space" via "HOL-Analysis.Product_Vector") class real_inner = dist_norm + real_vector + sgn_div_norm + uniformity_dist + open_uniformity + fixes inner :: "'a \ 'a \ real" assumes "inner_commute": "\x y. inner x y = inner y x" and "inner_add_left": "\x y z. inner (x + y) z = inner x z + inner y z" and "inner_scaleR_left": "\r x y. inner (r *\<^sub>R x) y = r * inner x y" and "inner_ge_zero": "\x. 0 \ inner x x" and "inner_eq_zero_iff": "\x. (inner x x = 0) = (x = (0::'a))" and "norm_eq_sqrt_inner": "\x. norm x = sqrt (inner x x)" instantiation real :: real_inner inner_real == inner :: real \ real \ real instantiation complex :: real_inner inner_complex == inner :: complex \ complex \ real ### theory "HOL-Computational_Algebra.Factorial_Ring" ### 8.371s elapsed time, 16.624s cpu time, 1.636s 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") ### theory "HOL-Analysis.Inner_Product" ### 1.198s elapsed time, 2.364s cpu time, 0.364s GC time Loading theory "HOL-Analysis.Product_Vector" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Continuous_Extension" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space" via "HOL-Analysis.Connected" via "HOL-Analysis.Topology_Euclidean_Space" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space") instantiation prod :: (real_vector, real_vector) real_vector scaleR_prod == scaleR :: real \ 'a \ 'b \ 'a \ 'b instantiation prod :: (metric_space, metric_space) dist dist_prod == dist :: 'a \ 'b \ 'a \ 'b \ real instantiation prod :: (metric_space, metric_space) uniformity_dist uniformity_prod == uniformity :: (('a \ 'b) \ 'a \ 'b) filter instantiation prod :: (metric_space, metric_space) metric_space instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector sgn_prod == sgn :: 'a \ 'b \ 'a \ 'b norm_prod == norm :: 'a \ 'b \ real instantiation prod :: (real_inner, real_inner) real_inner inner_prod == inner :: 'a \ 'b \ 'a \ 'b \ real ### theory "HOL-Analysis.Product_Vector" ### 0.575s elapsed time, 1.148s cpu time, 0.000s GC time Loading theory "HOL-Analysis.L2_Norm" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Continuous_Extension" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space" via "HOL-Analysis.Connected" via "HOL-Analysis.Topology_Euclidean_Space" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space") ### theory "HOL-Analysis.L2_Norm" ### 0.154s elapsed time, 0.308s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Euclidean_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Continuous_Extension" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space" via "HOL-Analysis.Connected" via "HOL-Analysis.Topology_Euclidean_Space" via "HOL-Analysis.Linear_Algebra") class euclidean_space = real_inner + fixes Basis :: "'a set" assumes "nonempty_Basis": "Basis \ {}" assumes "finite_Basis": "finite Basis" assumes "inner_Basis": "\u v. \u \ Basis; v \ Basis\ \ inner u v = (if u = v then 1 else 0)" assumes "euclidean_all_zero_iff": "\x. (\u\Basis. inner x u = 0) = (x = (0::'a))" instantiation real :: euclidean_space Basis_real == Basis :: real set instantiation complex :: euclidean_space Basis_complex == Basis :: complex set instantiation prod :: (euclidean_space, euclidean_space) euclidean_space Basis_prod == Basis :: ('a \ 'b) set ### theory "HOL-Analysis.Euclidean_Space" ### 1.513s elapsed time, 3.028s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Linear_Algebra" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Continuous_Extension" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space" via "HOL-Analysis.Connected" via "HOL-Analysis.Topology_Euclidean_Space") class euclidean_semiring_gcd = normalization_euclidean_semiring + Gcd + assumes "gcd_eucl": "normalization_euclidean_semiring_class.gcd = gcd" and "lcm_eucl": "normalization_euclidean_semiring_class.lcm = lcm" assumes "Gcd_eucl": "normalization_euclidean_semiring_class.Gcd = Gcd" and "Lcm_eucl": "normalization_euclidean_semiring_class.Lcm = Lcm" Proofs for inductive predicate(s) "span_induct_alt_helpp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... class real_inner = real_normed_vector + fixes inner :: "'a \ 'a \ real" assumes "inner_commute": "\x y. x \ y = y \ x" and "inner_add_left": "\x y z. (x + y) \ z = x \ z + y \ z" and "inner_scaleR_left": "\r x y. r *\<^sub>R x \ y = r * (x \ y)" and "inner_ge_zero": "\x. 0 \ x \ x" and "inner_eq_zero_iff": "\x. (x \ x = 0) = (x = (0::'a))" and "norm_eq_sqrt_inner": "\x. norm x = sqrt (x \ x)" ### theory "HOL-Analysis.Linear_Algebra" ### 3.504s elapsed time, 6.940s cpu time, 1.048s GC time Loading theory "HOL-Analysis.Finite_Cartesian_Product" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Cartesian_Euclidean_Space") bundle vec_syntax bundle no_vec_syntax instantiation vec :: (zero, finite) zero zero_vec == zero_class.zero :: ('a, 'b) vec instantiation vec :: (plus, finite) plus plus_vec == plus :: ('a, 'b) vec \ ('a, 'b) vec \ ('a, 'b) vec instantiation vec :: (minus, finite) minus minus_vec == minus :: ('a, 'b) vec \ ('a, 'b) vec \ ('a, 'b) vec instantiation vec :: (uminus, finite) uminus uminus_vec == uminus :: ('a, 'b) vec \ ('a, 'b) vec instantiation vec :: (real_vector, finite) real_vector scaleR_vec == scaleR :: real \ ('a, 'b) vec \ ('a, 'b) vec instantiation vec :: (topological_space, finite) topological_space open_vec == open :: ('a, 'b) vec set \ bool instantiation vec :: (metric_space, finite) dist dist_vec == dist :: ('a, 'b) vec \ ('a, 'b) vec \ real instantiation vec :: (metric_space, finite) uniformity_dist uniformity_vec == uniformity :: (('a, 'b) vec \ ('a, 'b) vec) filter instantiation vec :: (metric_space, finite) metric_space instantiation vec :: (real_normed_vector, finite) real_normed_vector sgn_vec == sgn :: ('a, 'b) vec \ ('a, 'b) vec norm_vec == norm :: ('a, 'b) vec \ real instantiation vec :: (real_inner, finite) real_inner inner_vec == inner :: ('a, 'b) vec \ ('a, 'b) vec \ real instantiation vec :: (euclidean_space, finite) euclidean_space Basis_vec == Basis :: ('a, 'b) vec set ### theory "HOL-Analysis.Finite_Cartesian_Product" ### 1.661s elapsed time, 3.316s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Operator_Norm" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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.Derivative") ### theory "HOL-Analysis.Operator_Norm" ### 0.148s elapsed time, 0.296s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Poly_Roots" (required by "HOL-Analysis.Analysis") ### theory "HOL-Analysis.Poly_Roots" ### 0.156s elapsed time, 0.312s cpu time, 0.000s GC time Loading theory "HOL-Library.Discrete" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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.Derivative" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests") ### 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-Computational_Algebra.Euclidean_Algorithm" ### 7.994s elapsed time, 15.908s cpu time, 1.048s 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-Library.Discrete" ### 0.256s elapsed time, 0.512s 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-Computational_Algebra.Primes" ### 0.635s elapsed time, 1.244s cpu time, 0.388s GC time Loading theory "HOL-Library.Indicator_Function" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Sigma_Algebra") instantiation fps :: (zero) zero zero_fps == zero_class.zero :: 'a fps instantiation fps :: ({one,zero}) one one_fps == one_class.one :: 'a fps instantiation fps :: (plus) plus plus_fps == plus :: 'a fps \ 'a fps \ 'a fps instantiation fps :: (minus) minus minus_fps == minus :: 'a fps \ 'a fps \ 'a fps ### theory "HOL-Library.Indicator_Function" ### 0.436s elapsed time, 0.872s cpu time, 0.000s GC time Loading theory "HOL-Library.Liminf_Limsup" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Sigma_Algebra" via "HOL-Library.Extended_Nonnegative_Real" via "HOL-Library.Extended_Real") instantiation fps :: (uminus) uminus uminus_fps == uminus :: 'a fps \ 'a fps instantiation fps :: ({comm_monoid_add,times}) times times_fps == times :: 'a fps \ 'a fps \ 'a fps instantiation fps :: (comm_ring_1) dist dist_fps == dist :: 'a fps \ 'a fps \ real instantiation fps :: (comm_ring_1) metric_space uniformity_fps == uniformity :: ('a fps \ 'a fps) filter open_fps == open :: 'a fps set \ bool instantiation fps :: ({inverse,comm_monoid_add,times,uminus}) inverse inverse_fps == inverse :: 'a fps \ 'a fps divide_fps == divide :: 'a fps \ 'a fps \ 'a fps ### theory "HOL-Library.Liminf_Limsup" ### 0.775s elapsed time, 1.556s cpu time, 0.000s GC time Loading theory "HOL-Library.Nonpos_Ints" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Jordan_Curve" via "HOL-Analysis.Further_Topology" via "HOL-Analysis.Complex_Transcendental" via "HOL-Analysis.Complex_Analysis_Basics") Found termination order: "(\p. size (snd p)) <*mlex*> {}" instantiation fps :: (field) normalization_semidom normalize_fps == normalize :: 'a fps \ 'a fps unit_factor_fps == unit_factor :: 'a fps \ 'a fps ### theory "HOL-Library.Nonpos_Ints" ### 0.253s elapsed time, 0.504s cpu time, 0.000s GC time Loading theory "HOL-Library.Order_Continuity" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Sigma_Algebra" via "HOL-Library.Extended_Nonnegative_Real" via "HOL-Library.Extended_Real" via "HOL-Library.Extended_Nat") instantiation fps :: (field) idom_modulo modulo_fps == modulo :: 'a fps \ 'a fps \ 'a fps instantiation fps :: (field) euclidean_ring_cancel euclidean_size_fps == euclidean_size :: 'a fps \ nat instantiation fps :: (field) euclidean_ring_gcd Gcd_fps == Gcd :: 'a fps set \ 'a fps Lcm_fps == Lcm :: 'a fps set \ 'a fps gcd_fps == gcd :: 'a fps \ 'a fps \ 'a fps lcm_fps == lcm :: 'a fps \ 'a fps \ 'a fps Found termination order: "(\p. size (fst p)) <*mlex*> {}" ### theory "HOL-Library.Order_Continuity" ### 0.779s elapsed time, 1.492s cpu time, 0.000s GC time Loading theory "HOL-Library.Extended_Nat" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Sigma_Algebra" via "HOL-Library.Extended_Nonnegative_Real" via "HOL-Library.Extended_Real") class infinity = type + fixes infinity :: "'a" instantiation enat :: infinity infinity_enat == infinity :: enat Proofs for inductive predicate(s) "rec_set_enat" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the simplification rules ... ### No equation for constructor "Extended_Nat.infinity_class.infinity" ### in definition of function "the_enat" consts the_enat :: "enat \ nat" instantiation enat :: zero_neq_one one_enat == one_class.one :: enat zero_enat == zero_class.zero :: enat instantiation enat :: comm_monoid_add plus_enat == plus :: enat \ enat \ enat instantiation enat :: {comm_semiring_1,semiring_no_zero_divisors} times_enat == times :: enat \ enat \ enat Found termination order: "(\p. size (snd p)) <*mlex*> {}" instantiation enat :: minus minus_enat == minus :: enat \ enat \ enat instantiation enat :: linordered_ab_semigroup_add less_eq_enat == less_eq :: enat \ enat \ bool less_enat == less :: enat \ enat \ bool Found termination order: "(\p. size (snd (snd p))) <*mlex*> {}" instantiation enat :: {order_bot,order_top} top_enat == top :: enat bot_enat == bot :: enat 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 instantiation enat :: complete_lattice Inf_enat == Inf :: enat set \ enat Sup_enat == Sup :: enat set \ enat sup_enat == sup :: enat \ enat \ enat inf_enat == inf :: enat \ enat \ enat ### theory "HOL-Library.Extended_Nat" ### 1.322s elapsed time, 2.608s cpu time, 0.640s GC time Loading theory "HOL-Library.Extended_Real" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Sigma_Algebra" via "HOL-Library.Extended_Nonnegative_Real") instantiation enat :: linorder_topology open_enat == open :: enat set \ bool bundle fps_notation ### theory "HOL-Computational_Algebra.Formal_Power_Series" ### 4.912s elapsed time, 9.692s cpu time, 1.028s GC time Loading theory "HOL-Library.Periodic_Fun" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Jordan_Curve" via "HOL-Analysis.Further_Topology" via "HOL-Analysis.Complex_Transcendental") locale periodic_fun fixes f :: "'a \ 'b" and g :: "'a \ 'a \ 'a" and gm :: "'a \ 'a \ 'a" and g1 :: "'a \ 'a" and gn1 :: "'a \ 'a" assumes "periodic_fun f g gm g1 gn1" locale periodic_fun_simple fixes f :: "'a \ 'b" and period :: "'a" assumes "periodic_fun_simple f period" locale periodic_fun_simple' fixes f :: "'a \ 'b" assumes "periodic_fun_simple' f" ### theory "HOL-Library.Periodic_Fun" ### 0.211s elapsed time, 0.424s cpu time, 0.000s GC time Loading theory "HOL-Library.Sum_of_Squares" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Continuous_Extension" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space" via "HOL-Analysis.Connected" via "HOL-Analysis.Topology_Euclidean_Space" via "HOL-Analysis.Norm_Arith") ### Rule already declared as safe introduction (intro!) ### True ### Ignoring duplicate introduction (intro) ### True instantiation ereal :: uminus uminus_ereal == uminus :: ereal \ ereal Found termination order: "{}" instantiation ereal :: infinity infinity_ereal == infinity :: ereal instantiation ereal :: abs abs_ereal == abs :: ereal \ ereal instantiation ereal :: {comm_monoid_add,zero_neq_one} one_ereal == one_class.one :: ereal zero_ereal == zero_class.zero :: ereal plus_ereal == plus :: ereal \ ereal \ ereal instantiation ereal :: linorder less_eq_ereal == less_eq :: ereal \ ereal \ bool less_ereal == less :: ereal \ ereal \ bool instantiation ereal :: {comm_monoid_mult,sgn} sgn_ereal == sgn :: ereal \ ereal times_ereal == times :: ereal \ ereal \ ereal instantiation ereal :: minus minus_ereal == minus :: ereal \ ereal \ ereal instantiation ereal :: inverse inverse_ereal == inverse :: ereal \ ereal divide_ereal == divide :: ereal \ ereal \ ereal instantiation ereal :: lattice inf_ereal == inf :: ereal \ ereal \ ereal sup_ereal == sup :: ereal \ ereal \ ereal instantiation ereal :: complete_lattice Inf_ereal == Inf :: ereal set \ ereal Sup_ereal == Sup :: ereal set \ ereal bot_ereal == bot :: ereal top_ereal == top :: ereal instantiation ereal :: linear_continuum_topology open_ereal == open :: ereal set \ bool ### ML warning (line 379 of "~~/src/HOL/Library/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 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 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 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.306s elapsed time, 6.540s cpu time, 0.748s GC time Loading theory "HOL-Analysis.Norm_Arith" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Continuous_Extension" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space" via "HOL-Analysis.Connected" via "HOL-Analysis.Topology_Euclidean_Space") ### 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.316s elapsed time, 0.632s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Topology_Euclidean_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Continuous_Extension" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space" via "HOL-Analysis.Connected") ### theory "HOL-Library.Extended_Real" ### 4.845s elapsed time, 9.616s cpu time, 0.748s GC time Loading theory "HOL-Library.Extended_Nonnegative_Real" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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" via "HOL-Analysis.Sigma_Algebra") instantiation ennreal :: complete_linorder Inf_ennreal == Inf :: ennreal set \ ennreal Sup_ennreal == Sup :: ennreal set \ ennreal bot_ennreal == bot :: ennreal sup_ennreal == sup :: ennreal \ ennreal \ ennreal top_ennreal == top :: ennreal inf_ennreal == inf :: ennreal \ ennreal \ ennreal less_eq_ennreal == less_eq :: ennreal \ ennreal \ bool less_ennreal == less :: ennreal \ ennreal \ bool instantiation ennreal :: infinity infinity_ennreal == infinity :: ennreal instantiation ennreal :: {comm_semiring_1,semiring_1_no_zero_divisors} zero_ennreal == zero_class.zero :: ennreal plus_ennreal == plus :: ennreal \ ennreal \ ennreal one_ennreal == one_class.one :: ennreal times_ennreal == times :: ennreal \ ennreal \ ennreal instantiation ennreal :: minus minus_ennreal == minus :: ennreal \ ennreal \ ennreal instantiation ennreal :: inverse inverse_ennreal == inverse :: ennreal \ ennreal divide_ennreal == divide :: ennreal \ ennreal \ ennreal 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 class topological_space = open + assumes "open_UNIV": "open UNIV" assumes "open_Int": "\S T. \open S; open T\ \ open (S \ T)" assumes "open_Union": "\K. Ball K open \ open (\K)" locale countable_basis fixes B :: "'a set set" assumes "countable_basis B" ### theory "HOL-Analysis.Topology_Euclidean_Space" ### 1.717s elapsed time, 3.440s cpu time, 0.000s GC time instantiation ennreal :: linear_continuum_topology open_ennreal == open :: ennreal set \ bool ### theory "HOL-Library.Extended_Nonnegative_Real" ### 2.713s elapsed time, 5.408s cpu time, 0.404s GC time Loading theory "HOL-Analysis.Sigma_Algebra" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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") locale subset_class fixes \ :: "'a set" and M :: "'a set set" assumes "subset_class \ M" locale semiring_of_sets fixes \ :: "'a set" and M :: "'a set set" assumes "semiring_of_sets \ M" locale ring_of_sets fixes \ :: "'a set" and M :: "'a set set" assumes "ring_of_sets \ M" locale algebra fixes \ :: "'a set" and M :: "'a set set" assumes "algebra \ M" locale sigma_algebra fixes \ :: "'a set" and M :: "'a set set" assumes "sigma_algebra \ M" 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 ... 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 ... locale dynkin_system fixes \ :: "'a set" and M :: "'a set set" assumes "dynkin_system \ M" ### theory "HOL-Analysis.Sigma_Algebra" ### 2.914s elapsed time, 5.812s cpu time, 0.296s GC time Loading theory "HOL-Analysis.Measurable" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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 ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### theory "HOL-Analysis.Measurable" ### 0.815s elapsed time, 1.604s cpu time, 0.220s GC time Loading theory "HOL-Analysis.Measure_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" 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") locale sigma_finite_measure fixes M :: "'a measure" assumes "sigma_finite_measure M" locale finite_measure fixes M :: "'a measure" assumes "finite_measure M" instantiation measure :: (type) order_bot bot_measure == bot :: 'a measure less_eq_measure == less_eq :: 'a measure \ 'a measure \ bool less_measure == less :: 'a measure \ 'a measure \ bool Proofs for inductive predicate(s) "less_eq_measure" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... instantiation measure :: (type) semilattice_sup sup_measure == sup :: 'a measure \ 'a measure \ 'a measure instantiation measure :: (type) complete_lattice Inf_measure == Inf :: 'a measure set \ 'a measure Sup_measure == Sup :: 'a measure set \ 'a measure top_measure == top :: 'a measure inf_measure == inf :: 'a measure \ 'a measure \ 'a measure ### theory "HOL-Analysis.Measure_Space" ### 2.666s elapsed time, 5.292s cpu time, 0.416s GC time Loading theory "HOL-Analysis.Caratheodory" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Lebesgue_Integral_Substitution" via "HOL-Analysis.Interval_Integral" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Lebesgue_Measure") ### theory "HOL-Analysis.Caratheodory" ### 0.563s elapsed time, 1.128s cpu time, 0.000s GC time ### Introduced fixed type variable(s): 'd, 'e, 'f in "f__" or "g__" ### Introduced fixed type variable(s): 'h in "A__" ### Introduced fixed type variable(s): 'd, 'e, 'f in "f__" or "g__" ### Introduced fixed type variable(s): 'd, 'e in "X__" or "f__" or "g__" ### Introduced fixed type variable(s): 'd, 'e in "f__" ### Introduced fixed type variable(s): 'd in "X__" ### Introduced fixed type variable(s): 'd, 'e, 'f in "R__" or "S__" ### Introduced fixed type variable(s): 'd, 'e in "R__" ### Ignoring duplicate rewrite rule: ### mset (map ?f1 ?xs1) \ image_mset ?f1 (mset ?xs1) ### Ignoring duplicate rewrite rule: ### mset (map ?f1 ?xs1) \ image_mset ?f1 (mset ?xs1) ### Introduced fixed type variable(s): 'd in "z__" ### Introduced fixed type variable(s): 'd in "P__" ### Ignoring duplicate rewrite rule: ### inverse_permutation_of_list [] ?y \ ?y ### Ignoring duplicate rewrite rule: ### span UNIV \ UNIV ### Ignoring duplicate rewrite rule: ### span UNIV \ UNIV ### Ignoring duplicate rewrite rule: ### of_nat (Suc ?m1) \ (1::?'a1) + of_nat ?m1 ### Ignoring duplicate rewrite rule: ### dim (span ?S1) \ dim ?S1 ### Ignoring duplicate rewrite rule: ### dim (span ?S1) \ dim ?S1 ### Ignoring duplicate rewrite rule: ### dim (span ?S1) \ dim ?S1 ### Ignoring duplicate rewrite rule: ### dim UNIV \ DIM(?'a1) ### Ignoring duplicate rewrite rule: ### (0::?'a1) \ span ?S1 \ True ### Ignoring duplicate rewrite rule: ### (0::?'a1) \ span ?S1 \ True ### Ignoring duplicate rewrite rule: ### collinear {?x1, ?y1} \ True ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if ?a1 = k then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if ?a1 = k then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if ?a1 = k then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Introduced fixed type variable(s): 'a in "P__" ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if ?a1 = k then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Introduced fixed type variable(s): 'b, 'c in "a__" or "r__" ### Introduced fixed type variable(s): 'b, 'c in "a__" or "r__" ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if ?a1 = k then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if ?a1 = k then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if ?a1 = k then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) "- \" :: "ereal" "\" :: "ereal" "True" :: "bool" "True" :: "bool" "ereal (13 / 4)" :: "ereal" ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### range ?A \ M \ (\i. ?A i) \ M ### Ignoring duplicate introduction (intro) ### ?a \ ?A \ ?a \ sigma_sets ?sp ?A ### Rule already declared as introduction (intro) ### \?a \ generated_ring; ?b \ generated_ring; ### ?a \ ?b = {}\ ### \ ?a \ ?b \ generated_ring ### Rule already declared as introduction (intro) ### \?a \ sets ?M; ?b \ sets ?M\ ### \ ?a \ ?b \ sets ?M ### Rule already declared as introduction (intro) ### ?x \ UNIV ### Rule already declared as introduction (intro) ### ?x \ UNIV ### Rule already declared as introduction (intro) ### \?a \ sets ?M; ?b \ sets ?M\ ### \ ?a - ?b \ sets ?M ### Rule already declared as introduction (intro) ### \?a \ M; ?b \ M\ \ ?a - ?b \ M ### Ignoring duplicate rewrite rule: ### enn2ereal top \ \ ### Rule already declared as introduction (intro) ### \?b = ?f ?x; ?x \ ?A\ \ ?b \ ?f ` ?A ### Metis: Unused theorems: "local.yl" ### Metis: Unused theorems: "local.xl" ### Rule already declared as introduction (intro) ### ?A ` ?X \ M \ (\x\?X. ?A x) \ M ### Rule already declared as introduction (intro) ### \?a \ generated_ring; ?b \ generated_ring\ ### \ ?a \ ?b \ generated_ring ### Rule already declared as introduction (intro) ### \finite ?X; ?X \ generated_ring\ ### \ \?X \ generated_ring ### Rule already declared as introduction (intro) ### \?a \ generated_ring; ?b \ generated_ring\ ### \ ?a \ ?b \ generated_ring ### Rule already declared as introduction (intro) ### \finite ?X; ?X \ generated_ring\ ### \ \?X \ generated_ring ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g isabelle document -d /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/manual -o pdf -n manual -t -proof,-ML,-unimportant *** Failed to load theory "HOL-Analysis.Connected" (unresolved "HOL-Analysis.Topology_Euclidean_Space") *** Failed to load theory "HOL-Analysis.Convex_Euclidean_Space" (unresolved "HOL-Analysis.Connected") *** Failed to load theory "HOL-Analysis.Starlike" (unresolved "HOL-Analysis.Convex_Euclidean_Space") *** Failed to load theory "HOL-Analysis.Continuous_Extension" (unresolved "HOL-Analysis.Starlike") *** Failed to load theory "HOL-Analysis.Path_Connected" (unresolved "HOL-Analysis.Continuous_Extension") *** Failed to load theory "HOL-Analysis.Homeomorphism" (unresolved "HOL-Analysis.Path_Connected") *** Failed to load theory "HOL-Analysis.Brouwer_Fixpoint" (unresolved "HOL-Analysis.Homeomorphism", "HOL-Analysis.Path_Connected") *** Failed to load theory "HOL-Analysis.Tagged_Division" (unresolved "HOL-Analysis.Connected") *** Failed to load theory "HOL-Analysis.Extended_Real_Limits" (unresolved "HOL-Analysis.Topology_Euclidean_Space") *** Failed to load theory "HOL-Analysis.Summation_Tests" (unresolved "HOL-Analysis.Extended_Real_Limits") *** Failed to load theory "HOL-Analysis.Uniform_Limit" (unresolved "HOL-Analysis.Connected", "HOL-Analysis.Summation_Tests") *** Failed to load theory "HOL-Analysis.Bounded_Linear_Function" (unresolved "HOL-Analysis.Topology_Euclidean_Space", "HOL-Analysis.Uniform_Limit") *** Failed to load theory "HOL-Analysis.Derivative" (unresolved "HOL-Analysis.Bounded_Linear_Function", "HOL-Analysis.Brouwer_Fixpoint", "HOL-Analysis.Uniform_Limit") *** Failed to load theory "HOL-Analysis.Cartesian_Euclidean_Space" (unresolved "HOL-Analysis.Derivative") *** Failed to load theory "HOL-Analysis.Determinants" (unresolved "HOL-Analysis.Cartesian_Euclidean_Space") *** Failed to load theory "HOL-Analysis.Fashoda_Theorem" (unresolved "HOL-Analysis.Brouwer_Fixpoint", "HOL-Analysis.Cartesian_Euclidean_Space", "HOL-Analysis.Path_Connected") *** Failed to load theory "HOL-Analysis.Ordered_Euclidean_Space" (unresolved "HOL-Analysis.Cartesian_Euclidean_Space") *** Failed to load theory "HOL-Analysis.Arcwise_Connected" (unresolved "HOL-Analysis.Ordered_Euclidean_Space", "HOL-Analysis.Path_Connected") *** Failed to load theory "HOL-Analysis.Polytope" (unresolved "HOL-Analysis.Cartesian_Euclidean_Space") *** Failed to load theory "HOL-Analysis.Weierstrass_Theorems" (unresolved "HOL-Analysis.Derivative", "HOL-Analysis.Path_Connected", "HOL-Analysis.Uniform_Limit") *** Failed to load theory "HOL-Analysis.Borel_Space" (unresolved "HOL-Analysis.Derivative", "HOL-Analysis.Extended_Real_Limits", "HOL-Analysis.Ordered_Euclidean_Space") *** Failed to load theory "HOL-Analysis.Lipschitz" (unresolved "HOL-Analysis.Borel_Space") *** Failed to load theory "HOL-Analysis.Nonnegative_Lebesgue_Integration" (unresolved "HOL-Analysis.Borel_Space") *** Failed to load theory "HOL-Analysis.Binary_Product_Measure" (unresolved "HOL-Analysis.Nonnegative_Lebesgue_Integration") *** Failed to load theory "HOL-Analysis.Embed_Measure" (unresolved "HOL-Analysis.Binary_Product_Measure") *** Failed to load theory "HOL-Analysis.Finite_Product_Measure" (unresolved "HOL-Analysis.Binary_Product_Measure") *** Failed to load theory "HOL-Analysis.Bochner_Integration" (unresolved "HOL-Analysis.Finite_Product_Measure") *** Failed to load theory "HOL-Analysis.Complete_Measure" (unresolved "HOL-Analysis.Bochner_Integration") *** Failed to load theory "HOL-Analysis.Radon_Nikodym" (unresolved "HOL-Analysis.Bochner_Integration") *** Failed to load theory "HOL-Analysis.Set_Integral" (unresolved "HOL-Analysis.Radon_Nikodym") *** Failed to load theory "HOL-Analysis.Infinite_Set_Sum" (unresolved "HOL-Analysis.Set_Integral") *** Failed to load theory "HOL-Analysis.Regularity" (unresolved "HOL-Analysis.Borel_Space") *** Failed to load theory "HOL-Analysis.Function_Topology" (unresolved "HOL-Analysis.Bounded_Linear_Function", "HOL-Analysis.Finite_Product_Measure", "HOL-Analysis.Topology_Euclidean_Space") *** Failed to load theory "HOL-Analysis.Lebesgue_Measure" (unresolved "HOL-Analysis.Bochner_Integration", "HOL-Analysis.Complete_Measure", "HOL-Analysis.Finite_Product_Measure", "HOL-Analysis.Regularity", "HOL-Analysis.Summation_Tests") *** Failed to load theory "HOL-Analysis.Henstock_Kurzweil_Integration" (unresolved "HOL-Analysis.Lebesgue_Measure", "HOL-Analysis.Tagged_Division") *** Failed to load theory "HOL-Analysis.Bounded_Continuous_Function" (unresolved "HOL-Analysis.Henstock_Kurzweil_Integration") *** Failed to load theory "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" (unresolved "HOL-Analysis.Complete_Measure", "HOL-Analysis.Henstock_Kurzweil_Integration", "HOL-Analysis.Lebesgue_Measure", "HOL-Analysis.Set_Integral") *** Failed to load theory "HOL-Analysis.Complex_Analysis_Basics" (unresolved "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration") *** Failed to load theory "HOL-Analysis.Complex_Transcendental" (unresolved "HOL-Analysis.Complex_Analysis_Basics", "HOL-Analysis.Summation_Tests") *** Failed to load theory "HOL-Analysis.Generalised_Binomial_Theorem" (unresolved "HOL-Analysis.Complex_Transcendental", "HOL-Analysis.Summation_Tests") *** Failed to load theory "HOL-Analysis.Improper_Integral" (unresolved "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration") *** Failed to load theory "HOL-Analysis.Interval_Integral" (unresolved "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration") *** Failed to load theory "HOL-Analysis.Lebesgue_Integral_Substitution" (unresolved "HOL-Analysis.Interval_Integral") *** Failed to load theory "HOL-Analysis.Integral_Test" (unresolved "HOL-Analysis.Henstock_Kurzweil_Integration") *** Failed to load theory "HOL-Analysis.Harmonic_Numbers" (unresolved "HOL-Analysis.Complex_Transcendental", "HOL-Analysis.Integral_Test", "HOL-Analysis.Summation_Tests") *** Failed to load theory "HOL-Analysis.Cauchy_Integral_Theorem" (unresolved "HOL-Analysis.Complex_Transcendental", "HOL-Analysis.Ordered_Euclidean_Space", "HOL-Analysis.Weierstrass_Theorems") *** Failed to load theory "HOL-Analysis.Conformal_Mappings" (unresolved "HOL-Analysis.Cauchy_Integral_Theorem") *** Failed to load theory "HOL-Analysis.FPS_Convergence" (unresolved "HOL-Analysis.Conformal_Mappings", "HOL-Analysis.Generalised_Binomial_Theorem") *** Failed to load theory "HOL-Analysis.Gamma_Function" (unresolved "HOL-Analysis.Conformal_Mappings", "HOL-Analysis.Harmonic_Numbers", "HOL-Analysis.Summation_Tests") *** Failed to load theory "HOL-Analysis.Ball_Volume" (unresolved "HOL-Analysis.Gamma_Function", "HOL-Analysis.Lebesgue_Integral_Substitution") *** Failed to load theory "HOL-Analysis.Further_Topology" (unresolved "HOL-Analysis.Complex_Transcendental", "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration", "HOL-Analysis.Polytope", "HOL-Analysis.Weierstrass_Theorems") *** Failed to load theory "HOL-Analysis.Great_Picard" (unresolved "HOL-Analysis.Conformal_Mappings", "HOL-Analysis.Further_Topology") *** Failed to load theory "HOL-Analysis.Riemann_Mapping" (unresolved "HOL-Analysis.Great_Picard") *** Failed to load theory "HOL-Analysis.Jordan_Curve" (unresolved "HOL-Analysis.Arcwise_Connected", "HOL-Analysis.Further_Topology") *** Failed to load theory "HOL-Analysis.Winding_Numbers" (unresolved "HOL-Analysis.Jordan_Curve", "HOL-Analysis.Polytope", "HOL-Analysis.Riemann_Mapping") *** Failed to load theory "HOL-Analysis.Analysis" (unresolved "HOL-Analysis.Ball_Volume", "HOL-Analysis.Bounded_Continuous_Function", "HOL-Analysis.Complete_Measure", "HOL-Analysis.Conformal_Mappings", "HOL-Analysis.Determinants", "HOL-Analysis.Embed_Measure", "HOL-Analysis.FPS_Convergence", "HOL-Analysis.Fashoda_Theorem", "HOL-Analysis.Function_Topology", "HOL-Analysis.Gamma_Function", "HOL-Analysis.Generalised_Binomial_Theorem", "HOL-Analysis.Homeomorphism", "HOL-Analysis.Improper_Integral", "HOL-Analysis.Infinite_Set_Sum", "HOL-Analysis.Jordan_Curve", "HOL-Analysis.Lebesgue_Integral_Substitution", "HOL-Analysis.Lipschitz", "HOL-Analysis.Polytope", "HOL-Analysis.Radon_Nikodym", "HOL-Analysis.Riemann_Mapping", "HOL-Analysis.Weierstrass_Theorems", "HOL-Analysis.Winding_Numbers") *** Sort constraint topological_space inconsistent with default type for type variable "'a" (line 399 of "~~/src/HOL/Analysis/Topology_Euclidean_Space.thy") *** At command "class" (line 397 of "~~/src/HOL/Analysis/Topology_Euclidean_Space.thy")