Re: [isabelle] HOL+ZF context
On 28/06/18 01:36, Makarius wrote:
(I have now changed the Subject to what we are talking about.)
On 27/06/18 06:51, Jeremy Dawson wrote:
val Main_thy = Thy_Info.get_theory "Main";
val ZF_thy = Thy_Info.get_theory "ZF";
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
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.
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)
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)
This archive was generated by a fusion of
Pipermail (Mailman edition) and