Does anybody know how to use Isabelle (the theorem prover)?

Factual Questions
1

Hi,
I’m trying to prove some relational theorems in the latest version of Isabelle, using ProofGeneral. I have two inductively defined sets, plus, defined like so:



  consts
    plus :: "(nat * nat * nat) set"
  inductive plus
    intros
      zero[intro!]: "(0, y, y) \<in> plus"
      addition[intro!]: "z = x + y ==> (x, y, z) \<in> plus"

  consts
    succ :: "(nat * nat) set"
  inductive succ
    intros
      addition[intro!]: "y = x + 1 ==> (x, y) \<in> succ"

Now, I’m trying to prove that (x + y) + z = x + (y + z) in relational form. To do this, I’m inducting on x. It would really help me if in the inductive conclusion, instead of having something like (Suc x, y, z) &lt;in> plus, I had &lt;exists>x’.succ(x, x’) /\ plus(x’, y, z) &lt;in> plus.

I’ve proven in a seperate lemma marked with [simp] that plus(Suc x, y, z) = &lt;exists>x’. succ(x, x’) /\ plus(x’, y, z). However, when I try to simplify the inductive conclusion using simp only: name_of_lemma I get an “empty” error.

What am I doing wrong?

Thanks.

2

Aw crap.

This:

Should read:

Now, I’m trying to prove that (x + y) + z = x + (y + z) in relational form. To do this, I’m inducting on x. It would really help me if in the inductive conclusion, instead of having something like (Suc x, y, z) &lt;in> plus, I had &lt;exists>x’. (x, x’) &lt;in> succ /\ (x’, y, z) &lt;in> plus.

i.e. I want to stop Isabelle inserting its own Suc x term into my formula in the step case and instead use my Prolog style succ relation. Is this possible?

Thanks.