[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

Brian Huffman brianh at cs.pdx.edu
Mon Aug 22 17:06:11 CEST 2011

On Mon, Aug 22, 2011 at 8:01 AM, Lawrence Paulson <lp15 at 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

More information about the isabelle-dev mailing list