Session Rank_Nullity_Theorem

Theory Dual_Order

(*  
    Title:      Dual_Order.thy
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
*)


section "Dual Order"

theory Dual_Order
  imports Main
begin

subsection‹Interpretation of dual wellorder based on wellorder›

lemma wf_wellorderI2:
  assumes wf: "wf {(x::'a::ord, y). y < x}"
  assumes lin: "class.linorder (λ(x::'a) y::'a. y  x) (λ(x::'a) y::'a. y < x)"
  shows "class.wellorder (λ(x::'a) y::'a. y  x) (λ(x::'a) y::'a. y < x)"
  using lin unfolding class.wellorder_def apply (rule conjI)
  apply (rule class.wellorder_axioms.intro) by (blast intro: wf_induct_rule [OF wf])


lemma (in preorder) tranclp_less': "(>)++ = (>)"
  by(auto simp add: fun_eq_iff intro: less_trans elim: tranclp.induct)

interpretation dual_wellorder: wellorder "(≥)::('a::{linorder, finite}=>'a=>bool)" "(>)" 
proof (rule wf_wellorderI2)
  show "wf {(x :: 'a, y). y < x}"
    by(auto simp add: trancl_def tranclp_less' intro!: finite_acyclic_wf acyclicI)
  show "class.linorder (λ(x::'a) y::'a. y  x) (λ(x::'a) y::'a. y < x)"
    unfolding class.linorder_def unfolding class.linorder_axioms_def unfolding class.order_def 
    unfolding class.preorder_def unfolding class.order_axioms_def by auto  
qed

subsection‹Properties of the Greatest operator›
  
lemma dual_wellorder_Least_eq_Greatest[simp]: "dual_wellorder.Least = Greatest" 
  by (auto simp add: Greatest_def dual_wellorder.Least_def)

lemmas GreatestI = dual_wellorder.LeastI[unfolded dual_wellorder_Least_eq_Greatest]
lemmas GreatestI2_ex = dual_wellorder.LeastI2_ex[unfolded dual_wellorder_Least_eq_Greatest]
lemmas GreatestI2_wellorder = dual_wellorder.LeastI2_wellorder[unfolded dual_wellorder_Least_eq_Greatest]
lemmas GreatestI_ex = dual_wellorder.LeastI_ex[unfolded dual_wellorder_Least_eq_Greatest]
lemmas not_greater_Greatest = dual_wellorder.not_less_Least[unfolded dual_wellorder_Least_eq_Greatest]
lemmas GreatestI2 = dual_wellorder.LeastI2[unfolded dual_wellorder_Least_eq_Greatest]
lemmas Greatest_ge = dual_wellorder.Least_le[unfolded dual_wellorder_Least_eq_Greatest]

end

Theory Mod_Type

(*
    Title:      Mod_Type.thy
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
*)

section‹Class for modular arithmetic›

theory Mod_Type
imports
  "HOL-Library.Numeral_Type"
  "HOL-Analysis.Cartesian_Euclidean_Space"
  Dual_Order
begin

subsection‹Definition and properties›

text‹Class for modular arithmetic. It is inspired by the locale mod\_type.›

class mod_type = times + wellorder + neg_numeral +
fixes Rep :: "'a => int"
  and Abs :: "int => 'a"
  assumes type: "type_definition Rep Abs {0..<int CARD ('a)}"
  and size1: "1 < int CARD ('a)"
  and zero_def: "0 = Abs 0"
  and one_def:  "1 = Abs 1"
  and add_def:  "x + y = Abs ((Rep x + Rep y) mod (int CARD ('a)))"
  and mult_def: "x * y = Abs ((Rep x * Rep y) mod (int CARD ('a)))"
  and diff_def: "x - y = Abs ((Rep x - Rep y) mod (int CARD ('a)))"
  and minus_def: "- x = Abs ((- Rep x) mod (int CARD ('a)))"
  and strict_mono_Rep: "strict_mono Rep"
begin

lemma size0: "0 < int CARD ('a)"
  using size1 by simp

lemmas definitions =
  zero_def one_def add_def mult_def minus_def diff_def

lemma Rep_less_n: "Rep x < int CARD ('a)"
  by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])

lemma Rep_le_n: "Rep x  int CARD ('a)"
  by (rule Rep_less_n [THEN order_less_imp_le])

lemma Rep_inject_sym: "x = y  Rep x = Rep y"
  by (rule type_definition.Rep_inject [OF type, symmetric])

lemma Rep_inverse: "Abs (Rep x) = x"
  by (rule type_definition.Rep_inverse [OF type])

lemma Abs_inverse: "m  {0..<int CARD ('a)}  Rep (Abs m) = m"
  by (rule type_definition.Abs_inverse [OF type])

lemma Rep_Abs_mod: "Rep (Abs (m mod int CARD ('a))) = m mod int CARD ('a)"
  by (simp add: Abs_inverse pos_mod_conj [OF size0])

lemma Rep_Abs_0: "Rep (Abs 0) = 0"
  apply (rule Abs_inverse [of 0])
  using size0 by simp

lemma Rep_0: "Rep 0 = 0"
  by (simp add: zero_def Rep_Abs_0)

lemma Rep_Abs_1: "Rep (Abs 1) = 1"
  by (simp add: Abs_inverse size1)

lemma Rep_1: "Rep 1 = 1"
  by (simp add: one_def Rep_Abs_1)

lemma Rep_mod: "Rep x mod int CARD ('a) = Rep x"
  apply (rule_tac x=x in type_definition.Abs_cases [OF type])
  apply (simp add: type_definition.Abs_inverse [OF type])
done

lemmas Rep_simps =
  Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1

subsection‹Conversion between a modular class and the subset of natural numbers associated.›
text‹Definitions to make transformations among elements of a modular class and naturals›
definition to_nat :: "'a => nat"
  where "to_nat = nat  Rep"

definition Abs' :: "int => 'a"
  where "Abs' x = Abs(x mod int CARD ('a))"

definition from_nat :: "nat  'a"
  where "from_nat = (Abs'  int)"

lemma bij_Rep: "bij_betw (Rep) (UNIV::'a set) {0..<int CARD('a)}"
proof (unfold bij_betw_def, rule conjI)
  show "inj Rep" by (metis strict_mono_imp_inj_on strict_mono_Rep)
  show "range Rep = {0..<int CARD('a)}" using Typedef.type_definition.Rep_range[OF type] .
qed

lemma mono_Rep: "mono Rep" by (metis strict_mono_Rep strict_mono_mono)

lemma Rep_ge_0: "0  Rep x" using bij_Rep unfolding bij_betw_def by auto

lemma bij_Abs: "bij_betw (Abs) {0..<int CARD('a)} (UNIV::'a set)"
proof (unfold bij_betw_def, rule conjI)
  show "inj_on Abs {0..<int CARD('a)}" by (metis inj_on_inverseI type type_definition.Abs_inverse)
  show "Abs ` {0..<int CARD('a)} = (UNIV::'a set)" by (metis type type_definition.univ)
qed

corollary bij_Abs': "bij_betw (Abs') {0..<int CARD('a)} (UNIV::'a set)"
proof (unfold bij_betw_def, rule conjI)
  show "inj_on Abs' {0..<int CARD('a)}"
    unfolding inj_on_def Abs'_def
    by (auto, metis Rep_Abs_mod mod_pos_pos_trivial)
  show "Abs' ` {0..<int CARD('a)} = (UNIV::'a set)"
  proof (unfold image_def Abs'_def, auto)
    fix x show "xa{0..<int CARD('a)}. x = Abs xa"
      by (rule bexI[of _ "Rep x"], auto simp add: Rep_less_n[of x] Rep_ge_0[of x], metis Rep_inverse)
  qed
qed

lemma bij_from_nat: "bij_betw (from_nat) {0..<CARD('a)} (UNIV::'a set)"
proof (unfold bij_betw_def, rule conjI)
  have set_eq: "{0::int..<int CARD('a)} = int` {0..<CARD('a)}" apply (auto)
  proof -
    fix x::int  assume x1: "(0::int)  x" and x2: "x < int CARD('a)" show "x  int ` {0::nat..<CARD('a)}"
    proof (unfold image_def, auto, rule bexI[of _ "nat x"])
      show " x = int (nat x)" using x1 by auto
      show "nat x  {0::nat..<CARD('a)}" using x1 x2 by auto
    qed
  qed
  show "inj_on (from_nat::nat'a) {0::nat..<CARD('a)}"
  proof (unfold from_nat_def , rule comp_inj_on)
    show "inj_on int {0::nat..<CARD('a)}" by (metis inj_of_nat subset_inj_on top_greatest)
    show "inj_on (Abs'::int=>'a) (int ` {0::nat..<CARD('a)})"
      using bij_Abs unfolding bij_betw_def set_eq
      by (metis (hide_lams, no_types) Abs'_def Abs_inverse Rep_inverse Rep_mod inj_on_def set_eq)
  qed
  show "(from_nat::nat=>'a)` {0::nat..<CARD('a)} = UNIV"
    unfolding from_nat_def using bij_Abs'
    unfolding bij_betw_def set_eq o_def by blast
qed

lemma to_nat_is_inv: "the_inv_into {0..<CARD('a)} (from_nat::nat=>'a) = (to_nat::'a=>nat)"
proof (unfold the_inv_into_def fun_eq_iff from_nat_def to_nat_def o_def, clarify)
  fix x::"'a" show "(THE y::nat. y  {0::nat..<CARD('a)}  Abs' (int y) = x) = nat (Rep x)"
  proof (rule the_equality, auto)
    show " Abs' (Rep x) = x" by (metis Abs'_def Rep_inverse Rep_mod)
    show "nat (Rep x) < CARD('a)" by (metis (full_types) Rep_less_n nat_int size0 zless_nat_conj)
    assume x:  "¬ (0::int)  Rep x" show "(0::nat) < CARD('a)" and "Abs' (0::int) = x"
      using Rep_ge_0 x by auto
  next
    fix y::nat assume y: "y < CARD('a)"
    have "(Rep(Abs'(int y)::'a)) = (Rep((Abs(int y mod int CARD('a)))::'a))" unfolding Abs'_def ..
    also have "... =  (Rep (Abs (int y)::'a))" using zmod_int[of y "CARD('a)"]
      using y mod_less by auto
    also have "... =  (int y)" proof (rule Abs_inverse) show "int y  {0::int..<int CARD('a)}"
      using y by auto qed
    finally show "y = nat (Rep (Abs' (int y)::'a))" by (metis nat_int)
  qed
qed

lemma bij_to_nat: "bij_betw (to_nat) (UNIV::'a set) {0..<CARD('a)}"
  using bij_betw_the_inv_into[OF bij_from_nat] unfolding to_nat_is_inv .

lemma finite_mod_type: "finite (UNIV::'a set)"
  using finite_imageD[of "to_nat" "UNIV::'a set"] using bij_to_nat unfolding bij_betw_def by auto

subclass (in mod_type) finite by (intro_classes, rule finite_mod_type)

lemma least_0: "(LEAST n. n  (UNIV::'a set)) = 0"
proof (rule Least_equality, auto)
  fix y::"'a"
  have "(0::'a)  Abs (Rep y mod int CARD('a))" using strict_mono_Rep unfolding strict_mono_def
  by (metis (hide_lams, mono_tags) Rep_0 Rep_ge_0 strict_mono_Rep strict_mono_less_eq)
  also have "... = y" by (metis Rep_inverse Rep_mod)
  finally show "(0::'a)  y" .
qed

lemma add_to_nat_def: "x + y = from_nat (to_nat x + to_nat y)"
  unfolding from_nat_def to_nat_def o_def using Rep_ge_0[of x] using Rep_ge_0[of y]
  using Rep_less_n[of x] Rep_less_n[of y]
  unfolding Abs'_def unfolding add_def[of x y] by auto

lemma to_nat_1: "to_nat 1 = 1"
  by (simp add: to_nat_def Rep_1)

lemma add_def':
  shows "x + y = Abs' (Rep x + Rep y)" unfolding Abs'_def using add_def by simp

lemma Abs'_0:
  shows "Abs' (CARD('a))=(0::'a)" by (metis (hide_lams, mono_tags) Abs'_def mod_self zero_def)

lemma Rep_plus_one_le_card:
  assumes a: "a + 1  0"
  shows "(Rep a) + 1 < CARD ('a)"
proof (rule ccontr)
  assume "¬ Rep a + 1 < CARD('a)" hence to_nat_eq_card: "Rep a + 1 = CARD('a)"
    using Rep_less_n
    by (simp add: add1_zle_eq order_class.less_le)
  have "a+1 = Abs' (Rep a + Rep (1::'a))" using add_def' by auto
  also have "... = Abs' ((Rep a) + 1)" using Rep_1 by simp
  also have "... = Abs' (CARD('a))" unfolding to_nat_eq_card ..
  also have "... = 0" using Abs'_0 by auto
  finally show False using a by contradiction
qed

lemma to_nat_plus_one_less_card: "a. a+1  0 --> to_nat a + 1 < CARD('a)"
proof (clarify)
fix a
assume a: "a + 1  0"
have "Rep a + 1 < int CARD('a)" using Rep_plus_one_le_card[OF a] by auto
hence "nat (Rep a + 1) < nat (int CARD('a))" unfolding zless_nat_conj using size0 by fast
thus "to_nat a + 1 < CARD('a)" unfolding to_nat_def o_def using nat_add_distrib[OF Rep_ge_0] by simp
qed

corollary to_nat_plus_one_less_card':
assumes "a+1  0"
shows "to_nat a + 1 < CARD('a)" using to_nat_plus_one_less_card assms by simp

lemma strict_mono_to_nat: "strict_mono to_nat"
  using strict_mono_Rep
  unfolding strict_mono_def to_nat_def using Rep_ge_0 by (metis comp_apply nat_less_eq_zless)

lemma to_nat_eq [simp]: "to_nat x = to_nat y  x = y"
  using injD [OF bij_betw_imp_inj_on[OF bij_to_nat]] by blast

lemma mod_type_forall_eq [simp]: "(j::'a. (to_nat j)<CARD('a)  P j) = (a. P a)"
proof (auto)
  fix a assume a: "j. (to_nat::'a=>nat) j < CARD('a)  P j"
  have "(to_nat::'a=>nat) a < CARD('a)" using bij_to_nat unfolding bij_betw_def by auto
  thus "P a" using a by auto
qed

lemma to_nat_from_nat:
  assumes t:"to_nat j = k"
  shows "from_nat k = j"
proof -
  have "from_nat k = from_nat (to_nat j)"  unfolding t ..
  also have "... = from_nat (the_inv_into {0..<CARD('a)} (from_nat) j)" unfolding to_nat_is_inv ..
  also have "... = j"
  proof (rule f_the_inv_into_f)
    show "inj_on from_nat {0..<CARD('a)}" by (metis bij_betw_imp_inj_on bij_from_nat)
    show "j  from_nat ` {0..<CARD('a)}" by (metis UNIV_I bij_betw_def bij_from_nat)
  qed
  finally show "from_nat k = j" .
qed

lemma to_nat_mono:
  assumes ab: "a < b"
  shows "to_nat a < to_nat b"
  using strict_mono_to_nat unfolding strict_mono_def using assms by fast

lemma to_nat_mono':
  assumes ab: "a  b"
  shows "to_nat a  to_nat b"
proof (cases "a=b")
  case True thus ?thesis by auto
next
  case False
  hence "a<b" using ab by simp
  thus ?thesis using to_nat_mono by fastforce
qed

lemma least_mod_type:
  shows "0  (n::'a)"
  using least_0 by (metis (full_types) Least_le UNIV_I)

lemma to_nat_from_nat_id:
  assumes x: "x<CARD('a)"
  shows "to_nat ((from_nat x)::'a) = x"
  unfolding to_nat_is_inv[symmetric] proof (rule the_inv_into_f_f)
  show "inj_on (from_nat::nat=>'a) {0..<CARD('a)}" using bij_from_nat unfolding bij_betw_def by auto
  show "x  {0..<CARD('a)}" using x by simp
qed

lemma from_nat_to_nat_id[simp]:
  shows "from_nat (to_nat x) = x" by (metis to_nat_from_nat)

lemma from_nat_to_nat:
  assumes t:"from_nat j = k" and j: "j<CARD('a)"
  shows "to_nat k = j" by (metis j t to_nat_from_nat_id)

lemma from_nat_mono:
  assumes i_le_j: "i<j" and j: "j<CARD('a)"
  shows "(from_nat i::'a) < from_nat j"
proof -
have i: "i<CARD('a)" using i_le_j j by simp
obtain a where a: "i=to_nat a"
  using bij_to_nat unfolding bij_betw_def using i to_nat_from_nat_id by metis
obtain b where b: "j=to_nat b"
  using bij_to_nat unfolding bij_betw_def using j to_nat_from_nat_id by metis
show ?thesis by (metis a b from_nat_to_nat_id i_le_j strict_mono_less strict_mono_to_nat)
qed

lemma from_nat_mono':
  assumes i_le_j: "i  j" and "j<CARD ('a)"
  shows "(from_nat i::'a)  from_nat j"
proof (cases "i=j")
  case True
  have "(from_nat i::'a) = from_nat j" using True by simp
  thus ?thesis by simp
next
  case False
  hence "i<j" using i_le_j by simp
  thus ?thesis by (metis assms(2) from_nat_mono less_imp_le)
qed

lemma to_nat_suc:
  assumes "to_nat (x)+1 < CARD ('a)"
  shows "to_nat (x + 1::'a) = (to_nat x) + 1"
proof -
  have "(x::'a) + 1 = from_nat (to_nat x + to_nat (1::'a))" unfolding add_to_nat_def ..
  hence "to_nat ((x::'a) + 1) = to_nat (from_nat (to_nat x + to_nat (1::'a))::'a)" by presburger
  also have "... = to_nat (from_nat (to_nat x + 1)::'a)" unfolding to_nat_1 ..
  also have "... = (to_nat x + 1)" by (metis assms to_nat_from_nat_id)
  finally show ?thesis .
qed

lemma to_nat_le:
  assumes "y < from_nat k"
  shows  "to_nat y < k"
proof (cases "k<CARD('a)")
  case True show ?thesis by (metis (full_types) True assms to_nat_from_nat_id to_nat_mono)
next
  case False have "to_nat y < CARD ('a)" using bij_to_nat unfolding bij_betw_def by auto
  thus ?thesis using False by auto
qed

lemma le_Suc:
  assumes ab: "a < (b::'a)"
  shows "a + 1  b"
proof -
  have "a + 1 = (from_nat (to_nat (a + 1))::'a)" using from_nat_to_nat_id [of "a+1",symmetric] .
  also have "...  (from_nat (to_nat (b::'a))::'a)"
  proof (rule from_nat_mono')
    have "to_nat a < to_nat b" using ab by (metis to_nat_mono)
    hence "to_nat a + 1  to_nat b" by simp
    thus "to_nat b < CARD ('a)" using bij_to_nat unfolding  bij_betw_def by auto
    hence "to_nat a + 1 < CARD ('a)" by (metis ‹to_nat a + 1  to_nat b preorder_class.le_less_trans)
    thus "to_nat (a + 1)  to_nat b" by (metis ‹to_nat a + 1  to_nat b to_nat_suc)
  qed
  also have "... = b" by (metis from_nat_to_nat_id)
  finally show "a + (1::'a)  b" .
qed

lemma le_Suc':
assumes ab: "a + 1  b"
  and less_card: "(to_nat a) + 1 < CARD ('a)"
  shows "a < b"
proof -
  have "a = (from_nat (to_nat a)::'a)" using from_nat_to_nat_id [of "a",symmetric] .
  also have "... < (from_nat (to_nat b)::'a)"
  proof (rule from_nat_mono)
    show "to_nat b < CARD('a)" using bij_to_nat unfolding  bij_betw_def by auto
    have "to_nat (a + 1)   to_nat b" using ab by (metis to_nat_mono')
    hence "to_nat (a) + 1   to_nat b"  using to_nat_suc[OF less_card] by auto
    thus "to_nat a < to_nat b" by simp
  qed
  finally show "a < b" by (metis to_nat_from_nat)
qed

lemma Suc_le:
  assumes less_card: "(to_nat a) + 1 < CARD ('a)"
  shows "a < a + 1"
proof -
  have "(to_nat a) < (to_nat a) + 1" by simp
  hence "(to_nat a) < to_nat (a + 1)" by (metis less_card to_nat_suc)
  hence "(from_nat (to_nat a)::'a) < from_nat (to_nat (a + 1))"
    by (rule from_nat_mono, metis less_card to_nat_suc)
  thus "a < a + 1" by (metis to_nat_from_nat)
qed

lemma Suc_le':
  fixes a::'a
  assumes "a + 1  0"
  shows "a < a + 1" using Suc_le to_nat_plus_one_less_card assms by blast

lemma from_nat_not_eq:
  assumes a_eq_to_nat: "a  to_nat b"
  and a_less_card: "a<CARD('a)"
  shows "from_nat a  b"
proof (rule ccontr)
  assume "¬ from_nat a  b" hence "from_nat a = b" by simp
  hence "to_nat ((from_nat a)::'a) = to_nat b" by auto
  thus False by (metis a_eq_to_nat a_less_card to_nat_from_nat_id)
qed

lemma Suc_less:
  fixes i::'a
  assumes "i<j"
  and "i+1  j"
  shows "i+1<j" by (metis assms le_Suc le_neq_trans)


lemma Greatest_is_minus_1: "a::'a. a  -1"
proof (clarify)
  fix a::'a
  have zero_ge_card_1: "0  int CARD('a) - 1" using size1 by auto
  have card_less: "int CARD('a) - 1 < int CARD('a)" by auto
  have not_zero: "1 mod int CARD('a)  0"
    by (metis (hide_lams, mono_tags) Rep_Abs_1 Rep_mod zero_neq_one)
  have int_card: "int (CARD('a) - 1) = int CARD('a) - 1" using of_nat_diff[of 1 "CARD ('a)"]
    using size1 by simp
  have "a = Abs' (Rep a)" by (metis (hide_lams, mono_tags) Rep_0 add_0_right add_def'
      monoid_add_class.add.right_neutral)
  also have "... = Abs' (int (nat (Rep a)))" by (metis Rep_ge_0 int_nat_eq)
  also have "...   Abs' (int (CARD('a) - 1))"
  proof (rule from_nat_mono'[unfolded from_nat_def o_def, of "nat (Rep a)" "CARD('a) - 1"])
    show "nat (Rep a)  CARD('a) - 1" using Rep_less_n
      using int_card nat_le_iff by auto
    show "CARD('a) - 1 < CARD('a)" using finite_UNIV_card_ge_0 finite_mod_type by fastforce
  qed
  also have "... = - 1"
  unfolding Abs'_def unfolding minus_def zmod_zminus1_eq_if unfolding Rep_1
  apply (rule cong [of Abs], rule refl)
  unfolding if_not_P [OF not_zero]
  unfolding int_card
  unfolding mod_pos_pos_trivial[OF zero_ge_card_1 card_less]
  using mod_pos_pos_trivial[OF _ size1] by presburger
  finally show "a  -1" by fastforce
qed

lemma a_eq_minus_1: "a::'a. a+1 = 0  a = -1"
  by (metis eq_neg_iff_add_eq_0)


lemma forall_from_nat_rw:
  shows "(x{0..<CARD('a)}. P (from_nat x::'a)) = (x. P (from_nat x))"
proof (auto)
  fix y assume *: "x{0..<CARD('a)}. P (from_nat x)"
  have "from_nat y  (UNIV::'a set)" by auto
  from this obtain x where x1: "from_nat y = (from_nat x::'a)" and x2: "x{0..<CARD('a)}"
    using bij_from_nat unfolding bij_betw_def
    by (metis from_nat_to_nat_id rangeI the_inv_into_onto to_nat_is_inv)
  show "P (from_nat y::'a)" unfolding x1 using * x2 by simp
qed

lemma from_nat_eq_imp_eq:
  assumes f_eq: "from_nat x = (from_nat xa::'a)"
and x: "x<CARD('a)" and xa: "xa<CARD('a)"
  shows "x=xa" using assms from_nat_not_eq by metis

lemma to_nat_less_card:
  fixes j::"'a"
  shows "to_nat j < CARD ('a)"
  using bij_to_nat unfolding bij_betw_def by auto

lemma from_nat_0: "from_nat 0 = 0"
  unfolding from_nat_def o_def of_nat_0 Abs'_def mod_0 zero_def ..
lemma to_nat_0: "to_nat 0 = 0" unfolding to_nat_def o_def Rep_0 nat_0 ..
lemma to_nat_eq_0: "(to_nat x = 0) = (x = 0)"
  by (auto simp add: to_nat_0 from_nat_0 dest: to_nat_from_nat)

lemma suc_not_zero:
  assumes "to_nat a + 1  CARD('a)"
  shows "a+1  0"
proof (rule ccontr, simp)
  assume a_plus_one_zero: "a + 1 = 0"
  hence rep_eq_card: "Rep a + 1 = CARD('a)"
    using assms to_nat_0 Suc_eq_plus1 Suc_lessI Zero_not_Suc to_nat_less_card to_nat_suc
    by (metis (hide_lams, mono_tags))
  moreover have "Rep a + 1 < CARD('a)"
    using Abs'_0 Rep_1 Suc_eq_plus1 Suc_lessI Suc_neq_Zero add_def' assms
    rep_eq_card to_nat_0 to_nat_less_card to_nat_suc by (metis (hide_lams, mono_tags))
  ultimately show False by fastforce
qed


lemma from_nat_suc:
shows "from_nat (j + 1) = from_nat j + 1"
unfolding from_nat_def o_def Abs'_def add_def' Rep_1 Rep_Abs_mod
unfolding of_nat_add apply (subst mod_add_left_eq) unfolding of_nat_1 ..

lemma to_nat_plus_1_set:
shows "to_nat a + 1  {1..<CARD('a)+1}"
using to_nat_less_card by simp

end

lemma from_nat_CARD:
  shows "from_nat (CARD('a)) = (0::'a::{mod_type})"
  unfolding from_nat_def o_def Abs'_def by (simp add: zero_def)


subsection‹Instantiations›

instantiation bit0 and bit1:: (finite) mod_type
begin

definition "(Rep::'a bit0 => int)  x = Rep_bit0 x"
definition "(Abs::int => 'a bit0) x = Abs_bit0' x"

definition "(Rep::'a bit1 => int)  x = Rep_bit1 x"
definition "(Abs::int => 'a bit1) x = Abs_bit1' x"

instance
proof
  show "(0::'a bit0) = Abs (0::int)" unfolding Abs_bit0_def Abs_bit0'_def zero_bit0_def by auto
  show "(1::int) < int CARD('a bit0)" by (metis bit0.size1)
  show "type_definition (Rep::'a bit0 => int) (Abs:: int => 'a bit0) {0::int..<int CARD('a bit0)}"
  proof (unfold type_definition_def Rep_bit0_def [abs_def]
      Abs_bit0_def [abs_def] Abs_bit0'_def, intro conjI)
    show "x::'a bit0. Rep_bit0 x  {0::int..<int CARD('a bit0)}"
      unfolding card_bit0 unfolding of_nat_mult
      using Rep_bit0 [where ?'a = "'a"] by simp
    show "x::'a bit0. Abs_bit0 (Rep_bit0 x mod int CARD('a bit0)) = x"
      by (metis Rep_bit0_inverse bit0.Rep_mod)
    show "y::int. y  {0::int..<int CARD('a bit0)}
       Rep_bit0 ((Abs_bit0::int => 'a bit0) (y mod int CARD('a bit0))) = y"
      by (metis bit0.Abs_inverse bit0.Rep_mod)
  qed
  show "(1::'a bit0) = Abs (1::int)" unfolding Abs_bit0_def Abs_bit0'_def one_bit0_def
    by (metis bit0.of_nat_eq of_nat_1 one_bit0_def)
  fix x y :: "'a bit0"
  show "x + y = Abs ((Rep x + Rep y) mod int CARD('a bit0))"
    unfolding Abs_bit0_def Rep_bit0_def plus_bit0_def Abs_bit0'_def by fastforce
  show "x * y = Abs (Rep x * Rep y mod int CARD('a bit0))"
    unfolding Abs_bit0_def Rep_bit0_def times_bit0_def Abs_bit0'_def by fastforce
  show "x - y = Abs ((Rep x - Rep y) mod int CARD('a bit0))"
    unfolding Abs_bit0_def Rep_bit0_def minus_bit0_def Abs_bit0'_def by fastforce
  show "- x = Abs (- Rep x mod int CARD('a bit0))"
    unfolding Abs_bit0_def Rep_bit0_def uminus_bit0_def Abs_bit0'_def by fastforce
  show "(0::'a bit1) = Abs (0::int)" unfolding Abs_bit1_def Abs_bit1'_def zero_bit1_def by auto
  show "(1::int) < int CARD('a bit1)" by (metis bit1.size1)
  show "(1::'a bit1) = Abs (1::int)" unfolding Abs_bit1_def Abs_bit1'_def one_bit1_def
    by (metis bit1.of_nat_eq of_nat_1 one_bit1_def)
  fix x y :: "'a bit1"
  show "x + y = Abs ((Rep x + Rep y) mod int CARD('a bit1))"
    unfolding Abs_bit1_def Abs_bit1'_def Rep_bit1_def plus_bit1_def by fastforce
  show "x * y = Abs (Rep x * Rep y mod int CARD('a bit1))"
    unfolding Abs_bit1_def Rep_bit1_def times_bit1_def Abs_bit1'_def by fastforce
  show "x - y = Abs ((Rep x - Rep y) mod int CARD('a bit1))"
    unfolding Abs_bit1_def Rep_bit1_def minus_bit1_def Abs_bit1'_def by fastforce
  show "- x = Abs (- Rep x mod int CARD('a bit1))"
    unfolding Abs_bit1_def Rep_bit1_def uminus_bit1_def Abs_bit1'_def by fastforce
  show "type_definition (Rep::'a bit1 => int) (Abs:: int => 'a bit1) {0::int..<int CARD('a bit1)}"
  proof (unfold type_definition_def Rep_bit1_def [abs_def]
      Abs_bit1_def [abs_def] Abs_bit1'_def, intro conjI)
    have int_2: "int 2 = 2" by auto
   show "x::'a bit1. Rep_bit1 x  {0::int..<int CARD('a bit1)}"
      unfolding card_bit1
      unfolding of_nat_Suc of_nat_mult
      using Rep_bit1 [where ?'a = "'a"]
      unfolding int_2 ..
   show "x::'a bit1. Abs_bit1 (Rep_bit1 x mod int CARD('a bit1)) = x"
      by (metis Rep_bit1_inverse bit1.Rep_mod)
   show "y::int. y  {0::int..<int CARD('a bit1)}
     Rep_bit1 ((Abs_bit1::int => 'a bit1) (y mod int CARD('a bit1))) = y"
   by (metis bit1.Abs_inverse bit1.Rep_mod)
  qed
  show "strict_mono (Rep::'a bit0 => int)" unfolding strict_mono_def
    by (metis Rep_bit0_def less_bit0_def)
  show "strict_mono (Rep::'a bit1 => int)" unfolding strict_mono_def
    by (metis Rep_bit1_def less_bit1_def)
qed
end

end


Theory Miscellaneous

(* 
    Title:      Miscellaneous.thy
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
*)

section‹Miscellaneous›

theory Miscellaneous
  imports
  "HOL-Analysis.Determinants"
  Mod_Type
  "HOL-Library.Function_Algebras"
begin

context Vector_Spaces.linear begin
sublocale vector_space_pair by unfold_locales―‹TODO: (re)move?›
end

hide_const (open) Real_Vector_Spaces.linear
abbreviation "linear  Vector_Spaces.linear"

text‹In this file, we present some basic definitions and lemmas about linear algebra and matrices.›

subsection‹Definitions of number of rows and columns of a matrix›

definition nrows :: "'a^'columns^'rows => nat"
  where "nrows A = CARD('rows)"

definition ncols :: "'a^'columns^'rows => nat"
  where "ncols A = CARD('columns)"
  
definition matrix_scalar_mult :: "'a::ab_semigroup_mult => 'a ^'n^'m => 'a ^'n^'m"
    (infixl "*k" 70)
  where "k *k A  (χ i j. k * A $ i $ j)"

subsection‹Basic properties about matrices›

lemma nrows_not_0[simp]:
  shows "0  nrows A" unfolding nrows_def by simp

lemma ncols_not_0[simp]:
  shows "0  ncols A" unfolding ncols_def by simp

lemma nrows_transpose: "nrows (transpose A) = ncols A"
  unfolding nrows_def ncols_def ..

lemma ncols_transpose: "ncols (transpose A) = nrows A"
  unfolding nrows_def ncols_def ..

lemma finite_rows: "finite (rows A)"
  using finite_Atleast_Atmost_nat[of "λi. row i A"] unfolding rows_def .

lemma finite_columns: "finite (columns A)"
  using finite_Atleast_Atmost_nat[of "λi. column i A"] unfolding columns_def .

lemma transpose_vector: "x v* A = transpose A *v x"
  by simp

lemma transpose_zero[simp]: "(transpose A = 0) = (A = 0)"
  unfolding transpose_def zero_vec_def vec_eq_iff by auto


subsection‹Theorems obtained from the AFP›

text‹The following theorems and definitions have been obtained from the AFP 
@{url "http://isa-afp.org/browser_info/current/HOL/Tarskis_Geometry/Linear_Algebra2.html"}.
I have removed some restrictions over the type classes.›


lemma vector_scalar_matrix_ac:
  fixes k :: "'a::{field}" and x :: "'a::{field}^'n" and A :: "'a^'m^'n"
  shows "x v* (k *k A) = k *s (x v* A)"
  using scalar_vector_matrix_assoc 
  unfolding vector_matrix_mult_def matrix_scalar_mult_def vec_eq_iff
  by (auto simp add: sum_distrib_left vector_space_over_itself.scale_scale)

lemma transpose_scalar: "transpose (k *k A) = k *k transpose A"
  unfolding transpose_def 
  by (vector, simp add: matrix_scalar_mult_def)

lemma scalar_matrix_vector_assoc:
  fixes A :: "'a::{field}^'m^'n"
  shows "k *s (A *v v) = k *k A *v v"
  by (metis transpose_scalar vector_scalar_matrix_ac vector_transpose_matrix)

lemma matrix_scalar_vector_ac:
  fixes A :: "'a::{field}^'m^'n"
  shows "A *v (k *s v) = k *k A *v v"
  by (simp add: Miscellaneous.scalar_matrix_vector_assoc vec.scale)


definition
  is_basis :: "('a::{field}^'n) set => bool" where
  "is_basis S  vec.independent S  vec.span S = UNIV"

lemma card_finite:
  assumes "card S = CARD('n::finite)"
  shows "finite S"
proof -
  from ‹card S = CARD('n) have "card S  0" by simp
  with card_eq_0_iff [of S] show "finite S" by simp
qed

lemma independent_is_basis:
  fixes B :: "('a::{field}^'n) set"
  shows "vec.independent B  card B = CARD('n)  is_basis B"
proof
  assume "vec.independent B  card B = CARD('n)"
  hence "vec.independent B" and "card B = CARD('n)" by simp+
  from card_finite [of B, where 'n = 'n] and ‹card B = CARD('n)
  have "finite B" by simp
  from ‹card B = CARD('n)
  have "card B = vec.dim (UNIV :: (('a^'n) set))" unfolding vec_dim_card .
  with vec.card_eq_dim [of B UNIV] and ‹finite B and ‹vec.independent B
  have "vec.span B = UNIV" by auto
  with ‹vec.independent B show "is_basis B" unfolding is_basis_def ..
next
  assume "is_basis B"
  hence "vec.independent B" unfolding is_basis_def ..
  moreover have "card B = CARD('n)"
  proof -
    have "B  UNIV" by simp
    moreover
    { from ‹is_basis B have "UNIV  vec.span B" and "vec.independent B"
        unfolding is_basis_def
        by simp+ }
    ultimately have "card B = vec.dim (UNIV::((real^'n) set))"
      using vec.basis_card_eq_dim [of B UNIV]
      unfolding vec_dim_card
      by simp
    then show "card B = CARD('n)"
      by (metis vec_dim_card)
  qed
  ultimately show "vec.independent B  card B = CARD('n)" ..
qed

lemma basis_finite:
  fixes B :: "('a::{field}^'n) set"
  assumes "is_basis B"
  shows "finite B"
proof -
  from independent_is_basis [of B] and ‹is_basis B have "card B = CARD('n)"
    by simp
  with card_finite [of B, where 'n = 'n] show "finite B" by simp
qed

text‹Here ends the statements obtained from AFP: 
  @{url "http://isa-afp.org/browser_info/current/HOL/Tarskis_Geometry/Linear_Algebra2.html"}
  which have been generalized.›

subsection‹Basic properties involving span, linearity and dimensions›

context finite_dimensional_vector_space
begin

text‹This theorem is the reciprocal theorem of @{thm "indep_card_eq_dim_span"}

lemma card_eq_dim_span_indep:
  assumes "dim (span A) = card A" and "finite A"
  shows "independent A" 
  by (metis assms card_le_dim_spanning dim_subset equalityE span_superset)

lemma dim_zero_eq:
  assumes dim_A: "dim A = 0"
  shows "A = {}  A = {0}"
  using dim_A local.card_ge_dim_independent local.independent_empty by force

lemma dim_zero_eq': 
  assumes A: "A = {}  A = {0}"
  shows "dim A = 0"
using assms local.dim_span local.indep_card_eq_dim_span local.independent_empty by fastforce

lemma dim_zero_subspace_eq:
  assumes subs_A: "subspace A"
  shows "(dim A = 0) = (A = {0})" 
  by (metis dim_zero_eq dim_zero_eq' subspace_0[OF subs_A] empty_iff)

lemma span_0_imp_set_empty_or_0:
  assumes "span A = {0}"
  shows "A = {}  A = {0}" by (metis assms span_superset subset_singletonD)

end

context Vector_Spaces.linear
begin

lemma linear_injective_ker_0:
  shows "inj f = ({x. f x = 0} = {0})"
  using inj_iff_eq_0 by auto

end

lemma snd_if_conv:
  shows "snd (if P then (A,B) else (C,D))=(if P then B else D)" by simp

subsection‹Basic properties about matrix multiplication›

lemma row_matrix_matrix_mult:
  fixes A::"'a::{comm_ring_1}^'n^'m"
  shows "(P $ i) v* A = (P ** A) $ i"
  unfolding vec_eq_iff
  unfolding vector_matrix_mult_def unfolding matrix_matrix_mult_def
  by (auto intro!: sum.cong)

corollary row_matrix_matrix_mult':
  fixes A::"'a::{comm_ring_1}^'n^'m"
  shows "(row i P) v* A = row i (P ** A)"
  using row_matrix_matrix_mult unfolding row_def vec_nth_inverse .

lemma column_matrix_matrix_mult:
  shows "column i (P**A) = P *v (column i A)"
  unfolding column_def matrix_vector_mult_def matrix_matrix_mult_def by fastforce

lemma matrix_matrix_mult_inner_mult:
  shows "(A ** B) $ i $ j = row i A  column j B"
  unfolding inner_vec_def matrix_matrix_mult_def row_def column_def by auto


lemma matrix_vmult_column_sum:
  fixes A::"'a::{field}^'n^'m"
  shows "f. A *v x = sum (λy. f y *s y) (columns A)"
proof (rule exI[of _ "λy. sum (λi. x $ i) {i. y = column i A}"])
  let ?f="λy. sum (λi. x $ i) {i. y = column i A}"  
  let ?g="(λy. {i. y=column i (A)})"
  have inj: "inj_on ?g (columns (A))" unfolding inj_on_def unfolding columns_def by auto
  have union_univ: " (?g`(columns (A))) = UNIV" unfolding columns_def by auto
  have "A *v x = (iUNIV. x $ i *s column i A)" unfolding matrix_mult_sum ..
  also have "... = sum (λi.  x $ i *s column i A) ((?g`(columns A)))" unfolding union_univ ..
  also have "... = sum (sum ((λi.  x $ i *s column i A)))  (?g`(columns A))"
    by (rule sum.Union_disjoint[unfolded o_def], auto) 
  also have "... = sum ((sum ((λi.  x $ i *s column i A)))  ?g)  (columns A)" 
    by (rule sum.reindex, simp add: inj)
  also have "... =  sum (λy. ?f y *s y) (columns A)"
  proof (rule sum.cong, unfold o_def)
    fix xa
    have "sum (λi. x $ i *s column i A) {i. xa = column i A} 
      = sum (λi. x $ i *s xa) {i. xa = column i A}" by simp
    also have "... = sum (λi. x $ i) {i. xa = column i A} *s xa" 
      using vec.scale_sum_left[of "(λi. x $ i)" "{i. xa = column i A}" xa] ..
    finally show "(i | xa = column i A. x $ i *s column i A) = (i | xa = column i A. x $ i) *s xa" . 
  qed rule
  finally show "A *v x = (ycolumns A. (i | y = column i A. x $ i) *s y)" .
qed


subsection‹Properties about invertibility›

lemma matrix_inv:
  assumes "invertible M"
  shows matrix_inv_left: "matrix_inv M ** M = mat 1"
    and matrix_inv_right: "M ** matrix_inv M = mat 1"
  using ‹invertible M and someI_ex [of "λ N. M ** N = mat 1  N ** M = mat 1"]
  unfolding invertible_def and matrix_inv_def
  by simp_all


text‹In the library, @{thm "matrix_inv_def"} allows the use of non squary matrices.
  The following lemma can be also proved fixing @{term "A::'a::{semiring_1}^'n^'m"}

lemma matrix_inv_unique:
  fixes A::"'a::{semiring_1}^'n^'n"
  assumes AB: "A ** B = mat 1" and BA: "B ** A = mat 1"
  shows "matrix_inv A = B"
  by (metis AB BA invertible_def matrix_inv_right matrix_mul_assoc matrix_mul_lid) 


lemma matrix_vector_mult_zero_eq:
  assumes P: "invertible P"
  shows "((P**A)*v x = 0) = (A *v x = 0)"
proof (rule iffI)
  assume "P ** A *v x = 0" 
  hence "matrix_inv P *v (P ** A *v x) = matrix_inv P *v 0" by simp
  hence "matrix_inv P *v (P ** A *v x) =  0" by (metis matrix_vector_mult_0_right)
  hence "(matrix_inv P ** P ** A) *v x =  0" by (metis matrix_vector_mul_assoc)
  thus "A *v x =  0" by (metis assms matrix_inv_left matrix_mul_lid)
next
  assume "A *v x = 0" 
  thus "P ** A *v x = 0" by (metis matrix_vector_mul_assoc matrix_vector_mult_0_right)
qed

lemma independent_image_matrix_vector_mult:
  fixes P::"'a::{field}^'n^'m"
  assumes ind_B: "vec.independent B" and inv_P: "invertible P"
  shows "vec.independent (((*v) P)` B)"
proof (rule vec.independent_injective_image)
  show "vec.independent B" using ind_B .
  show "inj_on ((*v) P) (vec.span B)" 
    using inj_matrix_vector_mult[OF inv_P] unfolding inj_on_def by simp
qed

lemma independent_preimage_matrix_vector_mult:
fixes P::"'a::{field}^'n^'n"
assumes ind_B: "vec.independent (((*v) P)` B)" and inv_P: "invertible P"
shows "vec.independent B"
proof -
have "vec.independent (((*v) (matrix_inv P))` (((*v) P)` B))"
  proof (rule independent_image_matrix_vector_mult)
    show "vec.independent ((*v) P ` B)" using ind_B .
    show "invertible (matrix_inv P)"
      by (metis matrix_inv_left matrix_inv_right inv_P invertible_def)
    qed
moreover have "((*v) (matrix_inv P))` (((*v) P)` B) = B"
    proof (auto)
      fix x assume x: "x  B" show "matrix_inv P *v (P *v x)  B" 
      by (metis (full_types) x inv_P matrix_inv_left matrix_vector_mul_assoc matrix_vector_mul_lid)
      thus "x  (*v) (matrix_inv P) ` (*v) P ` B" 
      unfolding image_def 
      by (auto, metis  inv_P matrix_inv_left matrix_vector_mul_assoc matrix_vector_mul_lid)
     qed
ultimately show ?thesis by simp
qed

subsection‹Properties about the dimension of vectors›

lemma dimension_vector[code_unfold]: "vec.dimension TYPE('a::{field}) TYPE('rows::{mod_type})=CARD('rows)"
proof -
let ?f="λx. axis (from_nat x) 1::'a^'rows::{mod_type}"
have "vec.dimension TYPE('a::{field}) TYPE('rows::{mod_type}) = card (cart_basis::('a^'rows::{mod_type}) set)"
  unfolding vec.dimension_def ..
also have "... = card{..<CARD('rows)}" unfolding cart_basis_def 
  proof (rule bij_betw_same_card[symmetric, of ?f], unfold bij_betw_def, unfold inj_on_def axis_eq_axis, auto)
     fix x y assume x: "x < CARD('rows)" and y: "y < CARD('rows)" and eq: "from_nat x = (from_nat y::'rows)"
     show "x = y" using from_nat_eq_imp_eq[OF eq x y] .
     next
     fix i show "axis i 1  (λx. axis (from_nat x::'rows) 1) ` {..<CARD('rows)}" unfolding image_def
     by (auto, metis lessThan_iff to_nat_from_nat to_nat_less_card)
  qed
also have "... = CARD('rows)" by (metis card_lessThan)
finally show ?thesis .
qed

subsection‹Instantiations and interpretations›

text‹Functions between two real vector spaces form a real vector›
instantiation "fun" :: (real_vector, real_vector) real_vector
begin

definition "scaleR_fun a f = (λi. a *R f i )"

instance 
  by (intro_classes, auto simp add: fun_eq_iff scaleR_fun_def scaleR_left.add scaleR_right.add)
end


instantiation vec :: (type, finite) equal
begin
definition equal_vec :: "('a, 'b::finite) vec => ('a, 'b::finite) vec => bool" 
  where "equal_vec x y = (i. x$i = y$i)"
instance 
proof (intro_classes)
  fix x y::"('a, 'b::finite) vec"
  show "equal_class.equal x y = (x = y)" unfolding equal_vec_def using vec_eq_iff by auto
qed
end

interpretation matrix: vector_space "((*k))::'a::{field}=>'a^'cols^'rows=>'a^'cols^'rows"
proof (unfold_locales)
fix a::'a and x y::"'a^'cols^'rows"
show "a *k (x + y) = a *k x + a *k y"
  unfolding matrix_scalar_mult_def vec_eq_iff
  by (simp add: vector_space_over_itself.scale_right_distrib)
next
fix a b::'a and x::"'a^'cols^'rows"
show "(a + b) *k x = a *k x + b *k x"
unfolding matrix_scalar_mult_def vec_eq_iff
  by (simp add: comm_semiring_class.distrib)
show "a *k (b *k x) = a * b *k x"
  unfolding matrix_scalar_mult_def vec_eq_iff by auto
show"1 *k x = x" unfolding matrix_scalar_mult_def vec_eq_iff by auto
qed

end

Theory Fundamental_Subspaces

(*  
    Title:      Fundamental_Subspaces.thy
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
    Maintainer: Jose Divasón <jose.divasonm at unirioja.es>
*)

section‹Fundamental Subspaces›

theory Fundamental_Subspaces
imports 
    Miscellaneous
begin

subsection‹The fundamental subspaces of a matrix›

subsubsection‹Definitions›

definition left_null_space :: "'a::{semiring_1}^'n^'m => ('a^'m) set"
  where "left_null_space A = {x. x v* A = 0}"

definition null_space :: "'a::{semiring_1}^'n^'m => ('a^'n) set"
  where "null_space A = {x. A *v x = 0}"

definition row_space :: "'a::{field}^'n^'m=>('a^'n) set"
  where "row_space A = vec.span (rows A)"

definition col_space :: "'a::{field}^'n^'m=>('a^'m) set"
  where "col_space A = vec.span (columns A)"

subsubsection‹Relationships among them›

lemma left_null_space_eq_null_space_transpose: "left_null_space A = null_space (transpose A)"
  unfolding null_space_def left_null_space_def transpose_vector ..

lemma null_space_eq_left_null_space_transpose: "null_space A = left_null_space (transpose A)" 
  using left_null_space_eq_null_space_transpose[of "transpose A"]
  unfolding transpose_transpose ..

lemma row_space_eq_col_space_transpose:
  fixes A::"'a::{field}^'columns^'rows"
  shows "row_space A = col_space (transpose A)"
  unfolding col_space_def row_space_def columns_transpose[of A] ..

lemma col_space_eq_row_space_transpose:
  fixes A::"'a::{field}^'n^'m"
  shows "col_space A = row_space (transpose A)"
  unfolding col_space_def row_space_def unfolding rows_transpose[of A] ..


subsection‹Proving that they are subspaces›

lemma subspace_null_space:
  fixes A::"'a::{field}^'n^'m"
  shows "vec.subspace (null_space A)"
  by (auto simp: vec.subspace_def null_space_def vec.scale vec.add)

lemma subspace_left_null_space:
  fixes A::"'a::{field}^'n^'m"
  shows "vec.subspace (left_null_space A)"
  unfolding left_null_space_eq_null_space_transpose using subspace_null_space .

lemma subspace_row_space:
  shows "vec.subspace (row_space A)" by (metis row_space_def vec.subspace_span)

lemma subspace_col_space:
  shows "vec.subspace (col_space A)" by (metis col_space_def vec.subspace_span)
  
subsection‹More useful properties and equivalences›

lemma col_space_eq:
  fixes A::"'a::{field}^'m::{finite, wellorder}^'n"
  shows "col_space A = {y. x. A *v x = y}"
proof (unfold col_space_def vec.span_finite[OF finite_columns], auto)
  fix x
  show "A *v x  range (λu. vcolumns A. u v *s v)" using matrix_vmult_column_sum[of A x] by auto
next
  fix u::"('a, 'n) vec  'a"
  let ?g="λy. {i. y=column i A}"
  let ?x="(χ i. if i=(LEAST a. a  ?g (column i A)) then u (column i A) else 0)"
  show "x. A *v x = (vcolumns A. u v *s v)"
  proof (unfold matrix_mult_sum, rule exI[of _ "?x"], auto)
    have inj: "inj_on ?g (columns A)" unfolding inj_on_def unfolding columns_def by auto
    have union_univ: "(?g`(columns A)) = UNIV" unfolding columns_def by auto               
    have "sum (λi.(if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A) UNIV 
        = sum (λi. (if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A) ((?g`(columns A)))"
      unfolding union_univ ..
    also have "... = sum (sum (λi.(if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A)) (?g`(columns A))" 
      by (rule sum.Union_disjoint[unfolded o_def], auto)
    also have "... = sum ((sum (λi.(if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A))  ?g) 
        (columns A)" by (rule sum.reindex, simp add: inj)
    also have "... = sum (λy. u y *s y) (columns A)"
    proof (rule sum.cong, auto)
      fix x
      assume x_in_cols: "x  columns A"
      obtain b where b: "x=column b A" using x_in_cols unfolding columns_def by blast
      let ?f="(λi. (if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A)" 
      have sum_rw: "sum ?f ({i. x = column i A} - {LEAST a. x = column a A}) = 0"
        by (rule sum.neutral, auto)
      have "sum ?f {i. x = column i A} = ?f (LEAST a. x = column a A) + sum ?f ({i. x = column i A} - {LEAST a. x = column a A})" 
        apply (rule sum.remove, auto, rule LeastI_ex) 
        using x_in_cols unfolding columns_def by auto
      also have "... = ?f (LEAST a. x = column a A)" unfolding sum_rw by simp
      also have "... = u x *s x"
      proof (auto, rule LeastI2)
        show "x = column b A" using b .
        fix xa
        assume x: "x = column xa A"
        show "u (column xa A) *s column xa A = u x *s x" unfolding x ..
      next
        assume "(LEAST a. x = column a A)  (LEAST a. column (LEAST c. x = column c A) A = column a A)"
        moreover have "(LEAST a. x = column a A) = (LEAST a. column (LEAST c. x = column c A) A = column a A)"
          by (rule Least_equality[symmetric], rule LeastI2, simp_all add: b, rule Least_le, metis (lifting, full_types) LeastI)
        ultimately show "u x = 0" by contradiction
      qed
      finally show " (i | x = column i A. (if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A) = u x *s x" .
    qed
    finally show "(iUNIV. (if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A) = (ycolumns A. u y *s y)" .
  qed
qed


corollary col_space_eq':
  fixes A::"'a::{field}^'m::{finite, wellorder}^'n"
  shows "col_space A = range (λx. A *v x)"
  unfolding col_space_eq by auto

lemma row_space_eq:
  fixes A::"'a::{field}^'m^'n::{finite, wellorder}"
  shows "row_space A = {w. y. (transpose A) *v y = w}"
  unfolding row_space_eq_col_space_transpose col_space_eq ..

lemma null_space_eq_ker:
  fixes f::"('a::field^'n) => ('a^'m)"
  assumes lf: "Vector_Spaces.linear (*s) (*s) f"
  shows "null_space (matrix f) = {x. f x = 0}" 
  unfolding null_space_def using matrix_works [OF lf] by auto

lemma col_space_eq_range:
  fixes f::"('a::field^'n::{finite, wellorder})  ('a^'m)"
  assumes lf: "Vector_Spaces.linear (*s) (*s) f"
  shows "col_space (matrix f) = range f"
  unfolding col_space_eq unfolding matrix_works[OF lf] by blast

lemma null_space_is_preserved:
  fixes A::"'a::{field}^'cols^'rows"
  assumes P: "invertible P"
  shows "null_space (P**A) = null_space A"
  unfolding null_space_def 
  using P matrix_inv_left matrix_left_invertible_ker matrix_vector_mul_assoc matrix_vector_mult_0_right
  by metis

lemma row_space_is_preserved:
  fixes A::"'a::{field}^'cols^'rows::{finite, wellorder}" 
    and P::"'a::{field}^'rows::{finite, wellorder}^'rows::{finite, wellorder}"
  assumes P: "invertible P"
  shows "row_space (P**A) = row_space A"
proof (auto)
  fix w
  assume w: "w  row_space (P**A)"
  from this obtain y where w_By: "w=(transpose (P**A)) *v y" 
    unfolding row_space_eq[of "P ** A" ] by fast
  have "w = (transpose (P**A)) *v y" using w_By .
  also have "... = ((transpose A) ** (transpose P)) *v y" unfolding matrix_transpose_mul ..
  also have "... = (transpose A) *v ((transpose P) *v y)" unfolding matrix_vector_mul_assoc ..
  finally show "w  row_space A" unfolding row_space_eq by blast
next
  fix w
  assume w: "w  row_space A"
  from this obtain y where w_Ay: "w=(transpose A) *v y" unfolding row_space_eq by fast
  have "w = (transpose A) *v y" using w_Ay .
  also have "... = (transpose ((matrix_inv P) ** (P**A))) *v y" 
    by (metis P matrix_inv_left matrix_mul_assoc matrix_mul_lid)
  also have "... = (transpose (P**A) ** (transpose (matrix_inv P))) *v y" 
    unfolding matrix_transpose_mul ..
  also have "... = transpose (P**A) *v (transpose (matrix_inv P) *v y)" 
    unfolding matrix_vector_mul_assoc ..
  finally show "w  row_space (P**A)"  unfolding row_space_eq by blast
qed
end

Theory Dim_Formula

(*  
    Title:      Dim_Formula.thy
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
    Maintainer: Jose Divasón <jose.divasonm at unirioja.es>
*)

section "Rank Nullity Theorem of Linear Algebra"

theory Dim_Formula
  imports Fundamental_Subspaces
begin

context vector_space
begin

subsection‹Previous results›

text‹Linear dependency is a monotone property, based on the 
  monotonocity of linear independence:›

lemma dependent_mono:
  assumes d:"dependent A"
  and A_in_B: "A  B"
  shows  "dependent B"
  using independent_mono [OF _ A_in_B] d by auto

text‹Given a finite independent set, a linear combination of its 
  elements equal to zero is possible only if every coefficient is zero:›

lemma scalars_zero_if_independent:
  assumes fin_A: "finite A"
  and ind: "independent A"
  and sum: "(xA. scale (f x) x) = 0"
  shows "x  A. f x = 0"
  using fin_A ind local.dependent_finite sum by blast

end

context finite_dimensional_vector_space
begin

text‹In an finite dimensional vector space, every independent set is finite, and 
  thus @{thm [display ]scalars_zero_if_independent [no_vars]} holds:›

corollary scalars_zero_if_independent_euclidean:
  assumes ind: "independent A"
    and sum: "(xA. scale (f x) x) = 0"
  shows "x  A. f x = 0"
  using finiteI_independent ind scalars_zero_if_independent sum by blast

end

text‹The following lemma states that every linear form is injective over the 
  elements which define the basis of the range of the linear form. 
  This property is applied later over the elements of an arbitrary 
  basis which are not in the basis of the nullifier or kernel set 
  (\emph{i.e.}, the candidates to be the basis of the range space 
  of the linear form).›

text‹Thanks to this result, it can be concluded that the cardinal 
  of the elements of a basis which do not belong to the kernel 
  of a linear form @{term "f::'a => 'b"} is equal to the cardinal 
  of the set obtained when applying @{term "f::'a => 'b"} to such elements.›

text‹The application of this lemma is not usually found in the pencil and paper 
  proofs of the ``rank nullity theorem'', but will be crucial to know that,
  being @{term "f::'a => 'b"} a linear form from a finite dimensional
  vector space @{term "V"} to a vector space @{term "V'"}, 
  and given a basis @{term "B::'a set"} of @{term "ker f"}, 
  when @{term "B"} is completed up to a basis of @{term "V::'a set"}
  with a set @{term "W::'a set"}, the cardinal of this set is
  equal to the cardinal of its range set:›
  
context vector_space
begin

lemma inj_on_extended:
  assumes lf: "Vector_Spaces.linear scaleB scaleC f"
  and f: "finite C"
  and ind_C: "independent C"
  and C_eq: "C = B  W"
  and disj_set: "B  W = {}"
  and span_B: "{x. f x = 0}  span B"
  shows "inj_on f W"
  ― ‹The proof is carried out by reductio ad absurdum›
proof (unfold inj_on_def, rule+, rule ccontr)
  interpret lf: Vector_Spaces.linear scaleB scaleC f using lf by simp
  ― ‹Some previous consequences of the premises that are used later:›
  have fin_B: "finite B" using finite_subset [OF _ f] C_eq by simp  
  have ind_B: "independent B" and ind_W: "independent W" 
    using independent_mono[OF ind_C] C_eq by simp_all
  ― ‹The proof starts here; we assume that there exist two different elements›
  ― ‹with the same image:›
  fix x::'b and y::'b
  assume x: "x  W" and y: "y  W" and f_eq: "f x = f y" and x_not_y: "x  y"
  have fin_yB: "finite (insert y B)" using fin_B by simp
  have "f (x - y) = 0" by (metis diff_self f_eq lf.diff)
  hence "x - y  {x. f x = 0}" by simp
  hence "g. (vB. scale (g v) v) = (x - y)" using span_B
    unfolding span_finite [OF fin_B] by force
  then obtain g where sum: "(vB. scale (g v) v) = (x - y)" by blast
  ― ‹We define one of the elements as a linear combination of the second 
      element and the ones in $B$›
  define h :: "'b  'a" where "h a = (if a = y then 1 else g a)" for a
  have "x = y + (vB. scale (g v) v)" using sum by auto
  also have "... = scale (h y) y  + (vB. scale (g v) v)" unfolding h_def by simp
  also have "... = scale (h y) y + (vB. scale (h v) v)"
    apply (unfold add_left_cancel, rule sum.cong) 
    using y h_def empty_iff disj_set by auto   
  also have "... = (v(insert y B). scale (h v) v)"
    by (rule sum.insert[symmetric], rule fin_B)
       (metis (lifting) IntI disj_set empty_iff y)
  finally have x_in_span_yB: "x  span (insert y B)"
    unfolding span_finite[OF fin_yB] by auto
  ― ‹We have that a subset of elements of $C$ is linearly dependent›
  have dep: "dependent (insert x (insert y B))" 
    by (unfold dependent_def, rule bexI [of _ x])
       (metis Diff_insert_absorb Int_iff disj_set empty_iff insert_iff 
         x x_in_span_yB x_not_y, simp)
  ― ‹Therefore, the set $C$ is also dependent:›
  hence "dependent C" using C_eq x y
    by (metis Un_commute Un_upper2 dependent_mono insert_absorb insert_subset)
  ― ‹This yields the contradiction, since $C$ is independent:›
  thus False using ind_C by contradiction
qed
end

subsection‹The proof›

text‹Now the rank nullity theorem can be proved; given any linear form 
  @{term "f::'a => 'b"}, the sum of the dimensions of its kernel and 
  range subspaces is equal to the dimension of the source vector space.›

text‹The statement of the ``rank nullity theorem for linear algebra'', as 
  well as its proof, follow the ones on~\cite{AX97}. The proof is the 
  traditional one found in the literature. The theorem is also named 
  ``fundamental theorem of linear algebra'' in some texts (for instance,
  in~\cite{GO10}).›

context finite_dimensional_vector_space
begin

theorem rank_nullity_theorem:
  assumes l: "Vector_Spaces.linear scale scaleC f"
  shows "dimension = dim {x. f x = 0} + vector_space.dim scaleC (range f)"
proof -
  ― ‹For convenience we define abbreviations for the universe set, $V$, 
    and the kernel of $f$›
  interpret l: Vector_Spaces.linear scale scaleC f by fact
  define V :: "'b set" where "V = UNIV"
  define ker_f where "ker_f = {x. f x = 0}"
  ― ‹The kernel is a proper subspace:›
  have sub_ker: "subspace {x. f x = 0}" using l.subspace_kernel .
  ― ‹The kernel has its proper basis, $B$:›
  obtain B where B_in_ker: "B  {x. f x = 0}"
    and independent_B: "independent B"
    and ker_in_span:"{x. f x = 0}  span B"
    and card_B: "card B = dim {x. f x = 0}" using basis_exists by blast
  ― ‹The space $V$ has a (finite dimensional) basis, $C$:›
  obtain C where B_in_C: "B  C" and C_in_V: "C  V" 
    and independent_C: "independent C"
    and span_C: "V = span C"
    unfolding V_def
    by (metis independent_B extend_basis_superset independent_extend_basis span_extend_basis span_superset)
  ― ‹The basis of $V$, $C$, can be decomposed in the disjoint union of the 
      basis of the kernel, $B$, and its complementary set, $C - B$›
  have C_eq: "C = B  (C - B)" by (rule Diff_partition [OF B_in_C, symmetric])
  have eq_fC: "f ` C = f ` B  f ` (C - B)" 
    by (subst C_eq, unfold image_Un, simp) 
  ― ‹The basis $C$, and its image, are finite, since $V$ is finite-dimensional›
  have finite_C: "finite C"
    using finiteI_independent[OF independent_C] .
  have finite_fC: "finite (f ` C)" by (rule finite_imageI [OF finite_C])
  ― ‹The basis $B$ of the kernel of $f$, and its image, are also finite›
  have finite_B: "finite B" by (rule rev_finite_subset [OF finite_C B_in_C])
  have finite_fB: "finite (f ` B)" by (rule finite_imageI[OF finite_B])
  ― ‹The set $C - B$ is also finite›
  have finite_CB: "finite (C - B)" by (rule finite_Diff [OF finite_C, of B])
  have dim_ker_le_dim_V:"dim (ker_f)  dim V" 
    using dim_subset [of ker_f V] unfolding V_def by simp
  ― ‹Here it starts the proof of the theorem: the sets $B$ and 
      $C - B$ must be proven to be bases, respectively, of the kernel 
      of $f$ and its range›
  show ?thesis
  proof -
    have "dimension = dim V" unfolding V_def dim_UNIV dimension_def
      by (metis basis_card_eq_dim dimension_def independent_Basis span_Basis top_greatest)
    also have "dim V = dim C" unfolding span_C dim_span ..
    also have "... = card C"
      using basis_card_eq_dim [of C C, OF _ span_superset independent_C] by simp
    also have "... = card (B  (C - B))" using C_eq by simp
    also have "... = card B + card (C-B)"
      by (rule card_Un_disjoint[OF finite_B finite_CB], fast)
    also have "... = dim ker_f + card (C-B)" unfolding ker_f_def card_B ..
    ― ‹Now it has to be proved that the elements of $C - B$ are a basis of 
      the range of $f$›
    also have "... = dim ker_f + l.vs2.dim (range f)"
    proof (unfold add_left_cancel)
      define W where "W = C - B"
      have finite_W: "finite W" unfolding W_def using finite_CB .
      have finite_fW: "finite (f ` W)" using finite_imageI[OF finite_W] .
      have "card W = card (f ` W)" 
        by (rule card_image [symmetric], rule inj_on_extended[OF l, of C B], rule finite_C)
          (rule independent_C,unfold W_def, subst C_eq, rule refl, simp, rule ker_in_span)
      also have "... = l.vs2.dim (range f)"
        ― ‹The image set of $W$ is independent and its span contains the range 
             of $f$, so it is a basis of the range:›
      proof (rule l.vs2.basis_card_eq_dim)
        ― ‹1. The image set of $W$ generates the range of $f$:›
        show "range f  l.vs2.span (f ` W)"
        proof (unfold l.vs2.span_finite [OF finite_fW], auto)
          ― ‹Given any element $v$ in $V$, its image can be expressed as a 
            linear combination of elements of the image by $f$ of $C$:›
          fix v :: 'b
          have fV_span: "f ` V  l.vs2.span  (f ` C)"
            by (simp add: span_C l.span_image)
          have "g. (xf`C. scaleC (g x) x) = f v"
            using fV_span unfolding V_def
            using l.vs2.span_finite[OF finite_fC]
            by (metis (no_types, lifting) V_def rangeE rangeI span_C l.span_image)
          then obtain g where fv: "f v = (xf ` C. scaleC (g x) x)" by metis
              ― ‹We recall that $C$ is equal to $B$ union $(C - B)$, and $B$ 
            is the basis of the kernel; thus, the image of the elements of 
            $B$ will be equal to zero:›
          have zero_fB: "(xf ` B. scaleC (g x) x) = 0"
            using B_in_ker by (auto intro!: sum.neutral)
          have zero_inter: "(x(f ` B  f ` W). scaleC (g x) x) = 0"
            using B_in_ker by (auto intro!: sum.neutral)
          have "f v = (xf ` C. scaleC (g x) x)" using fv .
          also have "... = (x(f ` B  f ` W).  scaleC (g x) x)" 
            using eq_fC W_def by simp
          also have "... = 
              (xf ` B. scaleC (g x) x) + (xf ` W. scaleC (g x) x) 
                - (x(f ` B  f ` W). scaleC (g x) x)" 
            using sum_Un [OF finite_fB finite_fW] by simp
          also have "... = (xf ` W. scaleC (g x) x)" 
            unfolding zero_fB zero_inter by simp
              ― ‹We have proved that the image set of $W$ is a generating set 
              of the range of $f$›
          finally show "f v  range (λu. vf ` W. scaleC (u v) v)" by auto
        qed
          ― ‹2. The image set of $W$ is linearly independent:›
        show "l.vs2.independent (f ` W)"
          using finite_fW
        proof (rule l.vs2.independent_if_scalars_zero)
          ― ‹Every linear combination (given by $g x$) of the elements of 
           the image set of $W$ equal to zero, requires every coefficient to 
           be zero:›
          fix g :: "'c => 'a" and w :: 'c
          assume sum: "(xf ` W. scaleC (g x) x) = 0" and w: "w  f ` W"
          have "0 = (xf ` W. scaleC (g x) x)" using sum by simp
          also have "... = sum ((λx. scaleC (g x) x)  f) W"
            by (rule sum.reindex, rule inj_on_extended[OF l, of C B])
              (unfold W_def, rule finite_C, rule independent_C, rule C_eq, simp, 
                rule ker_in_span)
          also have "... = (xW. scaleC ((g  f) x) (f x))" unfolding o_def ..
          also have "... = f (xW. scale ((g  f) x) x)"
            unfolding l.sum[symmetric] l.scale[symmetric] by simp
          finally have f_sum_zero:"f (xW. scale ((g  f) x) x) = 0" by (rule sym)
          hence "(xW. scale ((g  f) x) x)  ker_f" unfolding ker_f_def by simp
          hence "h. (vB. scale (h v) v) = (xW. scale ((g  f) x) x)"
            using span_finite[OF finite_B] using ker_in_span
            unfolding ker_f_def by force
          then obtain h where 
            sum_h: "(vB. scale (h v) v) = (xW. scale ((g  f) x) x)" by blast
          define t where "t a = (if a  B then h a else - ((g  f) a))" for a
          have "0 = (vB. scale (h v) v) + - (xW. scale ((g  f) x) x)" 
            using sum_h by simp
          also have "... =  (vB. scale (h v) v) + (xW. - (scale ((g  f) x) x))" 
            unfolding sum_negf ..
          also have "... = (vB. scale (t v) v) + (xW. -(scale((g  f) x) x))" 
            unfolding add_right_cancel unfolding t_def by simp
          also have "... =  (vB. scale (t v) v) + (xW. scale (t x) x)"
            by (unfold add_left_cancel t_def W_def, rule sum.cong) simp+
          also have "... = (vB  W. scale (t v) v)"
            by (rule sum.union_inter_neutral [symmetric], rule finite_B, rule finite_W) 
              (simp add: W_def)
          finally have "(vB  W. scale (t v) v) = 0" by simp
          hence coef_zero: "xB  W. t x = 0"
            using C_eq scalars_zero_if_independent [OF finite_C independent_C]
            unfolding W_def by simp
          obtain y where w_fy: "w = f y " and y_in_W: "y  W" using w by fast
          have "- g w = t y" 
            unfolding t_def w_fy using y_in_W unfolding W_def by simp
          also have "... = 0" using coef_zero y_in_W unfolding W_def by simp
          finally show "g w = 0" by simp
        qed
      qed auto
      finally show "card (C - B) = l.vs2.dim (range f)" unfolding W_def .
    qed
    finally show ?thesis unfolding V_def ker_f_def unfolding dim_UNIV .
  qed
qed

end

subsection‹The rank nullity theorem for matrices›

text‹The proof of the theorem for matrices
  is direct, as a consequence of the ``rank nullity theorem''.›

lemma rank_nullity_theorem_matrices:
  fixes A::"'a::{field}^'cols::{finite, wellorder}^'rows"
  shows "ncols A = vec.dim (null_space A) + vec.dim (col_space A)"
  using vec.rank_nullity_theorem[OF matrix_vector_mul_linear_gen, of A]
  apply (subst (2 3) matrix_of_matrix_vector_mul [of A, symmetric])
  unfolding null_space_eq_ker[OF matrix_vector_mul_linear_gen]
  unfolding col_space_eq_range [OF matrix_vector_mul_linear_gen]
  unfolding vec.dimension_def ncols_def card_cart_basis
  by simp

end