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