Email Gateway (Aug 18 2022 at 17:54): Email Gateway (Aug 18 2022 at 17:54):From: Данијела Петровић <danijela.p9@gmail.com>
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
Email Gateway (Aug 18 2022 at 18:00):From: Lars Noschinski <noschinl@in.tum.de>
You probably need to give arbitrary a list for each of the goals,
separated by "and": So try using "arbitrary: state and state".
-- Lars
Last updated: Nov 21 2024 at 12:39 UTC