Email Gateway (Aug 19 2022 at 15:20): Email Gateway (Aug 19 2022 at 15:20):From: Holden Lee <hl422@cam.ac.uk>
I've finished a formalisation of some basic linear algebra using locales,
available here:
https://dl.dropboxusercontent.com/u/27883775/work/Isabelle/LinearAlgebra.zip.
It includes (note that some concepts are actually written in module as they
also apply there)
- basic definitions: linear combinations, span, linear independence
- linear transformations
- direct sum of vector spaces, sum of subspaces
- the replacement theorem
- existence of bases in finite-dimensional vector spaces
- rank-nullity theorem
In the process, I also proved some basic facts about rings, modules, and
fields that seem to be missing, as well as finite sums in monoids/modules.
Note that infinite-dimensional vector spaces are supported, but "dim" is
only supported for finite-dimensional vector spaces.
As I alluded to in my previous email, I had trouble getting the
automation/simplification to work in my favor, so some of the writeups are
hacky/inconsistent.
[One "hack" I discovered near the end was: to prevent an infinite loop of
simplification from expanding "->" (Pi_I') and trying to show (a x \in
carrier K) by showing it is the image of something in A->B, create a "dummy
definition" Pi2 == Pi, and add simplification rules Pi_simp whose premises
involve Pi2 rather than Pi, and then do:
apply(drule Pi_implies_Pi2)+ (*"flags" all the assumptions piped in so they
aren't expanded.*)
apply(simp add: Pi_simp)
I would hope there is some way to do this more "natively."]
Any comments are appreciated, especially in streamlining the proofs.
Eventually I would like these developments to be integrated into the
Isabelle algebra library, so let me know about the protocol for this.
Cheers,
Holden
Last updated: May 07 2024 at 04:19 UTC