[isabelle] intro rule for &&&



Dear Isabelle,

When I type...

> lemma assumes "A ∧ B" shows "A" "B"
> using assms
> apply rule

...I obtain the following proof state...

> goal (2 subgoals):
>  1. A ⟹ B ⟹ A
>  2. B 

... which is insoluble. I think the "apply rule" step is using the conjE rule. Which rule should I apply in order to obtain the preferred proof state below? I briefly tried conjunctionI but that doesn't seem quite to fit.

> goal (2 subgoals):
>  1. A ⟹ B ⟹ A
>  2. A ⟹ B ⟹ B 

By the way, I know I can solve this lemma via auto; my question is pedagogical rather than practical.

cheers,
john




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