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
rewriter.thy
Description: Binary data
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev