Re: [isabelle] Obtain.result



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.