I have the following two Isabelle definitions:
fun remove_left :: "cmd ⇒ cmd × cmd option" where
"remove_left (Comp c d) = (case remove_left c of
(head, Some c') ⇒ (head, Some (Comp c' d)) |
(head, None) ⇒ (head, Some d)
)" |
"remove_left c = (c, None)"
function pop_flatten :: "cmd ⇒ cmd" where
"pop_flatten c = (case remove_left c of
(h, Some c') ⇒ Comp h (pop_flatten c') |
(h, None) ⇒ h
)"
by pat_completeness auto
termination by(relation "measure size"; simp; metis remove_left_decreases)
(As an exercise I am proving that various versions of program flattening routines are equal.)
The simplifier seems unable to handle this. For example, when I try the following obviously false lemma:
lemma "pop_flatten c = Skip"
apply(simp)
The simplifier immediately goes into a loop. simp_trace shows it is continuously applying the definition of pop_flatten. My suspicion is that the case expression introduces the term c' which the simplifier considers to be completely new, so it unfolds the definition again. I am unsure how to work around this, I would like to not change my definition. I tried removing the simp rules for pop_flatten as follows:
declare pop_flatten.simps [simp del]
But now several proof steps which I would normally do by simp obviously don't work anymore. My definition of cmd is standard, just a skip, sequential composition, if and while. Is there indeed an edge case in the simplifier I am running into here, or is my definition just wrong in some way I am not seeing?
It's not particularly surprising that this leads to an infinite loop: The left-hand side of the pop_flatten.simps rules is immediately applicable to its right-hand side again, so you are almost guaranteed an infinite rewrite loop.
For that reason, if you do a recursive definitions with just a single equation that isn't guarded by a condition or a pattern match, it is best to immediately delete the .simps rule from the simp set (as you have done).
If you do want to apply it, you can either apply it once in a very targeted way using apply (subst pop_flatten.simps) or you can restrict it to the particular value you want to apply it to, e.g. apply (simp add: pop_flatten.simps[of c]).