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 last.)


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.


	Makarius


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