*To*: Ramana Kumar <rk436 at cam.ac.uk>*Subject*: Re: [isabelle] FUN verses PRIMREC*From*: Tim Kremann <twkrema at orion.ncsc.mil>*Date*: Sun, 8 Jan 2012 09:41:46 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAMej=273bR8H8YO509MgVGT1Q4sG8_On-7Dd0R+2VuKW8o057Q@mail.gmail.com>*References*: <E6621900-3ACA-4927-BF56-CF976424D6B0@orion.ncsc.mil> <CAMej=273bR8H8YO509MgVGT1Q4sG8_On-7Dd0R+2VuKW8o057Q@mail.gmail.com>

Thank you. However, I am still unclear after reading that thread. Its seems that for the thread example, which goes two levels deep (disallowed for primrec) that fun is the better technique rather than rewriting it to a primitive recursive form. However I have three questions: 1) Does using primrec offer any advantages when using certain tactics? 2) Why use primrec at all? 3) What is the best way to search the archives before posting a question? Thanks, Tim On Jan 7, 2012, at 7:14 PM, Ramana Kumar wrote: > Something like this question was discussed recently: https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-November/msg00040.html > > On Jan 8, 2012 3:59 AM, "Tim Kremann" <twkrema at orion.ncsc.mil> wrote: > As a test case I wrote a simple routine as both a primrec and fun. Here they are: > > datatype T = N | S T T T > > primrec rev :: "T \<Rightarrow> T" > where > "rev N = N" | > "rev (S a b c) = S (rev c) (rev b) (rev a)" > > fun frev :: "T \<Rightarrow> T" > where > "frev N = N" | > "frev (S a b c) = S (frev c) (frev b) (frev a)" > > Now when I look at rules generated, fun produces an induct and cases rule that primrec does not. > > tt.frev.cases: [| ?x = N ==> ?P; \<And> a b c. ?x = S a b c ==> ?P |] ==> ?P > tt.frev.induct: [| ?P N; \<And> a b c. [| ?P c; ?P b; ?P a |] ==> ?P (S a b c)|] ==> ?P ?a0.0 > tt.frev.simps(1): frev N = N > tt.frev.simps(2): frev (S ?a ?b ?c) = S (frev ?c) (frev ?b) (frev ?a) > > tt.rev.simps(1): tt.rev N = N > tt.rev.simps(2): tt.rev (S ?a ?b ?c) = S (tt.rev ?c) (tt.rev ?b) (tt.rev ?a) > > Is there a reason to chose one over the other???? I assume use of primrec verses fun affects how the case and induct tactics work. Is this true? > > Thanks, > Tim

**Follow-Ups**:**Re: [isabelle] FUN verses PRIMREC***From:*Lawrence Paulson

**References**:**[isabelle] FUN verses PRIMREC***From:*Tim Kremann

**Re: [isabelle] FUN verses PRIMREC***From:*Ramana Kumar

- Previous by Date: Re: [isabelle] FUN verses PRIMREC
- Next by Date: Re: [isabelle] FUN verses PRIMREC
- Previous by Thread: Re: [isabelle] FUN verses PRIMREC
- Next by Thread: Re: [isabelle] FUN verses PRIMREC
- Cl-isabelle-users January 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