Computer-Supported Modeling and Reasoning - Exercises
| Number | Date | Additional Files | Model Solution |
|---|---|---|---|
| 1 | 22.10.2004 | ||
| 2 | 29.10.2004 | ||
| 3 | 05.11.2004 | ONE_AXIOM.thy, ONE_RULE_fragment.thy | |
| 4 | 12.11.2004 | NSet.thy, NSet.ML, RED.thy, CONV.thy, CNUM.thy | |
| 5 | 19.11.2004 | STT.thy | |
| 6 | 26.11.2004 | Encode_fragment.thy | |
| 7 | 03.12.2004 | ||
| 8 | 10.12.2004 | ||
| 9 | 17.12.2004 | HOL_BASIC.thy, HOL_BASIC.ML | |
| 10 | no session | ||
| 11 | 14.01.2005 | FinSet.thy | |
| 12 | 21.01.2005 | ||
| 13 | 28.01.2005 | ||
| 14 | 04.02.2005 | AVL_fragment.thy | |
| 15 | 11.02.2005 | AVL_fragment.ML |
Configuring your system for Isabelle
Open a shell and type setup isabelle in it. This is a shellscript that will modify your path so that all files related to Isabelle will be found. In future sessions, this command should be invoked automatically. For this purpose, add the following line to your shell configuration file (called .cshrc if your shell is the c-shell or tc-shell):setup isabelleYou will always run Isabelle by starting xemacs. Before starting xemacs, add the following line to the init.el file in your .xemacs directory:
(load-file "/usr/local/ProofGeneral-3.4/generic/proof-site.el")This will instruct xemacs to use ProofGeneral, which is a sophisticated specialized interface providing many functionalities for running Isabelle.
It is important that you start xemacs from the shell (and not using, say, pop-up menus of your window manager). For the first week's exercises, create a working directory and type xemacs ex1.ML. The file ex1.ML will be your first proof script, that is, a file containing Isabelle proofs. Now customize xemacs using the rich menus provided:
- Multiple Frames: Isabelle will use several xemacs subwindows (simply windows in emacs jargon). You may choose if you want these displayed all in one window (called frame in emacs jargon) split into several parts or as several windows. This is done by (un)ticking the box "Proof-General:Options:Multiple Frames".
- X-Symbol: For a nice rendering of mathematical symbols, xemacs uses the
X-symbol package. To enable it, tick the box
"Proof-General:Options:X-Symbol".
You should now select "Proof-General:Options:Save Options" - Choosing the logic: We will use the logic FOL. Go to "Proof-General:Advanced:Customize:Isabelle:Chosen Logic". This will open a new buffer. Set the logic to "FOL" in this buffer and click "Save".
- Electric terminator: This will save you from having to type the return key to fire proof commands. Go to "Proof-General:Advanced:Customize:User Options:Electric Terminator Enable". This will open a new buffer. Set the option to "On" and click "Save".
The course is now finished.