Re: [isabelle] making use of star



Hi James,

the relation you want is truly relational, you cannot compute one argument from
the other. Prolog can deal with such relations with the help of logical
variables and backtracking. Isabelle's execution mechanism does not support
logical variables but only backtracking. Thus you would need to enumerate all
the possible values of all the other fields, which is infeasible in general.

Tobias

Am 29/06/2012 16:28, schrieb James Smith:
> 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.