Re: [isabelle] attribute: rule_format

I use "rule_format" for other than legacy purposes.  Here is an
example where I give a name to a (paramaterized) bool so that I can
use it in various ways.  Perhaps someone will show me a better way.

  he :: "bbS \<Rightarrow> bool"
  where "he M == \<forall>(pi::name prm) X. F X M = F (pi\<bullet>X)
abbreviation  (* F equivariant (relativised) *)
  HE :: "bool"
  where "HE == \<forall>M. bbL M \<longrightarrow> he M"
abbreviation  (* F equivariant (unrelativised) *)
  XHE :: "bool"
  where "XHE == \<forall>M. he M"

This doesn't just save typing for me; it saves checking for a reader
that all the uses are the same formula.  "rule_format" is used in
proving things about HE and XHE.

On Thu, Nov 15, 2012 at 9:46 AM, Makarius <makarius at> wrote:
> 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.