The Bremen HOL-CASL system: Quick Introduction

It is recommended first to have a glimpse at the Isabelle documentation. We use Isabelle98. The documentation for Isabelle98 can be found here.
Also have a look at the IsaWin page. IsaWin is a graphical user interface for Isabelle. HOL-CASL is based on IsaWin.

Quick introduction into the menus of HOL-CASL:

Session Manager: You can save your work in a session and recover it later. When you start the system, the session manager asks you to create a new session or to recover an existing session.
File menu: Choose "Import file" to read a file. Files must end with ".casl" and must be stored in (a subfolder of) $HOL_CASL. Some example files are stored in the example subfolder. "Save" saves your session for later resuming it with the session manager. "Save & Quit" additionally quits, while "Abort" quits without saving - your work will be lost.
Development menu: You can search both theories ("Search Theories") and theorems ("Search Theories & Theorems"). To search a theorem, you first have to double-click on the theory in which the theorem lives. Using the button more, you can display more theories and theorems. You can drag and drop theories and theorems onto the desktop, for later use in proofs. The theory HOL1 is the theory of higher-order logic. All encodings of CASL theories are extensions of this theory. Sometimes, you need some theorem from HOL1 to proceed with a proof in a CASL theory.
Options menu: Here, you can setup various configurations of Isabelle. With "Isabelle Options" - "Open Isabelle Console" you can get a trace of the actions Isabelle performs (including simplifications).
Important : Under "CASL Options", with "Show Profiles" you can switch on or off the display of full profiles of CASL functions and predicates. Profiles can help to distinguish overloaded functions, but sometimes they are too noisy and lead to unreadable output.
Similarly, with "Show Injections" you can switch on or off the display of CASL subsort injections. An injection from a sort s to a sort s' is shown as s>s' .
Pop-up menu for theories: Click with the right mouse button at a theory. You can enter a proof goal, rename the theory or get the simplifier set or classical reasoner set associated with this theory. A goal for a CASL theory has to be entered in cASL syntax, while a goal for the theory HOL1 has to be entered in the Isabelle/HOL syntax.
Pop-up menu for theorems: Click with the right mouse button at theorem. You can select how the theorem is used when dragging it onto a goal (see the Isabelle manual for more information). Adding theorems to simplifier sets: Click at the theorem and drag it onto a simplifier set. A new simplifier set, with the theorem added, appears. You also can click at a number of theorems with the middle mouse button (the become yellow) and then drag them jointly onto a simplifier set.
Proving: Double click on a goal. A goal window opens. You can drag and drop theorems, simplifier sets or classical reasoner sets at the goal. The I button allows proof by assumption (this is relevant only for goal in the theory HOL1). With the three-square button, you can select alternative unifiers for a resolution step. The "H" button shows the proof history, and the left and right arrow button allow you to move back and forth within the proof history.
Finishing a proof: Within the state menu of the goal window, chose the bullet button to leave an unfinished proof, or the square button to turn a proven goal into a theorem.
Induction proofs: You can do an induction proof by resolving the current goal with an axiom named "_generated,s", where s is a sort that is generated by some operations. Use the three-square button to look for the correct match, i.e. for the induction over the variable or subterm that you have in mind.