Goals of the Exercises

This page is intended to give you an idea of what you should have learned from the exercises. Please be sure to check all the goals and spend additional time on the exercises if you do not meet them yet.

The exercise meetings are intended to give you time to solve the exercises under supervision and often also introduce new things. You should at least prepare the exercises which are marked accordingly and send in the solutions. Eventually, you should be able to solve all the exercises and you should spend as much additional time at home as you need to finish them. You are encouraged to ask questions either in person or per email at any point in time.

• Get familiar with the calculi, axioms, rules and what a proof is.
• Be able to do pen and paper proofs.
• Be able to translate your proofs to Isabelle/HOL, using a fixed pattern.
• Make first steps with the tool/editor Isabelle/HOL/Emacs.

• Be able to write basic Isabelle/HOL functions and recursive functions.
• Get familiar with functional programs, so you can at least read more complex programs.

• Be able to specify properties of functions in Isabelle/HOL.
• Be able to prove many of these properties with a simple proof pattern.
• First steps in finding missing lemmas from proofs which are not working yet.

• More advanced example.
• Be able to define the algorithm and specify its correctness.
• Doing the proof at this point can be challenging.
  • It highly depends on your definitions and your knowledge of the proof system.
  • You should be able to do it at the end of the semester the latest.

• Be able to define datatypes in Isabelle/HOL.
• Be able to define primitive recursive functions on datatypes.
• Be able to specify properties on such functions.
• Be able to prove many of these properties with a simple proof pattern.
• Next steps in finding missing lemmas from proofs which are not working yet.

• Get used to the idea of using existing types to define new ones.
• Get used to the idea that sets and predicates are pretty much equivalent.

• More exercise in writing, understanding and modifying functional programs and datatypes.
• Get familiar with proofs, proof commands and proof states in a very simple setting.
• In general, understand how provers work and how one could implement one.

• Basic theory questions you should be able to answer about the HOL core, universes, models, conservative extensions, etc.
• Exercise 2 (d/e) More and more advanced questions where you can get more familiar with using Isabelle/HOL, proofs, finding and applying theorems, etc.

• Be able to apply methods to rules and do proofs.
• Get to know the different methods.
• Get to know more and more rules.
• Be able to do arbitrary proofs on propositional and predicate logic theorems.

• Get familiar with designing and defining both syntax and semantics of languages.
• First steps towards formulating and proving properties relating models, in this case two language semantics and a compiler.

• First steps in finding needed theorems from the library, using the Find Theorems function.
• First steps in using different induction schemes.
• First case study about specifying models, properties and proving their consistency.

• Two more complex case studies for specifying models, properties and proving their consistency.
• Be able to define advanced models.
• Be able to specify properties for such models.
• Be able to prove those properties with regard to the models.

• Understand and proof properties on paper about lattices and fixpoints.
• Be able to specify inductive sets on paper and understand their semantics.

• Get familiar with LTL.
• Be able to specify properties about transition systems in LTL.
• Be able to do proofs of LTL properties, using the semantics.
• Get to know one possible definition of traces and transition systems and how to use it for proofs.
• First steps in defining a calculus for an embedded logic in Isabelle/HOL and using the calculus to do proofs.
• Learn how the specification affects proofs and how changes in the specification can help the proofs.

• Understand the difference between different styles of semantics.
• Be able to prove properties about language semantics.
• Be able to do induction over inductive sets / predicates.

• Be able to do pen & paper proofs using the Hoare calculus.
• Be able to find simple loop invariants.
• Be able to translate proofs into the framework created in the lecture.