--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Fri Jul 13 17:18:07 2018 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Fri Jul 13 17:27:05 2018 +0100
@@ -18,40 +18,6 @@
imports Path_Connected Homeomorphism
begin
-subsection \<open>Unit cubes\<close>
-
-(* FIXME mv euclidean topological space *)
-definition unit_cube :: "'a::euclidean_space set"
- where "unit_cube = {x. \<forall>i\<in>Basis. 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1}"
-
-lemma mem_unit_cube: "x \<in> unit_cube \<longleftrightarrow> (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
- unfolding unit_cube_def by simp
-
-lemma bounded_unit_cube: "bounded unit_cube"
- unfolding bounded_def
-proof (intro exI ballI)
- fix y :: 'a assume y: "y \<in> unit_cube"
- have "dist 0 y = norm y" by (rule dist_0_norm)
- also have "\<dots> = norm (\<Sum>i\<in>Basis. (y \<bullet> i) *\<^sub>R i)" unfolding euclidean_representation ..
- also have "\<dots> \<le> (\<Sum>i\<in>Basis. norm ((y \<bullet> i) *\<^sub>R i))" by (rule norm_sum)
- also have "\<dots> \<le> (\<Sum>i::'a\<in>Basis. 1)"
- by (rule sum_mono, simp add: y [unfolded mem_unit_cube])
- finally show "dist 0 y \<le> (\<Sum>i::'a\<in>Basis. 1)" .
-qed
-
-lemma closed_unit_cube: "closed unit_cube"
- unfolding unit_cube_def Collect_ball_eq Collect_conj_eq
- by (rule closed_INT, auto intro!: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
-
-lemma compact_unit_cube: "compact unit_cube" (is "compact ?C")
- unfolding compact_eq_seq_compact_metric
- using bounded_unit_cube closed_unit_cube
- by (rule bounded_closed_imp_seq_compact)
-
-lemma convex_unit_cube: "convex unit_cube"
- by (rule is_interval_convex) (fastforce simp add: is_interval_def mem_unit_cube)
-
-
(* FIXME mv topology euclidean space *)
subsection \<open>Retractions\<close>
@@ -3126,44 +3092,44 @@
subsection \<open>Brouwer's fixed point theorem\<close>
-text \<open>We start proving Brouwer's fixed point theorem for unit cubes.\<close>
+text \<open>We start proving Brouwer's fixed point theorem for the unit cube = \<open>cbox 0 One\<close>.\<close>
lemma brouwer_cube:
fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
- assumes "continuous_on unit_cube f"
- and "f ` unit_cube \<subseteq> unit_cube"
- shows "\<exists>x\<in>unit_cube. f x = x"
+ assumes "continuous_on (cbox 0 One) f"
+ and "f ` cbox 0 One \<subseteq> cbox 0 One"
+ shows "\<exists>x\<in>cbox 0 One. f x = x"
proof (rule ccontr)
define n where "n = DIM('a)"
have n: "1 \<le> n" "0 < n" "n \<noteq> 0"
unfolding n_def by (auto simp: Suc_le_eq DIM_positive)
assume "\<not> ?thesis"
- then have *: "\<not> (\<exists>x\<in>unit_cube. f x - x = 0)"
+ then have *: "\<not> (\<exists>x\<in>cbox 0 One. f x - x = 0)"
by auto
obtain d where
- d: "d > 0" "\<And>x. x \<in> unit_cube \<Longrightarrow> d \<le> norm (f x - x)"
- apply (rule brouwer_compactness_lemma[OF compact_unit_cube _ *])
+ d: "d > 0" "\<And>x. x \<in> cbox 0 One \<Longrightarrow> d \<le> norm (f x - x)"
+ apply (rule brouwer_compactness_lemma[OF compact_cbox _ *])
apply (rule continuous_intros assms)+
apply blast
done
- have *: "\<forall>x. x \<in> unit_cube \<longrightarrow> f x \<in> unit_cube"
- "\<forall>x. x \<in> (unit_cube::'a set) \<longrightarrow> (\<forall>i\<in>Basis. True \<longrightarrow> 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
+ have *: "\<forall>x. x \<in> cbox 0 One \<longrightarrow> f x \<in> cbox 0 One"
+ "\<forall>x. x \<in> (cbox 0 One::'a set) \<longrightarrow> (\<forall>i\<in>Basis. True \<longrightarrow> 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
using assms(2)[unfolded image_subset_iff Ball_def]
- unfolding mem_unit_cube
+ unfolding cbox_def
by auto
obtain label :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where label [rule_format]:
"\<forall>x. \<forall>i\<in>Basis. label x i \<le> 1"
- "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> x \<bullet> i = 0 \<longrightarrow> label x i = 0"
- "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> x \<bullet> i = 1 \<longrightarrow> label x i = 1"
- "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> label x i = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i"
- "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> label x i = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
+ "\<forall>x. \<forall>i\<in>Basis. x \<in> cbox 0 One \<and> x \<bullet> i = 0 \<longrightarrow> label x i = 0"
+ "\<forall>x. \<forall>i\<in>Basis. x \<in> cbox 0 One \<and> x \<bullet> i = 1 \<longrightarrow> label x i = 1"
+ "\<forall>x. \<forall>i\<in>Basis. x \<in> cbox 0 One \<and> label x i = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i"
+ "\<forall>x. \<forall>i\<in>Basis. x \<in> cbox 0 One \<and> label x i = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
using kuhn_labelling_lemma[OF *] by auto
note label = this [rule_format]
- have lem1: "\<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>i\<in>Basis. label x i \<noteq> label y i \<longrightarrow>
+ have lem1: "\<forall>x\<in>cbox 0 One. \<forall>y\<in>cbox 0 One. \<forall>i\<in>Basis. label x i \<noteq> label y i \<longrightarrow>
\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
proof safe
fix x y :: 'a
- assume x: "x \<in> unit_cube" and y: "y \<in> unit_cube"
+ assume x: "x \<in> cbox 0 One" and y: "y \<in> cbox 0 One"
fix i
assume i: "label x i \<noteq> label y i" "i \<in> Basis"
have *: "\<And>x y fx fy :: real. x \<le> fx \<and> fy \<le> y \<or> fx \<le> x \<and> y \<le> fy \<Longrightarrow>
@@ -3188,18 +3154,18 @@
finally show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
unfolding inner_simps .
qed
- have "\<exists>e>0. \<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>z\<in>unit_cube. \<forall>i\<in>Basis.
+ have "\<exists>e>0. \<forall>x\<in>cbox 0 One. \<forall>y\<in>cbox 0 One. \<forall>z\<in>cbox 0 One. \<forall>i\<in>Basis.
norm (x - z) < e \<longrightarrow> norm (y - z) < e \<longrightarrow> label x i \<noteq> label y i \<longrightarrow>
\<bar>(f(z) - z)\<bullet>i\<bar> < d / (real n)"
proof -
have d': "d / real n / 8 > 0"
using d(1) by (simp add: n_def DIM_positive)
- have *: "uniformly_continuous_on unit_cube f"
- by (rule compact_uniformly_continuous[OF assms(1) compact_unit_cube])
+ have *: "uniformly_continuous_on (cbox 0 One) f"
+ by (rule compact_uniformly_continuous[OF assms(1) compact_cbox])
obtain e where e:
"e > 0"
- "\<And>x x'. x \<in> unit_cube \<Longrightarrow>
- x' \<in> unit_cube \<Longrightarrow>
+ "\<And>x x'. x \<in> cbox 0 One \<Longrightarrow>
+ x' \<in> cbox 0 One \<Longrightarrow>
norm (x' - x) < e \<Longrightarrow>
norm (f x' - f x) < d / real n / 8"
using *[unfolded uniformly_continuous_on_def,rule_format,OF d']
@@ -3211,7 +3177,7 @@
using d' e by auto
fix x y z i
assume as:
- "x \<in> unit_cube" "y \<in> unit_cube" "z \<in> unit_cube"
+ "x \<in> cbox 0 One" "y \<in> cbox 0 One" "z \<in> cbox 0 One"
"norm (x - z) < min (e / 2) (d / real n / 8)"
"norm (y - z) < min (e / 2) (d / real n / 8)"
"label x i \<noteq> label y i"
@@ -3249,9 +3215,9 @@
then
obtain e where e:
"e > 0"
- "\<And>x y z i. x \<in> unit_cube \<Longrightarrow>
- y \<in> unit_cube \<Longrightarrow>
- z \<in> unit_cube \<Longrightarrow>
+ "\<And>x y z i. x \<in> cbox 0 One \<Longrightarrow>
+ y \<in> cbox 0 One \<Longrightarrow>
+ z \<in> cbox 0 One \<Longrightarrow>
i \<in> Basis \<Longrightarrow>
norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<Longrightarrow>
\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
@@ -3290,9 +3256,9 @@
using label(1)[OF b'']
by auto
{ fix x :: "nat \<Rightarrow> nat" and i assume "\<forall>i<n. x i \<le> p" "i < n" "x i = p \<or> x i = 0"
- then have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> (unit_cube::'a set)"
+ then have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> (cbox 0 One::'a set)"
using b'_Basis
- by (auto simp: mem_unit_cube inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1) }
+ by (auto simp: cbox_def inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1) }
note cube = this
have q2: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = 0 \<longrightarrow>
(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0)"
@@ -3314,8 +3280,8 @@
have "\<forall>i\<in>Basis. q (b' i) \<in> {0..p}"
using q(1) b'
by (auto intro: less_imp_le simp: bij_betw_def)
- then have "z \<in> unit_cube"
- unfolding z_def mem_unit_cube
+ then have "z \<in> cbox 0 One"
+ unfolding z_def cbox_def
using b'_Basis
by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1)
then have d_fz_z: "d \<le> norm (f z - z)"
@@ -3353,18 +3319,18 @@
using q(1)[rule_format,OF b'_im]
apply (auto simp: Suc_le_eq)
done
- then have "r' \<in> unit_cube"
- unfolding r'_def mem_unit_cube
+ then have "r' \<in> cbox 0 One"
+ unfolding r'_def cbox_def
using b'_Basis
by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1)
define s' :: 'a where "s' = (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i)"
have "\<And>i. i \<in> Basis \<Longrightarrow> s (b' i) \<le> p"
using b'_im q(1) rs(2) by fastforce
- then have "s' \<in> unit_cube"
- unfolding s'_def mem_unit_cube
+ then have "s' \<in> cbox 0 One"
+ unfolding s'_def cbox_def
using b'_Basis by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1)
- have "z \<in> unit_cube"
- unfolding z_def mem_unit_cube
+ have "z \<in> cbox 0 One"
+ unfolding z_def cbox_def
using b'_Basis q(1)[rule_format,OF b'_im] \<open>p > 0\<close>
by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le)
{
@@ -3394,7 +3360,7 @@
then have "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
using rs(3) i
unfolding r'_def[symmetric] s'_def[symmetric] o_def bb'
- by (intro e(2)[OF \<open>r'\<in>unit_cube\<close> \<open>s'\<in>unit_cube\<close> \<open>z\<in>unit_cube\<close>]) auto
+ by (intro e(2)[OF \<open>r'\<in>cbox 0 One\<close> \<open>s'\<in>cbox 0 One\<close> \<open>z\<in>cbox 0 One\<close>]) auto
then show False
using i by auto
qed
@@ -3410,7 +3376,7 @@
and "f ` S \<subseteq> S"
obtains x where "x \<in> S" and "f x = x"
proof -
- let ?U = "unit_cube :: 'a set"
+ let ?U = "cbox 0 One :: 'a set"
have "\<Sum>Basis /\<^sub>R 2 \<in> interior ?U"
proof (rule interiorI)
let ?I = "(\<Inter>i\<in>Basis. {x::'a. 0 < x \<bullet> i} \<inter> {x. x \<bullet> i < 1})"
@@ -3418,12 +3384,12 @@
by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less simp: continuous_on_inner continuous_on_const continuous_on_id)
show "\<Sum>Basis /\<^sub>R 2 \<in> ?I"
by simp
- show "?I \<subseteq> unit_cube"
- unfolding unit_cube_def by force
+ show "?I \<subseteq> cbox 0 One"
+ unfolding cbox_def by force
qed
then have *: "interior ?U \<noteq> {}" by fast
have *: "?U homeomorphic S"
- using homeomorphic_convex_compact[OF convex_unit_cube compact_unit_cube * assms(2,1,3)] .
+ using homeomorphic_convex_compact[OF convex_box(1) compact_cbox * assms(2,1,3)] .
have "\<forall>f. continuous_on ?U f \<and> f ` ?U \<subseteq> ?U \<longrightarrow>
(\<exists>x\<in>?U. f x = x)"
using brouwer_cube by auto
--- a/src/HOL/Analysis/Euclidean_Space.thy Fri Jul 13 17:18:07 2018 +0100
+++ b/src/HOL/Analysis/Euclidean_Space.thy Fri Jul 13 17:27:05 2018 +0100
@@ -341,6 +341,11 @@
intro!: finite_dimensional_vector_space.dimension_def
finite_dimensional_vector_space_euclidean)
+interpretation eucl?: finite_dimensional_vector_space_pair_1
+ "scaleR::real\<Rightarrow>'a::euclidean_space\<Rightarrow>'a" Basis
+ "scaleR::real\<Rightarrow>'b::real_vector \<Rightarrow> 'b"
+ by unfold_locales
+
interpretation eucl?: finite_dimensional_vector_space_prod scaleR scaleR Basis Basis
rewrites "Basis_pair = Basis"
and "module_prod.scale ( *\<^sub>R) ( *\<^sub>R) = (scaleR::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
--- a/src/HOL/Analysis/Inner_Product.thy Fri Jul 13 17:18:07 2018 +0100
+++ b/src/HOL/Analysis/Inner_Product.thy Fri Jul 13 17:27:05 2018 +0100
@@ -27,7 +27,7 @@
setup \<open>Sign.add_const_constraint
(@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
-class%important real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
+class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
assumes inner_commute: "inner x y = inner y x"
and inner_add_left: "inner (x + y) z = inner x z + inner y z"
--- a/src/HOL/Computational_Algebra/Primes.thy Fri Jul 13 17:18:07 2018 +0100
+++ b/src/HOL/Computational_Algebra/Primes.thy Fri Jul 13 17:27:05 2018 +0100
@@ -39,7 +39,7 @@
section \<open>Primes\<close>
theory Primes
-imports HOL.Binomial Euclidean_Algorithm
+imports Euclidean_Algorithm
begin
subsection \<open>Primes on @{typ nat} and @{typ int}\<close>
--- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy Fri Jul 13 17:18:07 2018 +0100
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy Fri Jul 13 17:27:05 2018 +0100
@@ -142,6 +142,14 @@
for S1:: "'b::ab_group_add set" and S2::"'c::ab_group_add set"
and scale1::"'a::field \<Rightarrow> _" and scale2::"'a \<Rightarrow> _"
+locale finite_dimensional_vector_space_pair_1_on =
+ vs1: finite_dimensional_vector_space_on S1 scale1 Basis1 +
+ vs2: vector_space_on S2 scale2
+ for S1 S2
+ and scale1::"'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b"
+ and scale2::"'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c"
+ and Basis1
+
locale finite_dimensional_vector_space_pair_on =
vs1: finite_dimensional_vector_space_on S1 scale1 Basis1 +
vs2: finite_dimensional_vector_space_on S2 scale2 Basis2
@@ -489,6 +497,24 @@
lt2.plus_S lt2.minus_S lt2.uminus_S (lt2.zero_S::'t) lt2.scale_S"
by (simp add: type_module_pair_on_with vector_space_pair_on_with_def)
+sublocale lt1: local_typedef_vector_space_on S1 scale1 s by unfold_locales
+sublocale lt2: local_typedef_vector_space_on S2 scale2 t by unfold_locales
+
+end
+
+locale local_typedef_finite_dimensional_vector_space_pair_1 =
+ lt1: local_typedef_finite_dimensional_vector_space_on S1 scale1 Basis1 s +
+ lt2: local_typedef_vector_space_on S2 scale2 t
+ for S1::"'b::ab_group_add set" and scale1::"'a::field \<Rightarrow> 'b \<Rightarrow> 'b" and Basis1 and s::"'s itself"
+ and S2::"'c::ab_group_add set" and scale2::"'a \<Rightarrow> 'c \<Rightarrow> 'c" and t::"'t itself"
+begin
+
+lemma type_finite_dimensional_vector_space_pair_1_on_with:
+ "finite_dimensional_vector_space_pair_1_on_with UNIV UNIV lt1.plus_S lt1.minus_S lt1.uminus_S (lt1.zero_S::'s) lt1.scale_S lt1.Basis_S
+ lt2.plus_S lt2.minus_S lt2.uminus_S (lt2.zero_S::'t) lt2.scale_S"
+ by (simp add: finite_dimensional_vector_space_pair_1_on_with_def
+ lt1.type_finite_dimensional_vector_space_on_with lt2.type_vector_space_on_with)
+
end
locale local_typedef_finite_dimensional_vector_space_pair =
@@ -507,6 +533,7 @@
end
+
subsection \<open>Transfer from type-based @{theory HOL.Modules} and @{theory HOL.Vector_Spaces}\<close>
context module_on begin
@@ -964,9 +991,12 @@
interpretation local_typedef_vector_space_pair S1 scale1 "TYPE('s)" S2 scale2 "TYPE('t)" by unfold_locales fact+
+
+
lemmas_with [var_simplified explicit_ab_group_add,
unoverload_type 'e 'b,
OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_vector_space_pair_on_with,
+ folded lt1.dim_S_def lt2.dim_S_def,
untransferred,
var_simplified implicit_ab_group_add]:
lt_linear_0 = vector_space_pair.linear_0
@@ -1007,6 +1037,7 @@
and lt_linear_injective_left_inverse = vector_space_pair.linear_injective_left_inverse
and lt_linear_surj_right_inverse = vector_space_pair.linear_surj_right_inverse
and lt_linear_surjective_right_inverse = vector_space_pair.linear_surjective_right_inverse
+and lt_finite_basis_to_basis_subspace_isomorphism = vector_space_pair.finite_basis_to_basis_subspace_isomorphism
(* should work, but doesnt
*)
(* not expected to work:
@@ -1067,9 +1098,42 @@
and linear_injective_left_inverse = lt_linear_injective_left_inverse
and linear_surj_right_inverse = lt_linear_surj_right_inverse
and linear_surjective_right_inverse = lt_linear_surjective_right_inverse
+ and finite_basis_to_basis_subspace_isomorphism = lt_finite_basis_to_basis_subspace_isomorphism
end
+context finite_dimensional_vector_space_pair_1_on begin
+
+context includes lifting_syntax
+ notes [transfer_rule del] = Collect_transfer
+ assumes
+ "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S1"
+ "\<exists>(Rep::'t \<Rightarrow> 'c) (Abs::'c \<Rightarrow> 't). type_definition Rep Abs S2" begin
+
+interpretation local_typedef_finite_dimensional_vector_space_pair_1 S1 scale1 Basis1 "TYPE('s)" S2 scale2 "TYPE('t)" by unfold_locales fact+
+
+lemmas_with [var_simplified explicit_ab_group_add,
+ unoverload_type 'e 'b,
+ OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_finite_dimensional_vector_space_pair_1_on_with,
+ folded lt1.dim_S_def lt2.dim_S_def,
+ untransferred,
+ var_simplified implicit_ab_group_add]:
+ lt_dim_image_eq = finite_dimensional_vector_space_pair_1.dim_image_eq
+and lt_dim_image_le = finite_dimensional_vector_space_pair_1.dim_image_le
+
+end
+
+lemmas_with [cancel_type_definition, OF vs1.S_ne,
+ cancel_type_definition, OF vs2.S_ne,
+ folded subset_iff' top_set_def,
+ simplified pred_fun_def,
+ simplified\<comment>\<open>too much?\<close>]:
+ dim_image_eq = lt_dim_image_eq
+and dim_image_le = lt_dim_image_le
+
+end
+
+
context finite_dimensional_vector_space_pair_on begin
context includes lifting_syntax
@@ -1090,9 +1154,7 @@
and lt_linear_injective_imp_surjective = finite_dimensional_vector_space_pair.linear_injective_imp_surjective
and lt_linear_injective_isomorphism = finite_dimensional_vector_space_pair.linear_injective_isomorphism
and lt_linear_surjective_isomorphism = finite_dimensional_vector_space_pair.linear_surjective_isomorphism
-and lt_dim_image_eq = finite_dimensional_vector_space_pair.dim_image_eq
and lt_basis_to_basis_subspace_isomorphism = finite_dimensional_vector_space_pair.basis_to_basis_subspace_isomorphism
-and lt_dim_image_le = finite_dimensional_vector_space_pair.dim_image_le
and lt_subspace_isomorphism = finite_dimensional_vector_space_pair.subspace_isomorphism
end
@@ -1106,9 +1168,7 @@
and linear_injective_imp_surjective = lt_linear_injective_imp_surjective
and linear_injective_isomorphism = lt_linear_injective_isomorphism
and linear_surjective_isomorphism = lt_linear_surjective_isomorphism
-and dim_image_eq = lt_dim_image_eq
and basis_to_basis_subspace_isomorphism = lt_basis_to_basis_subspace_isomorphism
-and dim_image_le = lt_dim_image_le
and subspace_isomorphism = lt_subspace_isomorphism
end
--- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy Fri Jul 13 17:18:07 2018 +0100
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy Fri Jul 13 17:27:05 2018 +0100
@@ -119,6 +119,11 @@
\<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>
@@ -239,6 +244,13 @@
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"
@@ -261,21 +273,24 @@
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]:
- "finite_dimensional_vector_space_on_with S (+) (-) uminus 0 s b"
+ "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
-
-lemma finite_dimensional_vector_space_pair_with_imp_vector_space_with[explicit_ab_group_add]:
- \<comment>\<open>this rule is strange: why is it needed, but not the one with \<open>module_with\<close> as conclusions?\<close>
- "vector_space_on_with S (+) (-) uminus 0 s"
- "vector_space_on_with T (+) (-) uminus 0 t"
- if "finite_dimensional_vector_space_pair_on_with S T (+) (-) uminus 0 s b (+) (-) uminus 0 t c"
- using that
- by (auto simp: finite_dimensional_vector_space_pair_on_with_def finite_dimensional_vector_space_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
--- a/src/HOL/Vector_Spaces.thy Fri Jul 13 17:18:07 2018 +0100
+++ b/src/HOL/Vector_Spaces.thy Fri Jul 13 17:27:05 2018 +0100
@@ -941,6 +941,56 @@
using linear_surj_right_inverse[of f UNIV UNIV]
by (auto simp: fun_eq_iff)
+lemma finite_basis_to_basis_subspace_isomorphism:
+ assumes s: "vs1.subspace S"
+ and t: "vs2.subspace T"
+ and d: "vs1.dim S = vs2.dim T"
+ and fB: "finite B"
+ and B: "B \<subseteq> S" "vs1.independent B" "S \<subseteq> vs1.span B" "card B = vs1.dim S"
+ and fC: "finite C"
+ and C: "C \<subseteq> T" "vs2.independent C" "T \<subseteq> vs2.span C" "card C = vs2.dim T"
+ shows "\<exists>f. linear s1 s2 f \<and> f ` B = C \<and> f ` S = T \<and> inj_on f S"
+proof -
+ from B(4) C(4) card_le_inj[of B C] d obtain f where
+ f: "f ` B \<subseteq> C" "inj_on f B" using \<open>finite B\<close> \<open>finite C\<close> by auto
+ from linear_independent_extend[OF B(2)] obtain g where
+ g: "linear s1 s2 g" "\<forall>x \<in> B. g x = f x" by blast
+ interpret g: linear s1 s2 g by fact
+ from inj_on_iff_eq_card[OF fB, of f] f(2)
+ have "card (f ` B) = card B" by simp
+ with B(4) C(4) have ceq: "card (f ` B) = card C" using d
+ by simp
+ have "g ` B = f ` B" using g(2)
+ by (auto simp add: image_iff)
+ also have "\<dots> = C" using card_subset_eq[OF fC f(1) ceq] .
+ finally have gBC: "g ` B = C" .
+ have gi: "inj_on g B" using f(2) g(2)
+ by (auto simp add: inj_on_def)
+ note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi]
+ {
+ fix x y
+ assume x: "x \<in> S" and y: "y \<in> S" and gxy: "g x = g y"
+ from B(3) x y have x': "x \<in> vs1.span B" and y': "y \<in> vs1.span B"
+ by blast+
+ from gxy have th0: "g (x - y) = 0"
+ by (simp add: g.diff)
+ have th1: "x - y \<in> vs1.span B" using x' y'
+ by (metis vs1.span_diff)
+ have "x = y" using g0[OF th1 th0] by simp
+ }
+ then have giS: "inj_on g S" unfolding inj_on_def by blast
+ from vs1.span_subspace[OF B(1,3) s]
+ have "g ` S = vs2.span (g ` B)"
+ by (simp add: g.span_image)
+ also have "\<dots> = vs2.span C"
+ unfolding gBC ..
+ also have "\<dots> = T"
+ using vs2.span_subspace[OF C(1,3) t] .
+ finally have gS: "g ` S = T" .
+ from g(1) gS giS gBC show ?thesis
+ by blast
+qed
+
end
lemma surjective_iff_injective_gen:
@@ -1347,6 +1397,54 @@
end
+locale finite_dimensional_vector_space_pair_1 =
+ vs1: finite_dimensional_vector_space s1 B1 + vs2: vector_space s2
+ for s1 :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*a" 75)
+ and B1 :: "'b set"
+ and s2 :: "'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr "*b" 75)
+begin
+
+sublocale vector_space_pair s1 s2 by unfold_locales
+
+lemma dim_image_eq:
+ assumes lf: "linear s1 s2 f"
+ and fi: "inj_on f (vs1.span S)"
+ shows "vs2.dim (f ` S) = vs1.dim S"
+proof -
+ interpret lf: linear by fact
+ obtain B where B: "B \<subseteq> S" "vs1.independent B" "S \<subseteq> vs1.span B" "card B = vs1.dim S"
+ using vs1.basis_exists[of S] by auto
+ then have "vs1.span S = vs1.span B"
+ using vs1.span_mono[of B S] vs1.span_mono[of S "vs1.span B"] vs1.span_span[of B] by auto
+ moreover have "card (f ` B) = card B"
+ using assms card_image[of f B] subset_inj_on[of f "vs1.span S" B] B vs1.span_superset by auto
+ moreover have "(f ` B) \<subseteq> (f ` S)"
+ using B by auto
+ ultimately show ?thesis
+ by (metis B(2) B(4) fi lf.dependent_inj_imageD lf.span_image vs2.dim_eq_card_independent vs2.dim_span)
+qed
+
+lemma dim_image_le:
+ assumes lf: "linear s1 s2 f"
+ shows "vs2.dim (f ` S) \<le> vs1.dim (S)"
+proof -
+ from vs1.basis_exists[of S] obtain B where
+ B: "B \<subseteq> S" "vs1.independent B" "S \<subseteq> vs1.span B" "card B = vs1.dim S" by blast
+ from B have fB: "finite B" "card B = vs1.dim S"
+ using vs1.independent_bound_general by blast+
+ have "vs2.dim (f ` S) \<le> card (f ` B)"
+ apply (rule vs2.span_card_ge_dim)
+ using lf B fB
+ apply (auto simp add: module_hom.span_image module_hom.spans_image subset_image_iff
+ linear_iff_module_hom)
+ done
+ also have "\<dots> \<le> vs1.dim S"
+ using card_image_le[OF fB(1)] fB by simp
+ finally show ?thesis .
+qed
+
+end
+
locale finite_dimensional_vector_space_pair =
vs1: finite_dimensional_vector_space s1 B1 + vs2: finite_dimensional_vector_space s2 B2
for s1 :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*a" 75)
@@ -1355,7 +1453,7 @@
and B2 :: "'c set"
begin
-sublocale vector_space_pair s1 s2 by unfold_locales
+sublocale finite_dimensional_vector_space_pair_1 ..
lemma linear_surjective_imp_injective:
assumes lf: "linear s1 s2 f" and sf: "surj f" and eq: "vs2.dim UNIV = vs1.dim UNIV"
@@ -1432,24 +1530,6 @@
linear_exists_left_inverse_on[OF lf vs1.subspace_UNIV]
dims lf linear_injective_isomorphism by auto
-lemma dim_image_eq:
- assumes lf: "linear s1 s2 f"
- and fi: "inj_on f (vs1.span S)"
- shows "vs2.dim (f ` S) = vs1.dim S"
-proof -
- interpret lf: linear by fact
- obtain B where B: "B \<subseteq> S" "vs1.independent B" "S \<subseteq> vs1.span B" "card B = vs1.dim S"
- using vs1.basis_exists[of S] by auto
- then have "vs1.span S = vs1.span B"
- using vs1.span_mono[of B S] vs1.span_mono[of S "vs1.span B"] vs1.span_span[of B] by auto
- moreover have "card (f ` B) = card B"
- using assms card_image[of f B] subset_inj_on[of f "vs1.span S" B] B vs1.span_superset by auto
- moreover have "(f ` B) \<subseteq> (f ` S)"
- using B by auto
- ultimately show ?thesis
- by (metis B(2) B(4) fi lf.dependent_inj_imageD lf.span_image vs2.dim_eq_card_independent vs2.dim_span)
-qed
-
lemma basis_to_basis_subspace_isomorphism:
assumes s: "vs1.subspace S"
and t: "vs2.subspace T"
@@ -1462,63 +1542,7 @@
by (simp add: vs1.finiteI_independent)
from C have fC: "finite C"
by (simp add: vs2.finiteI_independent)
- from B(4) C(4) card_le_inj[of B C] d obtain f where
- f: "f ` B \<subseteq> C" "inj_on f B" using \<open>finite B\<close> \<open>finite C\<close> by auto
- from linear_independent_extend[OF B(2)] obtain g where
- g: "linear s1 s2 g" "\<forall>x \<in> B. g x = f x" by blast
- interpret g: linear s1 s2 g by fact
- from inj_on_iff_eq_card[OF fB, of f] f(2)
- have "card (f ` B) = card B" by simp
- with B(4) C(4) have ceq: "card (f ` B) = card C" using d
- by simp
- have "g ` B = f ` B" using g(2)
- by (auto simp add: image_iff)
- also have "\<dots> = C" using card_subset_eq[OF fC f(1) ceq] .
- finally have gBC: "g ` B = C" .
- have gi: "inj_on g B" using f(2) g(2)
- by (auto simp add: inj_on_def)
- note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi]
- {
- fix x y
- assume x: "x \<in> S" and y: "y \<in> S" and gxy: "g x = g y"
- from B(3) x y have x': "x \<in> vs1.span B" and y': "y \<in> vs1.span B"
- by blast+
- from gxy have th0: "g (x - y) = 0"
- by (simp add: g.diff)
- have th1: "x - y \<in> vs1.span B" using x' y'
- by (metis vs1.span_diff)
- have "x = y" using g0[OF th1 th0] by simp
- }
- then have giS: "inj_on g S" unfolding inj_on_def by blast
- from vs1.span_subspace[OF B(1,3) s]
- have "g ` S = vs2.span (g ` B)"
- by (simp add: g.span_image)
- also have "\<dots> = vs2.span C"
- unfolding gBC ..
- also have "\<dots> = T"
- using vs2.span_subspace[OF C(1,3) t] .
- finally have gS: "g ` S = T" .
- from g(1) gS giS gBC show ?thesis
- by blast
-qed
-
-lemma dim_image_le:
- assumes lf: "linear s1 s2 f"
- shows "vs2.dim (f ` S) \<le> vs1.dim (S)"
-proof -
- from vs1.basis_exists[of S] obtain B where
- B: "B \<subseteq> S" "vs1.independent B" "S \<subseteq> vs1.span B" "card B = vs1.dim S" by blast
- from B have fB: "finite B" "card B = vs1.dim S"
- using vs1.independent_bound_general by blast+
- have "vs2.dim (f ` S) \<le> card (f ` B)"
- apply (rule vs2.span_card_ge_dim)
- using lf B fB
- apply (auto simp add: module_hom.span_image module_hom.spans_image subset_image_iff
- linear_iff_module_hom)
- done
- also have "\<dots> \<le> vs1.dim S"
- using card_image_le[OF fB(1)] fB by simp
- finally show ?thesis .
+ from finite_basis_to_basis_subspace_isomorphism[OF s t d fB B fC C] show ?thesis .
qed
end