[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Wed Aug 24 20:37:10 CEST 2011
> 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.
print_classes should give sufficient data to find out what is going here.
The duplication is the same I was referring to a few days ago:
> Complete_Lattices.thy
> and
> http://afp.hg.sourceforge.net/hgweb/afp/afp/file/dce6fbc4d6c0/thys/DataRefinementIBP/Preliminaries.thy
> (btw. it took me considerable time to figure out how the class hierarchy
> for complete lattices should look like, just to see now that somebody
> else got to the same conclusion independently already).
Indeed the classes in DataRefinement are duplication of work now in
Complete_Lattice.thy and have already been marked by Brian as such.
Logically they are equivalent and can be removed.
Hope this helps,
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110824/a5ba824e/attachment.sig>
More information about the isabelle-dev
mailing list