From: Jim Kingdon <address@hidden>
To: address@hidden
Sent: Wednesday, October 3, 2012 5:29 PM
Subject: [Isarmathlib-devel] how to get started?
Here are my instructions for how to get going with writing proofs using isarmathlib. I'm stuck at step 4, where I try to switch from proofs built on Isabelle's ZF, to proofs built on isarmathlib. Do I need to import the heap that I built in "isabelle make"? Do I need to somehow load the isarmathlib .thy files? Is there some other problem?
Every time I've vowed to try proving some theorems with Isarmathlib, I've hit a bit of a "what do I do next?" wall. Here's what I did.
1. Install Isabelle as described <a href=""https://slawekk.wordpress.com/2012/09/17/installing-isabelle/" target="_blank">https://slawekk.wordpress.com/2012/09/17/installing-isabelle/">here</a>. At the end of this step, run <code>isabelle jedit</code> and see if it brings up a window.
2. Install Isarmathlib as described on the isarmathlib web site. The "isabelle make" step will write files in a subdirectory of where you
installed isabelle (for example, the <code>heaps/polyml-5.4.1_x86_64-linux</code> directory).
3. Go back to the jedit window, and type the following into the "Scratch" pane:
theory Scratch imports Arith
begin
lemma pred_pred_succ_succ_eq [simp]: "pred(pred(succ(succ(y)))) = y"
by (unfold pred_def, auto)
end
The lack of squiggly red underlines means that it passed. Try removing one of the "pred" (while leaving everything else alone). Note the squiggly red underlines. Congratulations, this is your first proof. Here we are just using the ZF theory that ships with Isabelle; we haven't used anything from IsarMathLib yet.
4. Change Arith to AbelianGroup_ZF. Mousing over the squiggly red underline shows "bad theory (file . . . AbelianGroup_ZF.thy)".
_______________________________________________
Isarmathlib-devel mailing list
address@hiddenhttps://lists.nongnu.org/mailman/listinfo/isarmathlib-devel