[isabelle] Completeness of patterns for mutually recursive function definitions



Dear all,

I have a pair of mutually-recursive functions which are defined using
the function command, and I'm struggling to prove the completeness of
patterns for the definition. If I remove one of the recursive calls (so
that they are no longer mutually recursive) and separate out the
functions, the completeness of patterns for both functions is easily
solved by atomize_elim, auto, but when they are defined together this no
longer works. Can anybody please suggest how I might go about solving
this pattern completeness subgoal?

Thanks,

Amy

---

theory Example
imports Main
begin

datatype type1 = CON | ABS type2 type1
and type2 = FCON | FAPP type2 type1

definition regular1 :: "(type1 \<Rightarrow> type1) \<Rightarrow> bool"
where
"regular1 \<equiv> \<lambda>z. (z = (\<lambda>x. x))
  | (z = (\<lambda>x. CON))
  | (\<exists>f t. z = (\<lambda>x. ABS (t x) (f x)))"

definition regular2:: "(type1 \<Rightarrow> type2) \<Rightarrow> bool" where
"regular2 \<equiv> \<lambda>z. (z = (\<lambda>x. FCON))
  | (\<exists>f t. z = (\<lambda>x. FAPP (t x) (f x)))"

function fun1 :: "(type1 \<Rightarrow> type1) \<Rightarrow> type1"
and fun2 :: "(type1 \<Rightarrow> type2) \<Rightarrow> type2" where
"fun1 (\<lambda>x. x) = CON"
| "fun1 (\<lambda>x. CON) = CON"
| "fun1 (\<lambda>x. ABS (t x) (f x)) = ABS (fun2 t) (fun1 f)"
| "\<not>regular1 i \<Longrightarrow> fun1 i = CON"
| "fun2 (\<lambda>x. FCON) = FCON"
| "fun2 (\<lambda>x. FAPP (t x) (f x)) = FAPP (fun2 t) (fun1 f)"
| "\<not>regular2 i \<Longrightarrow> fun2 i = FCON"
apply(unfold regular1_def regular2_def)
apply(atomize_elim)
apply(auto)
sorry

end





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