Re: [isabelle] Problem with overloading and inductive



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.







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