Theory Kauffman_Matrix
section‹Kauffman Matrix and Kauffman Bracket- Definitions and Properties›
theory Kauffman_Matrix
imports
Matrix_Tensor.Matrix_Tensor
Link_Algebra
"HOL-Computational_Algebra.Polynomial"
"HOL-Computational_Algebra.Fraction_Field"
begin
section‹Rational Functions›
text‹intpoly is the type of integer polynomials›
type_synonym intpoly = "int poly"
lemma eval_pCons: "poly (pCons 0 1) x = x"
using poly_1 poly_pCons by auto
lemma pCons2:" (pCons 0 1) ≠ (1::int poly)"
using eval_pCons poly_1 zero_neq_one by metis
definition var_def: "x = (pCons 0 1)"
lemma non_zero:"x ≠ 0"
using var_def pCons_eq_0_iff zero_neq_one by (metis)
text‹rat$\_$poly is the fraction field of integer polynomials. In other
words, it is the type of rational functions›
type_synonym rat_poly = "intpoly fract"
text‹A is defined to be x/1, while B is defined to be 1/x›
definition var_def1:"A = Fract x 1"
definition var_def2: "B = Fract 1 x"
lemma assumes "b ≠ 0" and "d ≠ 0"
shows "Fract a b = Fract c d ⟷ a * d = c * b"
using eq_fract assms by auto
lemma A_non_zero:"A ≠ (0::rat_poly)"
unfolding var_def1
proof(rule ccontr)
assume 0:" ¬ (Fract x 1 ≠ (0::rat_poly)) "
then have "Fract x 1 = (0::rat_poly)"
by auto
moreover have "(0::rat_poly) = Fract (0::intpoly) (1::intpoly)"
by (metis Zero_fract_def)
ultimately have "Fract x (1::intpoly) = Fract (0::intpoly) (1::intpoly)"
by auto
moreover have "(1::intpoly) ≠ 0"
by auto
ultimately have "x*(1::intpoly) = (0::intpoly)*(1::intpoly)"
using eq_fract by metis
then have "x = (0::intpoly)"
by auto
then show False using non_zero by auto
qed
lemma mult_inv_non_zero:
assumes "(p::rat_poly) ≠ 0"
and "p*q = (1::rat_poly)"
shows "q ≠ 0"
using assms by auto
abbreviation rat_poly_times::"rat_poly ⇒ rat_poly ⇒ rat_poly"
where
"rat_poly_times p q ≡ p*q"
abbreviation rat_poly_plus::"rat_poly ⇒ rat_poly ⇒ rat_poly"
where
"rat_poly_plus p q ≡ p+q"
abbreviation rat_poly_inv::"rat_poly ⇒ rat_poly"
where
"rat_poly_inv p ≡ (- p)"
interpretation rat_poly:semiring_0 "rat_poly_plus" 0 "rat_poly_times"
by (unfold_locales)
interpretation rat_poly:semiring_1 1 "rat_poly_times" "rat_poly_plus" 0
by (unfold_locales)
lemma mat1_equiv:"mat1 (1::nat) = [[(1::rat_poly)]]"
by (simp add:mat1I_def vec1I_def)
text‹rat$\_$poly is an interpretation of the locale plus\_mult›