# 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.*