Adam Dingle (Mar 29 2026 at 10:14): Adam Dingle (Mar 29 2026 at 10:14):As I mentioned earlier, as an exercise I've made my own definition of the natural numbers and am attempting to prove some theorems about them.
I'm trying to prove by contradiction that ¬(x < x) for all x : ℕ. I've gotten this far:
definition less :: "natt ⇒ natt ⇒ bool" (infix "<" 50) where
"x < y = (∃z. x + z = y)"
theorem thm_4_1_a: "¬(x < x)"
proof -
assume "x < x"
then obtain z where eq: "x + z = x" using less_def by auto
have "x ≠ x + z" using thm_3_6 add_sym by auto
hence False using eq by auto
I've proven False, so the proof should be done. However, if I change "hence" to "thus" (= "then show"), Isabelle reports
Local statement fails to refine any pending goal
So I seem to be stuck. What am I doing wrong?
I'll attach my entire source file in case that is helpful:
arith.thy
Adam Dingle (Mar 29 2026 at 10:20):By trial and error I figured out the solution: I needed just "proof" instead of "proof -".
However, I don't completely understand this - I thought those had the same meaning.
Adam Dingle (Mar 29 2026 at 10:24):OK, I did some more reading in the reference manual and realized that "proof" and "proof -" are not the same. Apparently "proof -" does no refinement at all. "proof" is equivalent to "proof standard". According to the manual:
standard refers to the default refinement step of some Isar language elements (notably proof and “..”). It is dynamically scoped, so the behaviour depends on the application environment.
In Isabelle/Pure, standard performs elementary introduction / elimination steps (rule), introduction of type classes (intro_classes) and locales (intro_locales).
In Isabelle/HOL, standard also takes classical rules into account.
Notification Bot (Mar 29 2026 at 10:24):Adam Dingle has marked this topic as resolved.
Last updated: Apr 14 2026 at 09:21 UTC