Re: [isabelle] Obtain.result



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





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