author immler Fri, 13 Jul 2018 12:14:26 +0200 changeset 68620 707437105595 parent 68619 79abf4201e8d child 68622 0987ae51a3be
relaxed assumptions for dim_image_eq and dim_image_le
```--- 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\<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/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 @@
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"

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

+
+
+  folded lt1.dim_S_def lt2.dim_S_def,
untransferred,
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+
+
+  folded lt1.dim_S_def lt2.dim_S_def,
+  untransferred,
+   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	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 @@
\<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 @@
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 \<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)
+
"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)

+  "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
+
-  "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
-
-  \<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)

lemma finite_dimensional_vector_space_on_with_transfer[transfer_rule]:
includes lifting_syntax```
```--- 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 \<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"
+    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)"
+  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:
@@ -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 \<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)
@@ -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 \<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"
@@ -1500,63 +1580,7 @@
from C have fC: "finite C"
-  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"
-    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)"
-  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```