# 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.*