Sascha Kehrli (Aug 04 2025 at 18:54): Sascha Kehrli (Aug 04 2025 at 18:54):I'm writing a logic atop Pure with its own object-level equality. I have lots of theorems of the form "complicated lhs = simple rhs" which I'd like to use as simplifying rules. It seems this is not possible, as the simplifier works with meta-level equality only, right? Does every object logic need to implement its own simplifier/rewrite engine? Or can you 'hook into' the simplifier? I did already write a simplifier which takes a theorem, extracts its lhs and rhs, recursively finds a match for the lhs in a term and then applies the axioms for equality substitution and discharges the resulting subgoal with the theorem used for rewriting. Is this anywhere close to an idiomatic approach? I could still profit from existing infrastructure to be sublinear in the number of rewrite theorems. I'm really sorry if this is all the wrong place for a question like this.
Mathias Fleury (Aug 04 2025 at 18:56):I am confused by your question. There is a pure simplifier (Pure.simp) which should work also in your case
Sascha Kehrli (Aug 04 2025 at 18:58):It seems it only accepts rewrite rules using meta-level equality, which none of my rewrite rules use. They all use object-level equality. How can I circumvent that.
Mathias Fleury (Aug 04 2025 at 18:58):Ah, you mean that you have an equality that cannot be converted to ==?
Sascha Kehrli (Aug 04 2025 at 18:58):Yes.
Sascha Kehrli (Aug 04 2025 at 18:59):But maybe it is idiomatic to not do what I do (is object-level equality usually convertible to meta-level equality == ?) and I would be glad about a pointer like that as well
Mathias Fleury (Aug 04 2025 at 19:00):As far as I know, the simplifier only works for meta-equality (it is a limitation of Isabelle's simplifier)
Sascha Kehrli (Aug 04 2025 at 19:01):Do HOL and other object logics all have their own simplifier then?
Mathias Fleury (Aug 04 2025 at 19:03):No, in HOL = can be converted to ==
Mathias Fleury (Aug 04 2025 at 19:03):same in ZF
Mathias Fleury (Aug 04 2025 at 19:04):And if you look at ~~//Tools/eqsubst.ML, the first thing that happen is:
(* changes object "=" to meta "==" which prepares a given rewrite rule *)
fun prep_meta_eq ctxt =
Simplifier.mksimps ctxt #> map Drule.zero_var_indexes;
Thanks! Seems I should seek compatibility with meta equality then.
Manuel Eberl (Sep 12 2025 at 15:48):There's supposedly a draft version of a tool to do rewriting modulo arbitrary congruences by @Simon Roßkopf, but it's been a draft version for a long time at this point. :smile:
Manuel Eberl (Sep 12 2025 at 15:48):Not sure if it's specific to HOL though. Although I see no reason why it should be.
irvin (Sep 12 2025 at 16:24):Has there been a measure of slow down? Transitive is a kernel primitive in most HOL family theorem provers. Even HOL-light which was aiming for minimal inference rules has it.
irvin (Sep 12 2025 at 16:37):Also HOL4's simplifier supports rewriting with arbitrary preorders. see
8.5.6.6 of the description manual for a user guide https://github.com/HOL-Theorem-Prover/HOL/releases/download/trindemossen-2/trindemossen-2-description.pdf
you might want to look at the code here https://github.com/HOL-Theorem-Prover/HOL/tree/develop/src/simp/src
irvin (Sep 12 2025 at 16:47):The idea behind it isn't too hard you just need to provide a equivalent of Thm.reflexive and Conv.then_conv. Thm.reflexive is needed to discharge assumptions of congruence rules where no progress has been made.
Last updated: Sep 13 2025 at 12:36 UTC