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.Infinite_Set" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Linear_Algebra")
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")
consts
  enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"
### theory "HOL-Library.Disjoint_Sets"
### 0.299s elapsed time, 1.224s 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")
### theory "HOL-Library.Infinite_Set"
### 0.347s elapsed time, 1.416s 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
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
Found termination order: "size_list size <*mlex*> {}"
### theory "HOL-Library.FuncSet"
### 0.624s elapsed time, 2.508s 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")
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.698s elapsed time, 2.824s 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.Nat_Bijection"
### 0.440s elapsed time, 1.756s 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
instantiation
  prod :: (uminus, uminus) uminus
  uminus_prod == uminus :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
### theory "HOL-Library.Product_Plus"
### 0.121s 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
  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
  prod :: (inf, inf) inf
  inf_prod == inf ::
    'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<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.729s elapsed time, 2.884s cpu time, 0.424s 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 \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
instantiation
  prod :: (top, top) top
  top_prod == top :: '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
  prod :: (bot, bot) bot
  bot_prod == bot :: 'a \<times> 'b
instantiation
  set :: (zero) zero
  zero_set == zero_class.zero :: 'a set
instantiation
  prod :: (Inf, Inf) Inf
  Inf_prod == Inf :: ('a \<times> 'b) set \<Rightarrow> 'a \<times> 'b
instantiation
  set :: (one) one
  one_set == one_class.one :: 'a set
instantiation
  prod :: (Sup, Sup) Sup
  Sup_prod == Sup :: ('a \<times> 'b) set \<Rightarrow> 'a \<times> 'b
### theory "HOL-Library.Product_Order"
### 0.366s elapsed time, 1.448s cpu time, 0.424s 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.258s elapsed time, 1.044s 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.825s elapsed time, 3.284s cpu time, 0.424s 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
### 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 CARD_1 = type +
  assumes "CARD_1": "CARD('a) = 1"
### 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
### Additional type variable(s) in locale specification "countable": 'a
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)"
class countable = type +
  assumes "ex_inj": "\<exists>to_nat. inj to_nat"
### 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)"
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
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
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
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 ...
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
  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
  multiset :: (type) Inf
  Inf_multiset == Inf :: 'a multiset set \<Rightarrow> 'a multiset
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
  multiset :: (type) Sup
  Sup_multiset == Sup :: 'a multiset set \<Rightarrow> 'a multiset
instantiation
  fun :: (card_UNIV, card_UNIV) card_UNIV
  card_UNIV_fun == card_UNIV_class.card_UNIV ::
    ('a \<Rightarrow> '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
val old_countable_datatype_tac = fn: Proof.context -> int -> tactic
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
  multiset :: (type) size
  size_multiset == size :: 'a multiset \<Rightarrow> nat
instantiation
  real :: real_inner
  inner_real == inner :: real \<Rightarrow> real \<Rightarrow> real
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
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
val countable_datatype_tac = fn: Proof.context -> thm -> thm Seq.seq
val countable_tac = fn: Proof.context -> int -> tactic
locale comp_fun_commute
  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
  assumes "comp_fun_commute f"
bundle inner_syntax
bundle no_inner_syntax
### theory "HOL-Analysis.Inner_Product"
### 0.918s elapsed time, 3.676s 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
consts
  mset :: "'a list \<Rightarrow> 'a multiset"
### 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.246s elapsed time, 4.972s 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.092s 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")
### theory "HOL-Analysis.Operator_Norm"
### 0.132s elapsed time, 0.516s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Poly_Roots" (required by "HOL-Analysis.Analysis")
class linorder = order +
  assumes "linear": "\<And>x y. x \<le> y \<or> y \<le> x"
### theory "HOL-Analysis.Poly_Roots"
### 0.138s elapsed time, 0.536s 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
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 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
class comm_monoid_add = ab_semigroup_add + monoid_add +
  assumes "add_0": "\<And>a. (0::'a) + a = a"
class comm_monoid_add = ab_semigroup_add + monoid_add +
  assumes "add_0": "\<And>a. (0::'a) + a = a"
class canonically_ordered_monoid_add = ordered_comm_monoid_add +
  assumes "le_iff_add": "\<And>a b. (a \<le> b) = (\<exists>c. b = a + c)"
locale module_prod
  fixes s1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and s2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
  assumes "module_prod s1 s2"
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.577s elapsed time, 2.260s 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")
instantiation
  num0 :: equal
  equal_num0 == equal_class.equal ::
    num0 \<Rightarrow> num0 \<Rightarrow> bool
instantiation
  num1 :: equal
  equal_num1 == equal_class.equal ::
    num1 \<Rightarrow> num1 \<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 :: 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
instantiation
  prod :: (real_vector, real_vector) real_vector
  scaleR_prod == scaleR ::
    real \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
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
  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
  prod :: (metric_space, metric_space) metric_space
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
  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
class comm_monoid_mult = ab_semigroup_mult + monoid_mult + dvd +
  assumes "mult_1": "\<And>a. (1::'a) * a = a"
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
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
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 :: ({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.201s elapsed time, 4.644s cpu time, 0.868s 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")
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-Library.Set_Idioms"
### 0.220s elapsed time, 0.884s 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.Product_Vector"
### 1.248s elapsed time, 4.852s cpu time, 0.868s GC time
Loading theory "HOL-Analysis.Continuum_Not_Denumerable" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Abstract_Euclidean_Space" via "HOL-Analysis.Homotopy")
class linorder = order +
  assumes "linear": "\<And>x y. x \<le> y \<or> y \<le> x"
### theory "HOL-Analysis.Continuum_Not_Denumerable"
### 0.270s elapsed time, 1.088s 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")
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 ...
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)"
Found termination order: "(\<lambda>p. length (fst p)) <*mlex*> {}"
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
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 :: (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
locale countable_basis
  fixes p :: "'a set \<Rightarrow> bool"
    and B :: "'a set set"
  assumes "countable_basis p B"
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 ...
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.311s elapsed time, 9.104s cpu time, 1.520s GC time
Loading theory "HOL-Analysis.Euclidean_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Linear_Algebra")
### theory "HOL-Library.Multiset"
### 4.648s elapsed time, 18.376s cpu time, 1.944s 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 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)"
### Ignoring duplicate rewrite rule:
### homeomorphic_map ?X1 ?Y1 id \<equiv> ?Y1 = ?X1
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))"
### theory "HOL-Analysis.Elementary_Topology"
### 2.154s elapsed time, 8.592s cpu time, 0.652s GC time
Loading theory "HOL-Library.Permutations" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants")
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"
Proofs for inductive predicate(s) "swapidseq"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "generate_topology_on"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
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
instantiation
  prod :: (euclidean_space, euclidean_space) euclidean_space
  Basis_prod == Basis :: ('a \<times> 'b) set
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"
Found termination order: "(\<lambda>p. size_list size (fst p)) <*mlex*> {}"
### theory "HOL-Analysis.Euclidean_Space"
### 1.929s elapsed time, 7.676s cpu time, 0.704s GC time
Loading theory "HOL-Analysis.Finite_Cartesian_Product" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space")
### theory "HOL-Analysis.Abstract_Topology"
### 3.363s elapsed time, 13.380s cpu time, 1.356s GC time
Loading theory "HOL-Analysis.Abstract_Limits" (required by "HOL-Analysis.Analysis")
### theory "HOL-Library.Permutations"
### 0.984s elapsed time, 3.884s cpu time, 0.704s GC time
Loading theory "HOL-Analysis.Linear_Algebra" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex")
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.273s elapsed time, 1.096s 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")
### 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.186s elapsed time, 0.748s 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.384s 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
### theory "HOL-Analysis.Linear_Algebra"
### 1.102s elapsed time, 4.428s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Convex" (required by "HOL-Analysis.Analysis")
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
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
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.Finite_Cartesian_Product"
### 2.211s elapsed time, 8.824s cpu time, 0.664s GC time
Loading theory "HOL-Analysis.Cartesian_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants")
### theory "HOL-Analysis.Abstract_Topology_2"
### 1.704s elapsed time, 6.788s cpu time, 0.664s 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.Connected"
### 0.317s elapsed time, 1.280s cpu time, 0.000s 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.Convex"
### 1.720s elapsed time, 6.856s cpu time, 0.664s 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.458s elapsed time, 9.136s cpu time, 4.704s GC time
Loading theory "HOL-Analysis.Determinants" (required by "HOL-Analysis.Analysis")
### theory "HOL-Library.Liminf_Limsup"
### 1.948s elapsed time, 7.064s cpu time, 4.704s 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.302s elapsed time, 1.224s cpu time, 0.364s 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-Computational_Algebra.Factorial_Ring"
### 7.415s elapsed time, 28.912s cpu time, 6.436s 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.Determinants"
### 0.906s elapsed time, 3.640s cpu time, 0.364s 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.127s elapsed time, 0.512s 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-Library.Order_Continuity"
### 0.608s elapsed time, 2.444s cpu time, 0.000s 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.248s elapsed time, 12.272s cpu time, 5.068s 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.870s elapsed time, 3.432s 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.178s elapsed time, 4.696s cpu time, 0.616s GC time
instantiation
  ereal :: uminus
  uminus_ereal == uminus :: ereal \<Rightarrow> ereal
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"
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
### 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
instantiation
  ereal :: inverse
  inverse_ereal == inverse :: ereal \<Rightarrow> ereal
  divide_ereal == divide :: 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
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.255s elapsed time, 13.000s cpu time, 1.056s 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
instantiation
  ereal :: linear_continuum_topology
  open_ereal == open :: ereal set \<Rightarrow> bool
### 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.294s elapsed time, 1.180s 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.232s elapsed time, 12.976s cpu time, 1.056s 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-Computational_Algebra.Euclidean_Algorithm"
### 6.220s elapsed time, 24.908s cpu time, 1.968s GC time
Loading theory "HOL-Computational_Algebra.Primes" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Jordan_Curve" via "HOL-Analysis.Arcwise_Connected")
Loading theory "HOL-Computational_Algebra.Formal_Power_Series" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.FPS_Convergence")
### theory "HOL-Library.Extended_Nonnegative_Real"
### 1.905s elapsed time, 7.644s cpu time, 0.912s 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.654s elapsed time, 10.660s cpu time, 0.912s 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")
### theory "HOL-Computational_Algebra.Primes"
### 0.270s elapsed time, 1.088s cpu time, 0.000s GC time
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")
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
### 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 ...
instantiation
  fps :: (zero) unit_factor
  unit_factor_fps == unit_factor :: 'a fps \<Rightarrow> 'a fps
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "HOL-Analysis.Convex_Euclidean_Space"
### 1.005s elapsed time, 4.048s 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 :: ({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.Extended_Real_Limits"
### 1.013s elapsed time, 4.076s 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")
Found termination order: "(\<lambda>p. size (snd (snd p))) <*mlex*> {}"
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 ...
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
locale Dynkin_system
  fixes \<Omega> :: "'a set"
    and M :: "'a set set"
  assumes "Dynkin_system \<Omega> M"
### theory "HOL-Analysis.Summation_Tests"
### 0.966s elapsed time, 3.884s cpu time, 1.000s 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")
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
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
### theory "HOL-Analysis.Sigma_Algebra"
### 2.565s elapsed time, 10.332s cpu time, 1.000s 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")
### theory "HOL-Analysis.Uniform_Limit"
### 0.628s elapsed time, 2.528s 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")
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
instantiation
  fun :: (type, topological_space) topological_space
  open_fun == open :: ('a \<Rightarrow> 'b) set \<Rightarrow> bool
### theory "HOL-Analysis.Measurable"
### 2.621s elapsed time, 9.748s cpu time, 7.072s 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")
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
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
*** Interrupt