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