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.

2 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. One of the examples concerns the theory of modelchecking, and another is drawn from a classic textbook on formal languages.

3 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.

4 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. 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).

5 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.. Definitions.

6 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.

7 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.. Suppressing Output..63 Part II. Logic and Sets5. The Rules of the Natural Deduction.. Introduction Rules.. Elimination Rules.. Destruction Rules: Some Examples.. Implication.

8 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.

9 Finding More Theorems.. Forward Proof: Transforming Theorems.. Modifying a Theorem usingof,whereandTHEN.. Modifying a Theorem usingOF.. Forward Reasoning in a Backward Proof.. The Methodinsert.. 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.

10 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.