*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, 22 Jun 2012 16:08:03 +0200*In-reply-to*: <E1ShgXn-0005ii-OQ@smtp2.cc.ic.ac.uk>*References*: <E1ShgXn-0005ii-OQ@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

Am 21/06/2012 14:31, schrieb James Smith: > 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 > > 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. They are wrong. Isabelle (in contrast to Coq) can often execute inductive definitions. Hence your expectation makes sense. However, there are several difficulties with the way you have phrased your definitions: 1. You need to say code_pred start . in order to generate code for star (or any inductive predicate). 2. star is higher order. This complicates code generation to the point that it does not work for the situation where all arguments of "star r" are inputs. If you fix r in the defn of star, it works better. But let's assume we stick with your star. 3. What your defn of star will still allow us to do is to translate it into a Prolog-like enumeration of all y such that "star r x y" for some given r and x. This means not a single value but a set of values will be computed. The syntax is values "{y. star succ state_0 y}" 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" code_pred succ . 5. Now the above values command does not terminate because there are infinitely many successor states. You can look at the first 3 states like this: values 3 "{y. star succ state_0 y}" Happy? 6. The way you have written star makes it unsuitable for computing predecessors from successors: values 3 "{x. star succ x state_2}" will not terminate because star will call itself recursively forever without getting to a call of succ. For an impressive example of what code generation for inductive predicates can do see A. Lochbihler, L. Bulwahn : Animating the Formalised Semantics of a Java-like Language. ITP 2011 http://pp.info.uni-karlsruhe.de/personhp/andreas_lochbihler.php > 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. > This is the result of the fact that "normal" definitions and inductive ones are executed by different mechanisms. Tobias PS I have take the liberty to remove most of the blank lines from your email. > > Many thanks, > > > > James > > > > > > >

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

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

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

- Previous by Date: Re: [isabelle] jEdit: -l flag
- Next by Date: Re: [isabelle] making use of star
- Previous by Thread: [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