Re: [isabelle] FUN verses PRIMREC
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?
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"
> "rev N = N" |
> "rev (S a b c) = S (rev c) (rev b) (rev a)"
> fun frev :: "T \<Rightarrow> T"
> "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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and