[isabelle-dev] Auxiliary contexts again

[Andreas Lochbihler]

Hi Makarius,

Thanks for improving the auxiliary contexts.

 > The first three are should somehow work in Isabelle/18cb42182d3e, the
 > others are still unclear.  Are there further issues still pending?

Yes, in combination with type classes, there are still some strange behaviours. 
Here's an example, it refers to 875ed58b3b65:

context ord begin

definition foo :: "'a => 'a => bool" where "foo p n = (n < p)"
definition foo2 :: "'a => bool" where "foo2 p = foo p p"

context fixes p :: 'a begin
definition bar :: "'a => bool" where "bar n = (n < p)"
definition bar2 :: "bool" where "bar2 = bar p"

declare [[show_sorts]] (* 1 *)
term foo
term bar

end
end

(* 2 *)
thm foo_def
thm bar_def

a) The definition of bar2 fails with a type unification error because 'a is not 
of sort ord. Defining foo2, however, works fine. This can also be seen when 
inspecting foo's and bar's type: In (* 1 *), "term foo" prints
"foo" :: "'a :: type => 'a :: type => bool"
and "term bar" prints
"ord_class.bar" :: "'b :: ord => 'b :: ord => bool"

b) In (* 2 *), foo and bar both refer to the global constants foo and bar with 
sort constraint ord. However, "thm foo_def" prints

foo (?p :: ?'a :: ord) (?n :: ?'a :: ord) = (?n < ?p)

whereas "thm bar_def" prints

ord.bar op < (?p :: ?'a :: ord) (?n :: ?'a :: ord) = (?n < ?p)

which is the wrong theorem, i.e., lemmas such as
"bar p n = (n < p)" are unprovable.

Hope this helps,
Andreas

-- 
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft