*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Introduction rule for quantifiers over sets of pairs*From*: Stephan van Staden <Stephan.vanStaden at inf.ethz.ch>*Date*: Fri, 16 Nov 2012 15:26:58 +0100*Cc*: Stephan Merz <Stephan.Merz at loria.fr>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1211161514270.16259@macbroy21.informatik.tu-muenchen.de>*References*: <50A63C1B.6010501@inf.ethz.ch> <C826BDFF-0492-4A47-9C97-AAE2F1E07E76@loria.fr> <50A64103.4020108@inf.ethz.ch> <alpine.LNX.2.00.1211161514270.16259@macbroy21.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:16.0) Gecko/20121028 Thunderbird/16.0.2

Your solution works for me and is quite readable. Thanks for helping! Stephan On 11/16/2012 03:17 PM, Makarius wrote:

On Fri, 16 Nov 2012, Stephan van Staden wrote:Using allI twice (or with +) does not work for me, but clarify doesthe job perfectly. Thanks a lot!Putting automated tools like "clarify" or "auto" in the initial"proof" position is actually an anti-pattern of structured proofs.Sometimes it cannot be avoided, but it should not be done by default.Instead, the usual way is to make a bottom-up proof with automatedre-composition like this:notepad begin have "∀(a, b) ∈ S. P" proof - { fix a b assume "(a, b) ∈ S" have P sorry } then show ?thesis by auto -- "terminal auto, instead of initial clarify etc." qed endThis can also cause surprises sometimes, especially with too generaltypes for the body within { ... }, but it usually works in areasonably robust way, and does not depend on the details of whatautomation does.Makarius

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

**Re: [isabelle] Introduction rule for quantifiers over sets of pairs***From:*Stephan Merz

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

**Re: [isabelle] Introduction rule for quantifiers over sets of pairs***From:*Makarius

- Previous by Date: Re: [isabelle] Introduction rule for quantifiers over sets of pairs
- Next by Date: [isabelle] Composable induction invariants
- Previous by Thread: Re: [isabelle] Introduction rule for quantifiers over sets of pairs
- Next by Thread: Re: [isabelle] Introduction rule for quantifiers over sets of pairs
- 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