JFu (Dec 29 2023 at 13:39): JFu (Dec 29 2023 at 13:39):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.
Wolfgang Jeltsch (Dec 29 2023 at 16:23):Maybe don’t post screenshots but rather actual code as text, so that others can load it into their IDEs and experiment with it.
Manuel Eberl (Dec 30 2023 at 10:08):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: Apr 27 2024 at 20:14 UTC