Re: [isabelle] cases/induction on existential/free variables



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)





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.