Bachelor Thesis

Rewriting with conditional equations is one of the most important proof methods in Isabelle. When rewriting deep inside a term, we could use the knowledge about where we rewrite to discharge the conditions (e.g., if we rewrite in the left branch of an if expression, we can assume that the condition is true). This knowledge can be collected by using so-called congruence rules.

In Isabelle, conditional equations can be applied with the rewrite proof method. With the use of patterns, the user can specify where in the term the equation should be applied.

The goal of this bachelor thesis is to figure out how to properly combine patterns and congruence rules and implement this in Isabelle's rewrite method.

Programming language:
Standard ML
Prerequisites:
Familiarity with ML; English
Supervisor:
Johannes Hölzl, Raum FMI 01.11.060, email {hoelzl} AT [in.tum.de]
Professor:
Prof. Tobias Nipkow, Raum MI 01.11.058, email {nipkow} AT [in.tum.de]