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

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.

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

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

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