Re: [isabelle] Problem with mutual recursive primrecs



Sven,

datatype phi2 =
  Fin
  | Con "phi2 option"

Your datatype has nested recursion: The recursive occurrence occurs under the "option" type. Isabelle internally expresses this with a mutual recursion and requires you to express your primrecs with mutual recursion of a certain fixed form. The funny error messages you are getting are because you are not following that schema.

Section 3.4.2 in the Tutorial describes nested recursion of datatypes, and primrecs about such types.

The "fun" command is much more liberal about the form of the definitions, but proving termination can be an issue.

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)"

Obviously they *are* mutually recursive, but primrec is confused because you are not following the schema: "f1 (Con f)" should call "f2 f".

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

The same, but the confusion is slightly different, so you get a different error (from a different component of the system).

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)"
*)

The automatic termination prover does not deal very well with nested datatypes yet. Section 4 of the (separate) tutorial on functions explains how to do termination proofs manually. You should also read Section 5 about mutual recursive functions.

Hope this helps

Alex





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.