[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
   "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
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.