Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unnecessary Transitivity Assumption in Multise...

Email Gateway (Aug 22 2022 at 13:01):

From: Julian Nagele <julian.nagele@uibk.ac.at>
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

Email Gateway (Aug 22 2022 at 13:01):

From: Tobias Nipkow <nipkow@in.tum.de>
I have removed the superfluous assumption, thanks.

The AFP entry Decreasing-Diagrams also contains superfluous "trans r"
assumptions because it uses one_step_implies_mult. The proofs still work, but
the authors may want to update their theories anyway.

Tobias
smime.p7s

Last updated: Apr 25 2024 at 16:19 UTC