image.png
Hi, i am very new to isabelle. I write a theory "MyAdd.thy". it work well until line 27. no error messages. I am confused where it go wrong.
Maybe don’t post screenshots but rather actual code as text, so that others can load it into their IDEs and experiment with it.
It looks like that line is simply processing without ever completing. That typically means that the automation is going haywire one way or another. In your case the simplifier is looping, i.e. the simp
rules you added (plus the ones that are declared as simp
rules by default) are creating an infinite rewrite loop.
The simplifier does not really have any mechanisms to detect such infinite rewrite cycles except for some very simple obvious cases, both because of performance reasons and because the problem is, in general, undecidable. It takes some experience to figure out what a good simp
rule looks like and what direction is the best one (remember: simp
rules get applied left-to-right only). So as a beginner, it is perhaps a good idea not to be a bit conservative about declaring simp
rules and rather add them locally as needed (simp add: foo
, auto simp: foo
, etc). And if you ever have a rewrite loop like this, try removing simp
rules one by one until there is no infinite loop anymore to understand what causes it.
In your case, the defining equations of your add
function are theorems called add.simps
, and the second of these states add (Suc m) n = Suc (add m n)
. Moreover, the .simps
rules generated by the function package are declared as simp
rules by default. Your add_1
rule is the exact opposite of that equation, so it is not surprising that you get a cycle.
There are a few rules of thumb in figuring out what is and what isn't a good simp
rule. The rule should be as simple and general as possible, the right-hand side should ideally be "simpler" in some sense than the left-hand side (although it is not always obvious what that means) and it should not cause infinite loops in combination with existing simp rules.
Also, relevant for your use case, it is generally a good idea to move datatype constructors as far outside as possible. That is, you should have theorems that relate your add
function to the constructors of your nat
datatype, and they should be oriented in such a way that the constructors are moved as far outside as possible. For example: add (Suc m) n = Suc (add m n)
, add m (Suc n) = add m (Suc n)
, add 0 n = n
, add m 0 = m
. Half of these are defining equations of add
anyway, so they are for free, but the other two you have to prove yourself. If you don't have one of these rules, the simplifier is likely to get "stuck" in some proofs.
Last updated: Jan 05 2025 at 20:18 UTC