diff --git a/CONTRIBUTORS b/CONTRIBUTORS --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -1,994 +1,997 @@ For the purposes of the license agreement in the file COPYRIGHT, a 'contributor' is anybody who is listed in this file (CONTRIBUTORS) or who is listed as an author in one of the source files of this Isabelle distribution. Contributions to this Isabelle version -------------------------------------- * November 2020: Florian Haftmann Bundle mixins for locale and class expressions. +* November 2020: Jakub Kądziołka + Stronger lemmas about orders of group elements (generate_pow_card) + * October 2020: Jasmin Blanchette, Martin Desharnais, Mathias Fleury Use veriT in proof preplay in Sledgehammer. * October 2020: Mathias Fleury Updated proof reconstruction for the SMT solver veriT in the smt method. * October 2020: Jasmin Blanchette, Martin Desharnais Integration of E 2.5 for Sledgehammer. * September 2020: Florian Haftmann Substantial reworking and modularization of Word library, with generic type conversions. * August 2020: Makarius Wenzel Improved monitoring of runtime statistics: ML GC progress and Java. * July 2020: Martin Desharnais Integration of Metis 2.4. * June 2020: Makarius Wenzel Batch-builds via "isabelle build" allow to invoke Scala from ML. * June 2020: Florian Haftmann Simproc defined_all for more aggressive substitution with variables from assumptions. * May 2020: Makarius Wenzel Antiquotations for Isabelle systems programming, notably @{scala_function} and @{scala} to invoke Scala from ML. * May 2020: Florian Haftmann Generic algebraically founded bit operations NOT, AND, OR, XOR. Contributions to Isabelle2020 ----------------------------- * February 2020: E. Gunther, M. Pagano and P. Sánchez Terraf Simplified, generalised version of ZF/Constructible. * January 2020: LC Paulson The full finite Ramsey's theorem and elements of finite and infinite Ramsey theory. * December 2019: Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel Extension of lift_bnf to support quotient types. * November 2019: Peter Zeller, TU Kaiserslautern Update of Isabelle/VSCode to WebviewPanel API. * October..December 2019: Makarius Wenzel Isabelle/Phabrictor server setup, including Linux platform support in Isabelle/Scala. Client-side tool "isabelle hg_setup". * October 2019: Maximilian Schäffeler Port of the HOL Light decision procedure for metric spaces. * October 2019: Makarius Wenzel More scalable Isabelle dump and underlying headless PIDE session. * August 2019: Makarius Wenzel Better support for proof terms in Isabelle/Pure, notably via method combinator SUBPROOFS (ML) and "subproofs" (Isar). * July 2019: Alexander Krauss, Makarius Wenzel Minimal support for a soft-type system within the Isabelle logical framework. Contributions to Isabelle2019 ----------------------------- * April 2019: LC Paulson Homology and supporting lemmas on topology and group theory * April 2019: Paulo de Vilhena and Martin Baillon Group theory developments, esp. algebraic closure of a field * February/March 2019: Makarius Wenzel Stateless management of export artifacts in the Isabelle/HOL code generator. * February 2019: Manuel Eberl Exponentiation by squaring, used to implement "power" in monoid_mult and fast modular exponentiation. * February 2019: Manuel Eberl Carmichael's function, primitive roots in residue rings, more properties of the order in residue rings. * February 2019: Jeremy Sylvestre Formal Laurent Series and overhaul of Formal power series. * January 2019: Florian Haftmann Clarified syntax and congruence rules for big operators on sets involving the image operator. * January 2019: Florian Haftmann Renovation of code generation, particularly export into session data and proper strings and proper integers based on zarith for OCaml. * January 2019: Andreas Lochbihler New implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm. * November/December 2018: Makarius Wenzel Support for Isabelle/Haskell applications of Isabelle/PIDE. * August/September 2018: Makarius Wenzel Improvements of headless Isabelle/PIDE session and server, and systematic exports from theory documents. * December 2018: Florian Haftmann Generic executable sorting algorithms based on executable comparators. * October 2018: Mathias Fleury Proof reconstruction for the SMT solver veriT in the smt method. Contributions to Isabelle2018 ----------------------------- * July 2018: Manuel Eberl "real_asymp" proof method for automatic proofs of real limits, "Big-O" statements, etc. * June 2018: Fabian Immler More tool support for HOL-Types_To_Sets. * June 2018: Martin Baillon and Paulo Emílio de Vilhena A variety of contributions to HOL-Algebra. * June 2018: Wenda Li New/strengthened results involving analysis, topology, etc. * May/June 2018: Makarius Wenzel System infrastructure to export blobs as theory presentation, and to dump PIDE database content in batch mode. * May 2018: Manuel Eberl Landau symbols and asymptotic equivalence (moved from the AFP). * May 2018: Jose Divasón (Universidad de la Rioja), Jesús Aransay (Universidad de la Rioja), Johannes Hölzl (VU Amsterdam), Fabian Immler (TUM) Generalizations in the formalization of linear algebra. * May 2018: Florian Haftmann Consolidation of string-like types in HOL. * May 2018: Andreas Lochbihler (Digital Asset), Pascal Stoop (ETH Zurich) Code generation with lazy evaluation semantics. * March 2018: Florian Haftmann Abstract bit operations push_bit, take_bit, drop_bit, alongside with an algebraic foundation for bit strings and word types in HOL-ex. * March 2018: Viorel Preoteasa Generalisation of complete_distrib_lattice * February 2018: Wenda Li A unified definition for the order of zeros and poles. Improved reasoning around non-essential singularities. * January 2018: Sebastien Gouezel Various small additions to HOL-Analysis * December 2017: Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel A new conditional parametricity prover. * October 2017: Alexander Maletzky Derivation of axiom "iff" in theory HOL.HOL from the other axioms. Contributions to Isabelle2017 ----------------------------- * September 2017: Lawrence Paulson HOL-Analysis, e.g. simplicial complexes, Jordan Curve Theorem. * September 2017: Jasmin Blanchette Further integration of Nunchaku model finder. * November 2016 - June 2017: Makarius Wenzel New Isabelle/VSCode, with underlying restructuring of Isabelle/PIDE. * 2017: Makarius Wenzel Session-qualified theory names (theory imports and ROOT files). Prover IDE improvements. Support for SQL databases in Isabelle/Scala: SQLite and PostgreSQL. * August 2017: Andreas Lochbihler, ETH Zurich type of unordered pairs (HOL-Library.Uprod) * August 2017: Manuel Eberl, TUM HOL-Analysis: infinite products over natural numbers, infinite sums over arbitrary sets, connection between formal power series and analytic complex functions * March 2017: Alasdair Armstrong, University of Sheffield and Simon Foster, University of York Fixed-point theory and Galois Connections in HOL-Algebra. * February 2017: Florian Haftmann, TUM Statically embedded computations implemented by generated code. Contributions to Isabelle2016-1 ------------------------------- * December 2016: Ondřej Kunčar, TUM Types_To_Sets: experimental extension of Higher-Order Logic to allow translation of types to sets. * October 2016: Jasmin Blanchette Integration of Nunchaku model finder. * October 2016: Jaime Mendizabal Roche, TUM Ported remaining theories of session Old_Number_Theory to the new Number_Theory and removed Old_Number_Theory. * September 2016: Sascha Boehme Proof method "argo" based on SMT technology for a combination of quantifier-free propositional logic, equality and linear real arithmetic * July 2016: Daniel Stuewe Height-size proofs in HOL-Data_Structures. * July 2016: Manuel Eberl, TUM Algebraic foundation for primes; generalization from nat to general factorial rings. * June 2016: Andreas Lochbihler, ETH Zurich Formalisation of discrete subprobability distributions. * June 2016: Florian Haftmann, TUM Improvements to code generation: optional timing measurements, more succint closures for static evaluation, less ambiguities concering Scala implicits. * May 2016: Manuel Eberl, TUM Code generation for Probability Mass Functions. * March 2016: Florian Haftmann, TUM Abstract factorial rings with unique factorization. * March 2016: Florian Haftmann, TUM Reworking of the HOL char type as special case of a finite numeral type. * March 2016: Andreas Lochbihler, ETH Zurich Reasoning support for monotonicity, continuity and admissibility in chain-complete partial orders. * February - October 2016: Makarius Wenzel Prover IDE improvements. ML IDE improvements: bootstrap of Pure. Isar language consolidation. Notational modernization of HOL. Tight Poly/ML integration. More Isabelle/Scala system programming modules (e.g. SSH, Mercurial). * Winter 2016: Jasmin Blanchette, Inria & LORIA & MPII, Aymeric Bouzy, Ecole polytechnique, Andreas Lochbihler, ETH Zurich, Andrei Popescu, Middlesex University, and Dmitriy Traytel, ETH Zurich 'corec' command and friends. * January 2016: Florian Haftmann, TUM Abolition of compound operators INFIMUM and SUPREMUM for complete lattices. Contributions to Isabelle2016 ----------------------------- * Winter 2016: Manuel Eberl, TUM Support for real exponentiation ("powr") in the "approximation" method. (This was removed in Isabelle 2015 due to a changed definition of "powr".) * Summer 2015 - Winter 2016: Lawrence C Paulson, Cambridge General, homology form of Cauchy's integral theorem and supporting material (ported from HOL Light). * Winter 2015/16: Gerwin Klein, NICTA New print_record command. * May - December 2015: Makarius Wenzel Prover IDE improvements. More Isar language elements. Document language refinements. Poly/ML debugger integration. Improved multi-platform and multi-architecture support. * Winter 2015: Manuel Eberl, TUM The radius of convergence of power series and various summability tests. Harmonic numbers and the Euler-Mascheroni constant. The Generalised Binomial Theorem. The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and their most important properties. * Autumn 2015: Manuel Eberl, TUM Proper definition of division (with remainder) for formal power series; Euclidean Ring and GCD instance for formal power series. * Autumn 2015: Florian Haftmann, TUM Rewrite definitions for global interpretations and sublocale declarations. * Autumn 2015: Andreas Lochbihler Bourbaki-Witt fixpoint theorem for increasing functions on chain-complete partial orders. * Autumn 2015: Chaitanya Mangla, Lawrence C Paulson, and Manuel Eberl A large number of additional binomial identities. * Summer 2015: Daniel Matichuk, NICTA and Makarius Wenzel Isar subgoal command for proof structure within unstructured proof scripts. * Summer 2015: Florian Haftmann, TUM Generic partial division in rings as inverse operation of multiplication. * Summer 2015: Manuel Eberl and Florian Haftmann, TUM Type class hierarchy with common algebraic notions of integral (semi)domains like units, associated elements and normalization wrt. units. * Summer 2015: Florian Haftmann, TUM Fundamentals of abstract type class for factorial rings. * Summer 2015: Julian Biendarra, TUM and Dmitriy Traytel, ETH Zurich Command to lift a BNF structure on the raw type to the abstract type for typedefs. * Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM Proof of the central limit theorem: includes weak convergence, characteristic functions, and Levy's uniqueness and continuity theorem. Contributions to Isabelle2015 ----------------------------- * 2014/2015: Daniel Matichuk, Toby Murray, NICTA and Makarius Wenzel The Eisbach proof method language and "match" method. * Winter 2014 and Spring 2015: Ondrej Kuncar, TUM Extension of lift_definition to execute lifted functions that have as a return type a datatype containing a subtype. * March 2015: Jasmin Blanchette, Inria & LORIA & MPII, Mathias Fleury, MPII, and Dmitriy Traytel, TUM More multiset theorems, syntax, and operations. * December 2014: Johannes Hölzl, Manuel Eberl, Sudeep Kanav, TUM, and Jeremy Avigad, Luke Serafin, CMU Various integration theorems: mostly integration on intervals and substitution. * September 2014: Florian Haftmann, TUM Lexicographic order on functions and sum/product over function bodies. * August 2014: Andreas Lochbihler, ETH Zurich Test infrastructure for executing generated code in target languages. * August 2014: Manuel Eberl, TUM Generic euclidean algorithms for GCD et al. Contributions to Isabelle2014 ----------------------------- * July 2014: Thomas Sewell, NICTA Preserve equality hypotheses in "clarify" and friends. New "hypsubst_thin" method configuration option. * Summer 2014: Florian Haftmann, TUM Consolidation and generalization of facts concerning (abelian) semigroups and monoids, particularly products (resp. sums) on finite sets. * Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM Work on exotic automatic theorem provers for Sledgehammer (LEO-II, veriT, Waldmeister, etc.). * June 2014: Florian Haftmann, TUM Internal reorganisation of the local theory / named target stack. * June 2014: Sudeep Kanav, TUM, Jeremy Avigad, CMU, and Johannes Hölzl, TUM Various properties of exponentially, Erlang, and normal distributed random variables. * May 2014: Cezary Kaliszyk, University of Innsbruck, and Jasmin Blanchette, TUM SML-based engines for MaSh. * March 2014: René Thiemann Improved code generation for multisets. * February 2014: Florian Haftmann, TUM Permanent interpretation inside theory, locale and class targets with mixin definitions. * Spring 2014: Lawrence C Paulson, Cambridge Theory Complex_Basic_Analysis. Tidying up Number_Theory vs Old_Number_Theory * Winter 2013 and Spring 2014: Ondrej Kuncar, TUM Various improvements to Lifting/Transfer, integration with the BNF package. * Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE. * Fall 2013 and Winter 2014: Martin Desharnais, Lorenz Panny, Dmitriy Traytel, and Jasmin Blanchette, TUM Various improvements to the BNF-based (co)datatype package, including a more polished "primcorec" command, optimizations, and integration in the "HOL" session. * Winter/Spring 2014: Sascha Boehme, QAware GmbH, and Jasmin Blanchette, TUM "SMT2" module and "smt2" proof method, based on SMT-LIB 2 and Z3 4.3. * January 2014: Lars Hupel, TUM An improved, interactive simplifier trace with integration into the Isabelle/jEdit Prover IDE. * December 2013: Florian Haftmann, TUM Consolidation of abstract interpretations concerning min and max. * November 2013: Florian Haftmann, TUM Abolition of negative numeral literals in the logic. Contributions to Isabelle2013-1 ------------------------------- * September 2013: Lars Noschinski, TUM Conversion between function definitions as list of equations and case expressions in HOL. New library Simps_Case_Conv with commands case_of_simps, simps_of_case. * September 2013: Nik Sultana, University of Cambridge Improvements to HOL/TPTP parser and import facilities. * September 2013: Johannes Hölzl and Dmitriy Traytel, TUM New "coinduction" method (residing in HOL-BNF) to avoid boilerplate. * Summer 2013: Makarius Wenzel, Université Paris-Sud / LRI Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE. * Summer 2013: Manuel Eberl, TUM Generation of elimination rules in the function package. New command "fun_cases". * Summer 2013: Christian Sternagel, JAIST Improved support for ad hoc overloading of constants, including documentation and examples. * Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and Jasmin Blanchette, TUM Various improvements to the BNF-based (co)datatype package, including "primrec_new" and "primcorec" commands and a compatibility layer. * Spring and Summer 2013: Ondrej Kuncar, TUM Various improvements of Lifting and Transfer packages. * Spring 2013: Brian Huffman, Galois Inc. Improvements of the Transfer package. * Summer 2013: Daniel Kühlwein, ICIS, Radboud University Nijmegen Jasmin Blanchette, TUM Various improvements to MaSh, including a server mode. * First half of 2013: Steffen Smolka, TUM Further improvements to Sledgehammer's Isar proof generator. * May 2013: Florian Haftmann, TUM Ephemeral interpretation in local theories. * May 2013: Lukas Bulwahn and Nicolai Schaffroth, TUM Spec_Check: A Quickcheck tool for Isabelle/ML. * April 2013: Stefan Berghofer, secunet Security Networks AG Dmitriy Traytel, TUM Makarius Wenzel, Université Paris-Sud / LRI Case translations as a separate check phase independent of the datatype package. * March 2013: Florian Haftmann, TUM Reform of "big operators" on sets. * March 2013: Florian Haftmann, TUM Algebraic locale hierarchy for orderings and (semi)lattices. * February 2013: Florian Haftmann, TUM Reworking and consolidation of code generation for target language numerals. * February 2013: Florian Haftmann, TUM Sieve of Eratosthenes. Contributions to Isabelle2013 ----------------------------- * 2012: Makarius Wenzel, Université Paris-Sud / LRI Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE. * Fall 2012: Daniel Kühlwein, ICIS, Radboud University Nijmegen Jasmin Blanchette, TUM Implemented Machine Learning for Sledgehammer (MaSh). * Fall 2012: Steffen Smolka, TUM Various improvements to Sledgehammer's Isar proof generator, including a smart type annotation algorithm and proof shrinking. * December 2012: Alessandro Coglio, Kestrel Contributions to HOL's Lattice library. * November 2012: Fabian Immler, TUM "Symbols" dockable for Isabelle/jEdit. * November 2012: Fabian Immler, TUM Proof of the Daniell-Kolmogorov theorem: the existence of the limit of projective families. * October 2012: Andreas Lochbihler, KIT Efficient construction of red-black trees from sorted associative lists. * September 2012: Florian Haftmann, TUM Lattice instances for type option. * September 2012: Christian Sternagel, JAIST Consolidated HOL/Library (theories: Prefix_Order, Sublist, and Sublist_Order) w.r.t. prefixes, suffixes, and embedding on lists. * August 2012: Dmitriy Traytel, Andrei Popescu, Jasmin Blanchette, TUM New BNF-based (co)datatype package. * August 2012: Andrei Popescu and Dmitriy Traytel, TUM Theories of ordinals and cardinals. * July 2012: Makarius Wenzel, Université Paris-Sud / LRI Advanced support for Isabelle sessions and build management, notably "isabelle build". * June 2012: Felix Kuperjans, Lukas Bulwahn, TUM and Rafal Kolanski, NICTA Simproc for rewriting set comprehensions into pointfree expressions. * May 2012: Andreas Lochbihler, KIT Theory of almost everywhere constant functions. * 2010-2012: Markus Kaiser and Lukas Bulwahn, TUM Graphview in Scala/Swing. Contributions to Isabelle2012 ----------------------------- * April 2012: Johannes Hölzl, TUM Probability: Introduced type to represent measures instead of locales. * April 2012: Johannes Hölzl, Fabian Immler, TUM Float: Moved to Dyadic rationals to represent floating point numers. * April 2012: Thomas Sewell, NICTA and 2010: Sascha Boehme, TUM Theory HOL/Word/WordBitwise: logic/circuit expansion of bitvector equalities/inequalities. * March 2012: Christian Sternagel, JAIST Consolidated theory of relation composition. * March 2012: Nik Sultana, University of Cambridge HOL/TPTP parser and import facilities. * March 2012: Cezary Kaliszyk, University of Innsbruck and Alexander Krauss, QAware GmbH Faster and more scalable Import mechanism for HOL Light proofs. * January 2012: Florian Haftmann, TUM, et al. (Re-)Introduction of the "set" type constructor. * 2012: Ondrej Kuncar, TUM New package Lifting, various improvements and refinements to the Quotient package. * 2011/2012: Jasmin Blanchette, TUM Various improvements to Sledgehammer, notably: tighter integration with SPASS, support for more provers (Alt-Ergo, iProver, iProver-Eq). * 2011/2012: Makarius Wenzel, Université Paris-Sud / LRI Various refinements of local theory infrastructure. Improvements of Isabelle/Scala layer and Isabelle/jEdit Prover IDE. Contributions to Isabelle2011-1 ------------------------------- * September 2011: Peter Gammie Theory HOL/Library/Saturated: numbers with saturated arithmetic. * August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM Refined theory on complete lattices. * August 2011: Brian Huffman, Portland State University Miscellaneous cleanup of Complex_Main and Multivariate_Analysis. * June 2011: Brian Huffman, Portland State University Proof method "countable_datatype" for theory Library/Countable. * 2011: Jasmin Blanchette, TUM Various improvements to Sledgehammer, notably: use of sound translations, support for more provers (Waldmeister, LEO-II, Satallax). Further development of Nitpick and 'try' command. * 2011: Andreas Lochbihler, Karlsruhe Institute of Technology Theory HOL/Library/Cset_Monad allows do notation for computable sets (cset) via the generic monad ad-hoc overloading facility. * 2011: Johannes Hölzl, Armin Heller, TUM and Bogdan Grechuk, University of Edinburgh Theory HOL/Library/Extended_Reals: real numbers extended with plus and minus infinity. * 2011: Makarius Wenzel, Université Paris-Sud / LRI Various building blocks for Isabelle/Scala layer and Isabelle/jEdit Prover IDE. Contributions to Isabelle2011 ----------------------------- * January 2011: Stefan Berghofer, secunet Security Networks AG HOL-SPARK: an interactive prover back-end for SPARK. * October 2010: Bogdan Grechuk, University of Edinburgh Extended convex analysis in Multivariate Analysis. * October 2010: Dmitriy Traytel, TUM Coercive subtyping via subtype constraints. * October 2010: Alexander Krauss, TUM Command partial_function for function definitions based on complete partial orders in HOL. * September 2010: Florian Haftmann, TUM Refined concepts for evaluation, i.e., normalization of terms using different techniques. * September 2010: Florian Haftmann, TUM Code generation for Scala. * August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM Improved Probability theory in HOL. * July 2010: Florian Haftmann, TUM Reworking and extension of the Imperative HOL framework. * July 2010: Alexander Krauss, TUM and Christian Sternagel, University of Innsbruck Ad-hoc overloading. Generic do notation for monads. Contributions to Isabelle2009-2 ------------------------------- * 2009/2010: Stefan Berghofer, Alexander Krauss, and Andreas Schropp, TUM, Makarius Wenzel, TUM / LRI Elimination of type classes from proof terms. * April 2010: Florian Haftmann, TUM Reorganization of abstract algebra type classes. * April 2010: Florian Haftmann, TUM Code generation for data representations involving invariants; various collections avaiable in theories Fset, Dlist, RBT, Mapping and AssocList. * March 2010: Sascha Boehme, TUM Efficient SHA1 library for Poly/ML. * February 2010: Cezary Kaliszyk and Christian Urban, TUM Quotient type package for Isabelle/HOL. Contributions to Isabelle2009-1 ------------------------------- * November 2009, Brian Huffman, PSU New definitional domain package for HOLCF. * November 2009: Robert Himmelmann, TUM Derivation and Brouwer's fixpoint theorem in Multivariate Analysis. * November 2009: Stefan Berghofer and Lukas Bulwahn, TUM A tabled implementation of the reflexive transitive closure. * November 2009: Lukas Bulwahn, TUM Predicate Compiler: a compiler for inductive predicates to equational specifications. * November 2009: Sascha Boehme, TUM and Burkhart Wolff, LRI Paris HOL-Boogie: an interactive prover back-end for Boogie and VCC. * October 2009: Jasmin Blanchette, TUM Nitpick: yet another counterexample generator for Isabelle/HOL. * October 2009: Sascha Boehme, TUM Extension of SMT method: proof-reconstruction for the SMT solver Z3. * October 2009: Florian Haftmann, TUM Refinement of parts of the HOL datatype package. * October 2009: Florian Haftmann, TUM Generic term styles for term antiquotations. * September 2009: Thomas Sewell, NICTA More efficient HOL/record implementation. * September 2009: Sascha Boehme, TUM SMT method using external SMT solvers. * September 2009: Florian Haftmann, TUM Refinement of sets and lattices. * July 2009: Jeremy Avigad and Amine Chaieb New number theory. * July 2009: Philipp Meyer, TUM HOL/Library/Sum_Of_Squares: functionality to call a remote csdp prover. * July 2009: Florian Haftmann, TUM New quickcheck implementation using new code generator. * July 2009: Florian Haftmann, TUM HOL/Library/Fset: an explicit type of sets; finite sets ready to use for code generation. * June 2009: Florian Haftmann, TUM HOL/Library/Tree: search trees implementing mappings, ready to use for code generation. * March 2009: Philipp Meyer, TUM Minimization tool for results from Sledgehammer. Contributions to Isabelle2009 ----------------------------- * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of Cambridge Elementary topology in Euclidean space. * March 2009: Johannes Hoelzl, TUM Method "approximation", which proves real valued inequalities by computation. * February 2009: Filip Maric, Univ. of Belgrade A Serbian theory. * February 2009: Jasmin Christian Blanchette, TUM Misc cleanup of HOL/refute. * February 2009: Timothy Bourke, NICTA New find_consts command. * February 2009: Timothy Bourke, NICTA "solves" criterion for find_theorems and auto_solve option * December 2008: Clemens Ballarin, TUM New locale implementation. * December 2008: Armin Heller, TUM and Alexander Krauss, TUM Method "sizechange" for advanced termination proofs. * November 2008: Timothy Bourke, NICTA Performance improvement (factor 50) for find_theorems. * 2008: Florian Haftmann, TUM Various extensions and restructurings in HOL, improvements in evaluation mechanisms, new module binding.ML for name bindings. * October 2008: Fabian Immler, TUM ATP manager for Sledgehammer, based on ML threads instead of Posix processes. Additional ATP wrappers, including remote SystemOnTPTP services. * September 2008: Stefan Berghofer, TUM and Marc Bezem, Univ. Bergen Prover for coherent logic. * August 2008: Fabian Immler, TUM Vampire wrapper script for remote SystemOnTPTP service. Contributions to Isabelle2008 ----------------------------- * 2007/2008: Alexander Krauss, TUM and Florian Haftmann, TUM and Stefan Berghofer, TUM HOL library improvements. * 2007/2008: Brian Huffman, PSU HOLCF library improvements. * 2007/2008: Stefan Berghofer, TUM HOL-Nominal package improvements. * March 2008: Markus Reiter, TUM HOL/Library/RBT: red-black trees. * February 2008: Alexander Krauss, TUM and Florian Haftmann, TUM and Lukas Bulwahn, TUM and John Matthews, Galois: HOL/Library/Imperative_HOL: Haskell-style imperative data structures for HOL. * December 2007: Norbert Schirmer, Uni Saarbruecken Misc improvements of record package in HOL. * December 2007: Florian Haftmann, TUM Overloading and class instantiation target. * December 2007: Florian Haftmann, TUM New version of primrec package for local theories. * December 2007: Alexander Krauss, TUM Method "induction_scheme" in HOL. * November 2007: Peter Lammich, Uni Muenster HOL-Lattice: some more lemmas. Contributions to Isabelle2007 ----------------------------- * October 2007: Norbert Schirmer, TUM / Uni Saarbruecken State Spaces: The Locale Way (in HOL). * October 2007: Mark A. Hillebrand, DFKI Robust sub/superscripts in LaTeX document output. * August 2007: Jeremy Dawson, NICTA and Paul Graunke, Galois and Brian Huffman, PSU and Gerwin Klein, NICTA and John Matthews, Galois HOL-Word: a library for fixed-size machine words in Isabelle. * August 2007: Brian Huffman, PSU HOL/Library/Boolean_Algebra and HOL/Library/Numeral_Type. * June 2007: Amine Chaieb, TUM Semiring normalization and Groebner Bases. Support for dense linear orders. * June 2007: Joe Hurd, Oxford Metis theorem-prover. * 2007: Kong W. Susanto, Cambridge HOL: Metis prover integration. * 2007: Stefan Berghofer, TUM HOL: inductive predicates and sets. * 2007: Norbert Schirmer, TUM HOL/record: misc improvements. * 2006/2007: Alexander Krauss, TUM HOL: function package and related theories on termination. * 2006/2007: Florian Haftmann, TUM Pure: generic code generator framework. Pure: class package. HOL: theory reorganization, code generator setup. * 2006/2007: Christian Urban, TUM and Stefan Berghofer, TUM and Julien Narboux, TUM HOL/Nominal package and related tools. * November 2006: Lukas Bulwahn, TUM HOL: method "lexicographic_order" for function package. * October 2006: Stefan Hohe, TUM HOL-Algebra: ideals and quotients over rings. * August 2006: Amine Chaieb, TUM Experimental support for generic reflection and reification in HOL. * July 2006: Rafal Kolanski, NICTA Hex (0xFF) and binary (0b1011) numerals. * May 2006: Klaus Aehlig, LMU Command 'normal_form': normalization by evaluation. * May 2006: Amine Chaieb, TUM HOL-Complex: Ferrante and Rackoff Algorithm for linear real arithmetic. * February 2006: Benjamin Porter, NICTA HOL and HOL-Complex: generalised mean value theorem, continuum is not denumerable, harmonic and arithmetic series, and denumerability of rationals. * October 2005: Martin Wildmoser, TUM Sketch for Isar 'guess' element. Contributions to Isabelle2005 ----------------------------- * September 2005: Lukas Bulwahn and Bernhard Haeupler, TUM HOL-Complex: Formalization of Taylor series. * September 2005: Stephan Merz, Alwen Tiu, QSL Loria Components for SAT solver method using zChaff. * September 2005: Ning Zhang and Christian Urban, LMU Munich A Chinese theory. * September 2005: Bernhard Haeupler, TUM Method comm_ring for proving equalities in commutative rings. * July/August 2005: Jeremy Avigad, Carnegie Mellon University Various improvements of the HOL and HOL-Complex library. * July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM Some structured proofs about completeness of real numbers. * May 2005: Rafal Kolanski and Gerwin Klein, NICTA Improved retrieval of facts from theory/proof context. * February 2005: Lucas Dixon, University of Edinburgh Improved subst method. * 2005: Brian Huffman, OGI Various improvements of HOLCF. Some improvements of the HOL-Complex library. * 2005: Claire Quigley and Jia Meng, University of Cambridge Some support for asynchronous communication with external provers (experimental). * 2005: Florian Haftmann, TUM Contributions to document 'sugar'. Various ML combinators, notably linear functional transformations. Some cleanup of ML legacy. Additional antiquotations. Improved Isabelle web site. * 2004/2005: David Aspinall, University of Edinburgh Various elements of XML and PGIP based communication with user interfaces (experimental). * 2004/2005: Gerwin Klein, NICTA Contributions to document 'sugar'. Improved Isabelle web site. Improved HTML presentation of theories. * 2004/2005: Clemens Ballarin, TUM Provers: tools for transitive relations and quasi orders. Improved version of locales, notably interpretation of locales. Improved version of HOL-Algebra. * 2004/2005: Amine Chaieb, TUM Improved version of HOL presburger method. * 2004/2005: Steven Obua, TUM Improved version of HOL/Import, support for HOL-Light. Improved version of HOL-Complex-Matrix. Pure/defs: more sophisticated checks on well-formedness of overloading. Pure/Tools: an experimental evaluator for lambda terms. * 2004/2005: Norbert Schirmer, TUM Contributions to document 'sugar'. Improved version of HOL/record. * 2004/2005: Sebastian Skalberg, TUM Improved version of HOL/Import. Some internal ML reorganizations. * 2004/2005: Tjark Weber, TUM SAT solver method using zChaff. Improved version of HOL/refute. :maxLineLen=78: diff --git a/src/HOL/Algebra/Elementary_Groups.thy b/src/HOL/Algebra/Elementary_Groups.thy --- a/src/HOL/Algebra/Elementary_Groups.thy +++ b/src/HOL/Algebra/Elementary_Groups.thy @@ -1,667 +1,590 @@ section \Elementary Group Constructions\ (* Title: HOL/Algebra/Elementary_Groups.thy Author: LC Paulson, ported from HOL Light *) theory Elementary_Groups -imports Generated_Groups Multiplicative_Group "HOL-Library.Infinite_Set" +imports Generated_Groups "HOL-Library.Infinite_Set" begin subsection\Direct sum/product lemmas\ locale group_disjoint_sum = group G + AG: subgroup A G + BG: subgroup B G for G (structure) and A B begin lemma subset_one: "A \ B \ {\} \ A \ B = {\}" by auto lemma sub_id_iff: "A \ B \ {\} \ (\x\A. \y\B. x \ y = \ \ x = \ \ y = \)" (is "?lhs = ?rhs") proof - have "?lhs = (\x\A. \y\B. x \ inv y = \ \ x = \ \ inv y = \)" proof (intro ballI iffI impI) fix x y assume "A \ B \ {\}" "x \ A" "y \ B" "x \ inv y = \" then have "y = x" using group.inv_equality group_l_invI by fastforce then show "x = \ \ inv y = \" using \A \ B \ {\}\ \x \ A\ \y \ B\ by fastforce next assume "\x\A. \y\B. x \ inv y = \ \ x = \ \ inv y = \" then show "A \ B \ {\}" by auto qed also have "\ = ?rhs" by (metis BG.mem_carrier BG.subgroup_axioms inv_inv subgroup_def) finally show ?thesis . qed lemma cancel: "A \ B \ {\} \ (\x\A. \y\B. \x'\A. \y'\B. x \ y = x' \ y' \ x = x' \ y = y')" (is "?lhs = ?rhs") proof - have "(\x\A. \y\B. x \ y = \ \ x = \ \ y = \) = ?rhs" (is "?med = _") proof (intro ballI iffI impI) fix x y x' y' assume * [rule_format]: "\x\A. \y\B. x \ y = \ \ x = \ \ y = \" and AB: "x \ A" "y \ B" "x' \ A" "y' \ B" and eq: "x \ y = x' \ y'" then have carr: "x \ carrier G" "x' \ carrier G" "y \ carrier G" "y' \ carrier G" using AG.subset BG.subset by auto then have "inv x' \ x \ (y \ inv y') = inv x' \ (x \ y) \ inv y'" by (simp add: m_assoc) also have "\ = \" using carr by (simp add: eq) (simp add: m_assoc) finally have 1: "inv x' \ x \ (y \ inv y') = \" . show "x = x' \ y = y'" using * [OF _ _ 1] AB by simp (metis carr inv_closed inv_inv local.inv_equality) next fix x y assume * [rule_format]: "\x\A. \y\B. \x'\A. \y'\B. x \ y = x' \ y' \ x = x' \ y = y'" and xy: "x \ A" "y \ B" "x \ y = \" show "x = \ \ y = \" by (rule *) (use xy in auto) qed then show ?thesis by (simp add: sub_id_iff) qed lemma commuting_imp_normal1: assumes sub: "carrier G \ A <#> B" and mult: "\x y. \x \ A; y \ B\ \ x \ y = y \ x" shows "A \ G" proof - have AB: "A \ carrier G \ B \ carrier G" by (simp add: AG.subset BG.subset) have "A #> x = x <# A" if x: "x \ carrier G" for x proof - obtain a b where xeq: "x = a \ b" and "a \ A" "b \ B" and carr: "a \ carrier G" "b \ carrier G" using x sub AB by (force simp: set_mult_def) have Ab: "A <#> {b} = {b} <#> A" using AB \a \ A\ \b \ B\ mult by (force simp: set_mult_def m_assoc subset_iff) have "A #> x = A <#> {a \ b}" by (auto simp: l_coset_eq_set_mult r_coset_eq_set_mult xeq) also have "\ = A <#> {a} <#> {b}" using AB \a \ A\ \b \ B\ by (auto simp: set_mult_def m_assoc subset_iff) also have "\ = {a} <#> A <#> {b}" by (metis AG.rcos_const AG.subgroup_axioms \a \ A\ coset_join3 is_group l_coset_eq_set_mult r_coset_eq_set_mult subgroup.mem_carrier) also have "\ = {a} <#> {b} <#> A" by (simp add: is_group carr group.set_mult_assoc AB Ab) also have "\ = {x} <#> A" by (auto simp: set_mult_def xeq) finally show "A #> x = x <# A" by (simp add: l_coset_eq_set_mult) qed then show ?thesis by (auto simp: normal_def normal_axioms_def AG.subgroup_axioms is_group) qed lemma commuting_imp_normal2: assumes"carrier G \ A <#> B" "\x y. \x \ A; y \ B\ \ x \ y = y \ x" shows "B \ G" proof (rule group_disjoint_sum.commuting_imp_normal1) show "group_disjoint_sum G B A" proof qed next show "carrier G \ B <#> A" using BG.subgroup_axioms assms commut_normal commuting_imp_normal1 by blast qed (use assms in auto) lemma (in group) normal_imp_commuting: assumes "A \ G" "B \ G" "A \ B \ {\}" "x \ A" "y \ B" shows "x \ y = y \ x" proof - interpret AG: normal A G using assms by auto interpret BG: normal B G using assms by auto interpret group_disjoint_sum G A B proof qed have * [rule_format]: "(\x\A. \y\B. \x'\A. \y'\B. x \ y = x' \ y' \ x = x' \ y = y')" using cancel assms by (auto simp: normal_def) have carr: "x \ carrier G" "y \ carrier G" using assms AG.subset BG.subset by auto then show ?thesis using * [of x _ _ y] AG.coset_eq [rule_format, of y] BG.coset_eq [rule_format, of x] by (clarsimp simp: l_coset_def r_coset_def set_eq_iff) (metis \x \ A\ \y \ B\) qed lemma normal_eq_commuting: assumes "carrier G \ A <#> B" "A \ B \ {\}" shows "A \ G \ B \ G \ (\x\A. \y\B. x \ y = y \ x)" by (metis assms commuting_imp_normal1 commuting_imp_normal2 normal_imp_commuting) lemma (in group) hom_group_mul_rev: assumes "(\(x,y). x \ y) \ hom (subgroup_generated G A \\ subgroup_generated G B) G" (is "?h \ hom ?P G") and "x \ carrier G" "y \ carrier G" "x \ A" "y \ B" shows "x \ y = y \ x" proof - interpret P: group_hom ?P G ?h by (simp add: assms DirProd_group group_hom.intro group_hom_axioms.intro is_group) have xy: "(x,y) \ carrier ?P" by (auto simp: assms carrier_subgroup_generated generate.incl) have "x \ (x \ (y \ y)) = x \ (y \ (x \ y))" using P.hom_mult [OF xy xy] by (simp add: m_assoc assms) then have "x \ (y \ y) = y \ (x \ y)" using assms by simp then show ?thesis by (simp add: assms flip: m_assoc) qed lemma hom_group_mul_eq: "(\(x,y). x \ y) \ hom (subgroup_generated G A \\ subgroup_generated G B) G \ (\x\A. \y\B. x \ y = y \ x)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs using hom_group_mul_rev AG.subset BG.subset by blast next assume R: ?rhs have subG: "generate G (carrier G \ A) \ carrier G" for A by (simp add: generate_incl) have *: "x \ u \ (y \ v) = x \ y \ (u \ v)" if eq [rule_format]: "\x\A. \y\B. x \ y = y \ x" and gen: "x \ generate G (carrier G \ A)" "y \ generate G (carrier G \ B)" "u \ generate G (carrier G \ A)" "v \ generate G (carrier G \ B)" for x y u v proof - have "u \ y = y \ u" by (metis AG.carrier_subgroup_generated_subgroup BG.carrier_subgroup_generated_subgroup carrier_subgroup_generated eq that(3) that(4)) then have "x \ u \ y = x \ y \ u" using gen by (simp add: m_assoc subsetD [OF subG]) then show ?thesis using gen by (simp add: subsetD [OF subG] flip: m_assoc) qed show ?lhs using R by (auto simp: hom_def carrier_subgroup_generated subsetD [OF subG] *) qed lemma epi_group_mul_eq: "(\(x,y). x \ y) \ epi (subgroup_generated G A \\ subgroup_generated G B) G \ A <#> B = carrier G \ (\x\A. \y\B. x \ y = y \ x)" proof - have subGA: "generate G (carrier G \ A) \ A" by (simp add: AG.subgroup_axioms generate_subgroup_incl) have subGB: "generate G (carrier G \ B) \ B" by (simp add: BG.subgroup_axioms generate_subgroup_incl) have "(((\(x, y). x \ y) ` (generate G (carrier G \ A) \ generate G (carrier G \ B)))) = ((A <#> B))" by (auto simp: set_mult_def generate.incl pair_imageI dest: subsetD [OF subGA] subsetD [OF subGB]) then show ?thesis by (auto simp: epi_def hom_group_mul_eq carrier_subgroup_generated) qed lemma mon_group_mul_eq: "(\(x,y). x \ y) \ mon (subgroup_generated G A \\ subgroup_generated G B) G \ A \ B = {\} \ (\x\A. \y\B. x \ y = y \ x)" proof - have subGA: "generate G (carrier G \ A) \ A" by (simp add: AG.subgroup_axioms generate_subgroup_incl) have subGB: "generate G (carrier G \ B) \ B" by (simp add: BG.subgroup_axioms generate_subgroup_incl) show ?thesis apply (auto simp: mon_def hom_group_mul_eq simp flip: subset_one) apply (simp_all (no_asm_use) add: inj_on_def AG.carrier_subgroup_generated_subgroup BG.carrier_subgroup_generated_subgroup) using cancel apply blast+ done qed lemma iso_group_mul_alt: "(\(x,y). x \ y) \ iso (subgroup_generated G A \\ subgroup_generated G B) G \ A \ B = {\} \ A <#> B = carrier G \ (\x\A. \y\B. x \ y = y \ x)" by (auto simp: iso_iff_mon_epi mon_group_mul_eq epi_group_mul_eq) lemma iso_group_mul_eq: "(\(x,y). x \ y) \ iso (subgroup_generated G A \\ subgroup_generated G B) G \ A \ B = {\} \ A <#> B = carrier G \ A \ G \ B \ G" by (simp add: iso_group_mul_alt normal_eq_commuting cong: conj_cong) lemma (in group) iso_group_mul_gen: assumes "A \ G" "B \ G" shows "(\(x,y). x \ y) \ iso (subgroup_generated G A \\ subgroup_generated G B) G \ A \ B \ {\} \ A <#> B = carrier G" proof - interpret group_disjoint_sum G A B using assms by (auto simp: group_disjoint_sum_def normal_def) show ?thesis by (simp add: subset_one iso_group_mul_eq assms) qed lemma iso_group_mul: assumes "comm_group G" shows "((\(x,y). x \ y) \ iso (DirProd (subgroup_generated G A) (subgroup_generated G B)) G \ A \ B \ {\} \ A <#> B = carrier G)" proof (rule iso_group_mul_gen) interpret comm_group by (rule assms) show "A \ G" by (simp add: AG.subgroup_axioms subgroup_imp_normal) show "B \ G" by (simp add: BG.subgroup_axioms subgroup_imp_normal) qed end subsection\The one-element group on a given object\ definition singleton_group :: "'a \ 'a monoid" where "singleton_group a = \carrier = {a}, monoid.mult = (\x y. a), one = a\" lemma singleton_group [simp]: "group (singleton_group a)" unfolding singleton_group_def by (auto intro: groupI) lemma singleton_abelian_group [simp]: "comm_group (singleton_group a)" by (metis group.group_comm_groupI monoid.simps(1) singleton_group singleton_group_def) lemma carrier_singleton_group [simp]: "carrier (singleton_group a) = {a}" by (auto simp: singleton_group_def) lemma (in group) hom_into_singleton_iff [simp]: "h \ hom G (singleton_group a) \ h \ carrier G \ {a}" by (auto simp: hom_def singleton_group_def) declare group.hom_into_singleton_iff [simp] lemma (in group) id_hom_singleton: "id \ hom (singleton_group \) G" by (simp add: hom_def singleton_group_def) subsection\Similarly, trivial groups\ definition trivial_group :: "('a, 'b) monoid_scheme \ bool" where "trivial_group G \ group G \ carrier G = {one G}" lemma trivial_imp_finite_group: "trivial_group G \ finite(carrier G)" by (simp add: trivial_group_def) lemma trivial_singleton_group [simp]: "trivial_group(singleton_group a)" by (metis monoid.simps(2) partial_object.simps(1) singleton_group singleton_group_def trivial_group_def) lemma (in group) trivial_group_subset: "trivial_group G \ carrier G \ {one G}" using is_group trivial_group_def by fastforce lemma (in group) trivial_group: "trivial_group G \ (\a. carrier G = {a})" unfolding trivial_group_def using one_closed is_group by fastforce lemma (in group) trivial_group_alt: "trivial_group G \ (\a. carrier G \ {a})" by (auto simp: trivial_group) lemma (in group) trivial_group_subgroup_generated: assumes "S \ {one G}" shows "trivial_group(subgroup_generated G S)" proof - have "carrier (subgroup_generated G S) \ {\}" using generate_empty generate_one subset_singletonD assms by (fastforce simp add: carrier_subgroup_generated) then show ?thesis by (simp add: group.trivial_group_subset) qed lemma (in group) trivial_group_subgroup_generated_eq: "trivial_group(subgroup_generated G s) \ carrier G \ s \ {one G}" apply (rule iffI) apply (force simp: trivial_group_def carrier_subgroup_generated generate.incl) by (metis subgroup_generated_restrict trivial_group_subgroup_generated) lemma isomorphic_group_triviality1: assumes "G \ H" "group H" "trivial_group G" shows "trivial_group H" using assms by (auto simp: trivial_group_def is_iso_def iso_def group.is_monoid Group.group_def bij_betw_def hom_one) lemma isomorphic_group_triviality: assumes "G \ H" "group G" "group H" shows "trivial_group G \ trivial_group H" by (meson assms group.iso_sym isomorphic_group_triviality1) lemma (in group_hom) kernel_from_trivial_group: "trivial_group G \ kernel G H h = carrier G" by (auto simp: trivial_group_def kernel_def) lemma (in group_hom) image_from_trivial_group: "trivial_group G \ h ` carrier G = {one H}" by (auto simp: trivial_group_def) lemma (in group_hom) kernel_to_trivial_group: "trivial_group H \ kernel G H h = carrier G" unfolding kernel_def trivial_group_def using hom_closed by blast subsection\The additive group of integers\ definition integer_group where "integer_group = \carrier = UNIV, monoid.mult = (+), one = (0::int)\" lemma group_integer_group [simp]: "group integer_group" unfolding integer_group_def proof (rule groupI; simp) show "\x::int. \y. y + x = 0" by presburger qed lemma carrier_integer_group [simp]: "carrier integer_group = UNIV" by (auto simp: integer_group_def) lemma one_integer_group [simp]: "\\<^bsub>integer_group\<^esub> = 0" by (auto simp: integer_group_def) lemma mult_integer_group [simp]: "x \\<^bsub>integer_group\<^esub> y = x + y" by (auto simp: integer_group_def) lemma inv_integer_group [simp]: "inv\<^bsub>integer_group\<^esub> x = -x" by (rule group.inv_equality [OF group_integer_group]) (auto simp: integer_group_def) lemma abelian_integer_group: "comm_group integer_group" by (rule group.group_comm_groupI [OF group_integer_group]) (auto simp: integer_group_def) lemma group_nat_pow_integer_group [simp]: fixes n::nat and x::int shows "pow integer_group x n = int n * x" by (induction n) (auto simp: integer_group_def algebra_simps) lemma group_int_pow_integer_group [simp]: fixes n::int and x::int shows "pow integer_group x n = n * x" by (simp add: int_pow_def2) lemma (in group) hom_integer_group_pow: "x \ carrier G \ pow G x \ hom integer_group G" by (rule homI) (auto simp: int_pow_mult) subsection\Additive group of integers modulo n (n = 0 gives just the integers)\ definition integer_mod_group :: "nat \ int monoid" where "integer_mod_group n \ if n = 0 then integer_group else \carrier = {0..x y. (x+y) mod int n), one = 0\" lemma carrier_integer_mod_group: "carrier(integer_mod_group n) = (if n=0 then UNIV else {0..x y. (x + y) mod int n)" by (simp add: integer_mod_group_def integer_group_def) lemma group_integer_mod_group [simp]: "group (integer_mod_group n)" proof - have *: "\y\0. y < int n \ (y + x) mod int n = 0" if "x < int n" "0 \ x" for x proof (cases "x=0") case False with that show ?thesis by (rule_tac x="int n - x" in exI) auto qed (use that in auto) show ?thesis apply (rule groupI) apply (auto simp: integer_mod_group_def Bex_def *, presburger+) done qed lemma inv_integer_mod_group[simp]: "x \ carrier (integer_mod_group n) \ m_inv(integer_mod_group n) x = (-x) mod int n" by (rule group.inv_equality [OF group_integer_mod_group]) (auto simp: integer_mod_group_def add.commute mod_add_right_eq) lemma pow_integer_mod_group [simp]: fixes m::nat shows "pow (integer_mod_group n) x m = (int m * x) mod int n" proof (cases "n=0") case False show ?thesis by (induction m) (auto simp: add.commute mod_add_right_eq distrib_left mult.commute) qed (simp add: integer_mod_group_def) lemma int_pow_integer_mod_group: "pow (integer_mod_group n) x m = (m * x) mod int n" proof - have "inv\<^bsub>integer_mod_group n\<^esub> (- (m * x) mod int n) = m * x mod int n" by (simp add: carrier_integer_mod_group mod_minus_eq) then show ?thesis by (simp add: int_pow_def2) qed lemma abelian_integer_mod_group [simp]: "comm_group(integer_mod_group n)" by (simp add: add.commute group.group_comm_groupI) lemma integer_mod_group_0 [simp]: "0 \ carrier(integer_mod_group n)" by (simp add: integer_mod_group_def) lemma integer_mod_group_1 [simp]: "1 \ carrier(integer_mod_group n) \ (n \ 1)" by (auto simp: integer_mod_group_def) lemma trivial_integer_mod_group: "trivial_group(integer_mod_group n) \ n = 1" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (simp add: trivial_group_def carrier_integer_mod_group set_eq_iff split: if_split_asm) (presburger+) next assume ?rhs then show ?lhs by (force simp: trivial_group_def carrier_integer_mod_group) qed subsection\Cyclic groups\ lemma (in group) subgroup_of_powers: "x \ carrier G \ subgroup (range (\n::int. x [^] n)) G" apply (auto simp: subgroup_def image_iff simp flip: int_pow_mult int_pow_neg) apply (metis group.int_pow_diff int_pow_closed is_group r_inv) done lemma (in group) carrier_subgroup_generated_by_singleton: assumes "x \ carrier G" shows "carrier(subgroup_generated G {x}) = (range (\n::int. x [^] n))" proof show "carrier (subgroup_generated G {x}) \ range (\n::int. x [^] n)" proof (rule subgroup_generated_minimal) show "subgroup (range (\n::int. x [^] n)) G" using assms subgroup_of_powers by blast show "{x} \ range (\n::int. x [^] n)" by clarify (metis assms int_pow_1 range_eqI) qed have x: "x \ carrier (subgroup_generated G {x})" using assms subgroup_generated_subset_carrier_subset by auto show "range (\n::int. x [^] n) \ carrier (subgroup_generated G {x})" proof clarify fix n :: "int" show "x [^] n \ carrier (subgroup_generated G {x})" by (simp add: x subgroup_int_pow_closed subgroup_subgroup_generated) qed qed definition cyclic_group where "cyclic_group G \ \x \ carrier G. subgroup_generated G {x} = G" lemma (in group) cyclic_group: "cyclic_group G \ (\x \ carrier G. carrier G = range (\n::int. x [^] n))" proof - have "\x. \x \ carrier G; carrier G = range (\n::int. x [^] n)\ \ \x\carrier G. subgroup_generated G {x} = G" by (rule_tac x=x in bexI) (auto simp: generate_pow subgroup_generated_def intro!: monoid.equality) then show ?thesis unfolding cyclic_group_def using carrier_subgroup_generated_by_singleton by fastforce qed lemma cyclic_integer_group [simp]: "cyclic_group integer_group" proof - have *: "int n \ generate integer_group {1}" for n proof (induction n) case 0 then show ?case using generate.simps by force next case (Suc n) then show ?case by simp (metis generate.simps insert_subset integer_group_def monoid.simps(1) subsetI) qed have **: "i \ generate integer_group {1}" for i proof (cases i rule: int_cases) case (nonneg n) then show ?thesis by (simp add: *) next case (neg n) then have "-i \ generate integer_group {1}" by (metis "*" add.inverse_inverse) then have "- (-i) \ generate integer_group {1}" by (metis UNIV_I group.generate_m_inv_closed group_integer_group integer_group_def inv_integer_group partial_object.select_convs(1) subsetI) then show ?thesis by simp qed show ?thesis unfolding cyclic_group_def by (rule_tac x=1 in bexI) (auto simp: carrier_subgroup_generated ** intro: monoid.equality) qed lemma nontrivial_integer_group [simp]: "\ trivial_group integer_group" using integer_mod_group_def trivial_integer_mod_group by presburger lemma (in group) cyclic_imp_abelian_group: "cyclic_group G \ comm_group G" apply (auto simp: cyclic_group comm_group_def is_group intro!: monoid_comm_monoidI) apply (metis add.commute int_pow_mult rangeI) done lemma trivial_imp_cyclic_group: "trivial_group G \ cyclic_group G" by (metis cyclic_group_def group.subgroup_generated_group_carrier insertI1 trivial_group_def) lemma (in group) cyclic_group_alt: "cyclic_group G \ (\x. subgroup_generated G {x} = G)" proof safe fix x assume *: "subgroup_generated G {x} = G" show "cyclic_group G" proof (cases "x \ carrier G") case True then show ?thesis using \subgroup_generated G {x} = G\ cyclic_group_def by blast next case False then show ?thesis by (metis "*" Int_empty_right Int_insert_right_if0 carrier_subgroup_generated generate_empty trivial_group trivial_imp_cyclic_group) qed qed (auto simp: cyclic_group_def) lemma (in group) cyclic_group_generated: "cyclic_group (subgroup_generated G {x})" using group.cyclic_group_alt group_subgroup_generated subgroup_generated2 by blast lemma (in group) cyclic_group_epimorphic_image: assumes "h \ epi G H" "cyclic_group G" "group H" shows "cyclic_group H" proof - interpret h: group_hom using assms by (simp add: group_hom_def group_hom_axioms_def is_group epi_def) obtain x where "x \ carrier G" and x: "carrier G = range (\n::int. x [^] n)" and eq: "carrier H = h ` carrier G" using assms by (auto simp: cyclic_group epi_def) have "h ` carrier G = range (\n::int. h x [^]\<^bsub>H\<^esub> n)" by (metis (no_types, lifting) \x \ carrier G\ h.hom_int_pow image_cong image_image x) then show ?thesis using \x \ carrier G\ eq h.cyclic_group by blast qed lemma isomorphic_group_cyclicity: "\G \ H; group G; group H\ \ cyclic_group G \ cyclic_group H" by (meson ex_in_conv group.cyclic_group_epimorphic_image group.iso_sym is_iso_def iso_iff_mon_epi) -lemma (in group) - assumes "x \ carrier G" - shows finite_cyclic_subgroup: - "finite(carrier(subgroup_generated G {x})) \ (\n::nat. n \ 0 \ x [^] n = \)" (is "?fin \ ?nat1") - and infinite_cyclic_subgroup: - "infinite(carrier(subgroup_generated G {x})) \ (\m n::nat. x [^] m = x [^] n \ m = n)" (is "\ ?fin \ ?nateq") - and finite_cyclic_subgroup_int: - "finite(carrier(subgroup_generated G {x})) \ (\i::int. i \ 0 \ x [^] i = \)" (is "?fin \ ?int1") - and infinite_cyclic_subgroup_int: - "infinite(carrier(subgroup_generated G {x})) \ (\i j::int. x [^] i = x [^] j \ i = j)" (is "\ ?fin \ ?inteq") -proof - - have 1: "\ ?fin" if ?nateq - proof - - have "infinite (range (\n::nat. x [^] n))" - using that range_inj_infinite [of "(\n::nat. x [^] n)"] by (auto simp: inj_on_def) - moreover have "range (\n::nat. x [^] n) \ range (\i::int. x [^] i)" - apply clarify - by (metis assms group.int_pow_neg int_pow_closed int_pow_neg_int is_group local.inv_equality nat_pow_closed r_inv rangeI) - ultimately show ?thesis - using carrier_subgroup_generated_by_singleton [OF assms] finite_subset by auto - qed - have 2: "m = n" if mn: "x [^] m = x [^] n" and eq [rule_format]: "?inteq" for m n::nat - using eq [of "int m" "int n"] - by (simp add: int_pow_int mn) - have 3: ?nat1 if non: "\ ?inteq" - proof - - obtain i j::int where eq: "x [^] i = x [^] j" and "i \ j" - using non by auto - show ?thesis - proof (cases i j rule: linorder_cases) - case less - then have [simp]: "x [^] (j - i) = \" - by (simp add: eq assms int_pow_diff) - show ?thesis - using less by (rule_tac x="nat (j-i)" in exI) auto - next - case greater - then have [simp]: "x [^] (i - j) = \" - by (simp add: eq assms int_pow_diff) - then show ?thesis - using greater by (rule_tac x="nat (i-j)" in exI) auto - qed (use \i \ j\ in auto) - qed - have 4: "\i::int. (i \ 0) \ x [^] i = \" if "n \ 0" "x [^] n = \" for n::nat - apply (rule_tac x="int n" in exI) - by (simp add: int_pow_int that) - have 5: "finite (carrier (subgroup_generated G {x}))" if "i \ 0" and 1: "x [^] i = \" for i::int - proof - - obtain n::nat where n: "n > 0" "x [^] n = \" - using "1" "3" \i \ 0\ by fastforce - have "x [^] a \ ([^]) x ` {0.. {0.. ([^]) x ` {0.. ?nat1" "\ ?fin \ ?nateq" "?fin \ ?int1" "\ ?fin \ ?inteq" - using 1 2 3 4 5 by meson+ -qed - -lemma (in group) finite_cyclic_subgroup_order: - "x \ carrier G \ finite(carrier(subgroup_generated G {x})) \ ord x \ 0" - by (simp add: finite_cyclic_subgroup ord_eq_0) - -lemma (in group) infinite_cyclic_subgroup_order: - "x \ carrier G \ infinite (carrier(subgroup_generated G {x})) \ ord x = 0" - by (simp add: finite_cyclic_subgroup_order) - - end diff --git a/src/HOL/Algebra/Free_Abelian_Groups.thy b/src/HOL/Algebra/Free_Abelian_Groups.thy --- a/src/HOL/Algebra/Free_Abelian_Groups.thy +++ b/src/HOL/Algebra/Free_Abelian_Groups.thy @@ -1,755 +1,755 @@ section\Free Abelian Groups\ theory Free_Abelian_Groups imports - Product_Groups "HOL-Cardinals.Cardinal_Arithmetic" + Product_Groups FiniteProduct "HOL-Cardinals.Cardinal_Arithmetic" "HOL-Library.Countable_Set" "HOL-Library.Poly_Mapping" "HOL-Library.Equipollence" begin (*Move? But where?*) lemma eqpoll_Fpow: assumes "infinite A" shows "Fpow A \ A" unfolding eqpoll_iff_card_of_ordIso by (metis assms card_of_Fpow_infinite) lemma infinite_iff_card_of_countable: "\countable B; infinite B\ \ infinite A \ ( |B| \o |A| )" unfolding infinite_iff_countable_subset card_of_ordLeq countable_def by (force intro: card_of_ordLeqI ordLeq_transitive) lemma iso_imp_eqpoll_carrier: "G \ H \ carrier G \ carrier H" by (auto simp: is_iso_def iso_def eqpoll_def) subsection\Generalised finite product\ definition gfinprod :: "[('b, 'm) monoid_scheme, 'a \ 'b, 'a set] \ 'b" where "gfinprod G f A = (if finite {x \ A. f x \ \\<^bsub>G\<^esub>} then finprod G f {x \ A. f x \ \\<^bsub>G\<^esub>} else \\<^bsub>G\<^esub>)" context comm_monoid begin lemma gfinprod_closed [simp]: "f \ A \ carrier G \ gfinprod G f A \ carrier G" unfolding gfinprod_def by (auto simp: image_subset_iff_funcset intro: finprod_closed) lemma gfinprod_cong: "\A = B; f \ B \ carrier G; \i. i \ B =simp=> f i = g i\ \ gfinprod G f A = gfinprod G g B" unfolding gfinprod_def by (auto simp: simp_implies_def cong: conj_cong intro: finprod_cong) lemma gfinprod_eq_finprod [simp]: "\finite A; f \ A \ carrier G\ \ gfinprod G f A = finprod G f A" by (auto simp: gfinprod_def intro: finprod_mono_neutral_cong_left) lemma gfinprod_insert [simp]: assumes "finite {x \ A. f x \ \\<^bsub>G\<^esub>}" "f \ A \ carrier G" "f i \ carrier G" shows "gfinprod G f (insert i A) = (if i \ A then gfinprod G f A else f i \ gfinprod G f A)" proof - have f: "f \ {x \ A. f x \ \} \ carrier G" using assms by (auto simp: image_subset_iff_funcset) have "{x. x = i \ f x \ \ \ x \ A \ f x \ \} = (if f i = \ then {x \ A. f x \ \} else insert i {x \ A. f x \ \})" by auto then show ?thesis using assms unfolding gfinprod_def by (simp add: conj_disj_distribR insert_absorb f split: if_split_asm) qed lemma gfinprod_distrib: assumes fin: "finite {x \ A. f x \ \\<^bsub>G\<^esub>}" "finite {x \ A. g x \ \\<^bsub>G\<^esub>}" and "f \ A \ carrier G" "g \ A \ carrier G" shows "gfinprod G (\i. f i \ g i) A = gfinprod G f A \ gfinprod G g A" proof - have "finite {x \ A. f x \ g x \ \}" by (auto intro: finite_subset [OF _ finite_UnI [OF fin]]) then have "gfinprod G (\i. f i \ g i) A = gfinprod G (\i. f i \ g i) ({i \ A. f i \ \\<^bsub>G\<^esub>} \ {i \ A. g i \ \\<^bsub>G\<^esub>})" unfolding gfinprod_def using assms by (force intro: finprod_mono_neutral_cong) also have "\ = gfinprod G f A \ gfinprod G g A" proof - have "finprod G f ({i \ A. f i \ \\<^bsub>G\<^esub>} \ {i \ A. g i \ \\<^bsub>G\<^esub>}) = gfinprod G f A" "finprod G g ({i \ A. f i \ \\<^bsub>G\<^esub>} \ {i \ A. g i \ \\<^bsub>G\<^esub>}) = gfinprod G g A" using assms by (auto simp: gfinprod_def intro: finprod_mono_neutral_cong_right) moreover have "(\i. f i \ g i) \ {i \ A. f i \ \} \ {i \ A. g i \ \} \ carrier G" using assms by (force simp: image_subset_iff_funcset) ultimately show ?thesis using assms apply simp apply (subst finprod_multf, auto) done qed finally show ?thesis . qed lemma gfinprod_mono_neutral_cong_left: assumes "A \ B" and 1: "\i. i \ B - A \ h i = \" and gh: "\x. x \ A \ g x = h x" and h: "h \ B \ carrier G" shows "gfinprod G g A = gfinprod G h B" proof (cases "finite {x \ B. h x \ \}") case True then have "finite {x \ A. h x \ \}" apply (rule rev_finite_subset) using \A \ B\ by auto with True assms show ?thesis apply (simp add: gfinprod_def cong: conj_cong) apply (auto intro!: finprod_mono_neutral_cong_left) done next case False have "{x \ B. h x \ \} \ {x \ A. h x \ \}" using 1 by auto with False have "infinite {x \ A. h x \ \}" using infinite_super by blast with False assms show ?thesis by (simp add: gfinprod_def cong: conj_cong) qed lemma gfinprod_mono_neutral_cong_right: assumes "A \ B" "\i. i \ B - A \ g i = \" "\x. x \ A \ g x = h x" "g \ B \ carrier G" shows "gfinprod G g B = gfinprod G h A" using assms by (auto intro!: gfinprod_mono_neutral_cong_left [symmetric]) lemma gfinprod_mono_neutral_cong: assumes [simp]: "finite B" "finite A" and *: "\i. i \ B - A \ h i = \" "\i. i \ A - B \ g i = \" and gh: "\x. x \ A \ B \ g x = h x" and g: "g \ A \ carrier G" and h: "h \ B \ carrier G" shows "gfinprod G g A = gfinprod G h B" proof- have "gfinprod G g A = gfinprod G g (A \ B)" by (rule gfinprod_mono_neutral_cong_right) (use assms in auto) also have "\ = gfinprod G h (A \ B)" by (rule gfinprod_cong) (use assms in auto) also have "\ = gfinprod G h B" by (rule gfinprod_mono_neutral_cong_left) (use assms in auto) finally show ?thesis . qed end lemma (in comm_group) hom_group_sum: assumes hom: "\i. i \ I \ f i \ hom (A i) G" and grp: "\i. i \ I \ group (A i)" shows "(\x. gfinprod G (\i. (f i) (x i)) I) \ hom (sum_group I A) G" unfolding hom_def proof (intro CollectI conjI ballI) show "(\x. gfinprod G (\i. f i (x i)) I) \ carrier (sum_group I A) \ carrier G" using assms by (force simp: hom_def carrier_sum_group intro: gfinprod_closed simp flip: image_subset_iff_funcset) next fix x y assume x: "x \ carrier (sum_group I A)" and y: "y \ carrier (sum_group I A)" then have finx: "finite {i \ I. x i \ \\<^bsub>A i\<^esub>}" and finy: "finite {i \ I. y i \ \\<^bsub>A i\<^esub>}" using assms by (auto simp: carrier_sum_group) have finfx: "finite {i \ I. f i (x i) \ \}" using assms by (auto simp: is_group hom_one [OF hom] intro: finite_subset [OF _ finx]) have finfy: "finite {i \ I. f i (y i) \ \}" using assms by (auto simp: is_group hom_one [OF hom] intro: finite_subset [OF _ finy]) have carr: "f i (x i) \ carrier G" "f i (y i) \ carrier G" if "i \ I" for i using hom_carrier [OF hom] that x y assms by (fastforce simp add: carrier_sum_group)+ have lam: "(\i. f i ( x i \\<^bsub>A i\<^esub> y i)) \ I \ carrier G" using x y assms by (auto simp: hom_def carrier_sum_group PiE_def Pi_def) have lam': "(\i. f i (if i \ I then x i \\<^bsub>A i\<^esub> y i else undefined)) \ I \ carrier G" by (simp add: lam Pi_cong) with lam x y assms show "gfinprod G (\i. f i ((x \\<^bsub>sum_group I A\<^esub> y) i)) I = gfinprod G (\i. f i (x i)) I \ gfinprod G (\i. f i (y i)) I" by (simp add: carrier_sum_group PiE_def Pi_def hom_mult [OF hom] gfinprod_distrib finfx finfy carr cong: gfinprod_cong) qed subsection\Free Abelian groups on a set, using the "frag" type constructor. \ definition free_Abelian_group :: "'a set \ ('a \\<^sub>0 int) monoid" where "free_Abelian_group S = \carrier = {c. Poly_Mapping.keys c \ S}, monoid.mult = (+), one = 0\" lemma group_free_Abelian_group [simp]: "group (free_Abelian_group S)" proof - have "\x. Poly_Mapping.keys x \ S \ x \ Units (free_Abelian_group S)" unfolding free_Abelian_group_def Units_def by clarsimp (metis eq_neg_iff_add_eq_0 neg_eq_iff_add_eq_0 keys_minus) then show ?thesis unfolding free_Abelian_group_def by unfold_locales (auto simp: dest: subsetD [OF keys_add]) qed lemma carrier_free_Abelian_group_iff [simp]: shows "x \ carrier (free_Abelian_group S) \ Poly_Mapping.keys x \ S" by (auto simp: free_Abelian_group_def) lemma one_free_Abelian_group [simp]: "\\<^bsub>free_Abelian_group S\<^esub> = 0" by (auto simp: free_Abelian_group_def) lemma mult_free_Abelian_group [simp]: "x \\<^bsub>free_Abelian_group S\<^esub> y = x + y" by (auto simp: free_Abelian_group_def) lemma inv_free_Abelian_group [simp]: "Poly_Mapping.keys x \ S \ inv\<^bsub>free_Abelian_group S\<^esub> x = -x" by (rule group.inv_equality [OF group_free_Abelian_group]) auto lemma abelian_free_Abelian_group: "comm_group(free_Abelian_group S)" apply (rule group.group_comm_groupI [OF group_free_Abelian_group]) by (simp add: free_Abelian_group_def) lemma pow_free_Abelian_group [simp]: fixes n::nat shows "Group.pow (free_Abelian_group S) x n = frag_cmul (int n) x" by (induction n) (auto simp: nat_pow_def free_Abelian_group_def frag_cmul_distrib) lemma int_pow_free_Abelian_group [simp]: fixes n::int assumes "Poly_Mapping.keys x \ S" shows "Group.pow (free_Abelian_group S) x n = frag_cmul n x" proof (induction n) case (nonneg n) then show ?case by (simp add: int_pow_int) next case (neg n) have "x [^]\<^bsub>free_Abelian_group S\<^esub> - int (Suc n) = inv\<^bsub>free_Abelian_group S\<^esub> (x [^]\<^bsub>free_Abelian_group S\<^esub> int (Suc n))" by (rule group.int_pow_neg [OF group_free_Abelian_group]) (use assms in \simp add: free_Abelian_group_def\) also have "\ = frag_cmul (- int (Suc n)) x" by (metis assms inv_free_Abelian_group pow_free_Abelian_group int_pow_int minus_frag_cmul order_trans keys_cmul) finally show ?case . qed lemma frag_of_in_free_Abelian_group [simp]: "frag_of x \ carrier(free_Abelian_group S) \ x \ S" by simp lemma free_Abelian_group_induct: assumes major: "Poly_Mapping.keys x \ S" and minor: "P(0)" "\x y. \Poly_Mapping.keys x \ S; Poly_Mapping.keys y \ S; P x; P y\ \ P(x-y)" "\a. a \ S \ P(frag_of a)" shows "P x" proof - have "Poly_Mapping.keys x \ S \ P x" using major proof (induction x rule: frag_induction) case (diff a b) then show ?case by (meson Un_least minor(2) order.trans keys_diff) qed (auto intro: minor) then show ?thesis .. qed lemma sum_closed_free_Abelian_group: "(\i. i \ I \ x i \ carrier (free_Abelian_group S)) \ sum x I \ carrier (free_Abelian_group S)" apply (induction I rule: infinite_finite_induct, auto) by (metis (no_types, hide_lams) UnE subsetCE keys_add) lemma (in comm_group) free_Abelian_group_universal: fixes f :: "'c \ 'a" assumes "f ` S \ carrier G" obtains h where "h \ hom (free_Abelian_group S) G" "\x. x \ S \ h(frag_of x) = f x" proof have fin: "Poly_Mapping.keys u \ S \ finite {x \ S. f x [^] poly_mapping.lookup u x \ \}" for u :: "'c \\<^sub>0 int" apply (rule finite_subset [OF _ finite_keys [of u]]) unfolding keys.rep_eq by force define h :: "('c \\<^sub>0 int) \ 'a" where "h \ \x. gfinprod G (\a. f a [^] poly_mapping.lookup x a) S" show "h \ hom (free_Abelian_group S) G" proof (rule homI) fix x y assume xy: "x \ carrier (free_Abelian_group S)" "y \ carrier (free_Abelian_group S)" then show "h (x \\<^bsub>free_Abelian_group S\<^esub> y) = h x \ h y" using assms unfolding h_def free_Abelian_group_def by (simp add: fin gfinprod_distrib image_subset_iff Poly_Mapping.lookup_add int_pow_mult cong: gfinprod_cong) qed (use assms in \force simp: free_Abelian_group_def h_def intro: gfinprod_closed\) show "h(frag_of x) = f x" if "x \ S" for x proof - have fin: "(\a. f x [^] (1::int)) \ {x} \ carrier G" "f x [^] (1::int) \ carrier G" using assms that by force+ show ?thesis by (cases " f x [^] (1::int) = \") (use assms that in \auto simp: h_def gfinprod_def finprod_singleton\) qed qed lemma eqpoll_free_Abelian_group_infinite: assumes "infinite A" shows "carrier(free_Abelian_group A) \ A" proof (rule lepoll_antisym) have "carrier (free_Abelian_group A) \ {f::'a\int. f ` A \ UNIV \ {x. f x \ 0} \ A \ finite {x. f x \ 0}}" unfolding lepoll_def by (rule_tac x="Poly_Mapping.lookup" in exI) (auto simp: poly_mapping_eqI lookup_not_eq_zero_eq_in_keys inj_onI) also have "\ \ Fpow (A \ (UNIV::int set))" by (rule lepoll_restricted_funspace) also have "\ \ A \ (UNIV::int set)" proof (rule eqpoll_Fpow) show "infinite (A \ (UNIV::int set))" using assms finite_cartesian_productD1 by fastforce qed also have "\ \ A" unfolding eqpoll_iff_card_of_ordIso proof - have "|A \ (UNIV::int set)| <=o |A|" by (simp add: assms card_of_Times_ordLeq_infinite flip: infinite_iff_card_of_countable) moreover have "|A| \o |A \ (UNIV::int set)|" by simp ultimately have "|A| *c |(UNIV::int set)| =o |A|" by (simp add: cprod_def ordIso_iff_ordLeq) then show "|A \ (UNIV::int set)| =o |A|" by (metis Times_cprod ordIso_transitive) qed finally show "carrier (free_Abelian_group A) \ A" . have "inj_on frag_of A" by (simp add: frag_of_eq inj_on_def) moreover have "frag_of ` A \ carrier (free_Abelian_group A)" by (simp add: image_subsetI) ultimately show "A \ carrier (free_Abelian_group A)" by (force simp: lepoll_def) qed proposition (in comm_group) eqpoll_homomorphisms_from_free_Abelian_group: "{f. f \ extensional (carrier(free_Abelian_group S)) \ f \ hom (free_Abelian_group S) G} \ (S \\<^sub>E carrier G)" (is "?lhs \ ?rhs") unfolding eqpoll_def bij_betw_def proof (intro exI conjI) let ?f = "\f. restrict (f \ frag_of) S" show "inj_on ?f ?lhs" proof (clarsimp simp: inj_on_def) fix g h assume g: "g \ extensional (carrier (free_Abelian_group S))" "g \ hom (free_Abelian_group S) G" and h: "h \ extensional (carrier (free_Abelian_group S))" "h \ hom (free_Abelian_group S) G" and eq: "restrict (g \ frag_of) S = restrict (h \ frag_of) S" have 0: "0 \ carrier (free_Abelian_group S)" by simp interpret hom_g: group_hom "free_Abelian_group S" G g using g by (auto simp: group_hom_def group_hom_axioms_def is_group) interpret hom_h: group_hom "free_Abelian_group S" G h using h by (auto simp: group_hom_def group_hom_axioms_def is_group) have "Poly_Mapping.keys c \ S \ Poly_Mapping.keys c \ S \ g c = h c" for c proof (induction c rule: frag_induction) case zero show ?case using hom_g.hom_one hom_h.hom_one by auto next case (one x) then show ?case using eq by (simp add: fun_eq_iff) (metis comp_def) next case (diff a b) then show ?case using hom_g.hom_mult hom_h.hom_mult hom_g.hom_inv hom_h.hom_inv apply (auto simp: dest: subsetD [OF keys_diff]) by (metis keys_minus uminus_add_conv_diff) qed then show "g = h" by (meson g h carrier_free_Abelian_group_iff extensionalityI) qed have "f \ (\f. restrict (f \ frag_of) S) ` {f \ extensional (carrier (free_Abelian_group S)). f \ hom (free_Abelian_group S) G}" if f: "f \ S \\<^sub>E carrier G" for f :: "'c \ 'a" proof - obtain h where h: "h \ hom (free_Abelian_group S) G" "\x. x \ S \ h(frag_of x) = f x" proof (rule free_Abelian_group_universal) show "f ` S \ carrier G" using f by blast qed auto let ?h = "restrict h (carrier (free_Abelian_group S))" show ?thesis proof show "f = restrict (?h \ frag_of) S" using f by (force simp: h) show "?h \ {f \ extensional (carrier (free_Abelian_group S)). f \ hom (free_Abelian_group S) G}" using h by (auto simp: hom_def dest!: subsetD [OF keys_add]) qed qed then show "?f ` ?lhs = S \\<^sub>E carrier G" by (auto simp: hom_def Ball_def Pi_def) qed lemma hom_frag_minus: assumes "h \ hom (free_Abelian_group S) (free_Abelian_group T)" "Poly_Mapping.keys a \ S" shows "h (-a) = - (h a)" proof - have "Poly_Mapping.keys (h a) \ T" by (meson assms carrier_free_Abelian_group_iff hom_in_carrier) then show ?thesis by (metis (no_types) assms carrier_free_Abelian_group_iff group_free_Abelian_group group_hom.hom_inv group_hom_axioms_def group_hom_def inv_free_Abelian_group) qed lemma hom_frag_add: assumes "h \ hom (free_Abelian_group S) (free_Abelian_group T)" "Poly_Mapping.keys a \ S" "Poly_Mapping.keys b \ S" shows "h (a+b) = h a + h b" proof - have "Poly_Mapping.keys (h a) \ T" by (meson assms carrier_free_Abelian_group_iff hom_in_carrier) moreover have "Poly_Mapping.keys (h b) \ T" by (meson assms carrier_free_Abelian_group_iff hom_in_carrier) ultimately show ?thesis using assms hom_mult by fastforce qed lemma hom_frag_diff: assumes "h \ hom (free_Abelian_group S) (free_Abelian_group T)" "Poly_Mapping.keys a \ S" "Poly_Mapping.keys b \ S" shows "h (a-b) = h a - h b" by (metis (no_types, lifting) assms diff_conv_add_uminus hom_frag_add hom_frag_minus keys_minus) proposition isomorphic_free_Abelian_groups: "free_Abelian_group S \ free_Abelian_group T \ S \ T" (is "(?FS \ ?FT) = ?rhs") proof interpret S: group "?FS" by simp interpret T: group "?FT" by simp interpret G2: comm_group "integer_mod_group 2" by (rule abelian_integer_mod_group) let ?Two = "{0..<2::int}" have [simp]: "\ ?Two \ {a}" for a by (simp add: subset_iff) presburger assume L: "?FS \ ?FT" let ?HS = "{h \ extensional (carrier ?FS). h \ hom ?FS (integer_mod_group 2)}" let ?HT = "{h \ extensional (carrier ?FT). h \ hom ?FT (integer_mod_group 2)}" have "S \\<^sub>E ?Two \ ?HS" apply (rule eqpoll_sym) using G2.eqpoll_homomorphisms_from_free_Abelian_group by (simp add: carrier_integer_mod_group) also have "\ \ ?HT" proof - obtain f g where "group_isomorphisms ?FS ?FT f g" using L S.iso_iff_group_isomorphisms by (force simp: is_iso_def) then have f: "f \ hom ?FS ?FT" and g: "g \ hom ?FT ?FS" and gf: "\x \ carrier ?FS. g(f x) = x" and fg: "\y \ carrier ?FT. f(g y) = y" by (auto simp: group_isomorphisms_def) let ?f = "\h. restrict (h \ g) (carrier ?FT)" let ?g = "\h. restrict (h \ f) (carrier ?FS)" show ?thesis proof (rule lepoll_antisym) show "?HS \ ?HT" unfolding lepoll_def proof (intro exI conjI) show "inj_on ?f ?HS" apply (rule inj_on_inverseI [where g = ?g]) using hom_in_carrier [OF f] by (auto simp: gf fun_eq_iff carrier_integer_mod_group Ball_def Pi_def extensional_def) show "?f ` ?HS \ ?HT" proof clarsimp fix h assume h: "h \ hom ?FS (integer_mod_group 2)" have "h \ g \ hom ?FT (integer_mod_group 2)" by (rule hom_compose [OF g h]) moreover have "restrict (h \ g) (carrier ?FT) x = (h \ g) x" if "x \ carrier ?FT" for x using g that by (simp add: hom_def) ultimately show "restrict (h \ g) (carrier ?FT) \ hom ?FT (integer_mod_group 2)" using T.hom_restrict by fastforce qed qed next show "?HT \ ?HS" unfolding lepoll_def proof (intro exI conjI) show "inj_on ?g ?HT" apply (rule inj_on_inverseI [where g = ?f]) using hom_in_carrier [OF g] by (auto simp: fg fun_eq_iff carrier_integer_mod_group Ball_def Pi_def extensional_def) show "?g ` ?HT \ ?HS" proof clarsimp fix k assume k: "k \ hom ?FT (integer_mod_group 2)" have "k \ f \ hom ?FS (integer_mod_group 2)" by (rule hom_compose [OF f k]) moreover have "restrict (k \ f) (carrier ?FS) x = (k \ f) x" if "x \ carrier ?FS" for x using f that by (simp add: hom_def) ultimately show "restrict (k \ f) (carrier ?FS) \ hom ?FS (integer_mod_group 2)" using S.hom_restrict by fastforce qed qed qed qed also have "\ \ T \\<^sub>E ?Two" using G2.eqpoll_homomorphisms_from_free_Abelian_group by (simp add: carrier_integer_mod_group) finally have *: "S \\<^sub>E ?Two \ T \\<^sub>E ?Two" . then have "finite (S \\<^sub>E ?Two) \ finite (T \\<^sub>E ?Two)" by (rule eqpoll_finite_iff) then have "finite S \ finite T" by (auto simp: finite_funcset_iff) then consider "finite S" "finite T" | "~ finite S" "~ finite T" by blast then show ?rhs proof cases case 1 with * have "2 ^ card S = (2::nat) ^ card T" by (simp add: card_PiE finite_PiE eqpoll_iff_card) then have "card S = card T" by auto then show ?thesis using eqpoll_iff_card 1 by blast next case 2 have "carrier (free_Abelian_group S) \ carrier (free_Abelian_group T)" using L by (simp add: iso_imp_eqpoll_carrier) then show ?thesis using 2 eqpoll_free_Abelian_group_infinite eqpoll_sym eqpoll_trans by metis qed next assume ?rhs then obtain f g where f: "\x. x \ S \ f x \ T \ g(f x) = x" and g: "\y. y \ T \ g y \ S \ f(g y) = y" using eqpoll_iff_bijections by metis interpret S: comm_group "?FS" by (simp add: abelian_free_Abelian_group) interpret T: comm_group "?FT" by (simp add: abelian_free_Abelian_group) have "(frag_of \ f) ` S \ carrier (free_Abelian_group T)" using f by auto then obtain h where h: "h \ hom (free_Abelian_group S) (free_Abelian_group T)" and h_frag: "\x. x \ S \ h (frag_of x) = (frag_of \ f) x" using T.free_Abelian_group_universal [of "frag_of \ f" S] by blast interpret hhom: group_hom "free_Abelian_group S" "free_Abelian_group T" h by (simp add: h group_hom_axioms_def group_hom_def) have "(frag_of \ g) ` T \ carrier (free_Abelian_group S)" using g by auto then obtain k where k: "k \ hom (free_Abelian_group T) (free_Abelian_group S)" and k_frag: "\x. x \ T \ k (frag_of x) = (frag_of \ g) x" using S.free_Abelian_group_universal [of "frag_of \ g" T] by blast interpret khom: group_hom "free_Abelian_group T" "free_Abelian_group S" k by (simp add: k group_hom_axioms_def group_hom_def) have kh: "Poly_Mapping.keys x \ S \ Poly_Mapping.keys x \ S \ k (h x) = x" for x proof (induction rule: frag_induction) case zero then show ?case apply auto by (metis group_free_Abelian_group h hom_one k one_free_Abelian_group) next case (one x) then show ?case by (auto simp: h_frag k_frag f) next case (diff a b) with keys_diff have "Poly_Mapping.keys (a - b) \ S" by (metis Un_least order_trans) with diff hhom.hom_closed show ?case by (simp add: hom_frag_diff [OF h] hom_frag_diff [OF k]) qed have hk: "Poly_Mapping.keys y \ T \ Poly_Mapping.keys y \ T \ h (k y) = y" for y proof (induction rule: frag_induction) case zero then show ?case apply auto by (metis group_free_Abelian_group h hom_one k one_free_Abelian_group) next case (one y) then show ?case by (auto simp: h_frag k_frag g) next case (diff a b) with keys_diff have "Poly_Mapping.keys (a - b) \ T" by (metis Un_least order_trans) with diff khom.hom_closed show ?case by (simp add: hom_frag_diff [OF h] hom_frag_diff [OF k]) qed have "h \ iso ?FS ?FT" unfolding iso_def bij_betw_iff_bijections mem_Collect_eq proof (intro conjI exI ballI h) fix x assume x: "x \ carrier (free_Abelian_group S)" show "h x \ carrier (free_Abelian_group T)" by (meson x h hom_in_carrier) show "k (h x) = x" using x by (simp add: kh) next fix y assume y: "y \ carrier (free_Abelian_group T)" show "k y \ carrier (free_Abelian_group S)" by (meson y k hom_in_carrier) show "h (k y) = y" using y by (simp add: hk) qed then show "?FS \ ?FT" by (auto simp: is_iso_def) qed lemma isomorphic_group_integer_free_Abelian_group_singleton: "integer_group \ free_Abelian_group {x}" proof - have "(\n. frag_cmul n (frag_of x)) \ iso integer_group (free_Abelian_group {x})" proof (rule isoI [OF homI]) show "bij_betw (\n. frag_cmul n (frag_of x)) (carrier integer_group) (carrier (free_Abelian_group {x}))" apply (rule bij_betwI [where g = "\y. Poly_Mapping.lookup y x"]) by (auto simp: integer_group_def in_keys_iff intro!: poly_mapping_eqI) qed (auto simp: frag_cmul_distrib) then show ?thesis unfolding is_iso_def by blast qed lemma group_hom_free_Abelian_groups_id: "id \ hom (free_Abelian_group S) (free_Abelian_group T) \ S \ T" proof - have "x \ T" if ST: "\c:: 'a \\<^sub>0 int. Poly_Mapping.keys c \ S \ Poly_Mapping.keys c \ T" and "x \ S" for x using ST [of "frag_of x"] \x \ S\ by simp then show ?thesis by (auto simp: hom_def free_Abelian_group_def Pi_def) qed proposition iso_free_Abelian_group_sum: assumes "pairwise (\i j. disjnt (S i) (S j)) I" shows "(\f. sum' f I) \ iso (sum_group I (\i. free_Abelian_group(S i))) (free_Abelian_group (\(S ` I)))" (is "?h \ iso ?G ?H") proof (rule isoI) show hom: "?h \ hom ?G ?H" proof (rule homI) show "?h c \ carrier ?H" if "c \ carrier ?G" for c using that apply (simp add: sum.G_def carrier_sum_group) apply (rule order_trans [OF keys_sum]) apply (auto simp: free_Abelian_group_def) done show "?h (x \\<^bsub>?G\<^esub> y) = ?h x \\<^bsub>?H\<^esub> ?h y" if "x \ carrier ?G" "y \ carrier ?G" for x y using that by (simp add: sum.finite_Collect_op carrier_sum_group sum.distrib') qed interpret GH: group_hom "?G" "?H" "?h" using hom by (simp add: group_hom_def group_hom_axioms_def) show "bij_betw ?h (carrier ?G) (carrier ?H)" unfolding bij_betw_def proof (intro conjI subset_antisym) show "?h ` carrier ?G \ carrier ?H" apply (clarsimp simp: sum.G_def carrier_sum_group simp del: carrier_free_Abelian_group_iff) by (force simp: PiE_def Pi_iff intro!: sum_closed_free_Abelian_group) have *: "poly_mapping.lookup (Abs_poly_mapping (\j. if j \ S i then poly_mapping.lookup x j else 0)) k = (if k \ S i then poly_mapping.lookup x k else 0)" if "i \ I" for i k and x :: "'b \\<^sub>0 int" using that by (auto simp: conj_commute cong: conj_cong) have eq: "Abs_poly_mapping (\j. if j \ S i then poly_mapping.lookup x j else 0) = 0 \ (\c \ S i. poly_mapping.lookup x c = 0)" if "i \ I" for i and x :: "'b \\<^sub>0 int" apply (auto simp: poly_mapping_eq_iff fun_eq_iff) apply (simp add: * Abs_poly_mapping_inverse conj_commute cong: conj_cong) apply (force dest!: spec split: if_split_asm) done have "x \ ?h ` {x \ \\<^sub>E i\I. {c. Poly_Mapping.keys c \ S i}. finite {i \ I. x i \ 0}}" if x: "Poly_Mapping.keys x \ \ (S ` I)" for x :: "'b \\<^sub>0 int" proof - let ?f = "(\i c. if c \ S i then Poly_Mapping.lookup x c else 0)" define J where "J \ {i \ I. \c\S i. c \ Poly_Mapping.keys x}" have "J \ (\c. THE i. i \ I \ c \ S i) ` Poly_Mapping.keys x" proof (clarsimp simp: J_def) show "i \ (\c. THE i. i \ I \ c \ S i) ` Poly_Mapping.keys x" if "i \ I" "c \ S i" "c \ Poly_Mapping.keys x" for i c proof show "i = (THE i. i \ I \ c \ S i)" using assms that by (auto simp: pairwise_def disjnt_def intro: the_equality [symmetric]) qed (simp add: that) qed then have fin: "finite J" using finite_subset finite_keys by blast have [simp]: "Poly_Mapping.keys (Abs_poly_mapping (?f i)) = {k. ?f i k \ 0}" if "i \ I" for i by (simp add: eq_onp_def keys.abs_eq conj_commute cong: conj_cong) have [simp]: "Poly_Mapping.lookup (Abs_poly_mapping (?f i)) c = ?f i c" if "i \ I" for i c by (auto simp: Abs_poly_mapping_inverse conj_commute cong: conj_cong) show ?thesis proof have "poly_mapping.lookup x c = poly_mapping.lookup (?h (\i\I. Abs_poly_mapping (?f i))) c" for c proof (cases "c \ Poly_Mapping.keys x") case True then obtain i where "i \ I" "c \ S i" "?f i c \ 0" using x by (auto simp: in_keys_iff) then have 1: "poly_mapping.lookup (sum' (\j. Abs_poly_mapping (?f j)) (I - {i})) c = 0" using assms apply (simp add: sum.G_def Poly_Mapping.lookup_sum pairwise_def disjnt_def) apply (force simp: eq split: if_split_asm intro!: comm_monoid_add_class.sum.neutral) done have 2: "poly_mapping.lookup x c = poly_mapping.lookup (Abs_poly_mapping (?f i)) c" by (auto simp: \c \ S i\ Abs_poly_mapping_inverse conj_commute cong: conj_cong) have "finite {i \ I. Abs_poly_mapping (?f i) \ 0}" by (rule finite_subset [OF _ fin]) (use \i \ I\ J_def eq in \auto simp: in_keys_iff\) with \i \ I\ have "?h (\j\I. Abs_poly_mapping (?f j)) = Abs_poly_mapping (?f i) + sum' (\j. Abs_poly_mapping (?f j)) (I - {i})" by (simp add: sum_diff1') then show ?thesis by (simp add: 1 2 Poly_Mapping.lookup_add) next case False then have "poly_mapping.lookup x c = 0" using keys.rep_eq by force then show ?thesis unfolding sum.G_def by (simp add: lookup_sum * comm_monoid_add_class.sum.neutral) qed then show "x = ?h (\i\I. Abs_poly_mapping (?f i))" by (rule poly_mapping_eqI) have "(\i. Abs_poly_mapping (?f i)) \ (\ i\I. {c. Poly_Mapping.keys c \ S i})" by (auto simp: PiE_def Pi_def in_keys_iff) then show "(\i\I. Abs_poly_mapping (?f i)) \ {x \ \\<^sub>E i\I. {c. Poly_Mapping.keys c \ S i}. finite {i \ I. x i \ 0}}" using fin unfolding J_def by (simp add: eq in_keys_iff cong: conj_cong) qed qed then show "carrier ?H \ ?h ` carrier ?G" by (simp add: carrier_sum_group) (auto simp: free_Abelian_group_def) show "inj_on ?h (carrier (sum_group I (\i. free_Abelian_group (S i))))" unfolding GH.inj_on_one_iff proof clarify fix x assume "x \ carrier ?G" "?h x = \\<^bsub>?H\<^esub>" then have eq0: "sum' x I = 0" and xs: "\i. i \ I \ Poly_Mapping.keys (x i) \ S i" and xext: "x \ extensional I" and fin: "finite {i \ I. x i \ 0}" by (simp_all add: carrier_sum_group PiE_def Pi_def) have "x i = 0" if "i \ I" for i proof - have "sum' x (insert i (I - {i})) = 0" using eq0 that by (simp add: insert_absorb) moreover have "Poly_Mapping.keys (sum' x (I - {i})) = {}" proof - have "x i = - sum' x (I - {i})" by (metis (mono_tags, lifting) diff_zero eq0 fin sum_diff1' minus_diff_eq that) then have "Poly_Mapping.keys (x i) = Poly_Mapping.keys (sum' x (I - {i}))" by simp then have "Poly_Mapping.keys (sum' x (I - {i})) \ S i" using that xs by metis moreover have "Poly_Mapping.keys (sum' x (I - {i})) \ (\j \ I - {i}. S j)" proof - have "Poly_Mapping.keys (sum' x (I - {i})) \ (\i\{j \ I. j \ i \ x j \ 0}. Poly_Mapping.keys (x i))" using keys_sum [of x "{j \ I. j \ i \ x j \ 0}"] by (simp add: sum.G_def) also have "\ \ \ (S ` (I - {i}))" using xs by force finally show ?thesis . qed moreover have "A = {}" if "A \ S i" "A \ \ (S ` (I - {i}))" for A using assms that \i \ I\ by (force simp: pairwise_def disjnt_def image_def subset_iff) ultimately show ?thesis by metis qed then have [simp]: "sum' x (I - {i}) = 0" by (auto simp: sum.G_def) have "sum' x (insert i (I - {i})) = x i" by (subst sum.insert' [OF finite_subset [OF _ fin]]) auto ultimately show ?thesis by metis qed with xext [unfolded extensional_def] show "x = \\<^bsub>sum_group I (\i. free_Abelian_group (S i))\<^esub>" by (force simp: free_Abelian_group_def) qed qed qed lemma isomorphic_free_Abelian_group_Union: "pairwise disjnt I \ free_Abelian_group(\ I) \ sum_group I free_Abelian_group" using iso_free_Abelian_group_sum [of "\X. X" I] by (metis SUP_identity_eq empty_iff group.iso_sym group_free_Abelian_group is_iso_def sum_group) lemma isomorphic_sum_integer_group: "sum_group I (\i. integer_group) \ free_Abelian_group I" proof - have "sum_group I (\i. integer_group) \ sum_group I (\i. free_Abelian_group {i})" by (rule iso_sum_groupI) (auto simp: isomorphic_group_integer_free_Abelian_group_singleton) also have "\ \ free_Abelian_group I" using iso_free_Abelian_group_sum [of "\x. {x}" I] by (auto simp: is_iso_def) finally show ?thesis . qed end diff --git a/src/HOL/Algebra/Multiplicative_Group.thy b/src/HOL/Algebra/Multiplicative_Group.thy --- a/src/HOL/Algebra/Multiplicative_Group.thy +++ b/src/HOL/Algebra/Multiplicative_Group.thy @@ -1,910 +1,1061 @@ (* Title: HOL/Algebra/Multiplicative_Group.thy Author: Simon Wimmer Author: Lars Noschinski *) theory Multiplicative_Group imports Complex_Main Group Coset UnivPoly Generated_Groups + Elementary_Groups begin section \Simplification Rules for Polynomials\ text_raw \\label{sec:simp-rules}\ lemma (in ring_hom_cring) hom_sub[simp]: assumes "x \ carrier R" "y \ carrier R" shows "h (x \ y) = h x \\<^bsub>S\<^esub> h y" using assms by (simp add: R.minus_eq S.minus_eq) context UP_ring begin lemma deg_nzero_nzero: assumes deg_p_nzero: "deg R p \ 0" shows "p \ \\<^bsub>P\<^esub>" using deg_zero deg_p_nzero by auto lemma deg_add_eq: assumes c: "p \ carrier P" "q \ carrier P" assumes "deg R q \ deg R p" shows "deg R (p \\<^bsub>P\<^esub> q) = max (deg R p) (deg R q)" proof - let ?m = "max (deg R p) (deg R q)" from assms have "coeff P p ?m = \ \ coeff P q ?m \ \" by (metis deg_belowI lcoeff_nonzero[OF deg_nzero_nzero] linear max.absorb_iff2 max.absorb1) then have "coeff P (p \\<^bsub>P\<^esub> q) ?m \ \" using assms by auto then have "deg R (p \\<^bsub>P\<^esub> q) \ ?m" using assms by (blast intro: deg_belowI) with deg_add[OF c] show ?thesis by arith qed lemma deg_minus_eq: assumes "p \ carrier P" "q \ carrier P" "deg R q \ deg R p" shows "deg R (p \\<^bsub>P\<^esub> q) = max (deg R p) (deg R q)" using assms by (simp add: deg_add_eq a_minus_def) end context UP_cring begin lemma evalRR_add: assumes "p \ carrier P" "q \ carrier P" assumes x: "x \ carrier R" shows "eval R R id x (p \\<^bsub>P\<^esub> q) = eval R R id x p \ eval R R id x q" proof - interpret UP_pre_univ_prop R R id by unfold_locales simp interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x]) show ?thesis using assms by simp qed lemma evalRR_sub: assumes "p \ carrier P" "q \ carrier P" assumes x: "x \ carrier R" shows "eval R R id x (p \\<^bsub>P\<^esub> q) = eval R R id x p \ eval R R id x q" proof - interpret UP_pre_univ_prop R R id by unfold_locales simp interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x]) show ?thesis using assms by simp qed lemma evalRR_mult: assumes "p \ carrier P" "q \ carrier P" assumes x: "x \ carrier R" shows "eval R R id x (p \\<^bsub>P\<^esub> q) = eval R R id x p \ eval R R id x q" proof - interpret UP_pre_univ_prop R R id by unfold_locales simp interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x]) show ?thesis using assms by simp qed lemma evalRR_monom: assumes a: "a \ carrier R" and x: "x \ carrier R" shows "eval R R id x (monom P a d) = a \ x [^] d" proof - interpret UP_pre_univ_prop R R id by unfold_locales simp show ?thesis using assms by (simp add: eval_monom) qed lemma evalRR_one: assumes x: "x \ carrier R" shows "eval R R id x \\<^bsub>P\<^esub> = \" proof - interpret UP_pre_univ_prop R R id by unfold_locales simp interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x]) show ?thesis using assms by simp qed lemma carrier_evalRR: assumes x: "x \ carrier R" and "p \ carrier P" shows "eval R R id x p \ carrier R" proof - interpret UP_pre_univ_prop R R id by unfold_locales simp interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x]) show ?thesis using assms by simp qed lemmas evalRR_simps = evalRR_add evalRR_sub evalRR_mult evalRR_monom evalRR_one carrier_evalRR end section \Properties of the Euler \\\-function\ text_raw \\label{sec:euler-phi}\ text\ In this section we prove that for every positive natural number the equation $\sum_{d | n}^n \varphi(d) = n$ holds. \ lemma dvd_div_ge_1: fixes a b :: nat assumes "a \ 1" "b dvd a" shows "a div b \ 1" proof - from \b dvd a\ obtain c where "a = b * c" .. with \a \ 1\ show ?thesis by simp qed lemma dvd_nat_bounds: fixes n p :: nat assumes "p > 0" "n dvd p" shows "n > 0 \ n \ p" using assms by (simp add: dvd_pos_nat dvd_imp_le) (* TODO FIXME: This is the "totient" function from HOL-Number_Theory, but since part of HOL-Number_Theory depends on HOL-Algebra.Multiplicative_Group, there would be a cyclic dependency. *) definition phi' :: "nat => nat" where "phi' m = card {x. 1 \ x \ x \ m \ coprime x m}" notation (latex output) phi' ("\ _") lemma phi'_nonzero: assumes "m > 0" shows "phi' m > 0" proof - have "1 \ {x. 1 \ x \ x \ m \ coprime x m}" using assms by simp hence "card {x. 1 \ x \ x \ m \ coprime x m} > 0" by (auto simp: card_gt_0_iff) thus ?thesis unfolding phi'_def by simp qed lemma dvd_div_eq_1: fixes a b c :: nat assumes "c dvd a" "c dvd b" "a div c = b div c" shows "a = b" using assms dvd_mult_div_cancel[OF \c dvd a\] dvd_mult_div_cancel[OF \c dvd b\] by presburger lemma dvd_div_eq_2: fixes a b c :: nat assumes "c>0" "a dvd c" "b dvd c" "c div a = c div b" shows "a = b" proof - have "a > 0" "a \ c" using dvd_nat_bounds[OF assms(1-2)] by auto have "a*(c div a) = c" using assms dvd_mult_div_cancel by fastforce also have "\ = b*(c div a)" using assms dvd_mult_div_cancel by fastforce finally show "a = b" using \c>0\ dvd_div_ge_1[OF _ \a dvd c\] by fastforce qed lemma div_mult_mono: fixes a b c :: nat assumes "a > 0" "a\d" shows "a * b div d \ b" proof - have "a*b div d \ b*a div a" using assms div_le_mono2 mult.commute[of a b] by presburger thus ?thesis using assms by force qed text\ We arrive at the main result of this section: For every positive natural number the equation $\sum_{d | n}^n \varphi(d) = n$ holds. The outline of the proof for this lemma is as follows: We count the $n$ fractions $1/n$, $\ldots$, $(n-1)/n$, $n/n$. We analyze the reduced form $a/d = m/n$ for any of those fractions. We want to know how many fractions $m/n$ have the reduced form denominator $d$. The condition $1 \leq m \leq n$ is equivalent to the condition $1 \leq a \leq d$. Therefore we want to know how many $a$ with $1 \leq a \leq d$ exist, s.t. \<^term>\gcd a d = 1\. This number is exactly \<^term>\phi' d\. Finally, by counting the fractions $m/n$ according to their reduced form denominator, we get: @{term [display] "(\d | d dvd n . phi' d) = n"}. To formalize this proof in Isabelle, we analyze for an arbitrary divisor $d$ of $n$ \begin{itemize} \item the set of reduced form numerators \<^term>\{a. (1::nat) \ a \ a \ d \ coprime a d}\ \item the set of numerators $m$, for which $m/n$ has the reduced form denominator $d$, i.e. the set \<^term>\{m \ {1::nat .. n}. n div gcd m n = d}\ \end{itemize} We show that \<^term>\\a. a*n div d\ with the inverse \<^term>\\a. a div gcd a n\ is a bijection between theses sets, thus yielding the equality @{term [display] "phi' d = card {m \ {1 .. n}. n div gcd m n = d}"} This gives us @{term [display] "(\d | d dvd n . phi' d) = card (\d \ {d. d dvd n}. {m \ {1 .. n}. n div gcd m n = d})"} and by showing \<^term>\(\d \ {d. d dvd n}. {m \ {1::nat .. n}. n div gcd m n = d}) \ {1 .. n}\ (this is our counting argument) the thesis follows. \ lemma sum_phi'_factors: fixes n :: nat assumes "n > 0" shows "(\d | d dvd n. phi' d) = n" proof - { fix d assume "d dvd n" then obtain q where q: "n = d * q" .. have "card {a. 1 \ a \ a \ d \ coprime a d} = card {m \ {1 .. n}. n div gcd m n = d}" (is "card ?RF = card ?F") proof (rule card_bij_eq) { fix a b assume "a * n div d = b * n div d" hence "a * (n div d) = b * (n div d)" using dvd_div_mult[OF \d dvd n\] by (fastforce simp add: mult.commute) hence "a = b" using dvd_div_ge_1[OF _ \d dvd n\] \n>0\ by (simp add: mult.commute nat_mult_eq_cancel1) } thus "inj_on (\a. a*n div d) ?RF" unfolding inj_on_def by blast { fix a assume a: "a\?RF" hence "a * (n div d) \ 1" using \n>0\ dvd_div_ge_1[OF _ \d dvd n\] by simp hence ge_1: "a * n div d \ 1" by (simp add: \d dvd n\ div_mult_swap) have le_n: "a * n div d \ n" using div_mult_mono a by simp have "gcd (a * n div d) n = n div d * gcd a d" by (simp add: gcd_mult_distrib_nat q ac_simps) hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp hence "a * n div d \ ?F" using ge_1 le_n by (fastforce simp add: \d dvd n\) } thus "(\a. a*n div d) ` ?RF \ ?F" by blast { fix m l assume A: "m \ ?F" "l \ ?F" "m div gcd m n = l div gcd l n" hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce hence "m = l" using dvd_div_eq_1[of "gcd m n" m l] A(3) by fastforce } thus "inj_on (\a. a div gcd a n) ?F" unfolding inj_on_def by blast { fix m assume "m \ ?F" hence "m div gcd m n \ ?RF" using dvd_div_ge_1 by (fastforce simp add: div_le_mono div_gcd_coprime) } thus "(\a. a div gcd a n) ` ?F \ ?RF" by blast qed force+ } hence phi'_eq: "\d. d dvd n \ phi' d = card {m \ {1 .. n}. n div gcd m n = d}" unfolding phi'_def by presburger have fin: "finite {d. d dvd n}" using dvd_nat_bounds[OF \n>0\] by force have "(\d | d dvd n. phi' d) = card (\d \ {d. d dvd n}. {m \ {1 .. n}. n div gcd m n = d})" using card_UN_disjoint[OF fin, of "(\d. {m \ {1 .. n}. n div gcd m n = d})"] phi'_eq by fastforce also have "(\d \ {d. d dvd n}. {m \ {1 .. n}. n div gcd m n = d}) = {1 .. n}" (is "?L = ?R") proof show "?L \ ?R" proof fix m assume m: "m \ ?R" thus "m \ ?L" using dvd_triv_right[of "n div gcd m n" "gcd m n"] by simp qed qed fastforce finally show ?thesis by force qed + + section \Order of an Element of a Group\ text_raw \\label{sec:order-elem}\ context group begin definition (in group) ord :: "'a \ nat" where "ord x \ (@d. \n::nat. x [^] n = \ \ d dvd n)" lemma (in group) pow_eq_id: assumes "x \ carrier G" shows "x [^] n = \ \ (ord x) dvd n" proof (cases "\n::nat. pow G x n = one G \ n = 0") case True show ?thesis unfolding ord_def by (rule someI2 [where a=0]) (auto simp: True) next case False define N where "N \ LEAST n::nat. x [^] n = \ \ n > 0" have N: "x [^] N = \ \ N > 0" using False apply (simp add: N_def) by (metis (mono_tags, lifting) LeastI) have eq0: "n = 0" if "x [^] n = \" "n < N" for n using N_def not_less_Least that by fastforce show ?thesis unfolding ord_def proof (rule someI2 [where a = N], rule allI) fix n :: "nat" show "(x [^] n = \) \ (N dvd n)" proof (cases "n = 0") case False show ?thesis unfolding dvd_def proof safe assume 1: "x [^] n = \" have "x [^] n = x [^] (n mod N + N * (n div N))" by simp also have "\ = x [^] (n mod N) \ x [^] (N * (n div N))" by (simp add: assms nat_pow_mult) also have "\ = x [^] (n mod N)" by (metis N assms l_cancel_one nat_pow_closed nat_pow_one nat_pow_pow) finally have "x [^] (n mod N) = \" by (simp add: "1") then have "n mod N = 0" using N eq0 mod_less_divisor by blast then show "\k. n = N * k" by blast next fix k :: "nat" assume "n = N * k" with N show "x [^] (N * k) = \" by (metis assms nat_pow_one nat_pow_pow) qed qed simp qed blast qed lemma (in group) pow_ord_eq_1 [simp]: "x \ carrier G \ x [^] ord x = \" by (simp add: pow_eq_id) lemma (in group) int_pow_eq_id: assumes "x \ carrier G" shows "(pow G x i = one G \ int (ord x) dvd i)" proof (cases i rule: int_cases2) case (nonneg n) then show ?thesis by (simp add: int_pow_int pow_eq_id assms) next case (nonpos n) then have "x [^] i = inv (x [^] n)" by (simp add: assms int_pow_int int_pow_neg) then show ?thesis by (simp add: assms pow_eq_id nonpos) qed lemma (in group) int_pow_eq: "x \ carrier G \ (x [^] m = x [^] n) \ int (ord x) dvd (n - m)" apply (simp flip: int_pow_eq_id) by (metis int_pow_closed int_pow_diff inv_closed r_inv right_cancel) lemma (in group) ord_eq_0: "x \ carrier G \ (ord x = 0 \ (\n::nat. n \ 0 \ x [^] n \ \))" by (auto simp: pow_eq_id) lemma (in group) ord_unique: "x \ carrier G \ ord x = d \ (\n. pow G x n = one G \ d dvd n)" by (meson dvd_antisym dvd_refl pow_eq_id) lemma (in group) ord_eq_1: "x \ carrier G \ (ord x = 1 \ x = \)" by (metis pow_eq_id nat_dvd_1_iff_1 nat_pow_eone) lemma (in group) ord_id [simp]: "ord (one G) = 1" using ord_eq_1 by blast lemma (in group) ord_inv [simp]: "x \ carrier G \ ord (m_inv G x) = ord x" by (simp add: ord_unique pow_eq_id nat_pow_inv) lemma (in group) ord_pow: assumes "x \ carrier G" "k dvd ord x" "k \ 0" shows "ord (pow G x k) = ord x div k" proof - have "(x [^] k) [^] (ord x div k) = \" using assms by (simp add: nat_pow_pow) moreover have "ord x dvd k * ord (x [^] k)" by (metis assms(1) pow_ord_eq_1 pow_eq_id nat_pow_closed nat_pow_pow) ultimately show ?thesis by (metis assms div_dvd_div dvd_antisym dvd_triv_left pow_eq_id nat_pow_closed nonzero_mult_div_cancel_left) qed lemma (in group) ord_mul_divides: assumes eq: "x \ y = y \ x" and xy: "x \ carrier G" "y \ carrier G" shows "ord (x \ y) dvd (ord x * ord y)" apply (simp add: xy flip: pow_eq_id eq) by (metis dvd_triv_left dvd_triv_right eq pow_eq_id one_closed pow_mult_distrib r_one xy) lemma (in comm_group) abelian_ord_mul_divides: "\x \ carrier G; y \ carrier G\ \ ord (x \ y) dvd (ord x * ord y)" by (simp add: ord_mul_divides m_comm) lemma ord_inj: assumes a: "a \ carrier G" shows "inj_on (\ x . a [^] x) {0 .. ord a - 1}" proof - let ?M = "Max (ord ` carrier G)" have "finite {d \ {..?M}. a [^] d = \}" by auto have *: False if A: "x < y" "x \ {0 .. ord a - 1}" "y \ {0 .. ord a - 1}" "a [^] x = a [^] y" for x y proof - have "y - x < ord a" using that by auto moreover have "a [^] (y-x) = \" using a A by (simp add: pow_eq_div2) ultimately have "min (y - x) (ord a) = ord a" using A(1) a pow_eq_id by auto with \y - x < ord a\ show False by linarith qed show ?thesis unfolding inj_on_def by (metis nat_neq_iff *) qed lemma ord_inj': assumes a: "a \ carrier G" shows "inj_on (\ x . a [^] x) {1 .. ord a}" proof (rule inj_onI, rule ccontr) fix x y :: nat assume A: "x \ {1 .. ord a}" "y \ {1 .. ord a}" "a [^] x = a [^] y" "x\y" { assume "x < ord a" "y < ord a" hence False using ord_inj[OF assms] A unfolding inj_on_def by fastforce } moreover { assume "x = ord a" "y < ord a" hence "a [^] y = a [^] (0::nat)" using pow_ord_eq_1 A by (simp add: a) hence "y=0" using ord_inj[OF assms] \y < ord a\ unfolding inj_on_def by force hence False using A by fastforce } moreover { assume "y = ord a" "x < ord a" hence "a [^] x = a [^] (0::nat)" using pow_ord_eq_1 A by (simp add: a) hence "x=0" using ord_inj[OF assms] \x < ord a\ unfolding inj_on_def by force hence False using A by fastforce } ultimately show False using A by force qed lemma (in group) ord_ge_1: assumes finite: "finite (carrier G)" and a: "a \ carrier G" shows "ord a \ 1" proof - have "((\n::nat. a [^] n) ` {0<..}) \ carrier G" using a by blast then have "finite ((\n::nat. a [^] n) ` {0<..})" using finite_subset finite by auto then have "\ inj_on (\n::nat. a [^] n) {0<..}" using finite_imageD infinite_Ioi by blast then obtain i j::nat where "i \ j" "a [^] i = a [^] j" by (auto simp: inj_on_def) then have "\n::nat. n>0 \ a [^] n = \" by (metis a diffs0_imp_equal pow_eq_div2 neq0_conv) then have "ord a \ 0" by (simp add: ord_eq_0 [OF a]) then show ?thesis by simp qed lemma ord_elems: assumes "finite (carrier G)" "a \ carrier G" shows "{a[^]x | x. x \ (UNIV :: nat set)} = {a[^]x | x. x \ {0 .. ord a - 1}}" (is "?L = ?R") proof show "?R \ ?L" by blast { fix y assume "y \ ?L" then obtain x::nat where x: "y = a[^]x" by auto define r q where "r = x mod ord a" and "q = x div ord a" then have "x = q * ord a + r" by (simp add: div_mult_mod_eq) hence "y = (a[^]ord a)[^]q \ a[^]r" using x assms by (metis mult.commute nat_pow_mult nat_pow_pow) hence "y = a[^]r" using assms by (simp add: pow_ord_eq_1) have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def) hence "r \ {0 .. ord a - 1}" by (force simp: r_def) hence "y \ {a[^]x | x. x \ {0 .. ord a - 1}}" using \y=a[^]r\ by blast } thus "?L \ ?R" by auto qed +lemma (in group) + assumes "x \ carrier G" + shows finite_cyclic_subgroup: + "finite(carrier(subgroup_generated G {x})) \ (\n::nat. n \ 0 \ x [^] n = \)" (is "?fin \ ?nat1") + and infinite_cyclic_subgroup: + "infinite(carrier(subgroup_generated G {x})) \ (\m n::nat. x [^] m = x [^] n \ m = n)" (is "\ ?fin \ ?nateq") + and finite_cyclic_subgroup_int: + "finite(carrier(subgroup_generated G {x})) \ (\i::int. i \ 0 \ x [^] i = \)" (is "?fin \ ?int1") + and infinite_cyclic_subgroup_int: + "infinite(carrier(subgroup_generated G {x})) \ (\i j::int. x [^] i = x [^] j \ i = j)" (is "\ ?fin \ ?inteq") +proof - + have 1: "\ ?fin" if ?nateq + proof - + have "infinite (range (\n::nat. x [^] n))" + using that range_inj_infinite [of "(\n::nat. x [^] n)"] by (auto simp: inj_on_def) + moreover have "range (\n::nat. x [^] n) \ range (\i::int. x [^] i)" + apply clarify + by (metis assms group.int_pow_neg int_pow_closed int_pow_neg_int is_group local.inv_equality nat_pow_closed r_inv rangeI) + ultimately show ?thesis + using carrier_subgroup_generated_by_singleton [OF assms] finite_subset by auto + qed + have 2: "m = n" if mn: "x [^] m = x [^] n" and eq [rule_format]: "?inteq" for m n::nat + using eq [of "int m" "int n"] + by (simp add: int_pow_int mn) + have 3: ?nat1 if non: "\ ?inteq" + proof - + obtain i j::int where eq: "x [^] i = x [^] j" and "i \ j" + using non by auto + show ?thesis + proof (cases i j rule: linorder_cases) + case less + then have [simp]: "x [^] (j - i) = \" + by (simp add: eq assms int_pow_diff) + show ?thesis + using less by (rule_tac x="nat (j-i)" in exI) auto + next + case greater + then have [simp]: "x [^] (i - j) = \" + by (simp add: eq assms int_pow_diff) + then show ?thesis + using greater by (rule_tac x="nat (i-j)" in exI) auto + qed (use \i \ j\ in auto) + qed + have 4: "\i::int. (i \ 0) \ x [^] i = \" if "n \ 0" "x [^] n = \" for n::nat + apply (rule_tac x="int n" in exI) + by (simp add: int_pow_int that) + have 5: "finite (carrier (subgroup_generated G {x}))" if "i \ 0" and 1: "x [^] i = \" for i::int + proof - + obtain n::nat where n: "n > 0" "x [^] n = \" + using "1" "3" \i \ 0\ by fastforce + have "x [^] a \ ([^]) x ` {0.. {0.. ([^]) x ` {0.. ?nat1" "\ ?fin \ ?nateq" "?fin \ ?int1" "\ ?fin \ ?inteq" + using 1 2 3 4 5 by meson+ +qed + +lemma (in group) finite_cyclic_subgroup_order: + "x \ carrier G \ finite(carrier(subgroup_generated G {x})) \ ord x \ 0" + by (simp add: finite_cyclic_subgroup ord_eq_0) + +lemma (in group) infinite_cyclic_subgroup_order: + "x \ carrier G \ infinite (carrier(subgroup_generated G {x})) \ ord x = 0" + by (simp add: finite_cyclic_subgroup_order) + lemma generate_pow_on_finite_carrier: \<^marker>\contributor \Paulo Emílio de Vilhena\\ assumes "finite (carrier G)" and a: "a \ carrier G" shows "generate G { a } = { a [^] k | k. k \ (UNIV :: nat set) }" proof show "{ a [^] k | k. k \ (UNIV :: nat set) } \ generate G { a }" proof fix b assume "b \ { a [^] k | k. k \ (UNIV :: nat set) }" then obtain k :: nat where "b = a [^] k" by blast hence "b = a [^] (int k)" by (simp add: int_pow_int) thus "b \ generate G { a }" unfolding generate_pow[OF a] by blast qed next show "generate G { a } \ { a [^] k | k. k \ (UNIV :: nat set) }" proof fix b assume "b \ generate G { a }" then obtain k :: int where k: "b = a [^] k" unfolding generate_pow[OF a] by blast show "b \ { a [^] k | k. k \ (UNIV :: nat set) }" proof (cases "k < 0") assume "\ k < 0" hence "b = a [^] (nat k)" by (simp add: k) thus ?thesis by blast next assume "k < 0" hence b: "b = inv (a [^] (nat (- k)))" using k a by (auto simp: int_pow_neg) obtain m where m: "ord a * m \ nat (- k)" by (metis assms mult.left_neutral mult_le_mono1 ord_ge_1) hence "a [^] (ord a * m) = \" by (metis a nat_pow_one nat_pow_pow pow_ord_eq_1) then obtain k' :: nat where "(a [^] (nat (- k))) \ (a [^] k') = \" using m a nat_le_iff_add nat_pow_mult by auto hence "b = a [^] k'" using b a by (metis inv_unique' nat_pow_closed nat_pow_comm) thus "b \ { a [^] k | k. k \ (UNIV :: nat set) }" by blast qed qed qed -lemma generate_pow_card: \<^marker>\contributor \Paulo Emílio de Vilhena\\ - assumes "finite (carrier G)" and a: "a \ carrier G" - shows "ord a = card (generate G { a })" -proof - - have "generate G { a } = (([^]) a) ` {0..ord a - 1}" - using generate_pow_on_finite_carrier[OF assms] unfolding ord_elems[OF assms] by auto - thus ?thesis - using ord_inj[OF a] ord_ge_1[OF assms] by (simp add: card_image) +lemma ord_elems_inf_carrier: + assumes "a \ carrier G" "ord a \ 0" + shows "{a[^]x | x. x \ (UNIV :: nat set)} = {a[^]x | x. x \ {0 .. ord a - 1}}" (is "?L = ?R") +proof + show "?R \ ?L" by blast + { fix y assume "y \ ?L" + then obtain x::nat where x: "y = a[^]x" by auto + define r q where "r = x mod ord a" and "q = x div ord a" + then have "x = q * ord a + r" + by (simp add: div_mult_mod_eq) + hence "y = (a[^]ord a)[^]q \ a[^]r" + using x assms by (metis mult.commute nat_pow_mult nat_pow_pow) + hence "y = a[^]r" using assms by simp + have "r < ord a" using assms by (simp add: r_def) + hence "r \ {0 .. ord a - 1}" by (force simp: r_def) + hence "y \ {a[^]x | x. x \ {0 .. ord a - 1}}" using \y=a[^]r\ by blast + } + thus "?L \ ?R" by auto qed -lemma ord_dvd_group_order: - assumes "a \ carrier G" - shows "(ord a) dvd (order G)" -proof (cases "finite (carrier G)") +lemma generate_pow_nat: + assumes a: "a \ carrier G" and "ord a \ 0" + shows "generate G { a } = { a [^] k | k. k \ (UNIV :: nat set) }" +proof + show "{ a [^] k | k. k \ (UNIV :: nat set) } \ generate G { a }" + proof + fix b assume "b \ { a [^] k | k. k \ (UNIV :: nat set) }" + then obtain k :: nat where "b = a [^] k" by blast + hence "b = a [^] (int k)" + by (simp add: int_pow_int) + thus "b \ generate G { a }" + unfolding generate_pow[OF a] by blast + qed +next + show "generate G { a } \ { a [^] k | k. k \ (UNIV :: nat set) }" + proof + fix b assume "b \ generate G { a }" + then obtain k :: int where k: "b = a [^] k" + unfolding generate_pow[OF a] by blast + show "b \ { a [^] k | k. k \ (UNIV :: nat set) }" + proof (cases "k < 0") + assume "\ k < 0" + hence "b = a [^] (nat k)" + by (simp add: k) + thus ?thesis by blast + next + assume "k < 0" + hence b: "b = inv (a [^] (nat (- k)))" + using k a by (auto simp: int_pow_neg) + obtain m where m: "ord a * m \ nat (- k)" + by (metis assms(2) dvd_imp_le dvd_triv_right le_zero_eq mult_eq_0_iff not_gr_zero) + hence "a [^] (ord a * m) = \" + by (metis a nat_pow_one nat_pow_pow pow_ord_eq_1) + then obtain k' :: nat where "(a [^] (nat (- k))) \ (a [^] k') = \" + using m a nat_le_iff_add nat_pow_mult by auto + hence "b = a [^] k'" + using b a by (metis inv_unique' nat_pow_closed nat_pow_comm) + thus "b \ { a [^] k | k. k \ (UNIV :: nat set) }" by blast + qed + qed +qed + +lemma generate_pow_card: + assumes a: "a \ carrier G" + shows "ord a = card (generate G { a })" +proof (cases "ord a = 0") case True + then have "infinite (carrier (subgroup_generated G {a}))" + using infinite_cyclic_subgroup_order[OF a] by auto + then have "infinite (generate G {a})" + unfolding subgroup_generated_def + using a by simp then show ?thesis - using lagrange[OF generate_is_subgroup[of "{a}"]] assms - unfolding generate_pow_card[OF True assms] - by (metis dvd_triv_right empty_subsetI insert_subset) + using `ord a = 0` by auto next case False - then show ?thesis - using order_gt_0_iff_finite by auto + note finite_subgroup = this + then have "generate G { a } = (([^]) a) ` {0..ord a - 1}" + using generate_pow_nat ord_elems_inf_carrier a by auto + hence "card (generate G {a}) = card {0..ord a - 1}" + using ord_inj[OF a] card_image by metis + also have "... = ord a" using finite_subgroup by auto + finally show ?thesis.. qed +lemma (in group) cyclic_order_is_ord: + assumes "g \ carrier G" + shows "ord g = order (subgroup_generated G {g})" + unfolding order_def subgroup_generated_def + using assms generate_pow_card by simp + +lemma ord_dvd_group_order: + assumes "a \ carrier G" shows "(ord a) dvd (order G)" + using lagrange[OF generate_is_subgroup[of "{a}"]] assms + unfolding generate_pow_card[OF assms] + by (metis dvd_triv_right empty_subsetI insert_subset) + lemma (in group) pow_order_eq_1: assumes "a \ carrier G" shows "a [^] order G = \" using assms by (metis nat_pow_pow ord_dvd_group_order pow_ord_eq_1 dvdE nat_pow_one) lemma dvd_gcd: fixes a b :: nat obtains q where "a * (b div gcd a b) = b*q" proof have "a * (b div gcd a b) = (a div gcd a b) * b" by (simp add: div_mult_swap dvd_div_mult) also have "\ = b * (a div gcd a b)" by simp finally show "a * (b div gcd a b) = b * (a div gcd a b) " . qed lemma (in group) ord_le_group_order: assumes finite: "finite (carrier G)" and a: "a \ carrier G" shows "ord a \ order G" by (simp add: a dvd_imp_le local.finite ord_dvd_group_order order_gt_0_iff_finite) lemma (in group) ord_pow_gen: assumes "x \ carrier G" shows "ord (pow G x k) = (if k = 0 then 1 else ord x div gcd (ord x) k)" proof - have "ord (x [^] k) = ord x div gcd (ord x) k" if "0 < k" proof - have "(d dvd k * n) = (d div gcd (d) k dvd n)" for d n using that by (simp add: div_dvd_iff_mult gcd_mult_distrib_nat mult.commute) then show ?thesis using that by (auto simp add: assms ord_unique nat_pow_pow pow_eq_id) qed then show ?thesis by auto qed lemma (in group) assumes finite': "finite (carrier G)" "a \ carrier G" shows pow_ord_eq_ord_iff: "group.ord G (a [^] k) = ord a \ coprime k (ord a)" (is "?L \ ?R") using assms ord_ge_1 [OF assms] by (auto simp: div_eq_dividend_iff ord_pow_gen coprime_iff_gcd_eq_1 gcd.commute split: if_split_asm) lemma element_generates_subgroup: assumes finite[simp]: "finite (carrier G)" assumes a[simp]: "a \ carrier G" shows "subgroup {a [^] i | i. i \ {0 .. ord a - 1}} G" using generate_is_subgroup[of "{ a }"] assms(2) generate_pow_on_finite_carrier[OF assms] unfolding ord_elems[OF assms] by auto end section \Number of Roots of a Polynomial\ text_raw \\label{sec:number-roots}\ definition mult_of :: "('a, 'b) ring_scheme \ 'a monoid" where "mult_of R \ \ carrier = carrier R - {\\<^bsub>R\<^esub>}, mult = mult R, one = \\<^bsub>R\<^esub>\" lemma carrier_mult_of [simp]: "carrier (mult_of R) = carrier R - {\\<^bsub>R\<^esub>}" by (simp add: mult_of_def) lemma mult_mult_of [simp]: "mult (mult_of R) = mult R" by (simp add: mult_of_def) lemma nat_pow_mult_of: "([^]\<^bsub>mult_of R\<^esub>) = (([^]\<^bsub>R\<^esub>) :: _ \ nat \ _)" by (simp add: mult_of_def fun_eq_iff nat_pow_def) lemma one_mult_of [simp]: "\\<^bsub>mult_of R\<^esub> = \\<^bsub>R\<^esub>" by (simp add: mult_of_def) lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of context field begin lemma mult_of_is_Units: "mult_of R = units_of R" unfolding mult_of_def units_of_def using field_Units by auto lemma m_inv_mult_of: "\x. x \ carrier (mult_of R) \ m_inv (mult_of R) x = m_inv R x" using mult_of_is_Units units_of_inv unfolding units_of_def by simp lemma (in field) field_mult_group: "group (mult_of R)" proof (rule groupI) show "\y\carrier (mult_of R). y \\<^bsub>mult_of R\<^esub> x = \\<^bsub>mult_of R\<^esub>" if "x \ carrier (mult_of R)" for x using group.l_inv_ex mult_of_is_Units that units_group by fastforce qed (auto simp: m_assoc dest: integral) lemma finite_mult_of: "finite (carrier R) \ finite (carrier (mult_of R))" by simp lemma order_mult_of: "finite (carrier R) \ order (mult_of R) = order R - 1" unfolding order_def carrier_mult_of by (simp add: card.remove) end lemma (in monoid) Units_pow_closed : fixes d :: nat assumes "x \ Units G" shows "x [^] d \ Units G" by (metis assms group.is_monoid monoid.nat_pow_closed units_group units_of_carrier units_of_pow) lemma (in ring) r_right_minus_eq[simp]: assumes "a \ carrier R" "b \ carrier R" shows "a \ b = \ \ a = b" using assms by (metis a_minus_def add.inv_closed minus_equality r_neg) context UP_cring begin lemma is_UP_cring: "UP_cring R" by (unfold_locales) lemma is_UP_ring: shows "UP_ring R" by (unfold_locales) end context UP_domain begin lemma roots_bound: assumes f [simp]: "f \ carrier P" assumes f_not_zero: "f \ \\<^bsub>P\<^esub>" assumes finite: "finite (carrier R)" shows "finite {a \ carrier R . eval R R id a f = \} \ card {a \ carrier R . eval R R id a f = \} \ deg R f" using f f_not_zero proof (induction "deg R f" arbitrary: f) case 0 have "\x. eval R R id x f \ \" proof - fix x have "(\i\{..deg R f}. id (coeff P f i) \ x [^] i) \ \" using 0 lcoeff_nonzero_nonzero[where p = f] by simp thus "eval R R id x f \ \" using 0 unfolding eval_def P_def by simp qed then have *: "{a \ carrier R. eval R R (\a. a) a f = \} = {}" by (auto simp: id_def) show ?case by (simp add: *) next case (Suc x) show ?case proof (cases "\ a \ carrier R . eval R R id a f = \") case True then obtain a where a_carrier[simp]: "a \ carrier R" and a_root: "eval R R id a f = \" by blast have R_not_triv: "carrier R \ {\}" by (metis R.one_zeroI R.zero_not_one) obtain q where q: "(q \ carrier P)" and f: "f = (monom P \\<^bsub>R\<^esub> 1 \\<^bsub> P\<^esub> monom P a 0) \\<^bsub>P\<^esub> q \\<^bsub>P\<^esub> monom P (eval R R id a f) 0" using remainder_theorem[OF Suc.prems(1) a_carrier R_not_triv] by auto hence lin_fac: "f = (monom P \\<^bsub>R\<^esub> 1 \\<^bsub> P\<^esub> monom P a 0) \\<^bsub>P\<^esub> q" using q by (simp add: a_root) have deg: "deg R (monom P \\<^bsub>R\<^esub> 1 \\<^bsub> P\<^esub> monom P a 0) = 1" using a_carrier by (simp add: deg_minus_eq) hence mon_not_zero: "(monom P \\<^bsub>R\<^esub> 1 \\<^bsub> P\<^esub> monom P a 0) \ \\<^bsub>P\<^esub>" by (fastforce simp del: r_right_minus_eq) have q_not_zero: "q \ \\<^bsub>P\<^esub>" using Suc by (auto simp add : lin_fac) hence "deg R q = x" using Suc deg deg_mult[OF mon_not_zero q_not_zero _ q] by (simp add : lin_fac) hence q_IH: "finite {a \ carrier R . eval R R id a q = \} \ card {a \ carrier R . eval R R id a q = \} \ x" using Suc q q_not_zero by blast have subs: "{a \ carrier R . eval R R id a f = \} \ {a \ carrier R . eval R R id a q = \} \ {a}" (is "?L \ ?R \ {a}") using a_carrier \q \ _\ by (auto simp: evalRR_simps lin_fac R.integral_iff) have "{a \ carrier R . eval R R id a f = \} \ insert a {a \ carrier R . eval R R id a q = \}" using subs by auto hence "card {a \ carrier R . eval R R id a f = \} \ card (insert a {a \ carrier R . eval R R id a q = \})" using q_IH by (blast intro: card_mono) also have "\ \ deg R f" using q_IH \Suc x = _\ by (simp add: card_insert_if) finally show ?thesis using q_IH \Suc x = _\ using finite by force next case False hence "card {a \ carrier R. eval R R id a f = \} = 0" using finite by auto also have "\ \ deg R f" by simp finally show ?thesis using finite by auto qed qed end lemma (in domain) num_roots_le_deg : fixes p d :: nat assumes finite: "finite (carrier R)" assumes d_neq_zero: "d \ 0" shows "card {x \ carrier R. x [^] d = \} \ d" proof - let ?f = "monom (UP R) \\<^bsub>R\<^esub> d \\<^bsub> (UP R)\<^esub> monom (UP R) \\<^bsub>R\<^esub> 0" have one_in_carrier: "\ \ carrier R" by simp interpret R: UP_domain R "UP R" by (unfold_locales) have "deg R ?f = d" using d_neq_zero by (simp add: R.deg_minus_eq) hence f_not_zero: "?f \ \\<^bsub>UP R\<^esub>" using d_neq_zero by (auto simp add : R.deg_nzero_nzero) have roots_bound: "finite {a \ carrier R . eval R R id a ?f = \} \ card {a \ carrier R . eval R R id a ?f = \} \ deg R ?f" using finite by (intro R.roots_bound[OF _ f_not_zero]) simp have subs: "{x \ carrier R. x [^] d = \} \ {a \ carrier R . eval R R id a ?f = \}" by (auto simp: R.evalRR_simps) then have "card {x \ carrier R. x [^] d = \} \ card {a \ carrier R. eval R R id a ?f = \}" using finite by (simp add : card_mono) thus ?thesis using \deg R ?f = d\ roots_bound by linarith qed section \The Multiplicative Group of a Field\ text_raw \\label{sec:mult-group}\ text \ In this section we show that the multiplicative group of a finite field is generated by a single element, i.e. it is cyclic. The proof is inspired by the first proof given in the survey~@{cite "conrad-cyclicity"}. \ context field begin lemma num_elems_of_ord_eq_phi': assumes finite: "finite (carrier R)" and dvd: "d dvd order (mult_of R)" and exists: "\a\carrier (mult_of R). group.ord (mult_of R) a = d" shows "card {a \ carrier (mult_of R). group.ord (mult_of R) a = d} = phi' d" proof - note mult_of_simps[simp] have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of) interpret G:group "mult_of R" rewrites "([^]\<^bsub>mult_of R\<^esub>) = (([^]) :: _ \ nat \ _)" and "\\<^bsub>mult_of R\<^esub> = \" by (rule field_mult_group) simp_all from exists obtain a where a: "a \ carrier (mult_of R)" and ord_a: "group.ord (mult_of R) a = d" by (auto simp add: card_gt_0_iff) have set_eq1: "{a[^]n| n. n \ {1 .. d}} = {x \ carrier (mult_of R). x [^] d = \}" proof (rule card_seteq) show "finite {x \ carrier (mult_of R). x [^] d = \}" using finite by auto show "{a[^]n| n. n \ {1 ..d}} \ {x \ carrier (mult_of R). x[^]d = \}" proof fix x assume "x \ {a[^]n | n. n \ {1 .. d}}" then obtain n where n: "x = a[^]n \ n \ {1 .. d}" by auto have "x[^]d =(a[^]d)[^]n" using n a ord_a by (simp add:nat_pow_pow mult.commute) hence "x[^]d = \" using ord_a G.pow_ord_eq_1[OF a] by fastforce thus "x \ {x \ carrier (mult_of R). x[^]d = \}" using G.nat_pow_closed[OF a] n by blast qed show "card {x \ carrier (mult_of R). x [^] d = \} \ card {a[^]n | n. n \ {1 .. d}}" proof - have *: "{a[^]n | n. n \ {1 .. d }} = ((\ n. a[^]n) ` {1 .. d})" by auto have "0 < order (mult_of R)" unfolding order_mult_of[OF finite] using card_mono[OF finite, of "{\, \}"] by (simp add: order_def) have "card {x \ carrier (mult_of R). x [^] d = \} \ card {x \ carrier R. x [^] d = \}" using finite by (auto intro: card_mono) also have "\ \ d" using \0 < order (mult_of R)\ num_roots_le_deg[OF finite, of d] by (simp add : dvd_pos_nat[OF _ \d dvd order (mult_of R)\]) finally show ?thesis using G.ord_inj'[OF a] ord_a * by (simp add: card_image) qed qed have set_eq2: "{x \ carrier (mult_of R) . group.ord (mult_of R) x = d} = (\ n . a[^]n) ` {n \ {1 .. d}. group.ord (mult_of R) (a[^]n) = d}" (is "?L = ?R") proof { fix x assume x: "x \ (carrier (mult_of R)) \ group.ord (mult_of R) x = d" hence "x \ {x \ carrier (mult_of R). x [^] d = \}" by (simp add: G.pow_ord_eq_1[of x, symmetric]) then obtain n where n: "x = a[^]n \ n \ {1 .. d}" using set_eq1 by blast hence "x \ ?R" using x by fast } thus "?L \ ?R" by blast show "?R \ ?L" using a by (auto simp add: carrier_mult_of[symmetric] simp del: carrier_mult_of) qed have "inj_on (\ n . a[^]n) {n \ {1 .. d}. group.ord (mult_of R) (a[^]n) = d}" using G.ord_inj'[OF a, unfolded ord_a] unfolding inj_on_def by fast hence "card ((\n. a[^]n) ` {n \ {1 .. d}. group.ord (mult_of R) (a[^]n) = d}) = card {k \ {1 .. d}. group.ord (mult_of R) (a[^]k) = d}" using card_image by blast thus ?thesis using set_eq2 G.pow_ord_eq_ord_iff[OF finite' \a \ _\, unfolded ord_a] by (simp add: phi'_def) qed end theorem (in field) finite_field_mult_group_has_gen : assumes finite: "finite (carrier R)" shows "\ a \ carrier (mult_of R) . carrier (mult_of R) = {a[^]i | i::nat . i \ UNIV}" proof - note mult_of_simps[simp] have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of) interpret G: group "mult_of R" rewrites "([^]\<^bsub>mult_of R\<^esub>) = (([^]) :: _ \ nat \ _)" and "\\<^bsub>mult_of R\<^esub> = \" by (rule field_mult_group) (simp_all add: fun_eq_iff nat_pow_def) let ?N = "\ x . card {a \ carrier (mult_of R). group.ord (mult_of R) a = x}" have "0 < order R - 1" unfolding order_def using card_mono[OF finite, of "{\, \}"] by simp then have *: "0 < order (mult_of R)" using assms by (simp add: order_mult_of) have fin: "finite {d. d dvd order (mult_of R) }" using dvd_nat_bounds[OF *] by force have "(\d | d dvd order (mult_of R). ?N d) = card (UN d:{d . d dvd order (mult_of R) }. {a \ carrier (mult_of R). group.ord (mult_of R) a = d})" (is "_ = card ?U") using fin finite by (subst card_UN_disjoint) auto also have "?U = carrier (mult_of R)" proof { fix x assume x: "x \ carrier (mult_of R)" hence x': "x\carrier (mult_of R)" by simp then have "group.ord (mult_of R) x dvd order (mult_of R)" using G.ord_dvd_group_order by blast hence "x \ ?U" using dvd_nat_bounds[of "order (mult_of R)" "group.ord (mult_of R) x"] x by blast } thus "carrier (mult_of R) \ ?U" by blast qed auto also have "card ... = order (mult_of R)" using order_mult_of finite' by (simp add: order_def) finally have sum_Ns_eq: "(\d | d dvd order (mult_of R). ?N d) = order (mult_of R)" . { fix d assume d: "d dvd order (mult_of R)" have "card {a \ carrier (mult_of R). group.ord (mult_of R) a = d} \ phi' d" proof cases assume "card {a \ carrier (mult_of R). group.ord (mult_of R) a = d} = 0" thus ?thesis by presburger next assume "card {a \ carrier (mult_of R). group.ord (mult_of R) a = d} \ 0" hence "\a \ carrier (mult_of R). group.ord (mult_of R) a = d" by (auto simp: card_eq_0_iff) thus ?thesis using num_elems_of_ord_eq_phi'[OF finite d] by auto qed } hence all_le: "\i. i \ {d. d dvd order (mult_of R) } \ (\i. card {a \ carrier (mult_of R). group.ord (mult_of R) a = i}) i \ (\i. phi' i) i" by fast hence le: "(\i | i dvd order (mult_of R). ?N i) \ (\i | i dvd order (mult_of R). phi' i)" using sum_mono[of "{d . d dvd order (mult_of R)}" "\i. card {a \ carrier (mult_of R). group.ord (mult_of R) a = i}"] by presburger have "order (mult_of R) = (\d | d dvd order (mult_of R). phi' d)" using * by (simp add: sum_phi'_factors) hence eq: "(\i | i dvd order (mult_of R). ?N i) = (\i | i dvd order (mult_of R). phi' i)" using le sum_Ns_eq by presburger have "\i. i \ {d. d dvd order (mult_of R) } \ ?N i = (\i. phi' i) i" proof (rule ccontr) fix i assume i1: "i \ {d. d dvd order (mult_of R)}" and "?N i \ phi' i" hence "?N i = 0" using num_elems_of_ord_eq_phi'[OF finite, of i] by (auto simp: card_eq_0_iff) moreover have "0 < i" using * i1 by (simp add: dvd_nat_bounds[of "order (mult_of R)" i]) ultimately have "?N i < phi' i" using phi'_nonzero by presburger hence "(\i | i dvd order (mult_of R). ?N i) < (\i | i dvd order (mult_of R). phi' i)" using sum_strict_mono_ex1[OF fin, of "?N" "\ i . phi' i"] i1 all_le by auto thus False using eq by force qed hence "?N (order (mult_of R)) > 0" using * by (simp add: phi'_nonzero) then obtain a where a: "a \ carrier (mult_of R)" and a_ord: "group.ord (mult_of R) a = order (mult_of R)" by (auto simp add: card_gt_0_iff) hence set_eq: "{a[^]i | i::nat. i \ UNIV} = (\x. a[^]x) ` {0 .. group.ord (mult_of R) a - 1}" using G.ord_elems[OF finite'] by auto have card_eq: "card ((\x. a[^]x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 .. group.ord (mult_of R) a - 1}" by (intro card_image G.ord_inj finite' a) hence "card ((\ x . a[^]x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 ..order (mult_of R) - 1}" using assms by (simp add: card_eq a_ord) hence card_R_minus_1: "card {a[^]i | i::nat. i \ UNIV} = order (mult_of R)" using * by (subst set_eq) auto have **: "{a[^]i | i::nat. i \ UNIV} \ carrier (mult_of R)" using G.nat_pow_closed[OF a] by auto with _ have "carrier (mult_of R) = {a[^]i|i::nat. i \ UNIV}" by (rule card_seteq[symmetric]) (simp_all add: card_R_minus_1 finite order_def del: UNIV_I) thus ?thesis using a by blast qed end