Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Incomplete abbreviation folding in stacked abb...

Email Gateway (Dec 29 2024 at 16:36):

From: Alexander Pach <alexander.pach@tum.de>
Dear Users,

during writing, I stumbled upon the following unexpected incomplete
abbreviation foldings:

lemma test: "monotone_on A P Q f" sorry
thm test[of "UNIV" "(≤)" "(≤)"] (*Expected ‹mono ?f›, is ‹mono_on UNIV
?f› *)
thm test[of _ "(≤)" "(≥)"] (*Expected ‹antimono_on ?A ?f›, is
‹monotone_on ?A (≤) (λx y. y ≤ x) ?f› *)
thm test[of UNIV "(≤)" "(≥)"] (*Expected ‹antimono ?f›, is ‹monotone_on
?A (≤) (λx y. y ≤ x) ?f›*)
thm test[of UNIV "(<)" "(<)"] (*Expected ‹strict_mono ?f›, is
‹strict_mono_on UNIV ?f›*)
thm test[of _ "(<)" "(>)"] (*Expected ‹strict_antimono_on ?A ?f›, is
‹monotone_on ?A (<) (λx y. y < x) ?f›*)

all other foldings were as expected.
Moreover,

term ‹antimono_on›  (is ‹"λA. monotone_on A (≤) (λx y. y ≤ x)"›)
term ‹strict_antimono_on› (*is ‹"λA. monotone_on A (<) (λx y. y < x)"› *)

get expanded, while mono, mono_on, monotone, antimono, antimono_on,
strict_mono, strict_mono_on don't.

At last, i noticed that strict_antimono is not defined, is this intentional?

This behaviour appears in Isabelle2024 as well as isabelle-dev (tested
with bac9b067c768).

Kind regards,
Alexander

smime.p7s

Last updated: Jan 04 2025 at 20:18 UTC