On Mon, Aug 22, 2011 at 8:01 AM, Lawrence Paulson <l...@cam.ac.uk> wrote: > I've come across something strange in the file > isabelle/afp/devel/thys/DataRefinementIBP/Diagram.thy and was wondering if > anybody could think of an explanation. > > A proof works only if I insert before it the following: > > instance "set" :: (type) complete_boolean_algebra > proof > qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def Inf_bool_def > Sup_bool_def) > > this is strange because this exact text already appears in the file > Complete_Lattice.thy (I refer to Florian's version of HOL), which is imported > by Main, which is indirectly imported by Diagram. And just in case I was > mistaken on this last point, I modified Diagram to import Main explicitly, > just to be sure. This instance declaration is still necessary. > > I just don't get this. I thought that an instance declaration lasted for ever.
DataRefinementIBP/Preliminaries.thy contains the following line: class complete_boolean_algebra = distributive_complete_lattice + boolean_algebra So your instance proof above is for class Preliminaries.complete_boolean_algebra, while the instance in Complete_Lattice.thy is for the separate Complete_Lattice.complete_boolean_algebra class. - Brian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
