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.
Last updated: Aug 20 2025 at 20:23 UTC