*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Problem with overloading and inductive*From*: "Dr. Brendan Patrick Mahony" <brendan.mahony at dsto.defence.gov.au>*Date*: Tue, 3 Mar 2009 14:31:15 +1030*In-reply-to*: <20090302033145.2zfmei9jlcssok4k@webmail.pdx.edu>*References*: <a1e5e35a0902270527t75860ad4k8620771e8256ca29@mail.gmail.com> <20090228093206.icxiz8l74csc0c44@webmail.pdx.edu> <a1e5e35a0903020224m87fd855oc315300e59d2b9c0@mail.gmail.com> <20090302033145.2zfmei9jlcssok4k@webmail.pdx.edu>

On 02/03/2009, at 10:01 PM, Brian Huffman wrote: > Quoting c fe <zehfee at googlemail.com>: > >> 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. > > 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 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 at 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.

**References**:**Re: [isabelle] Problem with overloading and inductive***From:*c fe

**Re: [isabelle] Problem with overloading and inductive***From:*Brian Huffman

- Previous by Date: Re: [isabelle] And mask
- Next by Date: [isabelle] interpreters and continuations
- Previous by Thread: Re: [isabelle] Problem with overloading and inductive
- Next by Thread: Re: [isabelle] Problem with overloading and inductive
- Cl-isabelle-users March 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list