Re: [isabelle] type mappings



One way to find such a set is to search for theorems that use the 
"type_definition" predicate. For example, the typedef you mentioned causes 
Isabelle to generate the following theorem (a similar theorem is axiomatized 
for every typedef):

type_definition_Prod: "type_definition Rep_Prod Abs_Prod Prod"

"type_definition" has type "('a => 'b) => ('b => 'a) => 'b set => bool" where 
'a stands for the new type you are defining. So a theorem search with the 
pattern "type_definition :: (_ * _ => _) => _ => _ => _" will give you just 
the theorem you want.

- Brian

On Thursday 16 February 2006 08:31, Sean McLaughlin wrote:
> Hello,
>
>    Is there a way to determine, eg.
> that the "*" type constructor corresponds to "Prod",
> as in
>
> typedef (Prod)
>    ('a, 'b) "*"    (infixr 20)
>      = "{f. EX a b. f = Pair_Rep (a::'a) (b::'b)}"
>
> ?
>
> Thanks,
>
> Sean





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