*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Completeness of patterns for mutually recursive function definitions*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Wed, 13 Mar 2013 13:46:32 +0100*Cc*: Amy Furniss <mjf29 at leicester.ac.uk>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <514071A3.3080208@inf.ethz.ch>*References*: <513F378E.7020105@le.ac.uk> <514071A3.3080208@inf.ethz.ch>

Dear Amy, > 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) If you prefer to do it manually, you can instead use the following proof via fun_cong. proof - fix t f assume "(λx. CON) = (λx. ABS (t x) (f x))" from fun_cong[OF this] show False by simp next fix t f assume "(λx. FCON) = (λx. FAPP (t x) (f x))" from fun_cong[OF this] show False by simp next fix t f assume "(λx. x) = (λx. ABS (t x) (f x))" from fun_cong[OF this, of CON] show False by simp next fix t :: "type1 ⇒ type2" and f ta fa assume "(λx. FAPP (t x) (f x)) = (λx. FAPP (ta x) (fa x))" from fun_cong[OF this] have id: "t = ta" "f = fa" by (intro ext, auto) from id show "Sum_Type.Projl (fun1_fun2_sumC (Inl f)) = Sum_Type.Projl (fun1_fun2_sumC (Inl fa))" by simp from id show "Sum_Type.Projr (fun1_fun2_sumC (Inr t)) = Sum_Type.Projr (fun1_fun2_sumC (Inr ta))" by simp next fix t :: "type1 ⇒ type2" and f ta fa assume "(λx. ABS (t x) (f x)) = (λx. ABS (ta x) (fa x))" from fun_cong[OF this] have id: "t = ta" "f = fa" by (intro ext, auto) from id show "Sum_Type.Projr (fun1_fun2_sumC (Inr t)) = Sum_Type.Projr (fun1_fun2_sumC (Inr ta))" by simp from id show "Sum_Type.Projl (fun1_fun2_sumC (Inl f)) = Sum_Type.Projl (fun1_fun2_sumC (Inl fa))" by simp qed But of course, Andreas' proof is easier to type and maintain. Cheers, René

**References**:**[isabelle] Completeness of patterns for mutually recursive function definitions***From:*Amy Furniss

**Re: [isabelle] Completeness of patterns for mutually recursive function definitions***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Completeness of patterns for mutually recursive function definitions
- Next by Date: [isabelle] word wrapping in jEdit output panel
- Previous by Thread: Re: [isabelle] Completeness of patterns for mutually recursive function definitions
- Next by Thread: [isabelle] Lifting a partial definition to a quotient type
- Cl-isabelle-users March 2013 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