[isabelle-dev] New proof method "rewrite"

[Lars Noschinski]

On 09.04.2015 21:08, Makarius wrote:
> On Thu, 9 Apr 2015, Lars Noschinski wrote:
>
>> On 18.03.2015 15:16, Lars Noschinski wrote:
>>> commit 4ed50ebf5d36 adds a new proof method "rewrite". This is the
>>> pattern-based replacement for subst Christoph Traut and I presented at
>>> the last Isabelle Workshop [1]. For now, it lifes in
>>> ~~/src/HOL/Library/Rewrite and is still missing a proper documentation
>>> (but there are examples in ~~/src/HOL/ex/Rewrite_Examples).
>> I've used it now a bit to add annotations in program verification and
>> (contrary to my former intuition) found the order of the patterns to be
>> the wrong way around.
>>
>> If someone has used the rewrite method and has some opinions on that, I
>> would be glad to hear these.
>
> I haven't used it yet, although I looked a bit through the sources,
> just as a matter of pre-release routine.
>
> I also added a symbol assignment for \<hole> in the IsabelleText font
> and isabellesym.sty -- it is the result of spending 30min looking
> carefully through DejaVuSansMono and
> http://mirrors.ctan.org/info/symbols/comprehensive/symbols-a4.pdf --
> see now b911c8ba0b69.  LaTeX packages should not be overly exotic as
> rendering
> of Isabelle symbols -- hopefully wasysym.sty was a decent choice here.
Nice, this deals with the conflict I encountered a few days ago with the
use of the \<box> symbol in AutoCorres.
> Back to the actual topic of this thread: If you want to change the
> syntax for the release, there are a very few days left until the first
> release candidate is published, while the repository still remains in
> pre-forked state, probably until the end of next week.
>
> Technically, to have Parse.xthms1 before quasi-keywords like "at", you
> need some Scan.unless trickery, but it should be doable. 
> Method.sections also manages that with "add", "del" etc.
I was not clear above. I don't want to change the general syntax of
<position> <to> <rules>, but was contemplating whether the position
should read inside-out or outside-in. As I noted in my other mail, this
will have to wait for the next round.
> Here is also a command line to explore possibilities of true keywords,
> instead of quasi-keywords:
>
>   $ isabelle build -n -a -d '$AFP' -k at -k asm -k concl
>
> Note that outer syntax is now local to each theory, so as long as it
> is just a separate theory somewhere, one can be liberal.  Anything for
> main HOL needs more care, of course.  (For Eisbach we also have some
> open problems with keyword clashes still left to address, "concl" is
> one of them.)
The goal is definitely to have the tool end up in Main, so I will not
get too fancy with the syntax.

  -- Lars