CODEWITHSUNDEEP
debuggingisabelle
user1868607
user1868607

Reputation: 2610

Isabelle confused by a previous lemma?

I found something strange while doing exercise 2.5 of the Concrete Semantics book. Basically, we have to prove the famous Gauss formula for the sum n integers. Here is my code:

fun sum_upto :: "nat ⇒ nat" where
"sum_upto 0 = 0" |
"sum_upto (Suc n) = (Suc n) + (sum_upto n)"

lemma gauss: "sum_upto n = (n * (n + 1)) div 2"
apply(induction n)
apply(auto)
done

This won't proceed at least I remove a previous lemma from exercise 2.3:

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

lemma double_succ [simp]: "Suc (Suc (m)) = add m 2"
apply(induction m)
apply(auto)
done

lemma double_add: "double m = add m m"
apply(induction m)
apply(auto)
done

So here add is a user-defined function for addition. I've looked other solutions and my definition of double is substituted by Suc(Suc (double n)) in that case, the next lemma is unnecessary and the error in Gauss disappears.

However, I'm interested to know why is this happening because in principle both problems don't use any common structure.

Upvotes: 0

Views: 126

Answers (1)

larsrh
larsrh

Reputation: 2659

The [simp] is at fault here. Try removing it and see if that helps.

The underlying reason is that [simp] will add a rule to the so-called simpset and will be used by the simp, auto, etc. methods automatically. Great care needs to be taken before lemmas are declared as [simp] because of that.

In your case, the problem is that Suc (Suc m) = add m 2 is not a good rule for the simpset. It will replace all instances of Suc (Suc m) with add m 2, which is probably the opposite direction of what you want.

Upvotes: 1

Related Questions