Re: [isabelle] FUN verses PRIMREC



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.