# HG changeset patch # User immler # Date 1531476866 -7200 # Node ID 707437105595e41af2a4b535bcb5ae3aba7703eb # Parent 79abf4201e8dd94448eb73644dae0cc000f8a9f8 relaxed assumptions for dim_image_eq and dim_image_le diff -r 79abf4201e8d -r 707437105595 src/HOL/Analysis/Euclidean_Space.thy --- a/src/HOL/Analysis/Euclidean_Space.thy Thu Jul 12 17:23:38 2018 +0100 +++ b/src/HOL/Analysis/Euclidean_Space.thy Fri Jul 13 12:14:26 2018 +0200 @@ -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\'a::euclidean_space\'a" Basis + "scaleR::real\'b::real_vector \ '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::_\_\('a \ 'b))" diff -r 79abf4201e8d -r 707437105595 src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy --- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy Thu Jul 12 17:23:38 2018 +0100 +++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy Fri Jul 13 12:14:26 2018 +0200 @@ -142,6 +142,14 @@ for S1:: "'b::ab_group_add set" and S2::"'c::ab_group_add set" and scale1::"'a::field \ _" and scale2::"'a \ _" +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 \ 'b::ab_group_add \ 'b" + and scale2::"'a::field \ 'c::ab_group_add \ '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 \ 'b \ 'b" and Basis1 and s::"'s itself" + and S2::"'c::ab_group_add set" and scale2::"'a \ 'c \ '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 \Transfer from type-based @{theory HOL.Modules} and @{theory HOL.Vector_Spaces}\ 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 + "\(Rep::'s \ 'b) (Abs::'b \ 's). type_definition Rep Abs S1" + "\(Rep::'t \ 'c) (Abs::'c \ '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\\too much?\]: + 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 diff -r 79abf4201e8d -r 707437105595 src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy --- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy Thu Jul 12 17:23:38 2018 +0100 +++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy Fri Jul 13 12:14:26 2018 +0200 @@ -119,6 +119,11 @@ \ 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 \ @@ -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 \ + 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 \ 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]: - \\this rule is strange: why is it needed, but not the one with \module_with\ as conclusions?\ - "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 diff -r 79abf4201e8d -r 707437105595 src/HOL/Vector_Spaces.thy --- a/src/HOL/Vector_Spaces.thy Thu Jul 12 17:23:38 2018 +0100 +++ b/src/HOL/Vector_Spaces.thy Fri Jul 13 12:14:26 2018 +0200 @@ -954,6 +954,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 \ S" "vs1.independent B" "S \ vs1.span B" "card B = vs1.dim S" + and fC: "finite C" + and C: "C \ T" "vs2.independent C" "T \ vs2.span C" "card C = vs2.dim T" + shows "\f. linear s1 s2 f \ f ` B = C \ f ` S = T \ inj_on f S" +proof - + from B(4) C(4) card_le_inj[of B C] d obtain f where + f: "f ` B \ C" "inj_on f B" using \finite B\ \finite C\ by auto + from linear_independent_extend[OF B(2)] obtain g where + g: "linear s1 s2 g" "\x \ 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 "\ = 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 \ S" and y: "y \ S" and gxy: "g x = g y" + from B(3) x y have x': "x \ vs1.span B" and y': "y \ vs1.span B" + by blast+ + from gxy have th0: "g (x - y) = 0" + by (simp add: g.diff) + have th1: "x - y \ 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 "\ = vs2.span C" + unfolding gBC .. + also have "\ = 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: @@ -1366,6 +1416,54 @@ end +locale finite_dimensional_vector_space_pair_1 = + vs1: finite_dimensional_vector_space s1 B1 + vs2: vector_space s2 + for s1 :: "'a::field \ 'b::ab_group_add \ 'b" (infixr "*a" 75) + and B1 :: "'b set" + and s2 :: "'a::field \ 'c::ab_group_add \ '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 \ S" "vs1.independent B" "S \ 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) \ (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) \ vs1.dim (S)" +proof - + from vs1.basis_exists[of S] obtain B where + B: "B \ S" "vs1.independent B" "S \ 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) \ 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 "\ \ 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 \ 'b::ab_group_add \ 'b" (infixr "*a" 75) @@ -1374,7 +1472,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" @@ -1470,24 +1568,6 @@ done qed -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 \ S" "vs1.independent B" "S \ 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) \ (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" @@ -1500,63 +1580,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 \ C" "inj_on f B" using \finite B\ \finite C\ by auto - from linear_independent_extend[OF B(2)] obtain g where - g: "linear s1 s2 g" "\x \ 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 "\ = 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 \ S" and y: "y \ S" and gxy: "g x = g y" - from B(3) x y have x': "x \ vs1.span B" and y': "y \ vs1.span B" - by blast+ - from gxy have th0: "g (x - y) = 0" - by (simp add: g.diff) - have th1: "x - y \ 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 "\ = vs2.span C" - unfolding gBC .. - also have "\ = 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) \ vs1.dim (S)" -proof - - from vs1.basis_exists[of S] obtain B where - B: "B \ S" "vs1.independent B" "S \ 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) \ 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 "\ \ 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