(* 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 (\<lambda>a. scl (r a) a) t | t r. finite t \<and> t \<subseteq> 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 \<Rightarrow> _"
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 \<open>A z z'\<close> by force
have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t
by (meson Domainp.DomainI \<open>rel_set A X X'\<close> 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 "\<And>x. x \<in> t \<Longrightarrow> Domainp A (r x)" "t \<subseteq> Collect (Domainp A)" for r t
proof cases
assume ex: "\<exists>C. r ` t \<subseteq> C \<and> 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 \<subseteq> 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 \<open>A z _\<close> in \<open>auto simp: sum_with_def\<close>)
from Domainp_apply2I[OF transfer_rules(3)]
have Domainp_sI: "Domainp A x \<Longrightarrow> Domainp A (s y x)" for x y by auto
show "rel_set A
{sum_with p z (\<lambda>a. s (r a) a) t |t r. finite t \<and> t \<subseteq> X}
{sum_with p' z' (\<lambda>a. s' (r a) a) t |t r. finite t \<and> t \<subseteq> 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 =
(\<exists>t u. finite t \<and> t \<subseteq> s \<and> (sum_with pls zero (\<lambda>v. scl (u v) v) t = zero \<and> (\<exists>v\<in>t. u v \<noteq> 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 \<Rightarrow> _"
assume [transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'"
have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t
by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 subsetD)
show "(\<exists>t u. finite t \<and> t \<subseteq> X \<and> sum_with p z (\<lambda>v. s (u v) v) t = z \<and> (\<exists>v\<in>t. u v \<noteq> 0)) =
(\<exists>t u. finite t \<and> t \<subseteq> X' \<and> sum_with p' z' (\<lambda>v. s' (u v) v) t = z' \<and> (\<exists>v\<in>t. u v \<noteq> 0))"
apply (transfer_prover_start, transfer_step+)
using *
by (auto simp: intro!: comm_monoid_add_on_with.sum_with_mem)
qed
definition subspace_with
where "subspace_with pls zero scl S \<longleftrightarrow> zero \<in> S \<and> (\<forall>x\<in>S. \<forall>y\<in>S. pls x y \<in> S) \<and> (\<forall>c. \<forall>x\<in>S. scl c x \<in> 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\<Rightarrow>_) \<longleftrightarrow>
ab_group_add_on_with S pls zero mns um \<and>
((\<forall>a. \<forall>x\<in>S.
\<forall>y\<in>S. scl a (pls x y) = pls (scl a x) (scl a y)) \<and>
(\<forall>a b. \<forall>x\<in>S. scl (a + b) x = pls (scl a x) (scl b x))) \<and>
(\<forall>a b. \<forall>x\<in>S. scl a (scl b x) = scl (a * b) x) \<and>
(\<forall>x\<in>S. scl 1 x = x) \<and>
(\<forall>a. \<forall>x\<in>S. scl a x \<in> S)"
definition "vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_) \<longleftrightarrow>
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\<Rightarrow>_) pls' mns' um' zero' (scl'::'a::comm_ring_1\<Rightarrow>_) \<longleftrightarrow>
module_on_with S pls mns um zero scl \<and> module_on_with S' pls' mns' um' zero' scl'"
definition "vector_space_pair_on_with S S' pls mns um zero (scl::'a::field\<Rightarrow>_) pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_) \<longleftrightarrow>
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\<Rightarrow>_)
plus2 minus2 uminus2 zero2 (scale2::'a::comm_ring_1\<Rightarrow>_) f \<longleftrightarrow>
module_pair_on_with S1 S2 plus1 minus1 uminus1 zero1 scale1
plus2 minus2 uminus2 zero2 scale2 \<and>
(\<forall>x\<in>S1. \<forall>y\<in>S1. f (plus1 x y) = plus2 (f x) (f y)) \<and>
(\<forall>s. \<forall>x\<in>S1. f (scale1 s x) = scale2 s (f x))"
definition "linear_on_with S1 S2 plus1 minus1 uminus1 zero1 (scale1::'a::field\<Rightarrow>_)
plus2 minus2 uminus2 zero2 (scale2::'a::field\<Rightarrow>_) f \<longleftrightarrow>
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 \<exists>b \<subseteq> S. \<not> dependent_with pls zero scale b \<and> span_with pls zero scale b = span_with pls zero scale V
then card (SOME b. b \<subseteq> S \<and>\<not> dependent_with pls zero scale b \<and> 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\<Rightarrow>_) basis \<longleftrightarrow>
vector_space_on_with S pls mns um zero scl \<and>
finite basis \<and>
\<not> dependent_with pls zero scl basis \<and>
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\<Rightarrow>_) b
pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_) \<longleftrightarrow>
finite_dimensional_vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_) b \<and>
vector_space_on_with S' pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_)"
definition "finite_dimensional_vector_space_pair_on_with S S' pls mns um zero (scl::'a::field\<Rightarrow>_) b
pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_) b' \<longleftrightarrow>
finite_dimensional_vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_) b \<and>
finite_dimensional_vector_space_on_with S' pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_) b'"
context module begin
lemma span_with:
"span = (\<lambda>X. span_with (+) 0 scale X)"
unfolding span_explicit span_with_def sum_with ..
lemma dependent_with:
"dependent = (\<lambda>X. dependent_with (+) 0 scale X)"
unfolding dependent_explicit dependent_with_def sum_with ..
lemma subspace_with:
"subspace = (\<lambda>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 = (\<lambda>X. dim_on_with UNIV (+) 0 scale X)"
unfolding dim_def dim_on_with_def dependent_with span_with by force
end
lemmas [explicit_ab_group_add] = vector_space.dim_with
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 \<open>Explicit locale formulations\<close>
lemma module_on_with[explicit_ab_group_add]: "module s \<longleftrightarrow> module_on_with UNIV (+) (-) uminus 0 s"
and vector_space_on_with[explicit_ab_group_add]: "vector_space t \<longleftrightarrow> 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)
lemma vector_space_with_imp_module_with[explicit_ab_group_add]:
"vector_space_on_with S (+) (-) uminus 0 s \<Longrightarrow> module_on_with S (+) (-) uminus 0 s"
by (simp add: vector_space_on_with_def)
lemma finite_dimensional_vector_space_on_with[explicit_ab_group_add]:
"finite_dimensional_vector_space t b \<longleftrightarrow> 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_axioms_def explicit_ab_group_add)
lemma vector_space_with_imp_finite_dimensional_vector_space_with[explicit_ab_group_add]:
"finite_dimensional_vector_space_on_with S (+) (-) uminus 0 s basis \<Longrightarrow>
vector_space_on_with S (+) (-) uminus 0 s"
by (auto simp: finite_dimensional_vector_space_on_with_def)
lemma module_hom_on_with[explicit_ab_group_add]:
"module_hom s1 s2 f \<longleftrightarrow> module_hom_on_with UNIV UNIV (+) (-) uminus 0 s1 (+) (-) uminus 0 s2 f"
and linear_with[explicit_ab_group_add]:
"Vector_Spaces.linear t1 t2 f \<longleftrightarrow> linear_on_with UNIV UNIV (+) (-) uminus 0 t1 (+) (-) uminus 0 t2 f"
and module_pair_on_with[explicit_ab_group_add]:
"module_pair s1 s2 \<longleftrightarrow> 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)
lemma vector_space_pair_with[explicit_ab_group_add]:
"vector_space_pair s1 s2 \<longleftrightarrow> vector_space_pair_on_with UNIV UNIV (+) (-) uminus 0 s1 (+) (-) uminus 0 s2"
by (auto simp: module_pair_on_with_def explicit_ab_group_add
vector_space_pair_on_with_def vector_space_pair_def module_on_with_def vector_space_on_with_def)
lemma finite_dimensional_vector_space_pair_1_with[explicit_ab_group_add]:
"finite_dimensional_vector_space_pair_1 s1 b1 s2 \<longleftrightarrow>
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)
lemma finite_dimensional_vector_space_pair_with[explicit_ab_group_add]:
"finite_dimensional_vector_space_pair s1 b1 s2 b2 \<longleftrightarrow>
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)
lemma module_pair_with_imp_module_with[explicit_ab_group_add]:
"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
lemma vector_space_pair_with_imp_vector_space_with[explicit_ab_group_add]:
"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)
lemma finite_dimensional_vector_space_pair_1_with_imp_with[explicit_ab_group_add]:
"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
by (simp_all add: finite_dimensional_vector_space_on_with_def)
lemma finite_dimensional_vector_space_pair_with_imp_finite_dimensional_vector_space_with[explicit_ab_group_add]:
"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
by (simp_all add: finite_dimensional_vector_space_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