Re: [isabelle] Relation exponentiation

If I remember correctly, ^ was changed to ^^ for relations. Also note that in contrast to previous Isabelle versions, relation composition (O) now is defined such that "R O S" means: first a step in R and _then_ a step in S.



On 03/18/2010 12:13 PM, Hojjat Hossein wrote:
Hello everyone,

According to Section 6.3.1 of the tutorial the iterated composition of a relation is available with the exponentiation sign. I am not sure why I get errors in the following theory:

theory relation_exponent
imports Main
   value "({(1::nat,2::nat),(2::nat,3::nat)} O {(1::nat,2::nat),(2::nat,3::nat)})"
   value "({(1::nat,2::nat),(2::nat,3::nat)} ^ (2::nat))"

The first value is fine but for the second one I get the following error:

*** Type unification failed: No type arity fun :: power
*** Type error in application: Incompatible operand type
*** Operator:  op ^ :: (nat × nat =>  bool) =>  nat =>  nat × nat =>  bool
*** Operand:   {(1, 2), (2, 3)} :: nat × nat =>  bool
*** At command "value".

I am using Isabelle2009-1.

Hossein Hojjat

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