# 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)

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
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'
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"

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 = (∑i∈UNIV. 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 = (∑y∈columns 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. ∑v∈columns 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 = (∑v∈columns 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 "(∑i∈UNIV. (if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A) = (∑y∈columns 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: "(∑x∈A. 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: "(∑x∈A. 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. (∑v∈B. scale (g v) v) = (x - y)" using span_B unfolding span_finite [OF fin_B] by force then obtain g where sum: "(∑v∈B. 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 + (∑v∈B. scale (g v) v)" using sum by auto also have "... = scale (h y) y + (∑v∈B. scale (g v) v)" unfolding h_def by simp also have "... = scale (h y) y + (∑v∈B. 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. (∑x∈fC. 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 = (∑x∈f  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: "(∑x∈f  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 = (∑x∈f  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 "... = (∑x∈f  B. scaleC (g x) x) + (∑x∈f  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 "... = (∑x∈f  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. ∑v∈f  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: "(∑x∈f  W. scaleC (g x) x) = 0" and w: "w ∈ f  W"
have "0 = (∑x∈f  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 "... = (∑x∈W. scaleC ((g ∘ f) x) (f x))" unfolding o_def ..
also have "... = f (∑x∈W. scale ((g ∘ f) x) x)"
unfolding l.sum[symmetric] l.scale[symmetric] by simp
finally have f_sum_zero:"f (∑x∈W. scale ((g ∘ f) x) x) = 0" by (rule sym)
hence "(∑x∈W. scale ((g ∘ f) x) x) ∈ ker_f" unfolding ker_f_def by simp
hence "∃h. (∑v∈B. scale (h v) v) = (∑x∈W. 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: "(∑v∈B. scale (h v) v) = (∑x∈W. 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 = (∑v∈B. scale (h v) v) + - (∑x∈W. scale ((g ∘ f) x) x)"
using sum_h by simp
also have "... =  (∑v∈B. scale (h v) v) + (∑x∈W. - (scale ((g ∘ f) x) x))"
unfolding sum_negf ..
also have "... = (∑v∈B. scale (t v) v) + (∑x∈W. -(scale((g ∘ f) x) x))"
unfolding add_right_cancel unfolding t_def by simp
also have "... =  (∑v∈B. scale (t v) v) + (∑x∈W. scale (t x) x)"
by (unfold add_left_cancel t_def W_def, rule sum.cong) simp+
also have "... = (∑v∈B ∪ W. scale (t v) v)"
by (rule sum.union_inter_neutral [symmetric], rule finite_B, rule finite_W)
finally have "(∑v∈B ∪ W. scale (t v) v) = 0" by simp
hence coef_zero: "∀x∈B ∪ 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
`