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"
from T_st have T_not_under_S: "~(T <= S)"
unfolding property_lift_def by blast
thus ?thesis unfolding subset_def by blast
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
Isar is better at exploiting the power of automated reasoning than apply
scripts, because the effect can be limited to clearly delimited
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and