Re: [isabelle] schematic variables
On Wed, 10 Aug 2011, Mamoun FILALI-AMINE wrote:
After discussing with Sascha Boehme, it seems to be technically
impossible to match a goal against a pattern after unfolding with
some rewrite rule:
definition "foo x = bar x x"
have "foo (f x)" (is "foo ?X") [pattern is possible]
unfolding foo_def (is "bar ?X _") [pattern is not possible]
Strictly speaking it is not *technically* impossible, merely outside the
scope of the structured proof language of Isar. Structure emerges by
restricting low-level technical operations to something that conforms to
certain higher concepts. Take ML as programming language for example: it
allows much less operations than machine language, and is thus far more
powerful -- the compiler and runtime system can do smart things for you.
One of the key principles of Isar is the distinction of the proof text and
the proof state. Information may flow only from text to state, not the
other way round.
Anyway, your example reminds me of the Ltac tactic definition language of
Coq, with matching against the goal state. After so many years, Isar
still lacks a structured proof method definition language. You have to
use plain ML for that (via the 'method_setup' command, which is not really
When drafting the first versions of the Isar proof language, I was aware
of this omission of a method definition language. It made certain things
easier, and the quality of proofs (readability and maintainability) has
actually improved by making the language more restrictive.
Structured proof method definition languages are still an interesting area
of research, but I see more potential for the future in sophisticated
editing support of Isar text in the Prover IDE. (The current
Isabelle/jEdit implementation is a very modest beginning in that
This can be illustrated by looking again at what Coq has to offer. Since
I am myself located in France, I have the privilege to discuss with many
Coq users first-hand. I see two main movements of power-users at the
(1) Hardcore Ltac scripting according Chlipala.
(This reminds me a lot of a tactical style that was popular in
Isabelle/HOL in the late 1990-ies, e.g. see HOL/Bali or
(2) Quick in-place tactic composition via ssreflect, according to
Gonthier. His language assigns a meaning to almost every character
in the ASCII set, to make typing as efficient as possible. This
wins more and more converts, and recent versions of Matita seem to
have adopted it as well.
Instead of imitating any of the above, I would eventually like to see a
Prover IDE that allows very quick proof composition, but producing proper
Isar proof text instead of recording the keystrokes in the script. This
would be analogous to a typical Java IDE: a relatively weak language (here
Isar) is composed and maintained by relatively strong tooling.
This archive was generated by a fusion of
Pipermail (Mailman edition) and