[isabelle-dev] Experiments in best-first-search rewriter
bohuazhan at gmail.com
Sun Nov 2 16:56:27 CET 2014
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
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
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 9420 bytes
Desc: not available
More information about the isabelle-dev