isarmathlib-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Isarmathlib-devel] how to get started?


From: Jim Kingdon
Subject: [Isarmathlib-devel] how to get started?
Date: Wed, 03 Oct 2012 08:29:04 -0700
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:15.0) Gecko/20120912 Thunderbird/15.0.1

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




reply via email to

[Prev in Thread] Current Thread [Next in Thread]