Re: [isabelle] attribute: rule_format
On Thu, 1 Nov 2012, Lawrence Paulson wrote:
I think it was just a little more difficult to implement, and never
necessary, because you could always write your original theorem in the
form P —> Q —> R rather than P & Q —> R. And this sort of thing was only
necessary for proof by induction anyway.
With the Isar induction methods, which had been around for several years
now, the rule_format attribute is quite unnecessary.
It was indeed considered legacy since day 1, when I introduced the
attribute to imitate the old qed_spec_mp feature of that time. This also
explains what it does and what not. Generally it would be hard to say
where to stop making a "rule format", and an important purpose of the
explicit Pure rule notation with !! and ==> is to make clear what the
intended rule structure really is, without guessing by the system.
Moreover, the somewhat odd joining of what is now called "rule attribute"
vs. "declaration attribute" in the same notation goes back to the ancient
times of imitating qed_spec_mp. It has been a partial success in getting
rid of many qed commands, but at the cost of some confusion about what
attributes really are. (I've made some tiny reforms here for
Isabelle2012, to provide proper static evaluation of rule attributes at
It is retained only so that legacy proofs will continue to work.
Occasionally, I entertain myself in trying to eliminate such old uses of
"rule_format", or rather do it while testing Isabelle/jEdit performance
and robustness. Unfortunately, it often fails, because compact HOL
connectives passed through induction produce different goals for tools
like "auto": having nested !! and ==> in the induction hypotheses fails
for some reasons that are unknown to me. Empirically I've always taken
this as a feature of auto, but it might be worth revisiting it.
Larry himself has pointed out such observations about auto privately to me
some months ago, when porting older ZF scripts.
Maybe the isabelle-dev thread on "Safe approach to hypothesis
substitution" by Thomas Sewell from 2 years ago points into a direction to
improve the situation, or maybe it is unrelated.
This archive was generated by a fusion of
Pipermail (Mailman edition) and