This is a derivative question of Existing constants (e.g. constructors) in type class instantiations.
The short question is this: How can I prevent the error that occurs due to free_constructors
, so that I can combine the two theories that I include below.
I've been sitting on this for months. The other question helped me move forward (it appears). Thanks to the person who deserves thanks.
The real issue here is about overloading notation, though it looks like I now just have a namespace problem.
At this point, it's not a necessity, just an inconvenience that two theories have to be used. If the system allows, all this will disappear, but I ask anyway to make it possible to get a little extra information.
The big explanation here comes in explaining the motivation, which may lead to getting some extra information. I explain some, then include S1.thy
, make a few comments, and then include S2.thy
.
Motivation: using syntactic type classes for overloading notation of multiple binary datatypes
The basic idea is that I might have 5 different forms of binary words that have been defined with datatype
, and I want to define some binary and hexadecimal notation that's overloaded for all 5 types.
I don't know what all is possible, but the past tells me (by others telling me things) that if I want code generation, then I should use type classes, to get the magic that comes with type classes.
The first theory, S1
Next is the theory S1.thy
. What I do is instantiate bool
for the type classes zero
and one
, and then use free_constructors
to set up the notation 0
and 1
for use as the bool
constructors True
and False
. It seems to work. This in itself is something I specifically wanted, but didn't know how to do.
I then try to do the same thing with an example datatype
, BitA
. It doesn't work because constant case_BitA
is created when BitA
is defined with datatype
. It causes a conflict.
Further comments of mine are in the THY.
theory S1
imports Complex_Main
begin
declare[[show_sorts]]
(*---EXAMPLE, NAT 0: IT CAN BE USED AS A CONSTRUCTOR.--------------------*)
fun foo_nat :: "nat => nat" where
"foo_nat 0 = 0"
(*---SETTING UP BOOL TRUE & FALSE AS 0 AND 1.----------------------------*)
(*
I guess it works, because 'free_constructors' was used for 'bool' in
Product_Type.thy, instead of in this theory, like I try to do with 'BitA'.
*)
instantiation bool :: "{zero,one}"
begin
definition "zero_bool = False"
definition "one_bool = True"
instance ..
end
(*Non-constructor pattern error at this point.*)
fun foo1_bool :: "bool => bool" where
"foo1_bool 0 = False"
find_consts name: "case_bool"
free_constructors case_bool for "0::bool" | "1::bool"
by(auto simp add: zero_bool_def one_bool_def)
find_consts name: "case_bool"
(*found 2 constant(s):
Product_Type.bool.case_bool :: "'a∷type => 'a∷type => bool => 'a∷type"
S1.bool.case_bool :: "'a∷type => 'a∷type => bool => 'a∷type" *)
fun foo2_bool :: "bool => bool" where
"foo2_bool 0 = False"
|"foo2_bool 1 = True"
thm foo2_bool.simps
(*---TRYING TO WORK A DATATYPE LIKE I DID WITH BOOL.---------------------*)
(*
There will be 'S1.BitA.case_BitA', so I can't do it here.
*)
datatype BitA = A0 | A1
instantiation BitA :: "{zero,one}"
begin
definition "0 = A0"
definition "1 = A1"
instance ..
end
find_consts name: "case_BitA"
(*---ERROR NEXT: because there's already S1.BitA.case_BitA.---*)
free_constructors case_BitA for "0::BitA" | "1::BitA"
(*ERROR: Duplicate constant declaration "S1.BitA.case_BitA" vs.
"S1.BitA.case_BitA" *)
end
The second theory, S2
It seems that case_BitA
is necessary for free_constructors
to set things up, and it occurred to me that maybe I could get it to work by using datatype
in one theory, and use free_constructors
in another theory.
It seems to work. Is there a way I can combine these two theories?
theory S2
imports S1
begin
(*---HERE'S THE WORKAROUND. IT WORKS BECAUSE BitA IS IN S1.THY.----------*)
(*
I end up with 'S1.BitA.case_BitA' and 'S2.BitA.case_BitA'.
*)
declare[[show_sorts]]
find_consts name: "BitA"
free_constructors case_BitA for "0::BitA" | "1::BitA"
unfolding zero_BitA_def one_BitA_def
using BitA.exhaust
by(auto)
find_consts name: "BitA"
fun foo_BitA :: "BitA => BitA" where
"foo_BitA 0 = A0"
|"foo_BitA 1 = A1"
thm foo_BitA.simps
end
The command
free_constructors
always creates a new constant of the given name for the case expression and names the generated theorems in the same way asdatatype
does, becausedatatype
internaly callsfree_constructors
. Thus, you have to issue the commandfree_constructors
in a context that changes the name space. For example, use a locale:After that, you can use both
A0
andA1
as constructors in pattern matching equations and0
and1
, but you should not mix them in a single equation. Yet,A0
and0
are still different constants to Isabelle. This means that you may have to manually convert the one into the other during proofs and code generation works only for one of them. You would have to set up the code generator to replaceA0
with0
andA1
with1
(or vice versa) in the code equations. To that end, you want to declare the equationsA0 = 0
andA1 = 1
as[code_unfold]
, but you also probably want to write your own preprocessor function in ML that replacesA0
andA1
in left-hand sides of code equations, see the code generator tutorial for details.Note that if
BitA
was a polymorphic datatype, packages such asBNF
andlifting
would continue to use the old set of constructors.Given these problems, I would really go for the manual definition of the type as described in my answer to another question. This saves you a lot of potential issues later on. Also, if you are really only interested in notation, you might want to consider
adhoc_overloading
. It works perfectly well with code generation and is more flexible than type classes. However, you cannot talk about the overloaded notation abstractly, i.e., every occurrence of the overloaded constant must be disambiguated to a single use case. In terms of proving, this should not be a restriction, as you assume nothing about the overloaded constant. In terms of definitions over the abstract notation, you would have to repeat the overloading there as well (or abstract over the overloaded definitions in a locale and interpret the locale several times).