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.email@example.com>
- References: <4B7D669C.firstname.lastname@example.org> <alpine.LNX.email@example.com> <4B83CDB2.firstname.lastname@example.org>
- 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"
This archive was generated by a fusion of
Pipermail (Mailman edition) and