diff --git a/CONTRIBUTORS b/CONTRIBUTORS --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -1,999 +1,1002 @@ 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 -------------------------------------- +* December 2020 Walter Guttmann + Extension of session HOL/Hoare with total correctness proof system + * 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 Use veriT in proof preplay in Sledgehammer. * October 2020: Mathias Fleury Updated proof reconstruction for the SMT solver veriT in the smt method. * October 2020: Jasmin Blanchette, Martin Desharnais Integration of E 2.5 for Sledgehammer. * September 2020: Florian Haftmann Substantial reworking and modularization of Word library, with generic type conversions. * August 2020: Makarius Wenzel Improved monitoring of runtime statistics: ML GC progress and Java. * July 2020: Martin Desharnais Integration of Metis 2.4. * June 2020: Makarius Wenzel Batch-builds via "isabelle build" allow to invoke Scala from ML. * June 2020: Florian Haftmann Simproc defined_all for more aggressive substitution with variables from assumptions. * May 2020: Makarius Wenzel Antiquotations for Isabelle systems programming, notably @{scala_function} and @{scala} to invoke Scala from ML. * May 2020: Florian Haftmann Generic algebraically founded bit operations NOT, AND, OR, XOR. Contributions to Isabelle2020 ----------------------------- * February 2020: E. Gunther, M. Pagano and P. Sánchez Terraf Simplified, generalised version of ZF/Constructible. * January 2020: LC Paulson The full finite Ramsey's theorem and elements of finite and infinite Ramsey theory. * December 2019: Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel Extension of lift_bnf to support quotient types. * November 2019: Peter Zeller, TU Kaiserslautern Update of Isabelle/VSCode to WebviewPanel API. * October..December 2019: Makarius Wenzel Isabelle/Phabrictor server setup, including Linux platform support in Isabelle/Scala. Client-side tool "isabelle hg_setup". * October 2019: Maximilian Schäffeler Port of the HOL Light decision procedure for metric spaces. * October 2019: Makarius Wenzel More scalable Isabelle dump and underlying headless PIDE session. * August 2019: Makarius Wenzel Better support for proof terms in Isabelle/Pure, notably via method combinator SUBPROOFS (ML) and "subproofs" (Isar). * July 2019: Alexander Krauss, Makarius Wenzel Minimal support for a soft-type system within the Isabelle logical framework. Contributions to Isabelle2019 ----------------------------- * April 2019: LC Paulson Homology and supporting lemmas on topology and group theory * April 2019: Paulo de Vilhena and Martin Baillon Group theory developments, esp. algebraic closure of a field * February/March 2019: Makarius Wenzel Stateless management of export artifacts in the Isabelle/HOL code generator. * February 2019: Manuel Eberl Exponentiation by squaring, used to implement "power" in monoid_mult and fast modular exponentiation. * February 2019: Manuel Eberl Carmichael's function, primitive roots in residue rings, more properties of the order in residue rings. * February 2019: Jeremy Sylvestre Formal Laurent Series and overhaul of Formal power series. * January 2019: Florian Haftmann Clarified syntax and congruence rules for big operators on sets involving the image operator. * January 2019: Florian Haftmann Renovation of code generation, particularly export into session data and proper strings and proper integers based on zarith for OCaml. * January 2019: Andreas Lochbihler New implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm. * November/December 2018: Makarius Wenzel Support for Isabelle/Haskell applications of Isabelle/PIDE. * August/September 2018: Makarius Wenzel Improvements of headless Isabelle/PIDE session and server, and systematic exports from theory documents. * December 2018: Florian Haftmann Generic executable sorting algorithms based on executable comparators. * October 2018: Mathias Fleury Proof reconstruction for the SMT solver veriT in the smt method. Contributions to Isabelle2018 ----------------------------- * July 2018: Manuel Eberl "real_asymp" proof method for automatic proofs of real limits, "Big-O" statements, etc. * June 2018: Fabian Immler More tool support for HOL-Types_To_Sets. * June 2018: Martin Baillon and Paulo Emílio de Vilhena A variety of contributions to HOL-Algebra. * June 2018: Wenda Li New/strengthened results involving analysis, topology, etc. * May/June 2018: Makarius Wenzel System infrastructure to export blobs as theory presentation, and to dump PIDE database content in batch mode. * May 2018: Manuel Eberl Landau symbols and asymptotic equivalence (moved from the AFP). * May 2018: Jose Divasón (Universidad de la Rioja), Jesús Aransay (Universidad de la Rioja), Johannes Hölzl (VU Amsterdam), Fabian Immler (TUM) Generalizations in the formalization of linear algebra. * May 2018: Florian Haftmann Consolidation of string-like types in HOL. * May 2018: Andreas Lochbihler (Digital Asset), Pascal Stoop (ETH Zurich) Code generation with lazy evaluation semantics. * March 2018: Florian Haftmann Abstract bit operations push_bit, take_bit, drop_bit, alongside with an algebraic foundation for bit strings and word types in HOL-ex. * March 2018: Viorel Preoteasa Generalisation of complete_distrib_lattice * February 2018: Wenda Li A unified definition for the order of zeros and poles. Improved reasoning around non-essential singularities. * January 2018: Sebastien Gouezel Various small additions to HOL-Analysis * December 2017: Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel A new conditional parametricity prover. * October 2017: Alexander Maletzky Derivation of axiom "iff" in theory HOL.HOL from the other axioms. Contributions to Isabelle2017 ----------------------------- * September 2017: Lawrence Paulson HOL-Analysis, e.g. simplicial complexes, Jordan Curve Theorem. * September 2017: Jasmin Blanchette Further integration of Nunchaku model finder. * November 2016 - June 2017: Makarius Wenzel New Isabelle/VSCode, with underlying restructuring of Isabelle/PIDE. * 2017: Makarius Wenzel Session-qualified theory names (theory imports and ROOT files). Prover IDE improvements. Support for SQL databases in Isabelle/Scala: SQLite and PostgreSQL. * August 2017: Andreas Lochbihler, ETH Zurich type of unordered pairs (HOL-Library.Uprod) * August 2017: Manuel Eberl, TUM HOL-Analysis: infinite products over natural numbers, infinite sums over arbitrary sets, connection between formal power series and analytic complex functions * March 2017: Alasdair Armstrong, University of Sheffield and Simon Foster, University of York Fixed-point theory and Galois Connections in HOL-Algebra. * February 2017: Florian Haftmann, TUM Statically embedded computations implemented by generated code. Contributions to Isabelle2016-1 ------------------------------- * December 2016: Ondřej Kunčar, TUM Types_To_Sets: experimental extension of Higher-Order Logic to allow translation of types to sets. * October 2016: Jasmin Blanchette Integration of Nunchaku model finder. * October 2016: Jaime Mendizabal Roche, TUM Ported remaining theories of session Old_Number_Theory to the new Number_Theory and removed Old_Number_Theory. * September 2016: Sascha Boehme Proof method "argo" based on SMT technology for a combination of quantifier-free propositional logic, equality and linear real arithmetic * July 2016: Daniel Stuewe Height-size proofs in HOL-Data_Structures. * July 2016: Manuel Eberl, TUM Algebraic foundation for primes; generalization from nat to general factorial rings. * June 2016: Andreas Lochbihler, ETH Zurich Formalisation of discrete subprobability distributions. * June 2016: Florian Haftmann, TUM Improvements to code generation: optional timing measurements, more succint closures for static evaluation, less ambiguities concering Scala implicits. * May 2016: Manuel Eberl, TUM Code generation for Probability Mass Functions. * March 2016: Florian Haftmann, TUM Abstract factorial rings with unique factorization. * March 2016: Florian Haftmann, TUM Reworking of the HOL char type as special case of a finite numeral type. * March 2016: Andreas Lochbihler, ETH Zurich Reasoning support for monotonicity, continuity and admissibility in chain-complete partial orders. * February - October 2016: Makarius Wenzel Prover IDE improvements. ML IDE improvements: bootstrap of Pure. Isar language consolidation. Notational modernization of HOL. Tight Poly/ML integration. More Isabelle/Scala system programming modules (e.g. SSH, Mercurial). * Winter 2016: Jasmin Blanchette, Inria & LORIA & MPII, Aymeric Bouzy, Ecole polytechnique, Andreas Lochbihler, ETH Zurich, Andrei Popescu, Middlesex University, and Dmitriy Traytel, ETH Zurich 'corec' command and friends. * January 2016: Florian Haftmann, TUM Abolition of compound operators INFIMUM and SUPREMUM for complete lattices. Contributions to Isabelle2016 ----------------------------- * Winter 2016: Manuel Eberl, TUM Support for real exponentiation ("powr") in the "approximation" method. (This was removed in Isabelle 2015 due to a changed definition of "powr".) * Summer 2015 - Winter 2016: Lawrence C Paulson, Cambridge General, homology form of Cauchy's integral theorem and supporting material (ported from HOL Light). * Winter 2015/16: Gerwin Klein, NICTA New print_record command. * May - December 2015: Makarius Wenzel Prover IDE improvements. More Isar language elements. Document language refinements. Poly/ML debugger integration. Improved multi-platform and multi-architecture support. * Winter 2015: Manuel Eberl, TUM The radius of convergence of power series and various summability tests. Harmonic numbers and the Euler-Mascheroni constant. The Generalised Binomial Theorem. The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and their most important properties. * Autumn 2015: Manuel Eberl, TUM Proper definition of division (with remainder) for formal power series; Euclidean Ring and GCD instance for formal power series. * Autumn 2015: Florian Haftmann, TUM Rewrite definitions for global interpretations and sublocale declarations. * Autumn 2015: Andreas Lochbihler Bourbaki-Witt fixpoint theorem for increasing functions on chain-complete partial orders. * Autumn 2015: Chaitanya Mangla, Lawrence C Paulson, and Manuel Eberl A large number of additional binomial identities. * Summer 2015: Daniel Matichuk, NICTA and Makarius Wenzel Isar subgoal command for proof structure within unstructured proof scripts. * Summer 2015: Florian Haftmann, TUM Generic partial division in rings as inverse operation of multiplication. * Summer 2015: Manuel Eberl and Florian Haftmann, TUM Type class hierarchy with common algebraic notions of integral (semi)domains like units, associated elements and normalization wrt. units. * Summer 2015: Florian Haftmann, TUM Fundamentals of abstract type class for factorial rings. * Summer 2015: Julian Biendarra, TUM and Dmitriy Traytel, ETH Zurich Command to lift a BNF structure on the raw type to the abstract type for typedefs. * Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM Proof of the central limit theorem: includes weak convergence, characteristic functions, and Levy's uniqueness and continuity theorem. Contributions to Isabelle2015 ----------------------------- * 2014/2015: Daniel Matichuk, Toby Murray, NICTA and Makarius Wenzel The Eisbach proof method language and "match" method. * Winter 2014 and Spring 2015: Ondrej Kuncar, TUM Extension of lift_definition to execute lifted functions that have as a return type a datatype containing a subtype. * March 2015: Jasmin Blanchette, Inria & LORIA & MPII, Mathias Fleury, MPII, and Dmitriy Traytel, TUM More multiset theorems, syntax, and operations. * December 2014: Johannes Hölzl, Manuel Eberl, Sudeep Kanav, TUM, and Jeremy Avigad, Luke Serafin, CMU Various integration theorems: mostly integration on intervals and substitution. * September 2014: Florian Haftmann, TUM Lexicographic order on functions and sum/product over function bodies. * August 2014: Andreas Lochbihler, ETH Zurich Test infrastructure for executing generated code in target languages. * August 2014: Manuel Eberl, TUM Generic euclidean algorithms for GCD et al. Contributions to Isabelle2014 ----------------------------- * July 2014: Thomas Sewell, NICTA Preserve equality hypotheses in "clarify" and friends. New "hypsubst_thin" method configuration option. * Summer 2014: Florian Haftmann, TUM Consolidation and generalization of facts concerning (abelian) semigroups and monoids, particularly products (resp. sums) on finite sets. * Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM Work on exotic automatic theorem provers for Sledgehammer (LEO-II, veriT, Waldmeister, etc.). * June 2014: Florian Haftmann, TUM Internal reorganisation of the local theory / named target stack. * June 2014: Sudeep Kanav, TUM, Jeremy Avigad, CMU, and Johannes Hölzl, TUM Various properties of exponentially, Erlang, and normal distributed random variables. * May 2014: Cezary Kaliszyk, University of Innsbruck, and Jasmin Blanchette, TUM SML-based engines for MaSh. * March 2014: René Thiemann Improved code generation for multisets. * February 2014: Florian Haftmann, TUM Permanent interpretation inside theory, locale and class targets with mixin definitions. * Spring 2014: Lawrence C Paulson, Cambridge Theory Complex_Basic_Analysis. Tidying up Number_Theory vs Old_Number_Theory * Winter 2013 and Spring 2014: Ondrej Kuncar, TUM Various improvements to Lifting/Transfer, integration with the BNF package. * Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE. * Fall 2013 and Winter 2014: Martin Desharnais, Lorenz Panny, Dmitriy Traytel, and Jasmin Blanchette, TUM Various improvements to the BNF-based (co)datatype package, including a more polished "primcorec" command, optimizations, and integration in the "HOL" session. * Winter/Spring 2014: Sascha Boehme, QAware GmbH, and Jasmin Blanchette, TUM "SMT2" module and "smt2" proof method, based on SMT-LIB 2 and Z3 4.3. * January 2014: Lars Hupel, TUM An improved, interactive simplifier trace with integration into the Isabelle/jEdit Prover IDE. * December 2013: Florian Haftmann, TUM Consolidation of abstract interpretations concerning min and max. * November 2013: Florian Haftmann, TUM Abolition of negative numeral literals in the logic. Contributions to Isabelle2013-1 ------------------------------- * September 2013: Lars Noschinski, TUM Conversion between function definitions as list of equations and case expressions in HOL. New library Simps_Case_Conv with commands case_of_simps, simps_of_case. * September 2013: Nik Sultana, University of Cambridge Improvements to HOL/TPTP parser and import facilities. * September 2013: Johannes Hölzl and Dmitriy Traytel, TUM New "coinduction" method (residing in HOL-BNF) to avoid boilerplate. * Summer 2013: Makarius Wenzel, Université Paris-Sud / LRI Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE. * Summer 2013: Manuel Eberl, TUM Generation of elimination rules in the function package. New command "fun_cases". * Summer 2013: Christian Sternagel, JAIST Improved support for ad hoc overloading of constants, including documentation and examples. * Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and Jasmin Blanchette, TUM Various improvements to the BNF-based (co)datatype package, including "primrec_new" and "primcorec" commands and a compatibility layer. * Spring and Summer 2013: Ondrej Kuncar, TUM Various improvements of Lifting and Transfer packages. * Spring 2013: Brian Huffman, Galois Inc. Improvements of the Transfer package. * Summer 2013: Daniel Kühlwein, ICIS, Radboud University Nijmegen Jasmin Blanchette, TUM Various improvements to MaSh, including a server mode. * First half of 2013: Steffen Smolka, TUM Further improvements to Sledgehammer's Isar proof generator. * May 2013: Florian Haftmann, TUM Ephemeral interpretation in local theories. * May 2013: Lukas Bulwahn and Nicolai Schaffroth, TUM Spec_Check: A Quickcheck tool for Isabelle/ML. * April 2013: Stefan Berghofer, secunet Security Networks AG Dmitriy Traytel, TUM Makarius Wenzel, Université Paris-Sud / LRI Case translations as a separate check phase independent of the datatype package. * March 2013: Florian Haftmann, TUM Reform of "big operators" on sets. * March 2013: Florian Haftmann, TUM Algebraic locale hierarchy for orderings and (semi)lattices. * February 2013: Florian Haftmann, TUM Reworking and consolidation of code generation for target language numerals. * February 2013: Florian Haftmann, TUM Sieve of Eratosthenes. Contributions to Isabelle2013 ----------------------------- * 2012: Makarius Wenzel, Université Paris-Sud / LRI Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE. * Fall 2012: Daniel Kühlwein, ICIS, Radboud University Nijmegen Jasmin Blanchette, TUM Implemented Machine Learning for Sledgehammer (MaSh). * Fall 2012: Steffen Smolka, TUM Various improvements to Sledgehammer's Isar proof generator, including a smart type annotation algorithm and proof shrinking. * December 2012: Alessandro Coglio, Kestrel Contributions to HOL's Lattice library. * November 2012: Fabian Immler, TUM "Symbols" dockable for Isabelle/jEdit. * November 2012: Fabian Immler, TUM Proof of the Daniell-Kolmogorov theorem: the existence of the limit of projective families. * October 2012: Andreas Lochbihler, KIT Efficient construction of red-black trees from sorted associative lists. * September 2012: Florian Haftmann, TUM Lattice instances for type option. * September 2012: Christian Sternagel, JAIST Consolidated HOL/Library (theories: Prefix_Order, Sublist, and Sublist_Order) w.r.t. prefixes, suffixes, and embedding on lists. * August 2012: Dmitriy Traytel, Andrei Popescu, Jasmin Blanchette, TUM New BNF-based (co)datatype package. * August 2012: Andrei Popescu and Dmitriy Traytel, TUM Theories of ordinals and cardinals. * July 2012: Makarius Wenzel, Université Paris-Sud / LRI Advanced support for Isabelle sessions and build management, notably "isabelle build". * June 2012: Felix Kuperjans, Lukas Bulwahn, TUM and Rafal Kolanski, NICTA Simproc for rewriting set comprehensions into pointfree expressions. * May 2012: Andreas Lochbihler, KIT Theory of almost everywhere constant functions. * 2010-2012: Markus Kaiser and Lukas Bulwahn, TUM Graphview in Scala/Swing. Contributions to Isabelle2012 ----------------------------- * April 2012: Johannes Hölzl, TUM Probability: Introduced type to represent measures instead of locales. * April 2012: Johannes Hölzl, Fabian Immler, TUM Float: Moved to Dyadic rationals to represent floating point numers. * April 2012: Thomas Sewell, NICTA and 2010: Sascha Boehme, TUM Theory HOL/Word/WordBitwise: logic/circuit expansion of bitvector equalities/inequalities. * March 2012: Christian Sternagel, JAIST Consolidated theory of relation composition. * March 2012: Nik Sultana, University of Cambridge HOL/TPTP parser and import facilities. * March 2012: Cezary Kaliszyk, University of Innsbruck and Alexander Krauss, QAware GmbH Faster and more scalable Import mechanism for HOL Light proofs. * January 2012: Florian Haftmann, TUM, et al. (Re-)Introduction of the "set" type constructor. * 2012: Ondrej Kuncar, TUM New package Lifting, various improvements and refinements to the Quotient package. * 2011/2012: Jasmin Blanchette, TUM Various improvements to Sledgehammer, notably: tighter integration with SPASS, support for more provers (Alt-Ergo, iProver, iProver-Eq). * 2011/2012: Makarius Wenzel, Université Paris-Sud / LRI Various refinements of local theory infrastructure. Improvements of Isabelle/Scala layer and Isabelle/jEdit Prover IDE. Contributions to Isabelle2011-1 ------------------------------- * September 2011: Peter Gammie Theory HOL/Library/Saturated: numbers with saturated arithmetic. * August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM Refined theory on complete lattices. * August 2011: Brian Huffman, Portland State University Miscellaneous cleanup of Complex_Main and Multivariate_Analysis. * June 2011: Brian Huffman, Portland State University Proof method "countable_datatype" for theory Library/Countable. * 2011: Jasmin Blanchette, TUM Various improvements to Sledgehammer, notably: use of sound translations, support for more provers (Waldmeister, LEO-II, Satallax). Further development of Nitpick and 'try' command. * 2011: Andreas Lochbihler, Karlsruhe Institute of Technology Theory HOL/Library/Cset_Monad allows do notation for computable sets (cset) via the generic monad ad-hoc overloading facility. * 2011: Johannes Hölzl, Armin Heller, TUM and Bogdan Grechuk, University of Edinburgh Theory HOL/Library/Extended_Reals: real numbers extended with plus and minus infinity. * 2011: Makarius Wenzel, Université Paris-Sud / LRI Various building blocks for Isabelle/Scala layer and Isabelle/jEdit Prover IDE. Contributions to Isabelle2011 ----------------------------- * January 2011: Stefan Berghofer, secunet Security Networks AG HOL-SPARK: an interactive prover back-end for SPARK. * October 2010: Bogdan Grechuk, University of Edinburgh Extended convex analysis in Multivariate Analysis. * October 2010: Dmitriy Traytel, TUM Coercive subtyping via subtype constraints. * October 2010: Alexander Krauss, TUM Command partial_function for function definitions based on complete partial orders in HOL. * September 2010: Florian Haftmann, TUM Refined concepts for evaluation, i.e., normalization of terms using different techniques. * September 2010: Florian Haftmann, TUM Code generation for Scala. * August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM Improved Probability theory in HOL. * July 2010: Florian Haftmann, TUM Reworking and extension of the Imperative HOL framework. * July 2010: Alexander Krauss, TUM and Christian Sternagel, University of Innsbruck Ad-hoc overloading. Generic do notation for monads. Contributions to Isabelle2009-2 ------------------------------- * 2009/2010: Stefan Berghofer, Alexander Krauss, and Andreas Schropp, TUM, Makarius Wenzel, TUM / LRI Elimination of type classes from proof terms. * April 2010: Florian Haftmann, TUM Reorganization of abstract algebra type classes. * April 2010: Florian Haftmann, TUM Code generation for data representations involving invariants; various collections avaiable in theories Fset, Dlist, RBT, Mapping and AssocList. * March 2010: Sascha Boehme, TUM Efficient SHA1 library for Poly/ML. * February 2010: Cezary Kaliszyk and Christian Urban, TUM Quotient type package for Isabelle/HOL. Contributions to Isabelle2009-1 ------------------------------- * November 2009, Brian Huffman, PSU New definitional domain package for HOLCF. * November 2009: Robert Himmelmann, TUM Derivation and Brouwer's fixpoint theorem in Multivariate Analysis. * November 2009: Stefan Berghofer and Lukas Bulwahn, TUM A tabled implementation of the reflexive transitive closure. * November 2009: Lukas Bulwahn, TUM Predicate Compiler: a compiler for inductive predicates to equational specifications. * November 2009: Sascha Boehme, TUM and Burkhart Wolff, LRI Paris HOL-Boogie: an interactive prover back-end for Boogie and VCC. * October 2009: Jasmin Blanchette, TUM Nitpick: yet another counterexample generator for Isabelle/HOL. * October 2009: Sascha Boehme, TUM Extension of SMT method: proof-reconstruction for the SMT solver Z3. * October 2009: Florian Haftmann, TUM Refinement of parts of the HOL datatype package. * October 2009: Florian Haftmann, TUM Generic term styles for term antiquotations. * September 2009: Thomas Sewell, NICTA More efficient HOL/record implementation. * September 2009: Sascha Boehme, TUM SMT method using external SMT solvers. * September 2009: Florian Haftmann, TUM Refinement of sets and lattices. * July 2009: Jeremy Avigad and Amine Chaieb New number theory. * July 2009: Philipp Meyer, TUM HOL/Library/Sum_Of_Squares: functionality to call a remote csdp prover. * July 2009: Florian Haftmann, TUM New quickcheck implementation using new code generator. * July 2009: Florian Haftmann, TUM HOL/Library/Fset: an explicit type of sets; finite sets ready to use for code generation. * June 2009: Florian Haftmann, TUM HOL/Library/Tree: search trees implementing mappings, ready to use for code generation. * March 2009: Philipp Meyer, TUM Minimization tool for results from Sledgehammer. Contributions to Isabelle2009 ----------------------------- * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of Cambridge Elementary topology in Euclidean space. * March 2009: Johannes Hoelzl, TUM Method "approximation", which proves real valued inequalities by computation. * February 2009: Filip Maric, Univ. of Belgrade A Serbian theory. * February 2009: Jasmin Christian Blanchette, TUM Misc cleanup of HOL/refute. * February 2009: Timothy Bourke, NICTA New find_consts command. * February 2009: Timothy Bourke, NICTA "solves" criterion for find_theorems and auto_solve option * December 2008: Clemens Ballarin, TUM New locale implementation. * December 2008: Armin Heller, TUM and Alexander Krauss, TUM Method "sizechange" for advanced termination proofs. * November 2008: Timothy Bourke, NICTA Performance improvement (factor 50) for find_theorems. * 2008: Florian Haftmann, TUM Various extensions and restructurings in HOL, improvements in evaluation mechanisms, new module binding.ML for name bindings. * October 2008: Fabian Immler, TUM ATP manager for Sledgehammer, based on ML threads instead of Posix processes. Additional ATP wrappers, including remote SystemOnTPTP services. * September 2008: Stefan Berghofer, TUM and Marc Bezem, Univ. Bergen Prover for coherent logic. * August 2008: Fabian Immler, TUM Vampire wrapper script for remote SystemOnTPTP service. Contributions to Isabelle2008 ----------------------------- * 2007/2008: Alexander Krauss, TUM and Florian Haftmann, TUM and Stefan Berghofer, TUM HOL library improvements. * 2007/2008: Brian Huffman, PSU HOLCF library improvements. * 2007/2008: Stefan Berghofer, TUM HOL-Nominal package improvements. * March 2008: Markus Reiter, TUM HOL/Library/RBT: red-black trees. * February 2008: Alexander Krauss, TUM and Florian Haftmann, TUM and Lukas Bulwahn, TUM and John Matthews, Galois: HOL/Library/Imperative_HOL: Haskell-style imperative data structures for HOL. * December 2007: Norbert Schirmer, Uni Saarbruecken Misc improvements of record package in HOL. * December 2007: Florian Haftmann, TUM Overloading and class instantiation target. * December 2007: Florian Haftmann, TUM New version of primrec package for local theories. * December 2007: Alexander Krauss, TUM Method "induction_scheme" in HOL. * November 2007: Peter Lammich, Uni Muenster HOL-Lattice: some more lemmas. Contributions to Isabelle2007 ----------------------------- * October 2007: Norbert Schirmer, TUM / Uni Saarbruecken State Spaces: The Locale Way (in HOL). * October 2007: Mark A. Hillebrand, DFKI Robust sub/superscripts in LaTeX document output. * August 2007: Jeremy Dawson, NICTA and Paul Graunke, Galois and Brian Huffman, PSU and Gerwin Klein, NICTA and John Matthews, Galois HOL-Word: a library for fixed-size machine words in Isabelle. * August 2007: Brian Huffman, PSU HOL/Library/Boolean_Algebra and HOL/Library/Numeral_Type. * June 2007: Amine Chaieb, TUM Semiring normalization and Groebner Bases. Support for dense linear orders. * June 2007: Joe Hurd, Oxford Metis theorem-prover. * 2007: Kong W. Susanto, Cambridge HOL: Metis prover integration. * 2007: Stefan Berghofer, TUM HOL: inductive predicates and sets. * 2007: Norbert Schirmer, TUM HOL/record: misc improvements. * 2006/2007: Alexander Krauss, TUM HOL: function package and related theories on termination. * 2006/2007: Florian Haftmann, TUM Pure: generic code generator framework. Pure: class package. HOL: theory reorganization, code generator setup. * 2006/2007: Christian Urban, TUM and Stefan Berghofer, TUM and Julien Narboux, TUM HOL/Nominal package and related tools. * November 2006: Lukas Bulwahn, TUM HOL: method "lexicographic_order" for function package. * October 2006: Stefan Hohe, TUM HOL-Algebra: ideals and quotients over rings. * August 2006: Amine Chaieb, TUM Experimental support for generic reflection and reification in HOL. * July 2006: Rafal Kolanski, NICTA Hex (0xFF) and binary (0b1011) numerals. * May 2006: Klaus Aehlig, LMU Command 'normal_form': normalization by evaluation. * May 2006: Amine Chaieb, TUM HOL-Complex: Ferrante and Rackoff Algorithm for linear real arithmetic. * February 2006: Benjamin Porter, NICTA HOL and HOL-Complex: generalised mean value theorem, continuum is not denumerable, harmonic and arithmetic series, and denumerability of rationals. * October 2005: Martin Wildmoser, TUM Sketch for Isar 'guess' element. Contributions to Isabelle2005 ----------------------------- * September 2005: Lukas Bulwahn and Bernhard Haeupler, TUM HOL-Complex: Formalization of Taylor series. * September 2005: Stephan Merz, Alwen Tiu, QSL Loria Components for SAT solver method using zChaff. * September 2005: Ning Zhang and Christian Urban, LMU Munich A Chinese theory. * September 2005: Bernhard Haeupler, TUM Method comm_ring for proving equalities in commutative rings. * July/August 2005: Jeremy Avigad, Carnegie Mellon University Various improvements of the HOL and HOL-Complex library. * July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM Some structured proofs about completeness of real numbers. * May 2005: Rafal Kolanski and Gerwin Klein, NICTA Improved retrieval of facts from theory/proof context. * February 2005: Lucas Dixon, University of Edinburgh Improved subst method. * 2005: Brian Huffman, OGI Various improvements of HOLCF. Some improvements of the HOL-Complex library. * 2005: Claire Quigley and Jia Meng, University of Cambridge Some support for asynchronous communication with external provers (experimental). * 2005: Florian Haftmann, TUM Contributions to document 'sugar'. Various ML combinators, notably linear functional transformations. Some cleanup of ML legacy. Additional antiquotations. Improved Isabelle web site. * 2004/2005: David Aspinall, University of Edinburgh Various elements of XML and PGIP based communication with user interfaces (experimental). * 2004/2005: Gerwin Klein, NICTA Contributions to document 'sugar'. Improved Isabelle web site. Improved HTML presentation of theories. * 2004/2005: Clemens Ballarin, TUM Provers: tools for transitive relations and quasi orders. Improved version of locales, notably interpretation of locales. Improved version of HOL-Algebra. * 2004/2005: Amine Chaieb, TUM Improved version of HOL presburger method. * 2004/2005: Steven Obua, TUM Improved version of HOL/Import, support for HOL-Light. Improved version of HOL-Complex-Matrix. Pure/defs: more sophisticated checks on well-formedness of overloading. Pure/Tools: an experimental evaluator for lambda terms. * 2004/2005: Norbert Schirmer, TUM Contributions to document 'sugar'. Improved version of HOL/record. * 2004/2005: Sebastian Skalberg, TUM Improved version of HOL/Import. Some internal ML reorganizations. * 2004/2005: Tjark Weber, TUM SAT solver method using zChaff. Improved version of HOL/refute. :maxLineLen=78: diff --git a/src/HOL/Data_Structures/Tree23_Map.thy b/src/HOL/Data_Structures/Tree23_Map.thy --- a/src/HOL/Data_Structures/Tree23_Map.thy +++ b/src/HOL/Data_Structures/Tree23_Map.thy @@ -1,141 +1,141 @@ (* Author: Tobias Nipkow *) section \2-3 Tree Implementation of Maps\ theory Tree23_Map imports Tree23_Set Map_Specs begin fun lookup :: "('a::linorder * 'b) tree23 \ 'a \ 'b option" where "lookup Leaf x = None" | "lookup (Node2 l (a,b) r) x = (case cmp x a of LT \ lookup l x | GT \ lookup r x | EQ \ Some b)" | "lookup (Node3 l (a1,b1) m (a2,b2) r) x = (case cmp x a1 of LT \ lookup l x | EQ \ Some b1 | GT \ (case cmp x a2 of LT \ lookup m x | EQ \ Some b2 | GT \ lookup r x))" fun upd :: "'a::linorder \ 'b \ ('a*'b) tree23 \ ('a*'b) upI" where "upd x y Leaf = OF Leaf (x,y) Leaf" | "upd x y (Node2 l ab r) = (case cmp x (fst ab) of LT \ (case upd x y l of TI l' => TI (Node2 l' ab r) | OF l1 ab' l2 => TI (Node3 l1 ab' l2 ab r)) | EQ \ TI (Node2 l (x,y) r) | GT \ (case upd x y r of TI r' => TI (Node2 l ab r') | OF r1 ab' r2 => TI (Node3 l ab r1 ab' r2)))" | "upd x y (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of LT \ (case upd x y l of TI l' => TI (Node3 l' ab1 m ab2 r) | OF l1 ab' l2 => OF (Node2 l1 ab' l2) ab1 (Node2 m ab2 r)) | EQ \ TI (Node3 l (x,y) m ab2 r) | GT \ (case cmp x (fst ab2) of LT \ (case upd x y m of TI m' => TI (Node3 l ab1 m' ab2 r) | OF m1 ab' m2 => OF (Node2 l ab1 m1) ab' (Node2 m2 ab2 r)) | EQ \ TI (Node3 l ab1 m (x,y) r) | GT \ (case upd x y r of TI r' => TI (Node3 l ab1 m ab2 r') | OF r1 ab' r2 => OF (Node2 l ab1 m) ab2 (Node2 r1 ab' r2))))" definition update :: "'a::linorder \ 'b \ ('a*'b) tree23 \ ('a*'b) tree23" where "update a b t = treeI(upd a b t)" fun del :: "'a::linorder \ ('a*'b) tree23 \ ('a*'b) upD" where "del x Leaf = TD Leaf" | "del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then UF Leaf else TD(Node2 Leaf ab1 Leaf))" | "del x (Node3 Leaf ab1 Leaf ab2 Leaf) = TD(if x=fst ab1 then Node2 Leaf ab2 Leaf else if x=fst ab2 then Node2 Leaf ab1 Leaf else Node3 Leaf ab1 Leaf ab2 Leaf)" | "del x (Node2 l ab1 r) = (case cmp x (fst ab1) of LT \ node21 (del x l) ab1 r | GT \ node22 l ab1 (del x r) | EQ \ let (ab1',t) = split_min r in node22 l ab1' t)" | "del x (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of LT \ node31 (del x l) ab1 m ab2 r | EQ \ let (ab1',m') = split_min m in node32 l ab1' m' ab2 r | GT \ (case cmp x (fst ab2) of LT \ node32 l ab1 (del x m) ab2 r | EQ \ let (ab2',r') = split_min r in node33 l ab1 m ab2' r' | GT \ node33 l ab1 m ab2 (del x r)))" definition delete :: "'a::linorder \ ('a*'b) tree23 \ ('a*'b) tree23" where "delete x t = treeD(del x t)" subsection \Functional Correctness\ lemma lookup_map_of: "sorted1(inorder t) \ lookup t x = map_of (inorder t) x" by (induction t) (auto simp: map_of_simps split: option.split) lemma inorder_upd: "sorted1(inorder t) \ inorder(treeI(upd x y t)) = upd_list x y (inorder t)" by(induction t) (auto simp: upd_list_simps split: upI.splits) corollary inorder_update: "sorted1(inorder t) \ inorder(update x y t) = upd_list x y (inorder t)" by(simp add: update_def inorder_upd) lemma inorder_del: "\ complete t ; sorted1(inorder t) \ \ inorder(treeD (del x t)) = del_list x (inorder t)" by(induction t rule: del.induct) (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits) corollary inorder_delete: "\ complete t ; sorted1(inorder t) \ \ inorder(delete x t) = del_list x (inorder t)" by(simp add: delete_def inorder_del) subsection \Balancedness\ -lemma complete_upd: "complete t \ complete (treeI(upd x y t)) \ height(upd x y t) = height t" +lemma complete_upd: "complete t \ complete (treeI(upd x y t)) \ hI(upd x y t) = height t" by (induct t) (auto split!: if_split upI.split)(* 16 secs in 2015 *) corollary complete_update: "complete t \ complete (update x y t)" by (simp add: update_def complete_upd) -lemma height_del: "complete t \ height(del x t) = height t" +lemma height_del: "complete t \ hD(del x t) = height t" by(induction x t rule: del.induct) (auto simp add: heights max_def height_split_min split: prod.split) lemma complete_treeD_del: "complete t \ complete(treeD(del x t))" by(induction x t rule: del.induct) (auto simp: completes complete_split_min height_del height_split_min split: prod.split) corollary complete_delete: "complete t \ complete(delete x t)" by(simp add: delete_def complete_treeD_del) subsection \Overall Correctness\ interpretation M: Map_by_Ordered where empty = empty and lookup = lookup and update = update and delete = delete and inorder = inorder and inv = complete proof (standard, goal_cases) case 1 thus ?case by(simp add: empty_def) next case 2 thus ?case by(simp add: lookup_map_of) next case 3 thus ?case by(simp add: inorder_update) next case 4 thus ?case by(simp add: inorder_delete) next case 5 thus ?case by(simp add: empty_def) next case 6 thus ?case by(simp add: complete_update) next case 7 thus ?case by(simp add: complete_delete) qed end diff --git a/src/HOL/Data_Structures/Tree23_Set.thy b/src/HOL/Data_Structures/Tree23_Set.thy --- a/src/HOL/Data_Structures/Tree23_Set.thy +++ b/src/HOL/Data_Structures/Tree23_Set.thy @@ -1,395 +1,381 @@ (* Author: Tobias Nipkow *) section \2-3 Tree Implementation of Sets\ theory Tree23_Set imports Tree23 Cmp Set_Specs begin declare sorted_wrt.simps(2)[simp del] definition empty :: "'a tree23" where "empty = Leaf" fun isin :: "'a::linorder tree23 \ 'a \ bool" where "isin Leaf x = False" | "isin (Node2 l a r) x = (case cmp x a of LT \ isin l x | EQ \ True | GT \ isin r x)" | "isin (Node3 l a m b r) x = (case cmp x a of LT \ isin l x | EQ \ True | GT \ (case cmp x b of LT \ isin m x | EQ \ True | GT \ isin r x))" datatype 'a upI = TI "'a tree23" | OF "'a tree23" 'a "'a tree23" fun treeI :: "'a upI \ 'a tree23" where "treeI (TI t) = t" | "treeI (OF l a r) = Node2 l a r" fun ins :: "'a::linorder \ 'a tree23 \ 'a upI" where "ins x Leaf = OF Leaf x Leaf" | "ins x (Node2 l a r) = (case cmp x a of LT \ (case ins x l of TI l' => TI (Node2 l' a r) | OF l1 b l2 => TI (Node3 l1 b l2 a r)) | - EQ \ TI (Node2 l x r) | + EQ \ TI (Node2 l a r) | GT \ (case ins x r of TI r' => TI (Node2 l a r') | OF r1 b r2 => TI (Node3 l a r1 b r2)))" | "ins x (Node3 l a m b r) = (case cmp x a of LT \ (case ins x l of TI l' => TI (Node3 l' a m b r) | OF l1 c l2 => OF (Node2 l1 c l2) a (Node2 m b r)) | EQ \ TI (Node3 l a m b r) | GT \ (case cmp x b of GT \ (case ins x r of TI r' => TI (Node3 l a m b r') | OF r1 c r2 => OF (Node2 l a m) b (Node2 r1 c r2)) | EQ \ TI (Node3 l a m b r) | LT \ (case ins x m of TI m' => TI (Node3 l a m' b r) | OF m1 c m2 => OF (Node2 l a m1) c (Node2 m2 b r))))" hide_const insert definition insert :: "'a::linorder \ 'a tree23 \ 'a tree23" where "insert x t = treeI(ins x t)" datatype 'a upD = TD "'a tree23" | UF "'a tree23" fun treeD :: "'a upD \ 'a tree23" where "treeD (TD t) = t" | "treeD (UF t) = t" (* Variation: return None to signal no-change *) fun node21 :: "'a upD \ 'a \ 'a tree23 \ 'a upD" where "node21 (TD t1) a t2 = TD(Node2 t1 a t2)" | "node21 (UF t1) a (Node2 t2 b t3) = UF(Node3 t1 a t2 b t3)" | "node21 (UF t1) a (Node3 t2 b t3 c t4) = TD(Node2 (Node2 t1 a t2) b (Node2 t3 c t4))" fun node22 :: "'a tree23 \ 'a \ 'a upD \ 'a upD" where "node22 t1 a (TD t2) = TD(Node2 t1 a t2)" | "node22 (Node2 t1 b t2) a (UF t3) = UF(Node3 t1 b t2 a t3)" | "node22 (Node3 t1 b t2 c t3) a (UF t4) = TD(Node2 (Node2 t1 b t2) c (Node2 t3 a t4))" fun node31 :: "'a upD \ 'a \ 'a tree23 \ 'a \ 'a tree23 \ 'a upD" where "node31 (TD t1) a t2 b t3 = TD(Node3 t1 a t2 b t3)" | "node31 (UF t1) a (Node2 t2 b t3) c t4 = TD(Node2 (Node3 t1 a t2 b t3) c t4)" | "node31 (UF t1) a (Node3 t2 b t3 c t4) d t5 = TD(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)" fun node32 :: "'a tree23 \ 'a \ 'a upD \ 'a \ 'a tree23 \ 'a upD" where "node32 t1 a (TD t2) b t3 = TD(Node3 t1 a t2 b t3)" | "node32 t1 a (UF t2) b (Node2 t3 c t4) = TD(Node2 t1 a (Node3 t2 b t3 c t4))" | "node32 t1 a (UF t2) b (Node3 t3 c t4 d t5) = TD(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" fun node33 :: "'a tree23 \ 'a \ 'a tree23 \ 'a \ 'a upD \ 'a upD" where "node33 l a m b (TD r) = TD(Node3 l a m b r)" | "node33 t1 a (Node2 t2 b t3) c (UF t4) = TD(Node2 t1 a (Node3 t2 b t3 c t4))" | "node33 t1 a (Node3 t2 b t3 c t4) d (UF t5) = TD(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" fun split_min :: "'a tree23 \ 'a * 'a upD" where "split_min (Node2 Leaf a Leaf) = (a, UF Leaf)" | "split_min (Node3 Leaf a Leaf b Leaf) = (a, TD(Node2 Leaf b Leaf))" | "split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" | "split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))" text \In the base cases of \split_min\ and \del\ it is enough to check if one subtree is a \Leaf\, in which case completeness implies that so are the others. Exercise.\ fun del :: "'a::linorder \ 'a tree23 \ 'a upD" where "del x Leaf = TD Leaf" | "del x (Node2 Leaf a Leaf) = (if x = a then UF Leaf else TD(Node2 Leaf a Leaf))" | "del x (Node3 Leaf a Leaf b Leaf) = TD(if x = a then Node2 Leaf b Leaf else if x = b then Node2 Leaf a Leaf else Node3 Leaf a Leaf b Leaf)" | "del x (Node2 l a r) = (case cmp x a of LT \ node21 (del x l) a r | GT \ node22 l a (del x r) | EQ \ let (a',r') = split_min r in node22 l a' r')" | "del x (Node3 l a m b r) = (case cmp x a of LT \ node31 (del x l) a m b r | EQ \ let (a',m') = split_min m in node32 l a' m' b r | GT \ (case cmp x b of LT \ node32 l a (del x m) b r | EQ \ let (b',r') = split_min r in node33 l a m b' r' | GT \ node33 l a m b (del x r)))" definition delete :: "'a::linorder \ 'a tree23 \ 'a tree23" where "delete x t = treeD(del x t)" subsection "Functional Correctness" subsubsection "Proofs for isin" lemma isin_set: "sorted(inorder t) \ isin t x = (x \ set (inorder t))" by (induction t) (auto simp: isin_simps) subsubsection "Proofs for insert" lemma inorder_ins: "sorted(inorder t) \ inorder(treeI(ins x t)) = ins_list x (inorder t)" by(induction t) (auto simp: ins_list_simps split: upI.splits) lemma inorder_insert: "sorted(inorder t) \ inorder(insert a t) = ins_list a (inorder t)" by(simp add: insert_def inorder_ins) subsubsection "Proofs for delete" lemma inorder_node21: "height r > 0 \ inorder (treeD (node21 l' a r)) = inorder (treeD l') @ a # inorder r" by(induct l' a r rule: node21.induct) auto lemma inorder_node22: "height l > 0 \ inorder (treeD (node22 l a r')) = inorder l @ a # inorder (treeD r')" by(induct l a r' rule: node22.induct) auto lemma inorder_node31: "height m > 0 \ inorder (treeD (node31 l' a m b r)) = inorder (treeD l') @ a # inorder m @ b # inorder r" by(induct l' a m b r rule: node31.induct) auto lemma inorder_node32: "height r > 0 \ inorder (treeD (node32 l a m' b r)) = inorder l @ a # inorder (treeD m') @ b # inorder r" by(induct l a m' b r rule: node32.induct) auto lemma inorder_node33: "height m > 0 \ inorder (treeD (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (treeD r')" by(induct l a m b r' rule: node33.induct) auto lemmas inorder_nodes = inorder_node21 inorder_node22 inorder_node31 inorder_node32 inorder_node33 lemma split_minD: "split_min t = (x,t') \ complete t \ height t > 0 \ x # inorder(treeD t') = inorder t" by(induction t arbitrary: t' rule: split_min.induct) (auto simp: inorder_nodes split: prod.splits) lemma inorder_del: "\ complete t ; sorted(inorder t) \ \ inorder(treeD (del x t)) = del_list x (inorder t)" by(induction t rule: del.induct) (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits) lemma inorder_delete: "\ complete t ; sorted(inorder t) \ \ inorder(delete x t) = del_list x (inorder t)" by(simp add: delete_def inorder_del) subsection \Completeness\ subsubsection "Proofs for insert" text\First a standard proof that \<^const>\ins\ preserves \<^const>\complete\.\ -instantiation upI :: (type)height -begin +fun hI :: "'a upI \ nat" where +"hI (TI t) = height t" | +"hI (OF l a r) = height l" -fun height_upI :: "'a upI \ nat" where -"height (TI t) = height t" | -"height (OF l a r) = height l" - -instance .. - -end - -lemma complete_ins: "complete t \ complete (treeI(ins a t)) \ height(ins a t) = height t" +lemma complete_ins: "complete t \ complete (treeI(ins a t)) \ hI(ins a t) = height t" by (induct t) (auto split!: if_split upI.split) (* 15 secs in 2015 *) text\Now an alternative proof (by Brian Huffman) that runs faster because two properties (completeness and height) are combined in one predicate.\ inductive full :: "nat \ 'a tree23 \ bool" where "full 0 Leaf" | "\full n l; full n r\ \ full (Suc n) (Node2 l p r)" | "\full n l; full n m; full n r\ \ full (Suc n) (Node3 l p m q r)" inductive_cases full_elims: "full n Leaf" "full n (Node2 l p r)" "full n (Node3 l p m q r)" inductive_cases full_0_elim: "full 0 t" inductive_cases full_Suc_elim: "full (Suc n) t" lemma full_0_iff [simp]: "full 0 t \ t = Leaf" by (auto elim: full_0_elim intro: full.intros) lemma full_Leaf_iff [simp]: "full n Leaf \ n = 0" by (auto elim: full_elims intro: full.intros) lemma full_Suc_Node2_iff [simp]: "full (Suc n) (Node2 l p r) \ full n l \ full n r" by (auto elim: full_elims intro: full.intros) lemma full_Suc_Node3_iff [simp]: "full (Suc n) (Node3 l p m q r) \ full n l \ full n m \ full n r" by (auto elim: full_elims intro: full.intros) lemma full_imp_height: "full n t \ height t = n" by (induct set: full, simp_all) lemma full_imp_complete: "full n t \ complete t" by (induct set: full, auto dest: full_imp_height) lemma complete_imp_full: "complete t \ full (height t) t" by (induct t, simp_all) lemma complete_iff_full: "complete t \ (\n. full n t)" by (auto elim!: complete_imp_full full_imp_complete) text \The \<^const>\insert\ function either preserves the height of the tree, or increases it by one. The constructor returned by the \<^term>\insert\ function determines which: A return value of the form \<^term>\TI t\ indicates that the height will be the same. A value of the form \<^term>\OF l p r\ indicates an increase in height.\ fun full\<^sub>i :: "nat \ 'a upI \ bool" where "full\<^sub>i n (TI t) \ full n t" | "full\<^sub>i n (OF l p r) \ full n l \ full n r" lemma full\<^sub>i_ins: "full n t \ full\<^sub>i n (ins a t)" by (induct rule: full.induct) (auto split: upI.split) text \The \<^const>\insert\ operation preserves completeance.\ lemma complete_insert: "complete t \ complete (insert a t)" unfolding complete_iff_full insert_def apply (erule exE) apply (drule full\<^sub>i_ins [of _ _ a]) apply (cases "ins a t") apply (auto intro: full.intros) done subsection "Proofs for delete" -instantiation upD :: (type)height -begin - -fun height_upD :: "'a upD \ nat" where -"height (TD t) = height t" | -"height (UF t) = height t + 1" - -instance .. - -end +fun hD :: "'a upD \ nat" where +"hD (TD t) = height t" | +"hD (UF t) = height t + 1" lemma complete_treeD_node21: - "\complete r; complete (treeD l'); height r = height l' \ \ complete (treeD (node21 l' a r))" + "\complete r; complete (treeD l'); height r = hD l' \ \ complete (treeD (node21 l' a r))" by(induct l' a r rule: node21.induct) auto lemma complete_treeD_node22: - "\complete(treeD r'); complete l; height r' = height l \ \ complete (treeD (node22 l a r'))" + "\complete(treeD r'); complete l; hD r' = height l \ \ complete (treeD (node22 l a r'))" by(induct l a r' rule: node22.induct) auto lemma complete_treeD_node31: - "\ complete (treeD l'); complete m; complete r; height l' = height r; height m = height r \ + "\ complete (treeD l'); complete m; complete r; hD l' = height r; height m = height r \ \ complete (treeD (node31 l' a m b r))" by(induct l' a m b r rule: node31.induct) auto lemma complete_treeD_node32: - "\ complete l; complete (treeD m'); complete r; height l = height r; height m' = height r \ + "\ complete l; complete (treeD m'); complete r; height l = height r; hD m' = height r \ \ complete (treeD (node32 l a m' b r))" by(induct l a m' b r rule: node32.induct) auto lemma complete_treeD_node33: - "\ complete l; complete m; complete(treeD r'); height l = height r'; height m = height r' \ + "\ complete l; complete m; complete(treeD r'); height l = hD r'; height m = hD r' \ \ complete (treeD (node33 l a m b r'))" by(induct l a m b r' rule: node33.induct) auto lemmas completes = complete_treeD_node21 complete_treeD_node22 complete_treeD_node31 complete_treeD_node32 complete_treeD_node33 lemma height'_node21: - "height r > 0 \ height(node21 l' a r) = max (height l') (height r) + 1" + "height r > 0 \ hD(node21 l' a r) = max (hD l') (height r) + 1" by(induct l' a r rule: node21.induct)(simp_all) lemma height'_node22: - "height l > 0 \ height(node22 l a r') = max (height l) (height r') + 1" + "height l > 0 \ hD(node22 l a r') = max (height l) (hD r') + 1" by(induct l a r' rule: node22.induct)(simp_all) lemma height'_node31: - "height m > 0 \ height(node31 l a m b r) = - max (height l) (max (height m) (height r)) + 1" + "height m > 0 \ hD(node31 l a m b r) = + max (hD l) (max (height m) (height r)) + 1" by(induct l a m b r rule: node31.induct)(simp_all add: max_def) lemma height'_node32: - "height r > 0 \ height(node32 l a m b r) = - max (height l) (max (height m) (height r)) + 1" + "height r > 0 \ hD(node32 l a m b r) = + max (height l) (max (hD m) (height r)) + 1" by(induct l a m b r rule: node32.induct)(simp_all add: max_def) lemma height'_node33: - "height m > 0 \ height(node33 l a m b r) = - max (height l) (max (height m) (height r)) + 1" + "height m > 0 \ hD(node33 l a m b r) = + max (height l) (max (height m) (hD r)) + 1" by(induct l a m b r rule: node33.induct)(simp_all add: max_def) lemmas heights = height'_node21 height'_node22 height'_node31 height'_node32 height'_node33 lemma height_split_min: - "split_min t = (x, t') \ height t > 0 \ complete t \ height t' = height t" + "split_min t = (x, t') \ height t > 0 \ complete t \ hD t' = height t" by(induct t arbitrary: x t' rule: split_min.induct) (auto simp: heights split: prod.splits) -lemma height_del: "complete t \ height(del x t) = height t" +lemma height_del: "complete t \ hD(del x t) = height t" by(induction x t rule: del.induct) (auto simp: heights max_def height_split_min split: prod.splits) lemma complete_split_min: "\ split_min t = (x, t'); complete t; height t > 0 \ \ complete (treeD t')" by(induct t arbitrary: x t' rule: split_min.induct) (auto simp: heights height_split_min completes split: prod.splits) lemma complete_treeD_del: "complete t \ complete(treeD(del x t))" by(induction x t rule: del.induct) (auto simp: completes complete_split_min height_del height_split_min split: prod.splits) corollary complete_delete: "complete t \ complete(delete x t)" by(simp add: delete_def complete_treeD_del) subsection \Overall Correctness\ interpretation S: Set_by_Ordered where empty = empty and isin = isin and insert = insert and delete = delete and inorder = inorder and inv = complete proof (standard, goal_cases) case 2 thus ?case by(simp add: isin_set) next case 3 thus ?case by(simp add: inorder_insert) next case 4 thus ?case by(simp add: inorder_delete) next case 6 thus ?case by(simp add: complete_insert) next case 7 thus ?case by(simp add: complete_delete) qed (simp add: empty_def)+ end diff --git a/src/HOL/Hoare/ExamplesTC.thy b/src/HOL/Hoare/ExamplesTC.thy new file mode 100644 --- /dev/null +++ b/src/HOL/Hoare/ExamplesTC.thy @@ -0,0 +1,118 @@ +(* Title: Examples using Hoare Logic for Total Correctness + Author: Walter Guttmann +*) + +section \Examples using Hoare Logic for Total Correctness\ + +theory ExamplesTC + +imports Hoare_Logic + +begin + +text \ +This theory demonstrates a few simple partial- and total-correctness proofs. +The first example is taken from HOL/Hoare/Examples.thy written by N. Galm. +We have added the invariant \m \ a\. +\ + +lemma multiply_by_add: "VARS m s a b + {a=A \ b=B} + m := 0; s := 0; + WHILE m\a + INV {s=m*b \ a=A \ b=B \ m\a} + DO s := s+b; m := m+(1::nat) OD + {s = A*B}" + by vcg_simp + +text \ +Here is the total-correctness proof for the same program. +It needs the additional invariant \m \ a\. +\ + +lemma multiply_by_add_tc: "VARS m s a b + [a=A \ b=B] + m := 0; s := 0; + WHILE m\a + INV {s=m*b \ a=A \ b=B \ m\a} + VAR {a-m} + DO s := s+b; m := m+(1::nat) OD + [s = A*B]" + apply vcg_tc_simp + by auto + +text \ +Next, we prove partial correctness of a program that computes powers. +\ + +lemma power: "VARS (p::int) i + { True } + p := 1; + i := 0; + WHILE i < n + INV { p = x^i \ i \ n } + DO p := p * x; + i := i + 1 + OD + { p = x^n }" + apply vcg_simp + by auto + +text \ +Here is its total-correctness proof. +\ + +lemma power_tc: "VARS (p::int) i + [ True ] + p := 1; + i := 0; + WHILE i < n + INV { p = x^i \ i \ n } + VAR { n - i } + DO p := p * x; + i := i + 1 + OD + [ p = x^n ]" + apply vcg_tc + by auto + +text \ +The last example is again taken from HOL/Hoare/Examples.thy. +We have modified it to integers so it requires precondition \0 \ x\. +\ + +lemma sqrt_tc: "VARS r + [0 \ (x::int)] + r := 0; + WHILE (r+1)*(r+1) <= x + INV {r*r \ x} + VAR {nat (x-r)} + DO r := r+1 OD + [r*r \ x \ x < (r+1)*(r+1)]" + apply vcg_tc_simp + by (smt (verit) div_pos_pos_trivial mult_less_0_iff nonzero_mult_div_cancel_left) + +text \ +A total-correctness proof allows us to extract a function for further use. +For every input satisfying the precondition the function returns an output satisfying the postcondition. +\ + +lemma sqrt_exists: + "0 \ (x::int) \ \r' . r'*r' \ x \ x < (r'+1)*(r'+1)" + using tc_extract_function sqrt_tc by blast + +definition "sqrt (x::int) \ (SOME r' . r'*r' \ x \ x < (r'+1)*(r'+1))" + +lemma sqrt_function: + assumes "0 \ (x::int)" + and "r' = sqrt x" + shows "r'*r' \ x \ x < (r'+1)*(r'+1)" +proof - + let ?P = "\r' . r'*r' \ x \ x < (r'+1)*(r'+1)" + have "?P (SOME z . ?P z)" + by (metis (mono_tags, lifting) assms(1) sqrt_exists some_eq_imp) + thus ?thesis + using assms(2) sqrt_def by auto +qed + +end diff --git a/src/HOL/Hoare/Hoare.thy b/src/HOL/Hoare/Hoare.thy --- a/src/HOL/Hoare/Hoare.thy +++ b/src/HOL/Hoare/Hoare.thy @@ -1,9 +1,9 @@ (* Author: Tobias Nipkow Copyright 1998-2003 TUM *) theory Hoare -imports Examples ExamplesAbort Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation +imports Examples ExamplesAbort ExamplesTC Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation begin end diff --git a/src/HOL/Hoare/Hoare_Logic.thy b/src/HOL/Hoare/Hoare_Logic.thy --- a/src/HOL/Hoare/Hoare_Logic.thy +++ b/src/HOL/Hoare/Hoare_Logic.thy @@ -1,107 +1,220 @@ (* Title: HOL/Hoare/Hoare_Logic.thy Author: Leonor Prensa Nieto & Tobias Nipkow Copyright 1998 TUM + Author: Walter Guttmann (extension to total-correctness proofs) Sugared semantic embedding of Hoare logic. Strictly speaking a shallow embedding (as implemented by Norbert Galm following Mike Gordon) would suffice. Maybe the datatype com comes in useful later. *) theory Hoare_Logic imports Main begin type_synonym 'a bexp = "'a set" type_synonym 'a assn = "'a set" +type_synonym 'a var = "'a \ nat" datatype 'a com = Basic "'a \ 'a" | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) -| While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) +| While "'a bexp" "'a assn" "'a var" "'a com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61) + +syntax (xsymbols) + "_whilePC" :: "'a bexp \ 'a assn \ 'a com \ 'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) + +translations + "WHILE b INV {x} DO c OD" => "WHILE b INV {x} VAR {0} DO c OD" abbreviation annskip ("SKIP") where "SKIP == Basic id" type_synonym 'a sem = "'a => 'a => bool" inductive Sem :: "'a com \ 'a sem" where "Sem (Basic f) s (f s)" | "Sem c1 s s'' \ Sem c2 s'' s' \ Sem (c1;c2) s s'" | "s \ b \ Sem c1 s s' \ Sem (IF b THEN c1 ELSE c2 FI) s s'" | "s \ b \ Sem c2 s s' \ Sem (IF b THEN c1 ELSE c2 FI) s s'" -| "s \ b \ Sem (While b x c) s s" -| "s \ b \ Sem c s s'' \ Sem (While b x c) s'' s' \ - Sem (While b x c) s s'" +| "s \ b \ Sem (While b x y c) s s" +| "s \ b \ Sem c s s'' \ Sem (While b x y c) s'' s' \ + Sem (While b x y c) s s'" inductive_cases [elim!]: "Sem (Basic f) s s'" "Sem (c1;c2) s s'" "Sem (IF b THEN c1 ELSE c2 FI) s s'" +lemma Sem_deterministic: + assumes "Sem c s s1" + and "Sem c s s2" + shows "s1 = s2" +proof - + have "Sem c s s1 \ (\s2. Sem c s s2 \ s1 = s2)" + by (induct rule: Sem.induct) (subst Sem.simps, blast)+ + thus ?thesis + using assms by simp +qed + definition Valid :: "'a bexp \ 'a com \ 'a bexp \ bool" - where "Valid p c q \ (\s s'. Sem c s s' \ s \ p \ s' \ q)" + where "Valid p c q \ \s s'. Sem c s s' \ s \ p \ s' \ q" +definition ValidTC :: "'a bexp \ 'a com \ 'a bexp \ bool" + where "ValidTC p c q \ \s . s \ p \ (\t . Sem c s t \ t \ q)" + +lemma tc_implies_pc: + "ValidTC p c q \ Valid p c q" + by (metis Sem_deterministic Valid_def ValidTC_def) + +lemma tc_extract_function: + "ValidTC p c q \ \f . \s . s \ p \ f s \ q" + by (metis ValidTC_def) syntax "_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61) syntax "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) syntax ("" output) "_hoare" :: "['a assn,'a com,'a assn] => bool" ("{_} // _ // {_}" [0,55,0] 50) ML_file \hoare_syntax.ML\ parse_translation \[(\<^syntax_const>\_hoare_vars\, K Hoare_Syntax.hoare_vars_tr)]\ print_translation \[(\<^const_syntax>\Valid\, K (Hoare_Syntax.spec_tr' \<^syntax_const>\_hoare\))]\ +syntax + "_hoare_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" + ("VARS _// [_] // _ // [_]" [0,0,55,0] 50) +syntax ("" output) + "_hoare_tc" :: "['a assn,'a com,'a assn] => bool" + ("[_] // _ // [_]" [0,55,0] 50) + +parse_translation \[(\<^syntax_const>\_hoare_tc_vars\, K Hoare_Syntax.hoare_tc_vars_tr)]\ +print_translation \[(\<^const_syntax>\ValidTC\, K (Hoare_Syntax.spec_tr' \<^syntax_const>\_hoare_tc\))]\ + lemma SkipRule: "p \ q \ Valid p (Basic id) q" by (auto simp:Valid_def) lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) q" by (auto simp:Valid_def) lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (c1;c2) R" by (auto simp:Valid_def) lemma CondRule: "p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')} \ Valid w c1 q \ Valid w' c2 q \ Valid p (Cond b c1 c2) q" by (auto simp:Valid_def) lemma While_aux: - assumes "Sem (WHILE b INV {i} DO c OD) s s'" + assumes "Sem (WHILE b INV {i} VAR {v} DO c OD) s s'" shows "\s s'. Sem c s s' \ s \ I \ s \ b \ s' \ I \ s \ I \ s' \ I \ s' \ b" using assms - by (induct "WHILE b INV {i} DO c OD" s s') auto + by (induct "WHILE b INV {i} VAR {v} DO c OD" s s') auto lemma WhileRule: - "p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i c) q" + "p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i v c) q" apply (clarsimp simp:Valid_def) apply(drule While_aux) apply assumption apply blast apply blast done +lemma SkipRuleTC: + assumes "p \ q" + shows "ValidTC p (Basic id) q" + by (metis assms Sem.intros(1) ValidTC_def id_apply subsetD) -lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}" +lemma BasicRuleTC: + assumes "p \ {s. f s \ q}" + shows "ValidTC p (Basic f) q" + by (metis assms Ball_Collect Sem.intros(1) ValidTC_def) + +lemma SeqRuleTC: + assumes "ValidTC p c1 q" + and "ValidTC q c2 r" + shows "ValidTC p (c1;c2) r" + by (meson assms Sem.intros(2) ValidTC_def) + +lemma CondRuleTC: + assumes "p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')}" + and "ValidTC w c1 q" + and "ValidTC w' c2 q" + shows "ValidTC p (Cond b c1 c2) q" +proof (unfold ValidTC_def, rule allI) + fix s + show "s \ p \ (\t . Sem (Cond b c1 c2) s t \ t \ q)" + apply (cases "s \ b") + apply (metis (mono_tags, lifting) assms(1,2) Ball_Collect Sem.intros(3) ValidTC_def) + by (metis (mono_tags, lifting) assms(1,3) Ball_Collect Sem.intros(4) ValidTC_def) +qed + +lemma WhileRuleTC: + assumes "p \ i" + and "\n::nat . ValidTC (i \ b \ {s . v s = n}) c (i \ {s . v s < n})" + and "i \ uminus b \ q" + shows "ValidTC p (While b i v c) q" +proof - + { + fix s n + have "s \ i \ v s = n \ (\t . Sem (While b i v c) s t \ t \ q)" + proof (induction "n" arbitrary: s rule: less_induct) + fix n :: nat + fix s :: 'a + assume 1: "\(m::nat) s::'a . m < n \ s \ i \ v s = m \ (\t . Sem (While b i v c) s t \ t \ q)" + show "s \ i \ v s = n \ (\t . Sem (While b i v c) s t \ t \ q)" + proof (rule impI, cases "s \ b") + assume 2: "s \ b" and "s \ i \ v s = n" + hence "s \ i \ b \ {s . v s = n}" + using assms(1) by auto + hence "\t . Sem c s t \ t \ i \ {s . v s < n}" + by (metis assms(2) ValidTC_def) + from this obtain t where 3: "Sem c s t \ t \ i \ {s . v s < n}" + by auto + hence "\u . Sem (While b i v c) t u \ u \ q" + using 1 by auto + thus "\t . Sem (While b i v c) s t \ t \ q" + using 2 3 Sem.intros(6) by force + next + assume "s \ b" and "s \ i \ v s = n" + thus "\t . Sem (While b i v c) s t \ t \ q" + using Sem.intros(5) assms(3) by fastforce + qed + qed + } + thus ?thesis + using assms(1) ValidTC_def by force +qed + +lemma Compl_Collect: "-(Collect b) = {x. \(b x)}" by blast lemmas AbortRule = SkipRule \ \dummy version\ ML_file \hoare_tac.ML\ method_setup vcg = \ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\ "verification condition generator" method_setup vcg_simp = \ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))\ "verification condition generator plus simplification" +method_setup vcg_tc = \ + Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (K all_tac)))\ + "verification condition generator" + +method_setup vcg_tc_simp = \ + Scan.succeed (fn ctxt => + SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\ + "verification condition generator plus simplification" + end diff --git a/src/HOL/Hoare/Hoare_Logic_Abort.thy b/src/HOL/Hoare/Hoare_Logic_Abort.thy --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy @@ -1,132 +1,244 @@ (* Title: HOL/Hoare/Hoare_Logic_Abort.thy Author: Leonor Prensa Nieto & Tobias Nipkow Copyright 2003 TUM + Author: Walter Guttmann (extension to total-correctness proofs) -Like Hoare.thy, but with an Abort statement for modelling run time errors. +Like Hoare_Logic.thy, but with an Abort statement for modelling run time errors. *) theory Hoare_Logic_Abort imports Main begin type_synonym 'a bexp = "'a set" type_synonym 'a assn = "'a set" +type_synonym 'a var = "'a \ nat" datatype 'a com = Basic "'a \ 'a" | Abort | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) -| While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) +| While "'a bexp" "'a assn" "'a var" "'a com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61) + +syntax (xsymbols) + "_whilePC" :: "'a bexp \ 'a assn \ 'a com \ 'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) + +translations + "WHILE b INV {x} DO c OD" => "WHILE b INV {x} VAR {0} DO c OD" abbreviation annskip ("SKIP") where "SKIP == Basic id" type_synonym 'a sem = "'a option => 'a option => bool" inductive Sem :: "'a com \ 'a sem" where "Sem (Basic f) None None" | "Sem (Basic f) (Some s) (Some (f s))" | "Sem Abort s None" | "Sem c1 s s'' \ Sem c2 s'' s' \ Sem (c1;c2) s s'" | "Sem (IF b THEN c1 ELSE c2 FI) None None" | "s \ b \ Sem c1 (Some s) s' \ Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'" | "s \ b \ Sem c2 (Some s) s' \ Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'" -| "Sem (While b x c) None None" -| "s \ b \ Sem (While b x c) (Some s) (Some s)" -| "s \ b \ Sem c (Some s) s'' \ Sem (While b x c) s'' s' \ - Sem (While b x c) (Some s) s'" +| "Sem (While b x y c) None None" +| "s \ b \ Sem (While b x y c) (Some s) (Some s)" +| "s \ b \ Sem c (Some s) s'' \ Sem (While b x y c) s'' s' \ + Sem (While b x y c) (Some s) s'" inductive_cases [elim!]: "Sem (Basic f) s s'" "Sem (c1;c2) s s'" "Sem (IF b THEN c1 ELSE c2 FI) s s'" -definition Valid :: "'a bexp \ 'a com \ 'a bexp \ bool" where - "Valid p c q \ \s s'. Sem c s s' \ s \ Some ` p \ s' \ Some ` q" +lemma Sem_deterministic: + assumes "Sem c s s1" + and "Sem c s s2" + shows "s1 = s2" +proof - + have "Sem c s s1 \ (\s2. Sem c s s2 \ s1 = s2)" + by (induct rule: Sem.induct) (subst Sem.simps, blast)+ + thus ?thesis + using assms by simp +qed +definition Valid :: "'a bexp \ 'a com \ 'a bexp \ bool" + where "Valid p c q \ \s s'. Sem c s s' \ s \ Some ` p \ s' \ Some ` q" + +definition ValidTC :: "'a bexp \ 'a com \ 'a bexp \ bool" + where "ValidTC p c q \ \s . s \ p \ (\t . Sem c (Some s) (Some t) \ t \ q)" + +lemma tc_implies_pc: + "ValidTC p c q \ Valid p c q" + by (smt Sem_deterministic ValidTC_def Valid_def image_iff) + +lemma tc_extract_function: + "ValidTC p c q \ \f . \s . s \ p \ f s \ q" + by (meson ValidTC_def) syntax "_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61) syntax "_hoare_abort_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) syntax ("" output) "_hoare_abort" :: "['a assn,'a com,'a assn] => bool" ("{_} // _ // {_}" [0,55,0] 50) ML_file \hoare_syntax.ML\ parse_translation \[(\<^syntax_const>\_hoare_abort_vars\, K Hoare_Syntax.hoare_vars_tr)]\ -print_translation - \[(\<^const_syntax>\Valid\, K (Hoare_Syntax.spec_tr' \<^syntax_const>\_hoare_abort\))]\ +print_translation \[(\<^const_syntax>\Valid\, K (Hoare_Syntax.spec_tr' \<^syntax_const>\_hoare_abort\))]\ +syntax + "_hoare_abort_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" + ("VARS _// [_] // _ // [_]" [0,0,55,0] 50) +syntax ("" output) + "_hoare_abort_tc" :: "['a assn,'a com,'a assn] => bool" + ("[_] // _ // [_]" [0,55,0] 50) -section \The proof rules\ +parse_translation \[(\<^syntax_const>\_hoare_abort_tc_vars\, K Hoare_Syntax.hoare_tc_vars_tr)]\ +print_translation \[(\<^const_syntax>\ValidTC\, K (Hoare_Syntax.spec_tr' \<^syntax_const>\_hoare_abort_tc\))]\ + +text \The proof rules for partial correctness\ lemma SkipRule: "p \ q \ Valid p (Basic id) q" by (auto simp:Valid_def) lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) q" by (auto simp:Valid_def) lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (c1;c2) R" by (auto simp:Valid_def) lemma CondRule: "p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')} \ Valid w c1 q \ Valid w' c2 q \ Valid p (Cond b c1 c2) q" by (fastforce simp:Valid_def image_def) lemma While_aux: - assumes "Sem (WHILE b INV {i} DO c OD) s s'" + assumes "Sem (WHILE b INV {i} VAR {v} DO c OD) s s'" shows "\s s'. Sem c s s' \ s \ Some ` (I \ b) \ s' \ Some ` I \ s \ Some ` I \ s' \ Some ` (I \ -b)" using assms - by (induct "WHILE b INV {i} DO c OD" s s') auto + by (induct "WHILE b INV {i} VAR {v} DO c OD" s s') auto lemma WhileRule: - "p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i c) q" -apply(simp add:Valid_def) -apply(simp (no_asm) add:image_def) -apply clarify + "p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i v c) q" +apply (clarsimp simp:Valid_def) apply(drule While_aux) apply assumption apply blast apply blast done lemma AbortRule: "p \ {s. False} \ Valid p Abort q" by(auto simp:Valid_def) +text \The proof rules for total correctness\ + +lemma SkipRuleTC: + assumes "p \ q" + shows "ValidTC p (Basic id) q" + by (metis Sem.intros(2) ValidTC_def assms id_def subsetD) + +lemma BasicRuleTC: + assumes "p \ {s. f s \ q}" + shows "ValidTC p (Basic f) q" + by (metis Ball_Collect Sem.intros(2) ValidTC_def assms) + +lemma SeqRuleTC: + assumes "ValidTC p c1 q" + and "ValidTC q c2 r" + shows "ValidTC p (c1;c2) r" + by (meson assms Sem.intros(4) ValidTC_def) + +lemma CondRuleTC: + assumes "p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')}" + and "ValidTC w c1 q" + and "ValidTC w' c2 q" + shows "ValidTC p (Cond b c1 c2) q" +proof (unfold ValidTC_def, rule allI) + fix s + show "s \ p \ (\t . Sem (Cond b c1 c2) (Some s) (Some t) \ t \ q)" + apply (cases "s \ b") + apply (metis (mono_tags, lifting) Ball_Collect Sem.intros(6) ValidTC_def assms(1,2)) + by (metis (mono_tags, lifting) Ball_Collect Sem.intros(7) ValidTC_def assms(1,3)) +qed + +lemma WhileRuleTC: + assumes "p \ i" + and "\n::nat . ValidTC (i \ b \ {s . v s = n}) c (i \ {s . v s < n})" + and "i \ uminus b \ q" + shows "ValidTC p (While b i v c) q" +proof - + { + fix s n + have "s \ i \ v s = n \ (\t . Sem (While b i v c) (Some s) (Some t) \ t \ q)" + proof (induction "n" arbitrary: s rule: less_induct) + fix n :: nat + fix s :: 'a + assume 1: "\(m::nat) s::'a . m < n \ s \ i \ v s = m \ (\t . Sem (While b i v c) (Some s) (Some t) \ t \ q)" + show "s \ i \ v s = n \ (\t . Sem (While b i v c) (Some s) (Some t) \ t \ q)" + proof (rule impI, cases "s \ b") + assume 2: "s \ b" and "s \ i \ v s = n" + hence "s \ i \ b \ {s . v s = n}" + using assms(1) by auto + hence "\t . Sem c (Some s) (Some t) \ t \ i \ {s . v s < n}" + by (metis assms(2) ValidTC_def) + from this obtain t where 3: "Sem c (Some s) (Some t) \ t \ i \ {s . v s < n}" + by auto + hence "\u . Sem (While b i v c) (Some t) (Some u) \ u \ q" + using 1 by auto + thus "\t . Sem (While b i v c) (Some s) (Some t) \ t \ q" + using 2 3 Sem.intros(10) by force + next + assume "s \ b" and "s \ i \ v s = n" + thus "\t . Sem (While b i v c) (Some s) (Some t) \ t \ q" + using Sem.intros(9) assms(3) by fastforce + qed + qed + } + thus ?thesis + using assms(1) ValidTC_def by force +qed + subsection \Derivation of the proof rules and, most importantly, the VCG tactic\ lemma Compl_Collect: "-(Collect b) = {x. \(b x)}" by blast ML_file \hoare_tac.ML\ method_setup vcg = \ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\ "verification condition generator" method_setup vcg_simp = \ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))\ "verification condition generator plus simplification" +method_setup vcg_tc = \ + Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (K all_tac)))\ + "verification condition generator" + +method_setup vcg_tc_simp = \ + Scan.succeed (fn ctxt => + SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\ + "verification condition generator plus simplification" + \ \Special syntax for guarded statements and guarded array updates:\ syntax "_guarded_com" :: "bool \ 'a com \ 'a com" ("(2_ \/ _)" 71) "_array_update" :: "'a list \ nat \ 'a \ 'a com" ("(2_[_] :=/ _)" [70, 65] 61) translations "P \ c" == "IF P THEN c ELSE CONST Abort FI" "a[i] := v" => "(i < CONST length a) \ (a := CONST list_update a i v)" \ \reverse translation not possible because of duplicate \a\\ text \ Note: there is no special syntax for guarded array access. Thus you must write \j < length a \ a[i] := a!j\. \ end diff --git a/src/HOL/Hoare/README.html b/src/HOL/Hoare/README.html --- a/src/HOL/Hoare/README.html +++ b/src/HOL/Hoare/README.html @@ -1,93 +1,119 @@ HOL/Hoare/ReadMe

Hoare Logic for a Simple WHILE Language

Language and logic

This directory contains an implementation of Hoare logic for a simple WHILE language. The constructs are
  • SKIP
  • _ := _
  • _ ; _
  • IF _ THEN _ ELSE _ FI
  • WHILE _ INV {_} DO _ OD
Note that each WHILE-loop must be annotated with an invariant.

After loading theory Hoare, you can state goals of the form 

 VARS x y ... {P} prog {Q}
where prog is a program in the above language, P is the precondition, Q the postcondition, and x y ... is the list of all program variables in prog. The latter list must be nonempty and it must include all variables that occur on the left-hand side of an assignment in prog. Example: 
 VARS x {x = a} x := x+1 {x = a+1}
The (normal) variable a is merely used to record the initial value of x and is not a program variable. Pre/post conditions can be arbitrary HOL formulae mentioning both program variables and normal variables.

The implementation hides reasoning in Hoare logic completely and provides a method vcg for transforming a goal in Hoare logic into an equivalent list of verification conditions in HOL: 

 apply vcg
If you want to simplify the resulting verification conditions at the same time: 
 apply vcg_simp
which, given the example goal above, solves it completely. For further examples see Examples.

IMPORTANT: This is a logic of partial correctness. You can only prove that your program does the right thing if it terminates, but not that it terminates. +A logic of total correctness is also provided and described below. + +

Total correctness

+ +To prove termination, each WHILE-loop must be annotated with a variant: +
    +
  • WHILE _ INV {_} VAR {_} DO _ OD +
+A variant is an expression with type nat, which may use program +variables and normal variables. +

+ +A total-correctness goal has the form +

+VARS x y ... [P] prog [Q]
+
+enclosing the pre- and postcondition in square brackets. +

+ +Methods vcg_tc and vcg_tc_simp can be used to derive +verification conditions. +

+ +From a total-correctness proof, a function can be extracted which +for every input satisfying the precondition returns an output +satisfying the postcondition.

Notes on the implementation

The implementation loosely follows

Mike Gordon. Mechanizing Programming Logics in Higher Order Logic.
University of Cambridge, Computer Laboratory, TR 145, 1988.

published as

Mike Gordon. Mechanizing Programming Logics in Higher Order Logic.
In Current Trends in Hardware Verification and Automated Theorem Proving ,
edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989.

The main differences: the state is modelled as a tuple as suggested in

J. von Wright and J. Hekanaho and P. Luostarinen and T. Langbacka. Mechanizing Some Advanced Refinement Concepts. Formal Methods in System Design, 3, 1993, 49-81.

and the embeding is deep, i.e. there is a concrete datatype of programs. The latter is not really necessary. diff --git a/src/HOL/Hoare/SchorrWaite.thy b/src/HOL/Hoare/SchorrWaite.thy --- a/src/HOL/Hoare/SchorrWaite.thy +++ b/src/HOL/Hoare/SchorrWaite.thy @@ -1,576 +1,576 @@ (* Title: HOL/Hoare/SchorrWaite.thy Author: Farhad Mehta Copyright 2003 TUM Proof of the Schorr-Waite graph marking algorithm. *) theory SchorrWaite imports HeapSyntax begin section \Machinery for the Schorr-Waite proof\ definition \ \Relations induced by a mapping\ rel :: "('a \ 'a ref) \ ('a \ 'a) set" where "rel m = {(x,y). m x = Ref y}" definition relS :: "('a \ 'a ref) set \ ('a \ 'a) set" where "relS M = (\m \ M. rel m)" definition addrs :: "'a ref set \ 'a set" where "addrs P = {a. Ref a \ P}" definition reachable :: "('a \ 'a) set \ 'a ref set \ 'a set" where "reachable r P = (r\<^sup>* `` addrs P)" lemmas rel_defs = relS_def rel_def text \Rewrite rules for relations induced by a mapping\ lemma self_reachable: "b \ B \ b \ R\<^sup>* `` B" apply blast done lemma oneStep_reachable: "b \ R``B \ b \ R\<^sup>* `` B" apply blast done lemma still_reachable: "\B\Ra\<^sup>*``A; \ (x,y) \ Rb-Ra. y\ (Ra\<^sup>*``A)\ \ Rb\<^sup>* `` B \ Ra\<^sup>* `` A " apply (clarsimp simp only:Image_iff) apply (erule rtrancl_induct) apply blast apply (subgoal_tac "(y, z) \ Ra\(Rb-Ra)") apply (erule UnE) apply (auto intro:rtrancl_into_rtrancl) apply blast done lemma still_reachable_eq: "\ A\Rb\<^sup>*``B; B\Ra\<^sup>*``A; \ (x,y) \ Ra-Rb. y \(Rb\<^sup>*``B); \ (x,y) \ Rb-Ra. y\ (Ra\<^sup>*``A)\ \ Ra\<^sup>*``A = Rb\<^sup>*``B " apply (rule equalityI) apply (erule still_reachable ,assumption)+ done lemma reachable_null: "reachable mS {Null} = {}" apply (simp add: reachable_def addrs_def) done lemma reachable_empty: "reachable mS {} = {}" apply (simp add: reachable_def addrs_def) done lemma reachable_union: "(reachable mS aS \ reachable mS bS) = reachable mS (aS \ bS)" apply (simp add: reachable_def rel_defs addrs_def) apply blast done lemma reachable_union_sym: "reachable r (insert a aS) = (r\<^sup>* `` addrs {a}) \ reachable r aS" apply (simp add: reachable_def rel_defs addrs_def) apply blast done lemma rel_upd1: "(a,b) \ rel (r(q:=t)) \ (a,b) \ rel r \ a=q" apply (rule classical) apply (simp add:rel_defs fun_upd_apply) done lemma rel_upd2: "(a,b) \ rel r \ (a,b) \ rel (r(q:=t)) \ a=q" apply (rule classical) apply (simp add:rel_defs fun_upd_apply) done definition \ \Restriction of a relation\ restr ::"('a \ 'a) set \ ('a \ bool) \ ('a \ 'a) set" ("(_/ | _)" [50, 51] 50) where "restr r m = {(x,y). (x,y) \ r \ \ m x}" text \Rewrite rules for the restriction of a relation\ lemma restr_identity[simp]: " (\x. \ m x) \ (R |m) = R" by (auto simp add:restr_def) lemma restr_rtrancl[simp]: " \m l\ \ (R | m)\<^sup>* `` {l} = {l}" by (auto simp add:restr_def elim:converse_rtranclE) lemma [simp]: " \m l\ \ (l,x) \ (R | m)\<^sup>* = (l=x)" by (auto simp add:restr_def elim:converse_rtranclE) lemma restr_upd: "((rel (r (q := t)))|(m(q := True))) = ((rel (r))|(m(q := True))) " apply (auto simp:restr_def rel_def fun_upd_apply) apply (rename_tac a b) apply (case_tac "a=q") apply auto done lemma restr_un: "((r \ s)|m) = (r|m) \ (s|m)" by (auto simp add:restr_def) lemma rel_upd3: "(a, b) \ (r|(m(q := t))) \ (a,b) \ (r|m) \ a = q " apply (rule classical) apply (simp add:restr_def fun_upd_apply) done definition \ \A short form for the stack mapping function for List\ S :: "('a \ bool) \ ('a \ 'a ref) \ ('a \ 'a ref) \ ('a \ 'a ref)" where "S c l r = (\x. if c x then r x else l x)" text \Rewrite rules for Lists using S as their mapping\ lemma [rule_format,simp]: "\p. a \ set stack \ List (S c l r) p stack = List (S (c(a:=x)) (l(a:=y)) (r(a:=z))) p stack" apply(induct_tac stack) apply(simp add:fun_upd_apply S_def)+ done lemma [rule_format,simp]: "\p. a \ set stack \ List (S c l (r(a:=z))) p stack = List (S c l r) p stack" apply(induct_tac stack) apply(simp add:fun_upd_apply S_def)+ done lemma [rule_format,simp]: "\p. a \ set stack \ List (S c (l(a:=z)) r) p stack = List (S c l r) p stack" apply(induct_tac stack) apply(simp add:fun_upd_apply S_def)+ done lemma [rule_format,simp]: "\p. a \ set stack \ List (S (c(a:=z)) l r) p stack = List (S c l r) p stack" apply(induct_tac stack) apply(simp add:fun_upd_apply S_def)+ done primrec \ \Recursive definition of what is means for a the graph/stack structure to be reconstructible\ stkOk :: "('a \ bool) \ ('a \ 'a ref) \ ('a \ 'a ref) \ ('a \ 'a ref) \ ('a \ 'a ref) \ 'a ref \'a list \ bool" where stkOk_nil: "stkOk c l r iL iR t [] = True" | stkOk_cons: "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \ iL p = (if c p then l p else t) \ iR p = (if c p then t else r p))" text \Rewrite rules for stkOk\ lemma [simp]: "\t. \ x \ set xs; Ref x\t \ \ stkOk (c(x := f)) l r iL iR t xs = stkOk c l r iL iR t xs" apply (induct xs) apply (auto simp:eq_sym_conv) done lemma [simp]: "\t. \ x \ set xs; Ref x\t \ \ stkOk c (l(x := g)) r iL iR t xs = stkOk c l r iL iR t xs" apply (induct xs) apply (auto simp:eq_sym_conv) done lemma [simp]: "\t. \ x \ set xs; Ref x\t \ \ stkOk c l (r(x := g)) iL iR t xs = stkOk c l r iL iR t xs" apply (induct xs) apply (auto simp:eq_sym_conv) done lemma stkOk_r_rewrite [simp]: "\x. x \ set xs \ stkOk c l (r(x := g)) iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs" apply (induct xs) apply (auto simp:eq_sym_conv) done lemma [simp]: "\x. x \ set xs \ stkOk c (l(x := g)) r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs" apply (induct xs) apply (auto simp:eq_sym_conv) done lemma [simp]: "\x. x \ set xs \ stkOk (c(x := g)) l r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs" apply (induct xs) apply (auto simp:eq_sym_conv) done section\The Schorr-Waite algorithm\ theorem SchorrWaiteAlgorithm: "VARS c m l r t p q root {R = reachable (relS {l, r}) {root} \ (\x. \ m x) \ iR = r \ iL = l} t := root; p := Null; WHILE p \ Null \ t \ Null \ \ t^.m INV {\stack. List (S c l r) p stack \ \ \\i1\\ (\x \ set stack. m x) \ \ \\i2\\ R = reachable (relS{l, r}) {t,p} \ \ \\i3\\ (\x. x \ R \ \m x \ \ \\i4\\ x \ reachable (relS{l,r}|m) ({t}\set(map r stack))) \ (\x. m x \ x \ R) \ \ \\i5\\ (\x. x \ set stack \ r x = iR x \ l x = iL x) \ \ \\i6\\ (stkOk c l r iL iR t stack) \ \\i7\\} DO IF t = Null \ t^.m THEN IF p^.c THEN q := t; t := p; p := p^.r; t^.r := q \ \\pop\\ ELSE q := t; t := p^.r; p^.r := p^.l; \ \\swing\\ p^.l := q; p^.c := True FI ELSE q := p; p := t; t := t^.l; p^.l := q; \ \\push\\ p^.m := True; p^.c := False FI OD {(\x. (x \ R) = m x) \ (r = iR \ l = iL) }" (is "VARS c m l r t p q root {?Pre c m l r root} (?c1; ?c2; ?c3) {?Post c m l r}") proof (vcg) let "While {(c, m, l, r, t, p, q, root). ?whileB m t p} - {(c, m, l, r, t, p, q, root). ?inv c m l r t p} ?body" = ?c3 + {(c, m, l, r, t, p, q, root). ?inv c m l r t p} _ ?body" = ?c3 { fix c m l r t p q root assume "?Pre c m l r root" thus "?inv c m l r root Null" by (auto simp add: reachable_def addrs_def) next fix c m l r t p q let "\stack. ?Inv stack" = "?inv c m l r t p" assume a: "?inv c m l r t p \ \(p \ Null \ t \ Null \ \ t^.m)" then obtain stack where inv: "?Inv stack" by blast from a have pNull: "p = Null" and tDisj: "t=Null \ (t\Null \ t^.m )" by auto let "?I1 \ _ \ _ \ ?I4 \ ?I5 \ ?I6 \ _" = "?Inv stack" from inv have i1: "?I1" and i4: "?I4" and i5: "?I5" and i6: "?I6" by simp+ from pNull i1 have stackEmpty: "stack = []" by simp from tDisj i4 have RisMarked[rule_format]: "\x. x \ R \ m x" by(auto simp: reachable_def addrs_def stackEmpty) from i5 i6 show "(\x.(x \ R) = m x) \ r = iR \ l = iL" by(auto simp: stackEmpty fun_eq_iff intro:RisMarked) next fix c m l r t p q root let "\stack. ?Inv stack" = "?inv c m l r t p" let "\stack. ?popInv stack" = "?inv c m l (r(p \ t)) p (p^.r)" let "\stack. ?swInv stack" = "?inv (c(p \ True)) m (l(p \ t)) (r(p \ p^.l)) (p^.r) p" let "\stack. ?puInv stack" = "?inv (c(t \ False)) (m(t \ True)) (l(t \ p)) r (t^.l) t" let "?ifB1" = "(t = Null \ t^.m)" let "?ifB2" = "p^.c" assume "(\stack.?Inv stack) \ (p \ Null \ t \ Null \ \ t^.m)" (is "_ \ ?whileB") then obtain stack where inv: "?Inv stack" and whileB: "?whileB" by blast let "?I1 \ ?I2 \ ?I3 \ ?I4 \ ?I5 \ ?I6 \ ?I7" = "?Inv stack" from inv have i1: "?I1" and i2: "?I2" and i3: "?I3" and i4: "?I4" and i5: "?I5" and i6: "?I6" and i7: "?I7" by simp+ have stackDist: "distinct (stack)" using i1 by (rule List_distinct) show "(?ifB1 \ (?ifB2 \ (\stack.?popInv stack)) \ (\?ifB2 \ (\stack.?swInv stack)) ) \ (\?ifB1 \ (\stack.?puInv stack))" proof - { assume ifB1: "t = Null \ t^.m" and ifB2: "p^.c" from ifB1 whileB have pNotNull: "p \ Null" by auto then obtain addr_p where addr_p_eq: "p = Ref addr_p" by auto with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl" by auto with i2 have m_addr_p: "p^.m" by auto have stackDist: "distinct (stack)" using i1 by (rule List_distinct) from stack_eq stackDist have p_notin_stack_tl: "addr p \ set stack_tl" by simp let "?poI1\ ?poI2\ ?poI3\ ?poI4\ ?poI5\ ?poI6\ ?poI7" = "?popInv stack_tl" have "?popInv stack_tl" proof - \ \List property is maintained:\ from i1 p_notin_stack_tl ifB2 have poI1: "List (S c l (r(p \ t))) (p^.r) stack_tl" by(simp add: addr_p_eq stack_eq, simp add: S_def) moreover \ \Everything on the stack is marked:\ from i2 have poI2: "\ x \ set stack_tl. m x" by (simp add:stack_eq) moreover \ \Everything is still reachable:\ let "(R = reachable ?Ra ?A)" = "?I3" let "?Rb" = "(relS {l, r(p \ t)})" let "?B" = "{p, p^.r}" \ \Our goal is \R = reachable ?Rb ?B\.\ have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" (is "?L = ?R") proof show "?L \ ?R" proof (rule still_reachable) show "addrs ?A \ ?Rb\<^sup>* `` addrs ?B" by(fastforce simp:addrs_def relS_def rel_def addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2]) show "\(x,y) \ ?Ra-?Rb. y \ (?Rb\<^sup>* `` addrs ?B)" by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1) qed show "?R \ ?L" proof (rule still_reachable) show "addrs ?B \ ?Ra\<^sup>* `` addrs ?A" by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2]) next show "\(x, y)\?Rb-?Ra. y\(?Ra\<^sup>*``addrs ?A)" by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd2) qed qed with i3 have poI3: "R = reachable ?Rb ?B" by (simp add:reachable_def) moreover \ \If it is reachable and not marked, it is still reachable using...\ let "\x. x \ R \ \ m x \ x \ reachable ?Ra ?A" = ?I4 let "?Rb" = "relS {l, r(p \ t)} | m" let "?B" = "{p} \ set (map (r(p \ t)) stack_tl)" \ \Our goal is \\x. x \ R \ \ m x \ x \ reachable ?Rb ?B\.\ let ?T = "{t, p^.r}" have "?Ra\<^sup>* `` addrs ?A \ ?Rb\<^sup>* `` (addrs ?B \ addrs ?T)" proof (rule still_reachable) have rewrite: "\s\set stack_tl. (r(p \ t)) s = r s" by (auto simp add:p_notin_stack_tl intro:fun_upd_other) show "addrs ?A \ ?Rb\<^sup>* `` (addrs ?B \ addrs ?T)" by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable) show "\(x, y)\?Ra-?Rb. y\(?Rb\<^sup>*``(addrs ?B \ addrs ?T))" by (clarsimp simp:restr_def relS_def) (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1) qed \ \We now bring a term from the right to the left of the subset relation.\ hence subset: "?Ra\<^sup>* `` addrs ?A - ?Rb\<^sup>* `` addrs ?T \ ?Rb\<^sup>* `` addrs ?B" by blast have poI4: "\x. x \ R \ \ m x \ x \ reachable ?Rb ?B" proof (rule allI, rule impI) fix x assume a: "x \ R \ \ m x" \ \First, a disjunction on \<^term>\p^.r\ used later in the proof\ have pDisj:"p^.r = Null \ (p^.r \ Null \ p^.r^.m)" using poI1 poI2 by auto \ \\<^term>\x\ belongs to the left hand side of @{thm[source] subset}:\ have incl: "x \ ?Ra\<^sup>*``addrs ?A" using a i4 by (simp only:reachable_def, clarsimp) have excl: "x \ ?Rb\<^sup>*`` addrs ?T" using pDisj ifB1 a by (auto simp add:addrs_def) \ \And therefore also belongs to the right hand side of @{thm[source]subset},\ \ \which corresponds to our goal.\ from incl excl subset show "x \ reachable ?Rb ?B" by (auto simp add:reachable_def) qed moreover \ \If it is marked, then it is reachable\ from i5 have poI5: "\x. m x \ x \ R" . moreover \ \If it is not on the stack, then its \<^term>\l\ and \<^term>\r\ fields are unchanged\ from i7 i6 ifB2 have poI6: "\x. x \ set stack_tl \ (r(p \ t)) x = iR x \ l x = iL x" by(auto simp: addr_p_eq stack_eq fun_upd_apply) moreover \ \If it is on the stack, then its \<^term>\l\ and \<^term>\r\ fields can be reconstructed\ from p_notin_stack_tl i7 have poI7: "stkOk c l (r(p \ t)) iL iR p stack_tl" by (clarsimp simp:stack_eq addr_p_eq) ultimately show "?popInv stack_tl" by simp qed hence "\stack. ?popInv stack" .. } moreover \ \Proofs of the Swing and Push arm follow.\ \ \Since they are in principle simmilar to the Pop arm proof,\ \ \we show fewer comments and use frequent pattern matching.\ { \ \Swing arm\ assume ifB1: "?ifB1" and nifB2: "\?ifB2" from ifB1 whileB have pNotNull: "p \ Null" by clarsimp then obtain addr_p where addr_p_eq: "p = Ref addr_p" by clarsimp with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl" by clarsimp with i2 have m_addr_p: "p^.m" by clarsimp from stack_eq stackDist have p_notin_stack_tl: "(addr p) \ set stack_tl" by simp let "?swI1\?swI2\?swI3\?swI4\?swI5\?swI6\?swI7" = "?swInv stack" have "?swInv stack" proof - \ \List property is maintained:\ from i1 p_notin_stack_tl nifB2 have swI1: "?swI1" by (simp add:addr_p_eq stack_eq, simp add:S_def) moreover \ \Everything on the stack is marked:\ from i2 have swI2: "?swI2" . moreover \ \Everything is still reachable:\ let "R = reachable ?Ra ?A" = "?I3" let "R = reachable ?Rb ?B" = "?swI3" have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" proof (rule still_reachable_eq) show "addrs ?A \ ?Rb\<^sup>* `` addrs ?B" by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2]) next show "addrs ?B \ ?Ra\<^sup>* `` addrs ?A" by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2]) next show "\(x, y)\?Ra-?Rb. y\(?Rb\<^sup>*``addrs ?B)" by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1) next show "\(x, y)\?Rb-?Ra. y\(?Ra\<^sup>*``addrs ?A)" by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2) qed with i3 have swI3: "?swI3" by (simp add:reachable_def) moreover \ \If it is reachable and not marked, it is still reachable using...\ let "\x. x \ R \ \ m x \ x \ reachable ?Ra ?A" = ?I4 let "\x. x \ R \ \ m x \ x \ reachable ?Rb ?B" = ?swI4 let ?T = "{t}" have "?Ra\<^sup>*``addrs ?A \ ?Rb\<^sup>*``(addrs ?B \ addrs ?T)" proof (rule still_reachable) have rewrite: "(\s\set stack_tl. (r(addr p := l(addr p))) s = r s)" by (auto simp add:p_notin_stack_tl intro:fun_upd_other) show "addrs ?A \ ?Rb\<^sup>* `` (addrs ?B \ addrs ?T)" by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable) next show "\(x, y)\?Ra-?Rb. y\(?Rb\<^sup>*``(addrs ?B \ addrs ?T))" by (clarsimp simp:relS_def restr_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1) qed then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \ ?Rb\<^sup>*``addrs ?B" by blast have ?swI4 proof (rule allI, rule impI) fix x assume a: "x \ R \\ m x" with i4 addr_p_eq stack_eq have inc: "x \ ?Ra\<^sup>*``addrs ?A" by (simp only:reachable_def, clarsimp) with ifB1 a have exc: "x \ ?Rb\<^sup>*`` addrs ?T" by (auto simp add:addrs_def) from inc exc subset show "x \ reachable ?Rb ?B" by (auto simp add:reachable_def) qed moreover \ \If it is marked, then it is reachable\ from i5 have "?swI5" . moreover \ \If it is not on the stack, then its \<^term>\l\ and \<^term>\r\ fields are unchanged\ from i6 stack_eq have "?swI6" by clarsimp moreover \ \If it is on the stack, then its \<^term>\l\ and \<^term>\r\ fields can be reconstructed\ from stackDist i7 nifB2 have "?swI7" by (clarsimp simp:addr_p_eq stack_eq) ultimately show ?thesis by auto qed then have "\stack. ?swInv stack" by blast } moreover { \ \Push arm\ assume nifB1: "\?ifB1" from nifB1 whileB have tNotNull: "t \ Null" by clarsimp then obtain addr_t where addr_t_eq: "t = Ref addr_t" by clarsimp with i1 obtain new_stack where new_stack_eq: "new_stack = (addr t) # stack" by clarsimp from tNotNull nifB1 have n_m_addr_t: "\ (t^.m)" by clarsimp with i2 have t_notin_stack: "(addr t) \ set stack" by blast let "?puI1\?puI2\?puI3\?puI4\?puI5\?puI6\?puI7" = "?puInv new_stack" have "?puInv new_stack" proof - \ \List property is maintained:\ from i1 t_notin_stack have puI1: "?puI1" by (simp add:addr_t_eq new_stack_eq, simp add:S_def) moreover \ \Everything on the stack is marked:\ from i2 have puI2: "?puI2" by (simp add:new_stack_eq fun_upd_apply) moreover \ \Everything is still reachable:\ let "R = reachable ?Ra ?A" = "?I3" let "R = reachable ?Rb ?B" = "?puI3" have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" proof (rule still_reachable_eq) show "addrs ?A \ ?Rb\<^sup>* `` addrs ?B" by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2]) next show "addrs ?B \ ?Ra\<^sup>* `` addrs ?A" by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2]) next show "\(x, y)\?Ra-?Rb. y\(?Rb\<^sup>*``addrs ?B)" by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1) next show "\(x, y)\?Rb-?Ra. y\(?Ra\<^sup>*``addrs ?A)" by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2) qed with i3 have puI3: "?puI3" by (simp add:reachable_def) moreover \ \If it is reachable and not marked, it is still reachable using...\ let "\x. x \ R \ \ m x \ x \ reachable ?Ra ?A" = ?I4 let "\x. x \ R \ \ ?new_m x \ x \ reachable ?Rb ?B" = ?puI4 let ?T = "{t}" have "?Ra\<^sup>*``addrs ?A \ ?Rb\<^sup>*``(addrs ?B \ addrs ?T)" proof (rule still_reachable) show "addrs ?A \ ?Rb\<^sup>* `` (addrs ?B \ addrs ?T)" by (fastforce simp:new_stack_eq addrs_def intro:self_reachable) next show "\(x, y)\?Ra-?Rb. y\(?Rb\<^sup>*``(addrs ?B \ addrs ?T))" by (clarsimp simp:relS_def new_stack_eq restr_un restr_upd) (fastforce simp add:rel_def Image_iff restr_def addrs_def fun_upd_apply addr_t_eq dest:rel_upd3) qed then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \ ?Rb\<^sup>*``addrs ?B" by blast have ?puI4 proof (rule allI, rule impI) fix x assume a: "x \ R \ \ ?new_m x" have xDisj: "x=(addr t) \ x\(addr t)" by simp with i4 a have inc: "x \ ?Ra\<^sup>*``addrs ?A" by (fastforce simp:addr_t_eq addrs_def reachable_def intro:self_reachable) have exc: "x \ ?Rb\<^sup>*`` addrs ?T" using xDisj a n_m_addr_t by (clarsimp simp add:addrs_def addr_t_eq) from inc exc subset show "x \ reachable ?Rb ?B" by (auto simp add:reachable_def) qed moreover \ \If it is marked, then it is reachable\ from i5 have "?puI5" by (auto simp:addrs_def i3 reachable_def addr_t_eq fun_upd_apply intro:self_reachable) moreover \ \If it is not on the stack, then its \<^term>\l\ and \<^term>\r\ fields are unchanged\ from i6 have "?puI6" by (simp add:new_stack_eq) moreover \ \If it is on the stack, then its \<^term>\l\ and \<^term>\r\ fields can be reconstructed\ from stackDist i6 t_notin_stack i7 have "?puI7" by (clarsimp simp:addr_t_eq new_stack_eq) ultimately show ?thesis by auto qed then have "\stack. ?puInv stack" by blast } ultimately show ?thesis by blast qed } qed end diff --git a/src/HOL/Hoare/hoare_syntax.ML b/src/HOL/Hoare/hoare_syntax.ML --- a/src/HOL/Hoare/hoare_syntax.ML +++ b/src/HOL/Hoare/hoare_syntax.ML @@ -1,156 +1,170 @@ (* Title: HOL/Hoare/hoare_syntax.ML Author: Leonor Prensa Nieto & Tobias Nipkow + Author: Walter Guttmann (extension to total-correctness proofs) Syntax translations for Hoare logic. *) signature HOARE_SYNTAX = sig val hoare_vars_tr: term list -> term + val hoare_tc_vars_tr: term list -> term val spec_tr': string -> term list -> term end; structure Hoare_Syntax: HOARE_SYNTAX = struct (** parse translation **) local fun idt_name (Free (x, _)) = SOME x | idt_name (Const (\<^syntax_const>\_constrain\, _) $ t $ _) = idt_name t | idt_name _ = NONE; fun eq_idt tu = (case apply2 idt_name tu of (SOME x, SOME y) => x = y | _ => false); fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body] | mk_abstuple (x :: xs) body = Syntax.const \<^const_syntax>\case_prod\ $ Syntax_Trans.abs_tr [x, mk_abstuple xs body]; fun mk_fbody x e [y] = if eq_idt (x, y) then e else y | mk_fbody x e (y :: xs) = Syntax.const \<^const_syntax>\Pair\ $ (if eq_idt (x, y) then e else y) $ mk_fbody x e xs; fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs); (* bexp_tr & assn_tr *) (*all meta-variables for bexp except for TRUE are translated as if they were boolean expressions*) fun bexp_tr (Const ("TRUE", _)) _ = Syntax.const "TRUE" (* FIXME !? *) | bexp_tr b xs = Syntax.const \<^const_syntax>\Collect\ $ mk_abstuple xs b; fun assn_tr r xs = Syntax.const \<^const_syntax>\Collect\ $ mk_abstuple xs r; +fun var_tr v xs = mk_abstuple xs v; + (* com_tr *) fun com_tr (Const (\<^syntax_const>\_assign\, _) $ x $ e) xs = Syntax.const \<^const_syntax>\Basic\ $ mk_fexp x e xs | com_tr (Const (\<^const_syntax>\Basic\,_) $ f) _ = Syntax.const \<^const_syntax>\Basic\ $ f | com_tr (Const (\<^const_syntax>\Seq\,_) $ c1 $ c2) xs = Syntax.const \<^const_syntax>\Seq\ $ com_tr c1 xs $ com_tr c2 xs | com_tr (Const (\<^const_syntax>\Cond\,_) $ b $ c1 $ c2) xs = Syntax.const \<^const_syntax>\Cond\ $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs - | com_tr (Const (\<^const_syntax>\While\,_) $ b $ I $ c) xs = - Syntax.const \<^const_syntax>\While\ $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs + | com_tr (Const (\<^const_syntax>\While\,_) $ b $ I $ V $ c) xs = + Syntax.const \<^const_syntax>\While\ $ bexp_tr b xs $ assn_tr I xs $ var_tr V xs $ com_tr c xs | com_tr t _ = t; fun vars_tr (Const (\<^syntax_const>\_idts\, _) $ idt $ vars) = idt :: vars_tr vars | vars_tr t = [t]; in fun hoare_vars_tr [vars, pre, prg, post] = let val xs = vars_tr vars in Syntax.const \<^const_syntax>\Valid\ $ assn_tr pre xs $ com_tr prg xs $ assn_tr post xs end | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts); +fun hoare_tc_vars_tr [vars, pre, prg, post] = + let val xs = vars_tr vars + in Syntax.const \<^const_syntax>\ValidTC\ $ + assn_tr pre xs $ com_tr prg xs $ assn_tr post xs + end + | hoare_tc_vars_tr ts = raise TERM ("hoare_tc_vars_tr", ts); + end; (** print translation **) local fun dest_abstuple (Const (\<^const_syntax>\case_prod\, _) $ Abs (v, _, body)) = subst_bound (Syntax.free v, dest_abstuple body) | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body) | dest_abstuple tm = tm; fun abs2list (Const (\<^const_syntax>\case_prod\, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t | abs2list (Abs (x, T, _)) = [Free (x, T)] | abs2list _ = []; fun mk_ts (Const (\<^const_syntax>\case_prod\, _) $ Abs (_, _, t)) = mk_ts t | mk_ts (Abs (_, _, t)) = mk_ts t | mk_ts (Const (\<^const_syntax>\Pair\, _) $ a $ b) = a :: mk_ts b | mk_ts t = [t]; fun mk_vts (Const (\<^const_syntax>\case_prod\,_) $ Abs (x, _, t)) = (Syntax.free x :: abs2list t, mk_ts t) | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t]) | mk_vts _ = raise Match; fun find_ch [] _ _ = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) (* FIXME no_ch!? *) | find_ch ((v, t) :: vts) i xs = if t = Bound i then find_ch vts (i - 1) xs else (true, (v, subst_bounds (xs, t))); fun is_f (Const (\<^const_syntax>\case_prod\, _) $ Abs _) = true | is_f (Abs _) = true | is_f _ = false; (* assn_tr' & bexp_tr'*) fun assn_tr' (Const (\<^const_syntax>\Collect\, _) $ T) = dest_abstuple T | assn_tr' (Const (\<^const_syntax>\inter\, _) $ (Const (\<^const_syntax>\Collect\, _) $ T1) $ (Const (\<^const_syntax>\Collect\, _) $ T2)) = Syntax.const \<^const_syntax>\inter\ $ dest_abstuple T1 $ dest_abstuple T2 | assn_tr' t = t; fun bexp_tr' (Const (\<^const_syntax>\Collect\, _) $ T) = dest_abstuple T | bexp_tr' t = t; +fun var_tr' (Const (\<^const_syntax>\Collect\, _) $ T) = dest_abstuple T + | var_tr' t = t; + (* com_tr' *) fun mk_assign f = let val (vs, ts) = mk_vts f; val (ch, which) = find_ch (vs ~~ ts) (length vs - 1) (rev vs); in if ch then Syntax.const \<^syntax_const>\_assign\ $ fst which $ snd which else Syntax.const \<^const_syntax>\annskip\ end; fun com_tr' (Const (\<^const_syntax>\Basic\, _) $ f) = if is_f f then mk_assign f else Syntax.const \<^const_syntax>\Basic\ $ f | com_tr' (Const (\<^const_syntax>\Seq\,_) $ c1 $ c2) = Syntax.const \<^const_syntax>\Seq\ $ com_tr' c1 $ com_tr' c2 | com_tr' (Const (\<^const_syntax>\Cond\, _) $ b $ c1 $ c2) = Syntax.const \<^const_syntax>\Cond\ $ bexp_tr' b $ com_tr' c1 $ com_tr' c2 - | com_tr' (Const (\<^const_syntax>\While\, _) $ b $ I $ c) = - Syntax.const \<^const_syntax>\While\ $ bexp_tr' b $ assn_tr' I $ com_tr' c + | com_tr' (Const (\<^const_syntax>\While\, _) $ b $ I $ V $ c) = + Syntax.const \<^const_syntax>\While\ $ bexp_tr' b $ assn_tr' I $ var_tr' V $ com_tr' c | com_tr' t = t; in fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q; end; end; diff --git a/src/HOL/Hoare/hoare_tac.ML b/src/HOL/Hoare/hoare_tac.ML --- a/src/HOL/Hoare/hoare_tac.ML +++ b/src/HOL/Hoare/hoare_tac.ML @@ -1,199 +1,235 @@ (* Title: HOL/Hoare/hoare_tac.ML Author: Leonor Prensa Nieto & Tobias Nipkow + Author: Walter Guttmann (extension to total-correctness proofs) Derivation of the proof rules and, most importantly, the VCG tactic. *) signature HOARE = sig val hoare_rule_tac: Proof.context -> term list * thm -> (int -> tactic) -> bool -> int -> tactic val hoare_tac: Proof.context -> (int -> tactic) -> int -> tactic + val hoare_tc_tac: Proof.context -> (int -> tactic) -> int -> tactic end; structure Hoare: HOARE = struct (*** The tactics ***) (*****************************************************************************) (** The function Mset makes the theorem **) (** "?Mset <= {(x1,...,xn). ?P (x1,...,xn)} ==> ?Mset <= {s. ?P s}", **) (** where (x1,...,xn) are the variables of the particular program we are **) (** working on at the moment of the call **) (*****************************************************************************) local (** maps (%x1 ... xn. t) to [x1,...,xn] **) fun abs2list (Const (\<^const_name>\case_prod\, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t | abs2list (Abs (x, T, _)) = [Free (x, T)] | abs2list _ = []; (** maps {(x1,...,xn). t} to [x1,...,xn] **) fun mk_vars (Const (\<^const_name>\Collect\,_) $ T) = abs2list T | mk_vars _ = []; (** abstraction of body over a tuple formed from a list of free variables. Types are also built **) fun mk_abstupleC [] body = absfree ("x", HOLogic.unitT) body | mk_abstupleC [v] body = absfree (dest_Free v) body | mk_abstupleC (v :: w) body = let val (x, T) = dest_Free v; val z = mk_abstupleC w body; val T2 = (case z of Abs (_, T, _) => T | Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T); in Const (\<^const_name>\case_prod\, (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T, T2) --> HOLogic.boolT) $ absfree (x, T) z end; (** maps [x1,...,xn] to (x1,...,xn) and types**) fun mk_bodyC [] = HOLogic.unit | mk_bodyC [x] = x | mk_bodyC (x :: xs) = let val (_, T) = dest_Free x; val z = mk_bodyC xs; val T2 = (case z of Free (_, T) => T | Const (\<^const_name>\Pair\, Type ("fun", [_, Type ("fun", [_, T])])) $ _ $ _ => T); in Const (\<^const_name>\Pair\, [T, T2] ---> HOLogic.mk_prodT (T, T2)) $ x $ z end; (** maps a subgoal of the form: VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn] **) fun get_vars c = let val d = Logic.strip_assums_concl c; val Const _ $ pre $ _ $ _ = HOLogic.dest_Trueprop d; in mk_vars pre end; fun mk_CollectC tm = let val T as Type ("fun",[t,_]) = fastype_of tm; in HOLogic.Collect_const t $ tm end; fun inclt ty = Const (\<^const_name>\Orderings.less_eq\, [ty,ty] ---> HOLogic.boolT); in fun Mset ctxt prop = let val [(Mset, _), (P, _)] = Variable.variant_frees ctxt [] [("Mset", ()), ("P", ())]; val vars = get_vars prop; val varsT = fastype_of (mk_bodyC vars); val big_Collect = mk_CollectC (mk_abstupleC vars (Free (P, varsT --> HOLogic.boolT) $ mk_bodyC vars)); val small_Collect = mk_CollectC (Abs ("x", varsT, Free (P, varsT --> HOLogic.boolT) $ Bound 0)); val MsetT = fastype_of big_Collect; fun Mset_incl t = HOLogic.mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t); val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect); val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac ctxt 1); in (vars, th) end; end; (*****************************************************************************) (** Simplifying: **) (** Some useful lemmata, lists and simplification tactics to control which **) (** theorems are used to simplify at each moment, so that the original **) (** input does not suffer any unexpected transformation **) (*****************************************************************************) (**Simp_tacs**) fun before_set2pred_simp_tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}]); fun split_simp_tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]); (*****************************************************************************) (** set_to_pred_tac transforms sets inclusion into predicates implication, **) (** maintaining the original variable names. **) (** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1" **) (** Subgoals containing intersections (A Int B) or complement sets (-A) **) (** are first simplified by "before_set2pred_simp_tac", that returns only **) (** subgoals of the form "{x. P x} <= {x. Q x}", which are easily **) (** transformed. **) (** This transformation may solve very easy subgoals due to a ligth **) (** simplification done by (split_all_tac) **) (*****************************************************************************) fun set_to_pred_tac ctxt var_names = SUBGOAL (fn (_, i) => before_set2pred_simp_tac ctxt i THEN_MAYBE EVERY [ resolve_tac ctxt [subsetI] i, resolve_tac ctxt [CollectI] i, dresolve_tac ctxt [CollectD] i, TRY (split_all_tac ctxt i) THEN_MAYBE (rename_tac var_names i THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i)]); (*******************************************************************************) (** basic_simp_tac is called to simplify all verification conditions. It does **) (** a light simplification by applying "mem_Collect_eq", then it calls **) (** max_simp_tac, which solves subgoals of the form "A <= A", **) (** and transforms any other into predicates, applying then **) (** the tactic chosen by the user, which may solve the subgoal completely. **) (*******************************************************************************) fun max_simp_tac ctxt var_names tac = FIRST' [resolve_tac ctxt [subset_refl], set_to_pred_tac ctxt var_names THEN_MAYBE' tac]; fun basic_simp_tac ctxt var_names tac = simp_tac (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc]) THEN_MAYBE' max_simp_tac ctxt var_names tac; (** hoare_rule_tac **) fun hoare_rule_tac ctxt (vars, Mlem) tac = let val var_names = map (fst o dest_Free) vars; fun wlp_tac i = resolve_tac ctxt @{thms SeqRule} i THEN rule_tac false (i + 1) and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*) ((wlp_tac i THEN rule_tac pre_cond i) ORELSE (FIRST [ resolve_tac ctxt @{thms SkipRule} i, resolve_tac ctxt @{thms AbortRule} i, EVERY [ resolve_tac ctxt @{thms BasicRule} i, resolve_tac ctxt [Mlem] i, split_simp_tac ctxt i], EVERY [ resolve_tac ctxt @{thms CondRule} i, rule_tac false (i + 2), rule_tac false (i + 1)], EVERY [ resolve_tac ctxt @{thms WhileRule} i, basic_simp_tac ctxt var_names tac (i + 2), rule_tac true (i + 1)]] THEN ( if pre_cond then basic_simp_tac ctxt var_names tac i else resolve_tac ctxt [subset_refl] i))); in rule_tac end; (** tac is the tactic the user chooses to solve or simplify **) (** the final verification conditions **) fun hoare_tac ctxt tac = SUBGOAL (fn (goal, i) => SELECT_GOAL (hoare_rule_tac ctxt (Mset ctxt goal) tac true 1) i); + +(* total correctness rules *) + +fun hoare_tc_rule_tac ctxt (vars, Mlem) tac = + let + val var_names = map (fst o dest_Free) vars; + fun wlp_tac i = + resolve_tac ctxt @{thms SeqRuleTC} i THEN rule_tac false (i + 1) + and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*) + ((wlp_tac i THEN rule_tac pre_cond i) + ORELSE + (FIRST [ + resolve_tac ctxt @{thms SkipRuleTC} i, + EVERY [ + resolve_tac ctxt @{thms BasicRuleTC} i, + resolve_tac ctxt [Mlem] i, + split_simp_tac ctxt i], + EVERY [ + resolve_tac ctxt @{thms CondRuleTC} i, + rule_tac false (i + 2), + rule_tac false (i + 1)], + EVERY [ + resolve_tac ctxt @{thms WhileRuleTC} i, + basic_simp_tac ctxt var_names tac (i + 2), + rule_tac true (i + 1)]] + THEN ( + if pre_cond then basic_simp_tac ctxt var_names tac i + else resolve_tac ctxt [subset_refl] i))); + in rule_tac end; + + +fun hoare_tc_tac ctxt tac = SUBGOAL (fn (goal, i) => + SELECT_GOAL (hoare_tc_rule_tac ctxt (Mset ctxt goal) tac true 1) i); + end; diff --git a/src/HOL/Isar_Examples/Hoare.thy b/src/HOL/Isar_Examples/Hoare.thy --- a/src/HOL/Isar_Examples/Hoare.thy +++ b/src/HOL/Isar_Examples/Hoare.thy @@ -1,413 +1,419 @@ (* Title: HOL/Isar_Examples/Hoare.thy Author: Makarius A formulation of Hoare logic suitable for Isar. *) section \Hoare Logic\ theory Hoare imports Main begin subsection \Abstract syntax and semantics\ text \ The following abstract syntax and semantics of Hoare Logic over \<^verbatim>\WHILE\ programs closely follows the existing tradition in Isabelle/HOL of formalizing the presentation given in @{cite \\S6\ "Winskel:1993"}. See also \<^dir>\~~/src/HOL/Hoare\ and @{cite "Nipkow:1998:Winskel"}. \ type_synonym 'a bexp = "'a set" type_synonym 'a assn = "'a set" +type_synonym 'a var = "'a \ nat" datatype 'a com = Basic "'a \ 'a" | Seq "'a com" "'a com" ("(_;/ _)" [60, 61] 60) | Cond "'a bexp" "'a com" "'a com" - | While "'a bexp" "'a assn" "'a com" + | While "'a bexp" "'a assn" "'a var" "'a com" abbreviation Skip ("SKIP") where "SKIP \ Basic id" type_synonym 'a sem = "'a \ 'a \ bool" primrec iter :: "nat \ 'a bexp \ 'a sem \ 'a sem" where "iter 0 b S s s' \ s \ b \ s = s'" | "iter (Suc n) b S s s' \ s \ b \ (\s''. S s s'' \ iter n b S s'' s')" primrec Sem :: "'a com \ 'a sem" where "Sem (Basic f) s s' \ s' = f s" | "Sem (c1; c2) s s' \ (\s''. Sem c1 s s'' \ Sem c2 s'' s')" | "Sem (Cond b c1 c2) s s' \ (if s \ b then Sem c1 s s' else Sem c2 s s')" - | "Sem (While b x c) s s' \ (\n. iter n b (Sem c) s s')" + | "Sem (While b x y c) s s' \ (\n. iter n b (Sem c) s s')" definition Valid :: "'a bexp \ 'a com \ 'a bexp \ bool" ("(3\ _/ (2_)/ _)" [100, 55, 100] 50) where "\ P c Q \ (\s s'. Sem c s s' \ s \ P \ s' \ Q)" lemma ValidI [intro?]: "(\s s'. Sem c s s' \ s \ P \ s' \ Q) \ \ P c Q" by (simp add: Valid_def) lemma ValidD [dest?]: "\ P c Q \ Sem c s s' \ s \ P \ s' \ Q" by (simp add: Valid_def) subsection \Primitive Hoare rules\ text \ From the semantics defined above, we derive the standard set of primitive Hoare rules; e.g.\ see @{cite \\S6\ "Winskel:1993"}. Usually, variant forms of these rules are applied in actual proof, see also \S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}. \<^medskip> The \basic\ rule represents any kind of atomic access to the state space. This subsumes the common rules of \skip\ and \assign\, as formulated in \S\ref{sec:hoare-isar}. \ theorem basic: "\ {s. f s \ P} (Basic f) P" proof fix s s' assume s: "s \ {s. f s \ P}" assume "Sem (Basic f) s s'" then have "s' = f s" by simp with s show "s' \ P" by simp qed text \ The rules for sequential commands and semantic consequences are established in a straight forward manner as follows. \ theorem seq: "\ P c1 Q \ \ Q c2 R \ \ P (c1; c2) R" proof assume cmd1: "\ P c1 Q" and cmd2: "\ Q c2 R" fix s s' assume s: "s \ P" assume "Sem (c1; c2) s s'" then obtain s'' where sem1: "Sem c1 s s''" and sem2: "Sem c2 s'' s'" by auto from cmd1 sem1 s have "s'' \ Q" .. with cmd2 sem2 show "s' \ R" .. qed theorem conseq: "P' \ P \ \ P c Q \ Q \ Q' \ \ P' c Q'" proof assume P'P: "P' \ P" and QQ': "Q \ Q'" assume cmd: "\ P c Q" fix s s' :: 'a assume sem: "Sem c s s'" assume "s \ P'" with P'P have "s \ P" .. with cmd sem have "s' \ Q" .. with QQ' show "s' \ Q'" .. qed text \ The rule for conditional commands is directly reflected by the corresponding semantics; in the proof we just have to look closely which cases apply. \ theorem cond: assumes case_b: "\ (P \ b) c1 Q" and case_nb: "\ (P \ -b) c2 Q" shows "\ P (Cond b c1 c2) Q" proof fix s s' assume s: "s \ P" assume sem: "Sem (Cond b c1 c2) s s'" show "s' \ Q" proof cases assume b: "s \ b" from case_b show ?thesis proof from sem b show "Sem c1 s s'" by simp from s b show "s \ P \ b" by simp qed next assume nb: "s \ b" from case_nb show ?thesis proof from sem nb show "Sem c2 s s'" by simp from s nb show "s \ P \ -b" by simp qed qed qed text \ The \while\ rule is slightly less trivial --- it is the only one based on recursion, which is expressed in the semantics by a Kleene-style least fixed-point construction. The auxiliary statement below, which is by induction on the number of iterations is the main point to be proven; the rest is by routine application of the semantics of \<^verbatim>\WHILE\. \ theorem while: assumes body: "\ (P \ b) c P" - shows "\ P (While b X c) (P \ -b)" + shows "\ P (While b X Y c) (P \ -b)" proof fix s s' assume s: "s \ P" - assume "Sem (While b X c) s s'" + assume "Sem (While b X Y c) s s'" then obtain n where "iter n b (Sem c) s s'" by auto from this and s show "s' \ P \ -b" proof (induct n arbitrary: s) case 0 then show ?case by auto next case (Suc n) then obtain s'' where b: "s \ b" and sem: "Sem c s s''" and iter: "iter n b (Sem c) s'' s'" by auto from Suc and b have "s \ P \ b" by simp with body sem have "s'' \ P" .. with iter show ?case by (rule Suc) qed qed subsection \Concrete syntax for assertions\ text \ We now introduce concrete syntax for describing commands (with embedded expressions) and assertions. The basic technique is that of semantic ``quote-antiquote''. A \<^emph>\quotation\ is a syntactic entity delimited by an implicit abstraction, say over the state space. An \<^emph>\antiquotation\ is a marked expression within a quotation that refers the implicit argument; a typical antiquotation would select (or even update) components from the state. We will see some examples later in the concrete rules and applications. \<^medskip> The following specification of syntax and translations is for Isabelle experts only; feel free to ignore it. While the first part is still a somewhat intelligible specification of the concrete syntactic representation of our Hoare language, the actual ``ML drivers'' is quite involved. Just note that the we re-use the basic quote/antiquote translations as already defined in Isabelle/Pure (see \<^ML>\Syntax_Trans.quote_tr\, and \<^ML>\Syntax_Trans.quote_tr'\,). \ syntax "_quote" :: "'b \ ('a \ 'b)" "_antiquote" :: "('a \ 'b) \ 'b" ("\_" [1000] 1000) "_Subst" :: "'a bexp \ 'b \ idt \ 'a bexp" ("_[_'/\_]" [1000] 999) "_Assert" :: "'a \ 'a set" ("(\_\)" [0] 1000) "_Assign" :: "idt \ 'b \ 'a com" ("(\_ :=/ _)" [70, 65] 61) "_Cond" :: "'a bexp \ 'a com \ 'a com \ 'a com" ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61) "_While_inv" :: "'a bexp \ 'a assn \ 'a com \ 'a com" ("(0WHILE _/ INV _ //DO _ /OD)" [0, 0, 0] 61) "_While" :: "'a bexp \ 'a com \ 'a com" ("(0WHILE _ //DO _ /OD)" [0, 0] 61) translations "\b\" \ "CONST Collect (_quote b)" "B [a/\x]" \ "\\(_update_name x (\_. a)) \ B\" "\x := a" \ "CONST Basic (_quote (\(_update_name x (\_. a))))" "IF b THEN c1 ELSE c2 FI" \ "CONST Cond \b\ c1 c2" - "WHILE b INV i DO c OD" \ "CONST While \b\ i c" + "WHILE b INV i DO c OD" \ "CONST While \b\ i (\_. 0) c" "WHILE b DO c OD" \ "WHILE b INV CONST undefined DO c OD" parse_translation \ let fun quote_tr [t] = Syntax_Trans.quote_tr \<^syntax_const>\_antiquote\ t | quote_tr ts = raise TERM ("quote_tr", ts); in [(\<^syntax_const>\_quote\, K quote_tr)] end \ text \ As usual in Isabelle syntax translations, the part for printing is more complicated --- we cannot express parts as macro rules as above. Don't look here, unless you have to do similar things for yourself. \ print_translation \ let fun quote_tr' f (t :: ts) = Term.list_comb (f $ Syntax_Trans.quote_tr' \<^syntax_const>\_antiquote\ t, ts) | quote_tr' _ _ = raise Match; val assert_tr' = quote_tr' (Syntax.const \<^syntax_const>\_Assert\); fun bexp_tr' name ((Const (\<^const_syntax>\Collect\, _) $ t) :: ts) = quote_tr' (Syntax.const name) (t :: ts) | bexp_tr' _ _ = raise Match; fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = quote_tr' (Syntax.const \<^syntax_const>\_Assign\ $ Syntax_Trans.update_name_tr' f) (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) | assign_tr' _ = raise Match; in [(\<^const_syntax>\Collect\, K assert_tr'), (\<^const_syntax>\Basic\, K assign_tr'), (\<^const_syntax>\Cond\, K (bexp_tr' \<^syntax_const>\_Cond\)), (\<^const_syntax>\While\, K (bexp_tr' \<^syntax_const>\_While_inv\))] end \ subsection \Rules for single-step proof \label{sec:hoare-isar}\ text \ We are now ready to introduce a set of Hoare rules to be used in single-step structured proofs in Isabelle/Isar. We refer to the concrete syntax introduce above. \<^medskip> Assertions of Hoare Logic may be manipulated in calculational proofs, with the inclusion expressed in terms of sets or predicates. Reversed order is supported as well. \ lemma [trans]: "\ P c Q \ P' \ P \ \ P' c Q" by (unfold Valid_def) blast lemma [trans] : "P' \ P \ \ P c Q \ \ P' c Q" by (unfold Valid_def) blast lemma [trans]: "Q \ Q' \ \ P c Q \ \ P c Q'" by (unfold Valid_def) blast lemma [trans]: "\ P c Q \ Q \ Q' \ \ P c Q'" by (unfold Valid_def) blast lemma [trans]: "\ \\P\ c Q \ (\s. P' s \ P s) \ \ \\P'\ c Q" by (simp add: Valid_def) lemma [trans]: "(\s. P' s \ P s) \ \ \\P\ c Q \ \ \\P'\ c Q" by (simp add: Valid_def) lemma [trans]: "\ P c \\Q\ \ (\s. Q s \ Q' s) \ \ P c \\Q'\" by (simp add: Valid_def) lemma [trans]: "(\s. Q s \ Q' s) \ \ P c \\Q\ \ \ P c \\Q'\" by (simp add: Valid_def) text \ Identity and basic assignments.\<^footnote>\The \hoare\ method introduced in \S\ref{sec:hoare-vcg} is able to provide proper instances for any number of basic assignments, without producing additional verification conditions.\ \ lemma skip [intro?]: "\ P SKIP P" proof - have "\ {s. id s \ P} SKIP P" by (rule basic) then show ?thesis by simp qed lemma assign: "\ P [\a/\x::'a] \x := \a P" by (rule basic) text \ Note that above formulation of assignment corresponds to our preferred way to model state spaces, using (extensible) record types in HOL @{cite "Naraschewski-Wenzel:1998:HOOL"}. For any record field \x\, Isabelle/HOL provides a functions \x\ (selector) and \x_update\ (update). Above, there is only a place-holder appearing for the latter kind of function: due to concrete syntax \\x := \a\ also contains \x_update\.\<^footnote>\Note that due to the external nature of HOL record fields, we could not even state a general theorem relating selector and update functions (if this were required here); this would only work for any particular instance of record fields introduced so far.\ \<^medskip> Sequential composition --- normalizing with associativity achieves proper of chunks of code verified separately. \ lemmas [trans, intro?] = seq lemma seq_assoc [simp]: "\ P c1;(c2;c3) Q \ \ P (c1;c2);c3 Q" by (auto simp add: Valid_def) text \Conditional statements.\ lemmas [trans, intro?] = cond lemma [trans, intro?]: "\ \\P \ \b\ c1 Q \ \ \\P \ \ \b\ c2 Q \ \ \\P\ IF \b THEN c1 ELSE c2 FI Q" by (rule cond) (simp_all add: Valid_def) text \While statements --- with optional invariant.\ -lemma [intro?]: "\ (P \ b) c P \ \ P (While b P c) (P \ -b)" +lemma [intro?]: "\ (P \ b) c P \ \ P (While b P V c) (P \ -b)" by (rule while) -lemma [intro?]: "\ (P \ b) c P \ \ P (While b undefined c) (P \ -b)" +lemma [intro?]: "\ (P \ b) c P \ \ P (While b undefined V c) (P \ -b)" by (rule while) lemma [intro?]: "\ \\P \ \b\ c \\P\ \ \ \\P\ WHILE \b INV \\P\ DO c OD \\P \ \ \b\" by (simp add: while Collect_conj_eq Collect_neg_eq) lemma [intro?]: "\ \\P \ \b\ c \\P\ \ \ \\P\ WHILE \b DO c OD \\P \ \ \b\" by (simp add: while Collect_conj_eq Collect_neg_eq) subsection \Verification conditions \label{sec:hoare-vcg}\ text \ We now load the \<^emph>\original\ ML file for proof scripts and tactic definition for the Hoare Verification Condition Generator (see \<^dir>\~~/src/HOL/Hoare\). As far as we are concerned here, the result is a proof method \hoare\, which may be applied to a Hoare Logic assertion to extract purely logical verification conditions. It is important to note that the method requires \<^verbatim>\WHILE\ loops to be fully annotated with invariants beforehand. Furthermore, only \<^emph>\concrete\ pieces of code are handled --- the underlying tactic fails ungracefully if supplied with meta-variables or parameters, for example. \ lemma SkipRule: "p \ q \ Valid p (Basic id) q" by (auto simp add: Valid_def) lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) q" by (auto simp: Valid_def) lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (c1;c2) R" by (auto simp: Valid_def) lemma CondRule: "p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')} \ Valid w c1 q \ Valid w' c2 q \ Valid p (Cond b c1 c2) q" by (auto simp: Valid_def) lemma iter_aux: "\s s'. Sem c s s' \ s \ I \ s \ b \ s' \ I \ (\s s'. s \ I \ iter n b (Sem c) s s' \ s' \ I \ s' \ b)" by (induct n) auto lemma WhileRule: - "p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i c) q" + "p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i v c) q" apply (clarsimp simp: Valid_def) apply (drule iter_aux) prefer 2 apply assumption apply blast apply blast done lemma Compl_Collect: "- Collect b = {x. \ b x}" by blast lemmas AbortRule = SkipRule \ \dummy version\ +lemmas SeqRuleTC = SkipRule \ \dummy version\ +lemmas SkipRuleTC = SkipRule \ \dummy version\ +lemmas BasicRuleTC = SkipRule \ \dummy version\ +lemmas CondRuleTC = SkipRule \ \dummy version\ +lemmas WhileRuleTC = SkipRule \ \dummy version\ ML_file \~~/src/HOL/Hoare/hoare_tac.ML\ method_setup hoare = \Scan.succeed (fn ctxt => (SIMPLE_METHOD' (Hoare.hoare_tac ctxt (simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm "Record.K_record_comp"}] )))))\ "verification condition generator for Hoare logic" end diff --git a/src/HOL/Isar_Examples/Hoare_Ex.thy b/src/HOL/Isar_Examples/Hoare_Ex.thy --- a/src/HOL/Isar_Examples/Hoare_Ex.thy +++ b/src/HOL/Isar_Examples/Hoare_Ex.thy @@ -1,318 +1,318 @@ section \Using Hoare Logic\ theory Hoare_Ex imports Hoare begin subsection \State spaces\ text \ First of all we provide a store of program variables that occur in any of the programs considered later. Slightly unexpected things may happen when attempting to work with undeclared variables. \ record vars = I :: nat M :: nat N :: nat S :: nat text \ While all of our variables happen to have the same type, nothing would prevent us from working with many-sorted programs as well, or even polymorphic ones. Also note that Isabelle/HOL's extensible record types even provides simple means to extend the state space later. \ subsection \Basic examples\ text \ We look at few trivialities involving assignment and sequential composition, in order to get an idea of how to work with our formulation of Hoare Logic. \<^medskip> Using the basic \assign\ rule directly is a bit cumbersome. \ lemma "\ \\(N_update (\_. (2 * \N))) \ \\N = 10\\ \N := 2 * \N \\N = 10\" by (rule assign) text \ Certainly we want the state modification already done, e.g.\ by simplification. The \hoare\ method performs the basic state update for us; we may apply the Simplifier afterwards to achieve ``obvious'' consequences as well. \ lemma "\ \True\ \N := 10 \\N = 10\" by hoare lemma "\ \2 * \N = 10\ \N := 2 * \N \\N = 10\" by hoare lemma "\ \\N = 5\ \N := 2 * \N \\N = 10\" by hoare simp lemma "\ \\N + 1 = a + 1\ \N := \N + 1 \\N = a + 1\" by hoare lemma "\ \\N = a\ \N := \N + 1 \\N = a + 1\" by hoare simp lemma "\ \a = a \ b = b\ \M := a; \N := b \\M = a \ \N = b\" by hoare lemma "\ \True\ \M := a; \N := b \\M = a \ \N = b\" by hoare lemma "\ \\M = a \ \N = b\ \I := \M; \M := \N; \N := \I \\M = b \ \N = a\" by hoare simp text \ It is important to note that statements like the following one can only be proven for each individual program variable. Due to the extra-logical nature of record fields, we cannot formulate a theorem relating record selectors and updates schematically. \ lemma "\ \\N = a\ \N := \N \\N = a\" by hoare lemma "\ \\x = a\ \x := \x \\x = a\" oops lemma "Valid {s. x s = a} (Basic (\s. x_update (x s) s)) {s. x s = n}" \ \same statement without concrete syntax\ oops text \ In the following assignments we make use of the consequence rule in order to achieve the intended precondition. Certainly, the \hoare\ method is able to handle this case, too. \ lemma "\ \\M = \N\ \M := \M + 1 \\M \ \N\" proof - have "\\M = \N\ \ \\M + 1 \ \N\" by auto also have "\ \ \M := \M + 1 \\M \ \N\" by hoare finally show ?thesis . qed lemma "\ \\M = \N\ \M := \M + 1 \\M \ \N\" proof - have "m = n \ m + 1 \ n" for m n :: nat \ \inclusion of assertions expressed in ``pure'' logic,\ \ \without mentioning the state space\ by simp also have "\ \\M + 1 \ \N\ \M := \M + 1 \\M \ \N\" by hoare finally show ?thesis . qed lemma "\ \\M = \N\ \M := \M + 1 \\M \ \N\" by hoare simp subsection \Multiplication by addition\ text \ We now do some basic examples of actual \<^verbatim>\WHILE\ programs. This one is a loop for calculating the product of two natural numbers, by iterated addition. We first give detailed structured proof based on single-step Hoare rules. \ lemma "\ \\M = 0 \ \S = 0\ WHILE \M \ a DO \S := \S + b; \M := \M + 1 OD \\S = a * b\" proof - let "\ _ ?while _" = ?thesis let "\\?inv\" = "\\S = \M * b\" have "\\M = 0 \ \S = 0\ \ \\?inv\" by auto also have "\ \ ?while \\?inv \ \ (\M \ a)\" proof let ?c = "\S := \S + b; \M := \M + 1" have "\\?inv \ \M \ a\ \ \\S + b = (\M + 1) * b\" by auto also have "\ \ ?c \\?inv\" by hoare finally show "\ \\?inv \ \M \ a\ ?c \\?inv\" . qed also have "\ \ \\S = a * b\" by auto finally show ?thesis . qed text \ The subsequent version of the proof applies the \hoare\ method to reduce the Hoare statement to a purely logical problem that can be solved fully automatically. Note that we have to specify the \<^verbatim>\WHILE\ loop invariant in the original statement. \ lemma "\ \\M = 0 \ \S = 0\ WHILE \M \ a INV \\S = \M * b\ DO \S := \S + b; \M := \M + 1 OD \\S = a * b\" by hoare auto subsection \Summing natural numbers\ text \ We verify an imperative program to sum natural numbers up to a given limit. First some functional definition for proper specification of the problem. \<^medskip> The following proof is quite explicit in the individual steps taken, with the \hoare\ method only applied locally to take care of assignment and sequential composition. Note that we express intermediate proof obligation in pure logic, without referring to the state space. \ theorem "\ \True\ \S := 0; \I := 1; WHILE \I \ n DO \S := \S + \I; \I := \I + 1 OD \\S = (\j" (is "\ _ (_; ?while) _") proof - let ?sum = "\k::nat. \j \True\ \S := 0; \I := 1 \?inv \S \I\" proof - have "True \ 0 = ?sum 1" by simp also have "\ \\\ \S := 0; \I := 1 \?inv \S \I\" by hoare finally show ?thesis . qed also have "\ \ ?while \?inv \S \I \ \ \I \ n\" proof let ?body = "\S := \S + \I; \I := \I + 1" have "?inv s i \ i \ n \ ?inv (s + i) (i + 1)" for s i by simp also have "\ \\S + \I = ?sum (\I + 1)\ ?body \?inv \S \I\" by hoare finally show "\ \?inv \S \I \ \I \ n\ ?body \?inv \S \I\" . qed also have "s = ?sum i \ \ i \ n \ s = ?sum n" for s i by simp finally show ?thesis . qed text \ The next version uses the \hoare\ method, while still explaining the resulting proof obligations in an abstract, structured manner. \ theorem "\ \True\ \S := 0; \I := 1; WHILE \I \ n INV \\S = (\j<\I. j)\ DO \S := \S + \I; \I := \I + 1 OD \\S = (\j" proof - let ?sum = "\k::nat. \j i \ n" for s i using that by simp show "s = ?sum n" if "?inv s i \ \ i \ n" for s i using that by simp qed qed text \ Certainly, this proof may be done fully automatic as well, provided that the invariant is given beforehand. \ theorem "\ \True\ \S := 0; \I := 1; WHILE \I \ n INV \\S = (\j<\I. j)\ DO \S := \S + \I; \I := \I + 1 OD \\S = (\j" by hoare auto subsection \Time\ text \ A simple embedding of time in Hoare logic: function \timeit\ inserts an extra variable to keep track of the elapsed time. \ record tstate = time :: nat type_synonym 'a time = "\time :: nat, \ :: 'a\" primrec timeit :: "'a time com \ 'a time com" where "timeit (Basic f) = (Basic f; Basic(\s. s\time := Suc (time s)\))" | "timeit (c1; c2) = (timeit c1; timeit c2)" | "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)" - | "timeit (While b iv c) = While b iv (timeit c)" + | "timeit (While b iv v c) = While b iv v (timeit c)" record tvars = tstate + I :: nat J :: nat lemma lem: "(0::nat) < n \ n + n \ Suc (n * n)" by (induct n) simp_all lemma "\ \i = \I \ \time = 0\ (timeit (WHILE \I \ 0 INV \2 *\ time + \I * \I + 5 * \I = i * i + 5 * i\ DO \J := \I; WHILE \J \ 0 INV \0 < \I \ 2 * \time + \I * \I + 3 * \I + 2 * \J - 2 = i * i + 5 * i\ DO \J := \J - 1 OD; \I := \I - 1 OD)) \2 * \time = i * i + 5 * i\" apply simp apply hoare apply simp apply clarsimp apply clarsimp apply arith prefer 2 apply clarsimp apply (clarsimp simp: nat_distrib) apply (frule lem) apply arith done end