[isabelle] Interpretation of abbreviation in type class context forgets parameters
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Interpretation of abbreviation in type class context forgets parameters
- From: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
- Date: Mon, 5 Oct 2015 09:53:25 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.2.0
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 *)
This archive was generated by a fusion of
Pipermail (Mailman edition) and