[isabelle] Problem with mutual recursive primrecs



Hello mailinglist

I have a problem defining a mutually recursive primrec. My problem is of course more complex than the examples below. They are reduced versions.

_section_ 1
In this example it becomes obvious that primrec has a problem with case and option.

_section_ 2
In this example the same code as before is used but the fun (instead of the primrec) is capable to proof the termination.

_section_ 3
In this example the problem is more close to my problem and the primrec does not get the calls right. f1 and f2 indeed have calls to each other, therefore they should be at least mutually recursive... The message is a bit confusion in my opinion. At least if the real problem is that the primrec again cannot 'proof' termination.

_section_ 4
This example shows that f1 and f2 (defined as in section 3) depend on each other... This seems to be a contradiction to me. It seems that 'mutually recursive iff circular dependent' is incorrect (of course more than mutually recursion is necessary to be able to define a terminating function)?

_section_ 5
Using functions instead does not solve the problem. A termination argument is not found automaticly. Attempts to do it manually didn't resolve the problem.

_Questions_
If you haven't yet extracted any questions ;-) here they are:
1) What is the problem of the primrec exactly that the fun can resolve (section 1+2)?
2) How to prove termination and finish the definition in section 3-5?

Bye,
Sven


_CODE_

theory test
imports Main begin

datatype phi2 =
  Fin
  | Con "phi2 option"

section {* 1: f0 should be primrec but isn't. *}
(*
consts
  f0:: "phi2 \<Rightarrow> phi2"
primrec
  "f0 Fin = Fin"
"f0 (Con x) = (case x of None \<Rightarrow> Fin | (Some y) \<Rightarrow> Con (Some(f0 y)))"
*)
(*
*** Entity to be defined occurs on rhs
*** The error(s) above occurred in definition "f0_phi2_def":
*** "f0 \<equiv> phi2_rec_1 Fin (\<lambda>x xa. case x of None \<Rightarrow> Fin | Some y \<Rightarrow> Con (Some (f0 y))) undefined undefined"
*** At command "primrec".
*)

section {* 2: f3 (which is 'equal' to f0) is a function though. *}
fun f3:: "phi2 \<Rightarrow> phi2"
where
   "f3 Fin = Fin"
| "f3 (Con x) = (case x of None \<Rightarrow> Fin | (Some y) \<Rightarrow> Con (Some(f3 y)))"

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)"
*)
(*
*** Primrec definition error:
*** functions "test.f1", "test.f2"
*** are not mutually recursive
*** At command "primrec".
*)

section {* 4: f1,f2 call each other, they are not mutually recursive but there is a circular dependency between them.*}
(*
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))"
primrec
  "f2 None = None"
  "f2 (Some a) = Some (f1 a)"
*)
(*
*** Circular dependency of constant test.f1 -> test.f1
*** The error(s) above occurred in definition "f2_option_def":
***   "f2 \<equiv> option_rec None (\<lambda>a. Some (f1 a))"
*** At command "primrec".
*)

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)"
*)
(*
*** Unfinished subgoals: (..)
*)

end





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