Email Gateway (Aug 19 2022 at 10:44): Email Gateway (Aug 19 2022 at 10:44):From: Amy Furniss <mjf29@leicester.ac.uk>
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
Email Gateway (Aug 19 2022 at 10:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 19 2022 at 10:44):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Amy,
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é
Last updated: Apr 19 2024 at 12:27 UTC