Email Gateway (Aug 17 2022 at 13:46): Email Gateway (Aug 17 2022 at 13:46):From: Sean McLaughlin <seanmcl@cmu.edu>
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
Email Gateway (Aug 17 2022 at 13:46):From: Brian Huffman <brianh@csee.ogi.edu>
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.
Last updated: May 03 2024 at 08:18 UTC