Re: [isabelle] attribute: rule_format
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,
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"
blah blah blah
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)
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.
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.
I think that hypothesis substitution might be unrelated.
This archive was generated by a fusion of
Pipermail (Mailman edition) and