Re: [isabelle] lattice syntax problems (OR: what does it mean to merge two theories?)
On Thu, Jul 28, 2011 at 9:26 AM, Lukas Bulwahn <bulwahn at in.tum.de> wrote:
> 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.
Loading and merging are separate things. I am not asking Isabelle to
*load* the same theory twice. I am merely asking Isabelle to *merge* a
theory with one of its ancestors.
> I guess the pragmatic solution is to ask your users to use a clone of
> Lattice_Syntax with a different name.
I am well aware of a workaround. All I have to do is create a dummy
empty theory file called "Lattice_Syntax_Copy" that imports
theory Lattice_Syntax_Copy imports Lattice_Syntax begin
Now, since Lattice_Syntax_Copy is not actually an ancestor of
Free_Boolean_Algebra, then Isabelle can be persuaded to do actually
merge them together.
theory Scratch imports Lattice_Syntax_Copy Free_Boolean_Algebra begin
term "x \<sqinter> y" (* this works *)
> 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.
Yes, a much nicer long-term solution would be something that would
make the whole no_notation/Lattice_Syntax.thy hack unnecessary.
But in the short term, it would be nice for theory imports to behave
in the way I expect (i.e. actually merge every theory in the import
list, without throwing any away). I tracked the problem to the
function Context.begin_thy in Pure/context.ML. The function
maximal_thys implents the ignore-ancestors-in-imports bug/feature:
fun maximal_thys thys =
thys |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy,
fun begin_thy pp name imports =
if name = "" orelse name = draftN then error ("Bad theory name: " ^
val parents = maximal_thys (distinct eq_thy imports);
This archive was generated by a fusion of
Pipermail (Mailman edition) and