# [isabelle] Unnecessary Transitivity Assumption in Multiset Extension

Dear all,
recently, when using the multiset extension "mult" from
"~~/src/HOL/Library/Multiset", I noticed the following oddity:
The lemma
lemma one_step_implies_mult:
"trans r â J â {#} â âk â set_mset K. âj â set_mset J. (k, j) â r
â (I + K, I + J) â mult r"
requires transitivity of the underlying order, which I think is not
needed here. And indeed the proof of one_step_implies_mult is
using one_step_implies_mult_aux by blast
and one_step_implies_mult_aux, basically a object-level version
of one_step_implies_mult, reads
lemma one_step_implies_mult_aux:
"âI J K. size J = n â J â {#} â (âk â set_mset K. âj â set_mset J. (k, j) â r)
â (I + K, I + J) â mult r"
Is this intended?
Best,
Julian

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*