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

theory Lattice_Syntax_Copy imports Lattice_Syntax begin
end

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,
thy')) thys);

fun begin_thy pp name imports =
  if name = "" orelse name = draftN then error ("Bad theory name: " ^
quote name)
  else
    let
      val parents = maximal_thys (distinct eq_thy imports);
      ...

- Brian





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