*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] making use of star*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 29 Jun 2012 16:44:37 +0200*In-reply-to*: <E1SkcAl-0007RC-LX@smtp2.cc.ic.ac.uk>*References*: <E1SkcAl-0007RC-LX@smtp2.cc.ic.ac.uk>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:13.0) Gecko/20120614 Thunderbird/13.0.1

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

**Follow-Ups**:**Re: [isabelle] making use of star***From:*James Smith

**References**:**Re: [isabelle] making use of star***From:*James Smith

- Previous by Date: Re: [isabelle] The syntactic equality
- Next by Date: Re: [isabelle] making use of star
- Previous by Thread: Re: [isabelle] making use of star
- Next by Thread: Re: [isabelle] making use of star
- Cl-isabelle-users June 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list