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:

theory Scratch
   imports Pure

ML \<open>
   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
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.


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)


Jeremy Dawson

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