[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.