CODEWITHSUNDEEP
isabelle
Teharez
Teharez

Reputation: 603

Isabelle does not evaluate lemma

I'm reading the introduction "Programming and Provin in Isabelle/HOL" and try to do the exercise 2.2.

Currently I have the following:

theory Scratch
  imports Main
begin

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

lemma add_02 [simp]: "add m 0 = m"
  apply(induction m)
  apply(auto)
  done

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

lemma commutativity [simp]: "add n m = add m n"
  apply(induction n)
  apply(auto)
  done

lemma add1 [simp]: "Suc m = add m (Suc 0)"
  apply(induction m)
  apply(auto)
  done
  
lemma add1_commutativ [simp]: "add n (Suc m) = add m (Suc n) "
  apply(induction n)
  apply(auto)
  done

lemma associativity [simp]: "add n (add m t) = add (add n m) t"
  apply(induction n)
  apply(auto)
  done

end

In lemma add1_commutativ the apply(auto) has a red background color and the following keywords apply and done are all blue instead of the standard red.

Isabelle Editor

I do not get any error message. Neither when I hover hover it nor in the output console.

What am I doing wrong?

Upvotes: 1

Views: 95

Answers (1)

Peter Zeller
Peter Zeller

Reputation: 2276

The red background indicates that the line is currently being processed. It looks like the simplifier ran into an endless loop because of the add1 lemma. You can see this if you repeatedly apply the lemma manually using apply (subst add1):

Step 1. add 0 (Suc m) = add m (Suc 0)

Step 2. add 0 (add m (Suc 0)) = add m (Suc 0)

Step 3. add 0 (add m (add 0 (Suc 0))) = add m (Suc 0)

...

As you see, the term becomes bigger in every step and this process will never terminate.

In general you should try to write equations such that the right side is smaller than the left side, since the simplifier will use equations to rewrite terms from left to right.

So for your example you could change lemma add1 to add m (Suc 0) = Suc m and the proof will succeed.

Upvotes: 1

Related Questions