Double function in Isabelle

Question

I try to learn Isabelle/HOL by working through this tutorial. I have a problem with the exercise about the double function. I defined it like this:

fun double :: "nat ⇒ nat" where 
"double 0 = add 0 0" |
"double (Suc m) = Suc(Suc (double m))"

But when trying to prove that double m = add m m in my theorem:

theorem add_d [simp] : "double x = add x x"
apply(induction x)
apply(auto)
done

apply(auto) never gets evaluated (it's background is pink(?)). The same exercise asks to prove the commutativity and associativity of add and this worked ok. I am using Isabelle2014 with the default (Jedit) IDE.

Answer 1

In the code from your comment many theorems have [simp] attribute that tells Isabelle to add them to the simpset. However some of them are not suitable as a rewriting rule (used by simp and by auto), because they lead to a term to which the same rule can be applied again, causing an infinite loop. Removing the offending theorem from the simpset does the trick:

theorem add_d: "double x = add x x"
  apply (induction x)
  apply (auto simp del: add_zero)
done

But a better solution is to avoid adding such theorems to the simpset in the first place, e.g. to remove [simp] attribute from their declaration:

lemma add_zero: "add x 0 = add 0 x"
  apply (induction x)
  apply (auto)
done

After that add_d does not need the simp del part. But some other theorems may need to be explicitly told to use this particular rule, e.g. this one:

theorem add_com: "add x y = add y x"
  apply (induction x)
  apply (auto simp add: add_zero)
done

Note that, compared to your code, the [simp] attribute is dropped again to avoid circular rewriting if add_com is used elsewhere.

Answer 2

While Alexander's advice about simp-rules is sound, let me give some further comments.

Firstly, in your definition of double, I would replace add 0 0 by 0. As a general advice: prefer simple expressions over complex ones.

Secondly, Isabelle's simplifier is actually "smart" enough to handle rewriting with AC (i.e., associativity and commutativity) without looping, i.e., your two lemmas

lemma add_assoc [simp]:
  "add (add x y) z = add x (add y z)"

and

lemma add_commute [simp]:
  "add x y = add y x"

are fine as simp-rules (i.e., you can keep the [simp] attribute). The cause of the loop you are experiencing is your lemma

(*BAD*)
lemma add_zero [simp]:
  "add x 0 = add 0 x"

Since having it in the simpset (Isabelle jargon for the set of all simplification rules that are used by methods like simp and auto) allows for the infinite derivation:

add 0 0 = add 0 0 = add 0 0 = ...

I would suggest to replace it by

lemma add_zero [simp]:
  "add x 0 = x"

Then all your proofs (provided they are stated in the correct order) should be "automatic" in the sense

apply (induction ...)
apply auto
done

which can be abbreviated to

by (induction ...) (auto)