# [isabelle] Linear algebra formalisation

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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*