Re: [isabelle] treatment of qualified names in local theories



On Wed, 29 Jun 2011, Brian Huffman wrote:

Why can't I define two constants with the same base-name (but different qualifiers) in the same local theory? The following code, which tries to define "one.foo == True" and "two.foo == False", gives a "Duplicate fixed variable(s)" error message. It works just fine if I split it into two separate local_setup commands, however.

local_setup {*
fn lthy =>
 let
   val qual = Binding.qualify true
   val ((t1, (s1, thm1)), lthy) = lthy |>
     Local_Theory.define
       ((qual "one" @{binding foo}, NoSyn),
        ((qual "one" @{binding foo_def}, []), @{term "True"}))
   val ((t2, (s2, thm2)), lthy) = lthy |>
     Local_Theory.define
       ((qual "two" @{binding foo}, NoSyn),
        ((qual "two" @{binding foo_def}, []), @{term "False"}))
 in
   lthy
 end
*}

This is according to the specifications. The auxiliary context of the local theory target presents newly defined terms as fixed variables, but these cannot be qualified. (There are no kernel checks for that for performance reasons, but the overall system will make problems when the principle "consts: qualified, fixes: unqualified" is violated.)

The restriction holds only as long as the aux. context is active, i.e. you can introduce artificial boundaries as workaround, using Local_Theory.init/exit or reinit operations in a way that I cannot tell on the spot, without some study of the current state of the sources.


data MyBool = MyBool Bool

I want to add qualifiers to distinguish these in Isabelle, something like "type.MyBool" and "term.MyBool".

It is probably easier to avoid this clash by using the conventional Isabelle naming scheme in such situations: terms are called "foo", types are called "foo_type". A suffix will always be orthogonal to name spaces prefixes and qualifiers.

If you do not want to present it like that to the end user, you can additionally augment the global const name space afterwards using Sign.const_alias etc. -- this looks to be the least intrusive workaround at the moment.


Will local theories in a later version of Isabelle be able to use qualifiers to distinguish names?

Depends if I manage to localize HOL/datatype and record without it. Records have their own small qualifiers with potential duplication of base names, but it is possible that one can somehow avoid getting into the same trouble as above. If not, I not to devise some tricks to overcome the limitation somehow.


While I am still using Isabelle2011, is there a workaround that will let me avoid the error, while still generating the top-level qualified constant names that I want? Or will I have to "un-localize" the tool so that it uses top-level theories directly instead of local theories?

This is also possible, see Inductive.add_inductive_global, for example. (Operations called "global" are generally considered a bit fashioned, potentially being discontinued when localization has advanced further.)


	Makarius





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