*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Obtain.result*From*: Palle Raabjerg <palle.raabjerg at it.uu.se>*Date*: Tue, 23 Feb 2010 13:44:34 +0100*In-reply-to*: <alpine.LNX.1.10.1002221404040.27793@atbroy100.informatik.tu-muenchen.de>*References*: <4B7D669C.4010603@it.uu.se> <alpine.LNX.1.10.1002221404040.27793@atbroy100.informatik.tu-muenchen.de>*User-agent*: Thunderbird 2.0.0.19 (X11/20090123)

Makarius wrote: > On Thu, 18 Feb 2010, Palle Raabjerg wrote: > >> An example may be best at this stage, so let us take a simple one from >> the Isar tutorial: >> >> lemma >> assumes Pf: "\<exists>x. P(f x)" >> shows "\<exists>y. P y" >> using assms >> proof - >> from Pf obtain x where "P(f x)" .. >> thus "\<exists>y. P y" .. >> qed >> >> What might that look like in ML? > > The following version tries to imitate what the system actually does > -- only concerning contexts, facts and goals, without Isar proof > machinery getting in between. > > ML {* > val cert = Thm.cterm_of @{theory}; > val ctxt1 = @{context}; > > val (_, ctxt2) = ctxt1 |> Variable.add_fixes ["P", "f"]; > val [A, C] = Syntax.read_props ctxt2 ["EX x. P (f x)", "EX y. P y"]; > val ([a], ctxt3) = ctxt2 > |> Variable.declare_term A > |> Variable.declare_term C > |> Assumption.add_assumes [cert A]; > > val ((xs, [b]), ctxt4) = ctxt3 > |> Obtain.result (fn _ => etac @{thm exE} 1) [a]; > > val res = Goal.prove ctxt4 [] [] C (fn _ => rtac @{thm exI} 1 THEN > rtac b 1); > val final_res = singleton (ProofContext.export ctxt4 ctxt1) res; > *} > > This may also serve as an example of operations from Chapter 4 in the > Isar Implementation manual. > > When experimenting, you can often do it in a more light-weight > fashion, e.g. using @{cprop "EX x. P (f x)"} the produce a certified > proposition that will become the assumption later. Nonetheless, > simultaneous reading of propositions as above affects type-inference > -- a priori the "f" and "P" carry no type constraint. The fully > official Variable.declare_term is required in production code to get > implicit polymorphism of results right, among other things. > > > Makarius Thanks. 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" Which will give us the proof obligation: (\<And>T. [|Name a[xvec:=Tvec] = T; T mem Tvec|] ==> thesis) ==> thesis With the assumptions: length xvec = length Tvec \<not>(a \<sharp> xvec) Which we have a tactic for solving. 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. If we have an existentially quantified assumption and want it to become a proposition and a witness, then Obtain.result seems to work. 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. - Palle Raabjerg

**References**:**[isabelle] Obtain.result***From:*Palle Raabjerg

**Re: [isabelle] Obtain.result***From:*Makarius

- Previous by Date: Re: [isabelle] Feature Request
- Next by Date: Re: [isabelle] Replacing Integration by Multivariate_Analysis
- Previous by Thread: Re: [isabelle] Obtain.result
- Next by Thread: [isabelle] Giving a name to a tactics-expression
- Cl-isabelle-users February 2010 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