HOL Isabelle

1 Tobias NipkowLawrence C. PaulsonMarkus Wenzel = Isabelle HOLA proof Assistant forHigher-Order LogicDecember 12, 2021 Springer-VerlagBerlin Heidelberg NewYorkLondon Paris TokyoHong Kong BarcelonaBudapestPrefaceThis volume is a self-contained introduction to interactive proof in higher-order logic (HOL), using the proof assistant Isabelle . It is written for potentialusers rather than for our colleagues in the research book has three parts. The first part,Elementary Techniques, shows how to model functionalprograms in higher-order logic . Early examples involve lists and the naturalnumbers. Most proofs are two steps long, consisting of induction on achosen variable followed by theautotactic. But even this elementary partcovers such advanced topics as nested and mutual recursion. The second part, logic and Sets, presents a collection of lower-leveltactics that you can use to apply rules selectively. It also describes Isa-belle/HOL s treatment of sets, functions and relations and explains how todefine sets inductively.

2 One of the examples concerns the theory of modelchecking, and another is drawn from a classic textbook on formal languages. The third part,Advanced Material, describes a variety of other these are the real numbers, records and overloading. Advancedtechniques for induction and recursion are described. A whole chapter isdevoted to an extended example: the verification of a security typesetting relies on Wenzel s theory presentation tools. An anno-tated source file is run, typesetting the theory in the form of a LATEX sourcefile. This book is derived almost entirely from output generated in this final chapter of Part I explains how users may produce their own formaldocuments in a similar sweb site1contains links to the download area and to documenta-tion and other information. The classic Isabelle user interface is proof Gen-eral / Emacs by David Aspinall s. This book says very little about ProofGeneral, which has its own tutorial owes a lot to the constant discussions with and the valuablefeedback from the Isabelle group at Munich: Stefan Berghofer, Olaf M uller,Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, CorneliaPusch, Norbert Schirmer and Martin Strecker.

3 Stephan Merz was also kind1 to read and comment on a draft version. We received comments fromStefano Bistarelli, Gergely Buday, John Matthews and Tanja research has been funded by many sources, including thedfggrants NI 491/2, NI 491/3, NI 491/4, NI 491/6,bmbfproject Verisoft,theepsrcgrants GR/K57381, GR/K77051, GR/M75440, GR/R01156/01GR/S57198/01 and by theespritworking groups 21900 and IST-1999-29001(theTypesproject).Table of ContentsPart I. Elementary Techniques1. The Introduction.. Theories.. Types, Terms and Formulae.. Variables.. Interaction and Interfaces.. Getting Started..82. Functional Programming in An Introductory Theory.. Evaluation.. An Introductory proof .. Some Helpful Commands.. Datatypes.. Lists.. The General Format.. Primitive Recursion.. Case Expressions.. Structural Induction and Case Distinction.. Case Study: Boolean Expressions.. Some Basic Types.. Natural Numbers.. Pairs.. Datatypeoption.

4 Definitions.. Type Synonyms.. Constant Definitions.. The Definitional Approach..253. More Functional Simplification.. What is Simplification?.. Simplification Rules..28viTable of ThesimpMethod.. Adding and Deleting Simplification Rules.. Assumptions.. Rewriting with Definitions.. Simplifyinglet-Expressions.. Conditional Simplification Rules.. Automatic Case Splits.. Tracing.. Finding Theorems.. Induction Heuristics.. Case Study: Compiling Expressions.. Advanced Datatypes.. Mutual Recursion.. Nested Recursion.. The Limits of Nested Recursion.. Case Study: Tries.. Total Recursive Functions:fun.. Definition.. Termination.. Simplification.. Induction..504. Presenting Concrete Syntax.. Infix Annotations.. Mathematical Symbols.. Prefix Annotations.. Abbreviations.. Document Preparation.. Isabelle Sessions.. Structure Markup.. Formal Comments and Antiquotations.. Interpretation of Symbols.

5 Suppressing Output..63 Part II. logic and Sets5. The Rules of the Natural Deduction.. Introduction Rules.. Elimination Rules.. Destruction Rules: Some Examples.. Implication.. Negation..73 Table of Interlude: the Basic Methods for Rules.. Unification and Substitution.. Substitution and thesubstMethod.. Unification and Its Pitfalls.. Quantifiers.. The Universal Introduction Rule.. The Universal Elimination Rule.. The Existential Quantifier.. Renaming a Bound Variable:rename_tac.. Reusing an Assumption:frule.. Instantiating a Quantifier Explicitly.. Description Operators.. Definite Descriptions.. Indefinite Descriptions.. Some Proofs That Fail.. Proving Theorems Using theblastMethod.. Other Classical Reasoning Methods.. Finding More Theorems.. Forward proof : Transforming Theorems.. Modifying a Theorem usingof,whereandTHEN.. Modifying a Theorem usingOF.. Forward Reasoning in a Backward proof .. The Methodinsert.

6 The Methodsubgoal_tac.. Managing Large Proofs.. Tacticals, or Control Structures.. Subgoal Numbering.. Proving the Correctness of Euclid s Algorithm..1036. Sets, Functions and Sets.. Finite Set Notation.. Set Comprehension.. Binding Operators.. Finiteness and Cardinality.. Functions.. Function Basics.. Injections, Surjections, Bijections.. Function Image.. Relations.. Relation Basics.. The Reflexive and Transitive Closure.. A Sample proof .. Well-Founded Relations and Induction.. Fixed Point Operators..117viiiTable of Propositional Dynamic logic PDL.. Computation Tree logic CTL..1217. Inductively Defined The Set of Even Numbers.. Making an Inductive Definition.. Using Introduction Rules.. Rule Induction.. Generalization and Rule Induction.. Rule Inversion.. Mutually Inductive Definitions.. Inductively Defined Predicates.. The Reflexive Transitive Closure.. Advanced Inductive Definitions.

7 Universal Quantifiers in Introduction Rules.. Alternative Definition Using a Monotone Function.. A proof of Equivalence.. Another Example of Rule Inversion.. Case Study: A Context Free Grammar..141 Part III. Advanced Material8. More about Pairs and Tuples.. Pattern Matching with Tuples.. Theorem Proving.. Records.. Record Basics.. Extensible Records and Generic Operations.. Record Equality.. Extending and Truncating Records.. Type Classes.. Overloading.. Axioms.. Numbers.. Numeric Literals.. The Type of Natural Numbers,nat.. The Type of Integers,int.. The Types of Rational, Real and Complex Numbers.. The Numeric Type Classes.. Introducing New Types.. Declaring New Types.. Defining New Types..171 Table of Contentsix9. Advanced Simplification and Simplification.. Advanced Features.. How the Simplifier Works.. Advanced Induction Techniques.. Massaging the Proposition.. Beyond Structural and Recursion Induction.

8 Derivation of New Induction Schemas.. CTL Revisited..18210. Case Study: Verifying a Security The Needham-Schroeder Public-Key Protocol.. Agents and Messages.. Modelling the Adversary.. Event Traces.. Modelling the Protocol.. Proving Elementary Properties.. Proving Secrecy Theorems..195A. of ContentsPart IElementary Techniques1. The IntroductionThis book is a tutorial on how to use the theorem prover Isabelle /HOL as aspecification and verification system. Isabelle is a generic system for imple-menting logical formalisms, and Isabelle /HOL is the specialization of Isabellefor HOL, which abbreviates Higher-Order logic . We introduce HOL step bystep following the equationHOL=Functional Programming+ do not assume that you are familiar with mathematical logic . However, wedo assume that you are used to logical and set theoretic notation, as coveredin a good discrete mathematics course [34], and that you are familiar withthe basic concepts of functional programming [5, 14, 29, 35].

9 Although thistutorial initially concentrates on functional programming, do not be misled:HOL can express most mathematical concepts, and functional programmingis just one particularly simple and ubiquitous [28] is implemented in ML [19]. This has influenced some of Isa-belle/HOL s concrete syntax but is otherwise irrelevant for us: this tutorialis based on Isabelle /Isar [37], an extension of Isabelle which hides the im-plementation language almost completely. Thus the full name of the systemshould be Isabelle /Isar/HOL, but that is a bit of a are other implementations of HOL, in particular the one by MikeGordonet al., which is usually referred to as the HOL system [10]. Forus, HOL refers to the logical system, and sometimes its incarnation Isa- tutorial is by definition incomplete. Currently the tutorial only intro-duces the rudiments of Isar s proof language. To fully exploit the power ofIsar, in particular the ability to write readable and structured proofs, youshould start with Nipkow s overview [24] and consult the Isabelle /Isar Refer-ence Manual [37] and Wenzel s PhD thesis [38] (which discusses many proofpatterns) for further details.

10 If you want to use Isabelle s ML level directly(for example for writing your own proof procedures) see the Isabelle ReferenceManual [26]; for details relating to HOL see the Isabelle /HOL manual [25].All manuals have a comprehensive The TheoriesWorking with Isabelle means creating theories. Roughly speaking, atheoryis a named collection of types, functions, and theorems, much like a modulein a programming language or a specification in a specification language. Infact, theories in HOL can be either. The general format of a theoryTistheory Timports , definitions, and proofsendwhereB1..Bnare the names of existing theories thatTis based on anddeclarations, definitions, and proofsrepresents the newly introduced concepts(types, functions etc.) and proofs about them. TheBiare the directparenttheoriesofT. Everything defined in the parent theories (and their parents,recursively) is automatically visible. To avoid name clashes, identifiers canbequalifiedby theory names as Each theoryTmust residein atheory tutorial is concerned with introducing you to the different linguisticconstructs that can fill thedeclarations, definitions, and proofsabove.