*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Congruence rule for Let*From*: Jeremy Dawson <jlcaadawson at netspeed.com.au>*Date*: Fri, 10 Sep 2010 10:25:24 +1000*In-reply-to*: <4C87430E.5020801@in.tum.de>*References*: <4C865771.6010505@kit.edu> <4C87430E.5020801@in.tum.de>*Reply-to*: jeremy at rsise.anu.edu.au*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.2.8) Gecko/20100806 Fedora/3.1.2-1.fc13 Thunderbird/3.1.2

On 09/08/2010 06:02 PM, Alexander Krauss wrote:

Jeremy Dawson wrote:This seems easy enough using the functions in ch 5 of the ReferenceManualval 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.thmThe ind.hyp. Andreas is referring to appears nested inside theinduction rule, where it cannot be easily manipulated by hand...Alex

val th = "(!!x. x = t ==> ?P (?y x)) ==> ?Q" : Thm.thm > val th' = rule_by_tactic (hyp_subst_tac 1) th ; val th' = "(!!x. ?P (?y t)) ==> ?Q" : Thm.thm Regards, Jeremy

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

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

- Previous by Date: [isabelle] MetiTarski 1.6 released!
- Next by Date: [isabelle] Unicode (Was: Update on I3P)
- Previous by Thread: Re: [isabelle] Congruence rule for Let
- Next by Thread: [isabelle] problem with class and sulocale declarations
- 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