Определение матрицы 3 на 3 в Isabelle

Question

Я новичок в использовании Isabelle для формального подтверждения. Я должен делать умножение между векторной и 3 на 3 матрицей.

Прямо сейчас, я могу определить 3 элемента вектора, используя эту команду

'consts x_vec :: "('a::real_vector) set ⇒ ('a ⇒ real×real×real) ⇒ bool"' 

Мой вопрос заключается в том, как определить 3 на 3 матрицы. Матрицей, над которой мне нужно работать, является инерциальная матрица.

Answer 1

В Archive of Formal Proofs имеется довольно развитая библиотека матриц.

Это особенно приятно, потому что различные размеры матрицы покрываются единой схемой типа, с предикатами для подпространств, как в математике.