Re: [isabelle] Difficulties with Isar proofs and fix



On Tue, 26 Feb 2008, Denis Bueno wrote:

> >  Thank you all for your replies.  While I digest them, attached is the
> >  theory, so that you can play with it.  It requires the LList2 library
> >  (lazy, infinite lists) available at
> >  http://afp.sourceforge.net/entries/Lazy-Lists-II.shtml.  I'd
> >  appreciate any comments on my theory.
> 
> Well, I've completed the theorem I was having trouble with.  It is
> quite a bit longer than the apply-style proof, though much clearer.
> Any comments that would help me improve its readability and
> conciseness are welcome.

I've started to look at your proofs, which are quite impressive as your 
second attempt in Isar reasoning only.

One reason why things turn out a bit long is the general strategy of 
reducing things to predicate logic first, exposing it in the text, and 
then blasting your way through the thicked of quantifiers.  Even in your 
apply scripts, there have been these unfoldings of Pow_def, subset_def 
etc. followed by blast.

By proving derived natural deduction rules (and declaring them to the 
system as intro/elim, simp/iff etc.) you can work more smoothly without 
the detour through the object-logic.  This simplifies both apply scripts 
and Isar texts.

Moreover, in proper Isar you can usually avoid extra ``boiler plate 
statements'' like ``have EX x. P x'' before continuing to ``obtain x 
where P x'' --- the latter alone is usually sufficient.  Here is a 
concrete example from your proof of theorem proposition_1_oif:

    fix T :: property
    assume T_st: "T : Prop" "T ~: [[S]]"

    have t_is: "EX t:T. t ~: S"
    proof -
      from T_st have T_not_under_S: "~(T <= S)"
        unfolding property_lift_def by blast
      thus ?thesis unfolding subset_def by blast
    qed
    then obtain t where t_st: "t : T" "t ~: S" ..

Here t_is is only ever used to obtain the subsequent t.  The above 
hava/obtain part can be simplified as follows:

    from `T ~: [[S]]` have "~ T <= S"  by (simp add: property_lift_def)
    then obtain t where t_st: "t : T" "t ~: S" by blast

In fact you can also finish the obtain directly in one blow:

    from `T ~: [[S]]` obtain t where t_st: "t : T" "t ~: S"
      by (auto simp add: property_lift_def)

(Here I've merely applied the heuristic that auto somehow combines simp 
and blast.)

Isar is better at exploiting the power of automated reasoning than apply 
scripts, because the effect can be limited to clearly delimited 
sub-problems.

Readability should also be kept in mind, of course.  The challenge (and 
high art) in composing good Isar proofs is to expose just the relevant 
bits in the text, and manage to get it accepted by the proof tools.


	Makarius






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