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

Hi Andreas,

using the function package, I'd like to define a function whosedefinition contains a number of Let expressions. In the generatedinduction rule, a term "Let t (%x. y)" yields the induction hypothesis"!!x. x = t ==> P (y x)"However, I would like to get "P (y t)" directly. How do I have to changethe congruence rule for Let to achieve this?I tried two alternatives with fundef_cong: - "[| M = N; f N = g N |] ==> Let M f = Let N g" raises an exception: *** exception THM 1 raised (line 421 of "drule.ML"): COMP *** At command "function".- "[| M = N; f M = g N |] ==> Let M f = Let N g" eliminates thequantifier, but produces far to many induction hypotheses.What is the right congruence rule for this?

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

Jeremy Dawson wrote:

This seems easy enough using the functions in ch 5 of the Reference Manual val iax = "!!x. x = t ==> P (y x)" : Thm.thmval ax' = forall_elim_var 0 iax ;val ax' = "?x = t ==> P (y ?x)" : Thm.thmrefl RS ax' ;val it = "P (y t)" : Thm.thm

Alex

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

**Re: [isabelle] Congruence rule for Let***From:*Jeremy Dawson

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

- Previous by Date: Re: [isabelle] problem with class and sulocale declarations
- 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