*To*: Makarius <makarius at sketis.net>, cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>, "Dr. Brendan Patrick Mahony" <mahonybp at tpg.com.au>*Subject*: Re: [isabelle] HOL+ZF context*From*: Jeremy Dawson <Jeremy.Dawson at anu.edu.au>*Date*: Thu, 28 Jun 2018 14:56:50 +1000*Authentication-results*: spf=none (sender IP is ) smtp.mailfrom=Jeremy.Dawson at anu.edu.au;*In-reply-to*: <87247181-6649-fdfb-396f-9d9063aa3a79@sketis.net>*References*: <8c0ea221-8962-e324-335a-b9e4836e7de3@anu.edu.au> <c43bbd97-0899-0b30-903e-1402bc8d40ef@sketis.net> <23ed31ca-087e-f6eb-9e1d-bf97fe1734d0@anu.edu.au> <f6ffe4fb-9af8-df93-6894-6d4b73c58409@sketis.net> <f58355ff-054e-79a5-240f-8ef8b9cea59c@anu.edu.au> <b063399a-ce0d-2bde-bc1a-2deb9a97bb7d@sketis.net> <f8341060-2568-4967-293c-94d6e5f2c6fe@anu.edu.au> <555d77fe-9cc0-66ad-e957-467a1448b256@sketis.net> <39c53c5f-ddea-7da2-49fb-230fe7ac7559@anu.edu.au> <cbcf1dcb-3810-b10b-df31-cf57f65ad86e@sketis.net> <8bb88d12-6a9a-05fa-7e35-5c4de7ec6502@anu.edu.au> <87247181-6649-fdfb-396f-9d9063aa3a79@sketis.net>*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:99*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.8.0

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 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.thySo, 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

Hi Makarius, but what is "the" enclosing theory context?

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.

lemma (in the ZF context) and schematic goal (in the HOL context) together

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

Cheers, Jeremy Dawson

**References**:**[isabelle] make_string***From:*Jeremy Dawson

**Re: [isabelle] make_string***From:*Makarius

**Re: [isabelle] make_string***From:*Jeremy Dawson

**Re: [isabelle] make_string***From:*Makarius

**Re: [isabelle] make_string***From:*Jeremy Dawson

**Re: [isabelle] make_string***From:*Makarius

**Re: [isabelle] make_string***From:*Jeremy Dawson

**Re: [isabelle] make_string***From:*Makarius

**Re: [isabelle] make_string***From:*Jeremy Dawson

**Re: [isabelle] HOL+ZF context***From:*Makarius

- Previous by Date: [isabelle] to automatically generate all the 16 lemmas corresponding to all the possible cases just from the definition of the function
- Next by Date: Re: [isabelle] to automatically generate all the 16 lemmas corresponding to all the possible cases just from the definition of the function
- Previous by Thread: Re: [isabelle] HOL+ZF context
- Next by Thread: [isabelle] Coinduction on predicate defined wrt other coinductive predicates
- Cl-isabelle-users June 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list