Email Gateway (Aug 18 2022 at 10:52): Email Gateway (Aug 18 2022 at 10:52):From: Lucas Cavalcante <thesupervisar@gmail.com>
I thank you in advance for any clarification concerning my following doubts!
1.
Suppose I want to define a new datatype in terms of other fresh
datatypes, and then define a function over this new datatype, as for
instance in:
datatype
mytype = typ0 | typ1
and
typ0 = Zero
and
typ1 = One
consts And :: "[mytype, mytype] => mytype"
primrec
"And Zero One = Zero"
"And Zero Zero = Zero"
"And One Zero = Zero"
"And One One = One"
Why does Isabelle complain that the constructors Zero and One do not
have type "mytype", as I explicitly declared typ0 and typ1 as
particular cases of mytype?
I also tried to define, more simply:
consts AND :: "[mytype, mytype] => mytype"
primrec
"AND Zero x = Zero"
"AND x y = y"
bu that went even worse for Isabelle... I found the error messages
somewhat unexpected, as a completely similar definition works fine in
ML.
Of course, this is just a simple example of the problem I'm having.
What I am really interested in is in defining functions involving
mutually recursive datatypes, but first I have to understand what
happens in simpler cases such as the above one!
2.
Can I not use the same constructor name for different datatypes? In
the following example the second step of primrec is not correct
because Two is not from 'a n1 datatype anymore, but 'a n2.
datatype 'a n1 = One 'a | Two 'a | LotOf 'a
datatype 'a n2 = Two 'a | OddPrime 'a
consts ct :: "'a n1 => 'a n1"
primrec
"ct (One x) = One x"
"ct (Two x::'a n1) = (One x::'a n1)"
3.
When using the same syntax sugar for different constructors of
different datatypes, Isabelle finds it ambiguous to correctly parse
the terms. Can I not use the same connective symbol for these
constructions? Details follow in the example below:
datatype 'a t1 = At1 'a
| Not1 "'a t1" ("not_" [50])
| Imp1 "'a t1" "'a t1" ("_imp_" [45])
datatype
'a t2 = "'a t3"
| Not "'a t3" ("not_" [50])
and
'a t3 = At 'a
| Imp "'a t2" "'a t2" ("_imp_" [45])
consts
valid_t1 :: "'a t1 => prop" ("(_)" 5)
valid_t2 :: "'a t2 => prop" ("(_)" 5)
valid_t3 :: "'a t3 => prop" ("(_)" 5)
axioms
impIa: "(P ==> Q) ==> P imp Q"
Lucas
Email Gateway (Aug 18 2022 at 10:52):From: Tobias Nipkow <nipkow@in.tum.de>
does not do what you think it does, neither in Isabelle nor in ML.
The above declares mytype to be a type with two nullary constructors
typ0 and typ1. (The name space for types and functions is disjoint.)
There are no untagged union types in the ML family of languages, incl HOL.
Tobias
Email Gateway (Aug 18 2022 at 10:52):From: Brian Huffman <brianh@cs.pdx.edu>
You can indeed use the same constructor name for different datatypes, as you
have done in your example. But the unqualified name "Two" will always refer
to the most recently defined one, regardless of any type annotation you put
on it. To distinguish between them, you should use the qualified
names "n1.Two" and "n2.Two".
Note that Isabelle's pretty printer uses qualified names exactly when needed
for disambiguation, so if you type the command "term Two" after the above
datatype declarations, Isabelle responds with:
"n2.Two"
:: "'a => 'a n2"
Email Gateway (Aug 18 2022 at 10:52):From: Brian Huffman <brianh@cs.pdx.edu>
Isabelle finds the axiom "impla" ambiguous because it is ambiguous. This
axiom produces 128 parse trees (one 2-way ambiguity between Imp1/Imp, and
three 4-way ambiguities between valid_t1/valid_t2/valid_t3/Trueprop, which
makes 2 * 4 * 4 * 4 = 128), of which 2 are type-correct:
"(PROP valid_t1 P ==> PROP valid_t1 Q) ==> PROP valid_t1 (Imp1 P Q)"
"(PROP valid_t2 P ==> PROP valid_t2 Q) ==> PROP valid_t3 (Imp P Q)"
You could specify which one of these you mean by using type annotations, e.g.
axioms impIa: "((P::'a t1) ==> Q) ==> P imp Q"
Isabelle will still give a warning about the multiple parse trees, but it will
accept the declaration since now only one parse tree is type correct.
In general I think it is a bad idea to reuse the same syntactic sugar for
different constants, since it can slow down the parser a lot (In the example
above, Isabelle must attempt to type-check all 128 parse trees to find the
one that works). Instead, I would recommend using type classes and
overloading; you can associate the syntactic sugar with the overloaded
constant without causing any ambiguity in parsing.
Last updated: May 03 2024 at 08:18 UTC