*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] lattice syntax problems (OR: what does it mean to merge two theories?)*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Thu, 28 Jul 2011 08:28:24 -0700*Sender*: huffman.brian.c at gmail.com

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

**Follow-Ups**:

- Previous by Date: Re: [isabelle] the state of the lattice theories
- Next by Date: Re: [isabelle] lattice syntax problems (OR: what does it mean to merge two theories?)
- Previous by Thread: Re: [isabelle] [isabelle-dev] simplification theorems generated for records:
- Next by Thread: Re: [isabelle] lattice syntax problems (OR: what does it mean to merge two theories?)
- Cl-isabelle-users July 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list