Email Gateway (Aug 18 2022 at 14:35): Email Gateway (Aug 18 2022 at 14:35):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 14:37):From: Palle Raabjerg <palle.raabjerg@it.uu.se>
Makarius wrote:
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.
Email Gateway (Aug 18 2022 at 14:47):From: Palle Raabjerg <palle.raabjerg@it.uu.se>
First, thank you for the replies to "Structured induction with custom
tactics". FOCUS and SUBPROOF does indeed seem to be more or less what we
were looking for. We may have read over that particular part of the
programming tutorial a bit too lightly. At the time, we were also using
a slightly older Isabelle version without FOCUS.
Anyway. This time I have a somewhat more specific question. How do we
use Obtain.result?
For some proofs, we often need to fix variables using the Isar obtain
command. Obtain.result would seem to be the corresponding ML function,
but we have so far been unable to figure out how to use it properly. And
we may possibly be on the wrong track again.
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?
Regards,
Palle Raabjerg
Email Gateway (Aug 18 2022 at 14:49):From: Makarius <makarius@sketis.net>
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: fromlength 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 Tvecand\<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
Last updated: Apr 19 2024 at 20:15 UTC