*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] making use of star*From*: "James Smith" <jecs at imperial.ac.uk>*Date*: Fri, 29 Jun 2012 07:28:50 -0700*In-reply-to*: <4FE47C43.9000506@in.tum.de>*Organization*: Imperial College*Reply-to*: jecs at imperial.ac.uk*Thread-index*: Ac1QgN7x6nizY7s1TtWMxHHofOglawFXuEqw

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:*Tobias Nipkow

**References**:**Re: [isabelle] making use of star***From:*Tobias Nipkow

- Previous by Date: [isabelle] PIDE Display of Assumptions
- Next by Date: Re: [isabelle] The syntactic equality
- 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