On Fri, 13 Nov 2009, Lucas Dixon wrote:
> I was really wondering what the principle was that makes "-->" and "ALL"
> fail (or be inappropriately convoluted) than using the meta-level
> connectives: is there a small example that illustrates it?
>
> My own understanding was that the meta-level of Isabelle, and the use of
> it by Isar, facilitated the genericity natural deduction-style
> reasoning. Generic proof tools can be written that work across logics.
>
> Makarius, if I understood correctly, was saying that these meta-level
> logical mechanisms have a utility even when just within one logic, but I
> didn't understand what this would be, except perhaps distinguishing
> between ND syntax and other logical syntax (which is my interpretation
> of Michael's reply).
Yes, this "distinguishing" is an important aspect. If we go back to Isar
calculations again, print_trans_rules will tell you that there are also
variants of modus ponens as part of the game. If you would dedicate -->
for (homegrown) transitivity rule outlines, you would somehow need to mark
such rules or even transitivity over --> as special.
Another example are plain intro/elim rules for -->:
impI: (A ==> B) ==> (A --> B)
mp: (A --> B) ==> (A ==> B)
The system can make sense out of them "declaratively". In pure Isar you
do not even need the "rule" vs. "erule" distinction in the text. By
collapsing the structure of the framework, you would only get amorphic
(A --> B) --> (A --> B).
Yet another example, which of a slightly different category. The
framework represents goal states via iterated ==> (another really nice
idea by Larry from 20 years ago). So A1 ==> A2 ==> C means subgoals A1
and A2 are sufficient to establish the main conclusion C. If C is itself
an implication, we get into problems. As an extra-logical solution one
could pass around the length of the initial prefix (here 2) that counts as
subgoals. Internally there are indeed some (awkward) ML operations like
that. It has turned out much more practical to internalize the goal
outline structure, this time using the "prop" marker (identity on
propositions), which is often printed as # in my papers.
The latter is rarely encountered in user space -- similar to
Pure.conjunction. So one could ask if !! ==> could be hidden like that as
well. In that case, the user would be limited to flat rules. One would
also need to come up with extra ideas do reprent more deeply nested things
like well-founded induction.
Makarius
