Isabelle中等价幺半群同构定义为何无法被auto正常处理？

我正在对Isabelle中的Jacobson_Basic_Algebra做小幅改进：

• 原定义里，monoid_isomorphism直接被定义为满足复合交换、单位元交换的双射映射
• 我把定义拆成了两部分：
  1. monoid_morphism：只要求满足复合交换
  2. monoid_isomorphism：基于monoid_morphism加上双射性质
• 已经证明了单位元交换是可推导的定理，不再作为公理

尽管新旧定义逻辑等价、语法上看起来也一致，但原定理inverse_monoid_isomorphism的auto证明完全失效，试了好几种拆分方式都碰到这个问题。

可能的解决思路 #

• 检查自动推理规则适配性：拆分后的定义可能改变了术语的内部表示，导致auto依赖的化简、引入/消除规则没正确匹配上，可以手动确认相关规则是否被注册
• 显式引入关键定理：单位元交换现在是定理而非公理，auto可能不会自动调用它，试试把这个定理添加到auto的规则集，或者在证明里显式引用
• 排查定义细节差异：哪怕看起来语法一致，也可能存在隐式类型约束、参数顺序、展开方式的细微差别，导致auto的搜索路径中断，可尝试用print_theorems对比新旧定义生成的规则
• 调整证明策略：原证明可能依赖原定义里的单位元交换公理，拆分后可以先unfolding monoid_isomorphism_def展开定义，再一步步调用已证的单位元交换定理来完成证明

内容的提问来源于stack exchange，提问作者alagris