isar2html does not support definitions in a locale

[SKolodynski]

Example: definition (in topgroup) leftUniformity where "leftUniformity \<equiv> {V\<in>Pow(G\<times>G).\<exists>U\<in> \<N>\<^sub>0. {\<langle>s,t\<rangle>\<in>G\<times>G. (\<rm>s)\<ra>t \<in>U}\<subseteq> V}" in TopologicalGroup_Uniformity_ZF.

It is arguable if notions should be defined in a locale. The trade off here is that on one hand such definitions can be written in a notation used in the locale which is more readable than the raw set theory notation. On the other hand I don't know how to use such definition outside of that locale, for example in the above case if someone wants to continue the subject of topological group as a uniform space, but using the multiplicative notation instead of additive notation used in the topgroup locale. Probably the best approach is to define notions in raw set theory notation and then prove a lemma in the locale that shows the definition in locale-specific notation. Nevertheless the possibility of parsing a locale scoped definition should be added to isar2html.

[SKolodynski]

Turns out definitions inside a locale are already supported, the problem in parsing is that the notation part is not optional.

defpreamble :: Parser (String, String, String, String)
defpreamble = do
   c <- option "" incontext
   spaces
   name <- itemName
   spaces
   ts <- option "" typespec
   spaces
   spec <- defnotation
   spaces
   string "where"
   return (name, c, ts,spec)

[dan323]

Having different locales for the same thing but different notation is a bit of a mess. Nevertheless, you can create a locale with a different notation and instanciate it as the other one. This action carries all lemmas and definitions proven in one locale to the other. I left you a comment about it in here.

Once you instanciate topgroup with your new notation and give this instance a name "mult_not_top_group", then you can call "mult_not_top_group.leftUniformity" which will be this definition with the elements in your new locale. With this you do not need to prove "group0(G,P)" and carry it everywhere, for example.

I have not yet looked at the haskell parsers you use. I will have a look.

[SKolodynski]

I did not realize that one can change notation by instantiating a sublocale. Quite possibly this way did not exist around 2005-2006 when I was learning to use Isabelle. Anyway, next time when I want to create a locale that changes notation I will try to do that this way. I don't consider using different notations for the same notion a mess. What I consider a mess ( or rather an absurd ) is what happens in some other theorem provers where notions are so tightly coupled with notation that you need a separate notion of an "additive group" and "multiplicative group" that differ only in the symbol used for the group operation. I always wanted to avoid such things in IsarMathLib.

[dan323]

If I instanciate locales will it work with your parser to html?

[SKolodynski]

Most likely not out of the box, but I will extend the parser as needed. It would be helpful if you send me a small example of the syntax you are going to use.

[dan323]

There are 2 posibilities I know of:

sublocale topgroup < group0 G f gzero grop grinv unfolding group0_def gzero_def grop_def grinv_def
  using Ggroup by auto

sublocale topgroup \<subseteq> group0 G f gzero grop grinv unfolding group0_def gzero_def grop_def grinv_def
  using Ggroup by auto

with this line you can use all the theorems in the group0 locale within the topgroup locale, and your topgroup notation will be used properly in premises and conclusions.

[dan323]

Basically:

sublocale (name of your more specific locale: A) < (name of your more concrete locale: B) (fixed elements in the locale A that give the notation in the order they were fixed in the locale B) (proof of all assumptions of locale B)

[dan323]

Here it is a commit example