Introduction

This Isabelle tutorial will cover the following topics.

• Isabelle basics
• First order term rewriting in Isabelle
• Formalization: "A looping TRS is nonterminating"
• Formalization: "A sound matching algorithm"
• Formalization: "A certifier for nontermination"

See also the short intro on slides. For each topic we will develop parts of the Isabelle theories live during the lectures, other parts will be provided as exercises where solutions will be made available shortly afterwards. The relevant Isabelle theories will be made available on this website and there will be regular updates.

Preparation

In order to prepare for the course, each participant should install Isabelle and run it at least once.

1. Download Isabelle 2016-1 and install it.
2. Download a simple test theory and open it in Isabelle. The first start of Isabelle might take a while since it will start to compile the Isabelle theories for higher-order logic. The behavior of Isabelle should correspond to the following screenshot where in particular the quantifiers and the implications have nice symbols, and where the last proof is marked in red, indicating a non-accepted proof.
   
3. Download the Archive of formal proofs. We will explain how to import this large collection of Isabelle formalizations within the course.

Isabelle theories

This archive contains the theory files related to this course.

• Basics.thy
• Term.thy (Demo, Exercises, Complete)
• Trs.thy (Demo, Exercises, Complete)
• Matching.thy (Demo, Complete, and for completeness Matching_Completeness.thy)
• Loops.thy (Demo, Exercises, Complete)
  • looping TRSs are nonterminating
• Loop_Checker_1/2/3.thy: function to check whether derivation is loop
  • 1: basic version without error message
  • 2: static error messages
  • 3: dynamic error messages
• Nontermination_Checker_1/2/3.thy
  • extended checker for nontermination which also contains rule removal: in order to prove nontermination of R it suffices to prove nontermination of R - S
  • Variants 1/2/3 as in Loop_Checker_1/2/3
  • Exercise: implement Nontermination_Checker_i.thy completely on your own
    • prove that rule removal is sound for nontermination
    • write a check-function to test whether rule removal is applied correctly
    • combine the checker for rule-removal and the checker for loops into some recursive nontermination-checker
• Final_Nontermination_Checker.thy: includes XML-parser
• examples/loop.*: example XML-nontermination proof + schema
• Code/Main.hs: wrapper to invoke Isabelle-generated code from Final_Nontermination_Checker.thy

Last update: 2017-07-07, 12:05

Contact

• Christian Sternagel
• René Thiemann