TWiki> PG Web>ProofGeneralKit>ProofGeneralEclipse>PGEclipseUserDocumentation>PGEclipseIsabelleTutorial (23 Aug 2006, DavidAspinall)EditAttach

FIXME: this content from old wiki and not fully converted yet
# Isabelle Beginners Tutorial using PG Eclipse

## Prerequisites

## Creating a first theory file

## A first proof

## Syntax

## Infix operators, priorities, and mixfix syntax

### A word of warning=

Priorities are a source of many problems in Isabelle. Some of Isabelle's parsing is counter-intuitive. For example, ### Using syntax annotations to define 'pretty' operators=

& should be written ''infix'', i.e. as \&(P Q) .
& R will be interpreted as (P # Q) \& R), and ''defines a simple ascii alternative to using its name'' - namely #.
Writing ## Defining a new type

## The 'standard' proof process

Working within attachment:ToyList.thy, we now define some functions that work on our list type:
## Summnary

This first tutorial should have familiarized you with:

These pages provide a quick-and-dirty introduction to using Isabelle / Isar. Note: they were written for pre-Isar Isabelle, and we are still in the process of converting them to modern Isar syntax. Some sections may be incorrect (sorry!). For a more thorough introduction to Isabelle, see http://www.cse.unsw.edu.au/~kleing/ijcar04-tut/

We recommend using the PG TeacherView to read them (''not'' the Eclipse Help browser), as this allows you to open and use sample files directly with a single click.

Isabelle (see ["Isabelle"]).

The Proof General / Eclipse editor

We will create a theory '''!NatSum''' that extends the theory [http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/HOL/Main.html Main], the standard parent which is itself the union of all the basic pre-defined theories such as [http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/HOL/Arith.html arithmetic], [http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/HOL/List.html lists], [http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/HOL/Set.html sets], etc. You may have a look at some of these theory files by clicking on the appropriate links. Theory files have the '''.thy''' suffix.

Using your editor, create the file attachment:NatSum.thy. Note: this link points to an annotated version of this tutorial file. If you are using the PG TeacherView, then such links will be opened in Proof General as files for scripting / editing. If you use this, be aware that it creates ''temporary files'', which are deleted when Proof General closes. To keep these files, use 'Save as...' to give them a permanent location.

In attachment:NatSum.thy, write the following lines:

{theory NatSum = Main: (* We will now define a new function 'sum' *) consts sum :: "[nat => nat, nat] => nat" primrec "sum f 0 = 0" "sum f (Suc n) = f(n) + sum f n" end

Note: * The comment, using {{{(* comment text *)}}} * The standard types '''nat''' (for ''natural number'') and '''A => B''' (for a function that maps As to Bs). * The constant '''sum''' declared with the curried function type {{{[nat => nat, nat] => nat}}}. * The function sum is defined using primitive recursion as indicated by the keyword '''primrec'''. The two equations given correspond to the base and recursive cases respectively. * The keywords '''theory''', and '''end''' are part of the fixed syntax used to define theory files.

Now, start a new Isabelle session if necessary (hit the ''Restart'' button attachment:restart.gif), and process the attachment:NatSum.thy script. This loads the theory file into Isabelle, which should say (when everything is processed): {{{Theory "NatSum" completed.}}}

We will now state and prove a lemma. If you have processed the NatSum script, use the ''Undo'' or ''Retract'' buttons to unlock it. Otherwise, Proof General will not let you edit the script. At the bottom of the attachment:NatSum.thy script, but ''before'' the '''end''' keyword, type the goal:

lemma myFirstLemma: "sum (\<lambda>i. Suc(i+i)) n = n*n"

Note that the editor will convert \

proof (prove): step 0 fixed variables: n goal (lemma (myFirstLemma), 1 subgoal): 1. sum (%i. Suc (i + i)) n = n * n

Note: Isabelle uses "%" as an alternative for "\

Try applying the induction tactic '''induct_tac''' on the variable '''n''' as follows (note the use of brackets to pass parameters to the tactic):

apply (induct_tac "n")

This tactic produces two subgoals - the base case and the induction step. Apply the automatic tactic '''auto''' to the subgoals and then close the resulting theorem by typing:

apply auto done

Now try to prove the following goals using '''induct_tac''' and '''auto''':

lemma triangleNumLemma: "2*sum (\<lambda>i. i) (Suc n) = n*Suc(n)" lemma: "Suc(Suc(Suc(Suc 2)))*sum (\<lambda>i. i*i) (Suc n) = n*Suc(n)*Suc(2*n)"

Feel free to invent and try to prove other goals in Isabelle. In the end, your theory file attachment:NatSum.thy will make up the basis of a useful library of theorems that could be used to build other theories, for example.

Isabelle / Isar syntax is quite complex - especially as there are mechanisms for extending and re-defining it! There is also lots of 'syntactic sugar' that makes proof scripts easier to read - but makes explaining the syntax a bit more complicated.

For now, stay cool and try to learn by examples. We will work on a page describing IsabelleSyntax .

\\ <not>\<not>x=xis interpreted as

\<not>\<not>( x=x ), and

\<lambda>x.x+1will cause an error. The moral for beginners is '''USE LOTS OF BRACKETS AND SPACES'''.

Using your editor, create the theory attachment:Gates.thy containing the lines:

theory Gate = HOL: consts "\<not>&" :: "[bool,bool] => bool" (infixl 35) defs nand_def: "P \<not>& Q ---++ \<not>(P & Q)"

This defines '''nand''' (not and) as an infix operator. The constant definition has a ''syntax annotation''

(infixl 3\ 5). This specifies that \

P \<not>& Qrather than

Note: The ''l'' in

infixlmeans that nand associated to the left (there is also the keyword ''infixr''). The '35' sets the ''priority'' of the operator. Operators with a high priority 'bind strongly', which means they can 'grab' inputs from those with lower priorities - but you can always use brackets to specify how terms should be structured. For now, don't worry about priorities - just use lots of brackets.

We will now look at using syntax annotation to specify prettier syntax. Extend Gates.thy with the commands:

consts xor :: "[bool,bool] => bool" (infixl "#" 35) defs xor_def: "P # Q ---++ (\<not>P & Q) \<or> (P & \<not>Q)" endThis defines another gate, ''xor'', assigns it as an infix operator with slightly higher priority than nand (so P # Q \

A xor Bremains valid, but you can also write

A # B. This is of dubious benefit here, but it can be of considerable benefit, as the ToyList example below shows.

We will now define two new datatypes, using the '''typedecl''' and '''datatype''' keywords. Create attachment:ToyList.thy with the following definitions:

theory ToyList = PreList: (* PreList is a pre-defined theory that does *not* include lists. We use it here so that our list will not be confused with the standard version. *) typedecl myUndefinedType datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65)The keyword '''typedecl''' defines a new type - but without a constructor. The keyword '''datatype''' is more useful. This defines the type

'a list, with two constructors - Nil and Cons. The

|is a special form of ''or''. It is used to specify that objects of type

'a listcan be created using the Nil constructor ''or'' the Cons constructor.

Nil and Cons have syntax annotations (in brackets) to make them easier to use. The syntax annotations allow us to create a list as follows:

term "x = True # False # []"Note: '''term''' is a kind of 'null' keyword: it asserts that what follows is a term (which isn't saying much). term can be used to check syntax or type, since you get some feedback from Isabelle when you process it.

consts app :: "['a list, 'a list] => 'a list" (infixr "@" 65) rev :: "'a list => 'a list" primrec "[] @ ys = ys" "(x # xs) @ ys = x # (xs @ ys)" primrec "rev [] = []" "rev (x # xs) = (rev xs) @ (x # [])"We will try to prove:

theorem rev_rev: "rev(rev xs) = xs"

This will require some lemmas before the proof will go through. These can be proved inside the proof, but it is often clearer to prove them first. How do we come up with the required lemmas? Try to prove the main theorem without them and study carefully what

apply\ autoleaves unproved. This can provide the clue.

lemma app_Nil2 [simp]: "xs @ [] = xs" apply(induct_tac xs) apply auto done lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" apply(induct_tac xs) apply auto done lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)" apply(induct_tac xs) apply auto done theorem rev_rev: "rev(rev xs) = xs" apply(induct_tac xs) apply auto done

Note the use of

[simp]in the lemma declarations. This tells Isabelle to add these lemmas to the ''simplifying set'', which is used by the

apply autotactic. It is tempting to think that all lemmas should have the simp attribute. However novices should refrain from awarding a lemma the simp attribute, which can jam the auto theorem prover. Instead, lemmas can be applied locally where they are needed.

* The basic structure of a theory file, some of its syntax. * How to define new functions and types. * How to produce a simple proof.

You can browse the [http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library Isabelle theory library] on the World Wide Web.

Edit | Attach | Print version | History: r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions

Topic revision: r2 - 23 Aug 2006 - 23:44:23 - DavidAspinall

Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.

Ideas, requests, problems regarding TWiki? Send feedback

This Wiki uses Cookies

Ideas, requests, problems regarding TWiki? Send feedback

This Wiki uses Cookies