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.Linear_Algebra")
### theory "HOL-Library.Disjoint_Sets"
### 0.247s elapsed time, 1.016s cpu time, 0.000s GC time
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")
consts
  enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"
### theory "HOL-Library.Infinite_Set"
### 0.356s elapsed time, 1.448s cpu time, 0.000s GC time
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: "(\<lambda>p. size (snd p)) <*mlex*> {}"
### 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
Found termination order: "size_list size <*mlex*> {}"
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.FuncSet"
### 0.678s elapsed time, 2.724s 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.Nat_Bijection"
### 0.434s elapsed time, 1.720s cpu time, 0.000s GC time
Loading theory "HOL-Library.Product_Plus" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space" via "HOL-Analysis.Product_Vector")
instantiation
  prod :: (zero, zero) zero
  zero_prod == zero_class.zero :: 'a \<times> 'b
instantiation
  prod :: (plus, plus) plus
  plus_prod == plus ::
    'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
instantiation
  prod :: (minus, minus) minus
  minus_prod == minus ::
    'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
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.750s elapsed time, 3.024s cpu time, 0.000s GC time
Loading theory "HOL-Library.Multiset" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Library.Permutations")
instantiation
  prod :: (uminus, uminus) uminus
  uminus_prod == uminus :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
### theory "HOL-Library.Product_Plus"
### 0.120s elapsed time, 0.480s 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.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Henstock_Kurzweil_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 \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool
  less_prod == less ::
    'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool
instantiation
  prod :: (inf, inf) inf
  inf_prod == inf ::
    'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
instantiation
  prod :: (sup, sup) sup
  sup_prod == sup ::
    'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
instantiation
  prod :: (top, top) top
  top_prod == top :: 'a \<times> 'b
instantiation
  prod :: (bot, bot) bot
  bot_prod == bot :: 'a \<times> 'b
instantiation
  prod :: (Inf, Inf) Inf
  Inf_prod == Inf :: ('a \<times> 'b) set \<Rightarrow> 'a \<times> 'b
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.724s elapsed time, 2.856s cpu time, 0.428s GC time
Loading theory "HOL-Library.Set_Algebras" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex")
instantiation
  prod :: (Sup, Sup) Sup
  Sup_prod == Sup :: ('a \<times> 'b) set \<Rightarrow> 'a \<times> 'b
instantiation
  set :: (plus) plus
  plus_set == plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set
instantiation
  set :: (times) times
  times_set == times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set
instantiation
  set :: (zero) zero
  zero_set == zero_class.zero :: 'a set
instantiation
  multiset :: (type) cancel_comm_monoid_add
  zero_multiset == zero_class.zero :: 'a multiset
  minus_multiset == minus ::
    'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset
  plus_multiset == plus ::
    'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset
instantiation
  set :: (one) one
  one_set == one_class.one :: 'a set
### theory "HOL-Library.Product_Order"
### 0.381s elapsed time, 1.496s cpu time, 0.428s 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.231s elapsed time, 0.936s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Inner_Product" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space")
### theory "HOL-Library.Phantom_Type"
### 0.771s elapsed time, 3.064s cpu time, 0.428s 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
class CARD_1 = type +
  assumes "CARD_1": "CARD('a) = 1"
### Additional type variable(s) in locale specification "countable": 'a
### Partially applied constant "Multiset.inf_subset_mset" on left hand side of equation, in theorem:
### semilattice_inf.Inf_fin (\<inter>#) (set (?x # ?xs)) \<equiv>
### fold (\<inter>#) ?xs ?x
class countable = type +
  assumes "ex_inj": "\<exists>to_nat. inj to_nat"
### Partially applied constant "Multiset.sup_subset_mset" on left hand side of equation, in theorem:
### semilattice_sup.Sup_fin (\<union>#) (set (?x # ?xs)) \<equiv>
### fold (\<union>#) ?xs ?x
class real_inner = dist_norm + real_vector + sgn_div_norm +
  uniformity_dist + open_uniformity +
  fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
  assumes "inner_commute": "\<And>x y. inner x y = inner y x"
    and
    "inner_add_left": "\<And>x y z. inner (x + y) z = inner x z + inner y z"
    and
    "inner_scaleR_left":
      "\<And>r x y. inner (r *\<^sub>R x) y = r * inner x y"
    and "inner_ge_zero": "\<And>x. 0 \<le> inner x x"
    and "inner_eq_zero_iff": "\<And>x. (inner x x = 0) = (x = (0::'a))"
    and "norm_eq_sqrt_inner": "\<And>x. norm x = sqrt (inner x x)"
### Additional type variable(s) in locale specification "card2": 'a
class card2 = finite +
  assumes "two_le_card": "2 \<le> 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
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
instantiation
  integer :: card_UNIV
  card_UNIV_integer == card_UNIV_class.card_UNIV :: (integer, nat) phantom
  finite_UNIV_integer == finite_UNIV :: (integer, bool) phantom
Proofs for inductive predicate(s) "finite_item"
  Proving monotonicity ...
  Proving the introduction rules ...
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
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
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
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 \<times> 'b, bool) phantom
instantiation
  prod :: (card_UNIV, card_UNIV) card_UNIV
  card_UNIV_prod == card_UNIV_class.card_UNIV ::
    ('a \<times> '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 \<Rightarrow> 'b, bool) phantom
instantiation
  fun :: (card_UNIV, card_UNIV) card_UNIV
  card_UNIV_fun == card_UNIV_class.card_UNIV ::
    ('a \<Rightarrow> 'b, nat) phantom
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
  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
  multiset :: (type) Inf
  Inf_multiset == Inf :: 'a multiset set \<Rightarrow> 'a multiset
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
val old_countable_datatype_tac = fn: Proof.context -> int -> tactic
instantiation
  multiset :: (type) Sup
  Sup_multiset == Sup :: 'a multiset set \<Rightarrow> 'a multiset
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
  real :: real_inner
  inner_real == inner :: real \<Rightarrow> real \<Rightarrow> real
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
  complex :: real_inner
  inner_complex == inner :: complex \<Rightarrow> complex \<Rightarrow> real
### 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
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
val countable_datatype_tac = fn: Proof.context -> thm -> thm Seq.seq
val countable_tac = fn: Proof.context -> int -> tactic
instantiation
  multiset :: (type) size
  size_multiset == size :: 'a multiset \<Rightarrow> nat
bundle inner_syntax
bundle no_inner_syntax
### theory "HOL-Analysis.Inner_Product"
### 0.909s elapsed time, 3.632s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.L2_Norm" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space")
### Code generator: dropping subsumed code equation
### List.coset [] \<subseteq> set [] \<equiv> False
locale comp_fun_commute
  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
  assumes "comp_fun_commute f"
### theory "HOL-Analysis.L2_Norm"
### 0.121s elapsed time, 0.476s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Operator_Norm" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Complex_Transcendental" via "HOL-Analysis.Complex_Analysis_Basics" via "HOL-Analysis.Derivative")
### theory "HOL-Library.Countable"
### 1.228s elapsed time, 4.900s cpu time, 0.000s 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.026s elapsed time, 4.080s cpu time, 0.000s 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")
consts
  mset :: "'a list \<Rightarrow> 'a multiset"
### theory "HOL-Analysis.Operator_Norm"
### 0.131s elapsed time, 0.516s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Poly_Roots" (required by "HOL-Analysis.Analysis")
### theory "HOL-Analysis.Poly_Roots"
### 0.135s elapsed time, 0.540s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Product_Vector" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space")
instantiation
  num1 :: CARD_1
instantiation
  num1 :: {comm_monoid_mult,numeral,comm_ring}
  uminus_num1 == uminus :: num1 \<Rightarrow> num1
  zero_num1 == zero_class.zero :: num1
  minus_num1 == minus :: num1 \<Rightarrow> num1 \<Rightarrow> num1
  plus_num1 == plus :: num1 \<Rightarrow> num1 \<Rightarrow> num1
  one_num1 == one_class.one :: num1
  times_num1 == times :: num1 \<Rightarrow> num1 \<Rightarrow> num1
instantiation
  num1 :: linorder
  less_eq_num1 == less_eq :: num1 \<Rightarrow> num1 \<Rightarrow> bool
  less_num1 == less :: num1 \<Rightarrow> num1 \<Rightarrow> bool
class linorder = order +
  assumes "linear": "\<And>x y. x \<le> y \<or> y \<le> x"
locale mod_type
  fixes n :: "int"
    and Rep :: "'a \<Rightarrow> int"
    and Abs :: "int \<Rightarrow> 'a"
  assumes "mod_type n Rep Abs"
locale mod_ring
  fixes n :: "int"
    and Rep :: "'a \<Rightarrow> int"
    and Abs :: "int \<Rightarrow> 'a"
  assumes "mod_ring n Rep Abs"
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 \<Rightarrow> 'a bit0
  times_bit0 == times :: 'a bit0 \<Rightarrow> 'a bit0 \<Rightarrow> 'a bit0
  plus_bit0 == plus :: 'a bit0 \<Rightarrow> 'a bit0 \<Rightarrow> 'a bit0
  one_bit0 == one_class.one :: 'a bit0
  minus_bit0 == minus :: 'a bit0 \<Rightarrow> 'a bit0 \<Rightarrow> 'a bit0
  zero_bit1 == zero_class.zero :: 'a bit1
  uminus_bit1 == uminus :: 'a bit1 \<Rightarrow> 'a bit1
  times_bit1 == times :: 'a bit1 \<Rightarrow> 'a bit1 \<Rightarrow> 'a bit1
  plus_bit1 == plus :: 'a bit1 \<Rightarrow> 'a bit1 \<Rightarrow> 'a bit1
  one_bit1 == one_class.one :: 'a bit1
  minus_bit1 == minus :: 'a bit1 \<Rightarrow> 'a bit1 \<Rightarrow> 'a bit1
locale comm_monoid_mset
  fixes
    f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
      (infixl \<open>\<^bold>*\<close> 70)
    and z :: "'a"  (\<open>\<^bold>1\<close>)
  assumes "comm_monoid_mset (\<^bold>*) \<^bold>1"
locale module_prod
  fixes s1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and s2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
  assumes "module_prod s1 s2"
class comm_monoid_add = ab_semigroup_add + monoid_add +
  assumes "add_0": "\<And>a. (0::'a) + a = a"
instantiation
  bit0 :: (finite) linorder
  bit1 :: (finite) linorder
  less_eq_bit0 == less_eq ::
    'a bit0 \<Rightarrow> 'a bit0 \<Rightarrow> bool
  less_bit0 == less :: 'a bit0 \<Rightarrow> 'a bit0 \<Rightarrow> bool
  less_eq_bit1 == less_eq ::
    'a bit1 \<Rightarrow> 'a bit1 \<Rightarrow> bool
  less_bit1 == less :: 'a bit1 \<Rightarrow> 'a bit1 \<Rightarrow> bool
### theory "HOL-Library.Countable_Set"
### 0.573s elapsed time, 2.272s cpu time, 0.000s GC time
Loading theory "HOL-Library.Countable_Complete_Lattices" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Complex_Transcendental" via "HOL-Analysis.Complex_Analysis_Basics" via "HOL-Analysis.Derivative" 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")
class comm_monoid_add = ab_semigroup_add + monoid_add +
  assumes "add_0": "\<And>a. (0::'a) + a = a"
instantiation
  num0 :: equal
  equal_num0 == equal_class.equal ::
    num0 \<Rightarrow> num0 \<Rightarrow> bool
locale vector_space_prod
  fixes
    s1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
      (infixr \<open>*a\<close> 75)
    and
    s2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
      (infixr \<open>*b\<close> 75)
  assumes "vector_space_prod (*a) (*b)"
instantiation
  num1 :: equal
  equal_num1 == equal_class.equal ::
    num1 \<Rightarrow> num1 \<Rightarrow> bool
instantiation
  prod :: (real_vector, real_vector) real_vector
  scaleR_prod == scaleR ::
    real \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
instantiation
  num1 :: enum
  enum_num1 == enum_class.enum :: num1 list
  enum_all_num1 == enum_class.enum_all ::
    (num1 \<Rightarrow> bool) \<Rightarrow> bool
  enum_ex_num1 == enum_class.enum_ex ::
    (num1 \<Rightarrow> bool) \<Rightarrow> bool
class canonically_ordered_monoid_add = ordered_comm_monoid_add +
  assumes "le_iff_add": "\<And>a b. (a \<le> b) = (\<exists>c. b = a + c)"
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
  prod :: (metric_space, metric_space) dist
  dist_prod == dist ::
    'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> real
instantiation
  prod :: (metric_space, metric_space) uniformity_dist
  uniformity_prod == uniformity ::
    (('a \<times> 'b) \<times> 'a \<times> '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 \<times> 'b \<Rightarrow> 'a \<times> 'b
  norm_prod == norm :: 'a \<times> 'b \<Rightarrow> real
instantiation
  bit0 :: (finite) equal
  bit1 :: (finite) equal
  equal_bit0 == equal_class.equal ::
    'a bit0 \<Rightarrow> 'a bit0 \<Rightarrow> bool
  equal_bit1 == equal_class.equal ::
    'a bit1 \<Rightarrow> 'a bit1 \<Rightarrow> bool
instantiation
  bit0 :: (finite) enum
  enum_bit0 == enum_class.enum :: 'a bit0 list
  enum_all_bit0 == enum_class.enum_all ::
    ('a bit0 \<Rightarrow> bool) \<Rightarrow> bool
  enum_ex_bit0 == enum_class.enum_ex ::
    ('a bit0 \<Rightarrow> bool) \<Rightarrow> bool
instantiation
  bit1 :: (finite) enum
  enum_bit1 == enum_class.enum :: 'a bit1 list
  enum_all_bit1 == enum_class.enum_all ::
    ('a bit1 \<Rightarrow> bool) \<Rightarrow> bool
  enum_ex_bit1 == enum_class.enum_ex ::
    ('a bit1 \<Rightarrow> bool) \<Rightarrow> bool
class countable_complete_lattice = Inf + Sup + lattice + bot + top +
  assumes
    "ccInf_lower":
      "\<And>A x.
          \<lbrakk>countable A; x \<in> A\<rbrakk>
          \<Longrightarrow> Inf A \<le> x"
  assumes
    "ccInf_greatest":
      "\<And>A z.
          \<lbrakk>countable A;
           \<And>x. x \<in> A \<Longrightarrow> z \<le> x\<rbrakk>
          \<Longrightarrow> z \<le> Inf A"
  assumes
    "ccSup_upper":
      "\<And>A x.
          \<lbrakk>countable A; x \<in> A\<rbrakk>
          \<Longrightarrow> x \<le> Sup A"
  assumes
    "ccSup_least":
      "\<And>A z.
          \<lbrakk>countable A;
           \<And>x. x \<in> A \<Longrightarrow> x \<le> z\<rbrakk>
          \<Longrightarrow> Sup A \<le> z"
  assumes "ccInf_empty": "Inf {} = top"
  assumes "ccSup_empty": "Sup {} = bot"
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
### theory "HOL-Library.Numeral_Type"
### 1.178s elapsed time, 4.604s cpu time, 0.864s GC time
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")
class comm_monoid_mult = ab_semigroup_mult + monoid_mult + dvd +
  assumes "mult_1": "\<And>a. (1::'a) * a = a"
locale finite_dimensional_vector_space_prod
  fixes
    s1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
      (infixr \<open>*a\<close> 75)
    and
    s2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
      (infixr \<open>*b\<close> 75)
    and B1 :: "'b set"
    and B2 :: "'c set"
  assumes "finite_dimensional_vector_space_prod (*a) (*b) B1 B2"
### theory "HOL-Analysis.Product_Vector"
### 1.179s elapsed time, 4.612s cpu time, 0.864s GC time
Loading theory "HOL-Analysis.Continuum_Not_Denumerable" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Abstract_Euclidean_Space" via "HOL-Analysis.Homotopy")
### theory "HOL-Library.Set_Idioms"
### 0.226s elapsed time, 0.908s 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-Analysis.Continuum_Not_Denumerable"
### 0.264s elapsed time, 1.060s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Elementary_Topology" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Connected" via "HOL-Analysis.Abstract_Topology_2")
class linorder = order +
  assumes "linear": "\<And>x y. x \<le> y \<or> y \<le> x"
class countable_complete_distrib_lattice = countable_complete_lattice +
  assumes
    "sup_ccInf":
      "\<And>B a.
          countable B \<Longrightarrow> sup a (Inf B) = Inf (sup a ` B)"
  assumes
    "inf_ccSup":
      "\<And>B a.
          countable B \<Longrightarrow> inf a (Sup B) = Sup (inf a ` B)"
instantiation
  multiset :: (preorder) order
  less_eq_multiset == less_eq ::
    'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool
  less_multiset == less ::
    'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool
instantiation
  multiset :: (preorder) ordered_ab_semigroup_add
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 ...
Found termination order: "(\<lambda>p. length (fst p)) <*mlex*> {}"
class topological_space = open +
  assumes "open_UNIV": "open UNIV"
  assumes
    "open_Int":
      "\<And>S T.
          \<lbrakk>open S; open T\<rbrakk>
          \<Longrightarrow> open (S \<inter> T)"
  assumes
    "open_Union": "\<And>K. Ball K open \<Longrightarrow> open (\<Union> K)"
instantiation
  multiset :: (equal) equal
  equal_multiset == equal_class.equal ::
    'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool
instantiation
  multiset :: (random) random
  random_multiset == random_class.random ::
    natural
    \<Rightarrow> natural \<times> natural
                  \<Rightarrow> ('a multiset \<times>
                                 (unit \<Rightarrow> term)) \<times>
                                natural \<times> natural
locale countable_basis
  fixes p :: "'a set \<Rightarrow> bool"
    and B :: "'a set set"
  assumes "countable_basis p B"
class second_countable_topology = topological_space +
  assumes
    "ex_countable_subbasis":
      "\<exists>B. countable B \<and> open = generate_topology B"
### theory "HOL-Library.Countable_Complete_Lattices"
### 2.083s elapsed time, 8.252s cpu time, 0.864s GC time
Loading theory "HOL-Analysis.Euclidean_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Linear_Algebra")
instantiation
  multiset :: (full_exhaustive) full_exhaustive
  full_exhaustive_multiset == full_exhaustive_class.full_exhaustive ::
    ('a multiset \<times> (unit \<Rightarrow> term)
     \<Rightarrow> (bool \<times> term list) option)
    \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option
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 ...
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.765s elapsed time, 18.876s cpu time, 2.052s 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")
class euclidean_space = real_inner +
  fixes Basis :: "'a set"
  assumes "nonempty_Basis": "Basis \<noteq> {}"
  assumes "finite_Basis": "finite Basis"
  assumes
    "inner_Basis":
      "\<And>u v.
          \<lbrakk>u \<in> Basis; v \<in> Basis\<rbrakk>
          \<Longrightarrow> inner u v = (if u = v then 1 else 0)"
  assumes
    "euclidean_all_zero_iff":
      "\<And>x. (\<forall>u\<in>Basis. inner x u = 0) = (x = (0::'a))"
### Ignoring duplicate rewrite rule:
### homeomorphic_map ?X1 ?Y1 id \<equiv> ?Y1 = ?X1
### theory "HOL-Analysis.Elementary_Topology"
### 2.131s elapsed time, 8.496s cpu time, 0.760s GC time
Loading theory "HOL-Library.Permutations" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants")
class normalization_semidom = algebraic_semidom +
  semidom_divide_unit_factor +
  fixes normalize :: "'a \<Rightarrow> 'a"
  assumes
    "unit_factor_mult_normalize": "\<And>a. unit_factor a * normalize a = a"
    and "normalize_0": "normalize (0::'a) = (0::'a)"
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 semiring_gcd = gcd + normalization_semidom +
  assumes "gcd_dvd1": "\<And>a b. gcd a b dvd a"
    and "gcd_dvd2": "\<And>a b. gcd a b dvd b"
    and
    "gcd_greatest":
      "\<And>c a b.
          \<lbrakk>c dvd a; c dvd b\<rbrakk>
          \<Longrightarrow> c dvd gcd a b"
    and "normalize_gcd": "\<And>a b. normalize (gcd a b) = gcd a b"
    and "lcm_gcd": "\<And>a b. lcm a b = normalize (a * b) div gcd a b"
instantiation
  real :: euclidean_space
  Basis_real == Basis :: real set
instantiation
  complex :: euclidean_space
  Basis_complex == Basis :: complex set
instantiation
  prod :: (real_inner, real_inner) real_inner
  inner_prod == inner ::
    'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> real
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 ...
instantiation
  prod :: (euclidean_space, euclidean_space) euclidean_space
  Basis_prod == Basis :: ('a \<times> 'b) set
### theory "HOL-Analysis.Euclidean_Space"
### 2.203s elapsed time, 8.708s cpu time, 1.572s 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: "(\<lambda>p. size_list size (fst p)) <*mlex*> {}"
### theory "HOL-Library.Permutations"
### 1.118s elapsed time, 4.404s cpu time, 0.812s GC time
Loading theory "HOL-Analysis.Linear_Algebra" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex")
### theory "HOL-Analysis.Abstract_Topology"
### 3.463s elapsed time, 13.756s cpu time, 1.572s GC time
Loading theory "HOL-Analysis.Abstract_Limits" (required by "HOL-Analysis.Analysis")
class factorial_semiring = normalization_semidom +
  assumes
    "prime_factorization_exists":
      "\<And>x.
          x \<noteq> (0::'a) \<Longrightarrow>
          \<exists>A.
             (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and>
             prod_mset A = normalize x"
### theory "HOL-Analysis.Abstract_Limits"
### 0.276s elapsed time, 1.108s cpu time, 0.000s GC time
Loading theory "HOL-Library.Discrete" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Complex_Transcendental" via "HOL-Analysis.Complex_Analysis_Basics" via "HOL-Analysis.Derivative" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests")
class factorial_semiring = normalization_semidom +
  assumes
    "prime_factorization_exists":
      "\<And>x.
          x \<noteq> (0::'a) \<Longrightarrow>
          \<exists>A.
             (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and>
             prod_mset A = normalize x"
### Rewrite rule not in simpset:
### Wellfounded.accp log_rel ?n1 \<Longrightarrow>
### log ?n1 \<equiv> if ?n1 < 2 then 0 else Suc (log (?n1 div 2))
Found termination order: "size <*mlex*> {}"
### theory "HOL-Library.Discrete"
### 0.192s elapsed time, 0.772s 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")
class real_inner = real_normed_vector +
  fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
  assumes "inner_commute": "\<And>x y. x \<bullet> y = y \<bullet> x"
    and
    "inner_add_left":
      "\<And>x y z. (x + y) \<bullet> z = x \<bullet> z + y \<bullet> z"
    and
    "inner_scaleR_left":
      "\<And>r x y. r *\<^sub>R x \<bullet> y = r * (x \<bullet> y)"
    and "inner_ge_zero": "\<And>x. 0 \<le> x \<bullet> x"
    and "inner_eq_zero_iff": "\<And>x. (x \<bullet> x = 0) = (x = (0::'a))"
    and "norm_eq_sqrt_inner": "\<And>x. norm x = sqrt (x \<bullet> x)"
### theory "HOL-Library.Indicator_Function"
### 0.385s elapsed time, 1.544s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Abstract_Topology_2" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Connected")
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 \<Rightarrow> ('a, 'b) vec \<Rightarrow> ('a, 'b) vec
instantiation
  vec :: (minus, finite) minus
  minus_vec == minus ::
    ('a, 'b) vec \<Rightarrow> ('a, 'b) vec \<Rightarrow> ('a, 'b) vec
instantiation
  vec :: (uminus, finite) uminus
  uminus_vec == uminus :: ('a, 'b) vec \<Rightarrow> ('a, 'b) vec
instantiation
  vec :: (times, finite) times
  times_vec == times ::
    ('a, 'b) vec \<Rightarrow> ('a, 'b) vec \<Rightarrow> ('a, 'b) vec
instantiation
  vec :: (one, finite) one
  one_vec == one_class.one :: ('a, 'b) vec
instantiation
  vec :: (ord, finite) ord
  less_eq_vec == less_eq ::
    ('a, 'b) vec \<Rightarrow> ('a, 'b) vec \<Rightarrow> bool
  less_vec == less ::
    ('a, 'b) vec \<Rightarrow> ('a, 'b) vec \<Rightarrow> bool
instantiation
  vec :: (real_vector, finite) real_vector
  scaleR_vec == scaleR ::
    real \<Rightarrow> ('a, 'b) vec \<Rightarrow> ('a, 'b) vec
### theory "HOL-Analysis.Linear_Algebra"
### 1.109s elapsed time, 4.452s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Convex" (required by "HOL-Analysis.Analysis")
instantiation
  vec :: (topological_space, finite) topological_space
  open_vec == open :: ('a, 'b) vec set \<Rightarrow> bool
instantiation
  vec :: (metric_space, finite) dist
  dist_vec == dist ::
    ('a, 'b) vec \<Rightarrow> ('a, 'b) vec \<Rightarrow> real
instantiation
  vec :: (metric_space, finite) uniformity_dist
  uniformity_vec == uniformity ::
    (('a, 'b) vec \<times> ('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 \<Rightarrow> ('a, 'b) vec
  norm_vec == norm :: ('a, 'b) vec \<Rightarrow> real
instantiation
  vec :: (real_inner, finite) real_inner
  inner_vec == inner ::
    ('a, 'b) vec \<Rightarrow> ('a, 'b) vec \<Rightarrow> real
instantiation
  vec :: (euclidean_space, finite) euclidean_space
  Basis_vec == Basis :: ('a, 'b) vec set
### Ignoring duplicate rewrite rule:
### vec_lambda ?g1 $ ?i1 \<equiv> ?g1 ?i1
### theory "HOL-Analysis.Finite_Cartesian_Product"
### 2.173s elapsed time, 8.672s cpu time, 0.656s GC time
Loading theory "HOL-Analysis.Cartesian_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants")
class factorial_semiring_gcd = factorial_semiring + Gcd +
  assumes "gcd_eq_gcd_factorial": "\<And>a b. gcd a b = gcd_factorial a b"
    and "lcm_eq_lcm_factorial": "\<And>a b. lcm a b = lcm_factorial a b"
    and "Gcd_eq_Gcd_factorial": "\<And>A. Gcd A = Gcd_factorial A"
    and "Lcm_eq_Lcm_factorial": "\<And>A. Lcm A = Lcm_factorial A"
### theory "HOL-Analysis.Abstract_Topology_2"
### 1.706s elapsed time, 6.788s cpu time, 0.656s GC time
Loading theory "HOL-Analysis.Connected" (required by "HOL-Analysis.Analysis")
locale linear_first_finite_dimensional_vector_space
  fixes
    scaleB :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
      (infixr \<open>*b\<close> 75)
    and
    scaleC :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
      (infixr \<open>*c\<close> 75)
    and BasisB :: "'b set"
    and f :: "'b \<Rightarrow> 'c"
  assumes "linear_first_finite_dimensional_vector_space (*b) (*c) BasisB f"
### theory "HOL-Analysis.Convex"
### 1.695s elapsed time, 6.740s cpu time, 0.656s GC time
Loading theory "HOL-Analysis.Elementary_Metric_Spaces" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Abstract_Euclidean_Space" via "HOL-Analysis.Homotopy" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space" via "HOL-Analysis.Topology_Euclidean_Space" via "HOL-Analysis.Elementary_Normed_Spaces")
### theory "HOL-Analysis.Connected"
### 0.331s elapsed time, 1.320s cpu time, 0.000s GC time
Loading theory "HOL-Library.Liminf_Limsup" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Complex_Transcendental" via "HOL-Analysis.Complex_Analysis_Basics" via "HOL-Analysis.Derivative" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests" via "HOL-Library.Extended_Real")
### theory "HOL-Analysis.Cartesian_Space"
### 2.577s elapsed time, 9.492s cpu time, 4.924s GC time
Loading theory "HOL-Analysis.Determinants" (required by "HOL-Analysis.Analysis")
### theory "HOL-Library.Liminf_Limsup"
### 2.015s elapsed time, 7.232s cpu time, 4.924s 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.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Complex_Transcendental" via "HOL-Analysis.Complex_Analysis_Basics")
### theory "HOL-Library.Nonpos_Ints"
### 0.221s elapsed time, 0.864s cpu time, 0.000s GC time
Loading theory "HOL-Library.Order_Continuity" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Complex_Transcendental" via "HOL-Analysis.Complex_Analysis_Basics" via "HOL-Analysis.Derivative" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests" via "HOL-Library.Extended_Real" via "HOL-Library.Extended_Nat")
class heine_borel = metric_space +
  assumes
    "bounded_imp_convergent_subsequence":
      "\<And>f.
          bounded (range f) \<Longrightarrow>
          \<exists>l r.
             strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
### theory "HOL-Analysis.Determinants"
### 1.024s elapsed time, 4.084s cpu time, 0.420s 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.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Complex_Transcendental")
locale periodic_fun
  fixes f :: "'a \<Rightarrow> 'b"
    and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    and gm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    and g1 :: "'a \<Rightarrow> 'a"
    and gn1 :: "'a \<Rightarrow> 'a"
  assumes "periodic_fun f g gm g1 gn1"
locale periodic_fun_simple
  fixes f :: "'a \<Rightarrow> 'b"
    and period :: "'a"
  assumes "periodic_fun_simple f period"
locale periodic_fun_simple'
  fixes f :: "'a \<Rightarrow> 'b"
  assumes "periodic_fun_simple' f"
### theory "HOL-Library.Periodic_Fun"
### 0.160s elapsed time, 0.644s cpu time, 0.000s GC time
Loading theory "HOL-Library.Sum_of_Squares" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Abstract_Euclidean_Space" via "HOL-Analysis.Homotopy" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space" via "HOL-Analysis.Topology_Euclidean_Space" via "HOL-Analysis.Norm_Arith")
### theory "HOL-Computational_Algebra.Factorial_Ring"
### 7.808s elapsed time, 30.328s cpu time, 6.812s 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-Library.Order_Continuity"
### 0.802s elapsed time, 3.232s cpu time, 0.420s GC time
Loading theory "HOL-Library.Extended_Nat" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Complex_Transcendental" via "HOL-Analysis.Complex_Analysis_Basics" via "HOL-Analysis.Derivative" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests" via "HOL-Library.Extended_Real")
### Rule already declared as safe introduction (intro!)
### True
### Ignoring duplicate introduction (intro)
### True
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 ...
### theory "HOL-Analysis.Elementary_Metric_Spaces"
### 3.437s elapsed time, 12.916s cpu time, 5.344s GC time
Loading theory "HOL-Analysis.Elementary_Normed_Spaces" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Abstract_Euclidean_Space" via "HOL-Analysis.Homotopy" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space" via "HOL-Analysis.Topology_Euclidean_Space")
### No equation for constructor "Extended_Nat.infinity_class.infinity"
### in definition of function "the_enat"
consts
  the_enat :: "enat \<Rightarrow> 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 \<Rightarrow> enat \<Rightarrow> enat
instantiation
  enat :: {comm_semiring_1,semiring_no_zero_divisors}
  times_enat == times :: enat \<Rightarrow> enat \<Rightarrow> enat
instantiation
  enat :: minus
  minus_enat == minus :: enat \<Rightarrow> enat \<Rightarrow> enat
instantiation
  enat :: linordered_ab_semigroup_add
  less_eq_enat == less_eq :: enat \<Rightarrow> enat \<Rightarrow> bool
  less_enat == less :: enat \<Rightarrow> enat \<Rightarrow> bool
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 \<Rightarrow> enat
  Sup_enat == Sup :: enat set \<Rightarrow> enat
  sup_enat == sup :: enat \<Rightarrow> enat \<Rightarrow> enat
  inf_enat == inf :: enat \<Rightarrow> enat \<Rightarrow> enat
### theory "HOL-Library.Extended_Nat"
### 0.913s elapsed time, 3.616s cpu time, 0.000s GC time
Loading theory "HOL-Library.Extended_Real" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Complex_Transcendental" via "HOL-Analysis.Complex_Analysis_Basics" via "HOL-Analysis.Derivative" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests")
instantiation
  enat :: linorder_topology
  open_enat == open :: enat set \<Rightarrow> bool
### theory "HOL-Analysis.Elementary_Normed_Spaces"
### 1.311s elapsed time, 5.200s cpu time, 0.648s GC time
instantiation
  ereal :: uminus
  uminus_ereal == uminus :: ereal \<Rightarrow> ereal
Found termination order: "{}"
instantiation
  ereal :: infinity
  infinity_ereal == infinity :: ereal
instantiation
  ereal :: abs
  abs_ereal == abs :: ereal \<Rightarrow> 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 \<Rightarrow> ereal \<Rightarrow> ereal
instantiation
  ereal :: linorder
  less_eq_ereal == less_eq :: ereal \<Rightarrow> ereal \<Rightarrow> bool
  less_ereal == less :: ereal \<Rightarrow> ereal \<Rightarrow> bool
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"
### 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
instantiation
  ereal :: {comm_monoid_mult,sgn}
  sgn_ereal == sgn :: ereal \<Rightarrow> ereal
  times_ereal == times :: ereal \<Rightarrow> ereal \<Rightarrow> ereal
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
instantiation
  ereal :: minus
  minus_ereal == minus :: ereal \<Rightarrow> ereal \<Rightarrow> ereal
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
instantiation
  ereal :: inverse
  inverse_ereal == inverse :: ereal \<Rightarrow> ereal
  divide_ereal == divide :: ereal \<Rightarrow> ereal \<Rightarrow> ereal
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.469s elapsed time, 13.832s cpu time, 1.160s GC time
Loading theory "HOL-Analysis.Norm_Arith" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Abstract_Euclidean_Space" via "HOL-Analysis.Homotopy" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space" via "HOL-Analysis.Topology_Euclidean_Space")
instantiation
  ereal :: lattice
  inf_ereal == inf :: ereal \<Rightarrow> ereal \<Rightarrow> ereal
  sup_ereal == sup :: ereal \<Rightarrow> ereal \<Rightarrow> ereal
instantiation
  ereal :: complete_lattice
  Inf_ereal == Inf :: ereal set \<Rightarrow> ereal
  Sup_ereal == Sup :: ereal set \<Rightarrow> ereal
  bot_ereal == bot :: ereal
  top_ereal == top :: ereal
### 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
instantiation
  ereal :: linear_continuum_topology
  open_ereal == open :: ereal set \<Rightarrow> bool
### theory "HOL-Analysis.Norm_Arith"
### 0.307s elapsed time, 1.232s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Topology_Euclidean_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Abstract_Euclidean_Space" via "HOL-Analysis.Homotopy" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space")
### theory "HOL-Library.Extended_Real"
### 3.523s elapsed time, 14.108s cpu time, 1.160s GC time
Loading theory "HOL-Library.Extended_Nonnegative_Real" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Complex_Transcendental" via "HOL-Analysis.Complex_Analysis_Basics" via "HOL-Analysis.Derivative" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests" via "HOL-Analysis.Extended_Real_Limits")
instantiation
  ennreal :: complete_linorder
  Inf_ennreal == Inf :: ennreal set \<Rightarrow> ennreal
  Sup_ennreal == Sup :: ennreal set \<Rightarrow> ennreal
  bot_ennreal == bot :: ennreal
  sup_ennreal == sup :: ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal
  top_ennreal == top :: ennreal
  inf_ennreal == inf :: ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal
  less_eq_ennreal == less_eq ::
    ennreal \<Rightarrow> ennreal \<Rightarrow> bool
  less_ennreal == less :: ennreal \<Rightarrow> ennreal \<Rightarrow> 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 \<Rightarrow> ennreal \<Rightarrow> ennreal
  one_ennreal == one_class.one :: ennreal
  times_ennreal == times ::
    ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal
instantiation
  ennreal :: minus
  minus_ennreal == minus ::
    ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal
instantiation
  ennreal :: inverse
  inverse_ennreal == inverse :: ennreal \<Rightarrow> ennreal
  divide_ennreal == divide ::
    ennreal \<Rightarrow> ennreal \<Rightarrow> 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
instantiation
  ennreal :: linear_continuum_topology
  open_ennreal == open :: ennreal set \<Rightarrow> bool
### theory "HOL-Library.Extended_Nonnegative_Real"
### 1.971s elapsed time, 7.924s cpu time, 1.048s 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.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Henstock_Kurzweil_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")
### theory "HOL-Analysis.Topology_Euclidean_Space"
### 2.853s elapsed time, 11.468s cpu time, 1.048s GC time
Loading theory "HOL-Analysis.Convex_Euclidean_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Abstract_Euclidean_Space" via "HOL-Analysis.Homotopy" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Starlike")
Loading theory "HOL-Analysis.Extended_Real_Limits" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Complex_Transcendental" via "HOL-Analysis.Complex_Analysis_Basics" via "HOL-Analysis.Derivative" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests")
### theory "HOL-Computational_Algebra.Euclidean_Algorithm"
### 6.818s elapsed time, 27.288s cpu time, 2.208s 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-Computational_Algebra.Primes"
### 0.272s elapsed time, 1.100s cpu time, 0.000s GC time
Loading theory "HOL-Computational_Algebra.Formal_Power_Series" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.FPS_Convergence")
### Ignoring duplicate rewrite rule:
### interior (ball ?x1 ?e1) \<equiv> ball ?x1 ?e1
locale subset_class
  fixes \<Omega> :: "'a set"
    and M :: "'a set set"
  assumes "subset_class \<Omega> M"
locale semiring_of_sets
  fixes \<Omega> :: "'a set"
    and M :: "'a set set"
  assumes "semiring_of_sets \<Omega> M"
locale ring_of_sets
  fixes \<Omega> :: "'a set"
    and M :: "'a set set"
  assumes "ring_of_sets \<Omega> M"
locale algebra
  fixes \<Omega> :: "'a set"
    and M :: "'a set set"
  assumes "algebra \<Omega> M"
locale sigma_algebra
  fixes \<Omega> :: "'a set"
    and M :: "'a set set"
  assumes "sigma_algebra \<Omega> 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 ...
### theory "HOL-Analysis.Extended_Real_Limits"
### 1.026s elapsed time, 4.132s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Summation_Tests" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Complex_Transcendental" via "HOL-Analysis.Complex_Analysis_Basics" via "HOL-Analysis.Derivative" via "HOL-Analysis.Uniform_Limit")
### theory "HOL-Analysis.Convex_Euclidean_Space"
### 1.024s elapsed time, 4.120s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Starlike" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Abstract_Euclidean_Space" via "HOL-Analysis.Homotopy" via "HOL-Analysis.Path_Connected")
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 \<Rightarrow> 'a fps \<Rightarrow> 'a fps
instantiation
  fps :: (minus) minus
  minus_fps == minus :: 'a fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps
instantiation
  fps :: (uminus) uminus
  uminus_fps == uminus :: 'a fps \<Rightarrow> 'a fps
instantiation
  fps :: ({comm_monoid_add,times}) times
  times_fps == times :: 'a fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps
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 \<Omega> :: "'a set"
    and M :: "'a set set"
  assumes "Dynkin_system \<Omega> M"
instantiation
  fps :: (zero) unit_factor
  unit_factor_fps == unit_factor :: 'a fps \<Rightarrow> 'a fps
instantiation
  fps :: ({minus,zero}) dist
  dist_fps == dist :: 'a fps \<Rightarrow> 'a fps \<Rightarrow> real
instantiation
  fps :: (group_add) metric_space
  uniformity_fps == uniformity :: ('a fps \<times> 'a fps) filter
  open_fps == open :: 'a fps set \<Rightarrow> bool
### theory "HOL-Analysis.Summation_Tests"
### 1.082s elapsed time, 4.360s cpu time, 1.068s GC time
Loading theory "HOL-Analysis.Uniform_Limit" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Complex_Transcendental" via "HOL-Analysis.Complex_Analysis_Basics" via "HOL-Analysis.Derivative")
Found termination order: "(\<lambda>p. size (snd (snd p))) <*mlex*> {}"
Found termination order: "(\<lambda>p. size (snd (snd p))) <*mlex*> {}"
instantiation
  fps :: ({inverse,comm_monoid_add,times,uminus}) inverse
  inverse_fps == inverse :: 'a fps \<Rightarrow> 'a fps
  divide_fps == divide :: 'a fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps
### theory "HOL-Analysis.Sigma_Algebra"
### 2.636s elapsed time, 10.608s cpu time, 1.068s 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.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Henstock_Kurzweil_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.Uniform_Limit"
### 0.666s elapsed time, 2.680s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Function_Topology" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Abstract_Euclidean_Space" via "HOL-Analysis.Homotopy" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.T1_Spaces" via "HOL-Analysis.Product_Topology")
instantiation
  fps :: ({inverse,uminus,comm_semiring_1}) modulo
  modulo_fps == modulo :: 'a fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps
instantiation
  fps :: (field) normalization_semidom
  normalize_fps == normalize :: 'a fps \<Rightarrow> 'a fps
instantiation
  fps :: (field) euclidean_ring_cancel
  euclidean_size_fps == euclidean_size :: 'a fps \<Rightarrow> nat
instantiation
  fps :: (field) euclidean_ring_gcd
  Gcd_fps == Gcd :: 'a fps set \<Rightarrow> 'a fps
  Lcm_fps == Lcm :: 'a fps set \<Rightarrow> 'a fps
  gcd_fps == gcd :: 'a fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps
  lcm_fps == lcm :: 'a fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps
### theory "HOL-Analysis.Measurable"
### 0.646s elapsed time, 2.600s 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.Conformal_Mappings" via "HOL-Analysis.Cauchy_Integral_Theorem" via "HOL-Analysis.Henstock_Kurzweil_Integration" via "HOL-Analysis.Lebesgue_Measure" via "HOL-Analysis.Finite_Product_Measure" via "HOL-Analysis.Binary_Product_Measure" via "HOL-Analysis.Nonnegative_Lebesgue_Integration")
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
instantiation
  fun :: (type, topological_space) topological_space
  open_fun == open :: ('a \<Rightarrow> 'b) set \<Rightarrow> bool
instantiation
  fun :: (countable, metric_space) metric_space
  dist_fun == dist ::
    ('a \<Rightarrow> 'b)
    \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> real
  uniformity_fun == uniformity ::
    (('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter
*** Interrupt