Re: [isabelle] finishing a proof



The form "assumes-shows" separates facts, so if in the proof you want to rely on the facts from "assumes", you need to tell it by adding

ÂÂ using assms proof -

Then your version completes without an issue. (You can also use "pqr" instead of a general "assms" to refer to the particular fact.)

Another variant is to replace "assume" with the fact itself. In this case "using assms" is not required:

proof -
 Ânote pqr
ÂÂÂ...

Finally, you can just use "pqr" in the proof itself. Then neither "assume" nor "note" is required:

lemma assumes pqr: "P â (Q â R)" shows "Q â (P â R)"
proof -
Âhave "Q â R" if p: P using pqr p by (rule mp)
Âthen have "R" if p: P and q: Q using q by (rule mp) (insert p pqr)
Âthen have "P â R" if q: Q by (rule impI) (insert q pqr)
Âthen show "Q â (P â R)" by (rule impI) (insert pqr)
qed

Alexander Kogtenkov


>"Gergely Buday" <buday.gergely at uni-eszterhazy.hu>:
>
>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.