*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] cases/induction on existential/free variables*From*: Chris Capel <pdf23ds at gmail.com>*Date*: Mon, 23 Feb 2009 21:40:18 -0600*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20090223063018.2eqe7sh77oow4swo@webmail.pdx.edu>*References*: <737b61f30902220923w6c0e9272k293a44de19616267@mail.gmail.com> <20090223063018.2eqe7sh77oow4swo@webmail.pdx.edu>

On Mon, Feb 23, 2009 at 08:30, Brian Huffman <brianh at cs.pdx.edu> wrote: > You have two alternatives: > > 1. Use Isar-style declarative proofs. When proving this subgoal, you can > "fix z", after which "z" can be referred to as a free variable. This is helpful. But apply scripts are so much easier to do than Isar when you don't know either well! > 2. Stay with apply-style proofs, but use "rule_tac". The "_tac" variations > of tactics *can* refer to meta-universal-bound variables within your > subgoal. For example, try > > apply (rule_tac x="Q z" in exI) And this is exactly what I was looking for. I'm curious--why the difference in behavior? The documentation seems cryptic on this point. I hadn't been aware of the difference between this and (rule_tac exI[of _ "Q z"]). On Mon, Feb 23, 2009 at 14:56, Tobias Nipkow <nipkow at in.tum.de> wrote: > If you want to rewrite "EX (x :: dt). P x" into some other form, you can > do it explicitly by stating the subgoal "(EX (x :: dt). P x) = ...", > which you prove in the usual way (you may need extensionality here, rule > "ext"). Ah, yes. I think I accomplished what you speak of here using subgoal_tac followed by assumption, without needing extensionality. This disadvantage from rule_tac being that I have to state my entire Q again, which is quite large. However, with Isar I can use the "is" keyword and it's not a problem. Thank you all, Chris Capel -- "What is it like to be a bat? What is it like to bat a bee? What is it like to be a bee being batted? What is it like to be a batted bee?" -- The Mind's I (Hofstadter, Dennet)

**References**:**[isabelle] cases/induction on existential/free variables***From:*Chris Capel

**Re: [isabelle] cases/induction on existential/free variables***From:*Brian Huffman

- Previous by Date: [isabelle] apply (rule exI) diverging
- Next by Date: Re: [isabelle] apply (rule exI) diverging
- Previous by Thread: Re: [isabelle] cases/induction on existential/free variables
- Next by Thread: Re: [isabelle] cases/induction on existential/free variables
- Cl-isabelle-users February 2009 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