Theory Mod_Type_Connect
section ‹A new bridge to convert theorems from JNF to HOL Analysis and vice-versa,
based on the @{text "mod_type"} class›
theory Mod_Type_Connect
imports
Perron_Frobenius.HMA_Connect
Rank_Nullity_Theorem.Mod_Type
Gauss_Jordan.Elementary_Operations
begin
text ‹Some lemmas on @{text "Mod_Type.to_nat"} and @{text "Mod_Type.from_nat"} are added to have
them with the same names as the analogous ones for @{text "Bij_Nat.to_nat"}
and @{text "Bij_Nat.to_nat"}.›
lemma inj_to_nat: "inj to_nat" by (simp add: inj_on_def)
lemmas from_nat_inj = from_nat_eq_imp_eq
lemma range_to_nat: "range (to_nat :: 'a :: mod_type ⇒ nat) = {0 ..< CARD('a)}"
by (simp add: bij_betw_imp_surj_on mod_type_class.bij_to_nat)
text ‹This theory is an adaptation of the one presented in @{text "Perron_Frobenius.HMA_Connect"},
but for matrices and vectors where indexes have the @{text "mod_type"} class restriction.
It is worth noting that some definitions still use the old abbreviation for HOL Analysis
(HMA, from HOL Multivariate Analysis) instead of HA. This is done to be consistent with
the existing names in the Perron-Frobenius development›
context includes vec.lifting
begin
end
definition from_hma⇩v :: "'a ^ 'n :: mod_type ⇒ 'a Matrix.vec" where
"from_hma⇩v v = Matrix.vec CARD('n) (λ i. v $h from_nat i)"
definition from_hma⇩m :: "'a ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ 'a Matrix.mat" where
"from_hma⇩m a = Matrix.mat CARD('nr) CARD('nc) (λ (i,j). a $h from_nat i $h from_nat j)"
definition to_hma⇩v :: "'a Matrix.vec ⇒ 'a ^ 'n :: mod_type" where
"to_hma⇩v v = (χ i. v $v to_nat i)"
definition to_hma⇩m :: "'a Matrix.mat ⇒ 'a ^ 'nc :: mod_type ^ 'nr :: mod_type " where
"to_hma⇩m a = (χ i j. a $$ (to_nat i, to_nat j))"
lemma to_hma_from_hma⇩v[simp]: "to_hma⇩v (from_hma⇩v v) = v"
by (auto simp: to_hma⇩v_def from_hma⇩v_def to_nat_less_card)
lemma to_hma_from_hma⇩m[simp]: "to_hma⇩m (from_hma⇩m v) = v"
by (auto simp: to_hma⇩m_def from_hma⇩m_def to_nat_less_card)
lemma from_hma_to_hma⇩v[simp]:
"v ∈ carrier_vec (CARD('n)) ⟹ from_hma⇩v (to_hma⇩v v :: 'a ^ 'n :: mod_type) = v"
by (auto simp: to_hma⇩v_def from_hma⇩v_def to_nat_from_nat_id)
lemma from_hma_to_hma⇩m[simp]:
"A ∈ carrier_mat (CARD('nr)) (CARD('nc)) ⟹ from_hma⇩m (to_hma⇩m A :: 'a ^ 'nc :: mod_type ^ 'nr :: mod_type) = A"
by (auto simp: to_hma⇩m_def from_hma⇩m_def to_nat_from_nat_id)
lemma from_hma⇩v_inj[simp]: "from_hma⇩v x = from_hma⇩v y ⟷ x = y"
by (intro iffI, insert to_hma_from_hma⇩v[of x], auto)
lemma from_hma⇩m_inj[simp]: "from_hma⇩m x = from_hma⇩m y ⟷ x = y"
by(intro iffI, insert to_hma_from_hma⇩m[of x], auto)
definition HMA_V :: "'a Matrix.vec ⇒ 'a ^ 'n :: mod_type ⇒ bool" where
"HMA_V = (λ v w. v = from_hma⇩v w)"
definition HMA_M :: "'a Matrix.mat ⇒ 'a ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ bool" where
"HMA_M = (λ a b. a = from_hma⇩m b)"
definition HMA_I :: "nat ⇒ 'n :: mod_type ⇒ bool" where
"HMA_I = (λ i a. i = to_nat a)"
context includes lifting_syntax
begin
lemma Domainp_HMA_V [transfer_domain_rule]:
"Domainp (HMA_V :: 'a Matrix.vec ⇒ 'a ^ 'n :: mod_type ⇒ bool) = (λ v. v ∈ carrier_vec (CARD('n )))"
by(intro ext iffI, insert from_hma_to_hma⇩v[symmetric], auto simp: from_hma⇩v_def HMA_V_def)
lemma Domainp_HMA_M [transfer_domain_rule]:
"Domainp (HMA_M :: 'a Matrix.mat ⇒ 'a ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ bool)
= (λ A. A ∈ carrier_mat CARD('nr) CARD('nc))"
by (intro ext iffI, insert from_hma_to_hma⇩m[symmetric], auto simp: from_hma⇩m_def HMA_M_def)
lemma Domainp_HMA_I [transfer_domain_rule]:
"Domainp (HMA_I :: nat ⇒ 'n :: mod_type ⇒ bool) = (λ i. i < CARD('n))" (is "?l = ?r")
proof (intro ext)
fix i :: nat
show "?l i = ?r i"
unfolding HMA_I_def Domainp_iff
by (auto intro: exI[of _ "from_nat i"] simp: to_nat_from_nat_id to_nat_less_card)
qed
lemma bi_unique_HMA_V [transfer_rule]: "bi_unique HMA_V" "left_unique HMA_V" "right_unique HMA_V"
unfolding HMA_V_def bi_unique_def left_unique_def right_unique_def by auto
lemma bi_unique_HMA_M [transfer_rule]: "bi_unique HMA_M" "left_unique HMA_M" "right_unique HMA_M"
unfolding HMA_M_def bi_unique_def left_unique_def right_unique_def by auto
lemma bi_unique_HMA_I [transfer_rule]: "bi_unique HMA_I" "left_unique HMA_I" "right_unique HMA_I"
unfolding HMA_I_def bi_unique_def left_unique_def right_unique_def by auto
lemma right_total_HMA_V [transfer_rule]: "right_total HMA_V"
unfolding HMA_V_def right_total_def by simp
lemma right_total_HMA_M [transfer_rule]: "right_total HMA_M"
unfolding HMA_M_def right_total_def by simp
lemma right_total_HMA_I [transfer_rule]: "right_total HMA_I"
unfolding HMA_I_def right_total_def by simp
lemma HMA_V_index [transfer_rule]: "(HMA_V ===> HMA_I ===> (=)) ($v) ($h)"
unfolding rel_fun_def HMA_V_def HMA_I_def from_hma⇩v_def
by (auto simp: to_nat_less_card)
lemma HMA_M_index [transfer_rule]:
"(HMA_M ===> HMA_I ===> HMA_I ===> (=)) (λ A i j. A $$ (i,j)) index_hma"
by (intro rel_funI, simp add: index_hma_def to_nat_less_card HMA_M_def HMA_I_def from_hma⇩m_def)
lemma HMA_V_0 [transfer_rule]: "HMA_V (0⇩v CARD('n)) (0 :: 'a :: zero ^ 'n:: mod_type)"
unfolding HMA_V_def from_hma⇩v_def by auto
lemma HMA_M_0 [transfer_rule]:
"HMA_M (0⇩m CARD('nr) CARD('nc)) (0 :: 'a :: zero ^ 'nc:: mod_type ^ 'nr :: mod_type)"
unfolding HMA_M_def from_hma⇩m_def by auto
lemma HMA_M_1[transfer_rule]:
"HMA_M (1⇩m (CARD('n))) (mat 1 :: 'a::{zero,one}^'n:: mod_type^'n:: mod_type)"
unfolding HMA_M_def
by (auto simp add: mat_def from_hma⇩m_def from_nat_inj)
lemma from_hma⇩v_add: "from_hma⇩v v + from_hma⇩v w = from_hma⇩v (v + w)"
unfolding from_hma⇩v_def by auto
lemma HMA_V_add [transfer_rule]: "(HMA_V ===> HMA_V ===> HMA_V) (+) (+) "
unfolding rel_fun_def HMA_V_def
by (auto simp: from_hma⇩v_add)
lemma from_hma⇩v_diff: "from_hma⇩v v - from_hma⇩v w = from_hma⇩v (v - w)"
unfolding from_hma⇩v_def by auto
lemma HMA_V_diff [transfer_rule]: "(HMA_V ===> HMA_V ===> HMA_V) (-) (-)"
unfolding rel_fun_def HMA_V_def
by (auto simp: from_hma⇩v_diff)
lemma from_hma⇩m_add: "from_hma⇩m a + from_hma⇩m b = from_hma⇩m (a + b)"
unfolding from_hma⇩m_def by auto
lemma HMA_M_add [transfer_rule]: "(HMA_M ===> HMA_M ===> HMA_M) (+) (+) "
unfolding rel_fun_def HMA_M_def
by (auto simp: from_hma⇩m_add)
lemma from_hma⇩m_diff: "from_hma⇩m a - from_hma⇩m b = from_hma⇩m (a - b)"
unfolding from_hma⇩m_def by auto
lemma HMA_M_diff [transfer_rule]: "(HMA_M ===> HMA_M ===> HMA_M) (-) (-) "
unfolding rel_fun_def HMA_M_def
by (auto simp: from_hma⇩m_diff)
lemma scalar_product: fixes v :: "'a :: semiring_1 ^ 'n :: mod_type"
shows "scalar_prod (from_hma⇩v v) (from_hma⇩v w) = scalar_product v w"
unfolding scalar_product_def scalar_prod_def from_hma⇩v_def dim_vec
by (simp add: sum.reindex[OF inj_to_nat, unfolded range_to_nat])
lemma [simp]:
"from_hma⇩m (y :: 'a ^ 'nc :: mod_type ^ 'nr:: mod_type) ∈ carrier_mat (CARD('nr)) (CARD('nc))"
"dim_row (from_hma⇩m (y :: 'a ^ 'nc:: mod_type ^ 'nr :: mod_type)) = CARD('nr)"
"dim_col (from_hma⇩m (y :: 'a ^ 'nc :: mod_type ^ 'nr:: mod_type )) = CARD('nc)"
unfolding from_hma⇩m_def by simp_all
lemma [simp]:
"from_hma⇩v (y :: 'a ^ 'n:: mod_type) ∈ carrier_vec (CARD('n))"
"dim_vec (from_hma⇩v (y :: 'a ^ 'n:: mod_type)) = CARD('n)"
unfolding from_hma⇩v_def by simp_all
lemma HMA_scalar_prod [transfer_rule]:
"(HMA_V ===> HMA_V ===> (=)) scalar_prod scalar_product"
by (auto simp: HMA_V_def scalar_product)
lemma HMA_row [transfer_rule]: "(HMA_I ===> HMA_M ===> HMA_V) (λ i a. Matrix.row a i) row"
unfolding HMA_M_def HMA_I_def HMA_V_def
by (auto simp: from_hma⇩m_def from_hma⇩v_def to_nat_less_card row_def)
lemma HMA_col [transfer_rule]: "(HMA_I ===> HMA_M ===> HMA_V) (λ i a. col a i) column"
unfolding HMA_M_def HMA_I_def HMA_V_def
by (auto simp: from_hma⇩m_def from_hma⇩v_def to_nat_less_card column_def)
lemma HMA_M_mk_mat[transfer_rule]: "((HMA_I ===> HMA_I ===> (=)) ===> HMA_M)
(λ f. Matrix.mat (CARD('nr)) (CARD('nc)) (λ (i,j). f i j))
(mk_mat :: (('nr ⇒ 'nc ⇒ 'a) ⇒ 'a^'nc:: mod_type^'nr:: mod_type))"
proof-
{
fix x y i j
assume id: "∀ (ya :: 'nr) (yb :: 'nc). (x (to_nat ya) (to_nat yb) :: 'a) = y ya yb"
and i: "i < CARD('nr)" and j: "j < CARD('nc)"
from to_nat_from_nat_id[OF i] to_nat_from_nat_id[OF j] id[rule_format, of "from_nat i" "from_nat j"]
have "x i j = y (from_nat i) (from_nat j)" by auto
}
thus ?thesis
unfolding rel_fun_def mk_mat_def HMA_M_def HMA_I_def from_hma⇩m_def by auto
qed
lemma HMA_M_mk_vec[transfer_rule]: "((HMA_I ===> (=)) ===> HMA_V)
(λ f. Matrix.vec (CARD('n)) (λ i. f i))
(mk_vec :: (('n ⇒ 'a) ⇒ 'a^'n:: mod_type))"
proof-
{
fix x y i
assume id: "∀ (ya :: 'n). (x (to_nat ya) :: 'a) = y ya"
and i: "i < CARD('n)"
from to_nat_from_nat_id[OF i] id[rule_format, of "from_nat i"]
have "x i = y (from_nat i)" by auto
}
thus ?thesis
unfolding rel_fun_def mk_vec_def HMA_V_def HMA_I_def from_hma⇩v_def by auto
qed
lemma mat_mult_scalar: "A ** B = mk_mat (λ i j. scalar_product (row i A) (column j B))"
unfolding vec_eq_iff matrix_matrix_mult_def scalar_product_def mk_mat_def
by (auto simp: row_def column_def)
lemma mult_mat_vec_scalar: "A *v v = mk_vec (λ i. scalar_product (row i A) v)"
unfolding vec_eq_iff matrix_vector_mult_def scalar_product_def mk_mat_def mk_vec_def
by (auto simp: row_def column_def)
lemma dim_row_transfer_rule:
"HMA_M A (A' :: 'a ^ 'nc:: mod_type ^ 'nr:: mod_type) ⟹ (=) (dim_row A) (CARD('nr))"
unfolding HMA_M_def by auto
lemma dim_col_transfer_rule:
"HMA_M A (A' :: 'a ^ 'nc:: mod_type ^ 'nr:: mod_type) ⟹ (=) (dim_col A) (CARD('nc))"
unfolding HMA_M_def by auto
lemma HMA_M_mult [transfer_rule]: "(HMA_M ===> HMA_M ===> HMA_M) (*) (**)"
proof -
{
fix A B :: "'a :: semiring_1 mat" and A' :: "'a ^ 'n :: mod_type ^ 'nr:: mod_type"
and B' :: "'a ^ 'nc :: mod_type ^ 'n:: mod_type"
assume 1[transfer_rule]: "HMA_M A A'" "HMA_M B B'"
note [transfer_rule] = dim_row_transfer_rule[OF 1(1)] dim_col_transfer_rule[OF 1(2)]
have "HMA_M (A * B) (A' ** B')"
unfolding times_mat_def mat_mult_scalar
by (transfer_prover_start, transfer_step+, transfer, auto)
}
thus ?thesis by blast
qed
lemma HMA_V_smult [transfer_rule]: "((=) ===> HMA_V ===> HMA_V) (⋅⇩v) (*s)"
unfolding smult_vec_def
unfolding rel_fun_def HMA_V_def from_hma⇩v_def
by auto
lemma HMA_M_mult_vec [transfer_rule]: "(HMA_M ===> HMA_V ===> HMA_V) (*⇩v) (*v)"
proof -
{
fix A :: "'a :: semiring_1 mat" and v :: "'a Matrix.vec"
and A' :: "'a ^ 'nc :: mod_type ^ 'nr :: mod_type" and v' :: "'a ^ 'nc :: mod_type"
assume 1[transfer_rule]: "HMA_M A A'" "HMA_V v v'"
note [transfer_rule] = dim_row_transfer_rule
have "HMA_V (A *⇩v v) (A' *v v')"
unfolding mult_mat_vec_def mult_mat_vec_scalar
by (transfer_prover_start, transfer_step+, transfer, auto)
}
thus ?thesis by blast
qed
lemma HMA_det [transfer_rule]: "(HMA_M ===> (=)) Determinant.det
(det :: 'a :: comm_ring_1 ^ 'n :: mod_type ^ 'n :: mod_type ⇒ 'a)"
proof -
{
fix a :: "'a ^ 'n :: mod_type^ 'n:: mod_type"
let ?tn = "to_nat :: 'n :: mod_type ⇒ nat"
let ?fn = "from_nat :: nat ⇒ 'n"
let ?zn = "{0..< CARD('n)}"
let ?U = "UNIV :: 'n set"
let ?p1 = "{p. p permutes ?zn}"
let ?p2 = "{p. p permutes ?U}"
let ?f= "λ p i. if i ∈ ?U then ?fn (p (?tn i)) else i"
let ?g = "λ p i. ?fn (p (?tn i))"
have fg: "⋀ a b c. (if a ∈ ?U then b else c) = b" by auto
have "?p2 = ?f ` ?p1"
by (rule permutes_bij', auto simp: to_nat_less_card to_nat_from_nat_id)
hence id: "?p2 = ?g ` ?p1" by simp
have inj_g: "inj_on ?g ?p1"
unfolding inj_on_def
proof (intro ballI impI ext, auto)
fix p q i
assume p: "p permutes ?zn" and q: "q permutes ?zn"
and id: "(λ i. ?fn (p (?tn i))) = (λ i. ?fn (q (?tn i)))"
{
fix i
from permutes_in_image[OF p] have pi: "p (?tn i) < CARD('n)" by (simp add: to_nat_less_card)
from permutes_in_image[OF q] have qi: "q (?tn i) < CARD('n)" by (simp add: to_nat_less_card)
from fun_cong[OF id] have "?fn (p (?tn i)) = from_nat (q (?tn i))" .
from arg_cong[OF this, of ?tn] have "p (?tn i) = q (?tn i)"
by (simp add: to_nat_from_nat_id pi qi)
} note id = this
show "p i = q i"
proof (cases "i < CARD('n)")
case True
hence "?tn (?fn i) = i" by (simp add: to_nat_from_nat_id)
from id[of "?fn i", unfolded this] show ?thesis .
next
case False
thus ?thesis using p q unfolding permutes_def by simp
qed
qed
have mult_cong: "⋀ a b c d. a = b ⟹ c = d ⟹ a * c = b * d" by simp
have "sum (λ p.
signof p * (∏i∈?zn. a $h ?fn i $h ?fn (p i))) ?p1
= sum (λ p. of_int (sign p) * (∏i∈UNIV. a $h i $h p i)) ?p2"
unfolding id sum.reindex[OF inj_g]
proof (rule sum.cong[OF refl], unfold mem_Collect_eq o_def, rule mult_cong)
fix p
assume p: "p permutes ?zn"
let ?q = "λ i. ?fn (p (?tn i))"
from id p have q: "?q permutes ?U" by auto
from p have pp: "permutation p" unfolding permutation_permutes by auto
let ?ft = "λ p i. ?fn (p (?tn i))"
have fin: "finite ?zn" by simp
have "sign p = sign ?q ∧ p permutes ?zn"
using p fin proof (induction rule: permutes_induct)
case id
show ?case by (auto simp: sign_id[unfolded id_def] permutes_id[unfolded id_def])
next
case (swap a b p)
then have ‹permutation p›
using permutes_imp_permutation by blast
let ?sab = "Transposition.transpose a b"
let ?sfab = "Transposition.transpose (?fn a) (?fn b)"
have p_sab: "permutation ?sab" by (rule permutation_swap_id)
have p_sfab: "permutation ?sfab" by (rule permutation_swap_id)
from swap(4) have IH1: "p permutes ?zn" and IH2: "sign p = sign (?ft p)" by auto
have sab_perm: "?sab permutes ?zn" using swap(1-2) by (rule permutes_swap_id)
from permutes_compose[OF IH1 this] have perm1: "?sab o p permutes ?zn" .
from IH1 have p_p1: "p ∈ ?p1" by simp
hence "?ft p ∈ ?ft ` ?p1" by (rule imageI)
from this[folded id] have "?ft p permutes ?U" by simp
hence p_ftp: "permutation (?ft p)" unfolding permutation_permutes by auto
{
fix a b
assume a: "a ∈ ?zn" and b: "b ∈ ?zn"
hence "(?fn a = ?fn b) = (a = b)" using swap(1-2)
by (auto simp add: from_nat_eq_imp_eq)
} note inj = this
from inj[OF swap(1-2)] have id2: "sign ?sfab = sign ?sab" unfolding sign_swap_id by simp
have id: "?ft (Transposition.transpose a b ∘ p) = Transposition.transpose (?fn a) (?fn b) ∘ ?ft p"
proof
fix c
show "?ft (Transposition.transpose a b ∘ p) c = (Transposition.transpose (?fn a) (?fn b) ∘ ?ft p) c"
proof (cases "p (?tn c) = a ∨ p (?tn c) = b")
case True
thus ?thesis by (cases, auto simp add: o_def swap_id_eq)
next
case False
hence neq: "p (?tn c) ≠ a" "p (?tn c) ≠ b" by auto
have pc: "p (?tn c) ∈ ?zn" unfolding permutes_in_image[OF IH1]
by (simp add: to_nat_less_card)
from neq[folded inj[OF pc swap(1)] inj[OF pc swap(2)]]
have "?fn (p (?tn c)) ≠ ?fn a" "?fn (p (?tn c)) ≠ ?fn b" .
with neq show ?thesis by (auto simp: o_def swap_id_eq)
qed
qed
show ?case unfolding IH2 id sign_compose[OF p_sab ‹permutation p›] sign_compose[OF p_sfab p_ftp] id2
by (rule conjI[OF refl perm1])
qed
thus "signof p = of_int (sign ?q)" by simp
show "(∏i = 0..<CARD('n). a $h ?fn i $h ?fn (p i)) =
(∏i∈UNIV. a $h i $h ?q i)" unfolding
range_to_nat[symmetric] prod.reindex[OF inj_to_nat]
by (rule prod.cong[OF refl], unfold o_def, simp)
qed
}
thus ?thesis unfolding HMA_M_def
by (auto simp: from_hma⇩m_def Determinant.det_def det_def)
qed
lemma HMA_mat[transfer_rule]: "((=) ===> HMA_M) (λ k. k ⋅⇩m 1⇩m CARD('n))
(Finite_Cartesian_Product.mat :: 'a::semiring_1 ⇒ 'a^'n :: mod_type^'n :: mod_type)"
unfolding Finite_Cartesian_Product.mat_def[abs_def] rel_fun_def HMA_M_def
by (auto simp: from_hma⇩m_def from_nat_inj)
lemma HMA_mat_minus[transfer_rule]: "(HMA_M ===> HMA_M ===> HMA_M)
(λ A B. A + map_mat uminus B) ((-) :: 'a :: group_add ^'nc:: mod_type^'nr:: mod_type
⇒ 'a^'nc:: mod_type^'nr:: mod_type ⇒ 'a^'nc:: mod_type^'nr:: mod_type)"
unfolding rel_fun_def HMA_M_def from_hma⇩m_def by auto
lemma HMA_transpose_matrix [transfer_rule]:
"(HMA_M ===> HMA_M) transpose_mat transpose"
unfolding transpose_mat_def transpose_def HMA_M_def from_hma⇩m_def by auto
lemma HMA_invertible_matrix_mod_type[transfer_rule]:
"((Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'n :: mod_type ^ 'n :: mod_type
⇒ _) ===> (=)) invertible_mat invertible"
proof (intro rel_funI, goal_cases)
case (1 x y)
note rel_xy[transfer_rule] = "1"
have eq_dim: "dim_col x = dim_row x"
using Mod_Type_Connect.dim_col_transfer_rule Mod_Type_Connect.dim_row_transfer_rule rel_xy
by fastforce
moreover have "∃A'. y ** A' = mat 1 ∧ A' ** y = mat 1"
if xB: "x * B = 1⇩m (dim_row x)" and Bx: "B * x = 1⇩m (dim_row B)" for B
proof -
let ?A' = "Mod_Type_Connect.to_hma⇩m B:: 'a :: comm_ring_1 ^ 'n :: mod_type^ 'n :: mod_type"
have rel_BA[transfer_rule]: "Mod_Type_Connect.HMA_M B ?A'"
by (metis (no_types, lifting) Bx Mod_Type_Connect.HMA_M_def eq_dim carrier_mat_triv dim_col_mat(1)
Mod_Type_Connect.from_hma⇩m_def Mod_Type_Connect.from_hma_to_hma⇩m index_mult_mat(3)
index_one_mat(3) rel_xy xB)
have [simp]: "dim_row B = CARD('n)" using Mod_Type_Connect.dim_row_transfer_rule rel_BA by blast
have [simp]: "dim_row x = CARD('n)" using Mod_Type_Connect.dim_row_transfer_rule rel_xy by blast
have "y ** ?A' = mat 1" using xB by (transfer, simp)
moreover have "?A' ** y = mat 1" using Bx by (transfer, simp)
ultimately show ?thesis by blast
qed
moreover have "∃B. x * B = 1⇩m (dim_row x) ∧ B * x = 1⇩m (dim_row B)"
if yA: "y ** A' = mat 1" and Ay: "A' ** y = mat 1" for A'
proof -
let ?B = "(Mod_Type_Connect.from_hma⇩m A')"
have [simp]: "dim_row x = CARD('n)" using rel_xy Mod_Type_Connect.dim_row_transfer_rule by blast
have [transfer_rule]: "Mod_Type_Connect.HMA_M ?B A'" by (simp add: Mod_Type_Connect.HMA_M_def)
hence [simp]: "dim_row ?B = CARD('n)" using dim_row_transfer_rule by auto
have "x * ?B = 1⇩m (dim_row x)" using yA by (transfer', auto)
moreover have "?B * x = 1⇩m (dim_row ?B)" using Ay by (transfer', auto)
ultimately show ?thesis by auto
qed
ultimately show ?case unfolding invertible_mat_def invertible_def inverts_mat_def by auto
qed
end
text ‹Some transfer rules for relating the elementary operations are also proved.›
context
includes lifting_syntax
begin
lemma HMA_swaprows[transfer_rule]:
"((Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ _)
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nr :: mod_type ⇒ _ )
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nr :: mod_type ⇒ _ )
===> Mod_Type_Connect.HMA_M)
(λA a b. swaprows a b A) interchange_rows"
by (intro rel_funI, goal_cases, auto simp add: Mod_Type_Connect.HMA_M_def interchange_rows_def)
(rule eq_matI, auto simp add: Mod_Type_Connect.from_hma⇩m_def Mod_Type_Connect.HMA_I_def
to_nat_less_card to_nat_from_nat_id)
lemma HMA_swapcols[transfer_rule]:
"((Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ _)
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nc :: mod_type ⇒ _ )
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nc :: mod_type ⇒ _ )
===> Mod_Type_Connect.HMA_M)
(λA a b. swapcols a b A) interchange_columns"
by (intro rel_funI, goal_cases, auto simp add: Mod_Type_Connect.HMA_M_def interchange_columns_def)
(rule eq_matI, auto simp add: Mod_Type_Connect.from_hma⇩m_def Mod_Type_Connect.HMA_I_def
to_nat_less_card to_nat_from_nat_id)
lemma HMA_addrow[transfer_rule]:
"((Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ _)
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nr :: mod_type ⇒ _ )
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nr :: mod_type ⇒ _ )
===> (=)
===> Mod_Type_Connect.HMA_M)
(λA a b q. addrow q a b A) row_add"
by (intro rel_funI, goal_cases, auto simp add: Mod_Type_Connect.HMA_M_def row_add_def)
(rule eq_matI, auto simp add: Mod_Type_Connect.from_hma⇩m_def Mod_Type_Connect.HMA_I_def
to_nat_less_card to_nat_from_nat_id)
lemma HMA_addcol[transfer_rule]:
"((Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ _)
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nc :: mod_type ⇒ _ )
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nc :: mod_type ⇒ _ )
===> (=)
===> Mod_Type_Connect.HMA_M)
(λA a b q. addcol q a b A) column_add"
by (intro rel_funI, goal_cases, auto simp add: Mod_Type_Connect.HMA_M_def column_add_def)
(rule eq_matI, auto simp add: Mod_Type_Connect.from_hma⇩m_def Mod_Type_Connect.HMA_I_def
to_nat_less_card to_nat_from_nat_id)
lemma HMA_multrow[transfer_rule]:
"((Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ _)
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nr :: mod_type ⇒ _ )
===> (=)
===> Mod_Type_Connect.HMA_M)
(λA i q. multrow i q A) mult_row"
by (intro rel_funI, goal_cases, auto simp add: Mod_Type_Connect.HMA_M_def mult_row_def)
(rule eq_matI, auto simp add: Mod_Type_Connect.from_hma⇩m_def Mod_Type_Connect.HMA_I_def
to_nat_less_card to_nat_from_nat_id)
lemma HMA_multcol[transfer_rule]:
"((Mod_Type_Connect.HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'nc :: mod_type ^ 'nr :: mod_type ⇒ _)
===> (Mod_Type_Connect.HMA_I :: _ ⇒'nc :: mod_type ⇒ _ )
===> (=)
===> Mod_Type_Connect.HMA_M)
(λA i q. multcol i q A) mult_column"
by (intro rel_funI, goal_cases, auto simp add: Mod_Type_Connect.HMA_M_def mult_column_def)
(rule eq_matI, auto simp add: Mod_Type_Connect.from_hma⇩m_def Mod_Type_Connect.HMA_I_def
to_nat_less_card to_nat_from_nat_id)
end
fun HMA_M3 where
"HMA_M3 (P,A,Q)
(P' :: 'a :: comm_ring_1 ^ 'nr :: mod_type ^ 'nr :: mod_type,
A' :: 'a ^ 'nc :: mod_type ^ 'nr :: mod_type,
Q' :: 'a ^ 'nc :: mod_type ^ 'nc :: mod_type) =
(Mod_Type_Connect.HMA_M P P' ∧ Mod_Type_Connect.HMA_M A A' ∧ Mod_Type_Connect.HMA_M Q Q')"
lemma HMA_M3_def:
"HMA_M3 A B = (Mod_Type_Connect.HMA_M (fst A) (fst B)
∧ Mod_Type_Connect.HMA_M (fst (snd A)) (fst (snd B))
∧ Mod_Type_Connect.HMA_M (snd (snd A)) (snd (snd B)))"
by (smt (verit, ccfv_SIG) HMA_M3.simps prod.collapse)
context
includes lifting_syntax
begin
lemma Domainp_HMA_M3 [transfer_domain_rule]:
"Domainp (HMA_M3 :: _⇒(_×('a::comm_ring_1^'nc::mod_type^'nr::mod_type)×_)⇒_)
= (λ(P,A,Q). P ∈ carrier_mat CARD('nr) CARD('nr) ∧ A ∈ carrier_mat CARD('nr) CARD('nc)
∧ Q ∈ carrier_mat CARD('nc) CARD('nc))"
proof -
let ?HMA_M3 = "HMA_M3::_⇒(_×('a::comm_ring_1^'nc::mod_type^'nr::mod_type)×_)⇒_"
have 1: "P ∈ carrier_mat CARD('nr) CARD('nr) ∧
A ∈ carrier_mat CARD('nr) CARD('nc) ∧ Q ∈ carrier_mat CARD('nc) CARD('nc)"
if "Domainp ?HMA_M3 (P,A,Q)" for P A Q
using that unfolding Domainp_iff by (auto simp add: Mod_Type_Connect.HMA_M_def)
have 2: "Domainp ?HMA_M3 (P,A,Q)" if PAQ: "P ∈ carrier_mat CARD('nr) CARD('nr)
∧ A ∈ carrier_mat CARD('nr) CARD('nc) ∧Q ∈ carrier_mat CARD('nc) CARD('nc)" for P A Q
proof -
let ?P = "Mod_Type_Connect.to_hma⇩m P::'a^'nr::mod_type^'nr::mod_type"
let ?A = "Mod_Type_Connect.to_hma⇩m A::'a^'nc::mod_type^'nr::mod_type"
let ?Q = "Mod_Type_Connect.to_hma⇩m Q::'a^'nc::mod_type^'nc::mod_type"
have "HMA_M3 (P,A,Q) (?P,?A,?Q)"
by (auto simp add: Mod_Type_Connect.HMA_M_def PAQ)
thus ?thesis unfolding Domainp_iff by auto
qed
have "fst x ∈ carrier_mat CARD('nr) CARD('nr) ∧ fst (snd x) ∈ carrier_mat CARD('nr) CARD('nc)
∧ (snd (snd x)) ∈ carrier_mat CARD('nc) CARD('nc)"
if "Domainp ?HMA_M3 x" for x using 1
by (metis (full_types) surjective_pairing that)
moreover have "Domainp ?HMA_M3 x"
if "fst x ∈ carrier_mat CARD('nr) CARD('nr) ∧ fst (snd x) ∈ carrier_mat CARD('nr) CARD('nc)
∧ (snd (snd x)) ∈ carrier_mat CARD('nc) CARD('nc)" for x
using 2
by (metis (full_types) surjective_pairing that)
ultimately show ?thesis by (intro ext iffI, unfold split_beta, metis+)
qed
lemma bi_unique_HMA_M3 [transfer_rule]: "bi_unique HMA_M3" "left_unique HMA_M3" "right_unique HMA_M3"
unfolding HMA_M3_def bi_unique_def left_unique_def right_unique_def
by (auto simp add: Mod_Type_Connect.HMA_M_def)
lemma right_total_HMA_M3 [transfer_rule]: "right_total HMA_M3"
unfolding HMA_M_def right_total_def
by (simp add: Mod_Type_Connect.HMA_M_def)
end
end