[isabelle-dev] Homology

[Dr A. Koutsoukou-Argyraki]

On 2019-04-09 11:59, Lawrence Paulson wrote:
> I’m not sure how to do this without drastically restructuring Analysis.
> 
> Maybe we could have separate “top theories” (analogous to Main vs
> Complex_Main) within Analysis. But then HOL-Analysis would still
> depend on HOL-Algebra.
> 
> Or Homology could be a new development, importing Analysis, but with a
> plan to move most of the Analysis material to other places later?
> Homology needs only about a third of the Analysis theories.

I would vote for Larry's last suggestion as it seems that Analysis is 
absorbing too much material,
also having all of Analysis to import Algebra is not so ideal.
I don't really have a feeling of how difficult it would be to move some 
Analysis material elsewhere (hopefully not too difficult??) but it seems 
like the best option to me

Best,
Angeliki

> 
> Larry
> 
>> On 9 Apr 2019, at 11:49, Dr A. Koutsoukou-Argyraki <ak2110 at cam.ac.uk> 
>> wrote:
>> 
>> why not leave it as a separate Homology library that would be 
>> importing both Analysis and Algebra for now?
>> It would then evolve into an Algebraic Topology library with time.
>> This would also reflect how a "real-life" math library would be 
>> organised.
>> 
>> i.e. : I would prefer your suggestion of breaking up Analysis into 
>> several modules some of which may need to port Homology (and thus 
>> Algebra too)
>> and some not (if I correctly understand what you mean).
>> Could this be done at a second stage in time for Isabelle 2020 ?
>> Would that be feasible?
>> 
>> Best,
>> Angeliki
>> 
>> 
>> On 2019-04-09 11:14, Lawrence Paulson wrote:
>>> I’ve completed porting HOL Light’s homology library, which many 
>>> people
>>> have requested, and I’m trying to install it now into Analysis. This
>>> will have one big consequence: Analysis will now import Algebra. This
>>> in turn affects all theories that depend on Analysis.
>>> An alternative may be to break up Analysis into several modules,
>>> though I don’t see how that can be done in time for the next release.
>>> Larry
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev