*To*: "J.V. Paiva-Miranda-De-Siqueira" <jvp27 at cam.ac.uk>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Proving something is an instance of a locale*From*: Lars Hupel <hupel at in.tum.de>*Date*: Tue, 2 Aug 2016 23:13:56 +0200*In-reply-to*: <76d9a09ea33c20903bbe3f62896dba42@cam.ac.uk>*References*: <76d9a09ea33c20903bbe3f62896dba42@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0

Dear JosÃ, > I seem to be missing something while trying to show a certain > construction is a Ring (a locale in an imported theory). could you maybe point us to the theory file where this is defined? It would make helping you solve your problem much easier. (The answers below are speculations because I don't know the details.) > lemma stalk_set_is_ring: > assumes P: "x ââT" > shows "Ring (stalk_ring x)" > proof unfold_locales > > although at least most of them must be trivial (I built this ring out of > an existing one). There must be a gap in my understanding of this > process, since I tried to prove this apparently trivial Where exactly did you get stuck? This looks at least like the correct lemma statement. > lemma (in presheaf) objecstmapringvalued: > assumes L: "(U:: 'a set) â T" > shows "Ring (objectsmap U)" > proof unfold_locales > > and failed. This should show for each U that objectsmap U is a Ring, and > here objectsmap :: "'a set â ('a, 'm) Ring_scheme" is one of the > parameters of the locale presheaf, so wouldn't that be immediate since > the last type is ('a,'m) Ring_schemes? Again, this is hard to say without seeing the "Ring" locale. There could be additional assumptions you have to show. > I also noticed that although I > can invoke presheaf_axioms and presheaf_def, I can't directly use > something like the definition of objectsmap itself in a proof. How so? There should be a theorem called "objectsmap_def" if "objectsmap" is a regular "definition". You can unfold that using "apply (subst objectsmap_def)" or "unfolding objectsmap_def". > I'm still not sure about how to tell Isabelle to use an instance of the ring > axioms or theorems for a particular ring during a proof -- in my > situation, for example, all the new ring operations are built out of > those of rings objectsmap U, so it would be great to invoke facts for such. You can use the command "interpret" in a proof to obtain the facts for an existing structure, like so: interpret xyz: Ring "other_structure" ... then, if there's an assumption "abc" in the "Ring" locale, you can access that via "xyz.abc". See the locale manual for more details on this process. Cheers Lars

**References**:**[isabelle] Proving something is an instance of a locale***From:*J.V. Paiva-Miranda-De-Siqueira

- Previous by Date: Re: [isabelle] [noob] Classification functions as part of type definition?
- Next by Date: [isabelle] CfP: 3rd Workshop in MILS: Architecture and Assurance for Secure Systems
- Previous by Thread: [isabelle] Proving something is an instance of a locale
- Next by Thread: Re: [isabelle] Proving something is an instance of a locale
- Cl-isabelle-users August 2016 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