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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
