Homework 02

Question Formulation

For the last question you need to use Isabelle. Below are some examples to help you. You can also find useful information in the Isabelle tutorial and in the tutorial on Isar.

Isar is the proof language of Isabelle. If you don't know what the “have”, “with”, “thus”, etc… commands do, have a look at the Isar tutorial.

Not that in the provided Isabelle files, “- -” (double dash) and “txt” start a comment. The text of a comment is enclosed in “{**}” and the “@{}” annotations are just there for typesetting reasons.

Isabelle Examples as pdf

Isabelle code for the Dreadbury mansion

Isabelle code for problem 5 of exercises 2

Isabelle skeleton to complete