Re: [isabelle] [isabelle-dev] Relations vs. Predicates

On 03/22/2012 06:42 PM, Brian Huffman wrote:
On Thu, Mar 22, 2012 at 9:26 AM, Christian Sternagel
<c-sterna at>  wrote:
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?

Hi Chris,

I assume that by "currently", you refer to Isabelle 2011-1. I am
therefore replying to the isabelle-users list.

actually I was talking about the development version (hence the dev list) but the situation is essentially the same in Isabelle2011-1 I guess. By "adhoc overloading" I was referring to the theory Adhoc_Overloading (e.g., used for do-notation) which could (I think) be used to unify the syntax (independently from what you said about generic lemmas) of funpow, relpow, compow, and what is more.



Here's why "op ^" and "op ^^" are separate constants since 2009-1: "op
^^" is an ad hoc overloaded function, with a separate definition for
each type instance. On the other hand, "op ^" has a single generic

"a ^ 0 = 1"
"a ^ Suc n = a * a ^ n"

Having a single generic definition for "op ^" makes it possible to
prove generic lemmas about exponents, which are applicable to
arbitrary rings and semirings.

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?)

I think this is historical. Before the big set/predicate merge
experiment started in Isabelle 2008, predicates were not supported
very well by either the libraries or the definition tools (e.g.
"inductive" could only be used to define sets, not predicates).
Support for predicates has steadily improved since, and I see no
reason why we couldn't add "op ^^" for predicates now; I guess you're
the first to ask for it.

- Brian



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
isabelle-dev mailing list
isabelle-dev at

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