Re: [isabelle] FUN verses PRIMREC
Something like this question was discussed recently:
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 |] ==>
> 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
> 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