Re: [isabelle] transitive closure



The type is not correct -- you need st of type 'a * 'a set. You need to uncurry "less".

trancl (split less) should work.

Amine.

Randy Pollack wrote:
Transitive_Closure.thy defines
 inductive_set
   trancl :: "('a × 'a) set => ('a × 'a) set"  ("(_^+)" [1000] 999)
   for r :: "('a × 'a) set"
 where
     r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"
   | trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==>
	(b, c) : r ==> (a, c) : r^+"

but this doesn't seem to work right with new style relations, e.g.
  term "(less :: nat => nat => bool)^+"

produces a type error.  Is there a transitive closure operator for new
style relations?

Thanks,
Randy








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