diff --git a/CONTRIBUTORS b/CONTRIBUTORS --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -1,1027 +1,1030 @@ 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 -------------------------------------- +* January 2021: Jakub Kądziołka + Some lemmas for HOL-Computational_Algebra. + Contributions to Isabelle2021 ----------------------------- * January 2021: Manuel Eberl Characteristic of a semiring. * January 2021: Manuel Eberl Algebraic integers in HOL-Computational_Algebra. * December 2020: Stepan Holub Contributed lemmas for theory HOL.List. * December 2020: Martin Desharnais Zipperposition 2.0 as external prover for Sledgehammer. * December 2020: Walter Guttmann Extension of session HOL-Hoare with total correctness proof system. * November / December 2020: Makarius Wenzel Improved HTML presentation and PDF document preparation, using mostly Isabelle/Scala instead of Isabelle/ML. * November 2020: Stepan Holub Removed preconditions from lemma comm_append_are_replicate. * 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 Support veriT as external prover in Sledgehammer. * October 2020: Mathias Fleury Updated proof reconstruction for the SMT solver veriT in the smt method. * October 2020: Jasmin Blanchette, Martin Desharnais Support E prover 2.5 as external prover in Sledgehammer. * September 2020: Florian Haftmann Substantial reworking and modularization of Word library, with generic type conversions. * August 2020: Makarius Wenzel Finally enable PIDE protocol for batch-builds, with various consequences of handling session build databases, Isabelle/Scala within Isabelle/ML etc. * August 2020: Makarius Wenzel Improved monitoring of runtime statistics: ML GC progress and Java. * July 2020: Martin Desharnais Update to 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/Computational_Algebra/Factorial_Ring.thy b/src/HOL/Computational_Algebra/Factorial_Ring.thy --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy @@ -1,2134 +1,2239 @@ (* Title: HOL/Computational_Algebra/Factorial_Ring.thy Author: Manuel Eberl, TU Muenchen Author: Florian Haftmann, TU Muenchen *) section \Factorial (semi)rings\ theory Factorial_Ring imports Main "HOL-Library.Multiset" begin subsection \Irreducible and prime elements\ context comm_semiring_1 begin definition irreducible :: "'a \ bool" where "irreducible p \ p \ 0 \ \p dvd 1 \ (\a b. p = a * b \ a dvd 1 \ b dvd 1)" lemma not_irreducible_zero [simp]: "\irreducible 0" by (simp add: irreducible_def) lemma irreducible_not_unit: "irreducible p \ \p dvd 1" by (simp add: irreducible_def) lemma not_irreducible_one [simp]: "\irreducible 1" by (simp add: irreducible_def) lemma irreducibleI: "p \ 0 \ \p dvd 1 \ (\a b. p = a * b \ a dvd 1 \ b dvd 1) \ irreducible p" by (simp add: irreducible_def) lemma irreducibleD: "irreducible p \ p = a * b \ a dvd 1 \ b dvd 1" by (simp add: irreducible_def) lemma irreducible_mono: assumes irr: "irreducible b" and "a dvd b" "\a dvd 1" shows "irreducible a" proof (rule irreducibleI) fix c d assume "a = c * d" from assms obtain k where [simp]: "b = a * k" by auto from \a = c * d\ have "b = c * d * k" by simp hence "c dvd 1 \ (d * k) dvd 1" using irreducibleD[OF irr, of c "d * k"] by (auto simp: mult.assoc) thus "c dvd 1 \ d dvd 1" by auto qed (use assms in \auto simp: irreducible_def\) definition prime_elem :: "'a \ bool" where "prime_elem p \ p \ 0 \ \p dvd 1 \ (\a b. p dvd (a * b) \ p dvd a \ p dvd b)" lemma not_prime_elem_zero [simp]: "\prime_elem 0" by (simp add: prime_elem_def) lemma prime_elem_not_unit: "prime_elem p \ \p dvd 1" by (simp add: prime_elem_def) lemma prime_elemI: "p \ 0 \ \p dvd 1 \ (\a b. p dvd (a * b) \ p dvd a \ p dvd b) \ prime_elem p" by (simp add: prime_elem_def) lemma prime_elem_dvd_multD: "prime_elem p \ p dvd (a * b) \ p dvd a \ p dvd b" by (simp add: prime_elem_def) lemma prime_elem_dvd_mult_iff: "prime_elem p \ p dvd (a * b) \ p dvd a \ p dvd b" by (auto simp: prime_elem_def) lemma not_prime_elem_one [simp]: "\ prime_elem 1" by (auto dest: prime_elem_not_unit) lemma prime_elem_not_zeroI: assumes "prime_elem p" shows "p \ 0" using assms by (auto intro: ccontr) lemma prime_elem_dvd_power: "prime_elem p \ p dvd x ^ n \ p dvd x" by (induction n) (auto dest: prime_elem_dvd_multD intro: dvd_trans[of _ 1]) lemma prime_elem_dvd_power_iff: "prime_elem p \ n > 0 \ p dvd x ^ n \ p dvd x" by (auto dest: prime_elem_dvd_power intro: dvd_trans) lemma prime_elem_imp_nonzero [simp]: "ASSUMPTION (prime_elem x) \ x \ 0" unfolding ASSUMPTION_def by (rule prime_elem_not_zeroI) lemma prime_elem_imp_not_one [simp]: "ASSUMPTION (prime_elem x) \ x \ 1" unfolding ASSUMPTION_def by auto end lemma (in normalization_semidom) irreducible_cong: assumes "normalize a = normalize b" shows "irreducible a \ irreducible b" proof (cases "a = 0 \ a dvd 1") case True hence "\irreducible a" by (auto simp: irreducible_def) from True have "normalize a = 0 \ normalize a dvd 1" by auto also note assms finally have "b = 0 \ b dvd 1" by simp hence "\irreducible b" by (auto simp: irreducible_def) with \\irreducible a\ show ?thesis by simp next case False hence b: "b \ 0" "\is_unit b" using assms by (auto simp: is_unit_normalize[of b]) show ?thesis proof assume "irreducible a" thus "irreducible b" by (rule irreducible_mono) (use assms False b in \auto dest: associatedD2\) next assume "irreducible b" thus "irreducible a" by (rule irreducible_mono) (use assms False b in \auto dest: associatedD1\) qed qed lemma (in normalization_semidom) associatedE1: assumes "normalize a = normalize b" obtains u where "is_unit u" "a = u * b" proof (cases "a = 0") case [simp]: False from assms have [simp]: "b \ 0" by auto show ?thesis proof (rule that) show "is_unit (unit_factor a div unit_factor b)" by auto have "unit_factor a div unit_factor b * b = unit_factor a * (b div unit_factor b)" using \b \ 0\ unit_div_commute unit_div_mult_swap unit_factor_is_unit by metis also have "b div unit_factor b = normalize b" by simp finally show "a = unit_factor a div unit_factor b * b" by (metis assms unit_factor_mult_normalize) qed next case [simp]: True hence [simp]: "b = 0" using assms[symmetric] by auto show ?thesis by (intro that[of 1]) auto qed lemma (in normalization_semidom) associatedE2: assumes "normalize a = normalize b" obtains u where "is_unit u" "b = u * a" proof - from assms have "normalize b = normalize a" by simp then obtain u where "is_unit u" "b = u * a" by (elim associatedE1) thus ?thesis using that by blast qed (* TODO Move *) lemma (in normalization_semidom) normalize_power_normalize: "normalize (normalize x ^ n) = normalize (x ^ n)" proof (induction n) case (Suc n) have "normalize (normalize x ^ Suc n) = normalize (x * normalize (normalize x ^ n))" by simp also note Suc.IH finally show ?case by simp qed auto context algebraic_semidom begin lemma prime_elem_imp_irreducible: assumes "prime_elem p" shows "irreducible p" proof (rule irreducibleI) fix a b assume p_eq: "p = a * b" with assms have nz: "a \ 0" "b \ 0" by auto from p_eq have "p dvd a * b" by simp with \prime_elem p\ have "p dvd a \ p dvd b" by (rule prime_elem_dvd_multD) with \p = a * b\ have "a * b dvd 1 * b \ a * b dvd a * 1" by auto thus "a dvd 1 \ b dvd 1" by (simp only: dvd_times_left_cancel_iff[OF nz(1)] dvd_times_right_cancel_iff[OF nz(2)]) qed (insert assms, simp_all add: prime_elem_def) lemma (in algebraic_semidom) unit_imp_no_irreducible_divisors: assumes "is_unit x" "irreducible p" shows "\p dvd x" proof (rule notI) assume "p dvd x" with \is_unit x\ have "is_unit p" by (auto intro: dvd_trans) with \irreducible p\ show False by (simp add: irreducible_not_unit) qed lemma unit_imp_no_prime_divisors: assumes "is_unit x" "prime_elem p" shows "\p dvd x" using unit_imp_no_irreducible_divisors[OF assms(1) prime_elem_imp_irreducible[OF assms(2)]] . lemma prime_elem_mono: assumes "prime_elem p" "\q dvd 1" "q dvd p" shows "prime_elem q" proof - from \q dvd p\ obtain r where r: "p = q * r" by (elim dvdE) hence "p dvd q * r" by simp with \prime_elem p\ have "p dvd q \ p dvd r" by (rule prime_elem_dvd_multD) hence "p dvd q" proof assume "p dvd r" then obtain s where s: "r = p * s" by (elim dvdE) from r have "p * 1 = p * (q * s)" by (subst (asm) s) (simp add: mult_ac) with \prime_elem p\ have "q dvd 1" by (subst (asm) mult_cancel_left) auto with \\q dvd 1\ show ?thesis by contradiction qed show ?thesis proof (rule prime_elemI) fix a b assume "q dvd (a * b)" with \p dvd q\ have "p dvd (a * b)" by (rule dvd_trans) with \prime_elem p\ have "p dvd a \ p dvd b" by (rule prime_elem_dvd_multD) with \q dvd p\ show "q dvd a \ q dvd b" by (blast intro: dvd_trans) qed (insert assms, auto) qed lemma irreducibleD': assumes "irreducible a" "b dvd a" shows "a dvd b \ is_unit b" proof - from assms obtain c where c: "a = b * c" by (elim dvdE) from irreducibleD[OF assms(1) this] have "is_unit b \ is_unit c" . thus ?thesis by (auto simp: c mult_unit_dvd_iff) qed lemma irreducibleI': assumes "a \ 0" "\is_unit a" "\b. b dvd a \ a dvd b \ is_unit b" shows "irreducible a" proof (rule irreducibleI) fix b c assume a_eq: "a = b * c" hence "a dvd b \ is_unit b" by (intro assms) simp_all thus "is_unit b \ is_unit c" proof assume "a dvd b" hence "b * c dvd b * 1" by (simp add: a_eq) moreover from \a \ 0\ a_eq have "b \ 0" by auto ultimately show ?thesis by (subst (asm) dvd_times_left_cancel_iff) auto qed blast qed (simp_all add: assms(1,2)) lemma irreducible_altdef: "irreducible x \ x \ 0 \ \is_unit x \ (\b. b dvd x \ x dvd b \ is_unit b)" using irreducibleI'[of x] irreducibleD'[of x] irreducible_not_unit[of x] by auto lemma prime_elem_multD: assumes "prime_elem (a * b)" shows "is_unit a \ is_unit b" proof - from assms have "a \ 0" "b \ 0" by (auto dest!: prime_elem_not_zeroI) moreover from assms prime_elem_dvd_multD [of "a * b"] have "a * b dvd a \ a * b dvd b" by auto ultimately show ?thesis using dvd_times_left_cancel_iff [of a b 1] dvd_times_right_cancel_iff [of b a 1] by auto qed lemma prime_elemD2: assumes "prime_elem p" and "a dvd p" and "\ is_unit a" shows "p dvd a" proof - from \a dvd p\ obtain b where "p = a * b" .. with \prime_elem p\ prime_elem_multD \\ is_unit a\ have "is_unit b" by auto with \p = a * b\ show ?thesis by (auto simp add: mult_unit_dvd_iff) qed lemma prime_elem_dvd_prod_msetE: assumes "prime_elem p" assumes dvd: "p dvd prod_mset A" obtains a where "a \# A" and "p dvd a" proof - from dvd have "\a. a \# A \ p dvd a" proof (induct A) case empty then show ?case using \prime_elem p\ by (simp add: prime_elem_not_unit) next case (add a A) then have "p dvd a * prod_mset A" by simp with \prime_elem p\ consider (A) "p dvd prod_mset A" | (B) "p dvd a" by (blast dest: prime_elem_dvd_multD) then show ?case proof cases case B then show ?thesis by auto next case A with add.hyps obtain b where "b \# A" "p dvd b" by auto then show ?thesis by auto qed qed with that show thesis by blast qed context begin private lemma prime_elem_powerD: assumes "prime_elem (p ^ n)" shows "prime_elem p \ n = 1" proof (cases n) case (Suc m) note assms also from Suc have "p ^ n = p * p^m" by simp finally have "is_unit p \ is_unit (p^m)" by (rule prime_elem_multD) moreover from assms have "\is_unit p" by (simp add: prime_elem_def is_unit_power_iff) ultimately have "is_unit (p ^ m)" by simp with \\is_unit p\ have "m = 0" by (simp add: is_unit_power_iff) with Suc assms show ?thesis by simp qed (insert assms, simp_all) lemma prime_elem_power_iff: "prime_elem (p ^ n) \ prime_elem p \ n = 1" by (auto dest: prime_elem_powerD) end lemma irreducible_mult_unit_left: "is_unit a \ irreducible (a * p) \ irreducible p" by (auto simp: irreducible_altdef mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff dvd_mult_unit_iff) lemma prime_elem_mult_unit_left: "is_unit a \ prime_elem (a * p) \ prime_elem p" by (auto simp: prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff) lemma prime_elem_dvd_cases: assumes pk: "p*k dvd m*n" and p: "prime_elem p" shows "(\x. k dvd x*n \ m = p*x) \ (\y. k dvd m*y \ n = p*y)" proof - have "p dvd m*n" using dvd_mult_left pk by blast then consider "p dvd m" | "p dvd n" using p prime_elem_dvd_mult_iff by blast then show ?thesis proof cases case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) then have "\x. k dvd x * n \ m = p * x" using p pk by (auto simp: mult.assoc) then show ?thesis .. next case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel) with p pk have "\y. k dvd m*y \ n = p*y" by (metis dvd_mult_right dvd_times_left_cancel_iff mult.left_commute mult_zero_left) then show ?thesis .. qed qed lemma prime_elem_power_dvd_prod: assumes pc: "p^c dvd m*n" and p: "prime_elem p" shows "\a b. a+b = c \ p^a dvd m \ p^b dvd n" using pc proof (induct c arbitrary: m n) case 0 show ?case by simp next case (Suc c) consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y" using prime_elem_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force then show ?case proof cases case (1 x) with Suc.hyps[of x n] obtain a b where "a + b = c \ p ^ a dvd x \ p ^ b dvd n" by blast with 1 have "Suc a + b = Suc c \ p ^ Suc a dvd m \ p ^ b dvd n" by (auto intro: mult_dvd_mono) thus ?thesis by blast next case (2 y) with Suc.hyps[of m y] obtain a b where "a + b = c \ p ^ a dvd m \ p ^ b dvd y" by blast with 2 have "a + Suc b = Suc c \ p ^ a dvd m \ p ^ Suc b dvd n" by (auto intro: mult_dvd_mono) with Suc.hyps [of m y] show "\a b. a + b = Suc c \ p ^ a dvd m \ p ^ b dvd n" by blast qed qed lemma prime_elem_power_dvd_cases: assumes "p ^ c dvd m * n" and "a + b = Suc c" and "prime_elem p" shows "p ^ a dvd m \ p ^ b dvd n" proof - from assms obtain r s where "r + s = c \ p ^ r dvd m \ p ^ s dvd n" by (blast dest: prime_elem_power_dvd_prod) moreover with assms have "a \ r \ b \ s" by arith ultimately show ?thesis by (auto intro: power_le_dvd) qed lemma prime_elem_not_unit' [simp]: "ASSUMPTION (prime_elem x) \ \is_unit x" unfolding ASSUMPTION_def by (rule prime_elem_not_unit) lemma prime_elem_dvd_power_iff: assumes "prime_elem p" shows "p dvd a ^ n \ p dvd a \ n > 0" using assms by (induct n) (auto dest: prime_elem_not_unit prime_elem_dvd_multD) lemma prime_power_dvd_multD: assumes "prime_elem p" assumes "p ^ n dvd a * b" and "n > 0" and "\ p dvd a" shows "p ^ n dvd b" using \p ^ n dvd a * b\ and \n > 0\ proof (induct n arbitrary: b) case 0 then show ?case by simp next case (Suc n) show ?case proof (cases "n = 0") case True with Suc \prime_elem p\ \\ p dvd a\ show ?thesis by (simp add: prime_elem_dvd_mult_iff) next case False then have "n > 0" by simp from \prime_elem p\ have "p \ 0" by auto from Suc.prems have *: "p * p ^ n dvd a * b" by simp then have "p dvd a * b" by (rule dvd_mult_left) with Suc \prime_elem p\ \\ p dvd a\ have "p dvd b" by (simp add: prime_elem_dvd_mult_iff) moreover define c where "c = b div p" ultimately have b: "b = p * c" by simp with * have "p * p ^ n dvd p * (a * c)" by (simp add: ac_simps) with \p \ 0\ have "p ^ n dvd a * c" by simp with Suc.hyps \n > 0\ have "p ^ n dvd c" by blast with \p \ 0\ show ?thesis by (simp add: b) qed qed end subsection \Generalized primes: normalized prime elements\ context normalization_semidom begin lemma irreducible_normalized_divisors: assumes "irreducible x" "y dvd x" "normalize y = y" shows "y = 1 \ y = normalize x" proof - from assms have "is_unit y \ x dvd y" by (auto simp: irreducible_altdef) thus ?thesis proof (elim disjE) assume "is_unit y" hence "normalize y = 1" by (simp add: is_unit_normalize) with assms show ?thesis by simp next assume "x dvd y" with \y dvd x\ have "normalize y = normalize x" by (rule associatedI) with assms show ?thesis by simp qed qed lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x" using irreducible_mult_unit_left[of "1 div unit_factor x" x] by (cases "x = 0") (simp_all add: unit_div_commute) lemma prime_elem_normalize_iff [simp]: "prime_elem (normalize x) = prime_elem x" using prime_elem_mult_unit_left[of "1 div unit_factor x" x] by (cases "x = 0") (simp_all add: unit_div_commute) lemma prime_elem_associated: assumes "prime_elem p" and "prime_elem q" and "q dvd p" shows "normalize q = normalize p" using \q dvd p\ proof (rule associatedI) from \prime_elem q\ have "\ is_unit q" by (auto simp add: prime_elem_not_unit) with \prime_elem p\ \q dvd p\ show "p dvd q" by (blast intro: prime_elemD2) qed definition prime :: "'a \ bool" where "prime p \ prime_elem p \ normalize p = p" lemma not_prime_0 [simp]: "\prime 0" by (simp add: prime_def) lemma not_prime_unit: "is_unit x \ \prime x" using prime_elem_not_unit[of x] by (auto simp add: prime_def) lemma not_prime_1 [simp]: "\prime 1" by (simp add: not_prime_unit) lemma primeI: "prime_elem x \ normalize x = x \ prime x" by (simp add: prime_def) lemma prime_imp_prime_elem [dest]: "prime p \ prime_elem p" by (simp add: prime_def) lemma normalize_prime: "prime p \ normalize p = p" by (simp add: prime_def) lemma prime_normalize_iff [simp]: "prime (normalize p) \ prime_elem p" by (auto simp add: prime_def) lemma prime_power_iff: "prime (p ^ n) \ prime p \ n = 1" by (auto simp: prime_def prime_elem_power_iff) lemma prime_imp_nonzero [simp]: "ASSUMPTION (prime x) \ x \ 0" unfolding ASSUMPTION_def prime_def by auto lemma prime_imp_not_one [simp]: "ASSUMPTION (prime x) \ x \ 1" unfolding ASSUMPTION_def by auto lemma prime_not_unit' [simp]: "ASSUMPTION (prime x) \ \is_unit x" unfolding ASSUMPTION_def prime_def by auto lemma prime_normalize' [simp]: "ASSUMPTION (prime x) \ normalize x = x" unfolding ASSUMPTION_def prime_def by simp lemma unit_factor_prime: "prime x \ unit_factor x = 1" using unit_factor_normalize[of x] unfolding prime_def by auto lemma unit_factor_prime' [simp]: "ASSUMPTION (prime x) \ unit_factor x = 1" unfolding ASSUMPTION_def by (rule unit_factor_prime) lemma prime_imp_prime_elem' [simp]: "ASSUMPTION (prime x) \ prime_elem x" by (simp add: prime_def ASSUMPTION_def) lemma prime_dvd_multD: "prime p \ p dvd a * b \ p dvd a \ p dvd b" by (intro prime_elem_dvd_multD) simp_all lemma prime_dvd_mult_iff: "prime p \ p dvd a * b \ p dvd a \ p dvd b" by (auto dest: prime_dvd_multD) lemma prime_dvd_power: "prime p \ p dvd x ^ n \ p dvd x" by (auto dest!: prime_elem_dvd_power simp: prime_def) lemma prime_dvd_power_iff: "prime p \ n > 0 \ p dvd x ^ n \ p dvd x" by (subst prime_elem_dvd_power_iff) simp_all lemma prime_dvd_prod_mset_iff: "prime p \ p dvd prod_mset A \ (\x. x \# A \ p dvd x)" by (induction A) (simp_all add: prime_elem_dvd_mult_iff prime_imp_prime_elem, blast+) lemma prime_dvd_prod_iff: "finite A \ prime p \ p dvd prod f A \ (\x\A. p dvd f x)" by (auto simp: prime_dvd_prod_mset_iff prod_unfold_prod_mset) lemma primes_dvd_imp_eq: assumes "prime p" "prime q" "p dvd q" shows "p = q" proof - from assms have "irreducible q" by (simp add: prime_elem_imp_irreducible prime_def) from irreducibleD'[OF this \p dvd q\] assms have "q dvd p" by simp with \p dvd q\ have "normalize p = normalize q" by (rule associatedI) with assms show "p = q" by simp qed lemma prime_dvd_prod_mset_primes_iff: assumes "prime p" "\q. q \# A \ prime q" shows "p dvd prod_mset A \ p \# A" proof - from assms(1) have "p dvd prod_mset A \ (\x. x \# A \ p dvd x)" by (rule prime_dvd_prod_mset_iff) also from assms have "\ \ p \# A" by (auto dest: primes_dvd_imp_eq) finally show ?thesis . qed lemma prod_mset_primes_dvd_imp_subset: assumes "prod_mset A dvd prod_mset B" "\p. p \# A \ prime p" "\p. p \# B \ prime p" shows "A \# B" using assms proof (induction A arbitrary: B) case empty thus ?case by simp next case (add p A B) hence p: "prime p" by simp define B' where "B' = B - {#p#}" from add.prems have "p dvd prod_mset B" by (simp add: dvd_mult_left) with add.prems have "p \# B" by (subst (asm) (2) prime_dvd_prod_mset_primes_iff) simp_all hence B: "B = B' + {#p#}" by (simp add: B'_def) from add.prems p have "A \# B'" by (intro add.IH) (simp_all add: B) thus ?case by (simp add: B) qed lemma prod_mset_dvd_prod_mset_primes_iff: assumes "\x. x \# A \ prime x" "\x. x \# B \ prime x" shows "prod_mset A dvd prod_mset B \ A \# B" using assms by (auto intro: prod_mset_subset_imp_dvd prod_mset_primes_dvd_imp_subset) lemma is_unit_prod_mset_primes_iff: assumes "\x. x \# A \ prime x" shows "is_unit (prod_mset A) \ A = {#}" by (auto simp add: is_unit_prod_mset_iff) (meson all_not_in_conv assms not_prime_unit set_mset_eq_empty_iff) lemma prod_mset_primes_irreducible_imp_prime: assumes irred: "irreducible (prod_mset A)" assumes A: "\x. x \# A \ prime x" assumes B: "\x. x \# B \ prime x" assumes C: "\x. x \# C \ prime x" assumes dvd: "prod_mset A dvd prod_mset B * prod_mset C" shows "prod_mset A dvd prod_mset B \ prod_mset A dvd prod_mset C" proof - from dvd have "prod_mset A dvd prod_mset (B + C)" by simp with A B C have subset: "A \# B + C" by (subst (asm) prod_mset_dvd_prod_mset_primes_iff) auto define A1 and A2 where "A1 = A \# B" and "A2 = A - A1" have "A = A1 + A2" unfolding A1_def A2_def by (rule sym, intro subset_mset.add_diff_inverse) simp_all from subset have "A1 \# B" "A2 \# C" by (auto simp: A1_def A2_def Multiset.subset_eq_diff_conv Multiset.union_commute) from \A = A1 + A2\ have "prod_mset A = prod_mset A1 * prod_mset A2" by simp from irred and this have "is_unit (prod_mset A1) \ is_unit (prod_mset A2)" by (rule irreducibleD) with A have "A1 = {#} \ A2 = {#}" unfolding A1_def A2_def by (subst (asm) (1 2) is_unit_prod_mset_primes_iff) (auto dest: Multiset.in_diffD) with dvd \A = A1 + A2\ \A1 \# B\ \A2 \# C\ show ?thesis by (auto intro: prod_mset_subset_imp_dvd) qed lemma prod_mset_primes_finite_divisor_powers: assumes A: "\x. x \# A \ prime x" assumes B: "\x. x \# B \ prime x" assumes "A \ {#}" shows "finite {n. prod_mset A ^ n dvd prod_mset B}" proof - from \A \ {#}\ obtain x where x: "x \# A" by blast define m where "m = count B x" have "{n. prod_mset A ^ n dvd prod_mset B} \ {..m}" proof safe fix n assume dvd: "prod_mset A ^ n dvd prod_mset B" from x have "x ^ n dvd prod_mset A ^ n" by (intro dvd_power_same dvd_prod_mset) also note dvd also have "x ^ n = prod_mset (replicate_mset n x)" by simp finally have "replicate_mset n x \# B" by (rule prod_mset_primes_dvd_imp_subset) (insert A B x, simp_all split: if_splits) thus "n \ m" by (simp add: count_le_replicate_mset_subset_eq m_def) qed moreover have "finite {..m}" by simp ultimately show ?thesis by (rule finite_subset) qed end subsection \In a semiring with GCD, each irreducible element is a prime element\ context semiring_gcd begin lemma irreducible_imp_prime_elem_gcd: assumes "irreducible x" shows "prime_elem x" proof (rule prime_elemI) fix a b assume "x dvd a * b" from dvd_productE[OF this] obtain y z where yz: "x = y * z" "y dvd a" "z dvd b" . from \irreducible x\ and \x = y * z\ have "is_unit y \ is_unit z" by (rule irreducibleD) with yz show "x dvd a \ x dvd b" by (auto simp: mult_unit_dvd_iff mult_unit_dvd_iff') qed (insert assms, auto simp: irreducible_not_unit) lemma prime_elem_imp_coprime: assumes "prime_elem p" "\p dvd n" shows "coprime p n" proof (rule coprimeI) fix d assume "d dvd p" "d dvd n" show "is_unit d" proof (rule ccontr) assume "\is_unit d" from \prime_elem p\ and \d dvd p\ and this have "p dvd d" by (rule prime_elemD2) from this and \d dvd n\ have "p dvd n" by (rule dvd_trans) with \\p dvd n\ show False by contradiction qed qed lemma prime_imp_coprime: assumes "prime p" "\p dvd n" shows "coprime p n" using assms by (simp add: prime_elem_imp_coprime) lemma prime_elem_imp_power_coprime: "prime_elem p \ \ p dvd a \ coprime a (p ^ m)" by (cases "m > 0") (auto dest: prime_elem_imp_coprime simp add: ac_simps) lemma prime_imp_power_coprime: "prime p \ \ p dvd a \ coprime a (p ^ m)" by (rule prime_elem_imp_power_coprime) simp_all lemma prime_elem_divprod_pow: assumes p: "prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b" shows "p^n dvd a \ p^n dvd b" using assms proof - from p have "\ is_unit p" by simp with ab p have "\ p dvd a \ \ p dvd b" using not_coprimeI by blast with p have "coprime (p ^ n) a \ coprime (p ^ n) b" by (auto dest: prime_elem_imp_power_coprime simp add: ac_simps) with pab show ?thesis by (auto simp add: coprime_dvd_mult_left_iff coprime_dvd_mult_right_iff) qed lemma primes_coprime: "prime p \ prime q \ p \ q \ coprime p q" using prime_imp_coprime primes_dvd_imp_eq by blast end subsection \Factorial semirings: algebraic structures with unique prime factorizations\ class factorial_semiring = normalization_semidom + assumes prime_factorization_exists: "x \ 0 \ \A. (\x. x \# A \ prime_elem x) \ normalize (prod_mset A) = normalize x" text \Alternative characterization\ lemma (in normalization_semidom) factorial_semiring_altI_aux: assumes finite_divisors: "\x. x \ 0 \ finite {y. y dvd x \ normalize y = y}" assumes irreducible_imp_prime_elem: "\x. irreducible x \ prime_elem x" assumes "x \ 0" shows "\A. (\x. x \# A \ prime_elem x) \ normalize (prod_mset A) = normalize x" using \x \ 0\ proof (induction "card {b. b dvd x \ normalize b = b}" arbitrary: x rule: less_induct) case (less a) let ?fctrs = "\a. {b. b dvd a \ normalize b = b}" show ?case proof (cases "is_unit a") case True thus ?thesis by (intro exI[of _ "{#}"]) (auto simp: is_unit_normalize) next case False show ?thesis proof (cases "\b. b dvd a \ \is_unit b \ \a dvd b") case False with \\is_unit a\ less.prems have "irreducible a" by (auto simp: irreducible_altdef) hence "prime_elem a" by (rule irreducible_imp_prime_elem) thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto next case True then guess b by (elim exE conjE) note b = this from b have "?fctrs b \ ?fctrs a" by (auto intro: dvd_trans) moreover from b have "normalize a \ ?fctrs b" "normalize a \ ?fctrs a" by simp_all hence "?fctrs b \ ?fctrs a" by blast ultimately have "?fctrs b \ ?fctrs a" by (subst subset_not_subset_eq) blast with finite_divisors[OF \a \ 0\] have "card (?fctrs b) < card (?fctrs a)" by (rule psubset_card_mono) moreover from \a \ 0\ b have "b \ 0" by auto ultimately have "\A. (\x. x \# A \ prime_elem x) \ normalize (prod_mset A) = normalize b" by (intro less) auto then guess A .. note A = this define c where "c = a div b" from b have c: "a = b * c" by (simp add: c_def) from less.prems c have "c \ 0" by auto from b c have "?fctrs c \ ?fctrs a" by (auto intro: dvd_trans) moreover have "normalize a \ ?fctrs c" proof safe assume "normalize a dvd c" hence "b * c dvd 1 * c" by (simp add: c) hence "b dvd 1" by (subst (asm) dvd_times_right_cancel_iff) fact+ with b show False by simp qed with \normalize a \ ?fctrs a\ have "?fctrs a \ ?fctrs c" by blast ultimately have "?fctrs c \ ?fctrs a" by (subst subset_not_subset_eq) blast with finite_divisors[OF \a \ 0\] have "card (?fctrs c) < card (?fctrs a)" by (rule psubset_card_mono) with \c \ 0\ have "\A. (\x. x \# A \ prime_elem x) \ normalize (prod_mset A) = normalize c" by (intro less) auto then guess B .. note B = this show ?thesis proof (rule exI[of _ "A + B"]; safe) have "normalize (prod_mset (A + B)) = normalize (normalize (prod_mset A) * normalize (prod_mset B))" by simp also have "\ = normalize (b * c)" by (simp only: A B) auto also have "b * c = a" using c by simp finally show "normalize (prod_mset (A + B)) = normalize a" . next qed (use A B in auto) qed qed qed lemma factorial_semiring_altI: assumes finite_divisors: "\x::'a. x \ 0 \ finite {y. y dvd x \ normalize y = y}" assumes irreducible_imp_prime: "\x::'a. irreducible x \ prime_elem x" shows "OFCLASS('a :: normalization_semidom, factorial_semiring_class)" by intro_classes (rule factorial_semiring_altI_aux[OF assms]) text \Properties\ context factorial_semiring begin lemma prime_factorization_exists': assumes "x \ 0" obtains A where "\x. x \# A \ prime x" "normalize (prod_mset A) = normalize x" proof - from prime_factorization_exists[OF assms] obtain A where A: "\x. x \# A \ prime_elem x" "normalize (prod_mset A) = normalize x" by blast define A' where "A' = image_mset normalize A" have "normalize (prod_mset A') = normalize (prod_mset A)" by (simp add: A'_def normalize_prod_mset_normalize) also note A(2) finally have "normalize (prod_mset A') = normalize x" by simp moreover from A(1) have "\x. x \# A' \ prime x" by (auto simp: prime_def A'_def) ultimately show ?thesis by (intro that[of A']) blast qed lemma irreducible_imp_prime_elem: assumes "irreducible x" shows "prime_elem x" proof (rule prime_elemI) fix a b assume dvd: "x dvd a * b" from assms have "x \ 0" by auto show "x dvd a \ x dvd b" proof (cases "a = 0 \ b = 0") case False hence "a \ 0" "b \ 0" by blast+ note nz = \x \ 0\ this from nz[THEN prime_factorization_exists'] guess A B C . note ABC = this have "irreducible (prod_mset A)" by (subst irreducible_cong[OF ABC(2)]) fact moreover have "normalize (prod_mset A) dvd normalize (normalize (prod_mset B) * normalize (prod_mset C))" unfolding ABC using dvd by simp hence "prod_mset A dvd prod_mset B * prod_mset C" unfolding normalize_mult_normalize_left normalize_mult_normalize_right by simp ultimately have "prod_mset A dvd prod_mset B \ prod_mset A dvd prod_mset C" by (intro prod_mset_primes_irreducible_imp_prime) (use ABC in auto) hence "normalize (prod_mset A) dvd normalize (prod_mset B) \ normalize (prod_mset A) dvd normalize (prod_mset C)" by simp thus ?thesis unfolding ABC by simp qed auto qed (insert assms, simp_all add: irreducible_def) lemma finite_divisor_powers: assumes "y \ 0" "\is_unit x" shows "finite {n. x ^ n dvd y}" proof (cases "x = 0") case True with assms have "{n. x ^ n dvd y} = {0}" by (auto simp: power_0_left) thus ?thesis by simp next case False note nz = this \y \ 0\ from nz[THEN prime_factorization_exists'] guess A B . note AB = this from AB assms have "A \ {#}" by (auto simp: normalize_1_iff) from AB(2,4) prod_mset_primes_finite_divisor_powers [of A B, OF AB(1,3) this] have "finite {n. prod_mset A ^ n dvd prod_mset B}" by simp also have "{n. prod_mset A ^ n dvd prod_mset B} = {n. normalize (normalize (prod_mset A) ^ n) dvd normalize (prod_mset B)}" unfolding normalize_power_normalize by simp also have "\ = {n. x ^ n dvd y}" unfolding AB unfolding normalize_power_normalize by simp finally show ?thesis . qed lemma finite_prime_divisors: assumes "x \ 0" shows "finite {p. prime p \ p dvd x}" proof - from prime_factorization_exists'[OF assms] guess A . note A = this have "{p. prime p \ p dvd x} \ set_mset A" proof safe fix p assume p: "prime p" and dvd: "p dvd x" from dvd have "p dvd normalize x" by simp also from A have "normalize x = normalize (prod_mset A)" by simp finally have "p dvd prod_mset A" by simp thus "p \# A" using p A by (subst (asm) prime_dvd_prod_mset_primes_iff) qed moreover have "finite (set_mset A)" by simp ultimately show ?thesis by (rule finite_subset) qed +lemma infinite_unit_divisor_powers: + assumes "y \ 0" + assumes "is_unit x" + shows "infinite {n. x^n dvd y}" +proof - + from `is_unit x` have "is_unit (x^n)" for n + using is_unit_power_iff by auto + hence "x^n dvd y" for n + by auto + hence "{n. x^n dvd y} = UNIV" + by auto + thus ?thesis + by auto +qed + +corollary is_unit_iff_infinite_divisor_powers: + assumes "y \ 0" + shows "is_unit x \ infinite {n. x^n dvd y}" + using infinite_unit_divisor_powers finite_divisor_powers assms by auto + lemma prime_elem_iff_irreducible: "prime_elem x \ irreducible x" by (blast intro: irreducible_imp_prime_elem prime_elem_imp_irreducible) lemma prime_divisor_exists: assumes "a \ 0" "\is_unit a" shows "\b. b dvd a \ prime b" proof - from prime_factorization_exists'[OF assms(1)] guess A . note A = this moreover from A and assms have "A \ {#}" by auto then obtain x where "x \# A" by blast with A(1) have *: "x dvd normalize (prod_mset A)" "prime x" by (auto simp: dvd_prod_mset) hence "x dvd a" unfolding A by simp with * show ?thesis by blast qed lemma prime_divisors_induct [case_names zero unit factor]: assumes "P 0" "\x. is_unit x \ P x" "\p x. prime p \ P x \ P (p * x)" shows "P x" proof (cases "x = 0") case False from prime_factorization_exists'[OF this] guess A . note A = this from A obtain u where u: "is_unit u" "x = u * prod_mset A" by (elim associatedE2) from A(1) have "P (u * prod_mset A)" proof (induction A) case (add p A) from add.prems have "prime p" by simp moreover from add.prems have "P (u * prod_mset A)" by (intro add.IH) simp_all ultimately have "P (p * (u * prod_mset A))" by (rule assms(3)) thus ?case by (simp add: mult_ac) qed (simp_all add: assms False u) with A u show ?thesis by simp qed (simp_all add: assms(1)) lemma no_prime_divisors_imp_unit: assumes "a \ 0" "\b. b dvd a \ normalize b = b \ \ prime_elem b" shows "is_unit a" proof (rule ccontr) assume "\is_unit a" from prime_divisor_exists[OF assms(1) this] guess b by (elim exE conjE) with assms(2)[of b] show False by (simp add: prime_def) qed lemma prime_divisorE: assumes "a \ 0" and "\ is_unit a" obtains p where "prime p" and "p dvd a" using assms no_prime_divisors_imp_unit unfolding prime_def by blast definition multiplicity :: "'a \ 'a \ nat" where "multiplicity p x = (if finite {n. p ^ n dvd x} then Max {n. p ^ n dvd x} else 0)" lemma multiplicity_dvd: "p ^ multiplicity p x dvd x" proof (cases "finite {n. p ^ n dvd x}") case True hence "multiplicity p x = Max {n. p ^ n dvd x}" by (simp add: multiplicity_def) also have "\ \ {n. p ^ n dvd x}" by (rule Max_in) (auto intro!: True exI[of _ "0::nat"]) finally show ?thesis by simp qed (simp add: multiplicity_def) lemma multiplicity_dvd': "n \ multiplicity p x \ p ^ n dvd x" by (rule dvd_trans[OF le_imp_power_dvd multiplicity_dvd]) context fixes x p :: 'a assumes xp: "x \ 0" "\is_unit p" begin lemma multiplicity_eq_Max: "multiplicity p x = Max {n. p ^ n dvd x}" using finite_divisor_powers[OF xp] by (simp add: multiplicity_def) lemma multiplicity_geI: assumes "p ^ n dvd x" shows "multiplicity p x \ n" proof - from assms have "n \ Max {n. p ^ n dvd x}" by (intro Max_ge finite_divisor_powers xp) simp_all thus ?thesis by (subst multiplicity_eq_Max) qed lemma multiplicity_lessI: assumes "\p ^ n dvd x" shows "multiplicity p x < n" proof (rule ccontr) assume "\(n > multiplicity p x)" hence "p ^ n dvd x" by (intro multiplicity_dvd') simp with assms show False by contradiction qed lemma power_dvd_iff_le_multiplicity: "p ^ n dvd x \ n \ multiplicity p x" using multiplicity_geI[of n] multiplicity_lessI[of n] by (cases "p ^ n dvd x") auto lemma multiplicity_eq_zero_iff: shows "multiplicity p x = 0 \ \p dvd x" using power_dvd_iff_le_multiplicity[of 1] by auto lemma multiplicity_gt_zero_iff: shows "multiplicity p x > 0 \ p dvd x" using power_dvd_iff_le_multiplicity[of 1] by auto lemma multiplicity_decompose: "\p dvd (x div p ^ multiplicity p x)" proof assume *: "p dvd x div p ^ multiplicity p x" have "x = x div p ^ multiplicity p x * (p ^ multiplicity p x)" using multiplicity_dvd[of p x] by simp also from * have "x div p ^ multiplicity p x = (x div p ^ multiplicity p x div p) * p" by simp also have "x div p ^ multiplicity p x div p * p * p ^ multiplicity p x = x div p ^ multiplicity p x div p * p ^ Suc (multiplicity p x)" by (simp add: mult_assoc) also have "p ^ Suc (multiplicity p x) dvd \" by (rule dvd_triv_right) finally show False by (subst (asm) power_dvd_iff_le_multiplicity) simp qed lemma multiplicity_decompose': obtains y where "x = p ^ multiplicity p x * y" "\p dvd y" using that[of "x div p ^ multiplicity p x"] by (simp add: multiplicity_decompose multiplicity_dvd) end lemma multiplicity_zero [simp]: "multiplicity p 0 = 0" by (simp add: multiplicity_def) lemma prime_elem_multiplicity_eq_zero_iff: "prime_elem p \ x \ 0 \ multiplicity p x = 0 \ \p dvd x" by (rule multiplicity_eq_zero_iff) simp_all lemma prime_multiplicity_other: assumes "prime p" "prime q" "p \ q" shows "multiplicity p q = 0" using assms by (subst prime_elem_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq) lemma prime_multiplicity_gt_zero_iff: "prime_elem p \ x \ 0 \ multiplicity p x > 0 \ p dvd x" by (rule multiplicity_gt_zero_iff) simp_all lemma multiplicity_unit_left: "is_unit p \ multiplicity p x = 0" by (simp add: multiplicity_def is_unit_power_iff unit_imp_dvd) lemma multiplicity_unit_right: assumes "is_unit x" shows "multiplicity p x = 0" proof (cases "is_unit p \ x = 0") case False with multiplicity_lessI[of x p 1] this assms show ?thesis by (auto dest: dvd_unit_imp_unit) qed (auto simp: multiplicity_unit_left) lemma multiplicity_one [simp]: "multiplicity p 1 = 0" by (rule multiplicity_unit_right) simp_all lemma multiplicity_eqI: assumes "p ^ n dvd x" "\p ^ Suc n dvd x" shows "multiplicity p x = n" proof - consider "x = 0" | "is_unit p" | "x \ 0" "\is_unit p" by blast thus ?thesis proof cases assume xp: "x \ 0" "\is_unit p" from xp assms(1) have "multiplicity p x \ n" by (intro multiplicity_geI) moreover from assms(2) xp have "multiplicity p x < Suc n" by (intro multiplicity_lessI) ultimately show ?thesis by simp next assume "is_unit p" hence "is_unit (p ^ Suc n)" by (simp add: is_unit_power_iff del: power_Suc) hence "p ^ Suc n dvd x" by (rule unit_imp_dvd) with \\p ^ Suc n dvd x\ show ?thesis by contradiction qed (insert assms, simp_all) qed context fixes x p :: 'a assumes xp: "x \ 0" "\is_unit p" begin lemma multiplicity_times_same: assumes "p \ 0" shows "multiplicity p (p * x) = Suc (multiplicity p x)" proof (rule multiplicity_eqI) show "p ^ Suc (multiplicity p x) dvd p * x" by (auto intro!: mult_dvd_mono multiplicity_dvd) from xp assms show "\ p ^ Suc (Suc (multiplicity p x)) dvd p * x" using power_dvd_iff_le_multiplicity[OF xp, of "Suc (multiplicity p x)"] by simp qed end lemma multiplicity_same_power': "multiplicity p (p ^ n) = (if p = 0 \ is_unit p then 0 else n)" proof - consider "p = 0" | "is_unit p" |"p \ 0" "\is_unit p" by blast thus ?thesis proof cases assume "p \ 0" "\is_unit p" thus ?thesis by (induction n) (simp_all add: multiplicity_times_same) qed (simp_all add: power_0_left multiplicity_unit_left) qed lemma multiplicity_same_power: "p \ 0 \ \is_unit p \ multiplicity p (p ^ n) = n" by (simp add: multiplicity_same_power') lemma multiplicity_prime_elem_times_other: assumes "prime_elem p" "\p dvd q" shows "multiplicity p (q * x) = multiplicity p x" proof (cases "x = 0") case False show ?thesis proof (rule multiplicity_eqI) have "1 * p ^ multiplicity p x dvd q * x" by (intro mult_dvd_mono multiplicity_dvd) simp_all thus "p ^ multiplicity p x dvd q * x" by simp next define n where "n = multiplicity p x" from assms have "\is_unit p" by simp from multiplicity_decompose'[OF False this] guess y . note y = this [folded n_def] from y have "p ^ Suc n dvd q * x \ p ^ n * p dvd p ^ n * (q * y)" by (simp add: mult_ac) also from assms have "\ \ p dvd q * y" by simp also have "\ \ p dvd q \ p dvd y" by (rule prime_elem_dvd_mult_iff) fact+ also from assms y have "\ \ False" by simp finally show "\(p ^ Suc n dvd q * x)" by blast qed qed simp_all lemma multiplicity_self: assumes "p \ 0" "\is_unit p" shows "multiplicity p p = 1" proof - from assms have "multiplicity p p = Max {n. p ^ n dvd p}" by (simp add: multiplicity_eq_Max) also from assms have "p ^ n dvd p \ n \ 1" for n using dvd_power_iff[of p n 1] by auto hence "{n. p ^ n dvd p} = {..1}" by auto also have "\ = {0,1}" by auto finally show ?thesis by simp qed lemma multiplicity_times_unit_left: assumes "is_unit c" shows "multiplicity (c * p) x = multiplicity p x" proof - from assms have "{n. (c * p) ^ n dvd x} = {n. p ^ n dvd x}" by (subst mult.commute) (simp add: mult_unit_dvd_iff power_mult_distrib is_unit_power_iff) thus ?thesis by (simp add: multiplicity_def) qed lemma multiplicity_times_unit_right: assumes "is_unit c" shows "multiplicity p (c * x) = multiplicity p x" proof - from assms have "{n. p ^ n dvd c * x} = {n. p ^ n dvd x}" by (subst mult.commute) (simp add: dvd_mult_unit_iff) thus ?thesis by (simp add: multiplicity_def) qed lemma multiplicity_normalize_left [simp]: "multiplicity (normalize p) x = multiplicity p x" proof (cases "p = 0") case [simp]: False have "normalize p = (1 div unit_factor p) * p" by (simp add: unit_div_commute is_unit_unit_factor) also have "multiplicity \ x = multiplicity p x" by (rule multiplicity_times_unit_left) (simp add: is_unit_unit_factor) finally show ?thesis . qed simp_all lemma multiplicity_normalize_right [simp]: "multiplicity p (normalize x) = multiplicity p x" proof (cases "x = 0") case [simp]: False have "normalize x = (1 div unit_factor x) * x" by (simp add: unit_div_commute is_unit_unit_factor) also have "multiplicity p \ = multiplicity p x" by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor) finally show ?thesis . qed simp_all lemma multiplicity_prime [simp]: "prime_elem p \ multiplicity p p = 1" by (rule multiplicity_self) auto lemma multiplicity_prime_power [simp]: "prime_elem p \ multiplicity p (p ^ n) = n" by (subst multiplicity_same_power') auto lift_definition prime_factorization :: "'a \ 'a multiset" is "\x p. if prime p then multiplicity p x else 0" unfolding multiset_def proof clarify fix x :: 'a show "finite {p. 0 < (if prime p then multiplicity p x else 0)}" (is "finite ?A") proof (cases "x = 0") case False from False have "?A \ {p. prime p \ p dvd x}" by (auto simp: multiplicity_gt_zero_iff) moreover from False have "finite {p. prime p \ p dvd x}" by (rule finite_prime_divisors) ultimately show ?thesis by (rule finite_subset) qed simp_all qed abbreviation prime_factors :: "'a \ 'a set" where "prime_factors a \ set_mset (prime_factorization a)" lemma count_prime_factorization_nonprime: "\prime p \ count (prime_factorization x) p = 0" by transfer simp lemma count_prime_factorization_prime: "prime p \ count (prime_factorization x) p = multiplicity p x" by transfer simp lemma count_prime_factorization: "count (prime_factorization x) p = (if prime p then multiplicity p x else 0)" by transfer simp lemma dvd_imp_multiplicity_le: assumes "a dvd b" "b \ 0" shows "multiplicity p a \ multiplicity p b" proof (cases "is_unit p") case False with assms show ?thesis by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)]) qed (insert assms, auto simp: multiplicity_unit_left) lemma prime_power_inj: assumes "prime a" "a ^ m = a ^ n" shows "m = n" proof - have "multiplicity a (a ^ m) = multiplicity a (a ^ n)" by (simp only: assms) thus ?thesis using assms by (subst (asm) (1 2) multiplicity_prime_power) simp_all qed lemma prime_power_inj': assumes "prime p" "prime q" assumes "p ^ m = q ^ n" "m > 0" "n > 0" shows "p = q" "m = n" proof - from assms have "p ^ 1 dvd p ^ m" by (intro le_imp_power_dvd) simp also have "p ^ m = q ^ n" by fact finally have "p dvd q ^ n" by simp with assms have "p dvd q" using prime_dvd_power[of p q] by simp with assms show "p = q" by (simp add: primes_dvd_imp_eq) with assms show "m = n" by (simp add: prime_power_inj) qed lemma prime_power_eq_one_iff [simp]: "prime p \ p ^ n = 1 \ n = 0" using prime_power_inj[of p n 0] by auto lemma one_eq_prime_power_iff [simp]: "prime p \ 1 = p ^ n \ n = 0" using prime_power_inj[of p 0 n] by auto lemma prime_power_inj'': assumes "prime p" "prime q" shows "p ^ m = q ^ n \ (m = 0 \ n = 0) \ (p = q \ m = n)" using assms by (cases "m = 0"; cases "n = 0") (auto dest: prime_power_inj'[OF assms]) lemma prime_factorization_0 [simp]: "prime_factorization 0 = {#}" by (simp add: multiset_eq_iff count_prime_factorization) lemma prime_factorization_empty_iff: "prime_factorization x = {#} \ x = 0 \ is_unit x" proof assume *: "prime_factorization x = {#}" { assume x: "x \ 0" "\is_unit x" { fix p assume p: "prime p" have "count (prime_factorization x) p = 0" by (simp add: *) also from p have "count (prime_factorization x) p = multiplicity p x" by (rule count_prime_factorization_prime) also from x p have "\ = 0 \ \p dvd x" by (simp add: multiplicity_eq_zero_iff) finally have "\p dvd x" . } with prime_divisor_exists[OF x] have False by blast } thus "x = 0 \ is_unit x" by blast next assume "x = 0 \ is_unit x" thus "prime_factorization x = {#}" proof assume x: "is_unit x" { fix p assume p: "prime p" from p x have "multiplicity p x = 0" by (subst multiplicity_eq_zero_iff) (auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors) } thus ?thesis by (simp add: multiset_eq_iff count_prime_factorization) qed simp_all qed lemma prime_factorization_unit: assumes "is_unit x" shows "prime_factorization x = {#}" proof (rule multiset_eqI) fix p :: 'a show "count (prime_factorization x) p = count {#} p" proof (cases "prime p") case True with assms have "multiplicity p x = 0" by (subst multiplicity_eq_zero_iff) (auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors) with True show ?thesis by (simp add: count_prime_factorization_prime) qed (simp_all add: count_prime_factorization_nonprime) qed lemma prime_factorization_1 [simp]: "prime_factorization 1 = {#}" by (simp add: prime_factorization_unit) lemma prime_factorization_times_prime: assumes "x \ 0" "prime p" shows "prime_factorization (p * x) = {#p#} + prime_factorization x" proof (rule multiset_eqI) fix q :: 'a consider "\prime q" | "p = q" | "prime q" "p \ q" by blast thus "count (prime_factorization (p * x)) q = count ({#p#} + prime_factorization x) q" proof cases assume q: "prime q" "p \ q" with assms primes_dvd_imp_eq[of q p] have "\q dvd p" by auto with q assms show ?thesis by (simp add: multiplicity_prime_elem_times_other count_prime_factorization) qed (insert assms, auto simp: count_prime_factorization multiplicity_times_same) qed lemma prod_mset_prime_factorization_weak: assumes "x \ 0" shows "normalize (prod_mset (prime_factorization x)) = normalize x" using assms proof (induction x rule: prime_divisors_induct) case (factor p x) have "normalize (prod_mset (prime_factorization (p * x))) = normalize (p * normalize (prod_mset (prime_factorization x)))" using factor.prems factor.hyps by (simp add: prime_factorization_times_prime) also have "normalize (prod_mset (prime_factorization x)) = normalize x" by (rule factor.IH) (use factor in auto) finally show ?case by simp qed (auto simp: prime_factorization_unit is_unit_normalize) lemma in_prime_factors_iff: "p \ prime_factors x \ x \ 0 \ p dvd x \ prime p" proof - have "p \ prime_factors x \ count (prime_factorization x) p > 0" by simp also have "\ \ x \ 0 \ p dvd x \ prime p" by (subst count_prime_factorization, cases "x = 0") (auto simp: multiplicity_eq_zero_iff multiplicity_gt_zero_iff) finally show ?thesis . qed lemma in_prime_factors_imp_prime [intro]: "p \ prime_factors x \ prime p" by (simp add: in_prime_factors_iff) lemma in_prime_factors_imp_dvd [dest]: "p \ prime_factors x \ p dvd x" by (simp add: in_prime_factors_iff) lemma prime_factorsI: "x \ 0 \ prime p \ p dvd x \ p \ prime_factors x" by (auto simp: in_prime_factors_iff) lemma prime_factors_dvd: "x \ 0 \ prime_factors x = {p. prime p \ p dvd x}" by (auto intro: prime_factorsI) lemma prime_factors_multiplicity: "prime_factors n = {p. prime p \ multiplicity p n > 0}" by (cases "n = 0") (auto simp add: prime_factors_dvd prime_multiplicity_gt_zero_iff) lemma prime_factorization_prime: assumes "prime p" shows "prime_factorization p = {#p#}" proof (rule multiset_eqI) fix q :: 'a consider "\prime q" | "q = p" | "prime q" "q \ p" by blast thus "count (prime_factorization p) q = count {#p#} q" by cases (insert assms, auto dest: primes_dvd_imp_eq simp: count_prime_factorization multiplicity_self multiplicity_eq_zero_iff) qed lemma prime_factorization_prod_mset_primes: assumes "\p. p \# A \ prime p" shows "prime_factorization (prod_mset A) = A" using assms proof (induction A) case (add p A) from add.prems[of 0] have "0 \# A" by auto hence "prod_mset A \ 0" by auto with add show ?case by (simp_all add: mult_ac prime_factorization_times_prime Multiset.union_commute) qed simp_all lemma prime_factorization_cong: "normalize x = normalize y \ prime_factorization x = prime_factorization y" by (simp add: multiset_eq_iff count_prime_factorization multiplicity_normalize_right [of _ x, symmetric] multiplicity_normalize_right [of _ y, symmetric] del: multiplicity_normalize_right) lemma prime_factorization_unique: assumes "x \ 0" "y \ 0" shows "prime_factorization x = prime_factorization y \ normalize x = normalize y" proof assume "prime_factorization x = prime_factorization y" hence "prod_mset (prime_factorization x) = prod_mset (prime_factorization y)" by simp hence "normalize (prod_mset (prime_factorization x)) = normalize (prod_mset (prime_factorization y))" by (simp only: ) with assms show "normalize x = normalize y" by (simp add: prod_mset_prime_factorization_weak) qed (rule prime_factorization_cong) lemma prime_factorization_normalize [simp]: "prime_factorization (normalize x) = prime_factorization x" by (cases "x = 0", simp, subst prime_factorization_unique) auto lemma prime_factorization_eqI_strong: assumes "\p. p \# P \ prime p" "prod_mset P = n" shows "prime_factorization n = P" using prime_factorization_prod_mset_primes[of P] assms by simp lemma prime_factorization_eqI: assumes "\p. p \# P \ prime p" "normalize (prod_mset P) = normalize n" shows "prime_factorization n = P" proof - have "P = prime_factorization (normalize (prod_mset P))" using prime_factorization_prod_mset_primes[of P] assms(1) by simp with assms(2) show ?thesis by simp qed lemma prime_factorization_mult: assumes "x \ 0" "y \ 0" shows "prime_factorization (x * y) = prime_factorization x + prime_factorization y" proof - have "normalize (prod_mset (prime_factorization x) * prod_mset (prime_factorization y)) = normalize (normalize (prod_mset (prime_factorization x)) * normalize (prod_mset (prime_factorization y)))" by (simp only: normalize_mult_normalize_left normalize_mult_normalize_right) also have "\ = normalize (x * y)" by (subst (1 2) prod_mset_prime_factorization_weak) (use assms in auto) finally show ?thesis by (intro prime_factorization_eqI) auto qed lemma prime_factorization_prod: assumes "finite A" "\x. x \ A \ f x \ 0" shows "prime_factorization (prod f A) = (\n\A. prime_factorization (f n))" using assms by (induction A rule: finite_induct) (auto simp: Sup_multiset_empty prime_factorization_mult) lemma prime_elem_multiplicity_mult_distrib: assumes "prime_elem p" "x \ 0" "y \ 0" shows "multiplicity p (x * y) = multiplicity p x + multiplicity p y" proof - have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)" by (subst count_prime_factorization_prime) (simp_all add: assms) also from assms have "prime_factorization (x * y) = prime_factorization x + prime_factorization y" by (intro prime_factorization_mult) also have "count \ (normalize p) = count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)" by simp also have "\ = multiplicity p x + multiplicity p y" by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms) finally show ?thesis . qed lemma prime_elem_multiplicity_prod_mset_distrib: assumes "prime_elem p" "0 \# A" shows "multiplicity p (prod_mset A) = sum_mset (image_mset (multiplicity p) A)" using assms by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib) lemma prime_elem_multiplicity_power_distrib: assumes "prime_elem p" "x \ 0" shows "multiplicity p (x ^ n) = n * multiplicity p x" using assms prime_elem_multiplicity_prod_mset_distrib [of p "replicate_mset n x"] by simp lemma prime_elem_multiplicity_prod_distrib: assumes "prime_elem p" "0 \ f ` A" "finite A" shows "multiplicity p (prod f A) = (\x\A. multiplicity p (f x))" proof - have "multiplicity p (prod f A) = (\x\#mset_set A. multiplicity p (f x))" using assms by (subst prod_unfold_prod_mset) (simp_all add: prime_elem_multiplicity_prod_mset_distrib sum_unfold_sum_mset multiset.map_comp o_def) also from \finite A\ have "\ = (\x\A. multiplicity p (f x))" by (induction A rule: finite_induct) simp_all finally show ?thesis . qed lemma multiplicity_distinct_prime_power: "prime p \ prime q \ p \ q \ multiplicity p (q ^ n) = 0" by (subst prime_elem_multiplicity_power_distrib) (auto simp: prime_multiplicity_other) lemma prime_factorization_prime_power: "prime p \ prime_factorization (p ^ n) = replicate_mset n p" by (induction n) (simp_all add: prime_factorization_mult prime_factorization_prime Multiset.union_commute) lemma prime_factorization_subset_iff_dvd: assumes [simp]: "x \ 0" "y \ 0" shows "prime_factorization x \# prime_factorization y \ x dvd y" proof - have "x dvd y \ normalize (prod_mset (prime_factorization x)) dvd normalize (prod_mset (prime_factorization y))" using assms by (subst (1 2) prod_mset_prime_factorization_weak) auto also have "\ \ prime_factorization x \# prime_factorization y" by (auto intro!: prod_mset_primes_dvd_imp_subset prod_mset_subset_imp_dvd) finally show ?thesis .. qed lemma prime_factorization_subset_imp_dvd: "x \ 0 \ (prime_factorization x \# prime_factorization y) \ x dvd y" by (cases "y = 0") (simp_all add: prime_factorization_subset_iff_dvd) lemma prime_factorization_divide: assumes "b dvd a" shows "prime_factorization (a div b) = prime_factorization a - prime_factorization b" proof (cases "a = 0") case [simp]: False from assms have [simp]: "b \ 0" by auto have "prime_factorization ((a div b) * b) = prime_factorization (a div b) + prime_factorization b" by (intro prime_factorization_mult) (insert assms, auto elim!: dvdE) with assms show ?thesis by simp qed simp_all lemma zero_not_in_prime_factors [simp]: "0 \ prime_factors x" by (auto dest: in_prime_factors_imp_prime) lemma prime_prime_factors: "prime p \ prime_factors p = {p}" by (drule prime_factorization_prime) simp lemma prime_factors_product: "x \ 0 \ y \ 0 \ prime_factors (x * y) = prime_factors x \ prime_factors y" by (simp add: prime_factorization_mult) lemma dvd_prime_factors [intro]: "y \ 0 \ x dvd y \ prime_factors x \ prime_factors y" by (intro set_mset_mono, subst prime_factorization_subset_iff_dvd) auto (* RENAMED multiplicity_dvd *) lemma multiplicity_le_imp_dvd: assumes "x \ 0" "\p. prime p \ multiplicity p x \ multiplicity p y" shows "x dvd y" proof (cases "y = 0") case False from assms this have "prime_factorization x \# prime_factorization y" by (intro mset_subset_eqI) (auto simp: count_prime_factorization) with assms False show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd) qed auto lemma dvd_multiplicity_eq: "x \ 0 \ y \ 0 \ x dvd y \ (\p. multiplicity p x \ multiplicity p y)" by (auto intro: dvd_imp_multiplicity_le multiplicity_le_imp_dvd) lemma multiplicity_eq_imp_eq: assumes "x \ 0" "y \ 0" assumes "\p. prime p \ multiplicity p x = multiplicity p y" shows "normalize x = normalize y" using assms by (intro associatedI multiplicity_le_imp_dvd) simp_all lemma prime_factorization_unique': assumes "\p \# M. prime p" "\p \# N. prime p" "(\i \# M. i) = (\i \# N. i)" shows "M = N" proof - have "prime_factorization (\i \# M. i) = prime_factorization (\i \# N. i)" by (simp only: assms) also from assms have "prime_factorization (\i \# M. i) = M" by (subst prime_factorization_prod_mset_primes) simp_all also from assms have "prime_factorization (\i \# N. i) = N" by (subst prime_factorization_prod_mset_primes) simp_all finally show ?thesis . qed lemma prime_factorization_unique'': assumes "\p \# M. prime p" "\p \# N. prime p" "normalize (\i \# M. i) = normalize (\i \# N. i)" shows "M = N" proof - have "prime_factorization (normalize (\i \# M. i)) = prime_factorization (normalize (\i \# N. i))" by (simp only: assms) also from assms have "prime_factorization (normalize (\i \# M. i)) = M" by (subst prime_factorization_normalize, subst prime_factorization_prod_mset_primes) simp_all also from assms have "prime_factorization (normalize (\i \# N. i)) = N" by (subst prime_factorization_normalize, subst prime_factorization_prod_mset_primes) simp_all finally show ?thesis . qed lemma multiplicity_cong: "(\r. p ^ r dvd a \ p ^ r dvd b) \ multiplicity p a = multiplicity p b" by (simp add: multiplicity_def) lemma not_dvd_imp_multiplicity_0: assumes "\p dvd x" shows "multiplicity p x = 0" proof - from assms have "multiplicity p x < 1" by (intro multiplicity_lessI) auto thus ?thesis by simp qed -lemma multiplicity_zero_1 [simp]: "multiplicity 0 x = 0" - by (metis (mono_tags) local.dvd_0_left multiplicity_zero not_dvd_imp_multiplicity_0) +lemma multiplicity_zero_left [simp]: "multiplicity 0 x = 0" + by (cases "x = 0") (auto intro: not_dvd_imp_multiplicity_0) lemma inj_on_Prod_primes: assumes "\P p. P \ A \ p \ P \ prime p" assumes "\P. P \ A \ finite P" shows "inj_on Prod A" proof (rule inj_onI) fix P Q assume PQ: "P \ A" "Q \ A" "\P = \Q" with prime_factorization_unique'[of "mset_set P" "mset_set Q"] assms[of P] assms[of Q] have "mset_set P = mset_set Q" by (auto simp: prod_unfold_prod_mset) with assms[of P] assms[of Q] PQ show "P = Q" by simp qed lemma divides_primepow_weak: assumes "prime p" and "a dvd p ^ n" obtains m where "m \ n" and "normalize a = normalize (p ^ m)" proof - from assms have "a \ 0" by auto with assms have "normalize (prod_mset (prime_factorization a)) dvd normalize (prod_mset (prime_factorization (p ^ n)))" by (subst (1 2) prod_mset_prime_factorization_weak) auto then have "prime_factorization a \# prime_factorization (p ^ n)" by (simp add: in_prime_factors_imp_prime prod_mset_dvd_prod_mset_primes_iff) with assms have "prime_factorization a \# replicate_mset n p" by (simp add: prime_factorization_prime_power) then obtain m where "m \ n" and "prime_factorization a = replicate_mset m p" by (rule msubseteq_replicate_msetE) then have *: "normalize (prod_mset (prime_factorization a)) = normalize (prod_mset (replicate_mset m p))" by metis also have "normalize (prod_mset (prime_factorization a)) = normalize a" using \a \ 0\ by (simp add: prod_mset_prime_factorization_weak) also have "prod_mset (replicate_mset m p) = p ^ m" by simp finally show ?thesis using \m \ n\ by (intro that[of m]) qed lemma divide_out_primepow_ex: assumes "n \ 0" "\p\prime_factors n. P p" obtains p k n' where "P p" "prime p" "p dvd n" "\p dvd n'" "k > 0" "n = p ^ k * n'" proof - from assms obtain p where p: "P p" "prime p" "p dvd n" by auto define k where "k = multiplicity p n" define n' where "n' = n div p ^ k" have n': "n = p ^ k * n'" "\p dvd n'" using assms p multiplicity_decompose[of n p] by (auto simp: n'_def k_def multiplicity_dvd) from n' p have "k > 0" by (intro Nat.gr0I) auto with n' p that[of p n' k] show ?thesis by auto qed lemma divide_out_primepow: assumes "n \ 0" "\is_unit n" obtains p k n' where "prime p" "p dvd n" "\p dvd n'" "k > 0" "n = p ^ k * n'" using divide_out_primepow_ex[OF assms(1), of "\_. True"] prime_divisor_exists[OF assms] assms prime_factorsI by metis subsection \GCD and LCM computation with unique factorizations\ definition "gcd_factorial a b = (if a = 0 then normalize b else if b = 0 then normalize a else normalize (prod_mset (prime_factorization a \# prime_factorization b)))" definition "lcm_factorial a b = (if a = 0 \ b = 0 then 0 else normalize (prod_mset (prime_factorization a \# prime_factorization b)))" definition "Gcd_factorial A = (if A \ {0} then 0 else normalize (prod_mset (Inf (prime_factorization ` (A - {0})))))" definition "Lcm_factorial A = (if A = {} then 1 else if 0 \ A \ subset_mset.bdd_above (prime_factorization ` (A - {0})) then normalize (prod_mset (Sup (prime_factorization ` A))) else 0)" lemma prime_factorization_gcd_factorial: assumes [simp]: "a \ 0" "b \ 0" shows "prime_factorization (gcd_factorial a b) = prime_factorization a \# prime_factorization b" proof - have "prime_factorization (gcd_factorial a b) = prime_factorization (prod_mset (prime_factorization a \# prime_factorization b))" by (simp add: gcd_factorial_def) also have "\ = prime_factorization a \# prime_factorization b" by (subst prime_factorization_prod_mset_primes) auto finally show ?thesis . qed lemma prime_factorization_lcm_factorial: assumes [simp]: "a \ 0" "b \ 0" shows "prime_factorization (lcm_factorial a b) = prime_factorization a \# prime_factorization b" proof - have "prime_factorization (lcm_factorial a b) = prime_factorization (prod_mset (prime_factorization a \# prime_factorization b))" by (simp add: lcm_factorial_def) also have "\ = prime_factorization a \# prime_factorization b" by (subst prime_factorization_prod_mset_primes) auto finally show ?thesis . qed lemma prime_factorization_Gcd_factorial: assumes "\A \ {0}" shows "prime_factorization (Gcd_factorial A) = Inf (prime_factorization ` (A - {0}))" proof - from assms obtain x where x: "x \ A - {0}" by auto hence "Inf (prime_factorization ` (A - {0})) \# prime_factorization x" by (intro subset_mset.cInf_lower) simp_all hence "\y. y \# Inf (prime_factorization ` (A - {0})) \ y \ prime_factors x" by (auto dest: mset_subset_eqD) with in_prime_factors_imp_prime[of _ x] have "\p. p \# Inf (prime_factorization ` (A - {0})) \ prime p" by blast with assms show ?thesis by (simp add: Gcd_factorial_def prime_factorization_prod_mset_primes) qed lemma prime_factorization_Lcm_factorial: assumes "0 \ A" "subset_mset.bdd_above (prime_factorization ` A)" shows "prime_factorization (Lcm_factorial A) = Sup (prime_factorization ` A)" proof (cases "A = {}") case True hence "prime_factorization ` A = {}" by auto also have "Sup \ = {#}" by (simp add: Sup_multiset_empty) finally show ?thesis by (simp add: Lcm_factorial_def) next case False have "\y. y \# Sup (prime_factorization ` A) \ prime y" by (auto simp: in_Sup_multiset_iff assms) with assms False show ?thesis by (simp add: Lcm_factorial_def prime_factorization_prod_mset_primes) qed lemma gcd_factorial_commute: "gcd_factorial a b = gcd_factorial b a" by (simp add: gcd_factorial_def multiset_inter_commute) lemma gcd_factorial_dvd1: "gcd_factorial a b dvd a" proof (cases "a = 0 \ b = 0") case False hence "gcd_factorial a b \ 0" by (auto simp: gcd_factorial_def) with False show ?thesis by (subst prime_factorization_subset_iff_dvd [symmetric]) (auto simp: prime_factorization_gcd_factorial) qed (auto simp: gcd_factorial_def) lemma gcd_factorial_dvd2: "gcd_factorial a b dvd b" by (subst gcd_factorial_commute) (rule gcd_factorial_dvd1) lemma normalize_gcd_factorial [simp]: "normalize (gcd_factorial a b) = gcd_factorial a b" by (simp add: gcd_factorial_def) lemma normalize_lcm_factorial [simp]: "normalize (lcm_factorial a b) = lcm_factorial a b" by (simp add: lcm_factorial_def) lemma gcd_factorial_greatest: "c dvd gcd_factorial a b" if "c dvd a" "c dvd b" for a b c proof (cases "a = 0 \ b = 0") case False with that have [simp]: "c \ 0" by auto let ?p = "prime_factorization" from that False have "?p c \# ?p a" "?p c \# ?p b" by (simp_all add: prime_factorization_subset_iff_dvd) hence "prime_factorization c \# prime_factorization (prod_mset (prime_factorization a \# prime_factorization b))" using False by (subst prime_factorization_prod_mset_primes) auto with False show ?thesis by (auto simp: gcd_factorial_def prime_factorization_subset_iff_dvd [symmetric]) qed (auto simp: gcd_factorial_def that) lemma lcm_factorial_gcd_factorial: "lcm_factorial a b = normalize (a * b div gcd_factorial a b)" for a b proof (cases "a = 0 \ b = 0") case False let ?p = "prime_factorization" have 1: "normalize x * normalize y dvd z \ x * y dvd z" for x y z :: 'a proof - have "normalize (normalize x * normalize y) dvd z \ x * y dvd z" unfolding normalize_mult_normalize_left normalize_mult_normalize_right by simp thus ?thesis unfolding normalize_dvd_iff by simp qed have "?p (a * b) = (?p a \# ?p b) + (?p a \# ?p b)" using False by (subst prime_factorization_mult) (auto intro!: multiset_eqI) hence "normalize (prod_mset (?p (a * b))) = normalize (prod_mset ((?p a \# ?p b) + (?p a \# ?p b)))" by (simp only:) hence *: "normalize (a * b) = normalize (lcm_factorial a b * gcd_factorial a b)" using False by (subst (asm) prod_mset_prime_factorization_weak) (auto simp: lcm_factorial_def gcd_factorial_def) have [simp]: "gcd_factorial a b dvd a * b" "lcm_factorial a b dvd a * b" using associatedD2[OF *] by auto from False have [simp]: "gcd_factorial a b \ 0" "lcm_factorial a b \ 0" by (auto simp: gcd_factorial_def lcm_factorial_def) show ?thesis by (rule associated_eqI) (use * in \auto simp: dvd_div_iff_mult div_dvd_iff_mult dest: associatedD1 associatedD2\) qed (auto simp: lcm_factorial_def) lemma normalize_Gcd_factorial: "normalize (Gcd_factorial A) = Gcd_factorial A" by (simp add: Gcd_factorial_def) lemma Gcd_factorial_eq_0_iff: "Gcd_factorial A = 0 \ A \ {0}" by (auto simp: Gcd_factorial_def in_Inf_multiset_iff split: if_splits) lemma Gcd_factorial_dvd: assumes "x \ A" shows "Gcd_factorial A dvd x" proof (cases "x = 0") case False with assms have "prime_factorization (Gcd_factorial A) = Inf (prime_factorization ` (A - {0}))" by (intro prime_factorization_Gcd_factorial) auto also from False assms have "\ \# prime_factorization x" by (intro subset_mset.cInf_lower) auto finally show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd) (insert assms False, auto simp: Gcd_factorial_eq_0_iff) qed simp_all lemma Gcd_factorial_greatest: assumes "\y. y \ A \ x dvd y" shows "x dvd Gcd_factorial A" proof (cases "A \ {0}") case False from False obtain y where "y \ A" "y \ 0" by auto with assms[of y] have nz: "x \ 0" by auto from nz assms have "prime_factorization x \# prime_factorization y" if "y \ A - {0}" for y using that by (subst prime_factorization_subset_iff_dvd) auto with False have "prime_factorization x \# Inf (prime_factorization ` (A - {0}))" by (intro subset_mset.cInf_greatest) auto also from False have "\ = prime_factorization (Gcd_factorial A)" by (rule prime_factorization_Gcd_factorial [symmetric]) finally show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd) (insert nz False, auto simp: Gcd_factorial_eq_0_iff) qed (simp_all add: Gcd_factorial_def) lemma normalize_Lcm_factorial: "normalize (Lcm_factorial A) = Lcm_factorial A" by (simp add: Lcm_factorial_def) lemma Lcm_factorial_eq_0_iff: "Lcm_factorial A = 0 \ 0 \ A \ \subset_mset.bdd_above (prime_factorization ` A)" by (auto simp: Lcm_factorial_def in_Sup_multiset_iff) lemma dvd_Lcm_factorial: assumes "x \ A" shows "x dvd Lcm_factorial A" proof (cases "0 \ A \ subset_mset.bdd_above (prime_factorization ` A)") case True with assms have [simp]: "0 \ A" "x \ 0" "A \ {}" by auto from assms True have "prime_factorization x \# Sup (prime_factorization ` A)" by (intro subset_mset.cSup_upper) auto also have "\ = prime_factorization (Lcm_factorial A)" by (rule prime_factorization_Lcm_factorial [symmetric]) (insert True, simp_all) finally show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd) (insert True, auto simp: Lcm_factorial_eq_0_iff) qed (insert assms, auto simp: Lcm_factorial_def) lemma Lcm_factorial_least: assumes "\y. y \ A \ y dvd x" shows "Lcm_factorial A dvd x" proof - consider "A = {}" | "0 \ A" | "x = 0" | "A \ {}" "0 \ A" "x \ 0" by blast thus ?thesis proof cases assume *: "A \ {}" "0 \ A" "x \ 0" hence nz: "x \ 0" if "x \ A" for x using that by auto from * have bdd: "subset_mset.bdd_above (prime_factorization ` A)" by (intro subset_mset.bdd_aboveI[of _ "prime_factorization x"]) (auto simp: prime_factorization_subset_iff_dvd nz dest: assms) have "prime_factorization (Lcm_factorial A) = Sup (prime_factorization ` A)" by (rule prime_factorization_Lcm_factorial) fact+ also from * have "\ \# prime_factorization x" by (intro subset_mset.cSup_least) (auto simp: prime_factorization_subset_iff_dvd nz dest: assms) finally show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd) (insert * bdd, auto simp: Lcm_factorial_eq_0_iff) qed (auto simp: Lcm_factorial_def dest: assms) qed lemmas gcd_lcm_factorial = gcd_factorial_dvd1 gcd_factorial_dvd2 gcd_factorial_greatest normalize_gcd_factorial lcm_factorial_gcd_factorial normalize_Gcd_factorial Gcd_factorial_dvd Gcd_factorial_greatest normalize_Lcm_factorial dvd_Lcm_factorial Lcm_factorial_least end class factorial_semiring_gcd = factorial_semiring + gcd + Gcd + assumes gcd_eq_gcd_factorial: "gcd a b = gcd_factorial a b" and lcm_eq_lcm_factorial: "lcm a b = lcm_factorial a b" and Gcd_eq_Gcd_factorial: "Gcd A = Gcd_factorial A" and Lcm_eq_Lcm_factorial: "Lcm A = Lcm_factorial A" begin lemma prime_factorization_gcd: assumes [simp]: "a \ 0" "b \ 0" shows "prime_factorization (gcd a b) = prime_factorization a \# prime_factorization b" by (simp add: gcd_eq_gcd_factorial prime_factorization_gcd_factorial) lemma prime_factorization_lcm: assumes [simp]: "a \ 0" "b \ 0" shows "prime_factorization (lcm a b) = prime_factorization a \# prime_factorization b" by (simp add: lcm_eq_lcm_factorial prime_factorization_lcm_factorial) lemma prime_factorization_Gcd: assumes "Gcd A \ 0" shows "prime_factorization (Gcd A) = Inf (prime_factorization ` (A - {0}))" using assms by (simp add: prime_factorization_Gcd_factorial Gcd_eq_Gcd_factorial Gcd_factorial_eq_0_iff) lemma prime_factorization_Lcm: assumes "Lcm A \ 0" shows "prime_factorization (Lcm A) = Sup (prime_factorization ` A)" using assms by (simp add: prime_factorization_Lcm_factorial Lcm_eq_Lcm_factorial Lcm_factorial_eq_0_iff) lemma prime_factors_gcd [simp]: "a \ 0 \ b \ 0 \ prime_factors (gcd a b) = prime_factors a \ prime_factors b" by (subst prime_factorization_gcd) auto lemma prime_factors_lcm [simp]: "a \ 0 \ b \ 0 \ prime_factors (lcm a b) = prime_factors a \ prime_factors b" by (subst prime_factorization_lcm) auto subclass semiring_gcd by (standard, unfold gcd_eq_gcd_factorial lcm_eq_lcm_factorial) (rule gcd_lcm_factorial; assumption)+ subclass semiring_Gcd by (standard, unfold Gcd_eq_Gcd_factorial Lcm_eq_Lcm_factorial) (rule gcd_lcm_factorial; assumption)+ lemma assumes "x \ 0" "y \ 0" shows gcd_eq_factorial': "gcd x y = normalize (\p \ prime_factors x \ prime_factors y. p ^ min (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs1") and lcm_eq_factorial': "lcm x y = normalize (\p \ prime_factors x \ prime_factors y. p ^ max (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs2") proof - have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial) also have "\ = ?rhs1" by (auto simp: gcd_factorial_def assms prod_mset_multiplicity count_prime_factorization_prime intro!: arg_cong[of _ _ normalize] dest: in_prime_factors_imp_prime intro!: prod.cong) finally show "gcd x y = ?rhs1" . have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial) also have "\ = ?rhs2" by (auto simp: lcm_factorial_def assms prod_mset_multiplicity count_prime_factorization_prime intro!: arg_cong[of _ _ normalize] dest: in_prime_factors_imp_prime intro!: prod.cong) finally show "lcm x y = ?rhs2" . qed lemma assumes "x \ 0" "y \ 0" "prime p" shows multiplicity_gcd: "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)" and multiplicity_lcm: "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)" proof - have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial) also from assms have "multiplicity p \ = min (multiplicity p x) (multiplicity p y)" by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_gcd_factorial) finally show "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)" . have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial) also from assms have "multiplicity p \ = max (multiplicity p x) (multiplicity p y)" by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_lcm_factorial) finally show "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)" . qed lemma gcd_lcm_distrib: "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" proof (cases "x = 0 \ y = 0 \ z = 0") case True thus ?thesis by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd) next case False hence "normalize (gcd x (lcm y z)) = normalize (lcm (gcd x y) (gcd x z))" by (intro associatedI prime_factorization_subset_imp_dvd) (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm subset_mset.inf_sup_distrib1) thus ?thesis by simp qed lemma lcm_gcd_distrib: "lcm x (gcd y z) = gcd (lcm x y) (lcm x z)" proof (cases "x = 0 \ y = 0 \ z = 0") case True thus ?thesis by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd) next case False hence "normalize (lcm x (gcd y z)) = normalize (gcd (lcm x y) (lcm x z))" by (intro associatedI prime_factorization_subset_imp_dvd) (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm subset_mset.sup_inf_distrib1) thus ?thesis by simp qed end class factorial_ring_gcd = factorial_semiring_gcd + idom begin subclass ring_gcd .. subclass idom_divide .. end class factorial_semiring_multiplicative = factorial_semiring + normalization_semidom_multiplicative begin lemma normalize_prod_mset_primes: "(\p. p \# A \ prime p) \ normalize (prod_mset A) = prod_mset A" proof (induction A) case (add p A) hence "prime p" by simp hence "normalize p = p" by simp with add show ?case by (simp add: normalize_mult) qed simp_all lemma prod_mset_prime_factorization: assumes "x \ 0" shows "prod_mset (prime_factorization x) = normalize x" using assms by (induction x rule: prime_divisors_induct) (simp_all add: prime_factorization_unit prime_factorization_times_prime is_unit_normalize normalize_mult) lemma prime_decomposition: "unit_factor x * prod_mset (prime_factorization x) = x" by (cases "x = 0") (simp_all add: prod_mset_prime_factorization) lemma prod_prime_factors: assumes "x \ 0" shows "(\p \ prime_factors x. p ^ multiplicity p x) = normalize x" proof - have "normalize x = prod_mset (prime_factorization x)" by (simp add: prod_mset_prime_factorization assms) also have "\ = (\p \ prime_factors x. p ^ count (prime_factorization x) p)" by (subst prod_mset_multiplicity) simp_all also have "\ = (\p \ prime_factors x. p ^ multiplicity p x)" by (intro prod.cong) (simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime) finally show ?thesis .. qed lemma prime_factorization_unique'': assumes S_eq: "S = {p. 0 < f p}" and "finite S" and S: "\p\S. prime p" "normalize n = (\p\S. p ^ f p)" shows "S = prime_factors n \ (\p. prime p \ f p = multiplicity p n)" proof define A where "A = Abs_multiset f" from \finite S\ S(1) have "(\p\S. p ^ f p) \ 0" by auto with S(2) have nz: "n \ 0" by auto from S_eq \finite S\ have count_A: "count A = f" unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def) from S_eq count_A have set_mset_A: "set_mset A = S" by (simp only: set_mset_def) from S(2) have "normalize n = (\p\S. p ^ f p)" . also have "\ = prod_mset A" by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A) also from nz have "normalize n = prod_mset (prime_factorization n)" by (simp add: prod_mset_prime_factorization) finally have "prime_factorization (prod_mset A) = prime_factorization (prod_mset (prime_factorization n))" by simp also from S(1) have "prime_factorization (prod_mset A) = A" by (intro prime_factorization_prod_mset_primes) (auto simp: set_mset_A) also have "prime_factorization (prod_mset (prime_factorization n)) = prime_factorization n" by (intro prime_factorization_prod_mset_primes) auto finally show "S = prime_factors n" by (simp add: set_mset_A [symmetric]) show "(\p. prime p \ f p = multiplicity p n)" proof safe fix p :: 'a assume p: "prime p" have "multiplicity p n = multiplicity p (normalize n)" by simp also have "normalize n = prod_mset A" by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A S) also from p set_mset_A S(1) have "multiplicity p \ = sum_mset (image_mset (multiplicity p) A)" by (intro prime_elem_multiplicity_prod_mset_distrib) auto also from S(1) p have "image_mset (multiplicity p) A = image_mset (\q. if p = q then 1 else 0) A" by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other) also have "sum_mset \ = f p" by (simp add: semiring_1_class.sum_mset_delta' count_A) finally show "f p = multiplicity p n" .. qed qed lemma divides_primepow: assumes "prime p" and "a dvd p ^ n" obtains m where "m \ n" and "normalize a = p ^ m" using divides_primepow_weak[OF assms] that assms by (auto simp add: normalize_power) lemma Ex_other_prime_factor: assumes "n \ 0" and "\(\k. normalize n = p ^ k)" "prime p" shows "\q\prime_factors n. q \ p" proof (rule ccontr) assume *: "\(\q\prime_factors n. q \ p)" have "normalize n = (\p\prime_factors n. p ^ multiplicity p n)" using assms(1) by (intro prod_prime_factors [symmetric]) auto also from * have "\ = (\p\{p}. p ^ multiplicity p n)" using assms(3) by (intro prod.mono_neutral_left) (auto simp: prime_factors_multiplicity) finally have "normalize n = p ^ multiplicity p n" by auto with assms show False by auto qed +text \Now a string of results due to Jakub Kądziołka\ + +lemma multiplicity_dvd_iff_dvd: + assumes "x \ 0" + shows "p^k dvd x \ p^k dvd p^multiplicity p x" +proof (cases "is_unit p") + case True + then have "is_unit (p^k)" + using is_unit_power_iff by simp + hence "p^k dvd x" + by auto + moreover from `is_unit p` have "p^k dvd p^multiplicity p x" + using multiplicity_unit_left is_unit_power_iff by simp + ultimately show ?thesis by simp +next + case False + show ?thesis + proof (cases "p = 0") + case True + then have "p^multiplicity p x = 1" + by simp + moreover have "p^k dvd x \ k = 0" + proof (rule ccontr) + assume "p^k dvd x" and "k \ 0" + with `p = 0` have "p^k = 0" by auto + with `p^k dvd x` have "0 dvd x" by auto + hence "x = 0" by auto + with `x \ 0` show False by auto + qed + ultimately show ?thesis + by (auto simp add: is_unit_power_iff `\ is_unit p`) + next + case False + with `x \ 0` `\ is_unit p` show ?thesis + by (simp add: power_dvd_iff_le_multiplicity dvd_power_iff multiplicity_same_power) + qed +qed + +lemma multiplicity_decomposeI: + assumes "x = p^k * x'" and "\ p dvd x'" and "p \ 0" + shows "multiplicity p x = k" + using assms local.multiplicity_eqI local.power_Suc2 by force + +lemma multiplicity_sum_lt: + assumes "multiplicity p a < multiplicity p b" "a \ 0" "b \ 0" + shows "multiplicity p (a + b) = multiplicity p a" +proof - + let ?vp = "multiplicity p" + have unit: "\ is_unit p" + proof + assume "is_unit p" + then have "?vp a = 0" and "?vp b = 0" using multiplicity_unit_left by auto + with assms show False by auto + qed + + from multiplicity_decompose' obtain a' where a': "a = p^?vp a * a'" "\ p dvd a'" + using unit assms by metis + from multiplicity_decompose' obtain b' where b': "b = p^?vp b * b'" + using unit assms by metis + + show "?vp (a + b) = ?vp a" + proof (rule multiplicity_decomposeI) + let ?k = "?vp b - ?vp a" + from assms have k: "?k > 0" by simp + with b' have "b = p^?vp a * p^?k * b'" + by (simp flip: power_add) + with a' show *: "a + b = p^?vp a * (a' + p^?k * b')" + by (simp add: ac_simps distrib_left) + moreover show "\ p dvd a' + p^?k * b'" + using a' k dvd_add_left_iff by auto + show "p \ 0" using assms by auto + qed +qed + +corollary multiplicity_sum_min: + assumes "multiplicity p a \ multiplicity p b" "a \ 0" "b \ 0" + shows "multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)" +proof - + let ?vp = "multiplicity p" + from assms have "?vp a < ?vp b \ ?vp a > ?vp b" + by auto + then show ?thesis + by (metis assms multiplicity_sum_lt min.commute add_commute min.strict_order_iff) +qed + end end