Re: [isabelle] apply proof method to all subgoals



On 10.04.2011 13:48, Alex Katovsky wrote:
This is probably a very basic question, so I apologize if I'm not
reading the tutorial carefully enough. I have this lemma

lemma "(∀ x . A ⟶ B) ∧ (∀ y . C ⟶ D) ∧ (∀ x . E ⟶ F)"

and from this I want to generate the three subgoals

1. ⋀x. A ⟹ B
2. ⋀y. C ⟹ D
3. ⋀x. E ⟹ F

If you want to prove this lemma by proving the three goals mentioned above, the idiomatic way to would probably be something like the following:

lemma "(∀ x . A ⟶ B) ∧ (∀ y . C ⟶ D) ∧ (∀ x . E ⟶ F)"
proof -
  { have "ALL x. A -> B" <some proof> }
  moreover
  { have "ALL y. C -> D" <some proof> }
  moreover
  { have "ALL x. E -> F" <some proof> }
  ultimately
  show ?thesis by auto
qed

Regards,
  Lars





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