Re: [isabelle] Length of Proofs
On Fri, 23 Nov 2012, Jeremy Dawson wrote:
There is an ambiguity here between Isar (the language and its grammar)
and Isar (the design/structure, ie, methods, facts, etc).
The "plus" is much more than be discussed on such a mail thread. It also
depends on the imagination of users, what they make out of the vast
formal environment that Isabelle gives you today (as of current
There is indeed an ambiguity: "Isar" can mean several things at several
scales looking at it. And the "Isar framework" is still more vast and
spacious than the things mentioned in the paragraph above.
Obviously, nothing that has been implemented in Standard ML couldn't be
packaged in a way to make it convenient for users to use by calling
Standard ML functions. The fact that the developers have not done so
doesn't add to the merits of Isar (the language and its grammar).
The Isar proof method called "tactic" actually presents the ML name space
to the user in a way that you can write nostalgic tactic expressions right
into your Isar proofs. E.g. like this:
lemma "A & B --> B & A"
apply (tactic "rtac impI 1")
apply (tactic "etac conjE 1")
apply (tactic "rtac conjI 1")
apply (tactic "ALLGOALS atac")
So it is basically the same like in 1993, just with some extra boiler
plate. There is no practical point to use the above in reality, though.
This archive was generated by a fusion of
Pipermail (Mailman edition) and