Adam Dingle (Mar 28 2026 at 11:55): Adam Dingle (Mar 28 2026 at 11:55):As an exercise, I defined my own natural number type and addition function:
no_notation plus (infixl "+" 65)
datatype natt = One | S natt
fun add :: "natt ⇒ natt ⇒ natt" (infixl "+" 65) where
"add x One = S x" |
"add x (S y) = S (x + y)"
I proved inductively that x + One = One + x for all x:
lemma thm_3_3: "x + One = One + x" (is "?P x")
proof (induction x)
show "?P One" by auto
next
fix x assume "?P x"
have "S x + One = (x + One) + One" by auto
also have "... = (One + x) + One" by (auto cong add: ‹?P x›)
also have "... = One + (x + One)" by auto
also have "... = One + S x" by auto
finally show "?P (S x)" .
qed
In the first "also have" line above, I tried "auto simp add: ‹?P x›" but it failed. I don't understand why. I thought that would cause auto to use "x + One = One + x" as a simplification rule, i.e. replace "x + One" with "One + x" which would prove the step immediately. Randomly I tried "auto cong add" instead and it worked, but I don't really understand why since my understanding is that "cong" is intended for more general congruence rules, as explained e.g. in section 9.1.1 "Advanced Features" of the "Isabelle-HOL: A Proof Assistant" book.
Did I really need to use "auto cong add" here? Is there some easier/nicer way to prove the step?
Mathias Fleury (Mar 28 2026 at 12:39): also have "... = (One + x) + One"
supply [[simp_trace_new]] by (simp flip: ‹?P x›)
But the answer is boring: look at the trace of the simplifier with simp add and simp flip
Mathias Fleury (Mar 28 2026 at 12:42):but the real real answer to the question is not why it fails, but that you lemma is written the wrong way around
Mathias Fleury (Mar 28 2026 at 12:42):the left trivially simplifies to S x
Mathias Fleury (Mar 28 2026 at 12:42):and you absolutely should not rewrite anything away from that normalized form
Last updated: Apr 14 2026 at 09:21 UTC