The Isabelle/Isar Reference Manual

Markus Wenzel TU München 1 October 2005

Contents

1 Introduction 1 1.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Quick start . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

1.2.1 Terminal sessions . . . . . . . . . . . . . . . . . . . . . 2 1.2.2 Proof General . . . . . . . . . . . . . . . . . . . . . . . 2

1.3 Isabelle/Isar theories . . . . . . . . . . . . . . . . . . . . . . . 4 1.3.1 Document preparation . . . . . . . . . . . . . . . . . . 5 1.3.2 How to write Isar proofs anyway? . . . . . . . . . . . . 6

2 Syntax primitives 7 2.1 Lexical matters . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2 Common syntax entities . . . . . . . . . . . . . . . . . . . . . 9

2.2.1 Names . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.2.2 Comments . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.2.3 Type classes, sorts and arities . . . . . . . . . . . . . . 10 2.2.4 Types and terms . . . . . . . . . . . . . . . . . . . . . 11 2.2.5 Mixfix annotations . . . . . . . . . . . . . . . . . . . . 12 2.2.6 Proof methods . . . . . . . . . . . . . . . . . . . . . . 13 2.2.7 Attributes and theorems . . . . . . . . . . . . . . . . . 14 2.2.8 Term patterns and declarations . . . . . . . . . . . . . 16 2.2.9 Antiquotations . . . . . . . . . . . . . . . . . . . . . . 18 2.2.10 Tagged commands . . . . . . . . . . . . . . . . . . . . 22

3 Basic language elements 24

3.1 Theory commands . . . . . . . . . . . . . . . . . . . . . . . . 24 3.1.1 Defining theories . . . . . . . . . . . . . . . . . . . . . 24 3.1.2 Markup commands . . . . . . . . . . . . . . . . . . . . 26 3.1.3 Type classes and sorts . . . . . . . . . . . . . . . . . . 27 3.1.4 Primitive types and type abbreviations . . . . . . . . . 28 3.1.5 Constants and simple definitions . . . . . . . . . . . . . 29 3.1.6 Syntax and translations . . . . . . . . . . . . . . . . . 30 3.1.7 Axioms and theorems . . . . . . . . . . . . . . . . . . . 32 3.1.8 Name spaces . . . . . . . . . . . . . . . . . . . . . . . . 32 3.1.9 Incorporating ML code . . . . . . . . . . . . . . . . . . 33 3.1.10 Syntax translation functions . . . . . . . . . . . . . . . 35 3.1.11 Oracles . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

3.2 Proof commands . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.2.1 Markup commands . . . . . . . . . . . . . . . . . . . . 37 3.2.2 Context elements . . . . . . . . . . . . . . . . . . . . . 37 3.2.3 Facts and forward chaining . . . . . . . . . . . . . . . . 39 3.2.4 Goal statements . . . . . . . . . . . . . . . . . . . . . . 40 3.2.5 Initial and terminal proof steps . . . . . . . . . . . . . 43 3.2.6 Fundamental methods and attributes . . . . . . . . . . 45 3.2.7 Term abbreviations . . . . . . . . . . . . . . . . . . . . 47 3.2.8 Block structure . . . . . . . . . . . . . . . . . . . . . . 49 3.2.9 Emulating tactic scripts . . . . . . . . . . . . . . . . . 49 3.2.10 Meta-linguistic features . . . . . . . . . . . . . . . . . . 51

3.3 Other commands . . . . . . . . . . . . . . . . . . . . . . . . . 51 3.3.1 Diagnostics . . . . . . . . . . . . . . . . . . . . . . . . 51 3.3.2 Inspecting the context . . . . . . . . . . . . . . . . . . 53 3.3.3 History commands . . . . . . . . . . . . . . . . . . . . 55 3.3.4 System operations . . . . . . . . . . . . . . . . . . . . 56

4 Generic tools and packages 57

4.1 Theory specification commands . . . . . . . . . . . . . . . . . 57 4.1.1 Axiomatic type classes . . . . . . . . . . . . . . . . . . 57 4.1.2 Locales and local contexts . . . . . . . . . . . . . . . . 58

4.2 Derived proof schemes . . . . . . . . . . . . . . . . . . . . . . 65 4.2.1 Generalized elimination . . . . . . . . . . . . . . . . . . 65 4.2.2 Calculational reasoning . . . . . . . . . . . . . . . . . . 66

4.3 Proof tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 4.3.1 Miscellaneous methods and attributes . . . . . . . . . . 68 4.3.2 Further tactic emulations . . . . . . . . . . . . . . . . . 71 4.3.3 The Simplifier . . . . . . . . . . . . . . . . . . . . . . . 73 4.3.4 The Classical Reasoner . . . . . . . . . . . . . . . . . . 77 4.3.5 Proof by cases and induction . . . . . . . . . . . . . . . 82

5 Object-logic specific elements 88 5.1 General logic setup . . . . . . . . . . . . . . . . . . . . . . . . 88 5.2 HOL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89

5.2.1 Primitive types . . . . . . . . . . . . . . . . . . . . . . 89 5.2.2 Adhoc tuples . . . . . . . . . . . . . . . . . . . . . . . 91 5.2.3 Records . . . . . . . . . . . . . . . . . . . . . . . . . . 91 5.2.4 Datatypes . . . . . . . . . . . . . . . . . . . . . . . . . 95 5.2.5 Recursive functions . . . . . . . . . . . . . . . . . . . . 96 5.2.6 Definition by specification . . . . . . . . . . . . . . . . 98 5.2.7 (Co)Inductive sets . . . . . . . . . . . . . . . . . . . . 99 5.2.8 Arithmetic proof support . . . . . . . . . . . . . . . . . 100 5.2.9 Cases and induction: emulating tactic scripts . . . . . 101 5.2.10 Executable code . . . . . . . . . . . . . . . . . . . . . . 102

5.3 HOLCF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 5.3.1 Mixfix syntax for continuous operations . . . . . . . . . 104 5.3.2 Recursive domains . . . . . . . . . . . . . . . . . . . . 104

5.4 ZF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 5.4.1 Type checking . . . . . . . . . . . . . . . . . . . . . . . 105 5.4.2 (Co)Inductive sets and datatypes . . . . . . . . . . . . 105

A Isabelle/Isar quick reference 109

A.1 Proof commands . . . . . . . . . . . . . . . . . . . . . . . . . 109 A.1.1 Primitives and basic syntax . . . . . . . . . . . . . . . 109 A.1.2 Abbreviations and synonyms . . . . . . . . . . . . . . . 110 A.1.3 Derived elements . . . . . . . . . . . . . . . . . . . . . 110 A.1.4 Diagnostic commands . . . . . . . . . . . . . . . . . . . 110

A.2 Proof methods . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 A.3 Attributes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 A.4 Rule declarations and methods . . . . . . . . . . . . . . . . . 112 A.5 Emulating tactic scripts . . . . . . . . . . . . . . . . . . . . . 113

A.5.1 Commands . . . . . . . . . . . . . . . . . . . . . . . . 113 A.5.2 Methods . . . . . . . . . . . . . . . . . . . . . . . . . . 113

B Isabelle/Isar conversion guide 114

B.1 No conversion . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 B.1.1 Referring to theorem and theory values . . . . . . . . . 114 B.1.2 Storing theorem values . . . . . . . . . . . . . . . . . . 115 B.1.3 ML declarations in Isar . . . . . . . . . . . . . . . . . . 115

B.2 Porting theories and proof scripts . . . . . . . . . . . . . . . . 116 B.2.1 Theories . . . . . . . . . . . . . . . . . . . . . . . . . . 116 B.2.2 Goal statements . . . . . . . . . . . . . . . . . . . . . . 117 B.2.3 Tactics . . . . . . . . . . . . . . . . . . . . . . . . . . . 119 B.2.4 Declarations and ad-hoc operations . . . . . . . . . . . 123

B.3 Writing actual Isar proof texts . . . . . . . . . . . . . . . . . . 124 CONTENTS iv

Chapter 1

Introduction

1.1 Overview

The Isabelle system essentially provides a generic infrastructure for building deductive systems (programmed in Standard ML), with a special focus on interactive theorem proving in higher-order logics. In the olden days even end-users would refer to certain ML functions (goal commands, tactics, tacticals etc.) to pursue their everyday theorem proving tasks [9, 10].

In contrast Isar provides an interpreted language environment of its own, which has been specifically tailored for the needs of theory and proof development. Compared to raw ML, the Isabelle/Isar top-level provides a more robust and comfortable development platform, with proper support for theory development graphs, single-step transactions with unlimited undo, etc. The Isabelle/Isar version of the Proof General user interface [1, 2] provides an adequate front-end for interactive theory and proof development in this advanced theorem proving environment.

Apart from the technical advances over bare-bones ML programming, the main purpose of the Isar language is to provide a conceptually different view on machine-checked proofs [15, 17]. “Isar” stands for “Intelligible semi-automated reasoning”. Drawing from both the traditions of informal mathematical proof texts and high-level programming languages, Isar offers a versatile environment for structured formal proof documents. Thus properly written Isar proofs become accessible to a broader audience than unstructured tactic scripts (which typically only provide operational information for the machine). Writing human-readable proof texts certainly requires some additional efforts by the writer to achieve a good presentation, both of formal and informal parts of the text. On the other hand, human-readable formal texts gain some value in their own right, independently of the mechanic proof-checking process.

Despite its grand design of structured proof texts, Isar is able to assimilate the old tactical style as an “improper” sub-language. This provides an easy upgrade path for existing tactic scripts, as well as additional means for interactive experimentation and debugging of structured proofs. Isabelle/Isar supports a broad range of proof styles, both readable and unreadable ones.

The Isabelle/Isar framework is generic and should work reasonably well for any Isabelle object-logic that conforms to the natural deduction view of the Isabelle/Pure framework. Major Isabelle logics like HOL [7], HOLCF [5], FOL [11], and ZF [12] have already been set up for end-users. Nonetheless, much of the existing body of theories still consist of old-style theory files with accompanied ML code for proof scripts; this legacy will be gradually converted in due time.

1.2 Quick start

1.2.1 Terminal sessions

Isar is already part of Isabelle. The low-level isabelle binary provides option -I to run the Isabelle/Isar interaction loop at startup, rather than the raw ML top-level. So the most basic way to do anything with Isabelle/Isar is as follows:

      isabelle -I HOL
       > Welcome to Isabelle/HOL (Isabelle2005)
      theory Foo imports Main begin;
      constdefs foo :: nat  "foo == 1";
      lemma "0 < foo" by (simp add: foo_def);
      end;

Note that any Isabelle/Isar command may be retracted by undo. See the Isabelle/Isar Quick Reference (appendix A) for a comprehensive overview of available commands and other language elements.

1.2.2 Proof General

Plain TTY-based interaction as above used to be quite feasible with traditional tactic based theorem proving, but developing Isar documents really demands some better user-interface support. The Proof General environment by David Aspinall [1, 2] offers a generic Emacs interface for interactive theorem provers that organizes all the cut-and-paste and forward-backward walk through the text in a very neat way. In Isabelle/Isar, the current position within a partial proof document is equally important than the actual proof state. Thus Proof General provides the canonical working environment for Isabelle/Isar, both for getting acquainted (e.g. by replaying existing Isar documents) and for production work.

Proof General as default Isabelle interface

The Isabelle interface wrapper script provides an easy way to invoke Proof General (including XEmacs or GNU Emacs). The default configuration of Isabelle is smart enough to detect the Proof General distribution in several

canonical places (e.g. $ISABELLE_HOME/contrib/ProofGeneral). Thus the

capital Isabelle executable would already refer to the ProofGeneral/isar interface without further ado.^{1} The Isabelle interface script provides several options; pass -? to see its usage.

With the proper Isabelle interface setup, Isar documents may now be edited by visiting appropriate theory files, e.g.

      Isabelle ⟨isabellehome⟩/src/HOL/Isar_examples/Summation.thy

Beginners may note the tool bar for navigating forward and backward through the text (this depends on the local Emacs installation). Consult the Proof General documentation [1] for further basic command sequences, in particular “C-c C-return” and “C-c u”.

Proof General may be also configured manually by giving Isabelle settings like this (see also [18]):

      ISABELLE_INTERFACE=$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
      PROOFGENERAL_OPTIONS=""
You may have to change $ISABELLE_HOME/contrib/ProofGeneral to the

actual installation directory of Proof General.

Apart from the Isabelle command line, defaults for interface options may be given by the PROOFGENERAL_OPTIONS setting. For example, the Emacs executable to be used may be configured in Isabelle’s settings like this:

      PROOFGENERAL_OPTIONS="-p xemacs-mule"

Occasionally, a user’s ~/.emacs file contains code that is incompatible with the (X)Emacs version used by Proof General, causing the interface startup to fail prematurely. Here the -u false option helps to get the interface process up and running. Note that additional Lisp customization

code may reside in proofgeneral-settings.el of $ISABELLE_HOME/etc or
$ISABELLE_HOME_USER/etc.

1There is also a ProofGeneral/isa interface for old tactic scripts written in ML.

The X-Symbol package

Proof General provides native support for the Emacs X-Symbol package [13], which handles proper mathematical symbols displayed on screen. Pass option -x true to the Isabelle interface script, or check the appropriate Proof General menu setting by hand. In any case, the X-Symbol package must have been properly installed already.

Contrary to what you may expect from the documentation of X-Symbol, the package is very easy to install and configures itself automatically. The default configuration of Isabelle is smart enough to detect the X-Symbol package in several canonical places (e.g. $ISABELLE_HOME/contrib/x-symbol).

Using proper mathematical symbols in Isabelle theories can be very convenient for readability of large formulas. On the other hand, the plain ASCII sources easily become somewhat unintelligible. For example, ⟹ would appear as \<Longrightarrow> according the default set of Isabelle symbols. Nevertheless, the Isabelle document preparation system (see §1.3.1) will be happy to print non-ASCII symbols properly. It is even possible to invent additional notation beyond the display capabilities of Emacs and X-Symbol.

1.3 Isabelle/Isar theories

Isabelle/Isar offers the following main improvements over classic Isabelle.

1. A new theory format, occasionally referred to as “new-style theories”, supporting interactive development and unlimited undo operation.

2. A formal proof document language designed to support intelligible semiautomated reasoning. Instead of putting together unreadable tactic scripts, the author is enabled to express the reasoning in way that is close to usual mathematical practice. The old tactical style has been assimilated as “improper” language elements.

3. A simple document preparation system, for typesetting formal developments together with informal text. The resulting hyper-linked PDF documents are equally well suited for WWW presentation and as printed copies.

The Isar proof language is embedded into the new theory format as a proper sub-language. Proof mode is entered by stating some theorem or lemma at the theory level, and left again with the final conclusion (e.g. via qed). A few theory specification mechanisms also require some proof, such as HOL’s typedef which demands non-emptiness of the representing sets.

New-style theory files may still be associated with separate ML files consisting of plain old tactic scripts. There is no longer any ML binding generated for the theory and theorems, though. ML functions theory, thm, and thms retrieve this information from the context [10]. Nevertheless, migration between classic Isabelle and Isabelle/Isar is relatively easy. Thus users may start to benefit from interactive theory development and document preparation, even before they have any idea of the Isar proof language at all.

! Proof General does not support mixed interactive development of classic Isa-

belle theory files or tactic scripts, together with Isar documents. The “isa” and “isar” versions of Proof General are handled as two different theorem proving systems, only one of these may be active at the same time.

Manual conversion of existing tactic scripts may be done by running two separate Proof General sessions, one for replaying the old script and the other for the emerging Isabelle/Isar document. Also note that Isar supports emulation commands and methods that support traditional tactic scripts within new-style theories, see appendix B for more information.

1.3.1 Document preparation

Isabelle/Isar provides a simple document preparation system based on existing PDF-L^{A}TEX technology, with full support of hyper-links (both local references and URLs), bookmarks, and thumbnails. Thus the results are equally well suited for WWW browsing and as printed copies.

Isabelle generates L^{A}TEX output as part of the run of a logic session (see also [18]). Getting started with a working configuration for common situations is quite easy by using the Isabelle mkdir and make tools. First invoke

        isatool mkdir Foo

to initialize a separate directory for session Foo — it is safe to experiment, since isatool mkdir never overwrites existing files. Ensure that Foo/ROOT.ML holds ML commands to load all theories required for this session; furthermore Foo/document/root.tex should include any special L^{A}TEX macro packages required for your document (the default is usually sufficient as a start).

The session is controlled by a separate IsaMakefile (with crude source dependencies by default). This file is located one level up from the Foo directory location. Now invoke

        isatool make Foo

to run the Foo session, with browser information and document preparation enabled. Unless any errors are reported by Isabelle or L^{A}TEX, the output will appear inside the directory ISABELLE_BROWSER_INFO, as reported by the batch job in verbose mode.

You may also consider to tune the usedir options in IsaMakefile, for example to change the output format from pdf to dvi, or activate the -D option to retain a second copy of the generated L^{A}TEX sources.

See The Isabelle System Manual [18] for further details on Isabelle logic sessions and theory presentation. The Isabelle/HOL tutorial [8] also covers theory presentation issues.

1.3.2 How to write Isar proofs anyway?

This is one of the key questions, of course. First of all, the tactic script emulation of Isabelle/Isar essentially provides a clarified version of the very same unstructured proof style of classic Isabelle. Old-time users should quickly become acquainted with that (slightly degenerative) view of Isar.

Writing proper Isar proof texts targeted at human readers is quite different, though. Experienced users of the unstructured style may even have to unlearn some of their habits to master proof composition in Isar. In contrast, new users with less experience in old-style tactical proving, but a good understanding of mathematical proof in general, often get started easier.

The present text really is only a reference manual on Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to give some clues of how the concepts introduced here may be put into practice. Appendix A provides a quick reference card of the most common Isabelle/Isar language elements. Appendix B offers some practical hints on converting existing Isabelle theories and proof scripts to the new format (without restructuring proofs).

Further issues concerning the Isar concepts are covered in the literature [15, 19, 3, 4]. The author’s PhD thesis [17] presently provides the most complete exposition of Isar foundations, techniques, and applications. A number of example applications are distributed with Isabelle, and available via the Isabelle WWW library (e.g. http://isabelle.in.tum.de/library/). As a general rule of thumb, more recent Isabelle applications that also include a separate “document” (in PDF) are more likely to consist of proper Isabelle/Isar theories and proofs.

Syntax primitives

The rather generic framework of Isabelle/Isar syntax emerges from three main syntactic categories: commands of the top-level Isar engine (covering theory and proof elements), methods for general goal refinements (analogous to traditional “tactics”), and attributes for operations on facts (within a certain context). Here we give a reference of basic syntactic entities underlying Isabelle/Isar syntax in a bottom-up manner. Concrete theory and proof language elements will be introduced later on.

In order to get started with writing well-formed Isabelle/Isar documents, the most important aspect to be noted is the difference of inner versus outer syntax. Inner syntax is that of Isabelle types and terms of the logic, while outer syntax is that of Isabelle/Isar theory sources (including proofs). As a general rule, inner syntax entities may occur only as atomic entities within outer syntax. For example, the string "x + y" and identifier z are legal term specifications within a theory, while x + y is not.

! Old-style Isabelle theories used to fake parts of the inner syntax of types, with

rather complicated rules when quotes may be omitted. Despite the minor drawback of requiring quotes more often, the syntax of Isabelle/Isar is somewhat simpler and more robust in that respect.

Printed theory documents usually omit quotes to gain readability (this is a matter of L^{A}TEX macro setup, say via \isabellestyle, see also [18]). Experienced users of Isabelle/Isar may easily reconstruct the lost technical information, while mere readers need not care about quotes at all.

Isabelle/Isar input may contain any number of input termination characters “;” (semicolon) to separate commands explicitly. This is particularly useful in interactive shell sessions to make clear where the current command is intended to end. Otherwise, the interpreter loop will continue to issue a secondary prompt “#” until an end-of-command is clearly recognized from the input syntax, e.g. encounter of the next command keyword.

Advanced interfaces such as Proof General [1] do not require explicit semicolons, the amount of input text is determined automatically by inspecting the present content of the Emacs text buffer. In the printed presentation of Isabelle/Isar documents semicolons are omitted altogether for readability.

! Proof General requires certain syntax classification tables in order to achieve

properly synchronized interaction with the Isabelle/Isar process. These tables need to be consistent with the Isabelle version and particular logic image to be used in a running session (common object-logics may well change the outer syntax). The standard setup should work correctly with any of the “official” logic images derived from Isabelle/HOL (including HOLCF etc.). Users of alternative logics may need to tell Proof General explicitly, e.g. by giving an option -k ZF (in conjunction with -l ZF to specify the default logic image).

2.1 Lexical matters

The Isabelle/Isar outer syntax provides token classes as presented below; most of these coincide with the inner lexical syntax as presented in [10].

ident = letter quasiletter^{∗}
longident = ident(.ident)^{+}
symident = sym^{+} | \<ident>
nat = digit^{+}
var = ident | ?ident | ?ident.nat
typefree = 'ident
typevar = typefree | ?typefree | ?typefree.nat
string = " … "
verbatim = {* … *}
letter = latin | \<latin> | \<latin latin> | greek |

\<^isub> | \<^isup>

quasiletter = letter | digit | _| '
latin = a | … | z | A | … | Z
digit = 0 | … | 9
sym = ! | # | $ | % | & | * | + | - | / | : |

< | = | > | ? | @ | ^| _| | | ~

greek = \<alpha> | \<beta> | \<gamma> | \<delta> |

\<epsilon> | \<zeta> | \<eta> | \<theta> |
\<iota> | \<kappa> | \<mu> | \<nu> |
\<xi> | \<pi> | \<rho> | \<sigma> |
\<tau> | \<upsilon> | \<phi> | \<psi> |
\<omega> | \<Gamma> | \<Delta> | \<Theta> |
\<Lambda> | \<Xi> | \<Pi> | \<Sigma> |
\<Upsilon> | \<Phi> | \<Psi> | \<Omega>

The syntax of string admits any characters, including newlines; “"” (double-quote) and “\” (backslash) need to be escaped by a backslash. The body of verbatim may consist of any text not containing “*}”; this allows convenient inclusion of quotes without further escapes. The greek letters do not include \<lambda>, which is already used differently in the meta-logic.

Common mathematical symbols such as ∀ are represented in Isabelle as \<forall>. There are infinitely many legal symbols like this, although proper presentation is left to front-end tools such as L^{A}TEX or Proof General with the X-Symbol package. A list of standard Isabelle symbols that work well with these tools is given in [18, appendix A].

Comments take the form (* ... *) and may be nested, although userinterface tools may prevent this. Note that (* ... *) indicate source comments only, which are stripped after lexical analysis of the input. The Isar document syntax also provides formal comments that are considered as part of the text (see §2.2.2).

! Proof General does not handle nested comments properly; it is also unable to

keep (* / {* and *) / *} apart, despite their rather different meaning. These are inherent problems of Emacs legacy. Users should not be overly aggressive about nesting or alternating these delimiters.

2.2 Common syntax entities

Subsequently, we introduce several basic syntactic entities, such as names, terms, and theorem specifications, which have been factored out of the actual Isar language elements to be described later.

Note that some of the basic syntactic entities introduced below (e.g. name) act much like tokens rather than plain nonterminals (e.g. sort), especially for the sake of error messages. E.g. syntax elements like consts referring to name or type would really report a missing name or type rather than any of the constituent primitive tokens such as ident or string.

2.2.1 Names

Entity name usually refers to any name of types, constants, theorems etc. that are to be declared or defined (so qualified identifiers are excluded here). Quoted strings provide an escape for non-identifier names or those ruled out by outer syntax keywords (e.g. "let"). Already existing objects are usually referenced by nameref .

name

[figure: ident; symident; string; nat]

parname

[figure: (; name; )]

nameref

[figure: name; longident]

int

[figure: nat; -; nat]

2.2.2 Comments

Large chunks of plain text are usually given verbatim, i.e. enclosed in {* … *}. For convenience, any of the smaller text units conforming to nameref are admitted as well. A marginal comment is of the form -- text. Any number of these may occur within Isabelle/Isar commands.

text

[figure: verbatim; nameref]

comment

[figure: --; text]

2.2.3 Type classes, sorts and arities

Classes are specified by plain names. Sorts have a very simple inner syntax, which is either a single class name c or a list {c_{1}, …, c_{n}} referring to the intersection of these classes. The syntax of type arities is given directly at the outer level.

classdecl

[figure: name; <; ⊆; nameref; ,]

sort [figure: nameref]

arity

[figure: (; sort; ,; ); sort]

2.2.4 Types and terms

The actual inner Isabelle syntax, that of types and terms of the logic, is far too sophisticated in order to be modelled explicitly at the outer theory level. Basically, any such entity has to be quoted to turn it into a single token (the parsing and type-checking is performed internally later). For convenience, a slightly more liberal convention is adopted: quotes may be omitted for any type or term that is already atomic at the outer level. For example, one may just write x instead of "x". Note that symbolic identifiers (e.g. ++ or ∀) are available as well, provided these have not been superseded by commands or other keywords already (e.g. = or +).

type

[figure: nameref; typefree; typevar]

term

[figure: nameref; var]

prop [figure: term]

Positional instantiations are indicated by giving a sequence of terms, or the placeholder “ ” (underscore), which means to skip a position.

inst

[figure: term]

insts [figure: inst]

Type declarations and definitions usually refer to typespec on the left-hand side. This models basic type constructor application at the outer syntax level. Note that only plain postfix notation is available here, but no infixes.

typespec

[figure: typefree; (; typefree; ,; ); name]

2.2.5 Mixfix annotations

Mixfix annotations specify concrete inner syntax of Isabelle types and terms. Some commands such as types (see §3.1.4) admit infixes only, while consts (see §3.1.5) and syntax (see §3.1.6) support the full range of general mixfixes and binders.

infix

    [figure: (; infix; infixl; infixr; string; nat; )]

mixfix

[figure: infix; (; string; prios; nat; ); (; binder; string; prios; nat; )]

structmixfix

     [figure: mixfix; (; structure; )]

prios

    [figure: [; nat; ,; ]]

Here the string specifications refer to the actual mixfix template (see also [10]), which may include literal text, spacing, blocks, and arguments (denoted by “ ”); the special symbol \<index> (printed as “ı”) represents an index argument that specifies an implicit structure reference (see also §4.1.2). Infix and binder declarations provide common abbreviations for particular mixfix declarations. So in practice, mixfix templates mostly degenerate to literal text for concrete syntax, such as “++” for an infix symbol, or “++ı” for an infix of an implicit structure.

2.2.6 Proof methods

Proof methods are either basic ones, or expressions composed of methods via “,” (sequential composition), “|” (alternative choices), “?” (try), “+”

(repeat at least once). In practice, proof methods are usually just a comma separated list of nameref args specifications. Note that parentheses may be dropped for single method specifications (with no arguments).

method

[figure: nameref; (; methods; ); ?; +]

methods

[figure: nameref; args; method; ,; |]

Proper use of Isar proof methods does not involve goal addressing. Nevertheless, specifying goal ranges may occasionally come in handy in emulating tactic scripts. Note that [n−] refers to all goals, starting from n. All goals may be specified by [!], which is the same as [1−].

goalspec

[figure: [; nat; -; nat; nat; -; nat; !; ]]

2.2.7 Attributes and theorems

Attributes (and proof methods, see §2.2.6) have their own “semi-inner” syntax, in the sense that input conforming to args below is parsed by the attribute a second time. The attribute argument specifications may be any sequence of atomic entities (identifiers, strings etc.), or properly bracketed argument lists. Below atom refers to any atomic entity, including any keyword conforming to symident.

atom

[figure: nameref; typefree; typevar; var; nat; keyword]

arg

[figure: atom; (; args; ); [; args; ]]

args [figure: arg]

attributes

[figure: [; nameref; args; ,; ]]

Theorem specifications come in several flavors: axmdecl and thmdecl usually refer to axioms, assumptions or results of goal statements, while thmdef collects lists of existing theorems. Existing theorems are given by thmref and thmrefs, the former requires an actual singleton result. An optional index selection specifies the individual theorems to be picked out of a given fact list. Any kind of theorem specification may include lists of attributes both on the left and right hand sides; attributes are applied to any immediately preceding fact. If names are omitted, the theorems are not stored within the theorem database of the theory or proof context, but any given attributes are applied nonetheless.

CHAPTER 2. SYNTAX PRIMITIVES 16

axmdecl

[figure: name; attributes; :]

thmdecl

[figure: thmbind; :]

thmdef

[figure: thmbind; =]

thmref

[figure: nameref; selection; attributes]

thmrefs

[figure: thmref]

thmbind

[figure: name; attributes; name; attributes]

selection

[figure: (; nat; nat; -; nat; ,; )]

2.2.8 Term patterns and declarations

Wherever explicit propositions (or term fragments) occur in a proof text, casual binding of schematic term variables may be given specified via patterns of the form “(is p_{1} … is p_{n})”. There are separate versions available for terms and props. The latter provides a concl part with patterns referring the (atomic) conclusion of a rule.

termpat

    [figure: (; is; term; )]

proppat

    [figure: (; is; prop; concl; is; prop; is; prop; concl; is; prop; )]

Declarations of local variables x :: τ and logical propositions a : φ represent different views on the same principle of introducing a local scope. In practice, one may usually omit the typing of vars (due to type-inference), and the naming of propositions (due to implicit references of current facts). In any case, Isar proof elements usually admit to introduce multiple such items simultaneously.

vars

[figure: name; ::; type]

props

[figure: thmdecl; prop; proppat]

The treatment of multiple declarations corresponds to the complementary focus of vars versus props: in “x_{1} … x_{n} :: τ” the typing refers to all variables, while in a: φ_{1} … φ_{n} the naming refers to all propositions collectively. Isar language elements that refer to vars or props typically admit separate typings or namings via another level of iteration, with explicit and separators; e.g. see fix and assume in §3.2.2.

2.2.9 Antiquotations

thm : antiquotation
prop : antiquotation
term : antiquotation
const : antiquotation
typeof : antiquotation
typ : antiquotation
thm style : antiquotation
term style : antiquotation
text : antiquotation
goals : antiquotation
subgoals : antiquotation
prf : antiquotation
full prf : antiquotation
ML : antiquotation

The text body of formal comments (see also §2.2.2) may contain antiquotations of logical entities, such as theorems, terms and types, which are to be presented in the final output produced by the Isabelle document preparation system (see also §1.3.1).

   Thus embedding of “@{term [show_types] "f(x) = a + x"}” within a

text block would cause (f::'a ⇒ 'a) (x::'a) = (a::'a) + x to appear in the final L^{A}TEX document. Also note that theorem antiquotations may involve attributes as well. For example, @{thm sym [no_vars]} would print the statement where all schematic variables have been replaced by fixed ones, which are easier to read.

     @

[figure]

         {

[figure]

                            }

antiquotation

[figure]

CHAPTER 2. SYNTAX PRIMITIVES 19

antiquotation

[figure: thm; options; thmrefs; prop; options; prop; term; options; term; const; options; term; typeof; options; term; typ; options; type; thm style; options; name; thmref; term style; options; name; term; text; options; name; goals; options; subgoals; options; prf; options; thmrefs; full prf; options; thmrefs; ML; options; name]

options

[figure: [; option; ,; ]]

option

[figure: name; name; =; name]

Note that the syntax of antiquotations may not include source comments (* ... *) or verbatim text {* … *}.

@\{thm \overline{a}\} prints theorems \overline{a}. Note that attribute specifications may be included as well (see also §2.2.7); the no vars operation (see §4.3.1) would

be particularly useful to suppress printing of schematic variables.

@{prop φ} prints a well-typed proposition φ.

@{term t} prints a well-typed term t.

@{const c} prints a well-defined constant c.

@{typeof t} prints the type of a well-typed term t.

@{typ τ} prints a well-formed type τ.

@{thm style s a} prints theorem a, previously applying a style s to it (see below).

@{term style s t} prints a well-typed term t after applying a style s to it (see below).

@{text s} prints uninterpreted source text s. This is particularly useful to print portions of text according to the Isabelle L^{A}TEX output style, without demanding well-formedness (e.g. small pieces of terms that should not be parsed or type-checked yet).

@{goals} prints the current dynamic goal state. This is mainly for support of tactic-emulation scripts within Isar — presentation of goal states does not conform to actual human-readable proof documents. Please do not include goal states into document output unless you really know what you are doing!

@{subgoals} is similar to goals, but does not print the main goal.

@\{prf \overline{a}\} prints the (compact) proof terms corresponding to the theorems \overline{a}. Note that this requires proof terms to be switched on for the current object logic (see the “Proof terms” section of the Isabelle reference manual for information on how to do this).

@\{full prf \overline{a}\} is like @\{prf \overline{a}\}, but displays the full proof terms, i.e. also displays information omitted in the compact proof term, which is denoted by “ ” placeholders there.

@{ML s} checks text s as an ML expression in the current runtime environment, and displays the source verbatim.

The following standard styles for use with thm style and term style are available: lhs extracts the first argument of any application form with at least two

arguments – typically meta-level or object-level equality, or any other binary relation.

rhs is like lhs, but extracts the second argument.

concl extracts the conclusion C from a nested meta-level implication A_{1} ⟹ ⋯ A_{n} ⟹ C .

prem1, …, prem9 extract premise number 1, …, 9, respectively, from a nested meta-level implication A_{1} ⟹ ⋯ A_{n} ⟹ C .

The following options are available to tune the output. Note that most of these coincide with ML flags of the same names (see also [10]).

show types = bool and show sorts = bool control printing of explicit type and sort constraints.

show structs = bool controls printing of implicit structures.

long names = bool forces names of types and constants etc. to be printed in their fully qualified internal form.

short names = bool forces names of types and constants etc. to be printed unqualified. Note that internalizing the output again in the current context may well yield a different result.

unique names = bool determines whether the printed version of qualified names should be made sufficiently long to avoid overlap with names declared further back. Set to false for more concise output.

eta contract = bool prints terms in η-contracted form.

display = bool indicates if the text is to be output as multi-line “display material”, rather than a small piece of text without line breaks (which is the default).

breaks = bool controls line breaks in non-display material.

quotes = bool indicates if the output should be enclosed in double quotes.

mode = name adds name to the print mode to be used for presentation (see also [10]). Note that the standard setup for L^{A}TEX output is already present by default, including the modes “latex”, “xsymbols”, “symbols”. margin = nat and indent = nat change the margin or indentation for pretty

printing of display material.

source = bool prints the source text of the antiquotation arguments, rather than the actual value. Note that this does not affect well-formedness checks of thm, term, etc. (only the text antiquotation admits arbitrary output).

goals limit = nat determines the maximum number of goals to be printed.

locale = name specifies an alternative context used for evaluating and printing the subsequent argument.

For boolean flags, “name = true” may be abbreviated as “name”. All of the above flags are disabled by default, unless changed from ML.

Note that antiquotations do not only spare the author from tedious typing of logical entities, but also achieve some degree of consistency-checking of informal explanations with formal developments: well-formedness of terms and types with respect to the current theory or proof context is ensured here.

2.2.10 Tagged commands

Each Isabelle/Isar command may be decorated by presentation tags:

tags [figure: tag]

tag

[figure: %; ident; string]

The tags theory, proof , ML are already pre-declared for certain classes of commands:

theory theory begin and end
proof all proof commands
ML  all commands involving ML code

The Isabelle document preparation system (see also [18]) allows tagged command regions to be presented specifically, e.g. to fold proof texts, or drop parts of the text completely.

For example “by %invisible (auto)” would cause that piece of proof to be treated as invisible instead of proof (the default), which may be either show or hidden depending on the document setup. In contrast, “by %visible (auto)” would force this text to be shown invariably.

Explicit tag specifications within a proof apply to all subsequent commands of the same level of nesting. For example, “proof %visible … qed” would force the whole sub-proof to be typeset as visible (unless some of its parts are tagged differently).

Basic language elements

Subsequently, we introduce the main part of Pure theory and proof commands, together with fundamental proof methods and attributes. Chapter 4 describes further Isar elements provided by generic tools and packages (such as the Simplifier) that are either part of Pure Isabelle or pre-installed in most object logics. Chapter 5 refers to object-logic specific elements (mainly for HOL and ZF).

Isar commands may be either proper document constructors, or improper commands. Some proof methods and attributes introduced later are classified as improper as well. Improper Isar language elements, which are subsequently marked by “^{∗}”, are often helpful when developing proof documents, while their use is discouraged for the final human-readable outcome. Typical examples are diagnostic commands that print terms or theorems according to the current context; other commands emulate old-style tactical theorem proving.

3.1 Theory commands

3.1.1 Defining theories

header : toplevel → toplevel
theory : toplevel → theory
context^{∗} : toplevel → theory
end : theory → toplevel

Isabelle/Isar “new-style” theories are either defined via theory files or interactively. Both theory-level specifications and proofs are handled uniformly — occasionally definitional mechanisms even require some explicit proof as well. In contrast, “old-style” Isabelle theories support batch processing only, with the proof scripts collected in separate ML files.

The first “real” command of any theory has to be theory, which starts a new theory based on the merge of existing ones. Just preceding theory, there may be an optional header declaration, which is relevant to document preparation only; it acts very much like a special pre-theory markup command (cf. §3.1.2 and §3.1.2). The end command concludes a theory development; it has to be the very last command of any theory file loaded in batch-mode. The theory context may be also changed interactively by context without creating a new theory.

[figure: header; text]

[figure: theory; name; imports; name; uses; begin]
[figure: context; name]

uses

[figure: uses; name; parname]

header text provides plain text markup just preceding the formal beginning of a theory. In actual document preparation the corresponding L^{A}TEX macro \isamarkupheader may be redefined to produce chapter or section headings. See also §3.1.2 and §3.2.1 for further markup commands.

theory A imports B_{1} … B_{n} begin starts a new theory A based on the merge of existing theories B_{1}, …, B_{n}.

Due to inclusion of several ancestors, the overall theory structure emerging in an Isabelle session forms a directed acyclic graph (DAG). Isabelle’s theory loader ensures that the sources contributing to the development graph are always up-to-date. Changed files are automatically reloaded when processing theory headers interactively; batchmode explicitly distinguishes update_thy from use_thy, see also [10].

The optional uses specification declares additional dependencies on ML files. Files will be loaded immediately, unless the name is put in parentheses, which merely documents the dependency to be resolved later in the text (typically via explicit use in the body text, see §3.1.9). In reminiscence of the old-style theory system of Isabelle, A.thy may be also accompanied by an additional file A.ML consisting of ML code that is executed in the context of the finished theory A. That file should not be included in the files dependency declaration, though.

context B enters an existing theory context, basically in read-only mode, so only a limited set of commands may be performed without destroying the theory. Just as for theory, the theory loader ensures that B is loaded and up-to-date.

This command is occasionally useful for quick interactive experiments; normally one should always commence a new context via theory.

end concludes the current theory definition or context switch. Note that this command cannot be undone, but the whole theory definition has to be retracted.

3.1.2 Markup commands

chapter : theory → theory
section : theory → theory
subsection : theory → theory
subsubsection : theory → theory
text : theory → theory
text raw : theory → theory

Apart from formal comments (see §2.2.2), markup commands provide a structured way to insert text into the document generated from a theory (see [18] for more information on Isabelle’s document preparation tools).

[figure: chapter; section; subsection; subsubsection; text; locale; text]
[figure: text raw; text]

chapter, section, subsection, and subsubsection mark chapter and section headings. text specifies paragraphs of plain text.

text raw inserts L^{A}TEX source into the output, without additional markup. Thus the full range of document manipulations becomes available.

The text argument of these markup commands (except for text raw) may contain references to formal entities (“antiquotations”, see also §2.2.9). These are interpreted in the present theory context, or the specified locale.

Any of these markup elements corresponds to a L^{A}TEX command with the name prefixed by \isamarkup. For the sectioning commands this is a plain macro with a single argument, e.g. \isamarkupchapter{… } for chapter. The text markup results in a L^{A}TEX environment \begin{isamarkuptext} … \end{isamarkuptext}, while text raw causes the text to be inserted directly into the L^{A}TEX source.

Additional markup commands are available for proofs (see §3.2.1). Also note that the header declaration (see §3.1.1) admits to insert section markup just preceding the actual theory definition.

3.1.3 Type classes and sorts

classes : theory → theory
classrel : theory → theory (axiomatic!)
defaultsort : theory → theory

[figure: classes; classdecl]

[figure: classrel; nameref; <; ⊆; nameref; and]

    [figure: defaultsort; sort]

classes c ⊆ \overline{c} declares class c to be a subclass of existing classes \overline{c}. Cyclic class structures are ruled out.

classrel c_{1} ⊆ c_{2} states subclass relations between existing classes c_{1} and c_{2}. This is done axiomatically! The instance command (see §4.1.1) provides a way to introduce proven class relations. defaultsort s makes sort s the new default sort for any type variables

given without sort constraints. Usually, the default sort would be only changed when defining a new object-logic.

3.1.4 Primitive types and type abbreviations

types : theory → theory
typedecl : theory → theory
nonterminals : theory → theory
arities : theory → theory (axiomatic!)

[figure: types; typespec; =; type; infix]

[figure: typedecl; typespec; infix]

[figure: nonterminals; name]

[figure: arities; nameref; ::; arity]

types (\overline{α})t = τ introduces type synonym (\overline{α})t for existing type τ. Unlike actual type definitions, as are available in Isabelle/HOL for example, type synonyms are just purely syntactic abbreviations without any logical significance. Internally, type synonyms are fully expanded.

typedecl (\overline{α})t declares a new type constructor t, intended as an actual logical type. Note that the Isabelle/HOL object-logic overrides typedecl by its own version (§5.2.1).

nonterminals \overline{c} declares 0-ary type constructors \overline{c} to act as purely syntactic types, i.e. nonterminal symbols of Isabelle’s inner syntax of terms or types. arities t :: (\overline{s})s augments Isabelle’s order-sorted signature of types by new

type constructor arities. This is done axiomatically! The instance command (see §4.1.1) provides a way to introduce proven type arities.

3.1.5 Constants and simple definitions

consts : theory → theory
defs : theory → theory
constdefs : theory → theory

[figure: consts; name; ::; type; mixfix]

structs constdecl constdef

[figure: defs; (; overloaded; ); axmdecl; prop]

[figure: constdefs; structs; constdecl; constdef]

[figure: (; structure; vars; and; )]

[figure: name; ::; type; mixfix; name; ::; type; name; where; mixfix]

[figure: thmdecl; prop]

consts c :: σ declares constant c to have any instance of type scheme σ. The optional mixfix annotations may attach concrete syntax to the constants declared.

defs name : eqn introduces eqn as a definitional axiom for some existing constant. See [10, §6] for more details on the form of equations admitted as constant definitions. The (overloaded) option declares definitions to be potentially overloaded. Unless this option is given, a warning message would be issued for any definitional equation with a more special type than that of the corresponding constant declaration.

constdefs provides a streamlined combination of constants declarations and definitions: type-inference takes care of the most general typing of the given specification (the optional type constraint may refer to typeinference dummies “ ” as usual). The resulting type declaration needs to agree with that of the specification; overloading is not supported here! The constant name may be omitted altogether, if neither type nor syntax declarations are given. The canonical name of the definitional axiom for constant c will be c def , unless specified otherwise. Also note that the given list of specifications is processed in a strictly sequential manner, with type-checking being performed independently. An optional initial context of (structure) declarations admits use of indexed syntax, using the special symbol \<index> (printed as “ı”). The latter concept is particularly useful with locales (see also §4.1.2).

3.1.6 Syntax and translations

syntax : theory → theory
no syntax : theory → theory
translations : theory → theory

[figure: syntax; no syntax; mode; constdecl]

[figure: translations; transpat; ==; =>; <=; ⇀ ↽; ⇀; ↽; transpat]

mode

[figure: (; name; output; name; output; )]

transpat

[figure: (; nameref; ); string]

syntax (mode) decls is similar to consts decls, except that the actual logical signature extension is omitted. Thus the context free grammar of Isabelle’s inner syntax may be augmented in arbitrary ways, independently of the logic. The mode argument refers to the print mode that the grammar rules belong; unless the output indicator is given, all productions are added both to the input and output grammar.

no syntax (mode) decls removes grammar declarations (and translations) resulting from decls, which are interpreted in the same manner as for syntax above.

translations rules specifies syntactic translation rules (i.e. macros): parse / print rules (⇀ ↽), parse rules (⇀), or print rules (↽). Translation patterns may be prefixed by the syntactic category to be used for parsing; the default is logic.

3.1.7 Axioms and theorems

axioms : theory → theory (axiomatic!)
lemmas : theory → theory
theorems : theory → theory

[figure: axioms; axmdecl; prop]

[figure: lemmas; theorems; locale; thmdef; thmrefs; and]

axioms a : φ introduces arbitrary statements as axioms of the meta-logic. In fact, axioms are “axiomatic theorems”, and may be referred later just as any other theorem.

Axioms are usually only introduced when declaring new logical systems. Everyday work is typically done the hard way, with proper definitions and proven theorems.

lemmas a = \overline{b} retrieves and stores existing facts in the theory context, or the specified locale (see also §4.1.2). Typical applications would also involve attributes, to declare Simplifier rules, for example.

theorems is essentially the same as lemmas, but marks the result as a different kind of facts.

3.1.8 Name spaces

global : theory → theory
local : theory → theory
hide : theory → theory

[figure: hide; (; open; ); name; nameref]

Isabelle organizes any kind of name declarations (of types, constants, theorems etc.) by separate hierarchically structured name spaces. Normally the user does not have to control the behavior of name spaces by hand, yet the following commands provide some way to do so.

global and local change the current name declaration mode. Initially, theories start in local mode, causing all names to be automatically qualified by the theory name. Changing this to global causes all names to be declared without the theory prefix, until local is declared again.

Note that global names are prone to get hidden accidently later, when qualified names of the same base name are introduced.

hide space names fully removes declarations from a given name space (which may be class, type, or const); with the (open) option, only the base name is hidden. Global (unqualified) names may never be hidden.

Note that hiding name space accesses has no impact on logical declarations – they remain valid internally. Entities that are no longer accessible to the user are printed with the special qualifier “??” prefixed to the full internal name.

3.1.9 Incorporating ML code

use : · → ·
ML : · → ·
ML command : · → ·
ML setup : theory → theory
setup : theory → theory
method setup : theory → theory

[figure: use; name]

[figure: ML; ML command; ML setup; setup; text] [figure: method setup; name; =; text; text]

use file reads and executes ML commands from file. The current theory context (if present) is passed down to the ML session, but may not be modified. Furthermore, the file name is checked with the files dependency declaration given in the theory header (see also §3.1.1).

ML text and ML command text execute ML commands from text. The theory context is passed in the same way as for use, but may not be changed. Note that the output of ML command is less verbose than plain ML.

ML setup text executes ML commands from text. The theory context is passed down to the ML session, and fetched back afterwards. Thus text may actually change the theory as a side effect.

setup text changes the current theory context by applying text, which refers to an ML expression of type (theory -> theory) list. The setup command is the canonical way to initialize any object-logic specific tools and packages written in ML.

method setup name = text description defines a proof method in the current theory. The given text has to be an ML expression of type

Args.src -> Proof.context -> Proof.method. Parsing concrete

method syntax from Args.src input can be quite tedious in general. The following simple examples are for methods without any explicit arguments, or a list of theorems, respectively.

 Method.no_args (Method.METHOD (fn facts => foobar_tac))
 Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
 Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
 Method.thms_ctxt_args (fn thms => fn ctxt =>
    Method.METHOD (fn facts => foobar_tac))

Note that mere tactic emulations may ignore the facts parameter above. Proper proof methods would do something appropriate with the list of current facts, though. Single-rule methods usually do strict forward-chaining (e.g. by using Method.multi_resolves), while automatic ones just insert the facts using Method.insert_tac before applying the main tactic.

3.1.10 Syntax translation functions

parse ast translation : theory → theory
parse translation : theory → theory
print translation : theory → theory
typed print translation : theory → theory
print ast translation : theory → theory
token translation : theory → theory

     [figure: parse ast translation; parse translation; print translation; typed print translation; print ast translation; (; advanced; ); text]
    [figure: token translation; text]

Syntax translation functions written in ML admit almost arbitrary manipulations of Isabelle’s inner syntax. Any of the above commands have a single text argument that refers to an ML expression of appropriate type, which are as follows by default:

      val parse_ast_translation   : (string * (ast list -> ast)) list
      val parse_translation       : (string * (term list -> term)) list
      val print_translation       : (string * (term list -> term)) list
      val typed_print_translation :
        (string * (bool -> typ -> term list -> term)) list
      val print_ast_translation   : (string * (ast list -> ast)) list
      val token_translation       :
        (string * string * (string -> string * real)) list

In case that the (advanced) option is given, the corresponding translation functions may depend on the signature of the current theory context. This allows to implement advanced syntax mechanisms, as translations functions may refer to specific theory declarations and auxiliary data.

See also [10, §8] for more information on the general concept of syntax transformations in Isabelle.

      val parse_ast_translation:
        (string * (Sign.sg -> ast list -> ast)) list
      val parse_translation:
        (string * (Sign.sg -> term list -> term)) list
      val print_translation:
        (string * (Sign.sg -> term list -> term)) list
      val typed_print_translation:
        (string * (Sign.sg -> bool -> typ -> term list -> term)) list
      val print_ast_translation:
        (string * (Sign.sg -> ast list -> ast)) list

3.1.11 Oracles

oracle : theory → theory

The oracle interface promotes a given ML function theory -> T -> term to theory -> T -> thm, for some type T given by the user. This acts like an infinitary specification of axioms – there is no internal check of the correctness of the results! The inference kernel records oracle invocations within the internal derivation object of theorems, and the pretty printer attaches “[!]” to indicate results that are not fully checked by Isabelle inferences.

[figure: oracle; name; (; type; ); =; text]

oracle name (type) = text turns the given ML expression text of type theory -> type -> term into an ML function name of type

     theory -> type -> thm.

3.2 Proof commands

Proof commands perform transitions of Isar/VM machine configurations, which are block-structured, consisting of a stack of nodes with three main components: logical proof context, current facts, and open goals. Isar/VM transitions are typed according to the following three different modes of operation:

proof (prove) means that a new goal has just been stated that is now to be proven; the next command may refine it by some proof method, and enter a sub-proof to establish the actual result.

proof (state) is like a nested theory mode: the context may be augmented by stating additional assumptions, intermediate results etc. proof (chain) is intermediate between proof (state) and proof (prove): exist-

ing facts (i.e. the contents of the special “this” register) have been just picked up in order to be used when refining the goal claimed next.

The proof mode indicator may be read as a verb telling the writer what kind of operation may be performed next. The corresponding typings of proof commands restricts the shape of well-formed proof texts to particular command sequences. So dynamic arrangements of commands eventually turn out as static texts of a certain structure. Appendix A gives a simplified grammar of the overall (extensible) language emerging that way.

3.2.1 Markup commands

sect : proof → proof
subsect : proof → proof
subsubsect : proof → proof
txt : proof → proof
txt raw : proof → proof

These markup commands for proof mode closely correspond to the ones of theory mode (see §3.1.2).

     [figure: sect; subsect; subsubsect; txt; txt raw; text]

3.2.2 Context elements

fix : proof (state) → proof (state)
assume : proof (state) → proof (state)
presume : proof (state) → proof (state)
def : proof (state) → proof (state)

The logical proof context consists of fixed variables and assumptions. The former closely correspond to Skolem constants, or meta-level universal quantification as provided by the Isabelle/Pure logical framework. Introducing some arbitrary, but fixed variable via “fix x” results in a local value that may be used in the subsequent proof as any other variable or constant. Furthermore, any result ⊢ φ[x] exported from the context will be universally closed wrt. x at the outermost level: ⊢ ⋀ x . φ (this is expressed using Isabelle’s meta-variables).

Similarly, introducing some assumption χ has two effects. On the one hand, a local theorem is created that may be used as a fact in subsequent proof steps. On the other hand, any result χ ⊢ φ exported from the context becomes conditional wrt. the assumption: ⊢ χ ⟹ φ. Thus, solving an enclosing goal using such a result would basically introduce a new subgoal stemming from the assumption. How this situation is handled depends on the actual version of assumption command used: while assume insists on solving the subgoal by unification with some premise of the goal, presume leaves the subgoal unchanged in order to be proved later by the user.

Local definitions, introduced by “def x ≡ t”, are achieved by combining “fix x” with another version of assumption that causes any hypothetical equation x ≡ t to be eliminated by the reflexivity rule. Thus, exporting some result x ≡ t ⊢ φ[x] yields ⊢ φ[t].

    [figure: fix; vars; and]

     [figure: assume; presume; props; and]

[figure: def; thmdecl; name; ==; ≡; term; termpat]

fix \overline{x} introduces local arbitrary, but fixed variables \overline{x}.

assume a: \overline{φ} and presume a: \overline{φ} introduce local theorems \overline{φ} by assumption. Subsequent results applied to an enclosing goal (e.g. by show) are handled as follows: assume expects to be able to unify with existing premises in the goal, while presume leaves \overline{φ} as new subgoals.

Several lists of assumptions may be given (separated by and); the resulting list of current facts consists of all of these concatenated.

def a: x ≡ t introduces a local (non-polymorphic) definition. In results exported from the context, x is replaced by t. Basically, “def x ≡ t” abbreviates “fix x assume x ≡ t”, with the resulting hypothetical equation solved by reflexivity.

The default name for the definitional equation is x def .

The special name prems refers to all assumptions of the current context as a list of theorems.

3.2.3 Facts and forward chaining

note : proof (state) → proof (state)
then : proof (state) → proof (chain)
from : proof (state) → proof (chain)
with : proof (state) → proof (chain)
using : proof (prove) → proof (prove)

New facts are established either by assumption or proof of local statements. Any fact will usually be involved in further proofs, either as explicit arguments of proof methods, or when forward chaining towards the next goal via then (and variants); from and with are composite forms involving note. The using elements augments the collection of used facts after a goal has been stated. Note that the special theorem name this refers to the most recently established facts, but only before issuing a follow-up claim.

[figure: note; thmdef; thmrefs; and]

     [figure: from; with; using; thmrefs; and]

note a = \overline{b} recalls existing facts \overline{b}, binding the result as a. Note that attributes may be involved as well, both on the left and right hand sides. then indicates forward chaining by the current facts in order to establish

the goal to be claimed next. The initial proof method invoked to refine that will be offered the facts to do “anything appropriate” (see also §3.2.5). For example, method rule (see §3.2.6) would typically do an elimination rather than an introduction. Automatic methods usually insert the facts into the goal state before operation. This provides a simple scheme to control relevance of facts in automated proof search.

from \overline{b} abbreviates “note \overline{b} then”; thus then is equivalent to “from this”.

with \overline{b} abbreviates “from \overline{b} and this”; thus the forward chaining is from earlier facts together with the current ones.

using \overline{b} augments the facts being currently indicated for use by a subsequent refinement step (such as apply or proof).

Forward chaining with an empty list of theorems is the same as not chaining at all. Thus “from nothing” has no effect apart from entering prove(chain) mode, since nothing is bound to the empty list of theorems.

Basic proof methods (such as rule) expect multiple facts to be given in their proper order, corresponding to a prefix of the premises of the rule involved. Note that positions may be easily skipped using something like from _a b, for example. This involves the trivial rule PROP ψ ⟹ PROP ψ, which happens to be bound in Isabelle/Pure as “_” (underscore).

Automated methods (such as simp or auto) just insert any given facts before their usual operation. Depending on the kind of procedure involved, the order of facts is less significant here.

3.2.4 Goal statements

lemma : theory → proof (prove)
theorem : theory → proof (prove)
corollary : theory → proof (prove)
have : proof (state) | proof (chain) → proof (prove)
show : proof (state) | proof (chain) → proof (prove)
hence : proof (state) → proof (prove)
thus : proof (state) → proof (prove)

From a theory context, proof mode is entered by an initial goal command such as lemma, theorem, or corollary. Within a proof, new claims may be introduced locally as well; four variants are available here to indicate whether forward chaining of facts should be performed initially (via then), and whether the final result is meant to solve some pending goal.

Goals may consist of multiple statements, resulting in a list of facts eventually. A pending multi-goal is internally represented as a meta-level conjunction (printed as &&), which is usually split into the corresponding number of sub-goals prior to an initial method application, via proof (§3.2.5) or apply (§3.2.9). The induct method covered in §4.3.5 acts on multiple claims simultaneously.

Claims at the theory level may be either in short or long form. A short goal merely consists of several simultaneous propositions (often just one). A long goal includes an explicit context specification for the subsequent conclusions, involving local parameters; here the role of each part of the statement is explicitly marked by separate keywords (see also §4.1.2).

     [figure: lemma; theorem; corollary; locale; goal; longgoal]

     [figure: have; show; hence; thus; goal]

goal

[figure: props; and]

longgoal

[figure: thmdecl; contextelem; shows; goal]

lemma a: \overline{φ} enters proof mode with \overline{φ} as main goal, eventually resulting in some fact ⊢ \overline{φ} to be put back into the theory context, or into the specified locale (cf. §4.1.2). An additional context specification may build up an initial proof context for the subsequent claim; this includes local definitions and syntax as well, see the definition of contextelem in §4.1.2. theorem a: \overline{φ} and corollary a: \overline{φ} are essentially the same as lemma a: \overline{φ},

but the facts are internally marked as being of a different kind. This discrimination acts like a formal comment.

have a: \overline{φ} claims a local goal, eventually resulting in a fact within the current logical context. This operation is completely independent of any pending sub-goals of an enclosing goal statements, so have may be freely used for experimental exploration of potential results within a proof body.

show a: \overline{φ} is like have a: \overline{φ} plus a second stage to refine some pending sub-goal for each one of the finished result, after having been exported into the corresponding context (at the head of the sub-proof of this show command). To accommodate interactive debugging, resulting rules are printed before being applied internally. Even more, interactive execution of show predicts potential failure and displays the resulting error as a warning beforehand. Watch out for the following message:

       Problem! Local statement will fail to solve any pending goal

hence abbreviates “then have”, i.e. claims a local goal to be proven by forward chaining the current facts. Note that hence is also equivalent to “from this have”.

thus abbreviates “then show”. Note that thus is also equivalent to “from this show”.

Any goal statement causes some term abbreviations (such as ?thesis) to be bound automatically, see also §3.2.7. Furthermore, the local context of a (non-atomic) goal is provided via the rule context case.

! Isabelle/Isar suffers theory-level goal statements to contain unbound schematic

variables, although this does not conform to the aim of human-readable proof documents! The main problem with schematic goals is that the actual outcome is usually hard to predict, depending on the behavior of the proof methods applied during the course of reasoning. Note that most semi-automated methods heavily depend on several kinds of implicit rule declarations within the current theory context. As this would also result in non-compositional checking of sub-proofs, local goals are not allowed to be schematic at all. Nevertheless, schematic goals do have their use in Prolog-style interactive synthesis of proven results, usually by stepwise refinement via emulation of traditional Isabelle tactic scripts (see also §3.2.9). In any case, users should know what they are doing.

3.2.5 Initial and terminal proof steps

proof : proof (prove) → proof (state)
qed : proof (state) → proof (state) | theory
by : proof (prove) → proof (state) | theory
. . : proof (prove) → proof (state) | theory
. : proof (prove) → proof (state) | theory
sorry : proof (prove) → proof (state) | theory

Arbitrary goal refinement via tactics is considered harmful. Properly, the Isar framework admits proof methods to be invoked in two places only.

1. An initial refinement step proof m_{1} reduces a newly stated goal to a number of sub-goals that are to be solved later. Facts are passed to m_{1} for forward chaining, if so indicated by proof (chain) mode.

2. A terminal conclusion step qed m_{2} is intended to solve remaining goals. No facts are passed to m_{2}.

The only other (proper) way to affect pending goals in a proof body is by show, which involves an explicit statement of what is to be solved eventually. Thus we avoid the fundamental problem of unstructured tactic scripts that consist of numerous consecutive goal transformations, with invisible effects.

As a general rule of thumb for good proof style, initial proof methods should either solve the goal completely, or constitute some well-understood reduction to new sub-goals. Arbitrary automatic proof tools that are prone leave a large number of badly structured sub-goals are no help in continuing the proof document in an intelligible manner.

Unless given explicitly by the user, the default initial method is “rule”, which applies a single standard elimination or introduction rule according to the topmost symbol involved. There is no separate default terminal method. Any remaining goals are always solved by assumption in the very last step.

[figure: proof; method]

[figure: qed; method]

[figure: by; method; method]

[figure: .; ..; sorry]

proof m_{1} refines the goal by proof method m_{1}; facts for forward chaining are passed if so indicated by proof (chain) mode.

qed m_{2} refines any remaining goals by proof method m_{2} and concludes the sub-proof by assumption. If the goal had been show (or thus), some pending sub-goal is solved as well by the rule resulting from the result exported into the enclosing goal context. Thus qed may fail for two reasons: either m_{2} fails, or the resulting rule does not fit to any pending goal^{1} of the enclosing context. Debugging such a situation might involve temporarily changing show into have, or weakening the local context by replacing occurrences of assume by presume.

by m_{1} m_{2} is a terminal proof ; it abbreviates proof m_{1} qed m_{2}, but with backtracking across both methods. Debugging an unsuccessful by m_{1} m_{2} commands might be done by expanding its definition; in many cases proof m_{1} (or even apply m_{1}) is already sufficient to see the problem.

“. .” is a default proof ; it abbreviates by rule.

“.” is a trivial proof ; it abbreviates by this.

sorry is a fake proof pretending to solve the pending claim without further ado. This only works in interactive development, or if the quick_and_dirty flag is enabled. Facts emerging from fake proofs are not the real thing. Internally, each theorem container is tainted by an oracle invocation, which is indicated as “[!]” in the printed result.

The most important application of sorry is to support experimentation and top-down proof development.

1This includes any additional “strong” assumptions as introduced by assume.

3.2.6 Fundamental methods and attributes

The following proof methods and attributes refer to basic logical operations of Isar. Further methods and attributes are provided by several generic and object-logic specific tools and packages (see chapters 4 and 5).

− : method
assumption : method
this : method
rule : method
iprover : method
intro : attribute
elim : attribute
dest : attribute
rule : attribute
OF : attribute
of : attribute
where : attribute

rulemod

[figure: rule; thmrefs]

[figure: iprover; !; rulemod]

[figure: intro; elim; dest; !; ?; nat; del; :; thmrefs]

[figure: intro; elim; dest; !; ?; nat]

[figure: rule; del]

[figure: OF; thmrefs]

[figure: of; insts; concl; :; insts]

[figure: where; name; var; typefree; typevar; =; type; term; and]

“−” does nothing but insert the forward chaining facts as premises into the goal. Note that command proof without any method actually performs a single reduction step using the rule method; thus a plain do-nothing proof step would be “proof −” rather than proof alone.

assumption solves some goal by a single assumption step. All given facts are guaranteed to participate in the refinement; this means there may be only 0 or 1 in the first place. Recall that qed (see §3.2.5) already concludes any remaining sub-goals by assumption, so structured proofs usually need not quote the assumption method at all.

this applies all of the current facts directly as rules. Recall that “.” (dot) abbreviates “by this”.

rule \overline{a} applies some rule given as argument in backward manner; facts are used to reduce the rule before applying it to the goal. Thus rule without facts is plain introduction, while with facts it becomes elimination.

When no arguments are given, the rule method tries to pick appropriate rules automatically, as declared in the current context using the intro, elim, dest attributes (see below). This is the default behavior of proof and “. .” (double-dot) steps (see §3.2.5). iprover performs intuitionistic proof search, depending on specifically de-

clared rules from the context, or given as explicit arguments. Chained facts are inserted into the goal before commencing proof search; “iprover!” means to include the current prems as well.

Rules need to be classified as intro, elim, or dest; here the “!” indicator refers to “safe” rules, which may be applied aggressively (without considering back-tracking later). Rules declared with “?” are ignored in proof search (the single-step rule method still observes these). An explicit weight annotation may be given as well; otherwise the number of rule premises will be taken into account here.

intro, elim, and dest declare introduction, elimination, and destruct rules, to be used with the rule and iprover methods. Note that the latter will ignore rules declared with “?”, while “!” are used most aggressively.

The classical reasoner (see §4.3.4) introduces its own variants of these attributes; use qualified names to access the present versions of Isabelle/Pure, i.e. Pure.intro or CPure.intro.

rule del undeclares introduction, elimination, or destruct rules.

OF \overline{a} applies some theorem to given rules \overline{a} (in parallel). This corresponds to the MRS operator in ML [10, §5], but note the reversed order. Positions may be effectively skipped by including “ ” (underscore) as argument.

of \overline{t} performs positional instantiation of term variables. The terms \overline{t} are substituted for any schematic variables occurring in a theorem from left to right; “_” (underscore) indicates to skip a position. Arguments following a “concl:” specification refer to positions of the conclusion of a rule.

where \overline{x} = \overline{t} performs named instantiation of schematic type and term variables occurring in a theorem. Schematic variables have to be specified on the left-hand side (e.g. ?x1.3). The question mark may be omitted if the variable name is a plain identifier without index. As type instantiations are inferred from term instantiations, explicit type instantiations are seldom necessary.

3.2.7 Term abbreviations

let : proof (state) → proof (state)
is : syntax

Abbreviations may be either bound by explicit let p ≡ t statements, or by annotating assumptions or goal statements with a list of patterns “(is p_{1} … is p_{n})”. In both cases, higher-order matching is invoked to bind extra-logical term variables, which may be either named schematic variables of the form ?x, or nameless dummies “_” (underscore). Note that in the let form the patterns occur on the left-hand side, while the is patterns are in postfix position.

Polymorphism of term bindings is handled in Hindley-Milner style, similar to ML. Type variables referring to local assumptions or open goal statements are fixed, while those of finished results or bound by let may occur in arbitrary instances later. Even though actual polymorphism should be rarely used in practice, this mechanism is essential to achieve proper incremental typeinference, as the user proceeds to build up the Isar proof text from left to right.

Term abbreviations are quite different from local definitions as introduced via def (see §3.2.2). The latter are visible within the logic as actual equations, while abbreviations disappear during the input process just after type checking. Also note that def does not support polymorphism.

    [figure: let; term; and; =; term; and]

The syntax of is patterns follows termpat or proppat (see §2.2.8).

let \overline{p} = \overline{t} binds any text variables in patters \overline{p} by simultaneous higher-order matching against terms \overline{t}.

(is \overline{p}) resembles let, but matches \overline{p} against the preceding statement. Also note that is is not a separate command, but part of others (such as assume, have etc.).

Some automatic term abbreviations for goals and facts are available as well. For any open goal, ?thesis refers to its object-level statement, abstracted over any meta-level parameters (if present). Likewise, ?this is bound for fact statements resulting from assumptions or finished goals. In case ?this refers to an object-logic statement that is an application f (t), then t is bound to the special text variable “…” (three dots). The canonical application of the latter are calculational proofs (see §4.2.2).

3.2.8 Block structure

next : proof (state) → proof (state)
{ : proof (state) → proof (state)
} : proof (state) → proof (state)

While Isar is inherently block-structured, opening and closing blocks is mostly handled rather casually, with little explicit user-intervention. Any local goal statement automatically opens two blocks, which are closed again when concluding the sub-proof (by qed etc.). Sections of different context within a sub-proof may be switched via next, which is just a single blockclose followed by block-open again. The effect of next is to reset the local proof context; there is no goal focus involved here!

For slightly more advanced applications, there are explicit block parentheses as well. These typically achieve a stronger forward style of reasoning.

next switches to a fresh block within a sub-proof, resetting the local context to the initial one.

{ and } explicitly open and close blocks. Any current facts pass through “{” unchanged, while “}” causes any result to be exported into the enclosing context. Thus fixed variables are generalized, assumptions discharged, and local definitions unfolded (cf. §3.2.2). There is no difference of assume and presume in this mode of forward reasoning — in contrast to plain backward reasoning with the result exported at show time.

3.2.9 Emulating tactic scripts

The Isar provides separate commands to accommodate tactic-style proof scripts within the same system. While being outside the orthodox Isar proof language, these might come in handy for interactive exploration and debugging, or even actual tactical proof within new-style theories (to benefit from document preparation, for example). See also §4.3.2 for actual tactics, that have been encapsulated as proof methods. Proper proof methods may be used in scripts, too.

apply^{∗} : proof (prove) → proof (prove)
apply end^{∗} : proof (state) → proof (state)
done^{∗} : proof (prove) → proof (state)
defer^{∗} : proof → proof
prefer^{∗} : proof → proof
back^{∗} : proof → proof
declare^{∗} : theory → theory

[figure: apply; apply end; method]

[figure: defer; nat]
[figure: prefer; nat]

[figure: declare; locale; thmrefs; and]

apply m applies proof method m in initial position, but unlike proof it retains “proof (prove)” mode. Thus consecutive method applications may be given just as in tactic scripts.

Facts are passed to m as indicated by the goal’s forward-chain mode, and are consumed afterwards. Thus any further apply command would always work in a purely backward manner.

apply end (m) applies proof method m as if in terminal position. Basically, this simulates a multi-step tactic script for qed, but may be given anywhere within the proof body.

No facts are passed to m. Furthermore, the static context is that of the enclosing goal (as for actual qed). Thus the proof method may not refer to any assumptions introduced in the current body, for example.

done completes a proof script, provided that the current goal state is solved completely. Note that actual structured proof commands (e.g. “.” or sorry) may be used to conclude proof scripts as well.

defer n and prefer n shuffle the list of pending goals: defer puts off goal n to the end of the list (n = 1 by default), while prefer brings goal n to the top.

back does back-tracking over the result sequence of the latest proof command. Basically, any proof command may return multiple results.

declare thms declares theorems to the current theory context (or the specified locale, see also §4.1.2). No theorem binding is involved here, unlike theorems or lemmas (cf. §3.1.7), so declare only has the effect of applying attributes as included in the theorem specification.

Any proper Isar proof method may be used with tactic script commands such as apply. A few additional emulations of actual tactics are provided as well; these would be never used in actual structured proofs, of course.

3.2.10 Meta-linguistic features

oops : proof → theory

The oops command discontinues the current proof attempt, while considering the partial proof text as properly processed. This is conceptually quite different from “faking” actual proofs via sorry (see §3.2.5): oops does not observe the proof structure at all, but goes back right to the theory level. Furthermore, oops does not produce any result theorem — there is no intended claim to be able to complete the proof anyhow.

A typical application of oops is to explain Isar proofs within the system itself, in conjunction with the document preparation tools of Isabelle described in [18]. Thus partial or even wrong proof attempts can be discussed in a logically sound manner. Note that the Isabelle L^{A}TEX macros can be easily adapted to print something like “…” instead of an “oops” keyword.

The oops command is undo-able, unlike kill (see §3.3.3). The effect is to get back to the theory just before the opening of the proof.

3.3 Other commands

3.3.1 Diagnostics

pr^{∗} : · → ·
thm^{∗} : theory | proof → theory | proof
term^{∗} : theory | proof → theory | proof
prop^{∗} : theory | proof → theory | proof
typ^{∗} : theory | proof → theory | proof
prf^{∗} : theory | proof → theory | proof
full prf^{∗} : theory | proof → theory | proof

These diagnostic commands assist interactive development. Note that undo does not apply here, the theory or proof configuration is not changed.

[figure: pr; modes; nat; ,; nat]

[figure: thm; modes; thmrefs]

[figure: term; modes; term]

[figure: prop; modes; prop]

[figure: typ; modes; type]

[figure: prf; modes; thmrefs]

[figure: full prf; modes; thmrefs]

modes

[figure: (; name; )]

pr goals, prems prints the current proof state (if present), including the proof context, current facts and goals. The optional limit arguments affect the number of goals and premises to be displayed, which is initially 10 for both. Omitting limit values leaves the current setting unchanged.

thm \overline{a} retrieves theorems from the current theory or proof context. Note that any attributes included in the theorem specifications are applied to a temporary context derived from the current theory or proof; the result is discarded, i.e. attributes involved in \overline{a} do not have any permanent effect.

term t and prop φ read, type-check and print terms or propositions according to the current theory or proof context; the inferred type of t is output as well. Note that these commands are also useful in inspecting the current environment of term abbreviations.

typ τ reads and prints types of the meta-logic according to the current theory or proof context.

prf displays the (compact) proof term of the current proof state (if present), or of the given theorems. Note that this requires proof terms to be switched on for the current object logic (see the “Proof terms” section of the Isabelle reference manual for information on how to do this).

full prf is like prf, but displays the full proof term, i.e. also displays information omitted in the compact proof term, which is denoted by “ ” placeholders there.

All of the diagnostic commands above admit a list of modes to be specified, which is appended to the current print mode (see also [10]). Thus the output behavior may be modified according particular print mode features. For example, pr (latex xsymbols symbols) would print the current proof state with mathematical symbols and special characters represented in L^{A}TEX source, according to the Isabelle style [18].

Note that antiquotations (cf. §2.2.9) provide a more systematic way to include formal items into the printed text document.

3.3.2 Inspecting the context

print commands^{∗} : · → ·
print syntax^{∗} : theory | proof → theory | proof
print methods^{∗} : theory | proof → theory | proof
print attributes^{∗} : theory | proof → theory | proof
print theorems^{∗} : theory | proof → theory | proof
thms containing^{∗} : theory | proof → theory | proof
thms deps^{∗} : theory | proof → theory | proof
print facts^{∗} : proof → proof
print binds^{∗} : proof → proof

[figure: thms containing; (; nat; ); criterion]

criterion

[figure: -; name; :; nameref; intro; elim; dest; simp; :; term; term]
[figure: thm deps; thmrefs]

These commands print certain parts of the theory and proof context. Note that there are some further ones available, such as for the set of rules declared for simplifications.

print commands prints Isabelle’s outer theory syntax, including keywords and command.

print syntax prints the inner syntax of types and terms, depending on the current context. The output can be very verbose, including grammar tables and syntax translation rules. See [10, §7, §8] for further information on Isabelle’s inner syntax.

print methods prints all proof methods available in the current theory context.

print attributes prints all attributes available in the current theory context.

print theorems prints theorems available in the current theory context.

In interactive mode this actually refers to the theorems left by the last transaction; this allows to inspect the result of advanced definitional packages, such as datatype. thms containing \overline{c} retrieves facts from the theory or proof context match-

ing all of the search criteria \overline{c}. The criterion name : s selects all theorems that contain s in their fully qualified name. The criteria intro, elim, and dest select theorems that match the current goal as introduction, elimination or destruction rules, respectively. The criterion simp : t selects all rewrite rules whose left-hand side matches the given term. The criterion term t selects all theorems that contain the pattern t – as usual, patterns may contain occurrences of the dummy “ ”, schematic variables, and type constraints.

Criteria can be preceded by “−” to select theorems that do not match. Note that giving the empty list of criteria yields all currently known facts. An optional limit for the number of printed facts may be given; the default is 40.

thm deps \overline{a} visualizes dependencies of facts, using Isabelle’s graph browser tool (see also [18]).

print facts prints any named facts of the current context, including assumptions and local results.

print binds prints all term abbreviations present in the context.

3.3.3 History commands

undo^{∗∗} : · → ·
redo^{∗∗} : · → ·
kill^{∗∗} : · → ·

The Isabelle/Isar top-level maintains a two-stage history, for theory and proof state transformation. Basically, any command can be undone using undo, excluding mere diagnostic elements. Its effect may be revoked via redo, unless the corresponding undo step has crossed the beginning of a proof or theory. The kill command aborts the current history node altogether, discontinuing a proof or even the whole theory. This operation is not undo-able.

! History commands should never be used with user interfaces such as Proof Gen-

eral [1, 2], which takes care of stepping forth and back itself. Interfering by manual undo, redo, or even kill commands would quickly result in utter confusion.

3.3.4 System operations

cd^{∗} : · → ·
pwd^{∗} : · → ·
use thy^{∗} : · → ·
use thy only^{∗} : · → ·
update thy^{∗} : · → ·
update thy only^{∗} : · → ·
display drafts^{∗} : · → ·
print drafts^{∗} : · → ·

[figure: cd; use thy; use thy only; update thy; update thy only; name]

[figure: display drafts; print drafts; name]

cd path changes the current directory of the Isabelle process.

pwd prints the current working directory.

use thy, use thy only, update thy, update thy only load some theory given as name argument. These commands are basically the same as the corresponding ML functions^{2} (see also [10, §1,§6]). Note that both the ML and Isar versions may load new- and old-style theories alike.

display drafts paths and print drafts paths perform simple output of a given list of raw source files. Only those symbols that do not require additional L^{A}TEX packages are displayed properly, everything else is left verbatim.

These system commands are scarcely used when working with the Proof General interface, since loading of theories is done transparently.

2The ML versions also change the implicit theory context to that of the theory loaded.

Generic tools and packages

4.1 Theory specification commands

4.1.1 Axiomatic type classes

axclass : theory → theory
instance : theory → proof (prove)
intro classes : method

Axiomatic type classes are provided by Isabelle/Pure as a definitional interface to type classes (cf. §3.1.3). Thus any object logic may make use of this light-weight mechanism of abstract theories [14]. There is also a tutorial on using axiomatic type classes in Isabelle [16] that is part of the standard Isabelle documentation.

[figure: axclass; classdecl; axmdecl; prop]

[figure: instance; nameref; <; ⊆; nameref; nameref; ::; arity]

axclass c ⊆ \overline{c} axms defines an axiomatic type class as the intersection of existing classes, with additional axioms holding. Class axioms may not contain more than one type variable. The class axioms (with implicit sort constraints added) are bound to the given names. Furthermore a class introduction rule is generated (being bound as c class.intro); this rule is employed by method intro classes to support instantiation proofs of this class. The “axioms” are stored as theorems according to the given name specifications, adding the class name c as name space prefix; the same facts are also stored collectively as c class.axioms. instance c_{1} ⊆ c_{2} and instance t :: (\overline{s})s setup a goal stating a class relation

or type arity. The proof would usually proceed by intro classes, and then establish the characteristic theorems of the type classes involved. After finishing the proof, the theory will be augmented by a type signature declaration corresponding to the resulting theorem.

intro classes repeatedly expands all class introduction rules of this theory. Note that this method usually needs not be named explicitly, as it is already included in the default proof step (of proof etc.). In particular, instantiation of trivial (syntactic) classes may be performed by a single “. .” proof step.

4.1.2 Locales and local contexts

Locales are named local contexts, consisting of a list of declaration elements that are modeled after the Isar proof context commands (cf. §3.2.2).

Localized commands

Existing locales may be augmented later on by adding new facts. Note that the actual context definition may not be changed! Several theory commands that produce facts in some way are available in “localized” versions, referring to a named locale instead of the global theory context.

locale

    [figure: (; in; name; )]

Emerging facts of localized commands are stored in two versions, both in the target locale and the theory (after export). The latter view produces a qualified binding, using the locale name as a name space prefix.

For example, “lemmas (in loc) a = \overline{b}” retrieves facts \overline{b} from the locale context of loc and augments its body by an appropriate “notes” element (see below). The exported view of a, after discharging the locale context, is stored as loc.a within the global theory. A localized goal “lemma (in loc) a : φ” works similarly, only that the fact emerges through the subsequent proof, which may refer to the full infrastructure of the locale context (covering local parameters with typing and concrete syntax, assumptions, definitions etc.). Most notably, fact declarations of the locale are active during the proof as well (e.g. local simp rules).

As a general principle, results exported from a locale context acquire additional premises according to the specification. Usually this is only a single predicate according to the standard “closed” view of locale specifications.

CHAPTER 4. GENERIC TOOLS AND PACKAGES 59 Locale specifications

locale : theory → theory
print locale^{∗} : theory | proof → theory | proof
print locales^{∗} : theory | proof → theory | proof
[figure: locale; (open); name; =; localeexpr]

    [figure: print locale; !; localeexpr]

localeexpr

[figure: contextexpr; +; contextelem; contextexpr; contextelem] contextexpr

[figure: nameref; (; contextexpr; ); contextexpr; name; mixfix; contextexpr; +]

CHAPTER 4. GENERIC TOOLS AND PACKAGES 60

contextelem

[figure: fixes; constrains; assumes; defines; notes; includes]

fixes

[figure: fixes; name; ::; type; structmixfix; and]

constrains

[figure: constrains; name; ::; type; and]

assumes

[figure: assumes; thmdecl; props; and]

defines

[figure: defines; thmdecl; prop; proppat; and]

notes

[figure: notes; thmdef; thmrefs; and]

includes

[figure: includes; contextexpr]

locale loc = import + body defines a new locale loc as a context consisting of a certain view of existing locales (import) plus some additional elements (body). Both import and body are optional; the degenerate form locale loc defines an empty locale, which may still be useful to collect declarations of facts later on. Type-inference on locale expressions automatically takes care of the most general typing that the combined context elements may acquire.

The import consists of a structured context expression, consisting of references to existing locales, renamed contexts, or merged contexts. Renaming uses positional notation: c \overline{x} means that (a prefix of) the fixed parameters of context c are named according to \overline{x}; a “_” (underscore) means to skip that position. Renaming by default deletes existing syntax. Optionally, new syntax may by specified with a mixfix annotation. Note that the special syntax declared with “(structure)” (see below) is neither deleted nor can it be changed. Merging proceeds from left-to-right, suppressing any duplicates stemming from different paths through the import hierarchy.

The body consists of basic context elements, further context expressions may be included as well.

fixes x :: τ (mx) declares a local parameter of type τ and mixfix annotation mx (both are optional). The special syntax declaration “(structure)” means that x may be referenced implicitly in this context.

constrains x :: τ introduces a type constraint τ on the local parameter x.

assumes a: \overline{φ} introduces local premises, similar to assume within a proof (cf. §3.2.2). defines a: x ≡ t defines a previously declared parameter. This is close

to def within a proof (cf. §3.2.2), but defines takes an equational proposition instead of variable-term pair. The left-hand side of the equation may have additional arguments, e.g. “defines f \overline{x} ≡ t”.

notes a = \overline{b} reconsiders facts within a local context. Most notably, this may include arbitrary declarations in any attribute specifications included here, e.g. a local simp rule.

includes c copies the specified context in a statically scoped manner. Only available in the long goal format of §3.2.4. In contrast, the initial import specification of a locale expression maintains a dynamic relation to the locales being referenced (benefiting from any later fact declarations in the obvious manner).

Note that “(is p)” patterns given in the syntax of assumes and defines above are illegal in locale definitions. In the long goal format of §3.2.4, term bindings may be included as expected, though.

By default, locale specifications are “closed up” by turning the given text into a predicate definition loc axioms and deriving the original assumptions as local lemmas (modulo local definitions). The predicate statement covers only the newly specified assumptions, omitting the content of included locale expressions. The full cumulative view is only provided on export, involving another predicate loc that refers to the complete specification text.

In any case, the predicate arguments are those locale parameters that actually occur in the respective piece of text. Also note that these predicates operate at the meta-level in theory, but the locale packages attempts to internalize statements according to the object-logic setup (e.g. replacing ⋀ by ∀, and ⟹ by → in HOL; see also §5.1). Separate introduction rules loc axioms . intro and loc . intro are declared as well.

The (open) option of a locale specification prevents both the current loc axioms and cumulative loc predicate constructions. Predicates are also omitted for empty specification texts.

print locale import + body prints the specified locale expression in a flattened form. The notable special case print locale loc just prints the contents of the named locale, but keep in mind that type-inference will normalize type variables according to the usual alphabetical order. The command omits notes elements by default. Use print locale! to get them included. print locales prints the names of all locales of the current theory.

Interpretation of locales

Locale expressions (more precisely, context expressions) may be instantiated, and the instantiated facts added to the current context. This requires a proof of the instantiated specification and is called locale interpretation. Interpretation is possible in theories and locales (command interpretation) and also in proof contexts (interpret).

interpretation : theory → proof (prove)
interpret : proof (state) | proof (chain) → proof (prove)
print interps^{∗} : theory | proof → theory | proof

[figure: interpretation; interp; name; <; ⊆; contextexp]

    [figure: interpret; interp]

    [figure: print interps; !; name]

interp

[figure: thmdecl; contextexpr; [; inst; ]]

interpretation expr insts The first form of interpretation interprets expr in the theory. The instantiation is given as a list of terms insts and is positional. All parameters must receive an instantiation term — with the exception of defined parameters. These are, if omitted, derived from the defining equation and other instantiations. Use “ ” to omit an instantiation term. Free variables are automatically generalized.

The command generates proof obligations for the instantiated specifications (assumes and defines elements). Once these are discharged by the user, instantiated facts are added to the theory in a post-processing phase.

The command is aware of interpretations already active in the theory. No proof obligations are generated for those, neither is post-processing applied to their facts. This avoids duplication of interpreted facts, in particular. Note that, in the case of a locale with import, parts of the interpretation may already be active. The command will only generate proof obligations and add facts for new parts.

The context expression may be preceded by a name and/or attributes. These take effect in the post-processing of facts. The name is used to prefix fact names, for example to avoid accidental hiding of other facts. Attributes are applied after attributes of the interpreted facts.

Adding facts to locales has the effect of adding interpreted facts to the theory for all active interpretations also. That is, interpretations dynamically participate in any facts added to locales.

interpretation name ⊆ expr This form of the command interprets expr in the locale name. It requires a proof that the specification of name implies the specification of expr. As in the localized version of the theorem command, the proof is in the context of name. After the proof obligation has been dischared, the facts of expr become part of locale name as derived context elements and are available when the context name is subsequently entered. Note that, like import, this is dynamic: facts added to a locale part of expr after interpretation become also available in name. Like facts of renamed context elements, facts obtained by interpretation may be accessed by prefixing with the parameter renaming (where the parameters are separated by ‘ ’).

Unlike interpretation in theories, instantiation is confined to the renaming of parameters, which may be specified as part of the context expression expr. Using defined parameters in name one may achieve an effect similar to instantiation, though.

Only specification fragments of expr that are not already part of name (be it imported, derived or a derived fragment of the import) are considered by interpretation. This enables circular interpretations.

If interpretations of name exist in the current theory, the command adds interpretations for expr as well, with the same prefix and attributes, although only for fragments of expr that are not interpreted

in the theory already.

interpret expr insts interprets expr in the proof context and is otherwise similar to interpretation in theories. Free variables in instantiations are not generalized, however.

print interps loc prints the interpretations of a particular locale loc that are active in the current context, either theory or proof context. The exclamation point argument causes triggers printing of witness theorems justifying interpretations. These are normally omitted from the output.

! Since attributes are applied to interpreted theorems, interpretation may modify

the current simpset and claset. Take this into account when choosing attributes for local theorems.

! An interpretation in a theory may subsume previous interpretations. This

happens if the same specification fragment is interpreted twice and the instantiation of the second interpretation is more general than the interpretation of the first. A warning is issued, since it is likely that these could have been generalized in the first place. The locale package does not attempt to remove subsumed interpretations. This situation is normally harmless, but note that blast gets confused by the presence of multiple axclass instances of a rule.

4.2 Derived proof schemes

4.2.1 Generalized elimination

obtain : proof (state) → proof (prove)

Generalized elimination means that additional elements with certain properties may be introduced in the current context, by virtue of a locally proven “soundness statement”. Technically speaking, the obtain language element is like a declaration of fix and assume (see also see §3.2.2), together with a soundness proof of its additional claim. According to the nature of existential reasoning, assumptions get eliminated from any result exported from the context later, provided that the corresponding parameters do not occur in the conclusion.

    [figure: obtain; vars; and; where; props; and]

obtain is defined as a derived Isar command as follows, where \overline{b} shall refer to (optional) facts indicated for forward chaining.

⟨facts \overline{b}⟩

obtain \overline{x} where a: \overline{φ} ⟨proof ⟩ ≡

have ⋀ thesis . (⋀ \overline{x} . \overline{φ} ⟹ thesis) ⟹ thesis proof succeed fix thesis assume that [intro?]: ⋀ \overline{x} . \overline{φ} ⟹ thesis thus thesis apply − using \overline{b} ⟨proof ⟩

qed

fix \overline{x} assume^{∗} a: \overline{φ}

Typically, the soundness proof is relatively straight-forward, often just by canonical automated tools such as “by simp” or “by blast”. Accordingly, the “that” reduction above is declared as simplification and introduction rule.

In a sense, obtain represents at the level of Isar proofs what would be meta-logical existential quantifiers and conjunctions. This concept has a broad range of useful applications, ranging from plain elimination (or introduction) of object-level existentials and conjunctions, to elimination over results of symbolic evaluation of recursive definitions, for example. Also note that obtain without parameters acts much like have, where the result is treated as a genuine assumption.

4.2.2 Calculational reasoning

also : proof (state) → proof (state)
finally : proof (state) → proof (chain)
moreover : proof (state) → proof (state)
ultimately : proof (state) → proof (chain)
print trans rules^{∗} : theory | proof → theory | proof
trans : attribute
sym : attribute
symmetric : attribute

Calculational proof is forward reasoning with implicit application of transitivity rules (such those of =, ≤, <). Isabelle/Isar maintains an auxiliary register calculation for accumulating results obtained by transitivity composed with the current result. Command also updates calculation involving this, while finally exhibits the final calculation by forward chaining towards the next goal statement. Both commands require valid current facts, i.e. may occur only after commands that produce theorems such as assume, note, or some finished proof of have, show etc. The moreover and ultimately commands are similar to also and finally, but only collect further results in calculation without applying any rules yet.

Also note that the implicit term abbreviation “…” has its canonical application with calculational proofs. It refers to the argument of the preceding statement. (The argument of a curried infix expression happens to be its right-hand side.)

Isabelle/Isar calculations are implicitly subject to block structure in the sense that new threads of calculational reasoning are commenced for any new block (as opened by a local goal, for example). This means that, apart from being able to nest calculations, there is no separate begin-calculation command required.

The Isar calculation proof commands may be defined as follows:^{1}

also_{0} ≡ note calculation = this
also_{n+1} ≡ note calculation = trans [OF calculation this]
finally ≡ also from calculation
moreover ≡ note calculation = calculation this
ultimately ≡ moreover from calculation

     [figure: also; finally; (; thmrefs; )]

    [figure: trans; add; del]

also (\overline{a}) maintains the auxiliary calculation register as follows. The first occurrence of also in some calculational thread initializes calculation by this. Any subsequent also on the same level of block-structure updates calculation by some transitivity rule applied to calculation and this (in that order). Transitivity rules are picked from the current context, unless alternative rules are given as explicit arguments. finally (\overline{a}) maintaining calculation in the same way as also, and concludes

1We suppress internal bookkeeping such as proper handling of block-structure.

the current calculational thread. The final result is exhibited as fact for forward chaining towards the next goal. Basically, finally just abbreviates also from calculation. Note that “finally show ?thesis .” and “finally have φ .” are typical idioms for concluding calculational proofs.

moreover and ultimately are analogous to also and finally, but collect results only, without applying rules.

print trans rules prints the list of transitivity rules (for calculational commands also and finally) and symmetry rules (for the symmetric operation and single step elimination patters) of the current context.

trans declares theorems as transitivity rules.

sym declares symmetry rules.

symmetric resolves a theorem with some rule declared as sym in the current context. For example, “assume [symmetric]: x = y” produces a swapped fact derived from that assumption. In structured proof texts it is often more appropriate to use an explicit single-step elimination proof, such as “assume x = y hence y = x . .”. The very same rules known to symmetric are declared as elim? as well.

4.3 Proof tools

4.3.1 Miscellaneous methods and attributes

unfold : method
fold : method
insert : method
erule^{∗} : method
drule^{∗} : method
frule^{∗} : method
succeed : method
fail : method

[figure: fold; unfold; insert; thmrefs]

[figure: erule; drule; frule; (; nat; ); thmrefs]

unfold \overline{a} and fold \overline{a} expand (or fold back again) the given meta-level definitions throughout all goals; any chained facts provided are inserted into the goal and subject to rewriting as well.

insert \overline{a} inserts theorems as facts into all goals of the proof state. Note that current facts indicated for forward chaining are ignored.

erule \overline{a}, drule \overline{a}, and frule \overline{a} are similar to the basic rule method (see §3.2.6), but apply rules by elim-resolution, destruct-resolution, and forward-resolution, respectively [10]. The optional natural number argument (default 0) specifies additional assumption steps to be performed here.

Note that these methods are improper ones, mainly serving for experimentation and tactic script emulation. Different modes of basic rule application are usually expressed in Isar at the proof language level, rather than via implicit proof state manipulations. For example, a proper single-step elimination would be done using the plain rule method, with forward chaining of current facts.

succeed yields a single (unchanged) result; it is the identity of the “,” method combinator (cf. §2.2.6).

fail yields an empty result sequence; it is the identity of the “|” method combinator (cf. §2.2.6).

tagged : attribute
untagged : attribute
THEN : attribute
COMP : attribute
unfolded : attribute
folded : attribute
elim format : attribute
standard^{∗} : attribute
no vars^{∗} : attribute

[figure: tagged; nameref]

[figure: untagged; name]

[figure: THEN; COMP; [; nat; ]; thmref]

[figure: unfolded; folded; thmrefs]

tagged name args and untagged name add and remove tags of some theorem. Tags may be any list of strings that serve as comment for some tools (e.g. lemma causes the tag “lemma” to be added to the result). The first string is considered the tag name, the rest its arguments. Note that untag removes any tags of the same name.

THEN a and COMP a compose rules by resolution. THEN resolves with the first premise of a (an alternative position may be also specified); the COMP version skips the automatic lifting process that is normally intended (cf. RS and COMP in [10, §5]).

unfolded \overline{a} and folded \overline{a} expand and fold back again the given meta-level definitions throughout a rule.

elim format turns a destruction rule into elimination rule format, by resolving with the rule PROP A ⟹ (PROP A ⟹ PROP B) ⟹ PROP B.

Note that the Classical Reasoner (§4.3.4) provides its own version of this operation.

standard puts a theorem into the standard form of object-rules at the outermost theory level. Note that this operation violates the local proof context (including active locales).

no vars replaces schematic variables by free ones; this is mainly for tuning output of pretty printed theorems.

4.3.2 Further tactic emulations

The following improper proof methods emulate traditional tactics. These admit direct access to the goal state, which is normally considered harmful! In particular, this may involve both numbered goal addressing (default 1), and dynamic instantiation within the scope of some subgoal.

! Dynamic instantiations refer to universally quantified parameters of a subgoal

(the dynamic context) rather than fixed variables and term abbreviations of a (static) Isar context.

Tactic emulation methods, unlike their ML counterparts, admit simultaneous instantiation from both dynamic and static contexts. If names occur in both contexts goal parameters hide locally fixed variables. Likewise, schematic variables refer to term abbreviations, if present in the static context. Otherwise the schematic variable is interpreted as a schematic variable and left to be solved by unification with certain parts of the subgoal.

Note that the tactic emulation proof methods in Isabelle/Isar are consistently named foo tac. Note also that variable names occurring on left hand sides of instantiations must be preceded by a question mark if they coincide with a keyword or contain dots. This is consistent with the attribute where (see §3.2.6).

rule tac^{∗} : method
erule tac^{∗} : method
drule tac^{∗} : method
frule tac^{∗} : method
cut tac^{∗} : method
thin tac^{∗} : method
subgoal tac^{∗} : method
rename tac^{∗} : method
rotate tac^{∗} : method
tactic^{∗} : method

[figure: rule tac; erule tac; drule tac; frule tac; cut tac; thin tac; goalspec; insts; thmref; thmrefs]

[figure: subgoal tac; goalspec; prop]

[figure: rename tac; goalspec; name]

[figure: rotate tac; goalspec; int]

[figure: tactic; text]

insts

[figure: name; =; term; and; in]

rule tac etc. do resolution of rules with explicit instantiation. This works the same way as the ML tactics res_inst_tac etc. (see [10, §3]).

Multiple rules may be only given if there is no instantiation; then rule tac is the same as resolve_tac in ML (see [10, §3]).

cut tac inserts facts into the proof state as assumption of a subgoal, see also cut_facts_tac in [10, §3]. Note that the scope of schematic variables is spread over the main goal statement. Instantiations may be given as well, see also ML tactic cut_inst_tac in [10, §3]. thin tac φ deletes the specified assumption from a subgoal; note that φ may

contain schematic variables. See also thin_tac in [10, §3].

subgoal tac φ adds φ as an assumption to a subgoal. See also subgoal_tac and subgoals_tac in [10, §3].

rename tac \overline{x} renames parameters of a goal according to the list \overline{x}, which refers to the suffix of variables.

rotate tac n rotates the assumptions of a goal by n positions: from right to left if n is positive, and from left to right if n is negative; the default value is 1. See also rotate_tac in [10, §3].

tactic text produces a proof method from any ML text of type tactic. Apart from the usual ML environment and the current implicit theory context, the ML code may refer to the following locally bound values:

val ctxt  : Proof.context
val facts : thm list
val thm   : string -> thm
val thms  : string -> thm list

Here ctxt refers to the current proof context, facts indicates any current facts for forward-chaining, and thm / thms retrieve named facts (including global theorems) from the context.

4.3.3 The Simplifier

Simplification methods

simp : method
simp all : method

[figure: simp; simp all; !; opt; simpmod]

opt

[figure: (; no asm; no asm simp; no asm use; asm lr; )]

simpmod

     [figure: add; del; only; cong; add; del; split; add; del; :; thmrefs]

simp invokes Isabelle’s simplifier, after declaring additional rules according to the arguments given. Note that the only modifier first removes all other rewrite rules, congruences, and looper tactics (including splits), and then behaves like add.

The cong modifiers add or delete Simplifier congruence rules (see also [10]), the default is to add.

The split modifiers add or delete rules for the Splitter (see also [10]), the default is to add. This works only if the Simplifier method has been properly setup to include the Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already).

simp all is similar to simp, but acts on all goals (backwards from the last to the first one).

By default the Simplifier methods take local assumptions fully into account, using equational assumptions in the subsequent normalization process, or simplifying assumptions themselves (cf. asm_full_simp_tac in [10, §10]). In structured proofs this is usually quite well behaved in practice: just the local premises of the actual goal are involved, additional facts may be inserted via explicit forward-chaining (using then, from etc.). The full context of assumptions is only included if the “!” (bang) argument is given, which should be used with some care, though.

Additional Simplifier options may be specified to tune the behavior further (mostly for unstructured scripts with many accidental local facts): “(no asm)” means assumptions are ignored completely (cf. simp_tac), “(no asm simp)” means assumptions are used in the simplification of the conclusion but are not themselves simplified (cf. asm_simp_tac), and “(no asm use)” means assumptions are simplified but are not used in the simplification of each other or the conclusion (cf. full_simp_tac). For compatibility reasons, there is also an option “(asm lr)”, which means that an assumption is only used for simplifying assumptions which are to the right

of it (cf. asm_lr_simp_tac).

The Splitter package is usually configured to work as part of the Simplifier. The effect of repeatedly applying split_tac can be simulated by “(simp only: split: \overline{a})”. There is also a separate split method available for single-step case splitting.

Declaring rules

print simpset^{∗} : theory | proof → theory | proof
simp : attribute
cong : attribute
split : attribute

     [figure: simp; cong; split; add; del]

print simpset prints the collection of rules declared to the Simplifier, which is also known as “simpset” internally [10]. This is a diagnostic command; undo does not apply.

simp declares simplification rules.

cong declares congruence rules.

split declares case split rules.

Forward simplification

simplified : attribute

[figure: simplified; opt; thmrefs]

opt

[figure: (; no asm; no asm simp; no asm use; )]

simplified \overline{a} causes a theorem to be simplified, either by exactly the specified rules \overline{a}, or the implicit Simplifier context if no arguments are given. The result is fully simplified by default, including assumptions and conclusion; the options no asm etc. tune the Simplifier in the same way as the for the simp method. Note that forward simplification restricts the simplifier to its most basic operation of term rewriting; solver and looper tactics [10] are not involved here. The simplified attribute should be only rarely required under normal circumstances.

Low-level equational reasoning

subst^{∗} : method
hypsubst^{∗} : method
split^{∗} : method

[figure: subst; (; asm; ); (; nat; ); thmref]

[figure: split; (; asm; ); thmrefs]

These methods provide low-level facilities for equational reasoning that are intended for specialized applications only. Normally, single step calculations would be performed in a structured text (see also §4.2.2), while the Simplifier methods provide the canonical way for automated normalization (see §4.3.3). subst eq performs a single substitution step using rule eq, which may be

either a meta or object equality.

subst (asm) eq substitutes in an assumption.

subst (i … j ) eq performs several substitutions in the conclusion. The numbers i to j indicate the positions to substitute at. Positions are ordered from the top of the term tree moving down from left to right. For example, in (a + b) + (c + d) there are three positions where commutativity of + is applicable: 1 refers to the whole term, 2 to a + b and 3 to c +d. If the positions in the list (i … j ) are non-overlapping (e.g. (2 3) in (a + b) + (c + d)) you may assume all substitutions are performed simultaneously. Otherwise the behaviour of subst is not specified.

subst (asm) (i … j ) eq performs the substitutions in the assumptions. Positions 1 … i_{1} refer to assumption 1, positions i_{1} + 1 … i_{2} to assumption 2, and so on.

hypsubst performs substitution using some assumption; this only works for equations of the form x = t where x is a free or bound variable.

split \overline{a} performs single-step case splitting using rules thms. By default, splitting is performed in the conclusion of a goal; the asm option indicates to operate on assumptions instead.

Note that the simp method already involves repeated application of split rules as declared in the current context.

4.3.4 The Classical Reasoner

Basic methods

rule : method
contradiction : method
intro : method
elim : method

[figure: rule; intro; elim; thmrefs]

rule as offered by the classical reasoner is a refinement over the primitive one (see §3.2.6). Both versions essentially work the same, but the classical version observes the classical rule context in addition to that of Isabelle/Pure.

Common object logics (HOL, ZF, etc.) declare a rich collection of classical rules (even if these would qualify as intuitionistic ones), but only few declarations to the rule context of Isabelle/Pure (§3.2.6).

contradiction solves some goal by contradiction, deriving any result from both ¬A and A. Chained facts, which are guaranteed to participate, may appear in either order.

intro and elim repeatedly refine some goal by intro- or elim-resolution, after having inserted any chained facts. Exactly the rules given as arguments are taken into account; this allows fine-tuned decomposition of a proof problem, in contrast to common automated tools.

Automated methods

blast : method
fast : method
slow : method
best : method
safe : method
clarify : method

[figure: blast; !; nat; clamod]

[figure: fast; slow; best; safe; clarify; !; clamod]

clamod

     [figure: intro; elim; dest; !; ?; del; :; thmrefs]

blast refers to the classical tableau prover (see blast_tac in [10, §11]). The optional argument specifies a user-supplied search bound (default 20).

fast, slow, best, safe, and clarify refer to the generic classical reasoner. See

     fast_tac, slow_tac, best_tac, safe_tac, and clarify_tac in [10,

§11] for more information.

Any of the above methods support additional modifiers of the context of classical rules. Their semantics is analogous to the attributes given before. Facts provided by forward chaining are inserted into the goal before commencing proof search. The “!” argument causes the full context of assumptions to be included as well.

Combined automated methods

auto : method
force : method
clarsimp : method
fastsimp : method
slowsimp : method
bestsimp : method

[figure: auto; !; nat; nat; clasimpmod]

[figure: force; clarsimp; fastsimp; slowsimp; bestsimp; !; clasimpmod]

clasimpmod

[figure: simp; add; del; only; cong; split; add; del; iff; add; ?; del; intro; elim; dest; !; ?; del; :; thmrefs]

auto, force, clarsimp, fastsimp, slowsimp, and bestsimp provide access to Isabelle’s combined simplification and classical reasoning tactics. These

correspond to auto_tac, force_tac, clarsimp_tac, and Classical

Reasoner tactics with the Simplifier added as wrapper, see [10, §11] for more information. The modifier arguments correspond to those given in §4.3.3 and §4.3.4. Just note that the ones related to the Simplifier are prefixed by simp here.

Facts provided by forward chaining are inserted into the goal before doing the search. The “!” argument causes the full context of assumptions to be included as well.

Declaring rules

print claset^{∗} : theory | proof → theory | proof
intro : attribute
elim : attribute
dest : attribute
rule : attribute
iff : attribute

[figure: intro; elim; dest; !; ?]
[figure: rule; del]

[figure: iff; add; ?; del]

print claset prints the collection of rules declared to the Classical Reasoner, which is also known as “simpset” internally [10]. This is a diagnostic command; undo does not apply.

intro, elim, and dest declare introduction, elimination, and destruction rules, respectively. By default, rules are considered as unsafe (i.e. not applied blindly without backtracking), while a single “!” classifies as safe. Rule declarations marked by “?” coincide with those of Isabelle/Pure, cf. §3.2.6 (i.e. are only applied in single steps of the rule method).

rule del deletes introduction, elimination, or destruction rules from the context.

iff declares logical equivalences to the Simplifier and the Classical reasoner at the same time. Non-conditional rules result in a “safe” introduction and elimination pair; conditional ones are considered “unsafe”. Rules with negative conclusion are automatically inverted (using ¬ elimination internally).

The “?” version of iff declares rules to the Isabelle/Pure context only, and omits the Simplifier declaration.

Classical operations

elim format : attribute
swapped : attribute

elim format turns a destruction rule into elimination rule format; this operation is similar to the the intuitionistic version (§4.3.1), but each premise of the resulting rule acquires an additional local fact of the negated main thesis; according to the classical principle (¬A ⟹ A) ⟹ A.

swapped turns an introduction rule into an elimination, by resolving with the classical swap principle (¬B ⟹ A) ⟹ (¬A ⟹ B).

4.3.5 Proof by cases and induction

Rule contexts

case : proof (state) → proof (state)
print cases^{∗} : proof → proof
case names : attribute
params : attribute
consumes : attribute

Basically, Isar proof contexts are built up explicitly using commands like fix, assume etc. (see §3.2.2). In typical verification tasks this can become hard to manage, though. In particular, a large number of local contexts may emerge from case analysis or induction over inductive sets and types.

The case command provides a shorthand to refer to certain parts of logical context symbolically. Proof methods may provide an environment of named “cases” of the form c: \overline{x}, \overline{φ}. Then the effect of “case c” is that of “fix \overline{x} assume c: \overline{φ}”. Term bindings may be covered as well, such as ?case for the intended conclusion.

Normally the “terminology” of a case value (i.e. the parameters \overline{x}) are marked as hidden. Using the explicit form “case (c \overline{x})” enables proof writers to choose their own names for the subsequent proof text.

It is important to note that case does not provide direct means to peek at the current goal state, which is generally considered non-observable in Isar. The text of the cases basically emerge from standard elimination or induction rules, which in turn are derived from previous theory specifications in a canonical way (say from inductive definitions).

Named cases may be exhibited in the current proof context only if both the proof method and the rules involved support this. Case names and parameters of basic rules may be declared by hand as well, by using appropriate attributes. Thus variant versions of rules that have been derived manually may be used in advanced case analysis later.

[figure: case; caseref; (; caseref; name; )]

caseref

[figure: nameref; attributes]

    [figure: case names; name]

    [figure: params; name; and]

    [figure: consumes; nat]

case (c \overline{x}) invokes a named local context c: \overline{x}, \overline{φ}, as provided by an appropriate proof method (such as cases and induct, see §4.3.5). The command “case (c \overline{x})” abbreviates “fix \overline{x} assume c: \overline{φ}”.

print cases prints all local contexts of the current state, using Isar proof language notation. This is a diagnostic command; undo does not apply. case names \overline{c} declares names for the local contexts of premises of some the-

orem; \overline{c} refers to the suffix of the list of premises.

params \overline{p}_{1} … \overline{p}_{n} renames the innermost parameters of premises 1, …, n of some theorem. An empty list of names may be given to skip positions, leaving the present parameters unchanged.

Note that the default usage of case rules does not directly expose parameters to the proof context (see also §4.3.5).

consumes n declares the number of “major premises” of a rule, i.e. the number of facts to be consumed when it is applied by an appropriate proof method (cf. §4.3.5). The default value of consumes is n = 1, which is appropriate for the usual kind of cases and induction rules for inductive sets (cf. §5.2.7). Rules without any consumes declaration given are treated as if consumes 0 had been specified.

Note that explicit consumes declarations are only rarely needed; this is already taken care of automatically by the higher-level cases and induct declarations, see also §4.3.5.

Proof methods

cases : method
induct : method

The cases and induct methods provide a uniform interface to case analysis and induction over datatypes, inductive sets, and recursive functions. The corresponding rules may be specified and instantiated in a casual manner. Furthermore, these methods provide named local contexts that may be invoked via the case proof command within the subsequent proof text. This accommodates compact proof texts even when reasoning about large specifications.

[figure: cases; spec]
[figure: induct; spec]

spec open

[figure: open; args; rule]

[figure: (; open; )]

args

[figure: insts; and]

rule

[figure: type; set; :; nameref; rule; :; thmref]

cases insts R applies method rule with an appropriate case distinction theorem, instantiated to the subjects insts. Symbolic case names are bound according to the rule’s local contexts.

The rule is determined as follows, according to the facts and arguments passed to the cases method:

facts  arguments rule
cases  classical case split
cases t  datatype exhaustion (type of t)
⊢ a ∈ A cases …  inductive set elimination (of A)
…  cases … R  explicit rule R

Several instantiations may be given, referring to the suffix of premises of the case rule; within each premise, the prefix of variables is instantiated. In most situations, only a single term needs to be specified; this refers to the first variable of the last premise (it is usually the same for all cases).

The “(open)” option causes the parameters of the new local contexts to be exposed to the current proof context. Thus local variables stemming from distant parts of the theory development may be introduced in an implicit manner, which can be quite confusing to the reader. Furthermore, this option may cause unwanted hiding of existing local variables, resulting in less robust proof texts. induct insts R is analogous to the cases method, but refers to induction

rules, which are determined as follows:

facts  arguments rule
induct P x … datatype induction (type of x)
⊢ x ∈ A induct …  set induction (of A)
…  induct … R  explicit rule R

Several instantiations may be given, each referring to some part of a mutual inductive definition or datatype — only related partial induction rules may be used together, though. Any of the lists of terms P, x, … refers to the suffix of variables present in the induction rule. This enables the writer to specify only induction variables, or both predicates and variables, for example.

The “(open)” option works the same way as for cases.

Above methods produce named local contexts, as determined by the instantiated rule as specified in the text. Beyond that, the induct method guesses further instantiations from the goal specification itself. Any persisting unresolved schematic variables of the resulting rule will render the the corresponding case invalid. The term binding ?case for the conclusion will be provided with each case, provided that term is fully specified.

The print cases command prints all named cases present in the current proof state.

It is important to note that there is a fundamental difference of the cases and induct methods in handling of non-atomic goal statements: cases just applies a certain rule in backward fashion, splitting the result into new goals with the local contexts being augmented in a purely monotonic manner.

In contrast, induct passes the full goal statement through the “recursive” course involved in the induction. Thus the original statement is basically replaced by separate copies, corresponding to the induction hypotheses and conclusion; the original goal context is no longer available. This behavior allows strengthened induction predicates to be expressed concisely as metalevel rule statements, i.e. ⋀ \overline{x} . \overline{φ} ⟹ ψ to indicate “variable” parameters \overline{x} and “recursive” assumptions \overline{φ}. Note that “case c” already performs “fix \overline{x}”. Also note that local definitions may be expressed as ⋀ \overline{x} . n ≡ t[\overline{x}] ⟹ φ[n], with induction over n.

In induction proofs, local assumptions introduced by cases are split into two different kinds: hyps stemming from the rule and prems from the goal statement. This is reflected in the extracted cases accordingly, so invoking “case c” will provide separate facts c.hyps and c.prems, as well as fact c to hold the all-inclusive list.

Facts presented to either method are consumed according to the number of “major premises” of the rule involved (see also §4.3.5), which is usually 0 for plain cases and induction rules of datatypes etc. and 1 for rules of inductive sets and the like. The remaining facts are inserted into the goal verbatim before the actual cases or induct rule is applied (thus facts may be even passed through an induction).

Declaring rules

print induct rules^{∗} : theory | proof → theory | proof
cases : attribute
induct : attribute

    [figure: cases; spec]
    [figure: induct; spec]

spec

     [figure: type; set; :; nameref]

print induct rules prints cases and induct rules for sets and types of the current context.

cases and induct (as attributes) augment the corresponding context of rules for reasoning about inductive sets and types, using the corresponding methods of the same name. Certain definitional packages of objectlogics usually declare emerging cases and induction rules as expected, so users rarely need to intervene.

Manual rule declarations usually include the the case names and ps attributes to adjust names of cases and parameters of a rule (see §4.3.5); the consumes declaration is taken care of automatically: consumes 0 is specified for “type” rules and consumes 1 for “set” rules.

Object-logic specific elements

5.1 General logic setup

judgment : theory → theory
atomize : method
atomize : attribute
rule format : attribute
rulify : attribute

The very starting point for any Isabelle object-logic is a “truth judgment” that links object-level statements to the meta-logic (with its minimal language of prop that covers universal quantification ⋀ and implication ⟹).

Common object-logics are sufficiently expressive to internalize rule statements over ⋀ and ⟹ within their own language. This is useful in certain situations where a rule needs to be viewed as an atomic statement from the meta-level perspective, e.g. ⋀ x . x ∈ A ⟹ P(x) versus ∀x ∈ A . P(x).

From the following language elements, only the atomize method and rule format attribute are occasionally required by end-users, the rest is for those who need to setup their own object-logic. In the latter case existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.

Generic tools may refer to the information provided by object-logic declarations internally.

[figure: judgment; constdecl]

[figure: atomize; (; full; )]

[figure: rule format; (; noasm; )]

judgment c :: σ (mx) declares constant c as the truth judgment of the current object-logic. Its type σ should specify a coercion of the category of object-level propositions to prop of the Pure meta-logic; the mixfix annotation (mx) would typically just link the object language (internally of syntactic category logic) with that of prop. Only one judgment declaration may be given in any theory development.

atomize (as a method) rewrites any non-atomic premises of a sub-goal, using the meta-level equations declared via atomize (as an attribute) beforehand. As a result, heavily nested goals become amenable to fundamental operations such as resolution (cf. the rule method) and proof-by-assumption (cf. assumption). Giving the “(full)” option here means to turn the whole subgoal into an object-statement (if possible), including the outermost parameters and assumptions as well.

A typical collection of atomize rules for a particular object-logic would provide an internalization for each of the connectives of ⋀, ⟹, and ≡. Meta-level conjunction expressed in the manner of minimal higherorder logic as ⋀ PROP C . (A ⟹ B ⟹ PROP C ) ⟹ PROP C should be covered as well (this is particularly important for locales, see §4.1.2).

rule format rewrites a theorem by the equalities declared as rulify rules in the current object-logic. By default, the result is fully normalized, including assumptions and conclusions at any depth. The no asm option restricts the transformation to the conclusion of a rule.

In common object-logics (HOL, FOL, ZF), the effect of rule format is to replace (bounded) universal quantification (∀) and implication (→) by the corresponding rule statements over ⋀ and ⟹.

5.2 HOL

5.2.1 Primitive types

typedecl : theory → theory
typedef : theory → proof (prove)

[figure: typedecl; typespec; infix]

[figure: typedef; altname; abstype; =; repset]

altname

[figure: (; name; open; open; name; )]

abstype

[figure: typespec; infix]

repset

[figure: term; morphisms; name; name]

typedecl (\overline{α})t is similar to the original typedecl of Isabelle/Pure (see §3.1.4), but also declares type arity t :: (type, …, type)type, making t an actual HOL type constructor.

typedef (\overline{α})t = A sets up a goal stating non-emptiness of the set A. After finishing the proof, the theory will be augmented by a Gordon/HOLstyle type definition, which establishes a bijection between the representing set A and the new type t.

Technically, typedef defines both a type t and a set (term constant) of the same name (an alternative base name may be given in parentheses). The injection from type to set is called Rep t, its inverse Abs t (this may be changed via an explicit morphisms declaration).

Theorems Rep t, Rep t inverse, and Abs t inverse provide the most basic characterization as a corresponding injection/surjection pair (in both directions). Rules Rep t inject and Abs t inject provide a slightly more convenient view on the injectivity part, suitable for automated proof tools (e.g. in simp or iff declarations). Rules Rep t cases/Rep t induct, and Abs t cases/Abs t induct provide alternative views on surjectivity; these are already declared as set or type rules for the generic cases and induct methods.

An alternative name may be specified in parentheses; the default is to use t as indicated before. The open declaration suppresses a separate constant definition for the representing set.

Note that raw type declarations are rarely used in practice; the main application is with experimental (or even axiomatic!) theory fragments. Instead of primitive HOL type definitions, user-level theories usually refer to higher-level packages such as record (see §5.2.3) or datatype (see §5.2.4).

5.2.2 Adhoc tuples

split format^{∗} : attribute

    [figure: split format; name; and; (; complete; )]

split format \overline{p}_{1} … \overline{p}_{n} puts expressions of low-level tuple types into canonical form as specified by the arguments given; \overline{p}_{i} refers to occurrences in premise i of the rule. The “(complete)” option causes all arguments in function applications to be represented canonically according to their tuple type structure.

Note that these operations tend to invent funny names for new local parameters to be introduced.

5.2.3 Records

In principle, records merely generalize the concept of tuples, where components may be addressed by labels instead of just position. The logical infrastructure of records in Isabelle/HOL is slightly more advanced, though, supporting truly extensible record schemes. This admits operations that are polymorphic with respect to record extension, yielding “object-oriented” effects like (single) inheritance. See also [6] for more details on object-oriented verification and record subtyping in HOL.

Basic concepts

Isabelle/HOL supports both fixed and schematic records at the level of terms and types. The notation is as follows:

record terms  record types
fixed (|x = a, y = b|) (|x :: A, y :: B|)
schematic (|x = a, y = b, … = m|) (|x :: A, y :: B, …:: M |)

The ASCII representation of (|x = a|) is (| x = a |).

A fixed record (|x = a, y = b|) has field x of value a and field y of value b. The corresponding type is (|x :: A, y :: B|), assuming that a :: A and b :: B.

A record scheme like (|x = a, y = b, … = m|) contains fields x and y as before, but also possibly further fields as indicated by the “…” notation (which is actually part of the syntax). The improper field “…” of a record scheme is called the more part. Logically it is just a free variable, which is occasionally referred to as “row variable” in the literature. The more part of a record scheme may be instantiated by zero or more further components. For example, the previous scheme may get instantiated to (|x = a, y = b, z = c, … = m′|), where m′ refers to a different more part. Fixed records are special instances of record schemes, where “…” is properly terminated by the () :: unit element. Actually, (|x = a, y = b|) is just an abbreviation for (|x = a, y = b, … = ()|).

Two key observations make extensible records in a simply typed language like HOL feasible:

1. the more part is internalized, as a free term or type variable,

2. field names are externalized, they cannot be accessed within the logic as first-class values.

In Isabelle/HOL record types have to be defined explicitly, fixing their field names and types, and their (optional) parent record. Afterwards, records may be formed using above syntax, while obeying the canonical order of fields as given by their declaration. The record package provides several standard operations like selectors and updates. The common setup for various generic proof tools enable succinct reasoning patterns. See also the Isabelle/HOL tutorial [8] for further instructions on using records in practice.

Record specifications

record : theory → theory

[figure: record; typespec; =; type; +; constdecl]

record (\overline{α})t = τ + \overline{c} :: \overline{σ} defines extensible record type (\overline{α})t, derived from the optional parent record τ by adding new field components \overline{c} :: \overline{σ}.

The type variables of τ and \overline{σ} need to be covered by the (distinct) parameters \overline{α}. Type constructor t has to be new, while τ needs to specify an instance of an existing record type. At least one new field \overline{c} has to be specified. Basically, field names need to belong to a unique record. This is not a real restriction in practice, since fields are qualified by the record name internally.

The parent record specification τ is optional; if omitted t becomes a root record. The hierarchy of all records declared within a theory context forms a forest structure, i.e. a set of trees starting with a root record each. There is no way to merge multiple parent records!

For convenience, (\overline{α}) t is made a type abbreviation for the fixed record type (|\overline{c} :: \overline{σ}|), likewise is (\overline{α}, ζ) t scheme made an abbreviation for (|\overline{c} :: \overline{σ}, …:: ζ|).

Record operations

Any record definition of the form presented above produces certain standard operations. Selectors and updates are provided for any field, including the improper one “more”. There are also cumulative record constructor functions. To simplify the presentation below, we assume for now that (\overline{α}) t is a root record with fields \overline{c} :: \overline{σ}.

Selectors and updates are available for any field (including “more”):

c_{i}  :: (|\overline{c} :: \overline{σ}, …:: ζ|) ⇒ σ_{i}
c_{i} update :: σ_{i} ⇒ (|\overline{c} :: \overline{σ}, …:: ζ|) ⇒ (|\overline{c} :: \overline{σ}, …:: ζ|)

There is special syntax for application of updates: r (|x := a|) abbreviates term x update a r. Further notation for repeated updates is also available: r (|x := a|) (|y := b|) (|z := c|) may be written r (|x := a, y := b, z := c|). Note that because of postfix notation the order of fields shown here is reverse than in the actual term. Since repeated updates are just function applications, fields may be freely permuted in (|x := a, y := b, z := c|), as far as logical equality is concerned. Thus commutativity of independent updates can be proven within the logic for any two fields, but not as a general theorem.

The make operation provides a cumulative record constructor function:

t.make :: \overline{σ} ⇒ (|\overline{c} :: \overline{σ}|)

We now reconsider the case of non-root records, which are derived of some parent. In general, the latter may depend on another parent as well, resulting in a list of ancestor records. Appending the lists of fields of all ancestors results in a certain field prefix. The record package automatically takes care of this by lifting operations over this context of ancestor fields. Assuming that (\overline{α}) t has ancestor fields \overline{b} :: \overline{ρ}, the above record operations will get the following types:

c_{i}  :: (|\overline{b} :: \overline{ρ}, \overline{c} :: \overline{σ}, …:: ζ|) ⇒ σ_{i}
c_{i} update :: σ_{i} ⇒ (|\overline{b} :: \overline{ρ}, \overline{c} :: \overline{σ}, …:: ζ|) ⇒ (|\overline{b} :: \overline{ρ}, \overline{c} :: \overline{σ}, …:: ζ|)
t.make :: \overline{ρ} ⇒ \overline{σ} ⇒ (|\overline{b} :: \overline{ρ}, \overline{c} :: \overline{σ}|)

Some further operations address the extension aspect of a derived record scheme specifically: fields produces a record fragment consisting of exactly the new fields introduced here (the result may serve as a more part elsewhere); extend takes a fixed record and adds a given more part; truncate restricts a record scheme to a fixed record.

t.fields  :: \overline{σ} ⇒ (|\overline{c} :: \overline{σ}|)
t.extend :: (|\overline{d} :: \overline{ρ}, \overline{c} :: \overline{σ}|) ⇒ ζ ⇒ (|\overline{d} :: \overline{ρ}, \overline{c} :: \overline{σ}, …:: ζ|)
t.truncate :: (|\overline{d} :: \overline{ρ}, \overline{c} :: \overline{σ}, …:: ζ|) ⇒ (|\overline{d} :: \overline{ρ}, \overline{c} :: \overline{σ}|)

Note that t.make and t.fields actually coincide for root records.

Derived rules and proof tools

The record package proves several results internally, declaring these facts to appropriate proof tools. This enables users to reason about record structures quite conveniently. Assume that t is a record type as specified above.

1. Standard conversions for selectors or updates applied to record constructor terms are made part of the default Simplifier context; thus proofs by reduction of basic operations merely require the simp method without further arguments. These rules are available as t.simps, too.

2. Selectors applied to updated records are automatically reduced by an internal simplification procedure, which is also part of the standard Simplifier setup.

3. Inject equations of a form analogous to ((x, y) = (x′, y′)) ≡ x = x′∧y = y′ are declared to the Simplifier and Classical Reasoner as iff rules. These rules are available as t.iffs.

4. The introduction rule for record equality analogous to x r = x r′ ⟹ y r = y r′ ⟹ … ⟹ r = r′ is declared to the Simplifier, and as the basic rule context as “intro?”. The rule is called t.equality.

5. Representations of arbitrary record expressions as canonical constructor terms are provided both in cases and induct format (cf. the generic proof methods of the same name, §4.3.5). Several variations are available, for fixed records, record schemes, more parts etc.

The generic proof methods are sufficiently smart to pick the most sensible rule according to the type of the indicated record expression: users just need to apply something like “(cases r)” to a certain proof problem.

6. The derived record operations t.make, t.fields, t.extend, t.truncate are not treated automatically, but usually need to be expanded by hand, using the collective fact t.defs.

5.2.4 Datatypes

datatype : theory → theory
rep datatype : theory → theory

[figure: datatype; dtspec; and]

[figure: rep datatype; name; dtrules] dtspec

[figure: parname; typespec; infix; =; cons; |]

cons

[figure: name; type; mixfix]

dtrules

    [figure: distinct; thmrefs; inject; thmrefs; induction; thmrefs]

datatype defines inductive datatypes in HOL.

rep datatype represents existing types as inductive ones, generating the standard infrastructure of derived concepts (primitive recursion etc.).

The induction and exhaustion theorems generated provide case names according to the constructors involved, while parameters are named after the types (see also §4.3.5).

See [7] for more details on datatypes, but beware of the old-style theory syntax being used there! Apart from proper proof methods for caseanalysis and induction, there are also emulations of ML tactics case_tac and induct_tac available, see §5.2.9; these admit to refer directly to the internal structure of subgoals (including internally bound parameters).

5.2.5 Recursive functions

primrec : theory → theory
recdef : theory → theory
recdef tc^{∗} : theory → proof (prove)

[figure: primrec; parname; equation]

[figure: recdef; (; permissive; ); name; term; prop; hints]

[figure: recdef tc; thmdecl; tc]

equation

[figure: thmdecl; prop]

hints

[figure: (; hints; recdefmod; )]

recdefmod

[figure: recdef simp; recdef cong; recdef wf; add; del; :; thmrefs; clasimpmod]

tc

[figure: nameref; (; nat; )]

primrec defines primitive recursive functions over datatypes, see also [7].

recdef defines general well-founded recursive functions (using the TFL package), see also [7]. The “(permissive)” option tells TFL to recover from failed proof attempts, returning unfinished results. The recdef simp, recdef cong, and recdef wf hints refer to auxiliary rules to be used in the internal automated proof process of TFL. Additional clasimpmod declarations (cf. §4.3.4) may be given to tune the context of the Simplifier (cf. §4.3.3) and Classical reasoner (cf. §4.3.4).

recdef tc c (i) recommences the proof for leftover termination condition number i (default 1) as generated by a recdef definition of constant c.

Note that in most cases, recdef is able to finish its internal proofs without manual intervention.

Both kinds of recursive definitions accommodate reasoning by induction (cf. §4.3.5): rule c.induct (where c is the name of the function definition) refers to a specific induction rule, with parameters named according to the user-specified equations. Case names of primrec are that of the datatypes involved, while those of recdef are numbered (starting from 1).

The equations provided by these packages may be referred later as theorem list f .simps, where f is the (collective) name of the functions defined. Individual equations may be named explicitly as well; note that for recdef each specification given by the user may result in several theorems.

Hints for recdef may be also declared globally, using the following attributes.

recdef simp : attribute
recdef cong : attribute
recdef wf : attribute

     [figure: recdef simp; recdef cong; recdef wf; add; del]

5.2.6 Definition by specification

specification : theory → proof (prove)
ax specification : theory → proof (prove)

decl

[figure: specification; ax specification; (; decl; ); thmdecl; prop]

[figure: name; :; term; (; overloaded; )]

specification decls φ sets up a goal stating the existence of terms with the properties specified to hold for the constants given in decls. After finishing the proof, the theory will be augmented with definitions for the given constants, as well as with theorems stating the properties for these constants.

ax specification decls φ sets up a goal stating the existence of terms with the properties specified to hold for the constants given in decls. After finishing the proof, the theory will be augmented with axioms expressing the properties given in the first place.

decl declares a constant to be defined by the specification given. The definition for the constant c is bound to the name c def unless a theorem name is given in the declaration. Overloaded constants should be declared as such.

Whether to use specification or ax specification is to some extent a matter of style. specification introduces no new axioms, and so by construction cannot introduce inconsistencies, whereas ax specification does introduce axioms, but only after the user has explicitly proven it to be safe. A practical issue must be considered, though: After introducing two constants with the same properties using specification, one can prove that the two constants are, in fact, equal. If this might be a problem, one should use ax specification.

5.2.7 (Co)Inductive sets

inductive : theory → theory
coinductive : theory → theory
mono : attribute

[figure: inductive; coinductive; sets; intros; monos]

[figure: mono; add; del]

sets

[figure: term]

intros

[figure: intros; thmdecl; prop]

monos

[figure: monos; thmrefs]

inductive and coinductive define (co)inductive sets from the given introduction rules.

mono declares monotonicity rules. These rule are involved in the automated monotonicity proof of inductive.

See [7] for further information on inductive definitions in HOL, but note that this covers the old-style theory format.

5.2.8 Arithmetic proof support

arith : method
arith split : attribute

    [figure: arith; !]

The arith method decides linear arithmetic problems (on types nat, int, real). Any current facts are inserted into the goal before running the procedure. The “!” argument causes the full context of assumptions to be included. The arith split attribute declares case split rules to be expanded before the arithmetic procedure is invoked.

Note that a simpler (but faster) version of arithmetic reasoning is already performed by the Simplifier.

5.2.9 Cases and induction: emulating tactic scripts

The following important tactical tools of Isabelle/HOL have been ported to Isar. These should be never used in proper proof texts!

case tac^{∗} : method
induct tac^{∗} : method
ind cases^{∗} : method
inductive cases : theory → theory

[figure: case tac; goalspec; term; rule]

[figure: induct tac; goalspec; insts; and; rule]

[figure: ind cases; prop]

[figure: inductive cases; thmdecl; prop; and]

rule

[figure: rule; :; thmref]

case tac and induct tac admit to reason about inductive datatypes only (unless an alternative rule is given explicitly). Furthermore, case tac does a classical case split on booleans; induct tac allows only variables to be given as instantiation. These tactic emulations feature both goal addressing and dynamic instantiation. Note that named rule cases are not provided as would be by the proper induct and cases proof methods (see §4.3.5). ind cases and inductive cases provide an interface to the internal

mk_cases operation. Rules are simplified in an unrestricted forward manner.

While ind cases is a proof method to apply the result immediately as elimination rules, inductive cases provides case split theorems at the theory level for later use,

5.2.10 Executable code

Isabelle/Pure provides a generic infrastructure to support code generation from executable specifications, both functional and relational programs. Isabelle/HOL instantiates these mechanisms in a way that is amenable to enduser applications. See [7] for further information (this actually covers the new-style theory format as well).

code module : theory → theory
code library : theory → theory
consts code : theory → theory
types code : theory → theory
code : attribute

[figure: code module; code library; modespec; name; file; name; imports; name; contains; name; =; term; term]

CHAPTER 5. OBJECT-LOGIC SPECIFIC ELEMENTS 103

modespec

[figure: (; name; )]

[figure: consts code; codespec]

codespec

[figure: name; ::; type; template; attachment]
[figure: types code; tycodespec]

tycodespec

[figure: name; template; attachment]

template

[figure: (; string; )]

attachment

[figure: attach; modespec; {*; text; *}]

[figure: code; name]

5.3 HOLCF

5.3.1 Mixfix syntax for continuous operations

consts : theory → theory

HOLCF provides a separate type for continuous functions α → β, with an explicit application operator f · x. Isabelle mixfix syntax normally refers directly to the pure meta-level function type α ⇒ β, with application f x.

The HOLCF variant of consts modifies that of Pure Isabelle (cf. §3.1.5) such that declarations involving continuous function types are treated specifically. Any given syntax template is transformed internally, generating translation rules for the abstract and concrete representation of continuous application. Note that mixing of HOLCF and Pure application is not supported!

5.3.2 Recursive domains

domain : theory → theory

[figure: domain; parname; dmspec; and]

dmspec

[figure: typespec; =; cons; |]

cons

[figure: name; type; mixfix]

dtrules

    [figure: distinct; thmrefs; inject; thmrefs; induction; thmrefs]

Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf. §5.2.4). Mutual recursion is supported, but no nesting nor arbitrary branching. Domain constructors may be strict (default) or lazy, the latter admits to introduce infinitary objects in the typical LCF manner (e.g. lazy lists). See also [5] for a general discussion of HOLCF domains.

5.4 ZF

5.4.1 Type checking

The ZF logic is essentially untyped, so the concept of “type checking” is performed as logical reasoning about set-membership statements. A special method assists users in this task; a version of this is already declared as a “solver” in the standard Simplifier setup.

print tcset^{∗} : theory | proof → theory | proof
typecheck : method
TC : attribute

    [figure: TC; add; del]

print tcset prints the collection of typechecking rules of the current context.

Note that the component built into the Simplifier only knows about those rules being declared globally in the theory!

typecheck attempts to solve any pending type-checking problems in subgoals.

TC adds or deletes type-checking rules from the context.

5.4.2 (Co)Inductive sets and datatypes

Set definitions

In ZF everything is a set. The generic inductive package also provides a specific view for “datatype” specifications. Coinductive definitions are available in both cases, too.

inductive : theory → theory
coinductive : theory → theory
datatype : theory → theory
codatatype : theory → theory

     [figure: inductive; coinductive; domains; intros; hints]

CHAPTER 5. OBJECT-LOGIC SPECIFIC ELEMENTS 106

domains

    [figure: domains; term; +; <=; ⊆; term]

intros

[figure: intros; thmdecl; prop]

hints monos

[figure: monos; thmrefs]

condefs

     [figure: con defs; thmrefs]

typeintros

     [figure: type intros; thmrefs]

typeelims

     [figure: type elims; thmrefs]

In the following diagram monos, typeintros, and typeelims are the same as above.

[figure: monos; condefs; typeintros; typeelims]

     [figure: datatype; codatatype; domain; dtspec; and; hints]

domain

[figure: <=; ⊆; term]

dtspec

[figure: term; =; con; |]

con

[figure: name; (; term; ,; )]

hints

[figure: monos; typeintros; typeelims]

See [12] for further information on inductive definitions in HOL, but note that this covers the old-style theory format.

Primitive recursive functions

primrec : theory → theory

[figure: primrec; thmdecl; prop]

CHAPTER 5. OBJECT-LOGIC SPECIFIC ELEMENTS 108 Cases and induction: emulating tactic scripts The following important tactical tools of Isabelle/ZF have been ported to Isar. These should be never used in proper proof texts!

case tac^{∗} : method
induct tac^{∗} : method
ind cases^{∗} : method
inductive cases : theory → theory

[figure: case tac; induct tac; goalspec; name]

[figure: ind cases; prop]

[figure: inductive cases; thmdecl; prop; and]

Appendix A

Isabelle/Isar quick reference

A.1 Proof commands

A.1.1 Primitives and basic syntax

fix \overline{x}  augment context by ⋀ \overline{x} . □
assume a: \overline{φ}  augment context by \overline{φ} ⟹ □
then  indicate forward chaining of facts
have a: φ  prove local result
show a: φ  prove local result, establishing some goal
using \overline{a}  indicate use of additional facts
proof m_{1} … qed m_{2} apply proof methods
{ … }  declare explicit blocks
next  switch implicit blocks
note a = \overline{b}  reconsider facts
let p = t  abbreviate terms by higher-order matching
theory-stmt = theorem name: prop proof
| lemma name: prop proof
| types … | consts … | defs … | …
proof = prfx^{∗} proof method stmt^{∗} qed method
prfx = apply method
| using name^{+}
stmt = { stmt^{∗} }
| next
| note name = name^{+}
| let term = term
| fix var^{+}
| assume name: prop^{+}
| then goal-stmt
| goal
goal = have name: prop proof
| show name: prop proof

APPENDIX A. ISABELLE/ISAR QUICK REFERENCE 110

A.1.2 Abbreviations and synonyms

by m_{1} m_{2} ≡ proof m_{1} qed m_{2}
. . ≡ by rule
. ≡ by this
hence ≡ then have
thus ≡ then show
from \overline{a} ≡ note this = \overline{a} then
with \overline{a} ≡ from \overline{a} and this
from this ≡ then
from this have ≡ hence
from this show ≡ thus

A.1.3 Derived elements

also_{0} ≈ note calculation = this
also_{n+1} ≈ note calculation = trans [OF calculation this]
finally ≈ also from calculation
moreover ≈ note calculation = calculation this
ultimately ≈ moreover from calculation
presume a: \overline{φ} ≈ assume a: \overline{φ}
def a: x ≡ t ≈ fix x assume a: x ≡ t
obtain \overline{x} where a: \overline{φ} ≈ … fix \overline{x} assume a: \overline{φ}
case c ≈ fix \overline{x} assume c: \overline{φ}
sorry ≈ by cheating

A.1.4 Diagnostic commands

pr  print current state
thm \overline{a} print theorems
term t print term
prop φ print meta-level proposition
typ τ print meta-level type

APPENDIX A. ISABELLE/ISAR QUICK REFERENCE 111

A.2 Proof methods

Single steps (forward-chaining facts)

assumption  apply some assumption
this  apply current facts
rule \overline{a}  apply some rule
rule  apply standard rule (default for proof)
contradiction apply ¬ elimination rule (any order)
cases t  case analysis (provides cases)
induct \overline{x}  proof by induction (provides cases)

Repeated steps (inserting facts)

−  no rules
intro \overline{a}  introduction rules
intro classes class introduction rules
elim \overline{a}  elimination rules
unfold \overline{a}  definitions

Automated proof tools (inserting facts, or even prems!)

rules  intuitionistic proof search
blast, fast  Classical Reasoner
simp, simp all Simplifier (+ Splitter)
auto, force  Simplifier + Classical Reasoner
arith  Arithmetic procedure

APPENDIX A. ISABELLE/ISAR QUICK REFERENCE 112

A.3 Attributes

Operations

OF \overline{a}  rule resolved with facts (skipping “ ”)
of \overline{t}  rule instantiated with terms (skipping “ ”)
where \overline{x} = \overline{t}  rule instantiated with terms, by variable name
symmetric  resolution with symmetry rule
THEN b  resolution with another rule
rule format  result put into standard rule format
elim format  destruct rule turned into elimination rule format

Declarations

simp  Simplifier rule
intro, elim, dest Pure or Classical Reasoner rule
iff  Simplifier + Classical Reasoner rule
split  case split rule
trans  transitivity rule
sym  symmetry rule

A.4 Rule declarations and methods

rule rules blast etc. simp etc. auto etc.
elim! intro! (Pure) × ×
elim intro (Pure) × ×
elim! intro!  ×  ×  ×
elim intro  ×  ×  ×
iff  ×  ×  ×  ×
iff ?  ×
elim? intro?  ×
simp  ×  ×
cong  ×  ×
split  ×  ×

APPENDIX A. ISABELLE/ISAR QUICK REFERENCE 113

A.5 Emulating tactic scripts

A.5.1 Commands

apply m  apply proof method at initial position
apply end (m) apply proof method near terminal position
done  complete proof
defer n  move subgoal to end
prefer n  move subgoal to beginning
back  backtrack last command
declare  declare rules in current theory

A.5.2 Methods

rule tac insts resolution (with instantiation)
erule tac insts elim-resolution (with instantiation)
drule tac insts destruct-resolution (with instantiation)
frule tac insts forward-resolution (with instantiation)
cut tac insts insert facts (with instantiation)
thin tac φ  delete assumptions
subgoal tac φ new claims
rename tac \overline{x} rename suffix of goal parameters
rotate tac n  rotate assumptions of goal
tactic text  arbitrary ML tactic
case tac t  exhaustion (datatypes)
induct tac \overline{x}  induction (datatypes)
ind cases t  exhaustion + simplification (inductive sets)

Appendix B

Isabelle/Isar conversion guide

Subsequently, we give a few practical hints on working in a mixed environment of old Isabelle ML proof scripts and new Isabelle/Isar theories. There are basically three ways to cope with this issue.

1. Do not convert old sources at all, but communicate directly at the level of internal theory and theorem values.

2. Port old-style theory files to new-style ones (very easy), and ML proof scripts to Isar tactic-emulation scripts (quite easy).

3. Actually redo ML proof scripts as human-readable Isar proof texts (probably hard, depending who wrote the original scripts).

B.1 No conversion

Internally, Isabelle is able to handle both old and new-style theories at the same time; the theory loader automatically detects the input format. In any case, the results are certain internal ML values of type theory and thm. These may be accessed from either classic Isabelle or Isabelle/Isar, provided that some minimal precautions are observed.

B.1.1 Referring to theorem and theory values

      thm         : xstring -> thm
      thms        : xstring -> thm list
      the_context : unit -> theory
      theory      : string -> theory

These functions provide general means to refer to logical objects from ML. Old-style theories used to emit many ML bindings of theorems and theories, but this is no longer done in new-style Isabelle/Isar theories.

thm name and thms name retrieve theorems stored in the current theory context, including any ancestor node.

The convention of old-style theories was to bind any theorem as an ML value as well. New-style theories no longer do this, so ML code may require thm "foo" rather than just foo.

the context() refers to the current theory context.

Old-style theories often use the ML binding thy, which is dynamically created by the ML code generated from old theory source. This is no longer the recommended way in any case! Function the_context should be used for old scripts as well.

theory name retrieves the named theory from the global theory-loader database.

The ML code generated from old-style theories would include an ML binding name.thy as part of an ML structure.

B.1.2 Storing theorem values

      qed        : string -> unit
      bind_thm   : string * thm -> unit
      bind_thms  : string * thm list -> unit

ML proof scripts have to be well-behaved by storing theorems properly within the current theory context, in order to enable new-style theories to retrieve these later.

qed name is the canonical way to conclude a proof script in ML. This already manages entry in the theorem database of the current theory context.

bind thm (name, thm) and bind thms (name, thms) store theorems that have been produced in ML in an ad-hoc manner.

Note that the original “LCF-system” approach of binding theorem values on the ML toplevel only has long been given up in Isabelle! Despite of this, old legacy proof scripts occasionally contain code such as val foo = result(); which is ill-behaved in several respects. Apart from preventing access from Isar theories, it also omits the result from the WWW presentation, for example.

B.1.3 ML declarations in Isar

ML : · → ·
ML setup : theory → theory

Isabelle/Isar theories may contain ML declarations as well. For example, an old-style theorem binding may be mimicked as follows.

     ML {∗ val foo = thm "foo" ∗}

Note that this command cannot be undone, so invalid theorem bindings in ML may persist. Also note that the current theory may not be modified; use ML setup for declarations that act on the current context.

B.2 Porting theories and proof scripts

Porting legacy theory and ML files to proper Isabelle/Isar theories has several advantages. For example, the Proof General user interface [1] for Isabelle/Isar is more robust and more comfortable to use than the version for classic Isabelle. This is due to the fact that the generic ML toplevel has been replaced by a separate Isar interaction loop, with full control over input synchronization and error conditions.

Furthermore, the Isabelle document preparation system (see also [18]) only works properly with new-style theories. Output of old-style sources is at the level of individual characters (and symbols), without proper document markup as in Isabelle/Isar theories.

B.2.1 Theories

Basically, the Isabelle/Isar theory syntax is a proper superset of the classic one. Only a few quirks and legacy problems have been eliminated, resulting in simpler rules and less special cases. The main changes of theory syntax are as follows.

• Quoted strings may contain arbitrary white space, and span several lines without requiring \ … \ escapes.

• Names may always be quoted.

The old syntax would occasionally demand plain identifiers vs. quoted strings to accommodate certain syntactic features.

• Types and terms have to be atomic as far as the theory syntax is concerned; this typically requires quoting of input strings, e.g. “x + y”.

The old theory syntax used to fake part of the syntax of types in order to require less quoting in common cases; this was hard to predict, though. On the other hand, Isar does not require quotes for simple terms, such as plain identifiers x, numerals 1, or symbols ∀ (input as \<forall>).

• Theorem declarations require an explicit colon to separate the name from the statement (the name is usually optional). Cf. the syntax of defs in §3.1.5, or theorem in §3.1.7.

Note that Isabelle/Isar error messages are usually quite explicit about the problem at hand. So in cases of doubt, input syntax may be just as well tried out interactively.

B.2.2 Goal statements

Simple goals

In ML the canonical a goal statement together with a complete proof script is as follows:

       Goal "φ";

by tac_{1}; ⋮

       qed "name";

This form may be turned into an Isar tactic-emulation script like this:

lemma name: "φ" apply meth_{1}

⋮ done

Note that the main statement may be theorem or corollary as well. See §B.2.3 for further details on how to convert actual tactic expressions into proof methods.

Classic Isabelle provides many variant forms of goal commands, see also [10] for further details. The second most common one is Goalw, which expands definitions before commencing the actual proof script.

       Goalw [def_{1}, . . .] "φ";

This may be replaced by using the unfold proof method explicitly.

lemma name: "φ" apply (unfold def_{1} …)

Deriving rules

Deriving non-atomic meta-level propositions requires special precautions in classic Isabelle: the primitive goal command decomposes a statement into the atomic conclusion and a list of assumptions, which are exhibited as ML values of type thm. After the proof is finished, these premises are discharged again, resulting in the original rule statement. The “long format” of Isabelle/Isar goal statements admits to emulate this technique nicely. The general ML goal statement for derived rules looks like this:

       val [prem_{1}, ...] = goal "φ_{1} ⟹ . . . ⟹ ψ";

by tac_{1}; ⋮

       qed "a"

This form may be turned into a tactic-emulation script as follows:

lemma a:

assumes prem_{1}: "φ_{1}" and … shows "ψ"

apply meth_{1}

⋮ done

In practice, actual rules are often rather direct consequences of corresponding atomic statements, typically stemming from the definition of a new concept. In that case, the general scheme for deriving rules may be greatly simplified, using one of the standard automated proof tools, such as simp, blast, or auto. This could work as follows:

lemma "φ_{1} ⟹ … ⟹ ψ"

by (unfold defs) blast

Note that classic Isabelle would support this form only in the special case where φ_{1}, … are atomic statements (when using the standard Goal command). Otherwise the special treatment of rules would be applied, disturbing this simple setup.

Occasionally, derived rules would be established by first proving an appropriate atomic statement (using ∀ and ⟶ of the object-logic), and putting the final result into “rule format”. In classic Isabelle this would usually proceed as follows:

       Goal "φ";

by tac_{1}; ⋮

       qed_spec_mp "name";

The operation performed by qed_spec_mp is also performed by the Isar attribute “rule format”, see also §5.1. Thus the corresponding Isar text may look like this:

lemma name [rule format]: "φ" apply meth_{1}

⋮ done

Note plain “rule format” actually performs a slightly different operation: it fully replaces object-level implication and universal quantification throughout the whole result statement. This is the right thing in most cases. For historical reasons, qed_spec_mp would only operate on the conclusion; one may get this exact behavior by using “rule format (no asm)” instead.

Actually “rule format” is a bit unpleasant to work with, since the final result statement is not shown in the text. An alternative is to state the resulting rule in the intended form in the first place, and have the initial refinement step turn it into internal object-logic form using the atomize method indicated below. The remaining script is unchanged.

lemma name: "⋀ \overline{x} . \overline{φ} ⟹ ψ" apply (atomize (full)) apply meth_{1}

⋮ done

In many situations the atomize step above is actually unnecessary, especially if the subsequent script mainly consists of automated tools.

B.2.3 Tactics

Isar Proof methods closely resemble traditional tactics, when used in unstructured sequences of apply commands (cf. §B.2.2). Isabelle/Isar provides emulations for all major ML tactics of classic Isabelle — mostly for the sake of easy porting of existing developments, as actual Isar proof texts would demand much less diversity of proof methods.

Unlike tactic expressions in ML, Isar proof methods provide proper concrete syntax for additional arguments, options, modifiers etc. Thus a typical method text is usually more concise than the corresponding ML tactic. Furthermore, the Isar versions of classic Isabelle tactics often cover several variant forms by a single method with separate options to tune the behavior. For example, method simp replaces all of simp_tac / asm_simp_tac / full_simp_tac / asm_full_simp_tac, there is also concrete syntax for augmenting the Simplifier context (the current “simpset”) in a convenient way.

Resolution tactics

Classic Isabelle provides several variant forms of tactics for single-step rule applications (based on higher-order resolution). The space of resolution tactics has the following main dimensions.

1. The “mode” of resolution: intro, elim, destruct, or forward (e.g.

     resolve_tac, eresolve_tac, dresolve_tac, forward_tac).

2. Optional explicit instantiation (e.g. resolve_tac vs. res_inst_tac).

3. Abbreviations for singleton arguments (e.g. resolve_tac vs. rtac).

Basically, the set of Isar tactic emulations rule tac, erule tac, drule tac, frule tac (see §4.3.2) would be sufficient to cover the four modes, either with or without instantiation, and either with single or multiple arguments. Although it is more convenient in most cases to use the plain rule method (see §3.2.6), or any of its “improper” variants erule, drule, frule (see §4.3.1). Note that explicit goal addressing is only supported by the actual rule tac version.

With this in mind, plain resolution tactics may be ported as follows.

rtac a 1  rule a
resolve_tac [a_{1}, …] 1  rule a_{1} …
res_inst_tac [(x_{1}, t_{1}), …] a 1 rule tac x_{1} = t_{1} and … in a
rtac a i  rule tac [i] a
resolve_tac [a_{1}, …] i  rule tac [i] a_{1} …
res_inst_tac [(x_{1}, t_{1}), …] a i rule tac [i] x_{1} = t_{1} and … in a

Note that explicit goal addressing may be usually avoided by changing the order of subgoals with defer or prefer (see §3.2.9).

Some further (less frequently used) combinations of basic resolution tactics may be expressed as follows.

ares_tac [a_{1}, …] 1 assumption | rule a_{1} …
eatac a n 1  erule (n) a
datac a n 1  drule (n) a
fatac a n 1  frule (n) a

Simplifier tactics

The main Simplifier tactics Simp_tac, simp_tac and variants (cf. [10]) are all covered by the simp and simp all methods (see §4.3.3). Note that there is no individual goal addressing available, simplification acts either on the first goal (simp) or all goals (simp all).

     Asm_full_simp_tac 1  simp
     ALLGOALS Asm_full_simp_tac simp all

Simp_tac 1  simp (no asm)
Asm_simp_tac 1  simp (no asm simp)

     Full_simp_tac 1  simp (no asm use)
     Asm_lr_simp_tac 1  simp (asm lr)

Isar also provides separate method modifier syntax for augmenting the Simplifier context (see §4.3.3), which is known as the “simpset” in ML. A typical ML expression with simpset changes looks like this:

      asm_full_simp_tac (simpset () addsimps [a_{1}, . . .] delsimps [b_{1}, . . .]) 1

The corresponding Isar text is as follows:

simp add : a_{1} … del : b_{1} …

Global declarations of Simplifier rules (e.g. Addsimps) are covered by application of attributes, see §B.2.4 for more information.

Classical Reasoner tactics

The Classical Reasoner provides a rather large number of variations of automated tactics, such as Blast_tac, Fast_tac, Clarify_tac etc. (see [10]). The corresponding Isar methods usually share the same base name, such as blast, fast, clarify etc. (see §4.3.4).

Similar to the Simplifier, there is separate method modifier syntax for augmenting the Classical Reasoner context, which is known as the “claset” in ML. A typical ML expression with claset changes looks like this:

      blast_tac (claset () addIs [a_{1}, . . .] addSEs [b_{1}, . . .]) 1

The corresponding Isar text is as follows:

blast intro : a_{1} … elim! : b_{1} …

Global declarations of Classical Reasoner rules (e.g. AddIs) are covered by application of attributes, see §B.2.4 for more information.

Miscellaneous tactics

There are a few additional tactics defined in various theories of Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF. The most common ones of these may be ported to Isar as follows.

stac a 1  subst a

     hyp_subst_tac 1  hypsubst

strip_tac 1  ≈ intro strip
split_all_tac 1  simp (no asm simp) only : split tupled all
≈ simp only : split tupled all
≪ clarify

Tacticals

Classic Isabelle provides a huge amount of tacticals for combination and modification of existing tactics. This has been greatly reduced in Isar, providing the bare minimum of combinators only: “,” (sequential composition), “|” (alternative choices), “?” (try), “+” (repeat at least once). These are usually sufficient in practice; if all fails, arbitrary ML tactic code may be invoked via the tactic method (see §4.3.2).

Common ML tacticals may be expressed directly in Isar as follows:

tac_{1} THEN tac_{2}  meth_{1}, meth_{2}
tac_{1} ORELSE tac_{2} meth_{1} | meth_{2}
TRY tac  meth?
REPEAT1 tac  meth+
REPEAT tac  (meth+)?
EVERY [tac_{1}, …]  meth_{1}, …
FIRST [tac_{1}, …]  meth_{1} | …

CHANGED (see [10]) is usually not required in Isar, since most basic proof methods already fail unless there is an actual change in the goal state. Nevertheless, “?” (try) may be used to accept unchanged results as well.

ALLGOALS, SOMEGOAL etc. (see [10]) are not available in Isar, since there is no direct goal addressing. Nevertheless, some basic methods address all goals internally, notably simp all (see §4.3.3). Also note that ALLGOALS may be often replaced by “+” (repeat at least once), although this usually has a different operational behavior, such as solving goals in a different order.

Iterated resolution, such as REPEAT (FIRSTGOAL (resolve_tac …)), is usually better expressed using the intro and elim methods of Isar (see §4.3.4).

B.2.4 Declarations and ad-hoc operations

Apart from proof commands and tactic expressions, almost all of the remaining ML code occurring in legacy proof scripts are either global context declarations (such as Addsimps) or ad-hoc operations on theorems (such as RS). In Isar both of these are covered by theorem expressions with attributes.

Theorem operations may be attached as attributes in the very place where theorems are referenced, say within a method argument. The subsequent ML combinators may be expressed directly in Isar as follows.

thm_{1} RS thm_{2}  thm_{1} [THEN thm_{2}]
thm_{1} RSN (i, thm_{2})  thm_{1} [THEN [i] thm_{2}]
thm_{1} COMP thm_{2}  thm_{1} [COMP thm_{2}]
[thm_{1}, …] MRS thm  thm [OF thm_{1} …]
read_instantiate [(x_{1}, t_{1}), …] thm thm [where x_{1} = t_{1} and …]
make_elim thm  thm [elim format]
standard thm  thm [standard]

Note that OF is often more readable as THEN ; likewise positional instantiation with of is often more appropriate than where.

The special ML command qed_spec_mp of Isabelle/HOL and FOL may be replaced by passing the result of a proof through rule format.

Global ML declarations may be expressed using the declare command (see §3.2.9) together with appropriate attributes. The most common ones are as follows.

Addsimps [thm]  declare thm [simp]
Delsimps [thm]  declare thm [simp del]
Addsplits [thm] declare thm [split]
Delsplits [thm] declare thm [split del]
AddIs [thm]  declare thm [intro]
AddEs [thm]  declare thm [elim]
AddDs [thm]  declare thm [dest]
AddSIs [thm]  declare thm [intro!]
AddSEs [thm]  declare thm [elim!]
AddSDs [thm]  declare thm [dest!]
AddIffs [thm]  declare thm [iff ]

Note that explicit declare commands are rarely needed in practice; Isar admits to declare theorems on-the-fly wherever they emerge. Consider the following ML idiom:

      Goal "φ";

⋮

      qed "name";
      Addsimps [name];

This may be expressed more succinctly in Isar like this:

lemma name [simp]: φ

⋮

The name may be even omitted, although this would make it difficult to declare the theorem otherwise later (e.g. as [simp del]).

B.3 Writing actual Isar proof texts

Porting legacy ML proof scripts into Isar tactic emulation scripts (see §B.2) is mainly a technical issue, since the basic representation of formal “proof script” is preserved. In contrast, converting existing Isabelle developments into actual human-readably Isar proof texts is more involved, due to the fundamental change of the underlying paradigm.

This issue is comparable to that of converting programs written in a low-level programming languages (say Assembler) into higher-level ones (say Haskell). In order to accomplish this, one needs a working knowledge of the target language, as well an understanding of the original idea of the piece of code expressed in the low-level language.

As far as Isar proofs are concerned, it is usually much easier to re-use only definitions and the main statements, while following the arrangement of proof scripts only very loosely. Ideally, one would also have some informal proof outlines available for guidance as well. In the worst case, obscure proof scripts would have to be re-engineered by tracing forth and backwards, and by educated guessing!

This is a possible schedule to embark on actual conversion of legacy proof scripts into Isar proof texts.

1. Port ML scripts to Isar tactic emulation scripts (see §B.2).

2. Get sufficiently acquainted with Isabelle/Isar proof development.^{1}

3. Recover the proof structure of a few important theorems.

4. Rephrase the original intention of the course of reasoning in terms of Isar proof language elements.

Certainly, rewriting formal reasoning in Isar requires some additional effort. On the other hand, one gains a human-readable representation of machine-checked formal proof. Depending on the context of application, this might be even indispensable to start with!

1As there is still no Isar tutorial around, it is best to look at existing Isar examples, see also §1.3.2.

Bibliography

[1] David Aspinall. Proof General. http://proofgeneral.inf.ed.ac.uk/.

[2] David Aspinall. Proof General: A generic tool for proof development. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1785 of Lecture Notes in Computer Science, pages 38–42. Springer-Verlag, 2000.

[3] Gertrud Bauer and Markus Wenzel. Computer-assisted mathematics at work — the Hahn-Banach theorem in Isabelle/Isar. In Thierry Coquand, Peter Dybjer, Bengt Nordström, and Jan Smith, editors, Types for Proofs and Programs: TYPES’99, LNCS, 2000.

[4] Gertrud Bauer and Markus Wenzel. Calculational reasoning revisited — an Isabelle/Isar experience. In R. J. Boulton and P. B. Jackson, editors, Theorem Proving in Higher Order Logics: TPHOLs 2001, volume 2152 of Lecture Notes in Computer Science. Springer-Verlag, 2001.

[5] Olaf Müller, Tobias Nipkow, David von Oheimb, and Oscar Slotosch. HOLCF = HOL + LCF. Journal of Functional Programming, 9:191–223, 1999.

[6] Wolfgang Naraschewski and Markus Wenzel. Object-oriented verification based on record subtyping in higher-order logic. In Jim Grundy and Malcom Newey, editors, Theorem Proving in Higher Order Logics: TPHOLs ’98, volume 1479 of Lecture Notes in Computer Science. Springer-Verlag, 1998.

[7] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle’s Logics: HOL. http://isabelle.in.tum.de/doc/logics-HOL.pdf.

[8] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic. Springer, 2002. LNCS 2283.

[9] Lawrence C. Paulson. Introduction to Isabelle.

http://isabelle.in.tum.de/doc/intro.pdf.

[10] Lawrence C. Paulson. The Isabelle Reference Manual. http://isabelle.in.tum.de/doc/ref.pdf.

[11] Lawrence C. Paulson. Isabelle’s Logics.

http://isabelle.in.tum.de/doc/logics.pdf.

BIBLIOGRAPHY 127

[12] Lawrence C. Paulson. Isabelle’s Logics: FOL and ZF.

http://isabelle.in.tum.de/doc/logics-ZF.pdf.

[13] Christoph Wedler. Emacs package “X-Symbol”.

http://x-symbol.sourceforge.net.

[14] Markus Wenzel. Type classes and overloading in higher-order logic. In Elsa L. Gunter and Amy Felty, editors, Theorem Proving in Higher Order Logics: TPHOLs ’97, volume 1275 of Lecture Notes in Computer Science. Springer-Verlag, 1997.

[15] Markus Wenzel. Isar — a generic interpretative approach to readable formal proof documents. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics: TPHOLs ’99, volume 1690 of Lecture Notes in Computer Science. Springer-Verlag, 1999.

[16] Markus Wenzel. Using Axiomatic Type Classes in Isabelle, 2000. http://isabelle.in.tum.de/doc/axclass.pdf.

[17] Markus Wenzel. Isabelle/Isar — a versatile environment for human-readable formal proof documents. PhD thesis, Institut für Informatik, Technische Universität München, 2002. http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html.

[18] Markus Wenzel and Stefan Berghofer. The Isabelle System Manual. http://isabelle.in.tum.de/doc/system.pdf.

[19] Freek Wiedijk. The mathematical vernacular. Unpublished paper, 2000. http://www.cs.kun.nl/∼freek/notes/mv.ps.gz.

Index

− (method), 45 . (command), 43 .. (command), 43 … (variable), 48 { (command), 49 } (command), 49 _(theorem), 40, 61 _(variable), 48

also (command), 66 Antiquotations

const, 18 full-prf, 18 goals, 18 ML, 18 prf, 18 prop, 18 subgoals, 18 term, 18 term-style, 18 text, 18 thm, 18 thm-style, 18 typ, 18 typeof, 18

apply (command), 49 apply-end (command), 49 args (syntax), 14 arith (HOL method), 100 arith-split (HOL attribute), 100 arities (command), 28 arity (syntax), 11 assume (command), 37 assumption (method), 45 atom (syntax), 14 atomize (attribute), 88 atomize (method), 88 Attributes

arith-split (HOL), 100 atomize, 88 case-names, 82 cases, 87 code, 102 COMP, 69 cong, 75 consumes, 82 dest, 81 dest (Pure), 45 elim, 81 elim (Pure), 45 elim-format, 82 elim-format (Pure), 69 folded, 69 iff, 81 induct, 87 intro, 81 intro (Pure), 45 mono (HOL), 99 no-vars, 69 OF, 45 of, 45 params, 82 recdef-cong (HOL), 98 recdef-simp (HOL), 98 recdef-wf (HOL), 98 rule, 81 rule (Pure), 45 rule-format, 88 rulify, 88 simp, 75 simplified, 75 split, 75 split-format (HOL), 91 standard, 69 swapped, 82 sym, 66 symmetric, 66 tagged, 69 TC, 105 THEN, 69 trans, 66 typecheck, 105 unfolded, 69 untagged, 69 where, 45

attributes (syntax), 14 auto (method), 79 axclass (command), 57 axioms (command), 32 axmdecl (syntax), 15

back (command), 49 best (method), 78 bestsimp (method), 79 blast (method), 78 by (command), 43

calculation (theorem), 66 case (command), 82 case (variable), 86 case-names (attribute), 82 case-tac (HOL method), 101 case-tac (ZF method), 108 Cases

rule-context, 42 cases (attribute), 87 cases (method), 84 cd (command), 56 chapter (command), 26 clamod (syntax), 78 clarify (method), 78 clarsimp (method), 79 clasimpmod (syntax), 79 classdecl (syntax), 11 classes (command), 27 classrel (command), 27 codatatype (ZF command), 105 code (attribute), 102 code-library (command), 102 code-module (command), 102 coinductive (HOL command), 99 coinductive (ZF command), 105 Commands

., 43 .., 43 {, 49 }, 49 also, 66 apply, 49 apply-end, 49 arities, 28 assume, 37 axclass, 57 axioms, 32 back, 49 by, 43 case, 82 cd, 56 chapter, 26 classes, 27 classrel, 27 codatatype (ZF), 105 code-library, 102 code-module, 102 coinductive (HOL), 99 coinductive (ZF), 105 constdefs, 29 consts, 29 consts (HOLCF), 104 consts-code, 102 context, 24 corollary, 40 datatype (HOL), 95 datatype (ZF), 105 declare, 49 def, 37 defaultsort, 27 defer, 49 defs, 29 display-drafts, 56 domain (HOLCF), 104 done, 49 end, 24 finally, 66 fix, 37 from, 39 global, 32 have, 40 header, 24 hence, 40 hide, 32 inductive (HOL), 99 inductive (ZF), 105 inductive-cases (HOL), 101 inductive-cases (ZF), 108 instance, 57 interpret, 63 interpretation, 63 judgment, 88 kill, 55 lemma, 40 lemmas, 32 let, 47 local, 32 locale, 59 method-setup, 33 ML, 33 ML-command, 33 ML-setup, 33 moreover, 66 next, 49 no-syntax, 30 nonterminals, 28 note, 39 obtain, 65 oops, 51 oracle, 36 parse-ast-translation, 35 parse-translation, 35 pr, 51 prefer, 49 presume, 37 primrec (HOL), 96 primrec (ZF), 107 print-ast-translation, 35 print-attributes, 53 print-binds, 53 print-cases, 82 print-claset, 81 print-commands, 53 print-drafts, 56 print-facts, 53 print-induct-rules, 87 print-interps, 63 print-locale, 59 print-locales, 59 print-methods, 53 print-simpset, 75 print-syntax, 53 print-tcset, 105 print-theorems, 53 print-trans-rules, 66 print-translation, 35 proof, 43 prop, 51 pwd, 56 qed, 43 recdef (HOL), 96 recdef-tc (HOL), 96 record (HOL), 93 redo, 55 rep-datatype (HOL), 95 sect, 37 section, 26 setup, 33 show, 40 sorry, 43 specification (HOL), 98 subsect, 37 subsection, 26 subsubsect, 37 subsubsection, 26 syntax, 30 term, 51 text, 26 text-raw, 26 then, 39 theorem, 40 theorems, 32 theory, 24 thm, 51 thm-deps, 53 thms-containing, 53 thus, 40 token-translation, 35 translations, 30 txt, 37 txt-raw, 37 typ, 51 typed-print-translation, 35 typedecl, 28 typedecl (HOL), 89 typedef (HOL), 89 types, 28 types-code, 102 ultimately, 66 undo, 55 update-thy, 56 update-thy-only, 56 use, 33 use-thy, 56 use-thy-only, 56 using, 39 with, 39 comment (syntax), 10 COMP (attribute), 69 cong (attribute), 75 const (antiquotation), 18 constdecl (syntax), 29 constdefs (command), 29 consts (command), 29 consts (HOLCF command), 104 consts-code (command), 102 consumes (attribute), 82 context (command), 24 contextelem (syntax), 59 contextexpr (syntax), 59 contradiction (method), 77 corollary (command), 40 cut-tac (method), 71

datatype (HOL command), 95 datatype (ZF command), 105 declare (command), 49 def (command), 37 default (method), 77 defaultsort (command), 27 defer (command), 49 defs (command), 29 dest (attribute), 81 dest (Pure attribute), 45 display-drafts (command), 56 domain (HOLCF command), 104 done (command), 49 drule (method), 68 drule-tac (method), 71

elim (attribute), 81 elim (method), 77 elim (Pure attribute), 45 elim-format (attribute), 82 elim-format (Pure attribute), 69 end (command), 24 erule (method), 68 erule-tac (method), 71 fail (method), 68 fast (method), 78 fastsimp (method), 79 finally (command), 66 fix (command), 37 fold (method), 68 folded (attribute), 69 force (method), 79 from (command), 39 frule (method), 68 frule-tac (method), 71 full-prf (antiquotation), 18

global (command), 32 goals (antiquotation), 18 goalspec (syntax), 14

have (command), 40 header (command), 24 hence (command), 40 hide (command), 32 hypsubst (method), 76

ident (syntax), 8 iff (attribute), 81 ind-cases (HOL method), 101 ind-cases (ZF method), 108 induct (attribute), 87 induct (method), 84 induct-tac (HOL method), 101 induct-tac (ZF method), 108 inductive (HOL command), 99 inductive (ZF command), 105 inductive-cases (HOL command),

101 inductive-cases (ZF command),

108 infix (syntax), 12 insert (method), 68 inst (syntax), 12 instance (command), 57 insts (syntax), 12 int (syntax), 9 interp (syntax), 63 interpret (command), 63 interpretation (command), 63 intro (attribute), 81 intro (method), 77 intro (Pure attribute), 45 intro-classes (method), 57 iprover (method), 45

judgment (command), 88

kill (command), 55

lemma (command), 40 lemmas (command), 32 let (command), 47 local (command), 32 locale (command), 59 locale (syntax), 58 longident (syntax), 8

method (syntax), 14

method-setup (command), 33 Methods −, 45 arith (HOL), 100 assumption, 45 atomize, 88 auto, 79 best, 78 bestsimp, 79 blast, 78 case-tac (HOL), 101 case-tac (ZF), 108 cases, 84 clarify, 78 clarsimp, 79 contradiction, 77 cut-tac, 71 default, 77 drule, 68 drule-tac, 71 elim, 77 erule, 68 erule-tac, 71 fail, 68 fast, 78 fastsimp, 79 fold, 68 force, 79 frule, 68 frule-tac, 71 hypsubst, 76 ind-cases (HOL), 101 ind-cases (ZF), 108 induct, 84 induct-tac (HOL), 101 induct-tac (ZF), 108 insert, 68 intro, 77 intro-classes, 57 iprover, 45 rename-tac, 71 rotate-tac, 71 rule, 45, 77 rule-tac, 71 safe, 78 simp, 73 simp-all, 73 slow, 78 slowsimp, 79 split, 76 subgoal-tac, 71 subst, 76 succeed, 68 tactic, 71 thin-tac, 71 this, 45 unfold, 68

mixfix (syntax), 12 ML (antiquotation), 18 ML (command), 33 ML-command (command), 33 ML-setup (command), 33 mono (HOL attribute), 99 moreover (command), 66

name (syntax), 9 nameref (syntax), 9 nat (syntax), 8 next (command), 49 no-syntax (command), 30 no-vars (attribute), 69 nonterminals (command), 28 note (command), 39 nothing (theorem), 40

obtain (command), 65 OF (attribute), 45 of (attribute), 45 oops (command), 51 oracle (command), 36

params (attribute), 82 parname (syntax), 9 parse-ast-translation (command),

35 parse-translation (command), 35 pr (command), 51 prefer (command), 49 prems (theorem), 39 presume (command), 37 prf (antiquotation), 18 primrec (HOL command), 96 primrec (ZF command), 107 print-ast-translation (command),

35 print-attributes (command), 53 print-binds (command), 53 print-cases (command), 82 print-claset (command), 81 print-commands (command), 53 print-drafts (command), 56 print-facts (command), 53 print-induct-rules (command), 87 print-interps (command), 63 print-locale (command), 59 print-locales (command), 59 print-methods (command), 53 print-simpset (command), 75 print-syntax (command), 53 print-tcset (command), 105 print-theorems (command), 53 print-trans-rules (command), 66 print-translation (command), 35 proof

default, 44 fake, 44 terminal, 44 trivial, 44

proof (command), 43 prop (antiquotation), 18 prop (command), 51 prop (syntax), 11 proppat (syntax), 17 props (syntax), 17 pwd (command), 56

qed (command), 43

recdef (HOL command), 96 recdef-cong (HOL attribute), 98 recdef-simp (HOL attribute), 98 recdef-tc (HOL command), 96 recdef-wf (HOL attribute), 98 record (HOL command), 93 redo (command), 55 rename-tac (method), 71 rep-datatype (HOL command), 95 rotate-tac (method), 71 rule (attribute), 81 rule (method), 45, 77 rule (Pure attribute), 45 rule-context (case), 42 rule-format (attribute), 88 rule-tac (method), 71 rulify (attribute), 88

safe (method), 78 sect (command), 37 section (command), 26 selection (syntax), 15 setup (command), 33 show (command), 40 simp (attribute), 75 simp (method), 73 simp-all (method), 73 simplified (attribute), 75 simpmod (syntax), 73 slow (method), 78 slowsimp (method), 79 sorry (command), 43 sort (syntax), 11 specification (HOL command), 98 split (attribute), 75 split (method), 76 split-format (HOL attribute), 91 standard (attribute), 69 string (syntax), 8 structmixfix (syntax), 12 subgoal-tac (method), 71 subgoals (antiquotation), 18 subsect (command), 37 subsection (command), 26 subst (method), 76 subsubsect (command), 37 subsubsection (command), 26 succeed (method), 68 swapped (attribute), 82 sym (attribute), 66 symident (syntax), 8 symmetric (attribute), 66 Syntax

args, 14 arity, 11 atom, 14 attributes, 14 axmdecl, 15 clamod, 78 clasimpmod, 79 classdecl, 11 comment, 10 constdecl, 29 contextelem, 59 contextexpr, 59 goalspec, 14 ident, 8 infix, 12 inst, 12 insts, 12 int, 9 interp, 63 locale, 58 longident, 8 method, 14 mixfix, 12 name, 9 nameref, 9 nat, 8 parname, 9 prop, 11 proppat, 17 props, 17 selection, 15 simpmod, 73 sort, 11 string, 8 structmixfix, 12 symident, 8 tags, 22 term, 11 termpat, 17 text, 10 thmdecl, 15 thmdef, 15 thmref, 15 thmrefs, 15 type, 11 typefree, 8 typespec, 12 typevar, 8 var, 8 vars, 17 verbatim, 8 syntax (command), 30

tactic (method), 71 tagged (attribute), 69 tags (syntax), 22 TC (attribute), 105 term (antiquotation), 18 term (command), 51 term (syntax), 11 term abbreviations, 48 term-style (antiquotation), 18 termpat (syntax), 17 text (antiquotation), 18 text (command), 26 text (syntax), 10 text-raw (command), 26 THEN (attribute), 69 then (command), 39 theorem (command), 40 Theorems

_, 40, 61 calculation, 66 nothing, 40 prems, 39 this, 39

theorems (command), 32 theory (command), 24 thesis (variable), 48 thin-tac (method), 71 this (method), 45 this (theorem), 39 this (variable), 48 thm (antiquotation), 18 thm (command), 51 thm-deps (command), 53 thm-style (antiquotation), 18 thmdecl (syntax), 15 thmdef (syntax), 15 thmref (syntax), 15 thmrefs (syntax), 15 thms-containing (command), 53 thus (command), 40 token-translation (command), 35 trans (attribute), 66 translations (command), 30 txt (command), 37 txt-raw (command), 37 typ (antiquotation), 18 typ (command), 51 type (syntax), 11 typecheck (attribute), 105 typed-print-translation (com-

mand), 35 typedecl (command), 28 typedecl (HOL command), 89 typedef (HOL command), 89 typefree (syntax), 8 typeof (antiquotation), 18 types (command), 28 types-code (command), 102 typespec (syntax), 12 typevar (syntax), 8

ultimately (command), 66 undo (command), 55 unfold (method), 68 unfolded (attribute), 69 untagged (attribute), 69 update-thy (command), 56 update-thy-only (command), 56 use (command), 33 use-thy (command), 56 use-thy-only (command), 56 using (command), 39

var (syntax), 8 Variables

…, 48 _, 48 case, 86 thesis, 48 this, 48 vars (syntax), 17 verbatim (syntax), 8

where (attribute), 45 with (command), 39