Homework 02
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 code for the Dreadbury mansion