Loading theory "E_Transcendental.Cong" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues") Loading theory "E_Transcendental.Eratosthenes" (required by "E_Transcendental.Number_Theory") class cong = type + fixes cong :: "'a \ 'a \ 'a \ bool" instantiation nat :: cong cong_nat == cong :: nat \ nat \ nat \ bool instantiation int :: cong cong_int == cong :: int \ int \ int \ bool Found termination order: "(\p. length (snd p)) <*mlex*> {}" ### theory "E_Transcendental.Eratosthenes" ### 0.452s elapsed time, 0.964s cpu time, 0.000s GC time Loading theory "E_Transcendental.Totient" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues") ### theory "E_Transcendental.Totient" ### 0.175s elapsed time, 0.352s cpu time, 0.000s GC time Loading theory "E_Transcendental.Congruence" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues" via "E_Transcendental.More_Group" via "E_Transcendental.Ring" via "E_Transcendental.FiniteProduct" via "E_Transcendental.Group" via "E_Transcendental.Complete_Lattice" via "E_Transcendental.Lattice" via "E_Transcendental.Order") ### theory "E_Transcendental.Cong" ### 0.676s elapsed time, 1.404s cpu time, 0.000s GC time Loading theory "E_Transcendental.Fib" (required by "E_Transcendental.Number_Theory") Found termination order: "size <*mlex*> {}" Found termination order: "(\p. size (snd (snd p))) <*mlex*> {}" ### theory "E_Transcendental.Fib" ### 0.532s elapsed time, 1.068s cpu time, 0.000s GC time locale equivalence = fixes S :: "('a, 'b) eq_object_scheme" assumes "equivalence S" ### theory "E_Transcendental.Congruence" ### 1.233s elapsed time, 2.432s cpu time, 0.272s GC time Loading theory "E_Transcendental.Order" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues" via "E_Transcendental.More_Group" via "E_Transcendental.Ring" via "E_Transcendental.FiniteProduct" via "E_Transcendental.Group" via "E_Transcendental.Complete_Lattice" via "E_Transcendental.Lattice") locale weak_partial_order = fixes L :: "('a, 'b) gorder_scheme" assumes "weak_partial_order L" locale weak_partial_order = fixes L :: "('a, 'b) gorder_scheme" assumes "weak_partial_order L" locale weak_partial_order = fixes L :: "('a, 'b) gorder_scheme" assumes "weak_partial_order L" locale partial_order = fixes L :: "('a, 'b) gorder_scheme" assumes "partial_order L" locale weak_partial_order_bottom = fixes L :: "('a, 'b) gorder_scheme" assumes "weak_partial_order_bottom L" locale weak_partial_order_top = fixes L :: "('a, 'b) gorder_scheme" assumes "weak_partial_order_top L" locale weak_total_order = fixes L :: "('a, 'b) gorder_scheme" assumes "weak_total_order L" locale total_order = fixes L :: "('a, 'b) gorder_scheme" assumes "total_order L" ### theory "E_Transcendental.Order" ### 1.162s elapsed time, 2.332s cpu time, 0.000s GC time Loading theory "E_Transcendental.Lattice" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues" via "E_Transcendental.More_Group" via "E_Transcendental.Ring" via "E_Transcendental.FiniteProduct" via "E_Transcendental.Group" via "E_Transcendental.Complete_Lattice") locale weak_upper_semilattice = fixes L :: "('a, 'b) gorder_scheme" assumes "weak_upper_semilattice L" locale weak_lower_semilattice = fixes L :: "('a, 'b) gorder_scheme" assumes "weak_lower_semilattice L" locale weak_lattice = fixes L :: "('a, 'b) gorder_scheme" assumes "weak_lattice L" locale weak_bounded_lattice = fixes L :: "('a, 'b) gorder_scheme" assumes "weak_bounded_lattice L" locale upper_semilattice = fixes L :: "('a, 'b) gorder_scheme" assumes "upper_semilattice L" locale lower_semilattice = fixes L :: "('a, 'b) gorder_scheme" assumes "lower_semilattice L" locale Lattice.lattice = fixes L :: "('a, 'b) gorder_scheme" assumes "lattice L" locale Lattice.bounded_lattice = fixes L :: "('a, 'b) gorder_scheme" assumes "bounded_lattice L" locale Lattice.bounded_lattice = fixes L :: "('a, 'b) gorder_scheme" assumes "bounded_lattice L" ### theory "E_Transcendental.Lattice" ### 1.595s elapsed time, 3.124s cpu time, 0.484s GC time Loading theory "E_Transcendental.Complete_Lattice" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues" via "E_Transcendental.More_Group" via "E_Transcendental.Ring" via "E_Transcendental.FiniteProduct" via "E_Transcendental.Group") locale weak_complete_lattice = fixes L :: "('a, 'b) gorder_scheme" assumes "weak_complete_lattice L" locale weak_complete_lattice = fixes L :: "('a, 'b) gorder_scheme" assumes "weak_complete_lattice L" locale weak_complete_lattice = fixes L :: "('a, 'b) gorder_scheme" assumes "weak_complete_lattice L" locale Complete_Lattice.complete_lattice = fixes L :: "('a, 'b) gorder_scheme" assumes "complete_lattice L" locale Complete_Lattice.complete_lattice = fixes L :: "('a, 'b) gorder_scheme" assumes "complete_lattice L" locale weak_complete_lattice = fixes L :: "('a, 'b) gorder_scheme" assumes "weak_complete_lattice L" ### theory "E_Transcendental.Complete_Lattice" ### 0.878s elapsed time, 1.760s cpu time, 0.000s GC time Loading theory "E_Transcendental.Group" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues" via "E_Transcendental.More_Group" via "E_Transcendental.Ring" via "E_Transcendental.FiniteProduct") overloading nat_pow \ pow :: ('a, 'b) monoid_scheme \ 'a \ nat \ 'a overloading int_pow \ pow :: ('a, 'b) monoid_scheme \ 'a \ int \ 'a locale Group.monoid = fixes G :: "('a, 'b) monoid_scheme" assumes "Group.monoid G" locale Group.group = fixes G :: "('a, 'b) monoid_scheme" assumes "Group.group G" locale subgroup = fixes H :: "'a set" and G :: "('a, 'b) monoid_scheme" assumes "subgroup H G" locale group_hom = fixes G :: "('a, 'b) monoid_scheme" and H :: "('c, 'd) monoid_scheme" and h :: "'a \ 'c" assumes "group_hom G H h" locale Group.comm_monoid = fixes G :: "('a, 'b) monoid_scheme" assumes "Group.comm_monoid G" locale comm_group = fixes G :: "('a, 'b) monoid_scheme" assumes "comm_group G" ### theory "E_Transcendental.Group" ### 1.589s elapsed time, 3.128s cpu time, 0.524s GC time Loading theory "E_Transcendental.Coset" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues" via "E_Transcendental.Multiplicative_Group") locale normal = fixes H :: "'a set" and G :: "('a, 'b) monoid_scheme" assumes "normal H G" ### Ambiguous input (line 596 of "~~/src/HOL/Algebra/Coset.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^fixed>r_congruent_indexed" ("_index" ("_position" G)) ### ("\<^const>HOL.eq" ("_position" H) ### ("_Coll" ("_pattern" ("_position" x) ("_position" y)) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ("_position" x) ### ("_applC" ("_position" carrier) ("_position" G))) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ("_position" y) ### ("_applC" ("_position" carrier) ("_position" G))) ### ("\<^const>Set.member" ### ("\<^const>Group.monoid.mult_indexed" ### ("\<^const>Group.m_inv_indexed" ("_index" ("_position" G)) ### ("_position" x)) ### ("_index" ("_position" G)) ("_position" y)) ### ("_position" H)))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^fixed>r_congruent_indexed" ("_index" ("_position" G)) ### ("_position" H)) ### ("_Coll" ("_pattern" ("_position" x) ("_position" y)) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ("_position" x) ### ("_applC" ("_position" carrier) ("_position" G))) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ("_position" y) ### ("_applC" ("_position" carrier) ("_position" G))) ### ("\<^const>Set.member" ### ("\<^const>Group.monoid.mult_indexed" ### ("\<^const>Group.m_inv_indexed" ("_index" ("_position" G)) ### ("_position" x)) ### ("_index" ("_position" G)) ("_position" y)) ### ("_position" H))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 648 of "~~/src/HOL/Algebra/Coset.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Coset.l_coset_indexed" ("_position" a) ("_indexdefault") ### ("_position" H)) ### ("\<^const>Coset.r_congruent_indexed" ("_indexdefault") ### ("\<^const>Relation.Image" ("_position" H) ### ("_Finset" ("_position" a)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Coset.l_coset_indexed" ("_position" a) ("_indexdefault") ### ("_position" H)) ### ("\<^const>Relation.Image" ### ("\<^const>Coset.r_congruent_indexed" ("_indexdefault") ### ("_position" H)) ### ("_Finset" ("_position" a))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### theory "E_Transcendental.Coset" ### 1.070s elapsed time, 2.144s cpu time, 0.000s GC time Loading theory "E_Transcendental.FiniteProduct" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues" via "E_Transcendental.More_Group" via "E_Transcendental.Ring") Proofs for inductive predicate(s) "foldSetDp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... locale LCD = fixes B :: "'b set" and D :: "'a set" and f :: "'b \ 'a \ 'a" assumes "LCD B D op \" locale ACeD = fixes D :: "'a set" and f :: "'a \ 'a \ 'a" and e :: "'a" assumes "ACeD D op \ e" locale Group.comm_monoid = fixes G :: "('a, 'b) monoid_scheme" assumes "Group.comm_monoid G" locale Group.comm_monoid = fixes G :: "('a, 'b) monoid_scheme" assumes "Group.comm_monoid G" ### theory "E_Transcendental.FiniteProduct" ### 0.679s elapsed time, 1.360s cpu time, 0.000s GC time Loading theory "E_Transcendental.Ring" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues" via "E_Transcendental.More_Group") locale abelian_monoid = fixes G :: "('a, 'b) ring_scheme" assumes "abelian_monoid G" locale abelian_group = fixes G :: "('a, 'b) ring_scheme" assumes "abelian_group G" locale abelian_monoid = fixes G :: "('a, 'b) ring_scheme" assumes "abelian_monoid G" locale abelian_monoid = fixes G :: "('a, 'b) ring_scheme" assumes "abelian_monoid G" locale abelian_group = fixes G :: "('a, 'b) ring_scheme" assumes "abelian_group G" locale Ring.semiring = fixes R :: "('a, 'b) ring_scheme" assumes "semiring R" locale Ring.ring = fixes R :: "('a, 'b) ring_scheme" assumes "ring R" locale cring = fixes R :: "('a, 'b) ring_scheme" assumes "cring R" locale domain = fixes R :: "('a, 'b) ring_scheme" assumes "domain R" locale Ring.field = fixes R :: "('a, 'b) ring_scheme" assumes "field R" locale Ring.ring = fixes R :: "('a, 'b) ring_scheme" assumes "ring R" locale Ring.ring = fixes R :: "('a, 'b) ring_scheme" assumes "ring R" ### ML warning (line 45 of "~~/src/HOL/Algebra/ringsimp.ML"): ### Value identifier (s) has not been referenced. ### ML warning (line 48 of "~~/src/HOL/Algebra/ringsimp.ML"): ### Matches are not exhaustive. signature RINGSIMP = sig val add_struct: string * term list -> attribute val algebra_tac: Proof.context -> int -> tactic val del_struct: string * term list -> attribute val print_structures: Proof.context -> unit end structure Ringsimp: RINGSIMP locale Ring.semiring = fixes R :: "('a, 'b) ring_scheme" assumes "semiring R" locale domain = fixes R :: "('a, 'b) ring_scheme" assumes "domain R" locale ring_hom_cring = fixes R :: "('a, 'b) ring_scheme" and S :: "('c, 'd) ring_scheme" and h :: "'a \ 'c" assumes "ring_hom_cring R S h" ### theory "E_Transcendental.Ring" ### 3.808s elapsed time, 7.532s cpu time, 0.584s GC time Loading theory "E_Transcendental.AbelCoset" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues" via "E_Transcendental.Multiplicative_Group" via "E_Transcendental.UnivPoly" via "E_Transcendental.RingHom" via "E_Transcendental.Ideal") Loading theory "E_Transcendental.Module" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues" via "E_Transcendental.Multiplicative_Group" via "E_Transcendental.UnivPoly") locale abelian_group_hom = fixes G :: "('a, 'b) ring_scheme" and H :: "('c, 'd) ring_scheme" and h :: "'a \ 'c" assumes "abelian_group_hom G H h" locale module = fixes R :: "('a, 'b) ring_scheme" and M :: "('a, 'c, 'd) module_scheme" assumes "module R M" locale algebra = fixes R :: "('a, 'b) ring_scheme" and M :: "('a, 'c, 'd) module_scheme" assumes "algebra R M" locale additive_subgroup = fixes H :: "'a set" and G :: "('a, 'b) ring_scheme" assumes "additive_subgroup H G" locale abelian_subgroup = fixes H :: "'a set" and G :: "('a, 'b) ring_scheme" assumes "abelian_subgroup H G" ### theory "E_Transcendental.Module" ### 2.276s elapsed time, 4.512s cpu time, 0.316s GC time Loading theory "E_Transcendental.More_Group" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues") ### theory "E_Transcendental.More_Group" ### 0.173s elapsed time, 0.348s cpu time, 0.000s GC time Loading theory "E_Transcendental.More_Finite_Product" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues") ### theory "E_Transcendental.More_Finite_Product" ### 0.673s elapsed time, 1.308s cpu time, 0.440s GC time Loading theory "E_Transcendental.More_Ring" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues") ### theory "E_Transcendental.More_Ring" ### 0.313s elapsed time, 0.628s cpu time, 0.000s GC time ### theory "E_Transcendental.AbelCoset" ### 6.999s elapsed time, 13.848s cpu time, 1.264s GC time Loading theory "E_Transcendental.Ideal" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues" via "E_Transcendental.Multiplicative_Group" via "E_Transcendental.UnivPoly" via "E_Transcendental.RingHom") locale ideal = fixes I :: "'a set" and R :: "('a, 'b) ring_scheme" assumes "ideal I R" locale principalideal = fixes I :: "'a set" and R :: "('a, 'b) ring_scheme" assumes "principalideal I R" locale maximalideal = fixes I :: "'a set" and R :: "('a, 'b) ring_scheme" assumes "maximalideal I R" locale primeideal = fixes I :: "'a set" and R :: "('a, 'b) ring_scheme" assumes "primeideal I R" ### Rule already declared as introduction (intro) ### \?P ?x; ?x \ ?A\ ### \ \x\?A. ?P x ### Rule already declared as introduction (intro) ### \?b = ?f ?x; ?x \ ?A\ \ ?b \ ?f ` ?A ### Rule already declared as introduction (intro) ### \?b = ?f ?x; ?x \ ?A\ \ ?b \ ?f ` ?A ### theory "E_Transcendental.Ideal" ### 4.792s elapsed time, 9.492s cpu time, 0.724s GC time Loading theory "E_Transcendental.RingHom" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues" via "E_Transcendental.Multiplicative_Group" via "E_Transcendental.UnivPoly") locale ring_hom_ring = fixes R :: "('a, 'b) ring_scheme" and S :: "('c, 'd) ring_scheme" and h :: "'a \ 'c" assumes "ring_hom_ring R S h" ### theory "E_Transcendental.RingHom" ### 1.855s elapsed time, 3.672s cpu time, 0.296s GC time Loading theory "E_Transcendental.UnivPoly" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues" via "E_Transcendental.Multiplicative_Group") locale bound = fixes z :: "'a" and n :: "nat" and f :: "nat \ 'a" assumes "bound z n f" locale Ring.ring = fixes R :: "('a, 'b) ring_scheme" assumes "ring R" locale UP = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "P \ UP R" locale UP_ring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_ring R" and "P \ UP R" locale UP_cring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_cring R" and "P \ UP R" locale UP_domain = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_domain R" and "P \ UP R" locale UP = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "P \ UP R" locale UP_ring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_ring R" and "P \ UP R" locale UP_ring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_ring R" and "P \ UP R" locale UP_ring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_ring R" and "P \ UP R" locale UP_cring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_cring R" and "P \ UP R" locale UP_ring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_ring R" and "P \ UP R" locale UP_ring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_ring R" and "P \ UP R" locale UP_ring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_ring R" and "P \ UP R" locale UP_ring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_ring R" and "P \ UP R" locale UP_domain = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_domain R" and "P \ UP R" locale UP_ring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_ring R" and "P \ UP R" locale UP_domain = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_domain R" and "P \ UP R" locale UP_ring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_ring R" and "P \ UP R" locale UP_domain = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_domain R" and "P \ UP R" locale Ring.ring = fixes R :: "('a, 'b) ring_scheme" assumes "ring R" locale UP = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "P \ UP R" locale UP_pre_univ_prop = fixes R :: "('a, 'b) ring_scheme" and S :: "('c, 'd) ring_scheme" and h :: "'a \ 'c" and P :: "('a, nat \ 'a) up_ring" assumes "UP_pre_univ_prop R S h" and "P \ UP R" locale UP_univ_prop = fixes R :: "('a, 'b) ring_scheme" and S :: "('c, 'd) ring_scheme" and h :: "'a \ 'c" and P :: "('a, nat \ 'a) up_ring" and s :: "'c" and Eval :: "(nat \ 'a) \ 'c" assumes "UP_univ_prop R S h s" and "P \ UP R" and "Eval \ eval R S h s" locale UP_pre_univ_prop = fixes R :: "('a, 'b) ring_scheme" and S :: "('c, 'd) ring_scheme" and h :: "'a \ 'c" and P :: "('a, nat \ 'a) up_ring" assumes "UP_pre_univ_prop R S h" and "P \ UP R" locale UP_pre_univ_prop = fixes R :: "('a, 'b) ring_scheme" and S :: "('c, 'd) ring_scheme" and h :: "'a \ 'c" and P :: "('a, nat \ 'a) up_ring" assumes "UP_pre_univ_prop R S h" and "P \ UP R" locale Group.monoid = fixes G :: "('a, 'b) monoid_scheme" assumes "Group.monoid G" locale UP_ring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_ring R" and "P \ UP R" locale UP_cring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_cring R" and "P \ UP R" locale UP_cring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_cring R" and "P \ UP R" ### theory "E_Transcendental.UnivPoly" ### 14.093s elapsed time, 27.924s cpu time, 2.124s GC time Loading theory "E_Transcendental.Multiplicative_Group" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Residues") locale UP_ring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_ring R" and "P \ UP R" locale UP_cring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_cring R" and "P \ UP R" locale Group.group = fixes G :: "('a, 'b) monoid_scheme" assumes "Group.group G" locale Ring.field = fixes R :: "('a, 'b) ring_scheme" assumes "field R" locale UP_cring = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_cring R" and "P \ UP R" locale UP_domain = fixes R :: "('a, 'b) ring_scheme" and P :: "('a, nat \ 'a) up_ring" assumes "UP_domain R" and "P \ UP R" locale Ring.field = fixes R :: "('a, 'b) ring_scheme" assumes "field R" ### theory "E_Transcendental.Multiplicative_Group" ### 3.202s elapsed time, 6.368s cpu time, 0.312s GC time Loading theory "E_Transcendental.Residues" (required by "E_Transcendental.Number_Theory") locale residues = fixes m :: "int" and R :: "int ring" assumes "residues m" and "R \ residue_ring m" locale residues = fixes m :: "int" and R :: "int ring" assumes "residues m" and "R \ residue_ring m" locale residues_prime = fixes p :: "nat" and R :: "int ring" assumes "residues_prime p" and "R \ residue_ring (int p)" locale residues_prime = fixes p :: "nat" and R :: "int ring" assumes "residues_prime p" and "R \ residue_ring (int p)" ### theory "E_Transcendental.Residues" ### 3.532s elapsed time, 6.984s cpu time, 0.516s GC time Loading theory "E_Transcendental.Euler_Criterion" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Quadratic_Reciprocity" via "E_Transcendental.Gauss") Loading theory "E_Transcendental.Pocklington" (required by "E_Transcendental.Number_Theory") ### theory "E_Transcendental.Euler_Criterion" ### 0.260s elapsed time, 0.520s cpu time, 0.000s GC time Loading theory "E_Transcendental.Gauss" (required by "E_Transcendental.Number_Theory" via "E_Transcendental.Quadratic_Reciprocity") locale GAUSS = fixes p :: "nat" and a :: "int" assumes "GAUSS p a" ### theory "E_Transcendental.Pocklington" ### 0.356s elapsed time, 0.716s cpu time, 0.000s GC time ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### theory "E_Transcendental.Gauss" ### 0.358s elapsed time, 0.724s cpu time, 0.000s GC time Loading theory "E_Transcendental.Quadratic_Reciprocity" (required by "E_Transcendental.Number_Theory") locale QR = fixes p :: "nat" and q :: "nat" assumes "QR p q" ### theory "E_Transcendental.Quadratic_Reciprocity" ### 0.715s elapsed time, 1.388s cpu time, 0.308s GC time Loading theory "E_Transcendental.Number_Theory" ### theory "E_Transcendental.Number_Theory" ### 1.227s elapsed time, 2.456s cpu time, 0.000s GC time ### Ignoring duplicate rewrite rule: ### \?x1 \ carrier R; ?y1 \ carrier R\ ### \ ?x1 \ ?y1 \ carrier R \ True ### Ignoring duplicate rewrite rule: ### \ \ carrier R \ True ### Ignoring duplicate rewrite rule: ### ?x1 \ carrier R \ ### \ ?x1 \ carrier R \ True ### Ignoring duplicate rewrite rule: ### \?x1 \ carrier R; ?y1 \ carrier R\ ### \ ?x1 \ ?y1 \ carrier R \ True ### Ignoring duplicate rewrite rule: ### \?x1 \ carrier R; ?y1 \ carrier R\ ### \ ?x1 \ ?y1 \ carrier R \ True ### Ignoring duplicate rewrite rule: ### \ \ carrier R \ True ### Ignoring duplicate rewrite rule: ### ?y \ carrier R \ \ \ ?y \ ?y ### Ignoring duplicate rewrite rule: ### ?y \ carrier R \ \ \ ?y \ ?y ### Ignoring duplicate rewrite rule: ### ?y \ carrier R \ ?y \ \ \ ?y ### Ignoring duplicate rewrite rule: ### ?y \ carrier R \ \ (\ ?y) \ ?y ### Ignoring duplicate rewrite rule: ### \ \ \ \ ### Ignoring duplicate rewrite rule: ### ?x1 \ carrier R \ \ \ ?x1 \ \ ### Ignoring duplicate rewrite rule: ### ?x1 \ carrier R \ ?x1 \ \ \ \ ### Ignoring duplicate rewrite rule: ### \?x1 \ carrier R; ?y1 \ carrier R\ ### \ ?x1 \ ?y1 \ carrier R \ True ### Ignoring duplicate rewrite rule: ### \ \ carrier R \ True ### Ignoring duplicate rewrite rule: ### ?x1 \ carrier R \ ### \ ?x1 \ carrier R \ True ### Ignoring duplicate rewrite rule: ### \?x1 \ carrier R; ?y1 \ carrier R\ ### \ ?x1 \ ?y1 \ carrier R \ True ### Ignoring duplicate rewrite rule: ### \?x1 \ carrier R; ?y1 \ carrier R\ ### \ ?x1 \ ?y1 \ carrier R \ True ### Ignoring duplicate rewrite rule: ### \ \ carrier R \ True ### Ignoring duplicate rewrite rule: ### ?y \ carrier R \ \ \ ?y \ ?y ### Ignoring duplicate rewrite rule: ### ?y \ carrier R \ \ \ ?y \ ?y ### Ignoring duplicate rewrite rule: ### ?y \ carrier R \ ?y \ \ \ ?y ### Ignoring duplicate rewrite rule: ### ?y \ carrier R \ \ (\ ?y) \ ?y ### Ignoring duplicate rewrite rule: ### \ \ \ \ ### Ignoring duplicate rewrite rule: ### ?x1 \ carrier R \ \ \ ?x1 \ \ ### Ignoring duplicate rewrite rule: ### ?x1 \ carrier R \ ?x1 \ \ \ \ ### Ignoring duplicate rewrite rule: ### \?x1 \ carrier R; ?y1 \ carrier R\ ### \ ?x1 \ ?y1 \ carrier R \ True ### Ignoring duplicate rewrite rule: ### \ \ carrier R \ True ### Ignoring duplicate rewrite rule: ### ?x1 \ carrier R \ ### \ ?x1 \ carrier R \ True ### Ignoring duplicate rewrite rule: ### \?x1 \ carrier R; ?y1 \ carrier R\ ### \ ?x1 \ ?y1 \ carrier R \ True ### Ignoring duplicate rewrite rule: ### \?x1 \ carrier R; ?y1 \ carrier R\ ### \ ?x1 \ ?y1 \ carrier R \ True ### Ignoring duplicate rewrite rule: ### \ \ carrier R \ True ### Ignoring duplicate rewrite rule: ### ?y \ carrier R \ \ \ ?y \ ?y ### Ignoring duplicate rewrite rule: ### ?y \ carrier R \ \ \ ?y \ ?y ### Ignoring duplicate rewrite rule: ### ?y \ carrier R \ ?y \ \ \ ?y ### Ignoring duplicate rewrite rule: ### ?y \ carrier R \ \ (\ ?y) \ ?y ### Ignoring duplicate rewrite rule: ### \ \ \ \ ### Ignoring duplicate rewrite rule: ### ?x1 \ carrier R \ \ \ ?x1 \ \ ### Ignoring duplicate rewrite rule: ### ?x1 \ carrier R \ ?x1 \ \ \ \ ### Rule already declared as introduction (intro) ### \?b = ?f ?x; ?x \ ?A\ \ ?b \ ?f ` ?A ### Ignoring duplicate rewrite rule: ### ?a1 dvd ?y \ ?a1 * (?y div ?a1) \ ?y ### Ignoring duplicate rewrite rule: ### ?a1 dvd ?y \ ?a1 * (?y div ?a1) \ ?y ### Legacy feature! Old 'def' command -- use 'define' instead Loading theory "E_Transcendental.E_Transcendental" locale lindemann_weierstrass_aux = fixes f :: "complex poly" ### theory "E_Transcendental.E_Transcendental" ### 1.640s elapsed time, 2.036s cpu time, 0.000s GC time ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Rule already declared as introduction (intro) ### (\i. continuous_on UNIV (\