[isabelle] treatment of qualified names in local theories



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
*}

I should explain why I want to do this: The reason is that I (along
with a few other people) am working on a tool for importing Haskell
datatype definitions into Isabelle. We are using a form of "soft
typing", so type constructors are defined as Isabelle constants, along
with the data constructors. The problem is that in Haskell, type names
and constructor names are in separate name spaces, and it is quite
common for a Haskell type and its data constructor to have the same
name, e.g.

data MyBool = MyBool Bool

I want to add qualifiers to distinguish these in Isabelle, something
like "type.MyBool" and "term.MyBool". However, since the
implementation of the tool uses local theories (which as I understand
is the recommended programming practice), it runs into the "Duplicate
fixed variable" error I mentioned above.

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

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?

- Brian





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