[isabelle] lattice syntax problems (OR: what does it mean to merge two theories?)
I have recently noticed some weird/undesirable behavior with regards
to lattice syntax. Exploring this issue brings up some fundamental
questions about what it really means for Isabelle to merge two
As many of you may know, HOL/Lattices.thy defines infix syntax for
various lattice operations, including binary "inf" and "sup"; but then
it uses "no_notation" to erase this syntax at the end of the file, to
avoid using up so many precious symbols. Users who want to use the
syntax can import it from HOL/Library/Lattice_Syntax, like this:
theory Scratch imports "~~/src/HOL/Library/Lattice_Syntax" begin
term "x \<sqinter> y" (* parses as "inf x y" *)
When I wrote my Free Boolean Algebra AFP entry (which makes heavy use
of the lattice syntax) I followed what seemed to be the best practice,
and used "no_notation" to delete the syntax again.
I expected that users of my Free_Boolean_Algebra library would be able
to use the lattice syntax (if they chose to do so) by importing
Library/Lattice_Syntax again. Unfortunately this does not work!
term "x \<sqinter> y"
*** Inner lexical error at: \<sqinter> y (line 7 of
*** Failed to parse term
*** At command "term" (line 7 of "/home/brianh/Documents/Isabelle/Scratch.thy")
I thought that when you say "theory C imports A B begin", Isabelle
should actually merge theories A and B. In particular, any input
syntax that exists in either theory A or theory B should be available
in theory C. But that is not the case here! The syntax in
Lattice_Syntax is completely ignored.
Evidently, Isabelle assumes that merging Lattice_Syntax +
Free_Boolean_Algebra will be equal to the Free_Boolean_Algebra theory
by itself (because Lattice_Syntax is an ancestor theory of
Free_Boolean_Algebra) and optimizes away the actual theory merge. But
this is an invalid assumption.
This archive was generated by a fusion of
Pipermail (Mailman edition) and