Re: [isabelle] lattice syntax problems (OR: what does it mean to merge two theories?)



On 07/28/2011 05:28 PM, Brian Huffman wrote:
Hello all,

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
theories.

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!

theory Scratch
imports
   "~~/src/HOL/Library/Lattice_Syntax"
   "~/hg/afp/thys/Free-Boolean-Algebra/Free_Boolean_Algebra"
begin

term "x \<sqinter>  y"

*** Inner lexical error at: \<sqinter>  y (line 7 of
"/home/brianh/Documents/Isabelle/Scratch.thy")
*** 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.

Obviously, you cannot load a theory twice in Isabelle.
So, it is not only an optimization but an necessity not to load and merge the theory twice in your situation.

I guess the pragmatic solution is to ask your users to use a clone of Lattice_Syntax with a different name. The correct technical solution in Isabelle is a local context-aware infrastructure for syntax, which is just a little bit out of reach right now, but other people can probably describe the situation more in-depth than I can right now.


Lukas

- Brian







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