[isabelle] Interpretation of abbreviation in type class context forgets parameters



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




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