Re: [isabelle] Congruence rule for Let



Hi Alex,

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?
Inlining might increase the size of the induction rule exponentially, so it definitely is not optimal in all cases, i.e. you want to include an option to deactivate this. In my cases, this increase does not happend in the induction rule because contains fewer occurrences of the let-bound variable than the defining equations. If postprocessing is needed anyway, I would recommend to provide an attribute which perform this. Then, it might also be available for other rules (e.g. the .cases rule for (co)inductive predicates/sets).

Since the function package does not generate sensible case names for the induction rule (even without the sequential and every equation being given a name), I have to do some postprocessing with attributes anyway, so I would not mind adding an explicit postprocessing attribute there. Unfortunately, inside a local context, IIRC, such an attribute would be reexecuted whenever the context is opened.

Thanks for looking into this,
Andreas





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