[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.