# HG changeset patch
# User himmelma
# Date 1262779650 -3600
# Node ID c9c14c72d035bb4e17f176b27d0b97e3ad36bd7a
# Parent  cf455b5880e15f1e4292f170b22fe98b1c2eb562
Made finite cartesian products finite

diff -r cf455b5880e1 -r c9c14c72d035 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Jan 07 12:24:35 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Jan 06 13:07:30 2010 +0100
@@ -34,7 +34,7 @@
   thus ?thesis apply(rule that) using x(2) unfolding o_def by auto qed(rule that[of 1], auto)
 
 lemma kuhn_labelling_lemma:
-  assumes "(\<forall>x::real^'n. P x \<longrightarrow> P (f x))"  "\<forall>x. P x \<longrightarrow> (\<forall>i::'n. Q i \<longrightarrow> 0 \<le> x$i \<and> x$i \<le> 1)"
+  assumes "(\<forall>x::real^_. P x \<longrightarrow> P (f x))"  "\<forall>x. P x \<longrightarrow> (\<forall>i. Q i \<longrightarrow> 0 \<le> x$i \<and> x$i \<le> 1)"
   shows "\<exists>l. (\<forall>x i. l x i \<le> (1::nat)) \<and>
              (\<forall>x i. P x \<and> Q i \<and> (x$i = 0) \<longrightarrow> (l x i = 0)) \<and>
              (\<forall>x i. P x \<and> Q i \<and> (x$i = 1) \<longrightarrow> (l x i = 1)) \<and>
diff -r cf455b5880e1 -r c9c14c72d035 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Jan 07 12:24:35 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Jan 06 13:07:30 2010 +0100
@@ -19,8 +19,6 @@
 declare dot_lmult[simp] dot_rmult[simp] dot_lneg[simp] dot_rneg[simp]
 declare UNIV_1[simp]
 
-term "(x::real^'n \<Rightarrow> real) 0"
-
 lemma dim1in[intro]:"Suc 0 \<in> {1::nat .. CARD(1)}" by auto
 
 lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_le_def Cart_lambda_beta dest_vec1_def basis_component vector_uminus_component
@@ -1053,7 +1051,7 @@
 proof-
   have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto
   have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z"
-         "\<And>x y z ::real^'n. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by (auto simp add: ring_simps)
+         "\<And>x y z ::real^_. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by (auto simp add: ring_simps)
   show ?thesis unfolding convex_hull_finite[OF fin(1)] and Collect_def and convex_hull_finite_step[OF fin(2)] and *
     unfolding convex_hull_finite_step[OF fin(3)] apply(rule ext) apply simp apply auto
     apply(rule_tac x=va in exI) apply (rule_tac x="u c" in exI) apply simp
@@ -1903,7 +1901,7 @@
     using assms(2) by assumption qed
 
 lemma radon_v_lemma:
-  assumes "finite s" "setsum f s = 0" "\<forall>x. g x = (0::real) \<longrightarrow> f x = (0::real^'n)"
+  assumes "finite s" "setsum f s = 0" "\<forall>x. g x = (0::real) \<longrightarrow> f x = (0::real^_)"
   shows "(setsum f {x\<in>s. 0 < g x}) = - setsum f {x\<in>s. g x < 0}"
 proof-
   have *:"\<And>x. (if 0 < g x then f x else 0) + (if g x < 0 then f x else 0) = f x" using assms(3) by auto 
@@ -2245,7 +2243,7 @@
 
 subsection {* Epigraphs of convex functions. *}
 
-definition "epigraph s (f::real^'n \<Rightarrow> real) = {xy. fstcart xy \<in> s \<and> f(fstcart xy) \<le> dest_vec1 (sndcart xy)}"
+definition "epigraph s (f::real^'n::finite \<Rightarrow> real) = {xy. fstcart xy \<in> s \<and> f(fstcart xy) \<le> dest_vec1 (sndcart xy)}"
 
 lemma mem_epigraph: "(pastecart x (vec1 y)) \<in> epigraph s f \<longleftrightarrow> x \<in> s \<and> f x \<le> y" unfolding epigraph_def by auto
 
diff -r cf455b5880e1 -r c9c14c72d035 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Jan 07 12:24:35 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Jan 06 13:07:30 2010 +0100
@@ -205,7 +205,7 @@
     apply(subst vector_smult_lzero[THEN sym, of v]) unfolding scaleR_scaleR smult_conv_scaleR apply(rule Lim_vmul)
     using assms[unfolded has_derivative_def] unfolding Lim o_def apply- apply(cases "trivial_limit net")
     apply(rule,assumption,rule disjI2,rule,rule) proof-
-    have *:"\<And>x. x - vec 0 = (x::real^'n)" by auto 
+    have *:"\<And>x. x - vec 0 = (x::real^'n::finite)" by auto 
     have **:"\<And>d x. d * (c x $ k - (c (netlimit net) $ k + c' (x - netlimit net) $ k)) = (d *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net) ))) $k" by(auto simp add:field_simps)
     fix e assume "\<not> trivial_limit net" "0 < (e::real)"
     then have "eventually (\<lambda>x. dist ((1 / norm (x - netlimit net)) *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net)))) 0 < e) net"
diff -r cf455b5880e1 -r c9c14c72d035 src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Thu Jan 07 12:24:35 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Wed Jan 06 13:07:30 2010 +0100
@@ -67,22 +67,22 @@
 
 subsection{* Trace *}
 
-definition trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a" where
+definition trace :: "'a::semiring_1^'n^'n::finite \<Rightarrow> 'a" where
   "trace A = setsum (\<lambda>i. ((A$i)$i)) (UNIV::'n set)"
 
 lemma trace_0: "trace(mat 0) = 0"
   by (simp add: trace_def mat_def)
 
-lemma trace_I: "trace(mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))"
+lemma trace_I: "trace(mat 1 :: 'a::semiring_1^'n^'n::finite) = of_nat(CARD('n))"
   by (simp add: trace_def mat_def)
 
-lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B"
+lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n::finite) + B) = trace A + trace B"
   by (simp add: trace_def setsum_addf)
 
-lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B"
+lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n::finite) - B) = trace A - trace B"
   by (simp add: trace_def setsum_subtractf)
 
-lemma trace_mul_sym:"trace ((A::'a::comm_semiring_1^'n^'n) ** B) = trace (B**A)"
+lemma trace_mul_sym:"trace ((A::'a::comm_semiring_1^'n^'n::finite) ** B) = trace (B**A)"
   apply (simp add: trace_def matrix_matrix_mult_def)
   apply (subst setsum_commute)
   by (simp add: mult_commute)
@@ -91,7 +91,7 @@
 (* Definition of determinant.                                                *)
 (* ------------------------------------------------------------------------- *)
 
-definition det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where
+definition det:: "'a::comm_ring_1^'n^'n::finite \<Rightarrow> 'a" where
   "det A = setsum (\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)) {p. p permutes (UNIV :: 'n set)}"
 
 (* ------------------------------------------------------------------------- *)
@@ -495,7 +495,7 @@
 (* Multilinearity and the multiplication formula.                            *)
 (* ------------------------------------------------------------------------- *)
 
-lemma Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (Cart_lambda f::'a^'n) = (Cart_lambda g :: 'a^'n)"
+lemma Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (Cart_lambda f::'a^'n) = (Cart_lambda g :: 'a^'n::finite)"
   apply (rule iffD1[OF Cart_lambda_unique]) by vector
 
 lemma det_linear_row_setsum:
@@ -840,7 +840,7 @@
   apply (simp add: real_vector_norm_def)
   by (simp add: dot_norm  linear_add[symmetric])
 
-definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow> transp Q ** Q = mat 1 \<and> Q ** transp Q = mat 1"
+definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n::finite) \<longleftrightarrow> transp Q ** Q = mat 1 \<and> Q ** transp Q = mat 1"
 
 lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n::finite)  \<longleftrightarrow> transp Q ** Q = mat 1"
   by (metis matrix_left_right_inverse orthogonal_matrix_def)
diff -r cf455b5880e1 -r c9c14c72d035 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Jan 07 12:24:35 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Jan 06 13:07:30 2010 +0100
@@ -61,38 +61,38 @@
 
 subsection{* Basic componentwise operations on vectors. *}
 
-instantiation "^" :: (plus,type) plus
+instantiation "^" :: (plus,finite) plus
 begin
 definition  vector_add_def : "op + \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) + (y$i)))"
 instance ..
 end
 
-instantiation "^" :: (times,type) times
+instantiation "^" :: (times,finite) times
 begin
   definition vector_mult_def : "op * \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) * (y$i)))"
   instance ..
 end
 
-instantiation "^" :: (minus,type) minus begin
+instantiation "^" :: (minus,finite) minus begin
   definition vector_minus_def : "op - \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) - (y$i)))"
 instance ..
 end
 
-instantiation "^" :: (uminus,type) uminus begin
+instantiation "^" :: (uminus,finite) uminus begin
   definition vector_uminus_def : "uminus \<equiv> (\<lambda> x.  (\<chi> i. - (x$i)))"
 instance ..
 end
-instantiation "^" :: (zero,type) zero begin
+instantiation "^" :: (zero,finite) zero begin
   definition vector_zero_def : "0 \<equiv> (\<chi> i. 0)"
 instance ..
 end
 
-instantiation "^" :: (one,type) one begin
+instantiation "^" :: (one,finite) one begin
   definition vector_one_def : "1 \<equiv> (\<chi> i. 1)"
 instance ..
 end
 
-instantiation "^" :: (ord,type) ord
+instantiation "^" :: (ord,finite) ord
  begin
 definition vector_le_def:
   "less_eq (x :: 'a ^'b) y = (ALL i. x$i <= y$i)"
@@ -101,7 +101,7 @@
 instance by (intro_classes)
 end
 
-instantiation "^" :: (scaleR, type) scaleR
+instantiation "^" :: (scaleR, finite) scaleR
 begin
 definition vector_scaleR_def: "scaleR = (\<lambda> r x.  (\<chi> i. scaleR r (x$i)))"
 instance ..
@@ -109,7 +109,7 @@
 
 text{* Also the scalar-vector multiplication. *}
 
-definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
+definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n::finite \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
   where "c *s x = (\<chi> i. c * (x$i))"
 
 text{* Constant Vectors *} 
@@ -118,7 +118,7 @@
 
 text{* Dot products. *}
 
-definition dot :: "'a::{comm_monoid_add, times} ^ 'n \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" (infix "\<bullet>" 70) where
+definition dot :: "'a::{comm_monoid_add, times} ^ 'n::finite \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" (infix "\<bullet>" 70) where
   "x \<bullet> y = setsum (\<lambda>i. x$i * y$i) UNIV"
 
 lemma dot_1[simp]: "(x::'a::{comm_monoid_add, times}^1) \<bullet> y = (x$1) * (y$1)"
@@ -162,36 +162,36 @@
 
 text{* Obvious "component-pushing". *}
 
-lemma vec_component [simp]: "(vec x :: 'a ^ 'n)$i = x"
+lemma vec_component [simp]: "(vec x :: 'a ^ 'n::finite)$i = x"
   by (vector vec_def)
 
 lemma vector_add_component [simp]:
-  fixes x y :: "'a::{plus} ^ 'n"
+  fixes x y :: "'a::{plus} ^ 'n::finite"
   shows "(x + y)$i = x$i + y$i"
   by vector
 
 lemma vector_minus_component [simp]:
-  fixes x y :: "'a::{minus} ^ 'n"
+  fixes x y :: "'a::{minus} ^ 'n::finite"
   shows "(x - y)$i = x$i - y$i"
   by vector
 
 lemma vector_mult_component [simp]:
-  fixes x y :: "'a::{times} ^ 'n"
+  fixes x y :: "'a::{times} ^ 'n::finite"
   shows "(x * y)$i = x$i * y$i"
   by vector
 
 lemma vector_smult_component [simp]:
-  fixes y :: "'a::{times} ^ 'n"
+  fixes y :: "'a::{times} ^ 'n::finite"
   shows "(c *s y)$i = c * (y$i)"
   by vector
 
 lemma vector_uminus_component [simp]:
-  fixes x :: "'a::{uminus} ^ 'n"
+  fixes x :: "'a::{uminus} ^ 'n::finite"
   shows "(- x)$i = - (x$i)"
   by vector
 
 lemma vector_scaleR_component [simp]:
-  fixes x :: "'a::scaleR ^ 'n"
+  fixes x :: "'a::scaleR ^ 'n::finite"
   shows "(scaleR r x)$i = scaleR r (x$i)"
   by vector
 
@@ -204,95 +204,95 @@
 
 subsection {* Some frequently useful arithmetic lemmas over vectors. *}
 
-instance "^" :: (semigroup_add,type) semigroup_add
+instance "^" :: (semigroup_add,finite) semigroup_add
   apply (intro_classes) by (vector add_assoc)
 
 
-instance "^" :: (monoid_add,type) monoid_add
+instance "^" :: (monoid_add,finite) monoid_add
   apply (intro_classes) by vector+
 
-instance "^" :: (group_add,type) group_add
+instance "^" :: (group_add,finite) group_add
   apply (intro_classes) by (vector algebra_simps)+
 
-instance "^" :: (ab_semigroup_add,type) ab_semigroup_add
+instance "^" :: (ab_semigroup_add,finite) ab_semigroup_add
   apply (intro_classes) by (vector add_commute)
 
-instance "^" :: (comm_monoid_add,type) comm_monoid_add
+instance "^" :: (comm_monoid_add,finite) comm_monoid_add
   apply (intro_classes) by vector
 
-instance "^" :: (ab_group_add,type) ab_group_add
+instance "^" :: (ab_group_add,finite) ab_group_add
   apply (intro_classes) by vector+
 
-instance "^" :: (cancel_semigroup_add,type) cancel_semigroup_add
+instance "^" :: (cancel_semigroup_add,finite) cancel_semigroup_add
   apply (intro_classes)
   by (vector Cart_eq)+
 
-instance "^" :: (cancel_ab_semigroup_add,type) cancel_ab_semigroup_add
+instance "^" :: (cancel_ab_semigroup_add,finite) cancel_ab_semigroup_add
   apply (intro_classes)
   by (vector Cart_eq)
 
-instance "^" :: (real_vector, type) real_vector
+instance "^" :: (real_vector, finite) real_vector
   by default (vector scaleR_left_distrib scaleR_right_distrib)+
 
-instance "^" :: (semigroup_mult,type) semigroup_mult
+instance "^" :: (semigroup_mult,finite) semigroup_mult
   apply (intro_classes) by (vector mult_assoc)
 
-instance "^" :: (monoid_mult,type) monoid_mult
+instance "^" :: (monoid_mult,finite) monoid_mult
   apply (intro_classes) by vector+
 
-instance "^" :: (ab_semigroup_mult,type) ab_semigroup_mult
+instance "^" :: (ab_semigroup_mult,finite) ab_semigroup_mult
   apply (intro_classes) by (vector mult_commute)
 
-instance "^" :: (ab_semigroup_idem_mult,type) ab_semigroup_idem_mult
+instance "^" :: (ab_semigroup_idem_mult,finite) ab_semigroup_idem_mult
   apply (intro_classes) by (vector mult_idem)
 
-instance "^" :: (comm_monoid_mult,type) comm_monoid_mult
+instance "^" :: (comm_monoid_mult,finite) comm_monoid_mult
   apply (intro_classes) by vector
 
-fun vector_power :: "('a::{one,times} ^'n) \<Rightarrow> nat \<Rightarrow> 'a^'n" where
+fun vector_power :: "('a::{one,times} ^'n::finite) \<Rightarrow> nat \<Rightarrow> 'a^'n" where
   "vector_power x 0 = 1"
   | "vector_power x (Suc n) = x * vector_power x n"
 
-instance "^" :: (semiring,type) semiring
+instance "^" :: (semiring,finite) semiring
   apply (intro_classes) by (vector ring_simps)+
 
-instance "^" :: (semiring_0,type) semiring_0
+instance "^" :: (semiring_0,finite) semiring_0
   apply (intro_classes) by (vector ring_simps)+
-instance "^" :: (semiring_1,type) semiring_1
+instance "^" :: (semiring_1,finite) semiring_1
   apply (intro_classes) by vector
-instance "^" :: (comm_semiring,type) comm_semiring
+instance "^" :: (comm_semiring,finite) comm_semiring
   apply (intro_classes) by (vector ring_simps)+
 
-instance "^" :: (comm_semiring_0,type) comm_semiring_0 by (intro_classes)
-instance "^" :: (cancel_comm_monoid_add, type) cancel_comm_monoid_add ..
-instance "^" :: (semiring_0_cancel,type) semiring_0_cancel by (intro_classes)
-instance "^" :: (comm_semiring_0_cancel,type) comm_semiring_0_cancel by (intro_classes)
-instance "^" :: (ring,type) ring by (intro_classes)
-instance "^" :: (semiring_1_cancel,type) semiring_1_cancel by (intro_classes)
-instance "^" :: (comm_semiring_1,type) comm_semiring_1 by (intro_classes)
-
-instance "^" :: (ring_1,type) ring_1 ..
-
-instance "^" :: (real_algebra,type) real_algebra
+instance "^" :: (comm_semiring_0,finite) comm_semiring_0 by (intro_classes)
+instance "^" :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
+instance "^" :: (semiring_0_cancel,finite) semiring_0_cancel by (intro_classes)
+instance "^" :: (comm_semiring_0_cancel,finite) comm_semiring_0_cancel by (intro_classes)
+instance "^" :: (ring,finite) ring by (intro_classes)
+instance "^" :: (semiring_1_cancel,finite) semiring_1_cancel by (intro_classes)
+instance "^" :: (comm_semiring_1,finite) comm_semiring_1 by (intro_classes)
+
+instance "^" :: (ring_1,finite) ring_1 ..
+
+instance "^" :: (real_algebra,finite) real_algebra
   apply intro_classes
   apply (simp_all add: vector_scaleR_def ring_simps)
   apply vector
   apply vector
   done
 
-instance "^" :: (real_algebra_1,type) real_algebra_1 ..
+instance "^" :: (real_algebra_1,finite) real_algebra_1 ..
 
 lemma of_nat_index:
-  "(of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n"
+  "(of_nat n :: 'a::semiring_1 ^'n::finite)$i = of_nat n"
   apply (induct n)
   apply vector
   apply vector
   done
 lemma zero_index[simp]:
-  "(0 :: 'a::zero ^'n)$i = 0" by vector
+  "(0 :: 'a::zero ^'n::finite)$i = 0" by vector
 
 lemma one_index[simp]:
-  "(1 :: 'a::one ^'n)$i = 1" by vector
+  "(1 :: 'a::one ^'n::finite)$i = 1" by vector
 
 lemma one_plus_of_nat_neq_0: "(1::'a::semiring_char_0) + of_nat n \<noteq> 0"
 proof-
@@ -301,15 +301,15 @@
   finally show ?thesis by simp
 qed
 
-instance "^" :: (semiring_char_0,type) semiring_char_0
+instance "^" :: (semiring_char_0,finite) semiring_char_0
 proof (intro_classes)
   fix m n ::nat
   show "(of_nat m :: 'a^'b) = of_nat n \<longleftrightarrow> m = n"
     by (simp add: Cart_eq of_nat_index)
 qed
 
-instance "^" :: (comm_ring_1,type) comm_ring_1 by intro_classes
-instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes
+instance "^" :: (comm_ring_1,finite) comm_ring_1 by intro_classes
+instance "^" :: (ring_char_0,finite) ring_char_0 by intro_classes
 
 lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x"
   by (vector mult_assoc)
@@ -324,7 +324,7 @@
 lemma vector_smult_rneg: "(c::'a::ring) *s -x = -(c *s x)" by vector
 lemma vector_smult_lneg: "- (c::'a::ring) *s x = -(c *s x)" by vector
 lemma vector_sneg_minus1: "-x = (- (1::'a::ring_1)) *s x" by vector
-lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector
+lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n::finite)" by vector
 lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x"
   by (vector ring_simps)
 
@@ -828,20 +828,20 @@
 
 subsection{* Properties of the dot product.  *}
 
-lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x"
+lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n::finite) \<bullet> y = y \<bullet> x"
   by (vector mult_commute)
-lemma dot_ladd: "((x::'a::ring ^ 'n) + y) \<bullet> z = (x \<bullet> z) + (y \<bullet> z)"
+lemma dot_ladd: "((x::'a::ring ^ 'n::finite) + y) \<bullet> z = (x \<bullet> z) + (y \<bullet> z)"
   by (vector ring_simps)
-lemma dot_radd: "x \<bullet> (y + (z::'a::ring ^ 'n)) = (x \<bullet> y) + (x \<bullet> z)"
+lemma dot_radd: "x \<bullet> (y + (z::'a::ring ^ 'n::finite)) = (x \<bullet> y) + (x \<bullet> z)"
   by (vector ring_simps)
-lemma dot_lsub: "((x::'a::ring ^ 'n) - y) \<bullet> z = (x \<bullet> z) - (y \<bullet> z)"
+lemma dot_lsub: "((x::'a::ring ^ 'n::finite) - y) \<bullet> z = (x \<bullet> z) - (y \<bullet> z)"
   by (vector ring_simps)
-lemma dot_rsub: "(x::'a::ring ^ 'n) \<bullet> (y - z) = (x \<bullet> y) - (x \<bullet> z)"
+lemma dot_rsub: "(x::'a::ring ^ 'n::finite) \<bullet> (y - z) = (x \<bullet> y) - (x \<bullet> z)"
   by (vector ring_simps)
 lemma dot_lmult: "(c *s x) \<bullet> y = (c::'a::ring) * (x \<bullet> y)" by (vector ring_simps)
 lemma dot_rmult: "x \<bullet> (c *s y) = (c::'a::comm_ring) * (x \<bullet> y)" by (vector ring_simps)
-lemma dot_lneg: "(-x) \<bullet> (y::'a::ring ^ 'n) = -(x \<bullet> y)" by vector
-lemma dot_rneg: "(x::'a::ring ^ 'n) \<bullet> (-y) = -(x \<bullet> y)" by vector
+lemma dot_lneg: "(-x) \<bullet> (y::'a::ring ^ 'n::finite) = -(x \<bullet> y)" by vector
+lemma dot_rneg: "(x::'a::ring ^ 'n::finite) \<bullet> (-y) = -(x \<bullet> y)" by vector
 lemma dot_lzero[simp]: "0 \<bullet> x = (0::'a::{comm_monoid_add, mult_zero})" by vector
 lemma dot_rzero[simp]: "x \<bullet> 0 = (0::'a::{comm_monoid_add, mult_zero})" by vector
 lemma dot_pos_le[simp]: "(0::'a\<Colon>ordered_ring_strict) <= x \<bullet> x"
@@ -1299,7 +1299,7 @@
   by norm
 
 lemma setsum_component [simp]:
-  fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n"
+  fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n::finite"
   shows "(setsum f S)$i = setsum (\<lambda>x. (f x)$i) S"
   by (cases "finite S", induct S set: finite, simp_all)
 
@@ -1313,7 +1313,7 @@
   by (auto simp add: insert_absorb)
 
 lemma setsum_cmul:
-  fixes f:: "'c \<Rightarrow> ('a::semiring_1)^'n"
+  fixes f:: "'c \<Rightarrow> ('a::semiring_1)^'n::finite"
   shows "setsum (\<lambda>x. c *s f x) S = c *s setsum f S"
   by (simp add: Cart_eq setsum_right_distrib)
 
@@ -1452,10 +1452,10 @@
   finally show ?thesis .
 qed
 
-lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> (y::'a::{comm_ring}^'n) = setsum (\<lambda>x. f x \<bullet> y) S "
+lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> (y::'a::{comm_ring}^'n::finite) = setsum (\<lambda>x. f x \<bullet> y) S "
   by (induct rule: finite_induct, auto simp add: dot_lzero dot_ladd dot_radd)
 
-lemma dot_rsum: "finite S \<Longrightarrow> (y::'a::{comm_ring}^'n) \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
+lemma dot_rsum: "finite S \<Longrightarrow> (y::'a::{comm_ring}^'n::finite) \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
   by (induct rule: finite_induct, auto simp add: dot_rzero dot_radd)
 
 subsection{* Basis vectors in coordinate directions. *}
@@ -1521,11 +1521,11 @@
   unfolding inner_vector_def basis_def
   by (auto simp add: cond_application_beta  cond_value_iff setsum_delta cong del: if_weak_cong)
 
-lemma basis_eq_0: "basis i = (0::'a::semiring_1^'n) \<longleftrightarrow> False"
+lemma basis_eq_0: "basis i = (0::'a::semiring_1^'n::finite) \<longleftrightarrow> False"
   by (auto simp add: Cart_eq)
 
 lemma basis_nonzero:
-  shows "basis k \<noteq> (0:: 'a::semiring_1 ^'n)"
+  shows "basis k \<noteq> (0:: 'a::semiring_1 ^'n::finite)"
   by (simp add: basis_eq_0)
 
 lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = (z::'a::semiring_1^'n::finite)"
@@ -1560,7 +1560,7 @@
 
   (* FIXME : Maybe some of these require less than comm_ring, but not all*)
 lemma orthogonal_clauses:
-  "orthogonal a (0::'a::comm_ring ^'n)"
+  "orthogonal a (0::'a::comm_ring ^'n::finite)"
   "orthogonal a x ==> orthogonal a (c *s x)"
   "orthogonal a x ==> orthogonal a (-x)"
   "orthogonal a x \<Longrightarrow> orthogonal a y ==> orthogonal a (x + y)"
@@ -1574,7 +1574,7 @@
   dot_lzero dot_rzero dot_lneg dot_lmult dot_ladd dot_lsub
   by simp_all
 
-lemma orthogonal_commute: "orthogonal (x::'a::{ab_semigroup_mult,comm_monoid_add} ^'n)y \<longleftrightarrow> orthogonal y x"
+lemma orthogonal_commute: "orthogonal (x::'a::{ab_semigroup_mult,comm_monoid_add} ^'n::finite)y \<longleftrightarrow> orthogonal y x"
   by (simp add: orthogonal_def dot_sym)
 
 subsection{* Explicit vector construction from lists. *}
@@ -1648,12 +1648,12 @@
 lemma linear_compose_cmul: "linear f ==> linear (\<lambda>x. (c::'a::comm_semiring) *s f x)"
   by (vector linear_def Cart_eq ring_simps)
 
-lemma linear_compose_neg: "linear (f :: 'a ^'n \<Rightarrow> 'a::comm_ring ^'m) ==> linear (\<lambda>x. -(f(x)))" by (vector linear_def Cart_eq)
-
-lemma linear_compose_add: "linear (f :: 'a ^'n \<Rightarrow> 'a::semiring_1 ^'m) \<Longrightarrow> linear g ==> linear (\<lambda>x. f(x) + g(x))"
+lemma linear_compose_neg: "linear (f :: 'a ^'n::finite \<Rightarrow> 'a::comm_ring ^'m::finite) ==> linear (\<lambda>x. -(f(x)))" by (vector linear_def Cart_eq)
+
+lemma linear_compose_add: "linear (f :: 'a ^'n::finite \<Rightarrow> 'a::semiring_1 ^'m::finite) \<Longrightarrow> linear g ==> linear (\<lambda>x. f(x) + g(x))"
   by (vector linear_def Cart_eq ring_simps)
 
-lemma linear_compose_sub: "linear (f :: 'a ^'n \<Rightarrow> 'a::ring_1 ^'m) \<Longrightarrow> linear g ==> linear (\<lambda>x. f x - g x)"
+lemma linear_compose_sub: "linear (f :: 'a ^'n::finite \<Rightarrow> 'a::ring_1 ^'m::finite) \<Longrightarrow> linear g ==> linear (\<lambda>x. f x - g x)"
   by (vector linear_def Cart_eq ring_simps)
 
 lemma linear_compose: "linear f \<Longrightarrow> linear g ==> linear (g o f)"
@@ -1661,24 +1661,24 @@
 
 lemma linear_id: "linear id" by (simp add: linear_def id_def)
 
-lemma linear_zero: "linear (\<lambda>x. 0::'a::semiring_1 ^ 'n)" by (simp add: linear_def)
+lemma linear_zero: "linear (\<lambda>x. 0::'a::semiring_1 ^ 'n::finite)" by (simp add: linear_def)
 
 lemma linear_compose_setsum:
-  assumes fS: "finite S" and lS: "\<forall>a \<in> S. linear (f a :: 'a::semiring_1 ^ 'n \<Rightarrow> 'a ^ 'm)"
-  shows "linear(\<lambda>x. setsum (\<lambda>a. f a x :: 'a::semiring_1 ^'m) S)"
+  assumes fS: "finite S" and lS: "\<forall>a \<in> S. linear (f a :: 'a::semiring_1 ^ 'n::finite \<Rightarrow> 'a ^ 'm::finite)"
+  shows "linear(\<lambda>x. setsum (\<lambda>a. f a x :: 'a::semiring_1 ^'m::finite) S)"
   using lS
   apply (induct rule: finite_induct[OF fS])
   by (auto simp add: linear_zero intro: linear_compose_add)
 
 lemma linear_vmul_component:
-  fixes f:: "'a::semiring_1^'m \<Rightarrow> 'a^'n"
+  fixes f:: "'a::semiring_1^'m::finite \<Rightarrow> 'a^'n::finite"
   assumes lf: "linear f"
   shows "linear (\<lambda>x. f x $ k *s v)"
   using lf
   apply (auto simp add: linear_def )
   by (vector ring_simps)+
 
-lemma linear_0: "linear f ==> f 0 = (0::'a::semiring_1 ^'n)"
+lemma linear_0: "linear f ==> f 0 = (0::'a::semiring_1 ^'n::finite)"
   unfolding linear_def
   apply clarsimp
   apply (erule allE[where x="0::'a"])
@@ -1687,17 +1687,17 @@
 
 lemma linear_cmul: "linear f ==> f(c*s x) = c *s f x" by (simp add: linear_def)
 
-lemma linear_neg: "linear (f :: 'a::ring_1 ^'n \<Rightarrow> _) ==> f (-x) = - f x"
+lemma linear_neg: "linear (f :: 'a::ring_1 ^'n::finite \<Rightarrow> _) ==> f (-x) = - f x"
   unfolding vector_sneg_minus1
   using linear_cmul[of f] by auto
 
 lemma linear_add: "linear f ==> f(x + y) = f x + f y" by (metis linear_def)
 
-lemma linear_sub: "linear (f::'a::ring_1 ^'n \<Rightarrow> _) ==> f(x - y) = f x - f y"
+lemma linear_sub: "linear (f::'a::ring_1 ^'n::finite \<Rightarrow> _) ==> f(x - y) = f x - f y"
   by (simp add: diff_def linear_add linear_neg)
 
 lemma linear_setsum:
-  fixes f:: "'a::semiring_1^'n \<Rightarrow> _"
+  fixes f:: "'a::semiring_1^'n::finite \<Rightarrow> _"
   assumes lf: "linear f" and fS: "finite S"
   shows "f (setsum g S) = setsum (f o g) S"
 proof (induct rule: finite_induct[OF fS])
@@ -1712,14 +1712,14 @@
 qed
 
 lemma linear_setsum_mul:
-  fixes f:: "'a ^'n \<Rightarrow> 'a::semiring_1^'m"
+  fixes f:: "'a ^'n::finite \<Rightarrow> 'a::semiring_1^'m::finite"
   assumes lf: "linear f" and fS: "finite S"
   shows "f (setsum (\<lambda>i. c i *s v i) S) = setsum (\<lambda>i. c i *s f (v i)) S"
   using linear_setsum[OF lf fS, of "\<lambda>i. c i *s v i" , unfolded o_def]
   linear_cmul[OF lf] by simp
 
 lemma linear_injective_0:
-  assumes lf: "linear (f:: 'a::ring_1 ^ 'n \<Rightarrow> _)"
+  assumes lf: "linear (f:: 'a::ring_1 ^ 'n::finite \<Rightarrow> _)"
   shows "inj f \<longleftrightarrow> (\<forall>x. f x = 0 \<longrightarrow> x = 0)"
 proof-
   have "inj f \<longleftrightarrow> (\<forall> x y. f x = f y \<longrightarrow> x = y)" by (simp add: inj_on_def)
@@ -1835,33 +1835,33 @@
 lemma bilinear_rmul: "bilinear h ==> h x (c *s y) = c *s (h x y)"
   by (simp add: bilinear_def linear_def)
 
-lemma bilinear_lneg: "bilinear h ==> h (- (x:: 'a::ring_1 ^ 'n)) y = -(h x y)"
+lemma bilinear_lneg: "bilinear h ==> h (- (x:: 'a::ring_1 ^ 'n::finite)) y = -(h x y)"
   by (simp only: vector_sneg_minus1 bilinear_lmul)
 
-lemma bilinear_rneg: "bilinear h ==> h x (- (y:: 'a::ring_1 ^ 'n)) = - h x y"
+lemma bilinear_rneg: "bilinear h ==> h x (- (y:: 'a::ring_1 ^ 'n::finite)) = - h x y"
   by (simp only: vector_sneg_minus1 bilinear_rmul)
 
 lemma  (in ab_group_add) eq_add_iff: "x = x + y \<longleftrightarrow> y = 0"
   using add_imp_eq[of x y 0] by auto
 
 lemma bilinear_lzero:
-  fixes h :: "'a::ring^'n \<Rightarrow> _" assumes bh: "bilinear h" shows "h 0 x = 0"
+  fixes h :: "'a::ring^'n::finite \<Rightarrow> _" assumes bh: "bilinear h" shows "h 0 x = 0"
   using bilinear_ladd[OF bh, of 0 0 x]
     by (simp add: eq_add_iff ring_simps)
 
 lemma bilinear_rzero:
-  fixes h :: "'a::ring^'n \<Rightarrow> _" assumes bh: "bilinear h" shows "h x 0 = 0"
+  fixes h :: "'a::ring^_ \<Rightarrow> _" assumes bh: "bilinear h" shows "h x 0 = 0"
   using bilinear_radd[OF bh, of x 0 0 ]
     by (simp add: eq_add_iff ring_simps)
 
-lemma bilinear_lsub: "bilinear h ==> h (x - (y:: 'a::ring_1 ^ 'n)) z = h x z - h y z"
+lemma bilinear_lsub: "bilinear h ==> h (x - (y:: 'a::ring_1 ^ _)) z = h x z - h y z"
   by (simp  add: diff_def bilinear_ladd bilinear_lneg)
 
-lemma bilinear_rsub: "bilinear h ==> h z (x - (y:: 'a::ring_1 ^ 'n)) = h z x - h z y"
+lemma bilinear_rsub: "bilinear h ==> h z (x - (y:: 'a::ring_1 ^ _)) = h z x - h z y"
   by (simp  add: diff_def bilinear_radd bilinear_rneg)
 
 lemma bilinear_setsum:
-  fixes h:: "'a ^'n \<Rightarrow> 'a::semiring_1^'m \<Rightarrow> 'a ^ 'k"
+  fixes h:: "'a ^_ \<Rightarrow> 'a::semiring_1^_\<Rightarrow> 'a ^ _"
   assumes bh: "bilinear h" and fS: "finite S" and fT: "finite T"
   shows "h (setsum f S) (setsum g T) = setsum (\<lambda>(i,j). h (f i) (g j)) (S \<times> T) "
 proof-
@@ -2032,14 +2032,14 @@
 consts generic_mult :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" (infixr "\<star>" 75)
 
 defs (overloaded)
-matrix_matrix_mult_def: "(m:: ('a::semiring_1) ^'n^'m) \<star> (m' :: 'a ^'p^'n) \<equiv> (\<chi> i j. setsum (\<lambda>k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"
+matrix_matrix_mult_def: "(m:: ('a::semiring_1) ^('n::finite)^'m::finite) \<star> (m' :: 'a ^('p::finite)^'n) \<equiv> (\<chi> i j. setsum (\<lambda>k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"
 
 abbreviation
-  matrix_matrix_mult' :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"  (infixl "**" 70)
+  matrix_matrix_mult' :: "('a::semiring_1) ^('n::finite)^'m::finite \<Rightarrow> 'a ^('p::finite)^'n \<Rightarrow> 'a ^ 'p ^'m"  (infixl "**" 70)
   where "m ** m' == m\<star> m'"
 
 defs (overloaded)
-  matrix_vector_mult_def: "(m::('a::semiring_1) ^'n^'m) \<star> (x::'a ^'n) \<equiv> (\<chi> i. setsum (\<lambda>j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m"
+  matrix_vector_mult_def: "(m::('a::semiring_1) ^('n::finite)^('m::finite)) \<star> (x::'a ^'n) \<equiv> (\<chi> i. setsum (\<lambda>j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m"
 
 abbreviation
   matrix_vector_mult' :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'm"  (infixl "*v" 70)
@@ -2047,26 +2047,26 @@
   "m *v v == m \<star> v"
 
 defs (overloaded)
-  vector_matrix_mult_def: "(x::'a^'m) \<star> (m::('a::semiring_1) ^'n^'m) \<equiv> (\<chi> j. setsum (\<lambda>i. ((m$i)$j) * (x$i)) (UNIV :: 'm set)) :: 'a^'n"
+  vector_matrix_mult_def: "(x::'a^('m::finite)) \<star> (m::('a::semiring_1) ^('n::finite)^'m) \<equiv> (\<chi> j. setsum (\<lambda>i. ((m$i)$j) * (x$i)) (UNIV :: 'm set)) :: 'a^'n"
 
 abbreviation
   vactor_matrix_mult' :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n "  (infixl "v*" 70)
   where
   "v v* m == v \<star> m"
 
-definition "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"
-definition "(transp::'a^'n^'m \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A$j)$i))"
-definition "(row::'m => 'a ^'n^'m \<Rightarrow> 'a ^'n) i A = (\<chi> j. ((A$i)$j))"
-definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A$i)$j))"
-definition "rows(A::'a^'n^'m) = { row i A | i. i \<in> (UNIV :: 'm set)}"
-definition "columns(A::'a^'n^'m) = { column i A | i. i \<in> (UNIV :: 'n set)}"
+definition "(mat::'a::zero => 'a ^('n::finite)^'n::finite) k = (\<chi> i j. if i = j then k else 0)"
+definition "(transp::'a^('n::finite)^('m::finite) \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A$j)$i))"
+definition "(row::'m::finite => 'a ^'n^'m \<Rightarrow> 'a ^'n::finite) i A = (\<chi> j. ((A$i)$j))"
+definition "(column::'n::finite =>'a^'n^'m =>'a^'m::finite) j A = (\<chi> i. ((A$i)$j))"
+definition "rows(A::'a^('n::finite)^'m::finite) = { row i A | i. i \<in> (UNIV :: 'm set)}"
+definition "columns(A::'a^('n::finite)^'m::finite) = { column i A | i. i \<in> (UNIV :: 'n set)}"
 
 lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def)
 lemma matrix_add_ldistrib: "(A ** (B + C)) = (A \<star> B) + (A \<star> C)"
   by (vector matrix_matrix_mult_def setsum_addf[symmetric] ring_simps)
 
 lemma matrix_mul_lid:
-  fixes A :: "'a::semiring_1 ^ 'm ^ 'n::finite"
+  fixes A :: "'a::semiring_1 ^ ('m::finite) ^ _"
   shows "mat 1 ** A = A"
   apply (simp add: matrix_matrix_mult_def mat_def)
   apply vector
@@ -2074,7 +2074,7 @@
 
 
 lemma matrix_mul_rid:
-  fixes A :: "'a::semiring_1 ^ 'm::finite ^ 'n"
+  fixes A :: "'a::semiring_1 ^ 'm::finite ^ _::finite"
   shows "A ** mat 1 = A"
   apply (simp add: matrix_matrix_mult_def mat_def)
   apply vector
@@ -2097,11 +2097,11 @@
   by (simp add: cond_value_iff cond_application_beta
     setsum_delta' cong del: if_weak_cong)
 
-lemma matrix_transp_mul: "transp(A ** B) = transp B ** transp (A::'a::comm_semiring_1^'m^'n)"
+lemma matrix_transp_mul: "transp(A ** B) = transp B ** transp (A::'a::comm_semiring_1^_^_)"
   by (simp add: matrix_matrix_mult_def transp_def Cart_eq mult_commute)
 
 lemma matrix_eq:
-  fixes A B :: "'a::semiring_1 ^ 'n::finite ^ 'm"
+  fixes A B :: "'a::semiring_1 ^ 'n::finite ^ _::finite"
   shows "A = B \<longleftrightarrow>  (\<forall>x. A *v x = B *v x)" (is "?lhs \<longleftrightarrow> ?rhs")
   apply auto
   apply (subst Cart_eq)
@@ -2112,10 +2112,10 @@
   by (auto simp add: basis_def cond_value_iff cond_application_beta setsum_delta[OF finite] cong del: if_weak_cong)
 
 lemma matrix_vector_mul_component:
-  shows "((A::'a::semiring_1^'n'^'m) *v x)$k = (A$k) \<bullet> x"
+  shows "((A::'a::semiring_1^_^_) *v x)$k = (A$k) \<bullet> x"
   by (simp add: matrix_vector_mult_def dot_def)
 
-lemma dot_lmul_matrix: "((x::'a::comm_semiring_1 ^'n) v* A) \<bullet> y = x \<bullet> (A *v y)"
+lemma dot_lmul_matrix: "((x::'a::comm_semiring_1 ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
   apply (simp add: dot_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac)
   apply (subst setsum_commute)
   by simp
@@ -2127,26 +2127,26 @@
   by (vector transp_def)
 
 lemma row_transp:
-  fixes A:: "'a::semiring_1^'n^'m"
+  fixes A:: "'a::semiring_1^_^_"
   shows "row i (transp A) = column i A"
   by (simp add: row_def column_def transp_def Cart_eq)
 
 lemma column_transp:
-  fixes A:: "'a::semiring_1^'n^'m"
+  fixes A:: "'a::semiring_1^_^_"
   shows "column i (transp A) = row i A"
   by (simp add: row_def column_def transp_def Cart_eq)
 
-lemma rows_transp: "rows(transp (A::'a::semiring_1^'n^'m)) = columns A"
+lemma rows_transp: "rows(transp (A::'a::semiring_1^_^_)) = columns A"
 by (auto simp add: rows_def columns_def row_transp intro: set_ext)
 
-lemma columns_transp: "columns(transp (A::'a::semiring_1^'n^'m)) = rows A" by (metis transp_transp rows_transp)
+lemma columns_transp: "columns(transp (A::'a::semiring_1^_^_)) = rows A" by (metis transp_transp rows_transp)
 
 text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *}
 
 lemma matrix_mult_dot: "A *v x = (\<chi> i. A$i \<bullet> x)"
   by (simp add: matrix_vector_mult_def dot_def)
 
-lemma matrix_mult_vsum: "(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\<lambda>i. (x$i) *s column i A) (UNIV:: 'n set)"
+lemma matrix_mult_vsum: "(A::'a::comm_semiring_1^('n::finite)^'m::finite) *v x = setsum (\<lambda>i. (x$i) *s column i A) (UNIV:: 'n set)"
   by (simp add: matrix_vector_mult_def Cart_eq column_def mult_commute)
 
 lemma vector_componentwise:
@@ -2155,7 +2155,7 @@
   by (vector Cart_eq setsum_component)
 
 lemma linear_componentwise:
-  fixes f:: "'a::ring_1 ^ 'm::finite \<Rightarrow> 'a ^ 'n"
+  fixes f:: "'a::ring_1 ^ 'm::finite \<Rightarrow> 'a ^ _"
   assumes lf: "linear f"
   shows "(f x)$j = setsum (\<lambda>i. (x$i) * (f (basis i)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs")
 proof-
@@ -2171,17 +2171,17 @@
 
 text{* Inverse matrices  (not necessarily square) *}
 
-definition "invertible(A::'a::semiring_1^'n^'m) \<longleftrightarrow> (\<exists>A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
-
-definition "matrix_inv(A:: 'a::semiring_1^'n^'m) =
+definition "invertible(A::'a::semiring_1^('n::finite)^'m::finite) \<longleftrightarrow> (\<exists>A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
+
+definition "matrix_inv(A:: 'a::semiring_1^('n::finite)^'m::finite) =
         (SOME A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
 
 text{* Correspondence between matrices and linear operators. *}
 
-definition matrix:: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n"
+definition matrix:: "('a::{plus,times, one, zero}^'m::finite \<Rightarrow> 'a ^ 'n::finite) \<Rightarrow> 'a^'m^'n"
 where "matrix f = (\<chi> i j. (f(basis j))$i)"
 
-lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::'a::comm_semiring_1 ^ 'n))"
+lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::'a::comm_semiring_1 ^ _))"
   by (simp add: linear_def matrix_vector_mult_def Cart_eq ring_simps setsum_right_distrib setsum_addf)
 
 lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::'a::comm_ring_1 ^ 'n::finite)"
@@ -2197,12 +2197,12 @@
 
 lemma matrix_compose:
   assumes lf: "linear (f::'a::comm_ring_1^'n::finite \<Rightarrow> 'a^'m::finite)"
-  and lg: "linear (g::'a::comm_ring_1^'m::finite \<Rightarrow> 'a^'k)"
+  and lg: "linear (g::'a::comm_ring_1^'m::finite \<Rightarrow> 'a^_)"
   shows "matrix (g o f) = matrix g ** matrix f"
   using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]]
   by (simp  add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)
 
-lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\<lambda>i. (x$i) *s ((transp A)$i)) (UNIV:: 'n set)"
+lemma matrix_vector_column:"(A::'a::comm_semiring_1^('n::finite)^_) *v x = setsum (\<lambda>i. (x$i) *s ((transp A)$i)) (UNIV:: 'n set)"
   by (simp add: matrix_vector_mult_def transp_def Cart_eq mult_commute)
 
 lemma adjoint_matrix: "adjoint(\<lambda>x. (A::'a::comm_ring_1^'n::finite^'m::finite) *v x) = (\<lambda>x. transp A *v x)"
@@ -2287,7 +2287,7 @@
 
 
 lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
-   (\<exists>x::'a ^ 'n. \<forall>i. P i (x$i))" (is "?lhs \<longleftrightarrow> ?rhs")
+   (\<exists>x::'a ^ 'n::finite. \<forall>i. P i (x$i))" (is "?lhs \<longleftrightarrow> ?rhs")
 proof-
   let ?S = "(UNIV :: 'n set)"
   {assume H: "?rhs"
@@ -2534,14 +2534,14 @@
   apply(rule conjI) defer apply(rule conjI) defer apply(rule_tac x=1 in exI) by auto
 
 lemma linear_vmul_dest_vec1:
-  fixes f:: "'a::semiring_1^'n \<Rightarrow> 'a^1"
+  fixes f:: "'a::semiring_1^_ \<Rightarrow> 'a^1"
   shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"
   unfolding dest_vec1_def
   apply (rule linear_vmul_component)
   by auto
 
 lemma linear_from_scalars:
-  assumes lf: "linear (f::'a::comm_ring_1 ^1 \<Rightarrow> 'a^'n)"
+  assumes lf: "linear (f::'a::comm_ring_1 ^1 \<Rightarrow> 'a^_)"
   shows "f = (\<lambda>x. dest_vec1 x *s column 1 (matrix f))"
   apply (rule ext)
   apply (subst matrix_works[OF lf, symmetric])
@@ -2580,16 +2580,16 @@
 lemma fstcart_vec[simp]: "fstcart(vec x) = vec x"
   by (simp add: Cart_eq)
 
-lemma fstcart_add[simp]:"fstcart(x + y) = fstcart (x::'a::{plus,times}^('b + 'c)) + fstcart y"
+lemma fstcart_add[simp]:"fstcart(x + y) = fstcart (x::'a::{plus,times}^('b::finite + 'c::finite)) + fstcart y"
   by (simp add: Cart_eq)
 
-lemma fstcart_cmul[simp]:"fstcart(c*s x) = c*s fstcart (x::'a::{plus,times}^('b + 'c))"
+lemma fstcart_cmul[simp]:"fstcart(c*s x) = c*s fstcart (x::'a::{plus,times}^('b::finite + 'c::finite))"
   by (simp add: Cart_eq)
 
-lemma fstcart_neg[simp]:"fstcart(- x) = - fstcart (x::'a::ring_1^('b + 'c))"
+lemma fstcart_neg[simp]:"fstcart(- x) = - fstcart (x::'a::ring_1^(_ + _))"
   by (simp add: Cart_eq)
 
-lemma fstcart_sub[simp]:"fstcart(x - y) = fstcart (x::'a::ring_1^('b + 'c)) - fstcart y"
+lemma fstcart_sub[simp]:"fstcart(x - y) = fstcart (x::'a::ring_1^(_ + _)) - fstcart y"
   by (simp add: Cart_eq)
 
 lemma fstcart_setsum:
@@ -2601,16 +2601,16 @@
 lemma sndcart_vec[simp]: "sndcart(vec x) = vec x"
   by (simp add: Cart_eq)
 
-lemma sndcart_add[simp]:"sndcart(x + y) = sndcart (x::'a::{plus,times}^('b + 'c)) + sndcart y"
+lemma sndcart_add[simp]:"sndcart(x + y) = sndcart (x::'a::{plus,times}^(_ + _)) + sndcart y"
   by (simp add: Cart_eq)
 
-lemma sndcart_cmul[simp]:"sndcart(c*s x) = c*s sndcart (x::'a::{plus,times}^('b + 'c))"
+lemma sndcart_cmul[simp]:"sndcart(c*s x) = c*s sndcart (x::'a::{plus,times}^(_ + _))"
   by (simp add: Cart_eq)
 
-lemma sndcart_neg[simp]:"sndcart(- x) = - sndcart (x::'a::ring_1^('b + 'c))"
+lemma sndcart_neg[simp]:"sndcart(- x) = - sndcart (x::'a::ring_1^(_ + _))"
   by (simp add: Cart_eq)
 
-lemma sndcart_sub[simp]:"sndcart(x - y) = sndcart (x::'a::ring_1^('b + 'c)) - sndcart y"
+lemma sndcart_sub[simp]:"sndcart(x - y) = sndcart (x::'a::ring_1^(_ + _)) - sndcart y"
   by (simp add: Cart_eq)
 
 lemma sndcart_setsum:
@@ -2922,10 +2922,10 @@
 lemma subspace_mul: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> c *s x \<in> S"
   by (metis subspace_def)
 
-lemma subspace_neg: "subspace S \<Longrightarrow> (x::'a::ring_1^'n) \<in> S \<Longrightarrow> - x \<in> S"
+lemma subspace_neg: "subspace S \<Longrightarrow> (x::'a::ring_1^_) \<in> S \<Longrightarrow> - x \<in> S"
   by (metis vector_sneg_minus1 subspace_mul)
 
-lemma subspace_sub: "subspace S \<Longrightarrow> (x::'a::ring_1^'n) \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
+lemma subspace_sub: "subspace S \<Longrightarrow> (x::'a::ring_1^_) \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
   by (metis diff_def subspace_add subspace_neg)
 
 lemma subspace_setsum:
@@ -2937,7 +2937,7 @@
   by (simp add: subspace_def sA, auto simp add: sA subspace_add)
 
 lemma subspace_linear_image:
-  assumes lf: "linear (f::'a::semiring_1^'n \<Rightarrow> _)" and sS: "subspace S"
+  assumes lf: "linear (f::'a::semiring_1^_ \<Rightarrow> _)" and sS: "subspace S"
   shows "subspace(f ` S)"
   using lf sS linear_0[OF lf]
   unfolding linear_def subspace_def
@@ -2946,7 +2946,7 @@
   apply (rule_tac x="c*s x" in bexI, auto)
   done
 
-lemma subspace_linear_preimage: "linear (f::'a::semiring_1^'n \<Rightarrow> _) ==> subspace S ==> subspace {x. f x \<in> S}"
+lemma subspace_linear_preimage: "linear (f::'a::semiring_1^_ \<Rightarrow> _) ==> subspace S ==> subspace {x. f x \<in> S}"
   by (auto simp add: subspace_def linear_def linear_0[of f])
 
 lemma subspace_trivial: "subspace {0::'a::semiring_1 ^_}"
@@ -2997,11 +2997,11 @@
   show "P x" by (metis mem_def subset_eq)
 qed
 
-lemma span_empty: "span {} = {(0::'a::semiring_0 ^ 'n)}"
+lemma span_empty: "span {} = {(0::'a::semiring_0 ^ _)}"
   apply (simp add: span_def)
   apply (rule hull_unique)
   apply (auto simp add: mem_def subspace_def)
-  unfolding mem_def[of "0::'a^'n", symmetric]
+  unfolding mem_def[of "0::'a^_", symmetric]
   apply simp
   done
 
@@ -3023,13 +3023,13 @@
   and P: "subspace P" shows "\<forall>x \<in> span S. P x"
   using span_induct SP P by blast
 
-inductive span_induct_alt_help for S:: "'a::semiring_1^'n \<Rightarrow> bool"
+inductive span_induct_alt_help for S:: "'a::semiring_1^_ \<Rightarrow> bool"
   where
   span_induct_alt_help_0: "span_induct_alt_help S 0"
   | span_induct_alt_help_S: "x \<in> S \<Longrightarrow> span_induct_alt_help S z \<Longrightarrow> span_induct_alt_help S (c *s x + z)"
 
 lemma span_induct_alt':
-  assumes h0: "h (0::'a::semiring_1^'n)" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c*s x + y)" shows "\<forall>x \<in> span S. h x"
+  assumes h0: "h (0::'a::semiring_1^'n::finite)" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c*s x + y)" shows "\<forall>x \<in> span S. h x"
 proof-
   {fix x:: "'a^'n" assume x: "span_induct_alt_help S x"
     have "h x"
@@ -3078,7 +3078,7 @@
 qed
 
 lemma span_induct_alt:
-  assumes h0: "h (0::'a::semiring_1^'n)" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c*s x + y)" and x: "x \<in> span S"
+  assumes h0: "h (0::'a::semiring_1^'n::finite)" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c*s x + y)" and x: "x \<in> span S"
   shows "h x"
 using span_induct_alt'[of h S] h0 hS x by blast
 
@@ -3094,24 +3094,24 @@
 lemma span_mul: "x \<in> span S ==> (c *s x) \<in> span S"
   by (metis subspace_span subspace_mul)
 
-lemma span_neg: "x \<in> span S ==> - (x::'a::ring_1^'n) \<in> span S"
+lemma span_neg: "x \<in> span S ==> - (x::'a::ring_1^_) \<in> span S"
   by (metis subspace_neg subspace_span)
 
-lemma span_sub: "(x::'a::ring_1^'n) \<in> span S \<Longrightarrow> y \<in> span S ==> x - y \<in> span S"
+lemma span_sub: "(x::'a::ring_1^_) \<in> span S \<Longrightarrow> y \<in> span S ==> x - y \<in> span S"
   by (metis subspace_span subspace_sub)
 
 lemma span_setsum: "finite A \<Longrightarrow> \<forall>x \<in> A. f x \<in> span S ==> setsum f A \<in> span S"
   apply (rule subspace_setsum)
   by (metis subspace_span subspace_setsum)+
 
-lemma span_add_eq: "(x::'a::ring_1^'n) \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
+lemma span_add_eq: "(x::'a::ring_1^_) \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
   apply (auto simp only: span_add span_sub)
   apply (subgoal_tac "(x + y) - x \<in> span S", simp)
   by (simp only: span_add span_sub)
 
 (* Mapping under linear image. *)
 
-lemma span_linear_image: assumes lf: "linear (f::'a::semiring_1 ^ 'n => _)"
+lemma span_linear_image: assumes lf: "linear (f::'a::semiring_1 ^ _ => _)"
   shows "span (f ` S) = f ` (span S)"
 proof-
   {fix x
@@ -3144,7 +3144,7 @@
 (* The key breakdown property. *)
 
 lemma span_breakdown:
-  assumes bS: "(b::'a::ring_1 ^ 'n) \<in> S" and aS: "a \<in> span S"
+  assumes bS: "(b::'a::ring_1 ^ _) \<in> S" and aS: "a \<in> span S"
   shows "\<exists>k. a - k*s b \<in> span (S - {b})" (is "?P a")
 proof-
   {fix x assume xS: "x \<in> S"
@@ -3186,7 +3186,7 @@
 qed
 
 lemma span_breakdown_eq:
-  "(x::'a::ring_1^'n) \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. (x - k *s a) \<in> span S)" (is "?lhs \<longleftrightarrow> ?rhs")
+  "(x::'a::ring_1^_) \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. (x - k *s a) \<in> span S)" (is "?lhs \<longleftrightarrow> ?rhs")
 proof-
   {assume x: "x \<in> span (insert a S)"
     from x span_breakdown[of "a" "insert a S" "x"]
@@ -3217,7 +3217,7 @@
 (* Hence some "reversal" results.*)
 
 lemma in_span_insert:
-  assumes a: "(a::'a::field^'n) \<in> span (insert b S)" and na: "a \<notin> span S"
+  assumes a: "(a::'a::field^_) \<in> span (insert b S)" and na: "a \<notin> span S"
   shows "b \<in> span (insert a S)"
 proof-
   from span_breakdown[of b "insert b S" a, OF insertI1 a]
@@ -3256,7 +3256,7 @@
 qed
 
 lemma in_span_delete:
-  assumes a: "(a::'a::field^'n) \<in> span S"
+  assumes a: "(a::'a::field^_) \<in> span S"
   and na: "a \<notin> span (S-{b})"
   shows "b \<in> span (insert a (S - {b}))"
   apply (rule in_span_insert)
@@ -3270,7 +3270,7 @@
 (* Transitivity property. *)
 
 lemma span_trans:
-  assumes x: "(x::'a::ring_1^'n) \<in> span S" and y: "y \<in> span (insert x S)"
+  assumes x: "(x::'a::ring_1^_) \<in> span S" and y: "y \<in> span (insert x S)"
   shows "y \<in> span S"
 proof-
   from span_breakdown[of x "insert x S" y, OF insertI1 y]
@@ -3292,7 +3292,7 @@
 (* ------------------------------------------------------------------------- *)
 
 lemma span_explicit:
-  "span P = {y::'a::semiring_1^'n. \<exists>S u. finite S \<and> S \<subseteq> P \<and> setsum (\<lambda>v. u v *s v) S = y}"
+  "span P = {y::'a::semiring_1^_. \<exists>S u. finite S \<and> S \<subseteq> P \<and> setsum (\<lambda>v. u v *s v) S = y}"
   (is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \<exists>S u. ?Q S u y}")
 proof-
   {fix x assume x: "x \<in> ?E"
@@ -3351,7 +3351,7 @@
 qed
 
 lemma dependent_explicit:
-  "dependent P \<longleftrightarrow> (\<exists>S u. finite S \<and> S \<subseteq> P \<and> (\<exists>(v::'a::{idom,field}^'n) \<in>S. u v \<noteq> 0 \<and> setsum (\<lambda>v. u v *s v) S = 0))" (is "?lhs = ?rhs")
+  "dependent P \<longleftrightarrow> (\<exists>S u. finite S \<and> S \<subseteq> P \<and> (\<exists>(v::'a::{idom,field}^_) \<in>S. u v \<noteq> 0 \<and> setsum (\<lambda>v. u v *s v) S = 0))" (is "?lhs = ?rhs")
 proof-
   {assume dP: "dependent P"
     then obtain a S u where aP: "a \<in> P" and fS: "finite S"
@@ -3402,7 +3402,7 @@
 
 lemma span_finite:
   assumes fS: "finite S"
-  shows "span S = {(y::'a::semiring_1^'n). \<exists>u. setsum (\<lambda>v. u v *s v) S = y}"
+  shows "span S = {(y::'a::semiring_1^_). \<exists>u. setsum (\<lambda>v. u v *s v) S = y}"
   (is "_ = ?rhs")
 proof-
   {fix y assume y: "y \<in> span S"
@@ -3450,14 +3450,14 @@
 
 
 lemma independent_stdbasis_lemma:
-  assumes x: "(x::'a::semiring_1 ^ 'n) \<in> span (basis ` S)"
+  assumes x: "(x::'a::semiring_1 ^ _) \<in> span (basis ` S)"
   and iS: "i \<notin> S"
   shows "(x$i) = 0"
 proof-
   let ?U = "UNIV :: 'n set"
   let ?B = "basis ` S"
-  let ?P = "\<lambda>(x::'a^'n). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x$i =0"
- {fix x::"'a^'n" assume xS: "x\<in> ?B"
+  let ?P = "\<lambda>(x::'a^_). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x$i =0"
+ {fix x::"'a^_" assume xS: "x\<in> ?B"
    from xS have "?P x" by auto}
  moreover
  have "subspace ?P"
@@ -3490,7 +3490,7 @@
 (* This is useful for building a basis step-by-step.                         *)
 
 lemma independent_insert:
-  "independent(insert (a::'a::field ^'n) S) \<longleftrightarrow>
+  "independent(insert (a::'a::field ^_) S) \<longleftrightarrow>
       (if a \<in> S then independent S
                 else independent S \<and> a \<notin> span S)" (is "?lhs \<longleftrightarrow> ?rhs")
 proof-
@@ -3539,7 +3539,7 @@
   by (metis subset_eq span_superset)
 
 lemma spanning_subset_independent:
-  assumes BA: "B \<subseteq> A" and iA: "independent (A::('a::field ^'n) set)"
+  assumes BA: "B \<subseteq> A" and iA: "independent (A::('a::field ^_) set)"
   and AsB: "A \<subseteq> span B"
   shows "A = B"
 proof
@@ -3566,7 +3566,7 @@
 (* The general case of the Exchange Lemma, the key to what follows.  *)
 
 lemma exchange_lemma:
-  assumes f:"finite (t:: ('a::field^'n) set)" and i: "independent s"
+  assumes f:"finite (t:: ('a::field^'n::finite) set)" and i: "independent s"
   and sp:"s \<subseteq> span t"
   shows "\<exists>t'. (card t' = card t) \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
 using f i sp
@@ -3650,7 +3650,7 @@
 (* This implies corresponding size bounds.                                   *)
 
 lemma independent_span_bound:
-  assumes f: "finite t" and i: "independent (s::('a::field^'n) set)" and sp:"s \<subseteq> span t"
+  assumes f: "finite t" and i: "independent (s::('a::field^_) set)" and sp:"s \<subseteq> span t"
   shows "finite s \<and> card s \<le> card t"
   by (metis exchange_lemma[OF f i sp] finite_subset card_mono)
 
@@ -3835,7 +3835,7 @@
   by (metis dim_span)
 
 lemma spans_image:
-  assumes lf: "linear (f::'a::semiring_1^'n \<Rightarrow> _)" and VB: "V \<subseteq> span B"
+  assumes lf: "linear (f::'a::semiring_1^_ \<Rightarrow> _)" and VB: "V \<subseteq> span B"
   shows "f ` V \<subseteq> span (f ` B)"
   unfolding span_linear_image[OF lf]
   by (metis VB image_mono)
@@ -3857,7 +3857,7 @@
 (* Relation between bases and injectivity/surjectivity of map.               *)
 
 lemma spanning_surjective_image:
-  assumes us: "UNIV \<subseteq> span (S:: ('a::semiring_1 ^'n) set)"
+  assumes us: "UNIV \<subseteq> span (S:: ('a::semiring_1 ^_) set)"
   and lf: "linear f" and sf: "surj f"
   shows "UNIV \<subseteq> span (f ` S)"
 proof-
@@ -3867,7 +3867,7 @@
 qed
 
 lemma independent_injective_image:
-  assumes iS: "independent (S::('a::semiring_1^'n) set)" and lf: "linear f" and fi: "inj f"
+  assumes iS: "independent (S::('a::semiring_1^_) set)" and lf: "linear f" and fi: "inj f"
   shows "independent (f ` S)"
 proof-
   {fix a assume a: "a \<in> S" "f a \<in> span (f ` S - {f a})"
@@ -4058,7 +4058,7 @@
   assumes lf: "linear f" and fB: "finite B"
   and ifB: "independent (f ` B)"
   and fi: "inj_on f B" and xsB: "x \<in> span B"
-  and fx: "f (x::'a::field^'n) = 0"
+  and fx: "f (x::'a::field^_) = 0"
   shows "x = 0"
   using fB ifB fi xsB fx
 proof(induct arbitrary: x rule: finite_induct[OF fB])
@@ -4109,7 +4109,7 @@
 
 lemma linear_independent_extend_lemma:
   assumes fi: "finite B" and ib: "independent B"
-  shows "\<exists>g. (\<forall>x\<in> span B. \<forall>y\<in> span B. g ((x::'a::field^'n) + y) = g x + g y)
+  shows "\<exists>g. (\<forall>x\<in> span B. \<forall>y\<in> span B. g ((x::'a::field^'n::finite) + y) = g x + g y)
            \<and> (\<forall>x\<in> span B. \<forall>c. g (c*s x) = c *s g x)
            \<and> (\<forall>x\<in> B. g x = f x)"
 using ib fi
@@ -4288,14 +4288,14 @@
 (* linear functions are equal on a subspace if they are on a spanning set.   *)
 
 lemma subspace_kernel:
-  assumes lf: "linear (f::'a::semiring_1 ^'n \<Rightarrow> _)"
+  assumes lf: "linear (f::'a::semiring_1 ^_ \<Rightarrow> _)"
   shows "subspace {x. f x = 0}"
 apply (simp add: subspace_def)
 by (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf])
 
 lemma linear_eq_0_span:
   assumes lf: "linear f" and f0: "\<forall>x\<in>B. f x = 0"
-  shows "\<forall>x \<in> span B. f x = (0::'a::semiring_1 ^'n)"
+  shows "\<forall>x \<in> span B. f x = (0::'a::semiring_1 ^_)"
 proof
   fix x assume x: "x \<in> span B"
   let ?P = "\<lambda>x. f x = 0"
@@ -4305,11 +4305,11 @@
 
 lemma linear_eq_0:
   assumes lf: "linear f" and SB: "S \<subseteq> span B" and f0: "\<forall>x\<in>B. f x = 0"
-  shows "\<forall>x \<in> S. f x = (0::'a::semiring_1^'n)"
+  shows "\<forall>x \<in> S. f x = (0::'a::semiring_1^_)"
   by (metis linear_eq_0_span[OF lf] subset_eq SB f0)
 
 lemma linear_eq:
-  assumes lf: "linear (f::'a::ring_1^'n \<Rightarrow> _)" and lg: "linear g" and S: "S \<subseteq> span B"
+  assumes lf: "linear (f::'a::ring_1^_ \<Rightarrow> _)" and lg: "linear g" and S: "S \<subseteq> span B"
   and fg: "\<forall> x\<in> B. f x = g x"
   shows "\<forall>x\<in> S. f x = g x"
 proof-
@@ -4337,7 +4337,7 @@
 (* Similar results for bilinear functions.                                   *)
 
 lemma bilinear_eq:
-  assumes bf: "bilinear (f:: 'a::ring^'m \<Rightarrow> 'a^'n \<Rightarrow> 'a^'p)"
+  assumes bf: "bilinear (f:: 'a::ring^_ \<Rightarrow> 'a^_ \<Rightarrow> 'a^_)"
   and bg: "bilinear g"
   and SB: "S \<subseteq> span B" and TC: "T \<subseteq> span C"
   and fg: "\<forall>x\<in> B. \<forall>y\<in> C. f x y = g x y"
@@ -4365,7 +4365,7 @@
 qed
 
 lemma bilinear_eq_stdbasis:
-  assumes bf: "bilinear (f:: 'a::ring_1^'m::finite \<Rightarrow> 'a^'n::finite \<Rightarrow> 'a^'p)"
+  assumes bf: "bilinear (f:: 'a::ring_1^'m::finite \<Rightarrow> 'a^'n::finite \<Rightarrow> 'a^_)"
   and bg: "bilinear g"
   and fg: "\<forall>i j. f (basis i) (basis j) = g (basis i) (basis j)"
   shows "f = g"
@@ -4377,11 +4377,11 @@
 (* Detailed theorems about left and right invertibility in general case.     *)
 
 lemma left_invertible_transp:
-  "(\<exists>(B::'a^'n^'m). B ** transp (A::'a^'n^'m) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B::'a^'m^'n). A ** B = mat 1)"
+  "(\<exists>(B). B ** transp (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)"
   by (metis matrix_transp_mul transp_mat transp_transp)
 
 lemma right_invertible_transp:
-  "(\<exists>(B::'a^'n^'m). transp (A::'a^'n^'m) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B::'a^'m^'n). B ** A = mat 1)"
+  "(\<exists>(B). transp (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). B ** A = mat 1)"
   by (metis matrix_transp_mul transp_mat transp_transp)
 
 lemma linear_injective_left_inverse:
@@ -4816,8 +4816,8 @@
   by auto
 
 lemma infnorm_set_image:
-  "{abs(x$i) |i. i\<in> (UNIV :: 'n set)} =
-  (\<lambda>i. abs(x$i)) ` (UNIV :: 'n set)" by blast
+  "{abs(x$i) |i. i\<in> (UNIV :: _ set)} =
+  (\<lambda>i. abs(x$i)) ` (UNIV)" by blast
 
 lemma infnorm_set_lemma:
   shows "finite {abs((x::'a::abs ^'n::finite)$i) |i. i\<in> (UNIV :: 'n set)}"
@@ -5049,12 +5049,12 @@
 
 lemma collinear_empty:  "collinear {}" by (simp add: collinear_def)
 
-lemma collinear_sing: "collinear {(x::'a::ring_1^'n)}"
+lemma collinear_sing: "collinear {(x::'a::ring_1^_)}"
   apply (simp add: collinear_def)
   apply (rule exI[where x=0])
   by simp
 
-lemma collinear_2: "collinear {(x::'a::ring_1^'n),y}"
+lemma collinear_2: "collinear {(x::'a::ring_1^_),y}"
   apply (simp add: collinear_def)
   apply (rule exI[where x="x - y"])
   apply auto
@@ -5064,7 +5064,7 @@
   apply (rule exI[where x=0], simp)
   done
 
-lemma collinear_lemma: "collinear {(0::real^'n),x,y} \<longleftrightarrow> x = 0 \<or> y = 0 \<or> (\<exists>c. y = c *s x)" (is "?lhs \<longleftrightarrow> ?rhs")
+lemma collinear_lemma: "collinear {(0::real^_),x,y} \<longleftrightarrow> x = 0 \<or> y = 0 \<or> (\<exists>c. y = c *s x)" (is "?lhs \<longleftrightarrow> ?rhs")
 proof-
   {assume "x=0 \<or> y = 0" hence ?thesis
       by (cases "x = 0", simp_all add: collinear_2 insert_commute)}
diff -r cf455b5880e1 -r c9c14c72d035 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Jan 07 12:24:35 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Jan 06 13:07:30 2010 +0100
@@ -12,7 +12,7 @@
 
 typedef (open Cart)
   ('a, 'b) "^" (infixl "^" 15)
-    = "UNIV :: ('b \<Rightarrow> 'a) set"
+    = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
   morphisms Cart_nth Cart_lambda ..
 
 notation Cart_nth (infixl "$" 90)
@@ -25,14 +25,14 @@
   apply auto
   done
 
-lemma Cart_eq: "((x:: 'a ^ 'b) = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
+lemma Cart_eq: "((x:: 'a ^ 'b::finite) = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
   by (simp add: Cart_nth_inject [symmetric] expand_fun_eq)
 
 lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i"
   by (simp add: Cart_lambda_inverse)
 
 lemma Cart_lambda_unique:
-  fixes f :: "'a ^ 'b"
+  fixes f :: "'a ^ 'b::finite"
   shows "(\<forall>i. f$i = g i) \<longleftrightarrow> Cart_lambda g = f"
   by (auto simp add: Cart_eq)
 
@@ -41,13 +41,13 @@
 
 text{* A non-standard sum to "paste" Cartesian products. *}
 
-definition pastecart :: "'a ^ 'm \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ ('m + 'n)" where
+definition pastecart :: "'a ^ 'm::finite \<Rightarrow> 'a ^ 'n::finite \<Rightarrow> 'a ^ ('m + 'n)" where
   "pastecart f g = (\<chi> i. case i of Inl a \<Rightarrow> f$a | Inr b \<Rightarrow> g$b)"
 
-definition fstcart:: "'a ^('m + 'n) \<Rightarrow> 'a ^ 'm" where
+definition fstcart:: "'a ^('m::finite + 'n::finite) \<Rightarrow> 'a ^ 'm" where
   "fstcart f = (\<chi> i. (f$(Inl i)))"
 
-definition sndcart:: "'a ^('m + 'n) \<Rightarrow> 'a ^ 'n" where
+definition sndcart:: "'a ^('m::finite + 'n::finite) \<Rightarrow> 'a ^ 'n" where
   "sndcart f = (\<chi> i. (f$(Inr i)))"
 
 lemma nth_pastecart_Inl [simp]: "pastecart f g $ Inl a = f$a"
@@ -65,10 +65,10 @@
 lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \<union> range Inr"
 by (auto, case_tac x, auto)
 
-lemma fstcart_pastecart: "fstcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = x"
+lemma fstcart_pastecart: "fstcart (pastecart (x::'a ^'m::finite ) (y:: 'a ^ 'n::finite)) = x"
   by (simp add: Cart_eq)
 
-lemma sndcart_pastecart: "sndcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = y"
+lemma sndcart_pastecart: "sndcart (pastecart (x::'a ^'m::finite ) (y:: 'a ^ 'n::finite)) = y"
   by (simp add: Cart_eq)
 
 lemma pastecart_fst_snd: "pastecart (fstcart z) (sndcart z) = z"
diff -r cf455b5880e1 -r c9c14c72d035 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 07 12:24:35 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jan 06 13:07:30 2010 +0100
@@ -5563,7 +5563,7 @@
 subsection{* Some properties of a canonical subspace.                                  *}
 
 lemma subspace_substandard:
- "subspace {x::real^'n. (\<forall>i. P i \<longrightarrow> x$i = 0)}"
+ "subspace {x::real^_. (\<forall>i. P i \<longrightarrow> x$i = 0)}"
   unfolding subspace_def by(auto simp add: vector_add_component vector_smult_component elim!: ballE)
 
 lemma closed_substandard: