Loading theory "HOL-Library.Cancellation" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Library.Permutations" via "HOL-Library.Multiset")
Loading theory "HOL-Library.Disjoint_Sets" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Library.Permutations")
Loading theory "HOL-Library.FuncSet" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product")
Loading theory "HOL-Library.Infinite_Set" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Affine" via "HOL-Analysis.Linear_Algebra")
Loading theory "HOL-Library.Nat_Bijection" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product" via "HOL-Library.Countable_Set" via "HOL-Library.Countable")
Loading theory "HOL-Library.Old_Datatype" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product" via "HOL-Library.Countable_Set" via "HOL-Library.Countable")
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
consts
  enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"
Found termination order: "size_list size <*mlex*> {}"
### theory "HOL-Library.Disjoint_Sets"
### 0.369s elapsed time, 2.220s cpu time, 0.000s GC time
Loading theory "HOL-Library.Phantom_Type" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product" via "HOL-Library.Numeral_Type" via "HOL-Library.Cardinality")
### theory "HOL-Library.Infinite_Set"
### 0.378s elapsed time, 2.268s cpu time, 0.000s GC time
Loading theory "HOL-Library.Product_Plus" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Affine" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space" via "HOL-Analysis.Product_Vector")
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
signature CANCEL = sig val proc: Proof.context -> cterm -> thm option end
functor Cancel_Fun (Data: CANCEL_NUMERALS_DATA): CANCEL
### theory "HOL-Library.Product_Plus"
### 0.126s elapsed time, 0.744s cpu time, 0.000s GC time
Loading theory "HOL-Library.Product_Order" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Lebesgue_Measure" via "HOL-Analysis.Finite_Product_Measure" via "HOL-Analysis.Binary_Product_Measure" via "HOL-Analysis.Nonnegative_Lebesgue_Integration" via "HOL-Analysis.Borel_Space" via "HOL-Analysis.Ordered_Euclidean_Space")
### theory "HOL-Library.Nat_Bijection"
### 0.529s elapsed time, 3.168s cpu time, 0.000s GC time
Loading theory "HOL-Library.Set_Algebras" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex")
signature CANCEL_DATA =
  sig
    val dest_coeff: term -> int * term
    val dest_sum: term -> term list
    val find_first_coeff: term -> term list -> int * term list
    val mk_coeff: int * term -> term
    val mk_sum: typ -> term list -> term
    val norm_ss1: simpset
    val norm_ss2: simpset
    val norm_tac: Proof.context -> tactic
    val numeral_simp_tac: Proof.context -> tactic
    val prove_conv:
       tactic list -> Proof.context -> thm list -> term * term -> thm option
    val simplify_meta_eq: Proof.context -> thm -> thm
    val trans_tac: Proof.context -> thm option -> tactic
  end
structure Cancel_Data: CANCEL_DATA
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
  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 :: (inf, inf) inf
  inf_prod == inf ::
    'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
instantiation
  set :: (zero) zero
  zero_set == zero_class.zero :: 'a set
instantiation
  set :: (one) one
  one_set == one_class.one :: 'a set
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
### theory "HOL-Library.FuncSet"
### 0.742s elapsed time, 4.360s cpu time, 0.408s GC time
Loading theory "HOL-Analysis.Metric_Arith" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Elementary_Normed_Spaces" via "HOL-Analysis.Elementary_Metric_Spaces")
signature OLD_DATATYPE =
  sig
    val check_specs: spec list -> theory -> spec list * Proof.context
    type config = {quiet: bool, strict: bool}
    val default_config: config
    type descr =
       (int * (string * dtyp list * (string * dtyp list) list)) list
    val distinct_lemma: thm
    datatype dtyp
    = DtRec of int | DtTFree of string * sort | DtType of string * dtyp list
    type info =
       {case_cong: thm,
        case_cong_weak: thm,
        case_name: string,
        case_rewrites: thm list,
        descr: descr,
        distinct: thm list,
        exhaust: thm,
        index: int,
        induct: thm,
        inducts: thm list,
        inject: thm list,
        nchotomy: thm,
        rec_names: string list,
        rec_rewrites: thm list, split: thm, split_asm: thm}
    val read_specs: spec_cmd list -> theory -> spec list * Proof.context
    type spec =
       (binding * (string * sort) list * mixfix) *
       (binding * typ list * mixfix) list
    type spec_cmd =
       (binding * (string * string option) list * mixfix) *
       (binding * string list * mixfix) list
  end
structure Old_Datatype: OLD_DATATYPE
### theory "HOL-Library.Old_Datatype"
### 0.755s elapsed time, 4.440s cpu time, 0.408s 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")
instantiation
  prod :: (Sup, Sup) Sup
  Sup_prod == Sup :: ('a \<times> 'b) set \<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.789s elapsed time, 4.660s cpu time, 0.408s GC time
Loading theory "HOL-Library.Multiset" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Library.Permutations")
### theory "HOL-Library.Set_Algebras"
### 0.332s elapsed time, 1.924s cpu time, 0.408s GC time
Loading theory "HOL-Analysis.Inner_Product" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Affine" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space")
### theory "HOL-Library.Product_Order"
### 0.357s elapsed time, 2.068s cpu time, 0.408s GC time
Loading theory "HOL-Analysis.L2_Norm" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Affine" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space")
### theory "HOL-Analysis.L2_Norm"
### 0.085s elapsed time, 0.516s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Operator_Norm" (required by "HOL-Analysis.Analysis")
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
### theory "HOL-Analysis.Operator_Norm"
### 0.092s elapsed time, 0.556s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Poly_Roots" (required by "HOL-Analysis.Analysis")
### theory "HOL-Library.Phantom_Type"
### 0.749s elapsed time, 4.412s cpu time, 0.408s 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")
### theory "HOL-Analysis.Poly_Roots"
### 0.098s elapsed time, 0.580s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Product_Vector" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Affine" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space")
### Additional type variable(s) in locale specification "CARD_1": 'a
### Additional type variable(s) in locale specification "countable": 'a
class CARD_1 = type +
  assumes "CARD_1": "CARD('a) = 1"
class countable = type +
  assumes "ex_inj": "\<exists>to_nat. inj to_nat"
### Additional type variable(s) in locale specification "card2": 'a
signature METRIC_ARITH =
  sig
    val metric_arith_tac: Proof.context -> int -> tactic
    val trace: bool Config.T
  end
structure MetricArith: METRIC_ARITH
### theory "HOL-Analysis.Metric_Arith"
### 0.630s elapsed time, 3.788s cpu time, 0.000s GC time
Loading theory "HOL-Library.Discrete" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests")
class card2 = finite +
  assumes "two_le_card": "2 \<le> CARD('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
locale module_prod
  fixes s1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and s2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
  assumes "module_prod s1 s2"
Proofs for inductive predicate(s) "finite_item"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
class finite_UNIV = type +
  fixes finite_UNIV :: "('a, bool) phantom"
  assumes "finite_UNIV": "finite_UNIV = Phantom('a) (finite UNIV)"
  Proving the simplification rules ...
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)"
### 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
### 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*> {}"
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
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)"
### theory "HOL-Library.Discrete"
### 0.204s elapsed time, 1.192s 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")
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
  prod :: (real_vector, real_vector) real_vector
  scaleR_prod == scaleR ::
    real \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
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
val old_countable_datatype_tac = fn: Proof.context -> int -> tactic
instantiation
  prod :: (card_UNIV, card_UNIV) card_UNIV
  card_UNIV_prod == card_UNIV_class.card_UNIV ::
    ('a \<times> 'b, nat) phantom
instantiation
  prod :: (metric_space, metric_space) dist
  dist_prod == dist ::
    'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> real
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
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
instantiation
  prod :: (metric_space, metric_space) uniformity_dist
  uniformity_prod == uniformity ::
    (('a \<times> 'b) \<times> 'a \<times> 'b) filter
instantiation
  fun :: (finite_UNIV, card_UNIV) finite_UNIV
  finite_UNIV_fun == finite_UNIV :: ('a \<Rightarrow> 'b, bool) phantom
instantiation
  prod :: (metric_space, metric_space) metric_space
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
  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
  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
### 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
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
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
  Enum.finite_2 :: card_UNIV
  card_UNIV_finite_2 == card_UNIV_class.card_UNIV ::
    (Enum.finite_2, nat) phantom
  finite_UNIV_finite_2 == finite_UNIV :: (Enum.finite_2, bool) phantom
instantiation
  Enum.finite_3 :: card_UNIV
  card_UNIV_finite_3 == card_UNIV_class.card_UNIV ::
    (Enum.finite_3, nat) phantom
  finite_UNIV_finite_3 == finite_UNIV :: (Enum.finite_3, bool) phantom
instantiation
  Enum.finite_4 :: card_UNIV
  card_UNIV_finite_4 == card_UNIV_class.card_UNIV ::
    (Enum.finite_4, nat) phantom
  finite_UNIV_finite_4 == finite_UNIV :: (Enum.finite_4, bool) phantom
instantiation
  multiset :: (type) Inf
  Inf_multiset == Inf :: 'a multiset set \<Rightarrow> 'a multiset
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
  multiset :: (type) Sup
  Sup_multiset == Sup :: 'a multiset set \<Rightarrow> 'a multiset
instantiation
  real :: real_inner
  inner_real == inner :: real \<Rightarrow> real \<Rightarrow> real
instantiation
  complex :: real_inner
  inner_complex == inner :: complex \<Rightarrow> complex \<Rightarrow> real
### theory "HOL-Library.Indicator_Function"
### 0.465s elapsed time, 2.668s cpu time, 0.000s GC time
Loading theory "HOL-Library.Liminf_Limsup" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests" via "HOL-Library.Extended_Real")
### Code generator: dropping subsumed code equation
### List.coset [] \<subseteq> set [] \<equiv> False
bundle inner_syntax
bundle no_inner_syntax
### theory "HOL-Analysis.Inner_Product"
### 1.238s elapsed time, 7.256s cpu time, 0.000s GC time
Loading theory "HOL-Library.Nonpos_Ints" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Harmonic_Numbers" via "HOL-Analysis.Complex_Transcendental" via "HOL-Analysis.Complex_Analysis_Basics")
instantiation
  multiset :: (type) size
  size_multiset == size :: 'a multiset \<Rightarrow> nat
### theory "HOL-Library.Countable"
### 1.680s elapsed time, 9.720s cpu time, 0.836s 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")
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.Cardinality"
### 1.322s elapsed time, 7.556s cpu time, 0.836s 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-Library.Nonpos_Ints"
### 0.364s elapsed time, 1.988s cpu time, 0.836s GC time
Loading theory "HOL-Library.Periodic_Fun" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Harmonic_Numbers" via "HOL-Analysis.Complex_Transcendental")
locale comp_fun_commute
  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
  assumes "comp_fun_commute f"
### theory "HOL-Analysis.Product_Vector"
### 1.327s elapsed time, 7.600s cpu time, 0.836s GC time
Loading theory "HOL-Analysis.Euclidean_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Affine" via "HOL-Analysis.Linear_Algebra")
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"
consts
  mset :: "'a list \<Rightarrow> 'a multiset"
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
### theory "HOL-Library.Periodic_Fun"
### 0.138s elapsed time, 0.832s cpu time, 0.000s GC time
Loading theory "HOL-Library.Sum_of_Squares" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Norm_Arith")
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
### Rule already declared as safe introduction (intro!)
### True
### Ignoring duplicate introduction (intro)
### True
class linorder = order +
  assumes "linear": "\<And>x y. x \<le> y \<or> y \<le> x"
### theory "HOL-Library.Liminf_Limsup"
### 0.735s elapsed time, 4.224s cpu time, 0.836s GC time
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
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"
### theory "HOL-Library.Countable_Set"
### 0.450s elapsed time, 2.720s cpu time, 0.000s GC time
Loading theory "HOL-Library.Countable_Complete_Lattices" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests" via "HOL-Library.Extended_Real" via "HOL-Library.Extended_Nat" via "HOL-Library.Order_Continuity")
Loading theory "HOL-Library.Set_Idioms" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Connected" via "HOL-Analysis.Abstract_Topology_2" via "HOL-Analysis.Elementary_Topology")
instantiation
  num0 :: equal
  equal_num0 == equal_class.equal ::
    num0 \<Rightarrow> num0 \<Rightarrow> bool
class comm_monoid_add = ab_semigroup_add + monoid_add +
  assumes "add_0": "\<And>a. (0::'a) + a = a"
instantiation
  num1 :: equal
  equal_num1 == equal_class.equal ::
    num1 \<Rightarrow> num1 \<Rightarrow> bool
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
  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
class comm_monoid_add = ab_semigroup_add + monoid_add +
  assumes "add_0": "\<And>a. (0::'a) + a = a"
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
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
  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
### theory "HOL-Library.Set_Idioms"
### 0.233s elapsed time, 1.400s 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")
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"
### 0.756s elapsed time, 4.564s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Continuum_Not_Denumerable" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Homeomorphism" via "HOL-Analysis.Homotopy")
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))"
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"
class comm_monoid_mult = ab_semigroup_mult + monoid_mult + dvd +
  assumes "mult_1": "\<And>a. (1::'a) * a = a"
### theory "HOL-Analysis.Continuum_Not_Denumerable"
### 0.264s elapsed time, 1.584s 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 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)"
class linorder = order +
  assumes "linear": "\<And>x y. x \<le> y \<or> y \<le> x"
locale countable_basis
  fixes p :: "'a set \<Rightarrow> bool"
    and B :: "'a set set"
  assumes "countable_basis p 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
instantiation
  prod :: (euclidean_space, euclidean_space) euclidean_space
  Basis_prod == Basis :: ('a \<times> 'b) set
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)"
class second_countable_topology = topological_space +
  assumes
    "ex_countable_subbasis":
      "\<exists>B. countable B \<and> open = generate_topology 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
### theory "HOL-Analysis.Euclidean_Space"
### 2.027s elapsed time, 12.088s cpu time, 0.668s GC time
Loading theory "HOL-Analysis.Finite_Cartesian_Product" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space")
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*> {}"
### ML warning (line 379 of "~~/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML"):
### Pattern is not exhaustive.
signature FUNC =
  sig
    exception DUP of key
    exception SAME
    exception UNDEF of key
    val apply: 'a table -> key -> 'a
    val applyd: 'a table -> (key -> 'a) -> key -> 'a
    val choose: 'a table -> key * 'a
    val combine:
       ('a -> 'a -> 'a) -> ('a -> bool) -> 'a table -> 'a table -> 'a table
    val cons_list: key * 'a -> 'a list table -> 'a list table
    val default: key * 'a -> 'a table -> 'a table
    val defined: 'a table -> key -> bool
    val delete: key -> 'a table -> 'a table
    val delete_safe: key -> 'a table -> 'a table
    val dest: 'a table -> (key * 'a) list
    val dest_list: 'a list table -> (key * 'a) list
    val dom: 'a table -> key list
    val empty: 'a table
    val exists: (key * 'a -> bool) -> 'a table -> bool
    val fold: (key * 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
    val fold_rev: (key * 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
    val forall: (key * 'a -> bool) -> 'a table -> bool
    val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
    val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table
    val insert_list:
       ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
    val insert_set: key -> set -> set
    val is_empty: 'a table -> bool
    val is_single: 'a table -> bool
    val join: (key -> 'a * 'a -> 'a) -> 'a table * 'a table -> 'a table
    type key
    val keys: 'a table -> key list
    val lookup: 'a table -> key -> 'a option
    val lookup_key: 'a table -> key -> (key * 'a) option
    val lookup_list: 'a list table -> key -> 'a list
    val make: (key * 'a) list -> 'a table
    val make_list: (key * 'a) list -> 'a list table
    val make_set: key list -> set
    val map: (key -> 'a -> 'b) -> 'a table -> 'b table
    val map_default: key * 'a -> ('a -> 'a) -> 'a table -> 'a table
    val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
    val max: 'a table -> (key * 'a) option
    val member: ('a * 'b -> bool) -> 'b table -> key * 'a -> bool
    val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    val merge_list:
       ('a * 'a -> bool) -> 'a list table * 'a list table -> 'a list table
    val min: 'a table -> (key * 'a) option
    val onefunc: key * 'a -> 'a table
    val remove: ('a * 'b -> bool) -> key * 'a -> 'b table -> 'b table
    val remove_list:
       ('a * 'b -> bool) -> key * 'a -> 'b list table -> 'b list table
    val remove_set: key -> set -> set
    type set = unit table
    type 'a table
    val tryapplyd: 'a table -> key -> 'a -> 'a
    val update: key * 'a -> 'a table -> 'a table
    val update_list:
       ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
    val update_new: key * 'a -> 'a table -> 'a table
    val updatep: (key * 'a -> bool) -> key * 'a -> 'a table -> 'a table
  end
functor FuncFun (Key: KEY): FUNC
signature REAL_ARITH =
  sig
    type cert_conv = cterm -> thm * pss_tree
    val cterm_of_rat: Rat.rat -> cterm
    val dest_ratconst: cterm -> Rat.rat
    val gen_gen_real_arith:
       Proof.context ->
         (Rat.rat -> cterm) * conv * conv * conv * conv * conv * conv *
         conv * conv * conv * prover
           -> cert_conv
    val gen_prover_real_arith: Proof.context -> prover -> cert_conv
    val gen_real_arith:
       Proof.context ->
         (Rat.rat -> cterm) * conv * conv * conv * conv * conv * conv *
         conv * prover
           -> cert_conv
    val is_ratconst: cterm -> bool
    datatype positivstellensatz
    =
         Axiom_eq of int
       | Axiom_le of int
       | Axiom_lt of int
       | Eqmul of FuncUtil.poly * positivstellensatz
       | Product of positivstellensatz * positivstellensatz
       | Rational_eq of Rat.rat
       | Rational_le of Rat.rat
       | Rational_lt of Rat.rat
       | Square of FuncUtil.poly
       | Sum of positivstellensatz * positivstellensatz
    type prover =
       tree_choice list ->
         (thm list * thm list * thm list -> positivstellensatz -> thm) ->
           thm list * thm list * thm list -> thm * pss_tree
    datatype pss_tree
    = Branch of pss_tree * pss_tree | Cert of positivstellensatz | Trivial
    val real_linear_prover:
       (thm list * thm list * thm list -> positivstellensatz -> thm) ->
         thm list * thm list * thm list -> thm * pss_tree
    datatype tree_choice = Left | Right
  end
structure FuncUtil:
  sig
    structure Ctermfunc: FUNC
    structure Intfunc: FUNC
    structure Intpairfunc: FUNC
    structure Monomialfunc: FUNC
    structure Ratfunc: FUNC
    structure Symfunc: FUNC
    structure Termfunc: FUNC
    val dest_monomial: 'a Ctermfunc.table -> (cterm * 'a) list
    type monomial = int Ctermfunc.table
    val monomial_ord: int Ctermfunc.table * int Ctermfunc.table -> order
    val monomial_order: int Ctermfunc.table * int Ctermfunc.table -> order
    type poly = Rat.rat Monomialfunc.table
  end
structure RealArith: REAL_ARITH
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
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
### theory "HOL-Library.Countable_Complete_Lattices"
### 2.363s elapsed time, 13.992s cpu time, 1.236s GC time
Loading theory "HOL-Analysis.Linear_Algebra" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Affine")
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.779s elapsed time, 28.144s cpu time, 2.072s 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")
bundle vec_syntax
bundle no_vec_syntax
signature SUM_OF_SQUARES =
  sig
    exception Failure of string
    val debug: bool Config.T
    val debug_message: Proof.context -> (unit -> string) -> unit
    datatype proof_method
    = Certificate of RealArith.pss_tree | Prover of string -> string
    val sos_tac:
       (RealArith.pss_tree -> unit) ->
         proof_method -> Proof.context -> int -> tactic
    val trace: bool Config.T
    val trace_message: Proof.context -> (unit -> string) -> unit
  end
structure Sum_of_Squares: SUM_OF_SQUARES
signature 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.066s elapsed time, 18.228s cpu time, 1.236s GC time
Loading theory "HOL-Library.Permutations" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants")
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
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)"
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
### theory "HOL-Analysis.Elementary_Topology"
### 2.421s elapsed time, 14.232s cpu time, 1.724s GC time
Loading theory "HOL-Library.Order_Continuity" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests" via "HOL-Library.Extended_Real" via "HOL-Library.Extended_Nat")
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
Proofs for inductive predicate(s) "swapidseq"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
instantiation
  vec :: (real_inner, finite) real_inner
  inner_vec == inner ::
    ('a, 'b) vec \<Rightarrow> ('a, 'b) vec \<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
  vec :: (euclidean_space, finite) euclidean_space
  Basis_vec == Basis :: ('a, 'b) vec set
### theory "HOL-Analysis.Linear_Algebra"
### 1.103s elapsed time, 6.528s cpu time, 0.488s GC time
Loading theory "HOL-Analysis.Affine" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex")
### theory "HOL-Analysis.Abstract_Topology"
### 3.195s elapsed time, 18.896s cpu time, 1.724s GC time
Loading theory "HOL-Analysis.Abstract_Limits" (required by "HOL-Analysis.Analysis")
Found termination order: "(\<lambda>p. size_list size (fst p)) <*mlex*> {}"
### theory "HOL-Library.Permutations"
### 0.832s elapsed time, 4.908s cpu time, 0.488s GC time
Loading theory "HOL-Analysis.Abstract_Topology_2" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Connected")
### theory "HOL-Library.Order_Continuity"
### 0.596s elapsed time, 3.604s cpu time, 0.000s GC time
Loading theory "HOL-Library.Extended_Nat" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests" via "HOL-Library.Extended_Real")
class infinity = type +
  fixes infinity :: "'a"
### theory "HOL-Analysis.Abstract_Limits"
### 0.246s elapsed time, 1.484s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Norm_Arith" (required by "HOL-Analysis.Analysis")
### theory "HOL-Analysis.Finite_Cartesian_Product"
### 2.132s elapsed time, 12.624s cpu time, 1.056s GC time
Loading theory "HOL-Analysis.Cartesian_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants")
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.Affine"
### 0.621s elapsed time, 3.616s cpu time, 0.692s GC time
Loading theory "HOL-Analysis.Convex" (required by "HOL-Analysis.Analysis")
### No equation for constructor "Extended_Nat.infinity_class.infinity"
### in definition of function "the_enat"
consts
  the_enat :: "enat \<Rightarrow> nat"
instantiation
  enat :: zero_neq_one
  one_enat == one_class.one :: enat
  zero_enat == zero_class.zero :: enat
### ML warning (line 103 of "~~/src/HOL/Analysis/normarith.ML"):
### Matches are not exhaustive.
### ML warning (line 347 of "~~/src/HOL/Analysis/normarith.ML"):
### Value identifier (instantiate_cterm') has not been referenced.
signature NORM_ARITH =
  sig
    val norm_arith: Proof.context -> conv
    val norm_arith_tac: Proof.context -> int -> tactic
  end
structure NormArith: NORM_ARITH
### theory "HOL-Analysis.Norm_Arith"
### 0.470s elapsed time, 2.700s cpu time, 0.692s GC time
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
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)"
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.966s elapsed time, 5.668s cpu time, 0.692s GC time
Loading theory "HOL-Library.Extended_Real" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests")
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"
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
  enat :: linorder_topology
  open_enat == open :: enat set \<Rightarrow> bool
### theory "HOL-Analysis.Cartesian_Space"
### 2.485s elapsed time, 13.064s cpu time, 5.912s GC time
Loading theory "HOL-Analysis.Determinants" (required by "HOL-Analysis.Analysis")
### theory "HOL-Analysis.Convex"
### 2.229s elapsed time, 11.648s cpu time, 5.220s GC time
### theory "HOL-Analysis.Abstract_Topology_2"
### 2.871s elapsed time, 15.392s cpu time, 5.912s GC time
Loading theory "HOL-Analysis.Connected" (required by "HOL-Analysis.Analysis")
Loading theory "HOL-Analysis.Elementary_Metric_Spaces" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Elementary_Normed_Spaces")
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>
             normalize (prod_mset A) = normalize x"
instantiation
  ereal :: uminus
  uminus_ereal == uminus :: ereal \<Rightarrow> ereal
Found termination order: "{}"
instantiation
  ereal :: infinity
  infinity_ereal == infinity :: ereal
### theory "HOL-Analysis.Connected"
### 0.381s elapsed time, 2.284s cpu time, 0.352s GC time
Loading theory "HOL-Analysis.Function_Topology" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function")
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
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>
             normalize (prod_mset A) = normalize x"
### theory "HOL-Analysis.Determinants"
### 0.927s elapsed time, 5.520s cpu time, 0.352s GC time
instantiation
  ereal :: linorder
  less_eq_ereal == less_eq :: ereal \<Rightarrow> ereal \<Rightarrow> bool
  less_ereal == less :: ereal \<Rightarrow> ereal \<Rightarrow> bool
instantiation
  fun :: (type, topological_space) topological_space
  open_fun == open :: ('a \<Rightarrow> 'b) set \<Rightarrow> bool
instantiation
  ereal :: {comm_monoid_mult,sgn}
  sgn_ereal == sgn :: ereal \<Rightarrow> ereal
  times_ereal == times :: ereal \<Rightarrow> ereal \<Rightarrow> ereal
### theory "HOL-Analysis.Function_Topology"
### 1.004s elapsed time, 5.824s cpu time, 0.552s GC time
Loading theory "HOL-Analysis.Product_Topology" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Weierstrass_Theorems" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.T1_Spaces")
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"
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
### theory "HOL-Analysis.Product_Topology"
### 0.279s elapsed time, 1.688s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.T1_Spaces" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Weierstrass_Theorems" via "HOL-Analysis.Path_Connected")
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
### theory "HOL-Analysis.T1_Spaces"
### 0.291s elapsed time, 1.756s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Lindelof_Spaces" (required by "HOL-Analysis.Analysis")
instantiation
  ereal :: linear_continuum_topology
  open_ereal == open :: ereal set \<Rightarrow> bool
### theory "HOL-Analysis.Lindelof_Spaces"
### 0.093s elapsed time, 0.564s cpu time, 0.000s GC time
### theory "HOL-Analysis.Elementary_Metric_Spaces"
### 2.404s elapsed time, 14.260s cpu time, 1.048s GC time
Loading theory "HOL-Analysis.Elementary_Normed_Spaces" (required by "HOL-Analysis.Analysis")
Loading theory "HOL-Analysis.Function_Metric" (required by "HOL-Analysis.Analysis")
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
### theory "HOL-Analysis.Function_Metric"
### 0.355s elapsed time, 2.144s cpu time, 0.000s GC time
### theory "HOL-Library.Extended_Real"
### 4.782s elapsed time, 26.824s cpu time, 6.620s GC time
Loading theory "HOL-Library.Extended_Nonnegative_Real" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests" via "HOL-Analysis.Extended_Real_Limits")
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"
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
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
### theory "HOL-Analysis.Elementary_Normed_Spaces"
### 1.507s elapsed time, 9.056s cpu time, 0.420s GC time
Loading theory "HOL-Analysis.Topology_Euclidean_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex_Euclidean_Space")
instantiation
  ennreal :: linear_continuum_topology
  open_ennreal == open :: ennreal set \<Rightarrow> bool
### Ignoring duplicate rewrite rule:
### f (0::'a) \<equiv> 0::'b
### Ignoring duplicate rewrite rule:
### f (0::'a) \<equiv> 0::'b
### theory "HOL-Library.Extended_Nonnegative_Real"
### 1.765s elapsed time, 10.576s cpu time, 0.844s GC time
Loading theory "HOL-Analysis.Sigma_Algebra" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Lebesgue_Measure" via "HOL-Analysis.Finite_Product_Measure" via "HOL-Analysis.Binary_Product_Measure" via "HOL-Analysis.Nonnegative_Lebesgue_Integration" via "HOL-Analysis.Measure_Space" via "HOL-Analysis.Measurable")
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 ...
Proofs for inductive predicate(s) "smallest_ccdi_setsp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "HOL-Computational_Algebra.Factorial_Ring"
### 10.074s elapsed time, 58.288s cpu time, 9.184s 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")
locale Dynkin_system
  fixes \<Omega> :: "'a set"
    and M :: "'a set set"
  assumes "Dynkin_system \<Omega> M"
### theory "HOL-Analysis.Topology_Euclidean_Space"
### 2.353s elapsed time, 14.036s cpu time, 0.964s GC time
Loading theory "HOL-Analysis.Convex_Euclidean_Space" (required by "HOL-Analysis.Analysis")
Loading theory "HOL-Analysis.Extended_Real_Limits" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests")
Loading theory "HOL-Analysis.Line_Segment" (required by "HOL-Analysis.Analysis")
Loading theory "HOL-Analysis.Tagged_Division" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Henstock_Kurzweil_Integration")
### theory "HOL-Analysis.Sigma_Algebra"
### 2.513s elapsed time, 15.016s cpu time, 1.244s GC time
Loading theory "HOL-Analysis.Measurable" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Lebesgue_Measure" via "HOL-Analysis.Finite_Product_Measure" via "HOL-Analysis.Binary_Product_Measure" via "HOL-Analysis.Nonnegative_Lebesgue_Integration" via "HOL-Analysis.Measure_Space")
signature MEASURABLE =
  sig
    val add_del_cong_thm: bool -> thm -> Context.generic -> Context.generic
    val add_local_cong: thm -> Proof.context -> Proof.context
    val add_preprocessor:
       string -> preprocessor -> Context.generic -> Context.generic
    val cong_thm_attr: attribute context_parser
    val del_preprocessor: string -> Context.generic -> Context.generic
    val dest_thm_attr: attribute context_parser
    val get_all: Context.generic -> thm list
    val get_cong: Context.generic -> thm list
    val get_dest: Context.generic -> thm list
    datatype level = Concrete | Generic
    val measurable_tac: Proof.context -> thm list -> tactic
    val measurable_thm_attr: bool * (bool * level) -> attribute
    val prepare_facts: Proof.context -> thm list -> thm list * Proof.context
    type preprocessor = thm -> Proof.context -> thm list * Proof.context
    val simproc: Proof.context -> cterm -> thm option
  end
structure Measurable: MEASURABLE
locale operative
  fixes
    f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
      (infixl \<open>\<^bold>*\<close> 70)
    and z :: "'a"  (\<open>\<^bold>1\<close>)
    and g :: "'b set \<Rightarrow> 'a"
  assumes "operative (\<^bold>*) \<^bold>1 g"
locale operative_real
  fixes
    f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
      (infixl \<open>\<^bold>*\<close> 70)
    and z :: "'a"  (\<open>\<^bold>1\<close>)
    and g :: "real set \<Rightarrow> 'a"
  assumes "operative_real (\<^bold>*) \<^bold>1 g"
### theory "HOL-Analysis.Tagged_Division"
### 1.115s elapsed time, 6.704s cpu time, 0.704s GC time
### theory "HOL-Analysis.Line_Segment"
### 1.174s elapsed time, 7.064s cpu time, 0.704s GC time
### theory "HOL-Analysis.Convex_Euclidean_Space"
### 1.221s elapsed time, 7.344s cpu time, 0.704s GC time
Loading theory "HOL-Analysis.Ordered_Euclidean_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Lebesgue_Measure" via "HOL-Analysis.Finite_Product_Measure" via "HOL-Analysis.Binary_Product_Measure" via "HOL-Analysis.Nonnegative_Lebesgue_Integration" via "HOL-Analysis.Borel_Space")
### theory "HOL-Analysis.Extended_Real_Limits"
### 1.229s elapsed time, 7.396s cpu time, 0.704s GC time
Loading theory "HOL-Analysis.Summation_Tests" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit")
Loading theory "HOL-Analysis.Starlike" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Weierstrass_Theorems" via "HOL-Analysis.Path_Connected")
### theory "HOL-Analysis.Measurable"
### 0.571s elapsed time, 3.444s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Measure_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Lebesgue_Measure" via "HOL-Analysis.Finite_Product_Measure" via "HOL-Analysis.Binary_Product_Measure" via "HOL-Analysis.Nonnegative_Lebesgue_Integration")
*** Interrupt