ALERT! FIXME: this content from old wiki and not fully converted yet

Isabelle Beginners Tutorial using PG Eclipse

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.

Prerequisites

Isabelle (see ["Isabelle"]).

The Proof General / Eclipse editor smile

Creating a first theory file

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

A first proof

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 \ into a lambda character. You start the proof by processing this line (use either the ''Step Forward'' or ''Goto'' buttons). Isabelle will respond by going into ''proofstate'' mode and saying:

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.

Syntax

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 .

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,
\\
<not>\<not>x=x
is interpreted as
\<not>\<not>( x=x )
, and
\<lambda>x.x+1
will cause an error. The moral for beginners is '''USE LOTS OF BRACKETS AND SPACES'''.

Using syntax annotations to define 'pretty' operators=

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 \& should be written ''infix'', i.e. as
P \<not>& Q
rather than \&(P Q).

Note: The ''l'' in

infixl
means 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)"

end
This defines another gate, ''xor'', assigns it as an infix operator with slightly higher priority than nand (so P # Q \& R will be interpreted as (P # Q) \& R), and ''defines a simple ascii alternative to using its name'' - namely #. Writing
A xor B
remains 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.

Defining a new type

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 list
can 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.

The 'standard' proof process

Working within attachment:ToyList.thy, we now define some functions that work on our list type:
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\
 auto
leaves 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 auto
tactic. 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.

Summnary

This first tutorial should have familiarized you with:

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

Topic revision: r2 - 23 Aug 2006 - 23:44:23 - DavidAspinall
 
This site is powered by the TWiki collaboration platformCopyright © 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