*To*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Subject*: Re: [isabelle] Congruence rule for Let*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Tue, 14 Sep 2010 16:40:21 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4C874698.1040507@kit.edu>*References*: <4C865771.6010505@kit.edu> <4C87430E.5020801@in.tum.de> <4C874698.1040507@kit.edu>*User-agent*: Mozilla-Thunderbird 2.0.0.22 (X11/20091109)

Hi Andreas,

Actually, I had expected that the first rule works. I need to dig intothis 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 manyinduction hypotheses.

Alex

**Follow-Ups**:**Re: [isabelle] Congruence rule for Let***From:*Andreas Lochbihler

**References**:**[isabelle] Congruence rule for Let***From:*Andreas Lochbihler

**Re: [isabelle] Congruence rule for Let***From:*Alexander Krauss

**Re: [isabelle] Congruence rule for Let***From:*Andreas Lochbihler

- Previous by Date: [isabelle] Proof Pearl: Regular Expression Equivalence and Relation Algebra
- Next by Date: Re: [isabelle] Congruence rule for Let
- Previous by Thread: Re: [isabelle] Congruence rule for Let
- Next by Thread: Re: [isabelle] Congruence rule for Let
- Cl-isabelle-users September 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list