Lucas-Interpretation on Isabelle's Functions

TL;DR

This paper describes the adaptation of Lucas-Interpretation for Isabelle's functions, enabling reliable integration of automated reasoning tools into educational software for mathematics learning.

Contribution

It provides the first technical description of Lucas-Interpretation in Isabelle, demonstrating straightforward migration and adaptation to the proof assistant's function package.

Findings

Successful migration of Lucas-Interpretation to Isabelle's function package

Open-source code available for reuse and adaptation

Lessons learned from Isabelle's code structure development

Abstract

Software tools of Automated Reasoning are too sophisticated for general use in mathematics education and respective reasoning, while Lucas-Interpretation provides a general concept for integrating such tools into educational software with the purpose to reliably and flexibly check formal input of students. This paper gives the first technically concise description of Lucas-Interpretation at the occasion of migrating a prototype implementation to the function package of the proof assistant Isabelle. The description shows straightforward adaptations of Isabelle's programming language and shows, how simple migration of the interpreter was, since the design (before the function package has been introduced to Isabelle) recognised appropriateness of Isabelle's terms as middle end. The paper gives links into the code in an open repository as invitation to readers for re-using the prototyped code or adopt the general concept. And since the prototype has been designed before the function package was implemented, the paper is an opportunity for recording lessons learned from Isabelle's development of code structure.