# Re: [isabelle] Obtain.result

*To*: Palle Raabjerg <palle.raabjerg at it.uu.se>
*Subject*: Re: [isabelle] Obtain.result
*From*: Makarius <makarius at sketis.net>
*Date*: Mon, 1 Mar 2010 11:31:04 +0100 (CET)
*Cc*: isabelle-users at cl.cam.ac.uk
*In-reply-to*: <4B83CDB2.10608@it.uu.se>
*References*: <4B7D669C.4010603@it.uu.se> <alpine.LNX.1.10.1002221404040.27793@atbroy100.informatik.tu-muenchen.de> <4B83CDB2.10608@it.uu.se>
*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Tue, 23 Feb 2010, Palle Raabjerg wrote:

`It appears we are getting closer to a possible solution. But
``Obtain.result is still causing some headaches. In the specific case we
``are working on, we have this obtain line in Isar: from `length xvec =
``length Tvec` `¬(a \<sharp> xvec)` obtain T where "(Name a)[xvec:=Tvec] =
``T" and "T mem Tvec"
`

`What confuses me is that Obtain.result takes a list of assumptions and a
``tactic, and will give as output lists of bindings (witnesses) and a list
``of propositions, whereas the Isar-obtain allows us to specify the
``witnesses and propositions explicitly.
`
But if I want to do something like the above, and I give the assumptions
`length xvec = length Tvec` and `\<not>(a \<sharp> xvec)` to
Obtain.result, it simply expects us to prove ([|length xvec = length
Tvec; \<not>(a \<sharp> xvec)|] ==> thesis) ==> (thesis)
which is not quite what we want.

`The Isar-obtain and Obtain.result are clearly related. But there is a
``disconnect somewhere that I don't quite understand.
`

`Isar text is always based on explicit statements by the user, this is
``usually easy to write and easy to read. When working in ML, composing
``statements is often quite delicate, so Obtain.result refrains from asking
``for that. In stead the obtained result is specified indirectly via the
``given facts and the tactic to smash them, and extract the result context
``(with local parameters and premises).
`

If we have an existentially quantified assumption and want it to become
a proposition and a witness, then Obtain.result seems to work.

You can try it as follows (in ML):
have "EX x y. A x y & B x y" by your_specific_tactic
-- "explicit proposition composed in ML"
then obtain x y where "A x y" and "B x y" by (elim exE conjE)
-- "Obtain.result here"
Makarius

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