[isabelle] making use of star

Good afternoon,


this is the first of several neophyte questions I suspect...


I've defined reflexive transitive closure...


theory rtc

imports Main



inductive star :: "('a => 'a => bool) => ('a => 'a => bool)" for r where

base: "star r x x" |

step: "r x y ==> ( star r y z ==> star r x z )"




...and now want to apply this to a successor function I have on states...


definition succ :: "State => State => bool" 

  where "( succ x y ) \<equiv> ( index x = Suc(index y) )"


...where states are just records with an index field and other non
interfering fields:


record State = 

  index :: nat



My successor function works fine. If I instantiate a few states with the
obvious indeces I get, for example...


value "succ state_1 state_0"


...returning true, whereas


value "succ state_2 state_0"


returns false.


I (somewhat naively, it turns out) expected that...


value "star succ state_2 state_0"


..would return true, but it returns:


"star (\<lambda> u ua. Index = Suc( index ua)) (| index = Suc( Suc 0), ...\)
(| index = 0, ...|)"


My Coq colleagues in the room aren't suprised and tell me that my definition
of star is just that, and doesn't provide a way to actually compute the
transitive closure. Also, I note that if I do...


value "succ"


...I get "_", which I take to mean "some value", whereas if I do...


value "star"


...I just get "star", which I suspect has something to do with it.


Can anyone tell me what is going wrong and how to fix it?


Many thanks,






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