[isabelle-dev] Homology

[Lawrence Paulson]

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.

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