HOL-Theorem-Prover
quotient simps cannot deal with conjuncts.
Theorem PAIR_MAP_I[simp,quotient_simp]:
(I ## I) = (I : 'a # 'b -> 'a # 'b) /\
((\x. x) ## (\x. x)) = ((\x. x) : 'a # 'b -> 'a # 'b)
Proof
simp[FUN_EQ_THM, FORALL_PROD]
QED
given a theorem like this declaring it with attribute quotient_simp causes it to fail due to not splitting up the theorems into
(I ## I) = (I : 'a # 'b -> 'a # 'b) and
((\x. x) ## (\x. x)) = ((\x. x) : 'a # 'b -> 'a # 'b)
If I include that text in my script file, I do not see a failure. Please be more precise with your "causes it to fail".
It seems to fail when the theorem is actually used. If you modify PAIR_MAP_I in pairTheory, it fails when it's seems to be used by the quotient library in resulting theories.
An actual test-case would be helpful. The theorems stored with quotient_simp are passed to PURE_REWRITE_RULE (see the treatment of parameters tyop_simps in src/quotient/src/quotient.sml) and PURE_REWRITE_RULE has no problem interpreting conjunctions when performing rewrites. Of course, the presence of the additional rewrite with the lambda-abstraction may break things.