[isabelle-dev] New (Co)datatypes: Status & Plan 2

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20131118/ba8ecc01/attachment.sig>