Re: [isabelle] Length of Proofs



On Fri, 23 Nov 2012, Jeremy Dawson wrote:

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
Isabelle2012).

There is an ambiguity here between Isar (the language and its grammar) and Isar (the design/structure, ie, methods, facts, etc).

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")
  done

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.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.