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?

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.