*To*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Subject*: Re: [isabelle] Congruence rule for Let*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Wed, 08 Sep 2010 17:27:24 +1000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4C865771.6010505@kit.edu>*References*: <4C865771.6010505@kit.edu>*User-agent*: Thunderbird 2.0.0.24 (X11/20100317)

Andreas Lochbihler wrote:

Hi all,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 tochange the congruence rule for Let to achieve this?

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

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

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