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.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")
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")
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
consts
  enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"
### theory "HOL-Library.Disjoint_Sets"
### 0.318s elapsed time, 1.912s 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.337s elapsed time, 2.032s 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")
Found termination order: "size_list size <*mlex*> {}"
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.127s elapsed time, 0.752s 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
  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
signature CANCEL_DATA =
  sig
    val dest_coeff: term -> int * term
    val dest_sum: term -> term list
    val find_first_coeff: term -> term list -> int * term list
    val mk_coeff: int * term -> term
    val mk_sum: typ -> term list -> term
    val norm_ss1: simpset
    val norm_ss2: simpset
    val norm_tac: Proof.context -> tactic
    val numeral_simp_tac: Proof.context -> tactic
    val prove_conv:
       tactic list -> Proof.context -> thm list -> term * term -> thm option
    val simplify_meta_eq: Proof.context -> thm -> thm
    val trans_tac: Proof.context -> thm option -> tactic
  end
structure Cancel_Data: CANCEL_DATA
### theory "HOL-Library.Nat_Bijection"
### 0.510s elapsed time, 3.056s cpu time, 0.000s GC time
Loading theory "HOL-Library.Set_Algebras" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex")
instantiation
  prod :: (inf, inf) inf
  inf_prod == inf ::
    'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
instantiation
  set :: (plus) plus
  plus_set == plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set
instantiation
  prod :: (sup, sup) sup
  sup_prod == sup ::
    'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
instantiation
  set :: (times) times
  times_set == times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set
instantiation
  set :: (zero) zero
  zero_set == zero_class.zero :: 'a set
instantiation
  set :: (one) one
  one_set == one_class.one :: 'a set
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
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.725s elapsed time, 4.284s cpu time, 0.344s GC time
Loading theory "HOL-Library.Multiset" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Library.Permutations")
### theory "HOL-Library.FuncSet"
### 0.725s elapsed time, 4.272s cpu time, 0.344s 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.768s elapsed time, 4.536s cpu time, 0.344s GC time
Loading theory "HOL-Library.Countable" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product" via "HOL-Library.Countable_Set")
### theory "HOL-Library.Product_Order"
### 0.309s elapsed time, 1.788s cpu time, 0.344s 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.Set_Algebras"
### 0.319s elapsed time, 1.856s cpu time, 0.344s 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.083s elapsed time, 0.500s 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.090s elapsed time, 0.540s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Poly_Roots" (required by "HOL-Analysis.Analysis")
### theory "HOL-Library.Phantom_Type"
### 0.785s elapsed time, 4.644s cpu time, 0.344s 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.093s elapsed time, 0.560s 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"
class real_inner = dist_norm + real_vector + sgn_div_norm +
  uniformity_dist + open_uniformity +
  fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
  assumes "inner_commute": "\<And>x y. inner x y = inner y x"
    and
    "inner_add_left": "\<And>x y z. inner (x + y) z = inner x z + inner y z"
    and
    "inner_scaleR_left":
      "\<And>r x y. inner (r *\<^sub>R x) y = r * inner x y"
    and "inner_ge_zero": "\<And>x. 0 \<le> inner x x"
    and "inner_eq_zero_iff": "\<And>x. (inner x x = 0) = (x = (0::'a))"
    and "norm_eq_sqrt_inner": "\<And>x. norm x = sqrt (inner x x)"
### Additional type variable(s) in locale specification "card2": 'a
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.622s elapsed time, 3.740s 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")
### Partially applied constant "Multiset.inf_subset_mset" on left hand side of equation, in theorem:
### semilattice_inf.Inf_fin (\<inter>#) (set (?x # ?xs)) \<equiv>
### fold (\<inter>#) ?xs ?x
class card2 = finite +
  assumes "two_le_card": "2 \<le> CARD('a)"
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"
### 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
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
class finite_UNIV = type +
  fixes finite_UNIV :: "('a, bool) phantom"
  assumes "finite_UNIV": "finite_UNIV = Phantom('a) (finite UNIV)"
### 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
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
  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
### theory "HOL-Library.Discrete"
### 0.210s elapsed time, 1.228s 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
  integer :: card_UNIV
  card_UNIV_integer == card_UNIV_class.card_UNIV :: (integer, nat) phantom
  finite_UNIV_integer == finite_UNIV :: (integer, bool) phantom
instantiation
  prod :: (real_vector, real_vector) real_vector
  scaleR_prod == scaleR ::
    real \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
instantiation
  list :: (type) card_UNIV
  card_UNIV_list == card_UNIV_class.card_UNIV :: ('a list, nat) phantom
  finite_UNIV_list == finite_UNIV :: ('a list, bool) phantom
instantiation
  unit :: card_UNIV
  card_UNIV_unit == card_UNIV_class.card_UNIV :: (unit, nat) phantom
  finite_UNIV_unit == finite_UNIV :: (unit, bool) phantom
instantiation
  bool :: card_UNIV
  card_UNIV_bool == card_UNIV_class.card_UNIV :: (bool, nat) phantom
  finite_UNIV_bool == finite_UNIV :: (bool, bool) phantom
instantiation
  prod :: (metric_space, metric_space) dist
  dist_prod == dist ::
    'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> real
val old_countable_datatype_tac = fn: Proof.context -> int -> tactic
instantiation
  char :: card_UNIV
  card_UNIV_char == card_UNIV_class.card_UNIV :: (char, nat) phantom
  finite_UNIV_char == finite_UNIV :: (char, bool) 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
  prod :: (finite_UNIV, finite_UNIV) finite_UNIV
  finite_UNIV_prod == finite_UNIV :: ('a \<times> 'b, bool) phantom
instantiation
  prod :: (metric_space, metric_space) metric_space
instantiation
  prod :: (card_UNIV, card_UNIV) card_UNIV
  card_UNIV_prod == card_UNIV_class.card_UNIV ::
    ('a \<times> 'b, nat) phantom
instantiation
  sum :: (finite_UNIV, finite_UNIV) finite_UNIV
  finite_UNIV_sum == finite_UNIV :: ('a + 'b, bool) phantom
instantiation
  sum :: (card_UNIV, card_UNIV) card_UNIV
  card_UNIV_sum == card_UNIV_class.card_UNIV :: ('a + 'b, nat) phantom
instantiation
  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
  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
  option :: (finite_UNIV) finite_UNIV
  finite_UNIV_option == finite_UNIV :: ('a option, 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
instantiation
  option :: (card_UNIV) card_UNIV
  card_UNIV_option == card_UNIV_class.card_UNIV :: ('a option, nat) phantom
val countable_datatype_tac = fn: Proof.context -> thm -> thm Seq.seq
val countable_tac = fn: Proof.context -> int -> tactic
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
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
  set :: (finite_UNIV) finite_UNIV
  finite_UNIV_set == finite_UNIV :: ('a set, bool) phantom
instantiation
  real :: real_inner
  inner_real == inner :: real \<Rightarrow> real \<Rightarrow> real
instantiation
  set :: (card_UNIV) card_UNIV
  card_UNIV_set == card_UNIV_class.card_UNIV :: ('a set, nat) phantom
instantiation
  complex :: real_inner
  inner_complex == inner :: complex \<Rightarrow> complex \<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
  multiset :: (type) Inf
  Inf_multiset == Inf :: 'a multiset set \<Rightarrow> 'a multiset
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
  multiset :: (type) Sup
  Sup_multiset == Sup :: 'a multiset set \<Rightarrow> 'a multiset
instantiation
  Enum.finite_3 :: card_UNIV
  card_UNIV_finite_3 == card_UNIV_class.card_UNIV ::
    (Enum.finite_3, nat) phantom
  finite_UNIV_finite_3 == finite_UNIV :: (Enum.finite_3, bool) phantom
instantiation
  Enum.finite_4 :: card_UNIV
  card_UNIV_finite_4 == card_UNIV_class.card_UNIV ::
    (Enum.finite_4, nat) phantom
  finite_UNIV_finite_4 == finite_UNIV :: (Enum.finite_4, bool) phantom
instantiation
  Enum.finite_5 :: card_UNIV
  card_UNIV_finite_5 == card_UNIV_class.card_UNIV ::
    (Enum.finite_5, nat) phantom
  finite_UNIV_finite_5 == finite_UNIV :: (Enum.finite_5, bool) phantom
bundle inner_syntax
bundle no_inner_syntax
### theory "HOL-Analysis.Inner_Product"
### 1.191s elapsed time, 7.012s 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")
### theory "HOL-Library.Indicator_Function"
### 0.460s elapsed time, 2.624s 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
### Code generator: dropping subsumed code equation
### List.coset [] \<subseteq> set [] \<equiv> False
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.Countable"
### 1.603s elapsed time, 9.264s cpu time, 0.792s 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-Analysis.Product_Vector"
### 1.263s elapsed time, 7.220s cpu time, 0.792s 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")
### theory "HOL-Library.Nonpos_Ints"
### 0.374s elapsed time, 2.048s cpu time, 0.792s 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 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"
consts
  mset :: "'a list \<Rightarrow> 'a multiset"
### theory "HOL-Library.Cardinality"
### 1.371s elapsed time, 7.864s cpu time, 0.792s 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 periodic_fun_simple
  fixes f :: "'a \<Rightarrow> 'b"
    and period :: "'a"
  assumes "periodic_fun_simple f period"
locale periodic_fun_simple'
  fixes f :: "'a \<Rightarrow> 'b"
  assumes "periodic_fun_simple' f"
### theory "HOL-Library.Periodic_Fun"
### 0.140s elapsed time, 0.848s cpu time, 0.000s GC time
Loading theory "HOL-Library.Sum_of_Squares" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Norm_Arith")
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
class linorder = order +
  assumes "linear": "\<And>x y. x \<le> y \<or> y \<le> x"
### Rule already declared as safe introduction (intro!)
### True
### Ignoring duplicate introduction (intro)
### True
instantiation
  num1 :: linorder
  less_eq_num1 == less_eq :: num1 \<Rightarrow> num1 \<Rightarrow> bool
  less_num1 == less :: num1 \<Rightarrow> num1 \<Rightarrow> bool
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"
### theory "HOL-Library.Liminf_Limsup"
### 0.760s elapsed time, 4.324s cpu time, 0.792s GC time
instantiation
  bit0 :: (finite) {minus,one,plus,times,uminus,zero}
  bit1 :: (finite) {minus,one,plus,times,uminus,zero}
  zero_bit0 == zero_class.zero :: 'a bit0
  uminus_bit0 == uminus :: 'a bit0 \<Rightarrow> 'a bit0
  times_bit0 == times :: 'a bit0 \<Rightarrow> 'a bit0 \<Rightarrow> 'a bit0
  plus_bit0 == plus :: 'a bit0 \<Rightarrow> 'a bit0 \<Rightarrow> 'a bit0
  one_bit0 == one_class.one :: 'a bit0
  minus_bit0 == minus :: 'a bit0 \<Rightarrow> 'a bit0 \<Rightarrow> 'a bit0
  zero_bit1 == zero_class.zero :: 'a bit1
  uminus_bit1 == uminus :: 'a bit1 \<Rightarrow> 'a bit1
  times_bit1 == times :: 'a bit1 \<Rightarrow> 'a bit1 \<Rightarrow> 'a bit1
  plus_bit1 == plus :: 'a bit1 \<Rightarrow> 'a bit1 \<Rightarrow> 'a bit1
  one_bit1 == one_class.one :: 'a bit1
  minus_bit1 == minus :: 'a bit1 \<Rightarrow> 'a bit1 \<Rightarrow> 'a bit1
locale comm_monoid_mset
  fixes
    f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
      (infixl \<open>\<^bold>*\<close> 70)
    and z :: "'a"  (\<open>\<^bold>1\<close>)
  assumes "comm_monoid_mset (\<^bold>*) \<^bold>1"
### theory "HOL-Library.Countable_Set"
### 0.461s elapsed time, 2.756s 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")
class comm_monoid_add = ab_semigroup_add + monoid_add +
  assumes "add_0": "\<And>a. (0::'a) + a = a"
class comm_monoid_add = ab_semigroup_add + monoid_add +
  assumes "add_0": "\<And>a. (0::'a) + a = a"
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
class canonically_ordered_monoid_add = ordered_comm_monoid_add +
  assumes "le_iff_add": "\<And>a b. (a \<le> b) = (\<exists>c. b = a + c)"
instantiation
  num0 :: equal
  equal_num0 == equal_class.equal ::
    num0 \<Rightarrow> num0 \<Rightarrow> bool
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
  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
instantiation
  bit0 :: (finite) equal
  bit1 :: (finite) equal
  equal_bit0 == equal_class.equal ::
    'a bit0 \<Rightarrow> 'a bit0 \<Rightarrow> bool
  equal_bit1 == equal_class.equal ::
    'a bit1 \<Rightarrow> 'a bit1 \<Rightarrow> bool
instantiation
  bit0 :: (finite) enum
  enum_bit0 == enum_class.enum :: 'a bit0 list
  enum_all_bit0 == enum_class.enum_all ::
    ('a bit0 \<Rightarrow> bool) \<Rightarrow> bool
  enum_ex_bit0 == enum_class.enum_ex ::
    ('a bit0 \<Rightarrow> bool) \<Rightarrow> bool
instantiation
  bit1 :: (finite) enum
  enum_bit1 == enum_class.enum :: 'a bit1 list
  enum_all_bit1 == enum_class.enum_all ::
    ('a bit1 \<Rightarrow> bool) \<Rightarrow> bool
  enum_ex_bit1 == enum_class.enum_ex ::
    ('a bit1 \<Rightarrow> bool) \<Rightarrow> bool
class 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))"
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.Set_Idioms"
### 0.241s elapsed time, 1.452s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Abstract_Topology" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Connected" via "HOL-Analysis.Abstract_Topology_2")
### theory "HOL-Library.Numeral_Type"
### 0.801s elapsed time, 4.800s 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 comm_monoid_mult = ab_semigroup_mult + monoid_mult + dvd +
  assumes "mult_1": "\<And>a. (1::'a) * a = 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"
### theory "HOL-Analysis.Continuum_Not_Denumerable"
### 0.377s elapsed time, 2.168s cpu time, 0.544s GC time
Loading theory "HOL-Analysis.Elementary_Topology" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Connected" via "HOL-Analysis.Abstract_Topology_2")
class linorder = order +
  assumes "linear": "\<And>x y. x \<le> y \<or> y \<le> x"
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)"
instantiation
  multiset :: (preorder) order
  less_eq_multiset == less_eq ::
    'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool
  less_multiset == less ::
    'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool
instantiation
  multiset :: (preorder) ordered_ab_semigroup_add
### theory "HOL-Analysis.Euclidean_Space"
### 1.957s elapsed time, 11.656s cpu time, 0.544s GC time
Loading theory "HOL-Analysis.Finite_Cartesian_Product" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Space")
Proofs for inductive predicate(s) "pw_leq"
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)"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
locale countable_basis
  fixes p :: "'a set \<Rightarrow> bool"
    and B :: "'a set set"
  assumes "countable_basis p B"
class second_countable_topology = topological_space +
  assumes
    "ex_countable_subbasis":
      "\<exists>B. countable B \<and> open = generate_topology B"
Found termination order: "(\<lambda>p. length (fst p)) <*mlex*> {}"
instantiation
  multiset :: (equal) equal
  equal_multiset == equal_class.equal ::
    'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool
instantiation
  multiset :: (random) random
  random_multiset == random_class.random ::
    natural
    \<Rightarrow> natural \<times> natural
                  \<Rightarrow> ('a multiset \<times>
                                 (unit \<Rightarrow> term)) \<times>
                                natural \<times> natural
### 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
signature POSITIVSTELLENSATZ_TOOLS =
  sig
    val print_cert: RealArith.pss_tree -> string
    val read_cert: Proof.context -> string -> RealArith.pss_tree
  end
structure Positivstellensatz_Tools: POSITIVSTELLENSATZ_TOOLS
instantiation
  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 ...
### theory "HOL-Library.Countable_Complete_Lattices"
### 2.278s elapsed time, 13.500s cpu time, 1.040s GC time
Loading theory "HOL-Analysis.Linear_Algebra" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex" via "HOL-Analysis.Affine")
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.491s elapsed time, 26.420s cpu time, 1.832s 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")
### Ignoring duplicate rewrite rule:
### homeomorphic_map ?X1 ?Y1 id \<equiv> ?Y1 = ?X1
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
signature SUM_OF_SQUARES =
  sig
    exception Failure of string
    val debug: bool Config.T
    val debug_message: Proof.context -> (unit -> string) -> unit
    datatype proof_method
    = Certificate of RealArith.pss_tree | Prover of string -> string
    val sos_tac:
       (RealArith.pss_tree -> unit) ->
         proof_method -> Proof.context -> int -> tactic
    val trace: bool Config.T
    val trace_message: Proof.context -> (unit -> string) -> unit
  end
structure Sum_of_Squares: SUM_OF_SQUARES
instantiation
  vec :: (uminus, finite) uminus
  uminus_vec == uminus :: ('a, 'b) vec \<Rightarrow> ('a, 'b) vec
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"
### 2.934s elapsed time, 17.424s cpu time, 1.040s GC time
Loading theory "HOL-Library.Permutations" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants")
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
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 :: (metric_space, finite) dist
  dist_vec == dist ::
    ('a, 'b) vec \<Rightarrow> ('a, 'b) vec \<Rightarrow> real
instantiation
  vec :: (metric_space, finite) uniformity_dist
  uniformity_vec == uniformity ::
    (('a, 'b) vec \<times> ('a, 'b) vec) filter
instantiation
  vec :: (metric_space, finite) metric_space
instantiation
  vec :: (real_normed_vector, finite) real_normed_vector
  sgn_vec == sgn :: ('a, 'b) vec \<Rightarrow> ('a, 'b) vec
  norm_vec == norm :: ('a, 'b) vec \<Rightarrow> real
instantiation
  vec :: (real_inner, finite) real_inner
  inner_vec == inner ::
    ('a, 'b) vec \<Rightarrow> ('a, 'b) vec \<Rightarrow> real
instantiation
  vec :: (euclidean_space, finite) euclidean_space
  Basis_vec == Basis :: ('a, 'b) vec set
Proofs for inductive predicate(s) "swapidseq"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "HOL-Analysis.Elementary_Topology"
### 2.291s elapsed time, 13.552s cpu time, 0.996s 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")
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 ...
### theory "HOL-Analysis.Linear_Algebra"
### 1.158s elapsed time, 6.832s cpu time, 0.500s GC time
Loading theory "HOL-Analysis.Affine" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex")
Found termination order: "(\<lambda>p. size_list size (fst p)) <*mlex*> {}"
### theory "HOL-Library.Permutations"
### 0.899s elapsed time, 5.284s cpu time, 0.500s GC time
Loading theory "HOL-Analysis.Norm_Arith" (required by "HOL-Analysis.Analysis")
### theory "HOL-Analysis.Finite_Cartesian_Product"
### 2.053s elapsed time, 12.120s cpu time, 0.996s GC time
Loading theory "HOL-Analysis.Cartesian_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Determinants")
### theory "HOL-Analysis.Abstract_Topology"
### 3.119s elapsed time, 18.440s cpu time, 1.540s GC time
Loading theory "HOL-Analysis.Abstract_Limits" (required by "HOL-Analysis.Analysis")
### theory "HOL-Library.Order_Continuity"
### 0.668s elapsed time, 4.016s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Abstract_Topology_2" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Connected")
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)"
### theory "HOL-Analysis.Abstract_Limits"
### 0.398s elapsed time, 2.276s cpu time, 0.612s 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")
### 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.465s elapsed time, 2.680s cpu time, 0.612s GC time
class infinity = type +
  fixes infinity :: "'a"
### theory "HOL-Analysis.Affine"
### 0.649s elapsed time, 3.788s cpu time, 0.612s GC time
Loading theory "HOL-Analysis.Convex" (required by "HOL-Analysis.Analysis")
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 ...
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"
### 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
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 :: comm_monoid_add
  plus_enat == plus :: enat \<Rightarrow> enat \<Rightarrow> enat
instantiation
  enat :: {comm_semiring_1,semiring_no_zero_divisors}
  times_enat == times :: enat \<Rightarrow> enat \<Rightarrow> enat
instantiation
  enat :: minus
  minus_enat == minus :: enat \<Rightarrow> enat \<Rightarrow> enat
instantiation
  enat :: linordered_ab_semigroup_add
  less_eq_enat == less_eq :: enat \<Rightarrow> enat \<Rightarrow> bool
  less_enat == less :: enat \<Rightarrow> enat \<Rightarrow> bool
instantiation
  enat :: {order_bot,order_top}
  top_enat == top :: enat
  bot_enat == bot :: enat
structure Cancel_Enat_Common:
  sig
    val dest_sum: term -> term list
    val dest_summing: term * term list -> term list
    val find_first: term -> term list -> term list
    val find_first_t: term list -> term -> term list -> term list
    val mk_eq: term * term -> term
    val mk_sum: typ -> term list -> term
    val norm_ss: simpset
    val norm_tac: Proof.context -> tactic
    val simplify_meta_eq: Proof.context -> thm -> thm -> thm
    val trans_tac: Proof.context -> thm option -> tactic
  end
structure Eq_Enat_Cancel:
  sig val proc: Proof.context -> term -> thm option end
structure Le_Enat_Cancel:
  sig val proc: Proof.context -> term -> thm option end
structure Less_Enat_Cancel:
  sig val proc: Proof.context -> term -> thm option end
instantiation
  enat :: complete_lattice
  Inf_enat == Inf :: enat set \<Rightarrow> enat
  Sup_enat == Sup :: enat set \<Rightarrow> enat
  sup_enat == sup :: enat \<Rightarrow> enat \<Rightarrow> enat
  inf_enat == inf :: enat \<Rightarrow> enat \<Rightarrow> enat
### theory "HOL-Library.Extended_Nat"
### 0.799s elapsed time, 4.792s cpu time, 0.000s 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")
### theory "HOL-Analysis.Cartesian_Space"
### 1.225s elapsed time, 7.236s cpu time, 0.612s GC time
Loading theory "HOL-Analysis.Determinants" (required by "HOL-Analysis.Analysis")
class factorial_semiring = normalization_semidom +
  assumes
    "prime_factorization_exists":
      "\<And>x.
          x \<noteq> (0::'a) \<Longrightarrow>
          \<exists>A.
             (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and>
             normalize (prod_mset A) = normalize x"
### theory "HOL-Analysis.Convex"
### 2.151s elapsed time, 11.200s cpu time, 4.872s GC time
instantiation
  enat :: linorder_topology
  open_enat == open :: enat set \<Rightarrow> bool
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.Abstract_Topology_2"
### 2.843s elapsed time, 15.216s cpu time, 5.728s 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")
### theory "HOL-Analysis.Determinants"
### 1.931s elapsed time, 9.860s cpu time, 5.116s GC time
instantiation
  ereal :: uminus
  uminus_ereal == uminus :: ereal \<Rightarrow> ereal
Found termination order: "{}"
instantiation
  ereal :: infinity
  infinity_ereal == infinity :: ereal
### theory "HOL-Analysis.Connected"
### 0.393s elapsed time, 2.316s cpu time, 0.000s 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
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"
### 0.880s elapsed time, 5.188s cpu time, 0.528s 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.278s elapsed time, 1.692s 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 :: 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.369s elapsed time, 2.200s cpu time, 0.428s 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.096s elapsed time, 0.584s cpu time, 0.000s GC time
class factorial_semiring_gcd = factorial_semiring + Gcd +
  assumes "gcd_eq_gcd_factorial": "\<And>a b. gcd a b = gcd_factorial a b"
    and "lcm_eq_lcm_factorial": "\<And>a b. lcm a b = lcm_factorial a b"
    and "Gcd_eq_Gcd_factorial": "\<And>A. Gcd A = Gcd_factorial A"
    and "Lcm_eq_Lcm_factorial": "\<And>A. Lcm A = Lcm_factorial A"
### theory "HOL-Analysis.Elementary_Metric_Spaces"
### 2.295s elapsed time, 13.648s cpu time, 0.956s 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-Library.Extended_Real"
### 4.643s elapsed time, 26.028s cpu time, 6.072s 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")
### theory "HOL-Analysis.Function_Metric"
### 0.345s elapsed time, 2.080s cpu time, 0.000s GC time
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
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
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
### theory "HOL-Analysis.Elementary_Normed_Spaces"
### 1.506s elapsed time, 9.040s cpu time, 0.448s GC time
Loading theory "HOL-Analysis.Topology_Euclidean_Space" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Convex_Euclidean_Space")
### Ignoring duplicate rewrite rule:
### f (0::'a) \<equiv> 0::'b
### Ignoring duplicate rewrite rule:
### f (0::'a) \<equiv> 0::'b
instantiation
  ennreal :: linear_continuum_topology
  open_ennreal == open :: ennreal set \<Rightarrow> bool
### theory "HOL-Library.Extended_Nonnegative_Real"
### 1.799s elapsed time, 10.760s cpu time, 0.908s 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"
### theory "HOL-Computational_Algebra.Factorial_Ring"
### 9.644s elapsed time, 55.800s cpu time, 8.548s 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 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-Analysis.Topology_Euclidean_Space"
### 2.385s elapsed time, 14.308s cpu time, 0.916s 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")
locale Dynkin_system
  fixes \<Omega> :: "'a set"
    and M :: "'a set set"
  assumes "Dynkin_system \<Omega> M"
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.561s elapsed time, 15.484s cpu time, 1.068s GC time
Loading theory "HOL-Analysis.Measurable" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.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"
### theory "HOL-Analysis.Line_Segment"
### 1.211s elapsed time, 7.368s cpu time, 0.612s GC time
### theory "HOL-Analysis.Convex_Euclidean_Space"
### 1.249s elapsed time, 7.596s cpu time, 0.612s 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")
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"
Loading theory "HOL-Analysis.Starlike" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Weierstrass_Theorems" via "HOL-Analysis.Path_Connected")
### theory "HOL-Analysis.Extended_Real_Limits"
### 1.270s elapsed time, 7.724s cpu time, 0.612s 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.Tagged_Division"
### 1.150s elapsed time, 6.888s cpu time, 0.776s GC time
### theory "HOL-Analysis.Measurable"
### 0.763s elapsed time, 4.556s cpu time, 0.776s 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")
class euclidean_semiring_gcd = normalization_euclidean_semiring + Gcd +
  assumes "gcd_eucl": "normalization_euclidean_semiring_class.gcd = gcd"
    and "lcm_eucl": "normalization_euclidean_semiring_class.lcm = lcm"
  assumes "Gcd_eucl": "normalization_euclidean_semiring_class.Gcd = Gcd"
    and "Lcm_eucl": "normalization_euclidean_semiring_class.Lcm = Lcm"
locale sigma_finite_measure
  fixes M :: "'a measure"
  assumes "sigma_finite_measure M"
### theory "HOL-Analysis.Summation_Tests"
### 1.207s elapsed time, 7.196s cpu time, 0.776s GC time
Loading theory "HOL-Analysis.Uniform_Limit" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative" via "HOL-Analysis.Bounded_Linear_Function")
class ordered_euclidean_space = Inf + Sup + euclidean_space + abs + inf +
  sup + ord +
  assumes
    "eucl_le":
      "\<And>x y.
          (x \<le> y) =
          (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"
  assumes
    "eucl_less_le_not_le":
      "\<And>x y. (x < y) = (x \<le> y \<and> \<not> y \<le> x)"
  assumes
    "eucl_inf":
      "\<And>x y.
          inf x y =
          (\<Sum>i\<in>Basis.
             inf (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
  assumes
    "eucl_sup":
      "\<And>x y.
          sup x y =
          (\<Sum>i\<in>Basis.
             sup (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
  assumes
    "eucl_Inf":
      "\<And>X.
          Inf X =
          (\<Sum>i\<in>Basis. (INF x\<in>X. x \<bullet> i) *\<^sub>R i)"
  assumes
    "eucl_Sup":
      "\<And>X.
          Sup X =
          (\<Sum>i\<in>Basis. (SUP x\<in>X. x \<bullet> i) *\<^sub>R i)"
  assumes
    "eucl_abs":
      "\<And>x.
          \<bar>x\<bar> =
          (\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar> *\<^sub>R i)"
### Ignoring duplicate rewrite rule:
### finite UNIV \<equiv> False
locale finite_measure
  fixes M :: "'a measure"
  assumes "finite_measure M"
### theory "HOL-Analysis.Uniform_Limit"
### 2.459s elapsed time, 12.644s cpu time, 7.692s GC time
Loading theory "HOL-Analysis.Bounded_Continuous_Function" (required by "HOL-Analysis.Analysis")
Loading theory "HOL-Analysis.Bounded_Linear_Function" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Derivative")
instantiation
  measure :: (type) order_bot
  bot_measure == bot :: 'a measure
  less_eq_measure == less_eq ::
    'a measure \<Rightarrow> 'a measure \<Rightarrow> bool
  less_measure == less ::
    'a measure \<Rightarrow> 'a measure \<Rightarrow> bool
Proofs for inductive predicate(s) "less_eq_measure"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
instantiation
  bcontfun :: (topological_space, metric_space) metric_space
  dist_bcontfun == dist ::
    'a \<Rightarrow>\<^sub>C 'b
    \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> real
  uniformity_bcontfun == uniformity ::
    ('a \<Rightarrow>\<^sub>C 'b \<times>
     'a \<Rightarrow>\<^sub>C 'b) filter
  open_bcontfun == open ::
    ('a \<Rightarrow>\<^sub>C 'b) set \<Rightarrow> bool
instantiation
  measure :: (type) semilattice_sup
  sup_measure == sup ::
    'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure
### theory "HOL-Analysis.Starlike"
### 3.909s elapsed time, 21.304s cpu time, 8.468s GC time
Loading theory "HOL-Analysis.Continuous_Extension" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Equivalence_Measurable_On_Borel")
instantiation
  measure :: (type) complete_lattice
  Inf_measure == Inf :: 'a measure set \<Rightarrow> 'a measure
  Sup_measure == Sup :: 'a measure set \<Rightarrow> 'a measure
  top_measure == top :: 'a measure
  inf_measure == inf ::
    'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure
instantiation
  bcontfun :: (topological_space, real_normed_vector) real_vector
  uminus_bcontfun == uminus ::
    'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b
  zero_bcontfun == zero_class.zero :: 'a \<Rightarrow>\<^sub>C 'b
  minus_bcontfun == minus ::
    'a \<Rightarrow>\<^sub>C 'b
    \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b
                  \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b
  plus_bcontfun == plus ::
    'a \<Rightarrow>\<^sub>C 'b
    \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b
                  \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b
  scaleR_bcontfun == scaleR ::
    real
    \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b
                  \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b
### theory "HOL-Analysis.Continuous_Extension"
### 0.212s elapsed time, 1.264s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Path_Connected" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Weierstrass_Theorems")
instantiation
  bcontfun :: (topological_space, real_normed_vector) real_normed_vector
  sgn_bcontfun == sgn ::
    'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b
  norm_bcontfun == norm :: 'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> real
### theory "HOL-Analysis.Bounded_Continuous_Function"
### 0.599s elapsed time, 3.572s cpu time, 0.000s GC time
### theory "HOL-Analysis.Measure_Space"
### 3.988s elapsed time, 21.768s cpu time, 7.692s GC time
Loading theory "HOL-Analysis.Caratheodory" (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")
### theory "HOL-Analysis.Caratheodory"
### 0.530s elapsed time, 3.088s cpu time, 0.000s GC time
instantiation
  blinfun :: (real_normed_vector, real_normed_vector) real_normed_vector
  uminus_blinfun == uminus ::
    'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b
  zero_blinfun == zero_class.zero :: 'a \<Rightarrow>\<^sub>L 'b
  minus_blinfun == minus ::
    'a \<Rightarrow>\<^sub>L 'b
    \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b
                  \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b
  plus_blinfun == plus ::
    'a \<Rightarrow>\<^sub>L 'b
    \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b
                  \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b
  sgn_blinfun == sgn ::
    'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b
  norm_blinfun == norm :: 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real
  scaleR_blinfun == scaleR ::
    real
    \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b
                  \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b
  dist_blinfun == dist ::
    'a \<Rightarrow>\<^sub>L 'b
    \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real
  uniformity_blinfun == uniformity ::
    ('a \<Rightarrow>\<^sub>L 'b \<times>
     'a \<Rightarrow>\<^sub>L 'b) filter
  open_blinfun == open ::
    ('a \<Rightarrow>\<^sub>L 'b) set \<Rightarrow> bool
locale bounded_bilinear
  fixes
    prod :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
      (infixl \<open>**\<close> 70)
  assumes "bounded_bilinear (**)"
instantiation
  prod :: (abs, abs) abs
  abs_prod == abs :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b
instantiation
  vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
  abs_vec == abs :: ('a, 'b) vec \<Rightarrow> ('a, 'b) vec
  inf_vec == inf ::
    ('a, 'b) vec \<Rightarrow> ('a, 'b) vec \<Rightarrow> ('a, 'b) vec
  sup_vec == sup ::
    ('a, 'b) vec \<Rightarrow> ('a, 'b) vec \<Rightarrow> ('a, 'b) vec
  Inf_vec == Inf :: ('a, 'b) vec set \<Rightarrow> ('a, 'b) vec
  Sup_vec == Sup :: ('a, 'b) vec set \<Rightarrow> ('a, 'b) vec
### theory "HOL-Analysis.Ordered_Euclidean_Space"
### 5.815s elapsed time, 32.536s cpu time, 9.216s GC time
locale bounded_bilinear
  fixes
    prod :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
      (infixl \<open>**\<close> 70)
  assumes "bounded_bilinear (**)"
### theory "HOL-Analysis.Bounded_Linear_Function"
### 2.482s elapsed time, 14.712s cpu time, 0.748s GC time
Loading theory "HOL-Analysis.Derivative" (required by "HOL-Analysis.Analysis")
### Ignoring duplicate rewrite rule:
### ?a1 * ?b1 \<le> (0::?'a1) \<equiv>
### (0::?'a1) \<le> ?a1 \<and> ?b1 \<le> (0::?'a1) \<or>
### ?a1 \<le> (0::?'a1) \<and> (0::?'a1) \<le> ?b1
### Introduced fixed type variable(s): 'd, 'e, 'f in "f__" or "g__"
### Introduced fixed type variable(s): 'h in "A__"
### theory "HOL-Analysis.Path_Connected"
### 2.399s elapsed time, 14.248s cpu time, 0.748s GC time
Loading theory "HOL-Analysis.Homotopy" (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")
Loading theory "HOL-Analysis.Locally" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Abstract_Euclidean_Space")
### theory "HOL-Analysis.Locally"
### 0.394s elapsed time, 2.344s cpu time, 0.752s GC time
### Introduced fixed type variable(s): 'a in "P__"
### theory "HOL-Analysis.Derivative"
### 2.360s elapsed time, 14.160s cpu time, 1.300s GC time
Loading theory "HOL-Analysis.Borel_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")
Loading theory "HOL-Analysis.Cartesian_Euclidean_Space" (required by "HOL-Analysis.Analysis")
Loading theory "HOL-Analysis.Complex_Analysis_Basics" (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")
Loading theory "HOL-Analysis.Lipschitz" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Multivariate_Analysis")
bundle lipschitz_syntax
bundle no_lipschitz_syntax
locale Retracts
  fixes s :: "'a set"
    and h :: "'a \<Rightarrow> 'b"
    and t :: "'b set"
    and k :: "'b \<Rightarrow> 'a"
  assumes "Retracts s h t k"
### theory "HOL-Analysis.Cartesian_Euclidean_Space"
### 0.395s elapsed time, 2.356s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Cross3" (required by "HOL-Analysis.Analysis")
### theory "HOL-Analysis.Lipschitz"
### 0.614s elapsed time, 3.676s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Polytope" (required by "HOL-Analysis.Analysis")
### theory "HOL-Analysis.Homotopy"
### 2.769s elapsed time, 16.596s cpu time, 1.360s GC time
Loading theory "HOL-Analysis.Homeomorphism" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration")
### theory "HOL-Analysis.Complex_Analysis_Basics"
### 1.367s elapsed time, 8.172s cpu time, 0.812s GC time
Loading theory "HOL-Analysis.Complex_Transcendental" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Ball_Volume" via "HOL-Analysis.Gamma_Function" via "HOL-Analysis.Harmonic_Numbers")
### theory "HOL-Analysis.Homeomorphism"
### 0.549s elapsed time, 3.312s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Brouwer_Fixpoint" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Fashoda_Theorem")
bundle cross3_syntax
bundle no_cross3_syntax
instantiation
  complex :: ln
  ln_complex == ln :: complex \<Rightarrow> complex
### theory "HOL-Analysis.Polytope"
### 1.923s elapsed time, 11.504s cpu time, 1.656s GC time
Loading theory "HOL-Analysis.Abstract_Euclidean_Space" (required by "HOL-Analysis.Analysis")
### theory "HOL-Analysis.Borel_Space"
### 2.607s elapsed time, 15.596s cpu time, 1.656s GC time
Loading theory "HOL-Analysis.Nonnegative_Lebesgue_Integration" (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")
locale kuhn_simplex
  fixes p :: "nat"
    and n :: "nat"
    and base :: "nat \<Rightarrow> nat"
    and upd :: "nat \<Rightarrow> nat"
    and s :: "(nat \<Rightarrow> nat) set"
  assumes "kuhn_simplex p n base upd s"
### theory "HOL-Computational_Algebra.Euclidean_Algorithm"
### 13.619s elapsed time, 79.440s cpu time, 12.784s GC time
Loading theory "HOL-Computational_Algebra.Primes" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Jordan_Curve" via "HOL-Analysis.Arcwise_Connected")
locale kuhn_simplex_pair
  fixes p :: "nat"
    and n :: "nat"
    and b_s :: "nat \<Rightarrow> nat"
    and u_s :: "nat \<Rightarrow> nat"
    and s :: "(nat \<Rightarrow> nat) set"
    and b_t :: "nat \<Rightarrow> nat"
    and u_t :: "nat \<Rightarrow> nat"
    and t :: "(nat \<Rightarrow> nat) set"
  assumes "kuhn_simplex_pair p n b_s u_s s b_t u_t t"
Proofs for inductive predicate(s) "ksimplex"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "HOL-Analysis.Abstract_Euclidean_Space"
### 0.356s elapsed time, 2.144s cpu time, 0.000s GC time
Loading theory "HOL-Computational_Algebra.Formal_Power_Series" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.FPS_Convergence")
### theory "HOL-Computational_Algebra.Primes"
### 0.295s elapsed time, 1.784s cpu time, 0.000s GC time
Loading theory "HOL-Analysis.Regularity" (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")
### theory "HOL-Analysis.Brouwer_Fixpoint"
### 1.625s elapsed time, 9.748s cpu time, 0.844s GC time
Loading theory "HOL-Analysis.Arcwise_Connected" (required by "HOL-Analysis.Analysis" via "HOL-Analysis.Jordan_Curve")
*** Interrupt