[isabelle-dev] Feedback from a Isabelle tutorial

[Lukas Bulwahn]

Hello all,


this week, we, Johannes Hoelzl and me, gave a two-and-half-hour tutorial 
to Isabelle at a workshop meeting of PhD students in computer science in 
Dagstuhl (cf. http://www.model.in.tum.de/um/vernetzungstreffen/).


We used Isabelle/jEdit with some latest development snapshot and bundled 
this as a VirtualBox VM configuration.
Setting-up the system (installing VirtualBox, importing the VM 
configuation) in most cases took less than 10 minutes, which we assisted 
in the evening the day before the tutorial session.

We presented two basic examples, addition on natural number and reversal 
of lists, and let them work themselves with some guidance to prove one 
or two lemmas on their own.
In the end, Johannes presented a student exercise from a first-semester 
undergraduate analysis course and how he would solve that with Isabelle
to give the PhD students an idea what the system can do and how real 
proofs are developed and look like and not to leave the impression 
everything is proved by "induct auto/simp".

Overall, we got a positive feedback from many participants.
Working with the interaction model of Isabelle/jEdit seemed not to pose 
any problem for the students and we had no crash or unexpected behaviour 
with the current version.

I only noticed that using "try" you often get a misleading response from 
linarith that "linarith found a counterexample" which beginners might 
stumble on.
It might be better to switch off this warning by default (and offer a 
configuration to switch it on if it is of interest).



Lukas