Hi Jasmin, > First, LFP needs these five theories from "Library": > > Library/Wfrec.thy > Library/Infinite_Set.thy > Library/Order_Relation.thy > Library/Order_Union.thy > Library/Zorn.thy > > GFP also needs one more theory from "Library": > > Library/Sublist.thy > > Then LFP and GFP need the following cardinals theories (all by Popescu & > Traytel): > > Cardinals/Fun_More_FP.thy > Cardinals/Order_Relation_More_FP.thy > Cardinals/Wellfounded_More_FP.thy > Cardinals/Wellorder_Relation_FP.thy > Cardinals/Wellorder_Embedding_FP.thy > Cardinals/Constructions_on_Wellorders_FP.thy > Cardinals/Cardinal_Order_Relation_FP.thy > Cardinals/Cardinal_Arithmetic_FP.thy > > For completeness, these are the theories that are genuinely part of LFP: > > BNF/BNF_Util.thy > BNF/BNF_Def.thy > BNF/Basic_BNFs.thy > BNF/BNF_Comp.thy > BNF/BNF_FP_Base.thy > BNF/BNF_LFP.thy > > And part of GFP: > > BNF/Equiv_Relations_More.thy > BNF/BNF_GFP.thy >
a huge bunch indeed, but I am sure you will find ways to work this out.
From a theoretic point of view it is a little bit – irritating that so
much stuff is needed to issue something so fundamental as datatypes, but
similar opinions have been held about blast in its beginning.
Have you already thought about bootstrap order? If the datatype
construction demands already lists, there is a problem ;-)…
All the best,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
