*To*: Sven Schneider <svens at cs.tu-berlin.de>*Subject*: Re: [isabelle] Problem with mutual recursive primrecs*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Fri, 21 Mar 2008 12:22:59 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <47E24544.5060306@cs.tu-berlin.de>*References*: <47E24544.5060306@cs.tu-berlin.de>*User-agent*: Icedove 1.5.0.14pre (X11/20080208)

Sven,

datatype phi2 = Fin | Con "phi2 option"

section {* 3: f1,f2 call each other but they are not mutually recursive(primrecs).*}(* consts f1 :: "phi2 \<Rightarrow> phi2" f2 :: "phi2 option \<Rightarrow> phi2 option" primrec "f1 Fin = Fin""f1 (Con f) = Con (case f of None \<Rightarrow> None | Some x\<Rightarrow> f2 (Some x))""f2 None = None" "f2 (Some a) = Some (f1 a)"

section {* 4: f1,f2 call each other, they are not mutually recursive butthere is a circular dependency between them.*}

section {* 5: f1,f2 call each other but no termination argument is found.*} (* fun f1 :: "phi2 \<Rightarrow> phi2" and f2 :: "phi2 option \<Rightarrow> phi2 option" where "f1 Fin = Fin"| "f1 (Con f) = Con (case f of None \<Rightarrow> None | Some x\<Rightarrow> f2 (Some x))"| "f2 None = None" | "f2 (Some a) = Some (f1 a)" *)

Hope this helps Alex

**References**:**[isabelle] Problem with mutual recursive primrecs***From:*Sven Schneider

- Previous by Date: [isabelle] FMCAD 2008 Call For Papers
- Next by Date: [isabelle] E. W. Beth Dissertation Prize: 2008 call for submissions
- Previous by Thread: [isabelle] Problem with mutual recursive primrecs
- Next by Thread: [isabelle] LFM 2008 Call for Participation
- Cl-isabelle-users March 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list