In an Isabelle formalization, I’m representing relations by binary predicates. I would like to have operators that perform typical relation operations like composition and inversion using this representation.
The document “What’s in Main” only mentions such operators for the representation by sets of pairs. The Relation theory says at the beginning, “Relations – as sets of pairs, and binary predicates”. However, I couldn’t find much support for the binary predicate representation in this theory. All I found were several lemmas with a mysterious pred_set_conv attribute.
Is there extensive support for relations represented by binary predicates? In particular, are there operators for common relation operations defined? Where are these things documented?
The support for relations as sets of pairs is slightly better developed than for binary predicates, but quite a lot is available. Many relation operations, however, are instances of more general operations on functions and predicates or they are indeed obtained using pred_set_conv. They may therefore be quite hard to find. Use the find_theorems command or panel to find the lemmas. Here is a brief summary of the usual operations:
relcompp (infix OO)conversep (notation _\<inverse>\<inverse>)tranclp and rtranclpinfsupop <= (I find the lemmas predicate2I and predicate2D particularly useful)BNF_Def.GrpBNF_Def.vimage2pwfP and accp