# [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
begin
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 )"
end
...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,
James

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