[isabelle-dev] Relations vs. Predicates

[Christian Sternagel]

Hi all,

currently there are two constants

op ^  :: "'b => nat => 'b"
op ^^ :: "'b => nat => 'b"

making it a bit difficult for the user to choose the correct one in all 
situations. As far as I see "op ^^" is just syntax for the overloaded 
"compow". Shouldn't it be possible to unify this (and also relpow) by 
using adhoc overloading, so that only one operator, e.g., "op ^" remains?

To come back to the subject, I'm missing "iteration" of predicates, 
i.e., what "_^^n" is on relations but for predicates ("'a => 'a => 
bool"). (Why are predicates "less developed" than relations anyway?)

cheers

chris

PS: I suggest to rename "rel_comp" into "relcomp" (to be consistent with 
"relpow"). In @{theory Relation} there is a typo in the lemma name 
"prod_comp_bot1".