Email Gateway (Aug 22 2022 at 17:29): Email Gateway (Aug 22 2022 at 17:29):From: Makarius <makarius@sketis.net>
(I have now changed the Subject to what we are talking about.)
On 27/06/18 06:51, Jeremy Dawson wrote:
theory Scratch
imports Pure
beginML \<open>
val Main_thy = Thy_Info.get_theory "Main";val ZF_thy = Thy_Info.get_theory "ZF";
\<close>end
and it still works when I substitute imports ZF for imports Pure.
There is some freedom of choice here. In principle you can do everything
in a Pure-derived theory as above, and produce terms and facts from
other contexts as illustrated in the included Scratch.thy
In practice it might be better to chose a default standing point, e.g.
Main HOL, and cherry-pick things from the ZF-derived context. This also
allows to use regular Isar statements and proofs from HOL.
But how do I then start doing a proof in HOL involving that term? The
theory window won't let me put in another theory following the end of
the first one, and it won't let me do
theory Scratch
imports ZF Main
and if I back up to the beginning and replace imports ZF by imports Main
then it has forgotten the ML values which were declared.
So how does one transfer ML values from a ZF proof to a proof in Main?
ML values are not forgotten, but stored in the enclosing theory context.
It is possible to move values between such theory contexts, e.g. via a
global Synchronized.var but then you need to take the physics of
Isabelle theory versions and PIDE processing into account.
It is probably easier to pick plain values from a clearly defined theory
context (e.g. ZF) as illustrated in the included Scratch.thy
So, given that the problem is to take a goal from a ZF proof, compute a
goal to be proved in HOL, and start a HOL proof with that new goal, how
can I do that?
You work always in an implicit HOL context.
You occasionally use operations like Syntax.read_prop to produce ZF
terms within an explicit ZF context, and transform them to be usable in
the HOL context.
Makarius
Scratch.thy
Email Gateway (Aug 22 2022 at 17:29):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Makarius,
but what is "the" enclosing theory context?
Your example theory file shows how to parse, in ZF, a term that has been
typed in, and use an ML function to prove a goal (which could, in
general, be a HOL term computed from the ZF term).
But I want to grab a subgoal which arises in the course of proving a
lemma in ZF, calculate a HOL term, and postulate that term as a goal in
HOL, for proving in HOL (in Isar, not in ML)
That is,
theory Z imports ZF begin
lemma ..... (ie set out to prove something in ZF)
assorted proof steps
grab subgoal n as a ML value of type term
do things with it to create a term suitable for proving in HOL
call this term hol_term
oops or sorry or whatever
switch context to HOL
now set out to prove the goal, which is the term calculated previously,
eg, as someone suggested,
schematic goal "?P"
resolve_tac (Thm.trivial hol_term)
now continue the HOL proof
Now as far as I can tell,
lemma ... (following theory Z imports ZF begin)
works in the ZF context,
and I want the
schematic goal "?P" to work in the HOL context.
Now you have shown me how to get a HOL context and a ZF context present
together, but I still don't see how to get
lemma (in the ZF context) and
schematic goal (in the HOL context) together
(ie, without ML values created during the first proof being lost before
you start the second proof).
Re the suggestion to use Synchronized.var - if I do that wouldn't I just
have to somehow stop the Synchronized.var value getting lost, just as I
now have to stop the term value getting lost.
To sum up, the issue is to do
(1) grab a subgoal out of a proof in ZF
(2) massage it to create a term
(3) start up a proof in HOL with that term as the goal (and that proof
will be using Isar, not using Goal.prove and ML code)
Cheers,
Jeremy Dawson
Email Gateway (Aug 22 2022 at 17:46):From: Makarius <makarius@sketis.net>
On 28/06/18 06:56, Jeremy Dawson wrote:
On 28/06/18 01:36, Makarius wrote:
ML values are not forgotten, but stored in the enclosing theory context.
It is possible to move values between such theory contexts, e.g. via a
global Synchronized.var but then you need to take the physics of
Isabelle theory versions and PIDE processing into account.but what is "the" enclosing theory context?
It is the context of the 'ML' or 'ML_file' command (or any other command
than invokes the ML compiler). Everything in Isabelle has a formal
context; the ML environment is a part of that, and ML compilation is a
function to update that formal context.
In addition, Isabelle2018 will also provide 'ML_export' to write through
to the bootstrap ML environment, what you might remember as "the ML
toplevel" from 1998. That new feature needs to be used with great care,
though, and with an understanding how normal Isabelle/ML works within a
formal context.
Your example theory file shows how to parse, in ZF, a term that has been
typed in, and use an ML function to prove a goal (which could, in
general, be a HOL term computed from the ZF term).But I want to grab a subgoal which arises in the course of proving a
lemma in ZF, calculate a HOL term, and postulate that term as a goal in
HOL, for proving in HOL (in Isar, not in ML)That is,
theory Z imports ZF begin
lemma ..... (ie set out to prove something in ZF)
assorted proof steps
grab subgoal n as a ML value of type term
do things with it to create a term suitable for proving in HOL
call this term hol_term
oops or sorry or whateverswitch context to HOL
now set out to prove the goal, which is the term calculated previously,
eg, as someone suggested,
schematic goal "?P"
resolve_tac (Thm.trivial hol_term)
now continue the HOL proofNow as far as I can tell,
lemma ... (following theory Z imports ZF begin)
works in the ZF context,
and I want the
schematic goal "?P" to work in the HOL context.Now you have shown me how to get a HOL context and a ZF context present
together, but I still don't see how to get
lemma (in the ZF context) and
schematic goal (in the HOL context) together
(ie, without ML values created during the first proof being lost before
you start the second proof).
I also don't see that on the spot, which is why I did not answer this so
far. I guess it could work as a special Isar command like 'subgoal', but
it needs to switch the background theory context, which is normally not
supported in Isar proofs.
Re the suggestion to use Synchronized.var - if I do that wouldn't I just
have to somehow stop the Synchronized.var value getting lost, just as I
now have to stop the term value getting lost.To sum up, the issue is to do
(1) grab a subgoal out of a proof in ZF
(2) massage it to create a term
(3) start up a proof in HOL with that term as the goal (and that proof
will be using Isar, not using Goal.prove and ML code)
From what we've had so far on this thread, you should manage (1), (2),
and a variant of (3) that uses Goal.prove with a context derived from an
alien theory (HOL).
We can later look again to figure out how to turn this approximation of
(3) into an Isar goal command.
Note that in the coming days I will be on travel: FLoC at Oxford (UK)
until 15-Jul-2018.
Makarius
Last updated: Apr 23 2024 at 04:18 UTC