section ‹Connecting HMA-matrices with JNF-matrices›
text ‹The following theories provide a connection between the type-based representation of vectors
and matrices in HOL multivariate-analysis (HMA) with the set-based representation of vectors and matrices
with integer indices in the Jordan-normal-form (JNF) development.›
subsection ‹Bijections between index types of HMA and natural numbers›
text ‹At the core of HMA-connect, there has to be a translation between indices
of vectors and matrices, which are via index-types on the one hand, and natural
numbers on the other hand.
We some unspecified bijection in our application, and not the conversions
to-nat and from-nat in theory
Rank-Nullity-Theorem/Mod-Type, since our definitions
below do not enforce any further type constraints.›
theory Bij_Nat
imports
"HOL-Library.Cardinality"
"HOL-Library.Numeral_Type"
begin
lemma finite_set_to_list: "∃ xs :: 'a :: finite list. distinct xs ∧ set xs = Y"
proof -
have "finite Y" by simp
thus ?thesis
proof (induct Y rule: finite_induct)
case (insert y Y)
then obtain xs where xs: "distinct xs" "set xs = Y" by auto
show ?case
by (rule exI[of _ "y # xs"], insert xs insert(2), auto)
qed simp
qed
definition univ_list :: "'a :: finite list" where
"univ_list = (SOME xs. distinct xs ∧ set xs = UNIV)"
lemma univ_list: "distinct (univ_list :: 'a list)" "set univ_list = (UNIV :: 'a :: finite set)"
proof -
let ?xs = "univ_list :: 'a list"
have "distinct ?xs ∧ set ?xs = UNIV"
unfolding univ_list_def
by (rule someI_ex, rule finite_set_to_list)
thus "distinct ?xs" "set ?xs = UNIV" by auto
qed
definition to_nat :: "'a :: finite ⇒ nat" where
"to_nat a = (SOME i. univ_list ! i = a ∧ i < length (univ_list :: 'a list))"
definition from_nat :: "nat ⇒ 'a :: finite" where
"from_nat i = univ_list ! i"
lemma length_univ_list_card: "length (univ_list :: 'a :: finite list) = CARD('a)"
using distinct_card[of "univ_list :: 'a list", symmetric]
by (auto simp: univ_list)
lemma to_nat_ex: "∃! i. univ_list ! i = (a :: 'a :: finite) ∧ i < length (univ_list :: 'a list)"
proof -
let ?ul = "univ_list :: 'a list"
have a_in_set: "a ∈ set ?ul" unfolding univ_list by auto
from this [unfolded set_conv_nth]
obtain i where i1: "?ul ! i = a ∧ i < length ?ul" by auto
show ?thesis
proof (rule ex1I, rule i1)
fix j
assume "?ul ! j = a ∧ j < length ?ul"
moreover have "distinct ?ul" by (simp add: univ_list)
ultimately show "j = i" using i1 nth_eq_iff_index_eq by blast
qed
qed
lemma to_nat_less_card: "to_nat (a :: 'a :: finite) < CARD('a)"
proof -
let ?ul = "univ_list :: 'a list"
from to_nat_ex[of a] obtain i where
i1: "univ_list ! i = a ∧ i<length (univ_list::'a list)" by auto
show ?thesis unfolding to_nat_def
proof (rule someI2, rule i1)
fix x
assume x: "?ul ! x = a ∧ x < length ?ul"
thus "x < CARD ('a)" using x by (simp add: univ_list length_univ_list_card)
qed
qed
lemma to_nat_from_nat_id:
assumes i: "i < CARD('a :: finite)"
shows "to_nat (from_nat i :: 'a) = i"
unfolding to_nat_def from_nat_def
proof (rule some_equality, simp)
have l: "length (univ_list::'a list) = card (set (univ_list::'a list))"
by (rule distinct_card[symmetric], simp add: univ_list)
thus i2: "i < length (univ_list::'a list)"
using i unfolding univ_list by simp
fix n
assume n: "(univ_list::'a list) ! n = (univ_list::'a list) ! i ∧ n < length (univ_list::'a list)"
have d: "distinct (univ_list::'a list)" using univ_list by simp
show "n = i" using nth_eq_iff_index_eq[OF d _ i2] n by auto
qed
lemma from_nat_inj: assumes i: "i < CARD('a :: finite)"
and j: "j < CARD('a :: finite)"
and id: "(from_nat i :: 'a) = from_nat j"
shows "i = j"
proof -
from arg_cong[OF id, of to_nat]
show ?thesis using i j by (simp add: to_nat_from_nat_id)
qed
lemma from_nat_to_nat_id[simp]:
"(from_nat (to_nat a)) = (a::'a :: finite)"
proof -
have a_in_set: "a ∈ set (univ_list)" unfolding univ_list by auto
from this [unfolded set_conv_nth]
obtain i where i1: "univ_list ! i = a ∧ i<length (univ_list::'a list)" by auto
show ?thesis
unfolding to_nat_def from_nat_def
by (rule someI2, rule i1, simp)
qed
lemma to_nat_inj[simp]: assumes "to_nat a = to_nat b"
shows "a = b"
proof -
from to_nat_ex[of a] to_nat_ex[of b]
show "a = b" unfolding to_nat_def by (metis assms from_nat_to_nat_id)
qed
lemma range_to_nat: "range (to_nat :: 'a :: finite ⇒ nat) = {0 ..< CARD('a)}" (is "?l = ?r")
proof -
{
fix i
assume "i ∈ ?l"
hence "i ∈ ?r" using to_nat_less_card[where 'a = 'a] by auto
}
moreover
{
fix i
assume "i ∈ ?r"
hence "i < CARD('a)" by auto
from to_nat_from_nat_id[OF this]
have "i ∈ ?l" by (metis range_eqI)
}
ultimately show ?thesis by auto
qed
lemma inj_to_nat: "inj to_nat" by (simp add: inj_on_def)
lemma bij_to_nat: "bij_betw to_nat (UNIV :: 'a :: finite set) {0 ..< CARD('a)}"
unfolding bij_betw_def by (auto simp: range_to_nat inj_to_nat)
lemma numeral_nat: "(numeral m1 :: nat) * numeral n1 ≡ numeral (m1 * n1)"
"(numeral m1 :: nat) + numeral n1 ≡ numeral (m1 + n1)" by simp_all
lemmas card_num_simps =
card_num1 card_bit0 card_bit1
mult_num_simps
add_num_simps
eq_num_simps
mult_Suc_right mult_0_right One_nat_def add.right_neutral
numeral_nat Suc_numeral
end