[isabelle-dev] Isabelle/HOL axiom ext is redundant

[Makarius]

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