Re: [isabelle] Isar syntax question



On 17.07.2014 00:00, Vadim Zaliva wrote:
> I am learning Isar and have another naive question on the syntax:
> I am trying to do something like this in Isar:
>
> 1: lemma
> 2:   shows "not something"
> 3: proof(rule ccontr)
> 4:  assume "something"
> 5:  thus False proof cases
> 6: 	...
> 7:   qed
> 8: qed
Have a look ath the proof state after "proof (rule ccontr)". The
precondition is "~~ something". Your assumption "something" does not
unify with this, so you get an error message as soon as you try to
discharge a proof obligation with show (or thus).

(Actually, it would be nice if the system would actually warn you about
this probable error at the assume statement).

You can either assume "~~something", or -- which is nicer -- do not use
the rule "ccontr" here. You just need "notI" (which is actually the
default rule, so changing line 3 to just "proof" should make everything
go through).
> and get "*** Failed to refine any pending goal" error around line 5
>
> Why this does not work? Something like this works instead:
>
> lemma
>   shows "not something"
> proof
>  assume "something" 
>  hence False proof cases
>  	...
>    qed
>   thus False by simp
> qed
The important difference is not the split into hence/thus (which is
indeed entirely unnecessary), but "proof (rule ccontr)" vs just "proof"
(which is equivalent here to "proof (rule notI)".

Have a look at both rules by doing "print_statement ccontr notI".

Best regards, Lars




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