# [isabelle] mutually recursion problem

Dear Sir/Madam,
I am having problem in proving this lemma:
lemma coords_mono_point_poly:
"point_coords state \<subseteq>\<^sub>m point_coords (fst (point_poly p
state)) \<and>
line_coords state \<subseteq>\<^sub>m line_coords (fst (point_poly p
state))"
and
coords_mono_line_poly:
"point_coords state \<subseteq>\<^sub>m point_coords (fst (line_poly l
state)) \<and>
line_coords state \<subseteq>\<^sub>m line_coords (fst (line_poly l
state))"
proof (induct p and l arbitrary: state)
As you can see there are actually two lemmas, but they are "mutually
recursive" (because the functions point_poly and line_poly that I previously
defined are mutually recursive). The problem is that when i try to prove
like this, then this 'arbitrary:state' only affects the first lemma, but not
the second one, and that is not convenient at all. Any suggestions how to
solve this?
Yours faithfully,
Danijela Petrovic

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