*To*: Stephan van Staden <Stephan.vanStaden at inf.ethz.ch>*Subject*: Re: [isabelle] Introduction rule for quantifiers over sets of pairs*From*: Tjark Weber <webertj at in.tum.de>*Date*: Fri, 16 Nov 2012 14:59:50 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50A63C1B.6010501@inf.ethz.ch>*References*: <50A63C1B.6010501@inf.ethz.ch>

Hi Stephan, On Fri, 2012-11-16 at 14:14 +0100, Stephan van Staden wrote: > This one should be simple. I'm looking for the name of the rule that > will do the job of RRR below: > > lemma "\<forall> (a,b) \<in> S. P" > proof (rule RRR) > fix a b > assume "(a,b) \<in> S" > show "P" sorry > qed clarify may do more than you want if S or P are compound terms. Here is another solution: lemma RRR: assumes "⋀a b. (a,b) ∈ S ⟹ P" shows "∀ (a,b) ∈ S. P" by (metis assms splitI2) Best regards, Tjark

**References**:**[isabelle] Introduction rule for quantifiers over sets of pairs***From:*Stephan van Staden

- Previous by Date: Re: [isabelle] isabelle mailing lists
- Next by Date: Re: [isabelle] Introduction rule for quantifiers over sets of pairs
- Previous by Thread: Re: [isabelle] Introduction rule for quantifiers over sets of pairs
- Next by Thread: Re: [isabelle] isabelle mailing lists
- Cl-isabelle-users November 2012 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