Re: [isabelle] Completeness of patterns for mutually recursive function definitions



Hi Amy,

For mutual recursive definitions, the function package combines the two functions into one using a sum type. For your proof, you therefore first have to distinguish whether you are in the left or right branch, e.g., by case distinction on x. For the completeness part (first subgoal), the following works:

apply(unfold regular1_def regular2_def)
apply(atomize_elim)
apply(case_tac x) (* new *)
apply(auto)

Mutual recursion also adds four new cases where you have to prove consistency of the projections from the sum type. In your case,
the following solves all of them:

apply(auto simp add: fun_eq_iff intro: arg_cong)

Hope this helps,
Andreas


On 12/03/13 15:11, Amy Furniss wrote:
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.