# Theory Linear_Algebra_On_With

```(*  Title:      HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy
Author:     Fabian Immler, TU München
*)
theory Linear_Algebra_On_With
imports
Group_On_With
Complex_Main
begin

definition span_with
where "span_with pls zero scl b =
{sum_with pls zero (λa. scl (r a) a) t | t r. finite t ∧ t ⊆ b}"

lemma span_with_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A"
shows "((A ===> A ===> A) ===> A ===> ((=) ===> A ===> A) ===> rel_set A ===> rel_set A)
span_with span_with"
unfolding span_with_def
proof (intro rel_funI)
fix p p' z z' X X' and s s'::"'c ⇒ _"
assume transfer_rules[transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'"
have "Domainp A z" using ‹A z z'› by force
have *: "t ⊆ X ⟹ (∀x∈t. Domainp A x)" for t
by (meson Domainp.DomainI ‹rel_set A X X'› rel_setD1 subsetD)
note swt=sum_with_transfer[OF assms(1,2,2), THEN rel_funD, THEN rel_funD, THEN rel_funD, THEN rel_funD, OF transfer_rules(1,2)]
have DsI: "Domainp A (sum_with p z r t)" if "⋀x. x ∈ t ⟹ Domainp A (r x)" "t ⊆ Collect (Domainp A)" for r t
proof cases
assume ex: "∃C. r ` t ⊆ C ∧ comm_monoid_add_on_with C p z"
have "Domainp (rel_set A) t" using that by (auto simp: Domainp_set)
from ex_comm_monoid_add_around_imageE[OF ex transfer_rules(1,2) this that(1)]
obtain C where C: "comm_monoid_add_on_with C p z" "r ` t ⊆ C" "Domainp (rel_set A) C" by auto
interpret comm_monoid_add_on_with C p z by fact
from sum_with_mem[OF C(2)] C(3)
show ?thesis
by auto (meson C(3) Domainp_set)
qed (use ‹A z _› in ‹auto simp: sum_with_def›)
from Domainp_apply2I[OF transfer_rules(3)]
have Domainp_sI: "Domainp A x ⟹ Domainp A (s y x)" for x y by auto
show "rel_set A
{sum_with p z (λa. s (r a) a) t |t r. finite t ∧ t ⊆ X}
{sum_with p' z' (λa. s' (r a) a) t |t r. finite t ∧ t ⊆ X'}"
apply (transfer_prover_start, transfer_step+)
using *
by (auto simp: intro!: DsI Domainp_sI)
qed

definition dependent_with
where "dependent_with pls zero scl s =
(∃t u. finite t ∧ t ⊆ s ∧ (sum_with pls zero (λv. scl (u v) v) t = zero ∧ (∃v∈t. u v ≠ 0)))"

lemma dependent_with_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A"
shows "((A ===> A ===> A) ===> A ===> ((=) ===> A ===> A) ===> rel_set A ===> (=))
dependent_with dependent_with"
unfolding dependent_with_def dependent_with_def
proof (intro rel_funI)
fix p p' z z' X X' and s s'::"'c ⇒ _"
assume [transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'"
have *: "t ⊆ X ⟹ (∀x∈t. Domainp A x)" for t
by (meson Domainp.DomainI ‹rel_set A X X'› rel_setD1 subsetD)
show "(∃t u. finite t ∧ t ⊆ X ∧ sum_with p z (λv. s (u v) v) t = z ∧ (∃v∈t. u v ≠ 0)) =
(∃t u. finite t ∧ t ⊆ X' ∧ sum_with p' z' (λv. s' (u v) v) t = z' ∧ (∃v∈t. u v ≠ 0))"
apply (transfer_prover_start, transfer_step+)
using *
qed

definition subspace_with
where "subspace_with pls zero scl S ⟷ zero ∈ S ∧ (∀x∈S. ∀y∈S. pls x y ∈ S) ∧ (∀c. ∀x∈S. scl c x ∈ S)"

lemma subspace_with_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "bi_unique A"
shows "((A ===> A ===> A) ===> A ===> ((=) ===> A ===> A) ===> rel_set A ===> (=))
subspace_with subspace_with"
unfolding span_with_def subspace_with_def
by transfer_prover

definition "module_on_with S pls mns um zero (scl::'a::comm_ring_1⇒_) ⟷
ab_group_add_on_with S pls zero mns um ∧
((∀a. ∀x∈S.
∀y∈S. scl a (pls x y) = pls (scl a x) (scl a y)) ∧
(∀a b. ∀x∈S. scl (a + b) x = pls (scl a x) (scl b x))) ∧
(∀a b. ∀x∈S. scl a (scl b x) = scl (a * b) x) ∧
(∀x∈S. scl 1 x = x) ∧
(∀a. ∀x∈S. scl a x ∈ S)"

definition "vector_space_on_with S pls mns um zero (scl::'a::field⇒_) ⟷
module_on_with S pls mns um zero scl"

definition "module_pair_on_with S S' pls mns um zero (scl::'a::comm_ring_1⇒_) pls' mns' um' zero' (scl'::'a::comm_ring_1⇒_) ⟷
module_on_with S pls mns um zero scl ∧ module_on_with S' pls' mns' um' zero' scl'"

definition "vector_space_pair_on_with S S' pls mns um zero (scl::'a::field⇒_) pls' mns' um' zero' (scl'::'a::field⇒_) ⟷
module_pair_on_with S S' pls mns um zero scl pls' mns' um' zero' scl'"

definition "module_hom_on_with S1 S2 plus1 minus1 uminus1 zero1 (scale1::'a::comm_ring_1⇒_)
plus2 minus2 uminus2 zero2 (scale2::'a::comm_ring_1⇒_) f ⟷
module_pair_on_with S1 S2 plus1 minus1 uminus1 zero1 scale1
plus2 minus2 uminus2 zero2 scale2 ∧
(∀x∈S1. ∀y∈S1. f (plus1 x y) = plus2 (f x) (f y)) ∧
(∀s. ∀x∈S1. f (scale1 s x) = scale2 s (f x))"

definition "linear_on_with S1 S2 plus1 minus1 uminus1 zero1 (scale1::'a::field⇒_)
plus2 minus2 uminus2 zero2 (scale2::'a::field⇒_) f ⟷
module_hom_on_with S1 S2 plus1 minus1 uminus1 zero1 scale1
plus2 minus2 uminus2 zero2 scale2 f"

definition dim_on_with
where "dim_on_with S pls zero scale V =
(if ∃b ⊆ S. ¬ dependent_with pls zero scale b ∧ span_with pls zero scale b = span_with pls zero scale V
then card (SOME b. b ⊆ S ∧¬ dependent_with pls zero scale b ∧ span_with pls zero scale b = span_with pls zero scale V)
else 0)"

definition "finite_dimensional_vector_space_on_with S pls mns um zero (scl::'a::field⇒_) basis ⟷
vector_space_on_with S pls mns um zero scl ∧
finite basis ∧
¬ dependent_with pls zero scl basis ∧
span_with pls zero scl basis = S"

definition "finite_dimensional_vector_space_pair_1_on_with S S' pls mns um zero (scl::'a::field⇒_) b
pls' mns' um' zero' (scl'::'a::field⇒_) ⟷
finite_dimensional_vector_space_on_with S pls mns um zero (scl::'a::field⇒_) b ∧
vector_space_on_with S' pls' mns' um' zero' (scl'::'a::field⇒_)"

definition "finite_dimensional_vector_space_pair_on_with S S' pls mns um zero (scl::'a::field⇒_) b
pls' mns' um' zero' (scl'::'a::field⇒_) b' ⟷
finite_dimensional_vector_space_on_with S pls mns um zero (scl::'a::field⇒_) b ∧
finite_dimensional_vector_space_on_with S' pls' mns' um' zero' (scl'::'a::field⇒_) b'"

context module begin

lemma span_with:
"span = (λX. span_with (+) 0 scale X)"
unfolding span_explicit span_with_def sum_with ..

lemma dependent_with:
"dependent = (λX. dependent_with (+) 0 scale X)"
unfolding dependent_explicit dependent_with_def sum_with ..

lemma subspace_with:
"subspace = (λX. subspace_with (+) 0 scale X)"
unfolding subspace_def subspace_with_def ..

end

lemmas [explicit_ab_group_add] = module.span_with module.dependent_with module.subspace_with

lemma module_on_with_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A"
shows
"(rel_set A ===> (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===> (=))
module_on_with module_on_with"
unfolding module_on_with_def
by transfer_prover

lemma vector_space_on_with_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A"
shows
"(rel_set A ===> (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===> (=))
vector_space_on_with vector_space_on_with"
unfolding vector_space_on_with_def
by transfer_prover

context vector_space begin

lemma dim_with: "dim = (λX. dim_on_with UNIV (+) 0 scale X)"
unfolding dim_def dim_on_with_def dependent_with span_with by force

end

lemma module_pair_on_with_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A" "right_total C" "bi_unique C"
shows
"(rel_set A ===> rel_set C ===>
(A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===>
(C ===> C ===> C) ===> (C ===> C ===> C) ===> (C ===> C) ===> C ===> ((=) ===> C ===> C) ===>
(=)) module_pair_on_with module_pair_on_with"
unfolding module_pair_on_with_def
by transfer_prover

lemma module_hom_on_with_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A" "right_total C" "bi_unique C"
shows
"(rel_set A ===> rel_set C ===>
(A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===>
(C ===> C ===> C) ===> (C ===> C ===> C) ===> (C ===> C) ===> C ===> ((=) ===> C ===> C) ===>
(A ===> C) ===> (=)) module_hom_on_with module_hom_on_with"
unfolding module_hom_on_with_def
by transfer_prover

lemma linear_on_with_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A" "right_total C" "bi_unique C"
shows
"(rel_set A ===> rel_set C ===>
(A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===>
(C ===> C ===> C) ===> (C ===> C ===> C) ===> (C ===> C) ===> C ===> ((=) ===> C ===> C) ===>
(A ===> C) ===> (=)) linear_on_with linear_on_with"
unfolding linear_on_with_def
by transfer_prover

subsubsection ‹Explicit locale formulations›

lemma module_on_with[explicit_ab_group_add]: "module s ⟷ module_on_with UNIV (+) (-) uminus 0 s"
and vector_space_on_with[explicit_ab_group_add]: "vector_space t ⟷ vector_space_on_with UNIV (+) (-) uminus 0 t"
by (auto simp: module_def module_on_with_def ab_group_add_axioms
vector_space_def vector_space_on_with_def)

"vector_space_on_with S (+) (-) uminus 0 s ⟹ module_on_with S (+) (-) uminus 0 s"

"finite_dimensional_vector_space t b ⟷ finite_dimensional_vector_space_on_with UNIV (+) (-) uminus 0 t b"
by (auto simp: finite_dimensional_vector_space_on_with_def finite_dimensional_vector_space_def

"finite_dimensional_vector_space_on_with S (+) (-) uminus 0 s basis ⟹
vector_space_on_with S  (+) (-) uminus 0 s"
by (auto simp: finite_dimensional_vector_space_on_with_def)

"module_hom s1 s2 f ⟷ module_hom_on_with UNIV UNIV (+) (-) uminus 0 s1 (+) (-) uminus 0 s2 f"
"Vector_Spaces.linear t1 t2 f ⟷ linear_on_with UNIV UNIV (+) (-) uminus 0 t1 (+) (-) uminus 0 t2 f"
"module_pair s1 s2 ⟷ module_pair_on_with UNIV UNIV (+) (-) uminus 0 s1 (+) (-) uminus 0 s2"
by (auto simp: module_hom_def module_hom_on_with_def module_pair_on_with_def
Vector_Spaces.linear_def linear_on_with_def vector_space_on_with
module_on_with_def vector_space_on_with_def
module_hom_axioms_def module_pair_def module_on_with)

"vector_space_pair s1 s2 ⟷ vector_space_pair_on_with UNIV UNIV (+) (-) uminus 0 s1  (+) (-) uminus 0 s2"
vector_space_pair_on_with_def vector_space_pair_def module_on_with_def vector_space_on_with_def)

"finite_dimensional_vector_space_pair_1 s1 b1 s2 ⟷
finite_dimensional_vector_space_pair_1_on_with UNIV UNIV (+) (-) uminus 0 s1 b1 (+) (-) uminus 0 s2"
by (auto simp: finite_dimensional_vector_space_pair_1_def
finite_dimensional_vector_space_pair_1_on_with_def finite_dimensional_vector_space_on_with
vector_space_on_with)

"finite_dimensional_vector_space_pair s1 b1 s2 b2 ⟷
finite_dimensional_vector_space_pair_on_with UNIV UNIV (+) (-) uminus 0 s1 b1 (+) (-) uminus 0 s2 b2"
by (auto simp: finite_dimensional_vector_space_pair_def
finite_dimensional_vector_space_pair_on_with_def finite_dimensional_vector_space_on_with)

"module_on_with S (+) (-) uminus 0 s"
"module_on_with T (+) (-) uminus 0 t"
if "module_pair_on_with S T (+) (-) uminus 0 s (+) (-) uminus 0 t"
using that
unfolding module_pair_on_with_def
by simp_all

"vector_space_on_with S (+) (-) uminus 0 s"
"vector_space_on_with T (+) (-) uminus 0 t"
if "vector_space_pair_on_with S T(+) (-) uminus 0 s (+) (-) uminus 0 t"
using that
by (auto simp: vector_space_pair_on_with_def module_pair_on_with_def vector_space_on_with_def)

"vector_space_on_with S (+) (-) uminus 0 s"
"finite_dimensional_vector_space_on_with S (+) (-) uminus 0 s b"
"vector_space_on_with T (+) (-) uminus 0 t"
if "finite_dimensional_vector_space_pair_1_on_with S T (+) (-) uminus 0 s b (+) (-) uminus 0 t"
using that
unfolding finite_dimensional_vector_space_pair_1_on_with_def

"vector_space_on_with S (+) (-) uminus 0 s"
"finite_dimensional_vector_space_on_with T (+) (-) uminus 0 t c"
"vector_space_on_with T (+) (-) uminus 0 t"
"finite_dimensional_vector_space_on_with T (+) (-) uminus 0 t c"
if "finite_dimensional_vector_space_pair_on_with S T (+) (-) uminus 0 s b (+) (-) uminus 0 t c"
using that
unfolding finite_dimensional_vector_space_pair_on_with_def

lemma finite_dimensional_vector_space_on_with_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A"
shows
"(rel_set A ===>
(A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===>
rel_set A ===>
(=)) (finite_dimensional_vector_space_on_with) finite_dimensional_vector_space_on_with"
unfolding finite_dimensional_vector_space_on_with_def
by transfer_prover

lemma finite_dimensional_vector_space_pair_on_with_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A" "right_total C" "bi_unique C"
shows
"(rel_set A ===> rel_set C ===>
(A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===>
rel_set A ===>
(C ===> C ===> C) ===> (C ===> C ===> C) ===> (C ===> C) ===> C ===> ((=) ===> C ===> C) ===>
rel_set C ===>
(=)) (finite_dimensional_vector_space_pair_on_with) finite_dimensional_vector_space_pair_on_with"
unfolding finite_dimensional_vector_space_pair_on_with_def
by transfer_prover

end```