Email Gateway (Aug 18 2022 at 13:05): Email Gateway (Aug 18 2022 at 13:05):From: c_feller <c_feller@informatik.uni-kl.de>
Hallo,
I have a problem when I try to use a overloaded function in a
inductive definition. I've made a small example to illustrate that:
consts lifu :: "'a => 'b"
overloading lifu1 == "lifu::'a list => int"
lifu2 == "lifu::int => nat"
begin
definition lifu1 where "lifu1 == length"
definition lifu2 where "lifu2 == nat"
end
inductive ind_lifu :: "int list => int => bool"
where
base: "lifu (a::int list) = lifu (b::int) ==> ind_lifu a b"
If i try to give that to Isabelle/HOL, i get the message:
Specification depends on extra type variables: "'a::{}"
Did I do something wrong or is this a bug?
Thanks,
Christoph Feller
Email Gateway (Aug 18 2022 at 13:05):From: Brian Huffman <brianh@cs.pdx.edu>
Hi Christoph,
Your inductive specification fixes the argument type of each use of
"lifu", but it doesn't specify what the return type is. Do you intend
the equality comparison to be at type "nat", "int", or something else?
This is why you get the message about an extra type variable.
You'll need to add extra type annotations, like this:
inductive ind_lifu :: "int list => int => bool"
where
base: "(lifu a :: nat) = (lifu b :: nat) ==> ind_lifu a b"
Hope this helps,
Quoting c_feller <c_feller@informatik.uni-kl.de>:
Email Gateway (Aug 18 2022 at 13:06):From: Brian Huffman <brianh@cs.pdx.edu>
Quoting c fe <zehfee@googlemail.com>:
I'll give an example from the Isabelle libraries.
The libraries define a polymorphic function "of_nat :: nat => 'a" that
can convert from the naturals to any other semiring type. Lots of
generic lemmas are proved about it.
The function "int :: nat => int" used to be defined as a separate
constant, but now it is defined as an abbreviation for "of_nat :: nat
=> int". Since it is just an abbreviation, we can use all the lemmas
about "of_nat" for reasoning about "int" as well. Back when it was a
separate constant, the libraries had two separate versions of each
lemma, one for "of_nat" and one for "int".
So if you have any generic lemmas about "lifu", then that might be an
argument for using overloading+abbreviations instead of separate
constants.
On the other hand, if all of your lemmas about "lifu" are specific to
certain types, maybe you would be better off using separate functions.
(Unless you think it is really important to have the shared "lifu"
syntax.)
Email Gateway (Aug 18 2022 at 13:06):From: c fe <zehfee@googlemail.com>
But why then use overloading in the first place? If I'm going to use
lifu_nat from your example isn't it almost the same as declaring lifu
and lifu_nat as seperate functions?
Christoph
Email Gateway (Aug 18 2022 at 13:08):From: Brian Huffman <brianh@cs.pdx.edu>
Quoting c fe <zehfee@googlemail.com>:
Any time you have functions overloaded to such an extent (i.e.
overloaded with respect to more than one type variable), you are bound
to need a lot of those ugly type annotations.
A possible workaround is to use abbreviations for type-specific
instances. For example, if you have a lot of type annotations like
"(lifu whatever :: nat)" in your theory, then you would probably
benefit by making a nat-specific abbreviation, like this:
consts lifu :: "'a => 'b"
abbreviation
lifu_nat :: "'a => nat"
where
"lifu_nat == lifu"
inductive ind_lifu :: "int list => int => bool"
where
base: "lifu_nat a = lifu_nat b ==> ind_lifu a b"
Type-specific abbreviations are helpful for output too, since they can
indicate type information that is usually hidden, even when "show
types" is enabled. For example, without the abbreviation lifu_nat, the
command "thm base" would give you no indication of what return type
"lifu" is used at, but with the abbreviation you can tell that it is
used at type nat.
Email Gateway (Aug 18 2022 at 13:10):From: "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>
This whole "instantiate your favourite generic constant" game has been
driving me nuts for ages. I actually do define abbreviations for the
most common generics, but slightly more general ones than you suggest eg
syntax (xsymbols)
"_UNIV" :: "type => 'a set" ("\<aleph>-[_]")
"_empty" :: "type => 'a set" ("\<emptyset>-[_]")
translations
"\<aleph>-[t]" \<rightharpoonup> "UNIV::(t)set"
"\<emptyset>-[t]" \<rightharpoonup> "{}::(t)set"
Still, even defining such syntax for every generic gets tiresome, so
you've inspired me to write a totally general operator for
instantiating the generics of constants.
syntax
"_type_inst" :: "[logic, types] => logic" ("_-[_]" [1000, 0] 1000)
parse_translation (advanced) {*
let
fun type_inst_tr ctxt [term, typs] =
let
val thy = ProofContext.theory_of ctxt;
val map_sort = Sign.intern_sort thy;
val get_sort = Sign.get_sort thy (Variable.def_sort ctxt)
fun typ_of_term t =
let
val env = (Syntax.term_sorts map_sort t);
val T = Sign.intern_typ thy (Syntax.typ_of_term (get_sort env)
map_sort t)
in
ProofContext.cert_typ ctxt T
end;
fun mk_types (Const("_types", _) $ T $ Ts) = (typ_of_term T)::
(mk_types Ts)
| mk_types T = [typ_of_term T];
fun mk_name const_space (Free(nm, _)) = Consts.intern const_space nm
| mk_name const_space (Const(nm, _)) = Consts.intern const_space nm;
val const_space = Sign.consts_of thy;
val Ts = mk_types typs;
val inm = mk_name const_space term;
val CT = Sign.const_instance thy (inm, Ts);
in
Const(inm, CT)
end;
in
[ ("_type_inst", type_inst_tr) ]
end;
*}
Then you just write "Domain-[nat, 'a]" for "Domain::(nat * 'a) set =>
'a set", which is quicker to write and a lot easier to read as well.
It seems to work okay (with minimum testing). If any of the Isabelle
code wizards would like to check over the way sorts are treated in
particular, I'd appreciate it. Some of this stuff is really hard to
untangle!
It would be nice to see something like this in the standard
distribution.
Cheers,
Brendan
Dr Brendan Mahony
C3I Division ph +61 8 8259 6046
Defence Science and Technology Organisation fx +61 8 8259 5589
Edinburgh, South Australia Brendan.Mahony@dsto.defence.gov.au
Important: This document remains the property of the Australian
Government Department of Defence and is subject to the jurisdiction
of the Crimes Act section 70. If you have received this document in
error, you are requested to contact the sender and delete the document.
IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914. If you have received this email in error, you are requested to contact the sender and delete the email.
Email Gateway (Aug 18 2022 at 13:11):From: c fe <zehfee@googlemail.com>
Hallo Brian,
Thanks, that really helped. But it lead to me having to annotated
quite a lot of expressions which made my terms look rather convoluted.
And as I think that those terms are important I want them to look as
comprehensible as possible. So I'm now back to different functions
with the same mixfix syntax and keep getting ambiguous input warnings
but the definitions look ok.
But thanks, nevertheless. I don't know how long I would have been
trying to solve this.
Greeting,
Christoph
Last updated: May 03 2024 at 04:19 UTC