[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.