Email Gateway (Aug 22 2022 at 11:40): Email Gateway (Aug 22 2022 at 11:40):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Isabelle developers,
Interpretations treat abbreviations in a type class context strangely. Here's an example
for Isabelle2015. In List.thy, the function sort is defined as an abbreviation of sort_key
(%x. x) in the type class context linorder.
When I now interpret the linorder locale with the dual operations with prefix "dual", both
names "dual.sort" and "dual.sort_key" come into scope. The latter "dual.sort_key" indeed
refers to "linorder.sort_key (op >=)". However, "dual.sort" does NOT denote
"linorder.sort_key (op >=) (%x. x)", but "linorder.sort_key (op <=) (%x. x)", i.e., the
parameter instantiation of the interpretation is lost.
I find this extremely counter-intuitive, because dual.sort sorts ascendingly and
dual.sort_key sorts descendingly! Can this be changed such that dual.sort also refers to
the sorting with the dual operation?
theory Scratch imports "~~/src/HOL/Main" begin
interpretation dual!: linorder "op ≥" "op > :: _ :: linorder ⇒ _" by(rule dual_linorder)
lemma "dual.sort [1,2] = [1,2 :: int]" by simp (* ascendingly! *)
lemma "dual.sort_key (λx. x) [1,2] = [2,1 :: int]" by simp (* descendingly *)
end
Best,
Andreas
Last updated: Apr 26 2024 at 12:28 UTC