Email Gateway (Aug 19 2022 at 09:07): Email Gateway (Aug 19 2022 at 09:07):From: Lawrence Paulson <lp15@cam.ac.uk>
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 is retained only so that legacy proofs will continue to work.
Larry Paulson
Email Gateway (Aug 19 2022 at 09:18):From: Christian Sternagel <c-sterna@jaist.ac.jp>
What is the reason for "rule_format" not to touch HOL conjunction in
premises, i.e., why is, e.g., "A & B --> A" not transformed into "A ==>
B ==> A" by "rule_format"?
I often thought such a behavior useful. Is there another way of
replacing every HOL connective by an appropriate Pure connective (as far
as possible)?
cheers
chris
Email Gateway (Aug 19 2022 at 09:21):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 09:22):From: Randy Pollack <rpollack@inf.ed.ac.uk>
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.
abbreviation
he :: "bbS \<Rightarrow> bool"
where "he M == \<forall>(pi::name prm) X. F X M = F (pi\<bullet>X)
(pi\<bullet>M)"
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.
Randy
Email Gateway (Aug 19 2022 at 09:22):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Ideally all of our tools would care only about the semantics of the
rules we provide, rather than the specific syntactic arrangement. In
practice we are far from that, and conversion between logically
equivalent lemmas seems to be a fact of life.
For instance, it is sometimes useful to state a lemma "P ==> Q" to
exactly match an assumption "Q" of another rule and then resolve them
with OF. It may be convenient to state "Q" using --> and ALL rather than
==> and !! to ensure it is completely consumed with one OF.
I see [rule_format] as just a shorthand for one of the kinds of
conversions that are often needed. Often it's not the right one, and a
longhand [OF allI conjI ...] comes out.
I wonder if anonymous contexts are a (partial) solution to this problem,
for instance:
anonymous context begin
abbreviation (input) "P x y == ..."
abbreviation (input) "Q x y z == ..."
abbreviation (input) "R z == ..."
theorem foo: "P x y & Q x y z ==> R z"
proof
blah blah blah
qed
corollary foo_tupleD: "P x y ==> Q x y (x, y) ==> R (x, y)"
and foo_tupleI: "P (fst z) (snd z) ==> Q (fst z) (snd z) z ==> R z"
and foo_simp: "Q x y z ==> (P x y & R z) = P x y"
by (metis foo)
end
This is a generalisation of the Isar (is "?P x y & ?Q x y z --> ?R z")
which also allows easy statement of closely related corollaries.
I think that hypothesis substitution might be unrelated.
Yours,
Thomas.
Last updated: Apr 26 2024 at 20:16 UTC