Theory Perron_Frobenius.Bij_Nat

(*
  Authors: J. Divasón, R. Thiemann, A. Yamada
*)
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