# Re: [isabelle] finishing a proof

Alexander Kogtenkov wrote:
> "assume" is used to state what is used as a premise of a goal, and neither P
> nor Q are given, that's why the proof fails. So, instead of proving a fact relying
> on "assume" you can prove a fact relying on "if we assume...":
>
> proof -
> assume "P â (Q â R)"
> then have "Q â R" if p: P by (simp add: p)
> then have "R" if p: P and q: Q by (simp add: p q)
> then have "P â R" if q: Q by (simp add: q)
> then have "Q â (P â R)" by simp
> then show ?thesis by assumption
> qed
>
> Given that "simp" is too powerful and could be used to prove the original
> lemma right away, you can also use explicit rules:
>
> proof -
> assume "P â (Q â R)"
> then have "Q â R" if p: P using p by (rule mp)
> then have "R" if p: P and q: Q using q by (rule mp) (insert p)
> then have "P â R" if q: Q by (rule impI) (insert q)
> then show "Q â (P â R)" by (rule impI) qed
Thanks.
A question:
if I write
lemma assumes pqr: "P â (Q â R)" shows "Q â (P â R)"
proof -
assume "P â Q â R"
then have "Q â R" if p: P using p by (rule mp)
then have "R" if p: P and q: Q using q by (rule mp) (insert p)
then have "P â R" if q: Q by (rule impI) (insert q)
then have "Q â (P â R)" by (rule impI)
I have
have Q â P â R
proof (state)
this:
Q â P â R
goal (1 subgoal):
1. Q â P â R
which I guess should be trivial to solve but it resisted any attempt.
What is wrong here?
- Gergely

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