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*> {}"
### theory "HOL-Library.Disjoint_Sets"
### 0.313s elapsed time, 1.908s 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")
consts
  enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"
Found termination order: "size_list size <*mlex*> {}"
### theory "HOL-Library.Infinite_Set"
### 0.443s elapsed time, 2.672s cpu time, 0.000s GC time
Loading theory "HOL-Library.Product_Plus" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Affine" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space" via "HOL-Analysis.Product_Vector")
signature CANCEL = sig val proc: Proof.context -> cterm -> thm option end
functor Cancel_Fun (Data: CANCEL_NUMERALS_DATA): CANCEL
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.Nat_Bijection"
### 0.514s elapsed time, 3.104s 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
  set :: (plus) plus
  plus_set == plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set
instantiation
  set :: (times) times
  times_set == times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set
instantiation
  set :: (zero) zero
  zero_set == zero_class.zero :: 'a set
### theory "HOL-Library.Product_Plus"
### 0.126s elapsed time, 0.740s 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")
instantiation
  set :: (one) one
  one_set == one_class.one :: 'a set
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
### theory "HOL-Library.FuncSet"
### 0.614s elapsed time, 3.688s cpu time, 0.000s 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")
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.743s elapsed time, 4.396s cpu time, 0.452s 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 \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
signature CANCEL_SIMPROCS =
  sig
    val diff_cancel: Proof.context -> cterm -> thm option
    val eq_cancel: Proof.context -> cterm -> thm option
    val less_cancel: Proof.context -> cterm -> thm option
    val less_eq_cancel: Proof.context -> cterm -> thm option
  end
structure Cancel_Simprocs: CANCEL_SIMPROCS
### theory "HOL-Library.Cancellation"
### 0.787s elapsed time, 4.676s cpu time, 0.452s GC time
Loading theory "HOL-Library.Multiset" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Library.Permutations")
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
instantiation
  prod :: (Sup, Sup) Sup
  Sup_prod == Sup :: ('a \<times> 'b) set \<Rightarrow> 'a \<times> 'b
### theory "HOL-Library.Set_Algebras"
### 0.333s elapsed time, 1.932s cpu time, 0.452s 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.335s elapsed time, 1.952s cpu time, 0.452s 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")
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.L2_Norm"
### 0.081s elapsed time, 0.488s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Operator_Norm" (required by "HOL-Analysis.Analysis")
### theory "HOL-Library.Phantom_Type"
### 0.754s elapsed time, 4.444s cpu time, 0.452s 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.Operator_Norm"
### 0.089s elapsed time, 0.536s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Poly_Roots" (required by "HOL-Analysis.Analysis")
### 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"
### theory "HOL-Analysis.Poly_Roots"
### 0.096s elapsed time, 0.572s 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")
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.735s elapsed time, 4.360s cpu time, 0.452s 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)"
Proofs for inductive predicate(s) "finite_item"
class finite_UNIV = type +
  fixes finite_UNIV :: "('a, bool) phantom"
  assumes "finite_UNIV": "finite_UNIV = Phantom('a) (finite UNIV)"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### 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
### 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))
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)"
Found termination order: "size <*mlex*> {}"
### Partially applied constant "Multiset.sup_subset_mset" on left hand side of equation, in theorem:
### semilattice_sup.Sup_fin (\<union>#) (set (?x # ?xs)) \<equiv>
### fold (\<union>#) ?xs ?x
class 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
locale module_prod
  fixes s1 :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    and s2 :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
  assumes "module_prod s1 s2"
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
### theory "HOL-Library.Discrete"
### 0.196s elapsed time, 1.144s 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
  unit :: card_UNIV
  card_UNIV_unit == card_UNIV_class.card_UNIV :: (unit, nat) phantom
  finite_UNIV_unit == finite_UNIV :: (unit, bool) phantom
instantiation
  bool :: card_UNIV
  card_UNIV_bool == card_UNIV_class.card_UNIV :: (bool, nat) phantom
  finite_UNIV_bool == finite_UNIV :: (bool, bool) phantom
instantiation
  char :: card_UNIV
  card_UNIV_char == card_UNIV_class.card_UNIV :: (char, nat) phantom
  finite_UNIV_char == finite_UNIV :: (char, bool) phantom
instantiation
  prod :: (finite_UNIV, finite_UNIV) finite_UNIV
  finite_UNIV_prod == finite_UNIV :: ('a \<times> 'b, bool) phantom
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
  sum :: (finite_UNIV, finite_UNIV) finite_UNIV
  finite_UNIV_sum == finite_UNIV :: ('a + 'b, 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)"
instantiation
  sum :: (card_UNIV, card_UNIV) card_UNIV
  card_UNIV_sum == card_UNIV_class.card_UNIV :: ('a + 'b, nat) phantom
instantiation
  fun :: (finite_UNIV, card_UNIV) finite_UNIV
  finite_UNIV_fun == finite_UNIV :: ('a \<Rightarrow> 'b, bool) phantom
instantiation
  fun :: (card_UNIV, card_UNIV) card_UNIV
  card_UNIV_fun == card_UNIV_class.card_UNIV ::
    ('a \<Rightarrow> 'b, nat) phantom
instantiation
  prod :: (real_vector, real_vector) real_vector
  scaleR_prod == scaleR ::
    real \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
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
### 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
  prod :: (metric_space, metric_space) dist
  dist_prod == dist ::
    'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> real
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
  prod :: (metric_space, metric_space) uniformity_dist
  uniformity_prod == uniformity ::
    (('a \<times> 'b) \<times> 'a \<times> 'b) filter
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
  prod :: (metric_space, metric_space) metric_space
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
  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
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_4 :: card_UNIV
  card_UNIV_finite_4 == card_UNIV_class.card_UNIV ::
    (Enum.finite_4, nat) phantom
  finite_UNIV_finite_4 == finite_UNIV :: (Enum.finite_4, bool) phantom
instantiation
  Enum.finite_5 :: card_UNIV
  card_UNIV_finite_5 == card_UNIV_class.card_UNIV ::
    (Enum.finite_5, nat) phantom
  finite_UNIV_finite_5 == finite_UNIV :: (Enum.finite_5, bool) phantom
instantiation
  multiset :: (type) Inf
  Inf_multiset == Inf :: 'a multiset set \<Rightarrow> 'a multiset
instantiation
  real :: real_inner
  inner_real == inner :: real \<Rightarrow> real \<Rightarrow> real
instantiation
  multiset :: (type) Sup
  Sup_multiset == Sup :: 'a multiset set \<Rightarrow> 'a multiset
instantiation
  complex :: real_inner
  inner_complex == inner :: complex \<Rightarrow> complex \<Rightarrow> real
### theory "HOL-Library.Indicator_Function"
### 0.463s elapsed time, 2.656s 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.230s elapsed time, 7.204s 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.629s elapsed time, 9.400s cpu time, 0.812s 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.344s elapsed time, 7.684s cpu time, 0.812s 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")
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"
locale comp_fun_commute
  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
  assumes "comp_fun_commute f"
### theory "HOL-Library.Nonpos_Ints"
### 0.380s elapsed time, 2.088s cpu time, 0.812s GC time
Loading theory "HOL-Library.Periodic_Fun" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Harmonic_Numbers" via "HOL-Analysis.Complex_Transcendental")
### theory "HOL-Analysis.Product_Vector"
### 1.291s elapsed time, 7.372s cpu time, 0.812s 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"
consts
  mset :: "'a list \<Rightarrow> 'a multiset"
locale periodic_fun_simple'
  fixes f :: "'a \<Rightarrow> 'b"
  assumes "periodic_fun_simple' f"
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.836s 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.780s elapsed time, 4.472s cpu time, 0.812s 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.463s elapsed time, 2.796s 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
### theory "HOL-Library.Set_Idioms"
### 0.228s elapsed time, 1.372s 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
  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
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.754s elapsed time, 4.552s 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.270s elapsed time, 1.620s 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"
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)"
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 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.088s elapsed time, 12.436s cpu time, 0.600s 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.377s elapsed time, 14.056s cpu time, 1.212s 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.845s elapsed time, 28.504s cpu time, 2.024s GC time
Loading theory "HOL-Computational_Algebra.Factorial_Ring" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Jordan_Curve" via "HOL-Analysis.Arcwise_Connected" via "HOL-Computational_Algebra.Primes" via "HOL-Computational_Algebra.Euclidean_Algorithm")
signature SUM_OF_SQUARES =
  sig
    exception Failure of string
    val debug: bool Config.T
    val debug_message: Proof.context -> (unit -> string) -> unit
    datatype proof_method
    = Certificate of RealArith.pss_tree | Prover of string -> string
    val sos_tac:
       (RealArith.pss_tree -> unit) ->
         proof_method -> Proof.context -> int -> tactic
    val trace: bool Config.T
    val trace_message: Proof.context -> (unit -> string) -> unit
  end
structure Sum_of_Squares: SUM_OF_SQUARES
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.092s elapsed time, 18.360s cpu time, 1.212s GC time
Loading theory "HOL-Library.Permutations" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants")
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)"
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
### theory "HOL-Analysis.Elementary_Topology"
### 2.406s elapsed time, 14.212s cpu time, 1.176s 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 :: (times, finite) times
  times_vec == times ::
    ('a, 'b) vec \<Rightarrow> ('a, 'b) vec \<Rightarrow> ('a, 'b) vec
instantiation
  vec :: (one, finite) one
  one_vec == one_class.one :: ('a, 'b) vec
instantiation
  vec :: (ord, finite) ord
  less_eq_vec == less_eq ::
    ('a, 'b) vec \<Rightarrow> ('a, 'b) vec \<Rightarrow> bool
  less_vec == less ::
    ('a, 'b) vec \<Rightarrow> ('a, 'b) vec \<Rightarrow> bool
instantiation
  vec :: (real_vector, finite) real_vector
  scaleR_vec == scaleR ::
    real \<Rightarrow> ('a, 'b) vec \<Rightarrow> ('a, 'b) vec
instantiation
  vec :: (topological_space, finite) topological_space
  open_vec == open :: ('a, 'b) vec set \<Rightarrow> bool
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 :: (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) "generate_topology_on"
  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
instantiation
  vec :: (euclidean_space, finite) euclidean_space
  Basis_vec == Basis :: ('a, 'b) vec set
### theory "HOL-Analysis.Linear_Algebra"
### 1.176s elapsed time, 6.968s cpu time, 0.564s GC time
Loading theory "HOL-Analysis.Affine" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex")
### theory "HOL-Analysis.Abstract_Topology"
### 3.348s elapsed time, 19.792s cpu time, 1.776s 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.859s elapsed time, 5.072s cpu time, 0.564s GC time
Loading theory "HOL-Analysis.Abstract_Topology_2" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Connected")
### theory "HOL-Library.Order_Continuity"
### 0.635s elapsed time, 3.840s 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")
### theory "HOL-Analysis.Abstract_Limits"
### 0.248s elapsed time, 1.496s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Norm_Arith" (required by "HOL-Analysis.Analysis")
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.Finite_Cartesian_Product"
### 2.241s elapsed time, 13.280s cpu time, 1.176s GC time
Loading theory "HOL-Analysis.Cartesian_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants")
### theory "HOL-Analysis.Affine"
### 0.613s elapsed time, 3.576s cpu time, 0.696s GC time
Loading theory "HOL-Analysis.Convex" (required by "HOL-Analysis.Analysis")
### 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.432s elapsed time, 2.484s cpu time, 0.696s GC time
### 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
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 :: {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.908s elapsed time, 5.356s cpu time, 0.696s 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.Convex"
### 2.198s elapsed time, 11.420s cpu time, 5.116s GC time
### theory "HOL-Analysis.Cartesian_Space"
### 2.447s elapsed time, 12.800s cpu time, 5.812s GC time
Loading theory "HOL-Analysis.Determinants" (required by "HOL-Analysis.Analysis")
### theory "HOL-Analysis.Abstract_Topology_2"
### 2.768s elapsed time, 14.736s cpu time, 5.812s 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
### theory "HOL-Analysis.Connected"
### 0.413s elapsed time, 2.456s cpu time, 0.360s GC time
Loading theory "HOL-Analysis.Function_Topology" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function")
Found termination order: "{}"
instantiation
  ereal :: infinity
  infinity_ereal == infinity :: ereal
instantiation
  ereal :: abs
  abs_ereal == abs :: 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"
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
### theory "HOL-Analysis.Determinants"
### 1.011s elapsed time, 5.964s cpu time, 0.360s GC time
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"
### 0.910s elapsed time, 5.268s cpu time, 0.000s 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
### theory "HOL-Analysis.Product_Topology"
### 0.432s elapsed time, 2.600s cpu time, 0.684s 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 :: inverse
  inverse_ereal == inverse :: ereal \<Rightarrow> ereal
  divide_ereal == divide :: ereal \<Rightarrow> ereal \<Rightarrow> ereal
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.300s elapsed time, 1.812s 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.106s elapsed time, 0.644s cpu time, 0.000s GC time
### theory "HOL-Analysis.Elementary_Metric_Spaces"
### 2.505s elapsed time, 14.860s cpu time, 1.044s 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.339s elapsed time, 2.044s cpu time, 0.000s GC time
### theory "HOL-Library.Extended_Real"
### 4.873s elapsed time, 27.260s cpu time, 6.684s 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
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
structure Cancel_Ennreal_Common:
  sig
    val dest_sum: term -> term list
    val dest_summing: term * term list -> term list
    val find_first: term -> term list -> term list
    val find_first_t: term list -> term -> term list -> term list
    val mk_eq: term * term -> term
    val mk_sum: typ -> term list -> term
    val norm_ss: simpset
    val norm_tac: Proof.context -> tactic
    val simplify_meta_eq: Proof.context -> thm -> thm -> thm
    val trans_tac: Proof.context -> thm option -> tactic
  end
structure Eq_Ennreal_Cancel:
  sig val proc: Proof.context -> term -> thm option end
structure Le_Ennreal_Cancel:
  sig val proc: Proof.context -> term -> thm option end
structure Less_Ennreal_Cancel:
  sig val proc: Proof.context -> term -> thm option end
### theory "HOL-Analysis.Elementary_Normed_Spaces"
### 1.560s elapsed time, 9.380s cpu time, 0.484s 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
### theory "HOL-Library.Extended_Nonnegative_Real"
### 1.851s elapsed time, 11.108s cpu time, 1.004s 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")
### Ignoring duplicate rewrite rule:
### f (0::'a) \<equiv> 0::'b
### Ignoring duplicate rewrite rule:
### f (0::'a) \<equiv> 0::'b
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.183s elapsed time, 58.984s cpu time, 9.488s 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.470s elapsed time, 14.860s cpu time, 1.060s 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.544s elapsed time, 15.272s cpu time, 1.264s GC time
Loading theory "HOL-Analysis.Measurable" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration" via "HOL-Analysis.Lebesgue_Measure" via "HOL-Analysis.Finite_Product_Measure" via "HOL-Analysis.Binary_Product_Measure" via "HOL-Analysis.Nonnegative_Lebesgue_Integration" via "HOL-Analysis.Measure_Space")
signature MEASURABLE =
  sig
    val add_del_cong_thm: bool -> thm -> Context.generic -> Context.generic
    val add_local_cong: thm -> Proof.context -> Proof.context
    val add_preprocessor:
       string -> preprocessor -> Context.generic -> Context.generic
    val cong_thm_attr: attribute context_parser
    val del_preprocessor: string -> Context.generic -> Context.generic
    val dest_thm_attr: attribute context_parser
    val get_all: Context.generic -> thm list
    val get_cong: Context.generic -> thm list
    val get_dest: Context.generic -> thm list
    datatype level = Concrete | Generic
    val measurable_tac: Proof.context -> thm list -> tactic
    val measurable_thm_attr: bool * (bool * level) -> attribute
    val prepare_facts: Proof.context -> thm list -> thm list * Proof.context
    type preprocessor = thm -> Proof.context -> thm list * Proof.context
    val simproc: Proof.context -> cterm -> thm option
  end
structure Measurable: MEASURABLE
### theory "HOL-Analysis.Convex_Euclidean_Space"
### 1.263s elapsed time, 7.560s cpu time, 0.724s 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.245s elapsed time, 7.452s cpu time, 0.724s GC time
Loading theory "HOL-Analysis.Summation_Tests" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function" via "HOL-Analysis.Uniform_Limit")
### theory "HOL-Analysis.Line_Segment"
### 1.217s elapsed time, 7.288s cpu time, 0.724s GC time
Loading theory "HOL-Analysis.Starlike" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Weierstrass_Theorems" via "HOL-Analysis.Path_Connected")
### theory "HOL-Analysis.Measurable"
### 0.602s elapsed time, 3.632s 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")
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"
### 2.705s elapsed time, 14.088s cpu time, 7.548s GC time
*** Interrupt