[isabelle] Weak lemmas in HOL-Analysis.Affine



Dear Isabelle maintainers,

(which mailinglist should this go on? I'm not sure)

I have encountered some weak theorems in HOL-Analysis.Affine, where a
type is constrained to an euclidean space while any real vector space
suffices. Please consider the following diff.

Regards,
Jakub Kądziołka

@@ -1008,7 +1008,7 @@
   using affine_hull_span_gen[of "0" S] assms by auto

 lemma extend_to_affine_basis_nonempty:
-  fixes S V :: "'n::euclidean_space set"
+  fixes S V :: "'n::real_vector set"
   assumes "\<not> affine_dependent S" "S \<subseteq> V" "S \<noteq> {}"
   shows "\<exists>T. \<not> affine_dependent T \<and> S \<subseteq> T \<and> T \<subseteq> V \<and> affine hull T = affine hull V"
 proof -
@@ -1044,7 +1044,7 @@
 qed

 lemma affine_basis_exists:
-  fixes V :: "'n::euclidean_space set"
+  fixes V :: "'n::real_vector set"
   shows "\<exists>B. B \<subseteq> V \<and> \<not> affine_dependent B \<and> affine hull V = affine hull B"
 proof (cases "V = {}")
   case True
@@ -1059,7 +1059,7 @@
 qed

 proposition extend_to_affine_basis:
-  fixes S V :: "'n::euclidean_space set"
+  fixes S V :: "'n::real_vector set"
   assumes "\<not> affine_dependent S" "S \<subseteq> V"
   obtains T where "\<not> affine_dependent T" "S \<subseteq> T" "T \<subseteq> V" "affine hull T = affine hull V"
 proof (cases "S = {}")
@@ -1073,13 +1073,13 @@

 subsection \<open>Affine Dimension of a Set\<close>

-definition\<^marker>\<open>tag important\<close> aff_dim :: "('a::euclidean_space) set \<Rightarrow> int"
+definition\<^marker>\<open>tag important\<close> aff_dim :: "('a::real_vector) set \<Rightarrow> int"
   where "aff_dim V =
   (SOME d :: int.
     \<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = d + 1)"

 lemma aff_dim_basis_exists:
-  fixes V :: "('n::euclidean_space) set"
+  fixes V :: "('n::real_vector) set"
   shows "\<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = aff_dim V + 1"
 proof -
   obtain B where "\<not> affine_dependent B \<and> affine hull B = affine hull V"




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.