*To*: Lars Noschinski <noschinl at in.tum.de>*Subject*: Re: [isabelle] Basic question about apply-style reasoning*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Tue, 03 May 2011 20:59:56 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4DC00B84.7050005@in.tum.de>*References*: <4DBFFF78.9030509@uni-muenster.de> <4DC0060A.2030500@in.tum.de> <4DC00A1F.8060405@uni-muenster.de> <4DC00B84.7050005@in.tum.de>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.16) Gecko/20101125 SUSE/3.0.11 Thunderbird/3.0.11

>> apply (subst arg_cong2[where f=I]) by auto >> does the job, but introduces some odd-looking schematic variables in >> between. > > In your case, this rule is more suitable as an introduction rule, i.e. > > by (rule arg_cong2[where f=I]) auto > This does not work. thm arg_cong2[where f=I] yields [|?a = ?b; ?c = ?d|] ==> I ?a ?c = I ?b ?d and the conclusion of this rule (topmost operator is =) does not unify with "I a' b'", so you cannot use it as introduction rule. Indeed, apply (rule arg_cong2[where f=I]) fails. However, a (lengthy) apply (erule rev_iffD2[OF _ arg_cong2[where f=I]]) does the job, and yields a'=a &&& b'=b I have defined a shortcut for rev_iffD2[OF _ arg_cong2], and use this. Best and thanks again, Peter

**Follow-Ups**:**Re: [isabelle] Basic question about apply-style reasoning***From:*Jeremy Dawson

**References**:**[isabelle] Basic question about apply-style reasoning***From:*Peter Lammich

**Re: [isabelle] Basic question about apply-style reasoning***From:*Lars Noschinski

**Re: [isabelle] Basic question about apply-style reasoning***From:*Peter Lammich

**Re: [isabelle] Basic question about apply-style reasoning***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] Basic question about apply-style reasoning
- Next by Date: Re: [isabelle] where to post jedit 4.3.2 bugs/feature requests?
- Previous by Thread: Re: [isabelle] Basic question about apply-style reasoning
- Next by Thread: Re: [isabelle] Basic question about apply-style reasoning
- Cl-isabelle-users May 2011 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