Theorem Proving in Isabelle

ECEN 5013, Spring 2011

Location: ECCE 1B47. (In the Civil Engineering Wing of the Engineering Center, see this map).

Have you ever wanted or needed to prove a property about a formal system but did not know where to start or what techniques to use? Have you ever had trouble sleeping, worrying whether you made a mistake in a paper you just submitted to a conference? If so then this course is for you. The course is a hands-on introduction to theorem proving using the Isabelle proof assistant. The course will cover reasoning about inductive datatypes, recursive functions, and sets using higher-order logic (HOL). The course will cover common proof techniques including a cornucopia of induction methods. Last but not least, this course will cover practical issues such as how to ``debug'' your proofs, techniques for structuring large proofs, how to make the best use of Isabelle's decision procedures, and how to get Isabelle to typeset your definitions and proofs in LaTeX. The course has no explicit prerequisites, but a basic understanding of logic is helpful, as is some exposure to functional programming.

Students should bring a laptop computer to class and have a working installation of Isabelle 2009-2 (see below). 

Grading

Course grades will be based on weekly homework assignments (70%) and a final project (30%).

Textbook

Isabelle/HOL: A Proof Assistant for Higher-Order Logic, June 21, 2010 edition. PDF

Isabelle Resources

The main web page for Isabelle is here: http://isabelle.in.tum.de/index.html. From there you can find the software download page. There are versions of Isabelle available for Linux, MacOS X, and Windows.

Homework

  1. Exercise 2.5.1 (mirror and flatten on binary trees), due Wednesday, Jan. 19.
  2. Exercise 2.5.2 (normalizing Boolean expressions), due Wednesday, Jan. 26.
  3. Compiling Let Expressions, due Wednesday, Feb. 2. See CompilingLets.thy.
  4. Exercises 5.4.1, 5.9.1, and add a theorem to the Binary Search Tree theory that proves that the lookup function finds the element if and only if the in_tree function finds the element. Due Wednesday, Feb. 9.
  5. Leftist Heaps, due Wednesday, Feb. 16. See Heap.thy and for further explanation, google "leftist heap".
  6. Strong Connectivity is an equivalence relation, due Wednesday, Feb. 23. See Graphs.thy.
  7. Proof of type safety for a variant of the simply-typed lambda calculus, due Wednesday, March 9. See STLC.thy.
  8. Preliminary project proposal (definitions and theorem statements), due Wednesday, March 16.

Reading

  1. Chapter 1 and 2. By Jan. 19.
  2. Chapter 3. By Jan. 28.
  3. Chapter 5 and A Tutorial Introduction to Structured Isar Proofs. By Feb. 11.
  4. Chapter 6. By Feb. 18.
  5. Chapter 7. By Feb. 25.

Isabelle Files from Lecture

  1. Definition and properties of f^n: ComposeNInClass.thy.
  2. Binary Search Trees: BSTInClass.thy.
  3. Flatten in Accumulator Passing Style: Ex3_2_2.thy.
  4. Negation Normal Form: NNFInClass.thy.
  5. Compiling Expressions: CompilingInClass.thy.
  6. Function Package and a Little Isar FibInClass.thy.
  7. Rules of Logic RulesOfTheGameInClass.thy.
  8. Rules of Logic, Part 2 RulesOfTheGame2InClass.thy.
  9. Homework solution BSTHW.thy and correctness of GCD GCDInClass.thy.
  10. Finite State Machines FSMInClass.thy.
  11. Leftist Heap Solution HeapHW.thy.
  12. Graph Solution GraphsHW.thy.
  13. A language of typed arithmetic TypedArithInClass.thy (taken from chapters 3 and 8 of the text Types and Programming Languages).
  14. Type Safety for the Simply Typed Lambda calculus STLC.thy and STLCHW.thy
  15. Metatheory of Propositional Logic PropLogicND.thy
  16. Separation Logic, in progress SepLogic.thy

Course Email Group

The google group for this course is at http://groups.google.com/group/theorem-proving-spring-2011. Please sign up immediately. The email address for the group is theorem-proving-spring-2011@googlegroups.com.

Some Notes

The following works through an example use of the Lookup inference rule in separation logic. We make the following abbreviations. \begin{align*} A & \equiv i \mapsto a \\ B & \equiv i+1 \mapsto j \\ L & \equiv \mathit{list} \, \alpha \, (j,k) \end{align*} We want to show that \[ \{ A * (\exists j. B * L) \}\; \mathsf{j := [i+1]} \;\{ A * B * L \} \] Using the Lookup (backwards reasoning) rule we have \[ \{ \exists j. B * (B {-\!*} (B * L)) \}\; \mathsf{j := [i+1]} \;\{ B * L \} \] If we can show that \((\exists j. B * L) \Rightarrow (\exists j. B * (B {-\!*} (B * L)))\), then we can use the rule of consequence to get \[ \{ \exists j. B * L \}\; \mathsf{j := [i+1]} \;\{ B * L \} \] and then the frame rule to obtain our conclusion \[ \{ A * (\exists j. B * L) \}\; \mathsf{j := [i+1]} \;\{ A * B * L \}. \] So it remains to show that \[ (\exists j. B * L) \Rightarrow (\exists j. B * (B {-\!*} (B * L))). \] It suffices to show \[ B * L \Rightarrow B * (B {-\!*} (B * L)) \] and in turn, it suffices to show \[ L \Rightarrow (B {-\!*} (B * L)). \] So it suffices to show \[ L * B \Rightarrow B * L \] which is true by the commutativity of separating conjunction.