[isabelle-dev] Experiments in best-first-search rewriter

[Bohua Zhan]

Hi, everyone

My name is Bohua Zhan, a postdoc in mathematics at MIT. I am
interested in doing some experiments in automated proof techniques in
Isabelle. I have been reading the documentations and existing code for
some time, but this is my first attempt at writing some code, so here
it is (attached).

I am trying to implement a simplifier / rewriter that uses
best-first-search instead of depth-first-search as the current simp
tactic does. This avoids a major problem with DFS simp: being trapped
into loops by rewriting rules that can be used back and forth or
repeatedly. This implementation memorizes terms that have already been
explored.

Two examples are given at the end: the first refers to the permutation
example in section 6.4 of the new Isabelle Cookbook manual, rewriting:

   pi1 . (c, pi2 . ((rev pi1) . d)
= (pi1 . c, pi1 . (pi2 . (rev pi1) . d))
= (pi1 . c, (pi1 . pi2) . (pi1 . ((rev pi1) . d)))
= (pi1 . c, (pi1 . pi2) . d)

avoiding the use of ".aux" (which I suppose is not the ideal solution).

The second example is simplification with ring axioms. I certainly
don't propose this is how it should be done, but just to test how
large an example this rewriter can handle without any domain-specific
knowledge.

Any suggestions? One major feature to be added is dealing with rules
with assumptions. I would especially like to see examples of hard
rewriting problems that come up in actual proof development.

Thanks,
Bohua
-------------- next part --------------
A non-text attachment was scrubbed...
Name: rewriter.thy
Type: application/octet-stream
Size: 9420 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20141102/625b9e02/attachment.obj>