Ideas for simp trace

From Isabelle Community Wiki
Jump to navigation Jump to search

  • click on a symbol in the resulting term and trace back which rewrite rules where used to generate this symbol
  • click on a subterm of the start term to jump to the place where it is rewritten
  • which rewrite rules where used to /remove/ a assumption (often assumptions get removed which are then missing for the arith tactics)
  • why is certain conditional rewrite rule not applied, look at the simp trace of its conditions
    • in addition to "certain conditional rewrite rule": rewrite rules from specific theories (or rule sets like ring_simps)
    • which rewrite rules failed to apply at a particular intermediate step (perhaps also filtered by theories)
  • a option to get after a (successful) simp the set of rewrite rules that were applied, such that if I were to do (simp only: that_set), the command would get the same result. (similar to sledgehammer)
    • in the same spirit: report rules that have been added explicitly (via "add:" or "using", if this is possible to detect) but not used
  • search the trace for a particular rule