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.