Re: [isabelle] display of types



On 11/04/2007, at 8:38 AM, Jeremy Dawson wrote:

> I've also noticed this - presumably the thinking is, that if a user  
> has declared a constant, he/she knows what type it is.
>
> But often I've found it would be helpful, when a polymorphic  
> constant is used monomorphically (or with a less general  
> polymorphic type) in a theorem, it would be nice to be able to see  
> the type.
>
> Apart from printing out the term (which can give rather long  
> output) is there any way of doing this?

This is indeed a problem, including the need to type cast constants  
frequently in local goals to ensuring
matching to global goals.

A useful flag is the show constants flag, this at least gives you a  
list of the constants in the goal state and
their types, but not of which instance is which in the actual goals.

Specialised syntax for type casting constants is useful. eg

syntax
   "_empty" :: "type \<fun> logic"  ("{}[_]")

translations
   "{}[T]" => "{}::T set"

This sort of syntax helps clarify the instantiated type parameters  
and saves clutter.
A suitable typed print translation will allow this operator to appear  
in the goal state display too.
This is, of course, a lot of effort!
Some automatic support for declaring such instantiation syntax for  
every generic constant would be useful.

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.