[Isarmathlib-devel] how to get started?

[Jim Kingdon]

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/";>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)".