Re: [isabelle] Congruence rule for Let



Hi Andreas,

Actually, I had expected that the first rule works. I need to dig into this again. The rule that should definitely work is the following

  "f M = g N ==> Let M f = Let N g"

It has the same effect on the induction rule as unfolding all lets. Can you try if it works for your function?
No, it doesn't. This produces the same effect like the congruence rule "[| M = N; f M = g N |] ==> Let M f = Let N g", it produces too many induction hypotheses.

After playing the complete example that you provided off-list, I think I now understood the problem.

The let binding itself contains recursive calls. Using the above congruence rule is equivalent to inlining all lets for the purpose of the analysis. This automatically duplicates recursive calls, if the let-bound variable occurs more than once. I think there is no way to avoid this using congruence rules.

The transformation you would like to see could in fact be done as a post-processing step on the induction rule. Would you (and other users) think it is a good idea to inline assumptions of the form "x = t" in general?

Alex





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.