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



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é



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