Re: [isabelle] making use of star



Tobias, hi,

back with Isabelle today...

>4. This does still not quite work because "succ" is not defined in a manner
>that the second argument can be computed from the first. It needs to be an
>inductive definition
>
>inductive succ :: "State => State => bool"
>where "y = x(|index := Suc(index x)|) ==> succ x y"

Hmm, I've just looked at this again. I think I haven't explained myself well
and so have been misunderstood. I have my definition of State:

---------------------------------------------------------------------------
record State =
	index :: nat
	cookies :: "Cookie set"
---------------------------------------------------------------------------

A cookie is just a string for the time being, and I instantiate one:

---------------------------------------------------------------------------
type_synonym Cookie = string
definition c :: Cookie where "counter=[CHR ''c'']"
---------------------------------------------------------------------------

I also instantiate a few states:

---------------------------------------------------------------------------
definition state_0 :: State where "state_0\<equiv>(|index=0,cookies={}|)"
definition state_1 :: State where "state_1\<equiv>(|index=1,cookies={c}|)"
definition state_2 :: State where "state_2\<equiv>(|index=2,cookies={c}|)"
---------------------------------------------------------------------------

Now with the succ predicate defined about the following...

---------------------------------------------------------------------------
value "succ state_0 state_1"
---------------------------------------------------------------------------

...returns false and it took me a while to work out why. If I delete the
cookie from state_1, or, alternatively, add a cookie to state_0, it works.
This is because the inductive predicate, as you rightly point out,
calculates the second argument from the first, taking x and changing its
index to get y. Therefore y is only the successor to x if y agrees in all
its other fields. But this isn't the required behaviour, y should be the
successor if its index is one greater, that's all.

I understand inductive definitions a little better now so I have, for
example:

---------------------------------------------------------------------------
Inductive succ :: "nat => nat => bool" where
"succ 1 0" |
"succ n m ==> succ (Suc n) (Suc m)
---------------------------------------------------------------------------

But how can I get this with states? I have a signature...

---------------------------------------------------------------------------
Inductive succ :: "nat => nat => bool" where
...
---------------------------------------------------------------------------

...but it's not obvious to me how I create a base step without instantiating
states, which I don't want to do except for ``testing''. I mean with nat you
already have an inductive set to work with, to do induction over, so
defining succ n m is easy from there. But with my states I don't have a
structure already in place so I can't do induction over it.

It seems to me I should just use "State list", in which case, if I take the
time to understand the functionality available with lists, I won't need to
define succ at all.

Regards,

James








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