Proof using Igloo

Now we prove equation A.1 in Igloo. Before getting started on the proof, a small amount of housekeeping needs to be performed: connect to the Isabelle Server, and select the theories to work with.

Figure A.1: Igloo's main window

For the moment, this window is largely unused, except to connect to the

Isabelle Server (figure A.2), start a new theory, or quit

Igloo.

Figure A.2: Initiating a connection to the Isabelle Server

To connect to the

Isabelle Server, the user selects

Connect from the

Proof Engine menu.

Figure A.3: Successful connection to the Isabelle Server

Once the connection is successful, the user is notified via the status bar.

Figure A.4: Begin a new theory

Next, the user can define new theories. To get started, they select

New Theory from the

Theory menu.

Figure A.5: Naming a new theory

To specify a theorem to be proven,

Isabelle requires a name and a list of theories to extend.

Figure A.6: Naming theories to inherit

Most proofs can make good use of previously proven theorems. In order to do this, we tell

Isabelle which theories our new theory should inherit. This requires that the user have some knowledge of

Isabelle's theories. This is a restriction due to the current implementation of

PGIP. For proposed amendments that would remove these limitations, see §5.1.

Figure A.7: Igloo's proof window

Now the user is presented with

Igloo's

Proof Window. All theorems for this particular theory will be proved from this window. For a detailed description of what each component does, see page .

Figure A.8: Start a new theorem

To begin proving a theorem, the user selects

New Theorem from the

Theory menu.

Figure A.9: Naming the new theorem

To begin proving a theorem,

Isabelle requires a name and a specification (we have chosen ``sum of naturals''), figure A.10 shows the specification.

Figure A.10: Defining a new theorem

Note that the user is currently expected to know how to specify theorems in

Isabelle. This indicates a weak point of the current

PGIP interface.

Figure A.11: Initial proof state

The result from defining the name and specification of the theorem, is a proof state, which

Isabelle calls

Step 0.

Figure A.12: Initial subgoals

By expanding the node for the proof state, the user is able to see the current subgoals that need to be proven. Since this is the initial proof state, the goal that needs to be proven is the theorem itself.

Figure A.13: Apply induction to a subgoal

As in the human-written proof, we decide to apply mathematical induction, and split the proof into a base case and an inductive case. To do this, the user

right-clicks on the subgoal they wish to induct on, and selects

induct from the

apply tactic submenu. The tactics that are available are currently hard coded into

Igloo, this is another feature that

PGIP could provide.

Figure A.14: Second proof state

The result of applying this tactic is a new proof state.

Figure A.15: Theorem split into base and inductive cases

By expanding the proof state, we can see the two subgoals. The first subgoal is the base case, the second is the inductive case.

Figure A.16: Simplify the base case

Again, as in the human-written proof, we attempt to prove the base case of the induction, this time by the

simp tactic, which rewrites subterms in the hope of making the term simpler.

Figure A.17: Second proof state

Figure A.18: Removing an earlier proof state from the display

Since the previous proof state is the only one we are interested in, we can close the initial proof state.

Figure A.19: Inductive subgoal remains

Expanding the most recent proof state, we can see that the base case has been proven, and we are only left with the inductive case to prove.

Figure A.20: Simplifying the inductive case

Next, we attempt to prove the inductive case by simplification.

Figure A.21: Third proof state

Figure A.22: A complete proof

The next proof state is expanded to reveal no subgoals. This means the proof is now complete.