Re: [isabelle] HOL+ZF context

(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
> begin
> ML \<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.


theory Scratch
  imports Pure

ML \<open>
  val ZF_ctxt = Proof_Context.init_global (Thy_Info.get_theory "ZFC");
  val ZF_prop = Syntax.read_prop ZF_ctxt "x = x";

  val HOL_ctxt = Proof_Context.init_global (Thy_Info.get_theory "Main");
  val HOL_thm =
    Goal.prove HOL_ctxt
      ["x", "y"]
      [Syntax.read_prop HOL_ctxt "(x::'a) = y"]
      (Syntax.read_prop HOL_ctxt "(y::'a) = x")
      (fn {context = goal_ctxt, prems} =>
        resolve_tac goal_ctxt (Proof_Context.get_thms goal_ctxt "sym") 1 THEN
        resolve_tac goal_ctxt prems 1);


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