Re: [isabelle] make_string

On 06/24/2018 08:40 PM, Makarius wrote:
On 23/06/18 14:58, Jeremy Dawson wrote:

On 06/22/2018 11:46 PM, Makarius wrote:
Isabelle/ZF and Isabelle/HOL can coexist happily within the same
Isabelle/ML process: Isabelle2017 has already introduced a reform on
theory names to make them globally unique accross all Isabelle + AFP

Hi Makarius,

How so?  When I try
theory Scratch imports ZF Main begin
I get an error message

See the included ROOT file which defines a session that contains all
theories from HOL + ZF. You can copy that to your project DIRECTORY and
use the session in Isabelle/jEdit as follows:

   isabelle jedit -d DIRECTORY -l "HOL+ZF"

Then you can work with theory ML values from unrelated contexts as
illustrated in the included Scratch.thy, but note that
Thy_Info.get_theory only works for theories loaded into the underlying
session image.

So there is no need to write out string representations of ML values at
all, and try to read them back again (that additional problem has not
even been touch on this thread so far).


Hi Makarius,

OK, I've downloaded Isabelle 2018 RC0, and got your attached Scratch.thy to work (which was as follows)

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.

So no doubt I could grab a goal from the middle of a ZF proof and create a HOL term/cterm out of it.

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?

Plus, there is the additional problem that
ML_prf {* @{Isar.goal} *} doesn't work (why?) and that
although ML_val {* @{Isar.goal} *} works,
ML_val {* ... *} seems to forget any ML value definitions anyway.
So that seems like an additional impediment to the idea of transferring computed ML terms from a ZF proof to a HOL proof.

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?



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