[isabelle] Relation exponentiation



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
begin
  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))"
end

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
EPFL




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