# [isabelle] FUN verses PRIMREC

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.*