Re: [isabelle] Benchmark suite for Isabelle's `rewrite` tactic



On 15/10/2020 13:55, Zack Grannan wrote:
> 
> Is there a benchmark suite that tests the rewriting tactic of Isabelle or some
> references we can read how it works/performs?
> 
> We are implementing a rewrite tactic for Liquid Haskell and it would be great
> to compare it with Isabelle's.

I guess you mean the "simp" family of proof methods, or rather "The
Simplifier" behind it. The  isar-ref manual, section 9.3 has many explanations
about it, but you probably need some practical experience with it to see the
points.

It might also help to study the sources:

https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/Pure/raw_simplifier.ML
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/Pure/simplifier.ML

(You can read Isabelle/Pure sources in the Prover IDE by opening the central
ROOT.ML, which is also in the Documentation panel.)


Various people on this list can probably provide more concrete answers:
high-end users routinely tinker with the Simplifier setup.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.