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, 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"
   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 MHonArc.