Lucas-Interpretation on Isabelle's Functions
This work addresses the problem of integrating sophisticated reasoning tools into educational software for students, but it is incremental as it focuses on migrating an existing prototype to a new system component.
The paper tackles the challenge of making automated reasoning tools accessible for mathematics education by adapting Lucas-Interpretation to Isabelle's function package, resulting in a straightforward migration and prototype code available for reuse.
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.