# HG changeset patch
# User wenzelm
# Date 1519821453 -3600
# Node ID 184c293f0a33924623b4f2c88d0318fe72707ef4
# Parent  f91c437f6f6893ea911a4fde572cbf94524b7f64
clarified use of vec type syntax;

diff -r f91c437f6f68 -r 184c293f0a33 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Feb 26 11:52:53 2018 +0000
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Feb 28 13:37:33 2018 +0100
@@ -360,9 +360,9 @@
 using interior_halfspace_le [of "-a" "-b"] by simp
 
 lemma interior_halfspace_component_le [simp]:
-     "interior {x. x$k \<le> a} = {x :: (real,'n::finite) vec. x$k < a}" (is "?LE")
+     "interior {x. x$k \<le> a} = {x :: (real^'n). x$k < a}" (is "?LE")
   and interior_halfspace_component_ge [simp]:
-     "interior {x. x$k \<ge> a} = {x :: (real,'n::finite) vec. x$k > a}" (is "?GE")
+     "interior {x. x$k \<ge> a} = {x :: (real^'n). x$k > a}" (is "?GE")
 proof -
   have "axis k (1::real) \<noteq> 0"
     by (simp add: axis_def vec_eq_iff)
@@ -389,9 +389,9 @@
 using closure_halfspace_lt [of "-a" "-b"] by simp
 
 lemma closure_halfspace_component_lt [simp]:
-     "closure {x. x$k < a} = {x :: (real,'n::finite) vec. x$k \<le> a}" (is "?LE")
+     "closure {x. x$k < a} = {x :: (real^'n). x$k \<le> a}" (is "?LE")
   and closure_halfspace_component_gt [simp]:
-     "closure {x. x$k > a} = {x :: (real,'n::finite) vec. x$k \<ge> a}" (is "?GE")
+     "closure {x. x$k > a} = {x :: (real^'n). x$k \<ge> a}" (is "?GE")
 proof -
   have "axis k (1::real) \<noteq> 0"
     by (simp add: axis_def vec_eq_iff)
@@ -453,7 +453,7 @@
 qed
 
 lemma interior_standard_hyperplane:
-   "interior {x :: (real,'n::finite) vec. x$k = a} = {}"
+   "interior {x :: (real^'n). x$k = a} = {}"
 proof -
   have "axis k (1::real) \<noteq> 0"
     by (simp add: axis_def vec_eq_iff)
@@ -773,7 +773,7 @@
   assumes "\<And>i j. abs(A$i$j) \<le> B"
   shows "onorm(( *v) A) \<le> real (CARD('m)) * real (CARD('n)) * B"
 proof (rule onorm_le)
-  fix x :: "(real, 'n) vec"
+  fix x :: "real^'n::_"
   have "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<bar>(A *v x) $ i\<bar>)"
     by (rule norm_le_l1_cart)
   also have "\<dots> \<le> (\<Sum>i::'m \<in>UNIV. real (CARD('n)) * B * norm x)"
diff -r f91c437f6f68 -r 184c293f0a33 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Mon Feb 26 11:52:53 2018 +0000
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Feb 28 13:37:33 2018 +0100
@@ -15,7 +15,7 @@
 
 subsection \<open>Finite Cartesian products, with indexing and lambdas.\<close>
 
-typedef ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
+typedef ('a, 'b) vec = "UNIV :: ('b::finite \<Rightarrow> 'a) set"
   morphisms vec_nth vec_lambda ..
 
 declare vec_lambda_inject [simplified, simp]
@@ -34,13 +34,12 @@
 
 unbundle vec_syntax
 
-(*
-  Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than
-  the finite type class write "vec 'b 'n"
-*)
-
+text \<open>
+  Concrete syntax for \<open>('a, 'b) vec\<close>:
+    \<^item> \<open>'a^'b\<close> becomes \<open>('a, 'b::finite) vec\<close>
+    \<^item> \<open>'a^'b::_\<close> becomes \<open>('a, 'b) vec\<close> without extra sort-constraint
+\<close>
 syntax "_finite_vec" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15)
-
 parse_translation \<open>
   let
     fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
@@ -107,7 +106,7 @@
 
 lemma infinite_UNIV_vec:
   assumes "infinite (UNIV :: 'a set)"
-  shows   "infinite (UNIV :: ('a, 'b :: finite) vec set)"
+  shows   "infinite (UNIV :: ('a^'b) set)"
 proof (subst bij_betw_finite)
   show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
     by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff)
@@ -127,7 +126,7 @@
 qed
 
 lemma CARD_vec [simp]:
-  "CARD(('a,'b::finite) vec) = CARD('a) ^ CARD('b)"
+  "CARD('a^'b) = CARD('a) ^ CARD('b)"
 proof (cases "finite (UNIV :: 'a set)")
   case True
   show ?thesis
@@ -385,7 +384,7 @@
 begin
 
 definition [code del]:
-  "(uniformity :: (('a, 'b) vec \<times> ('a, 'b) vec) filter) =
+  "(uniformity :: (('a^'b::_) \<times> ('a^'b::_)) filter) =
     (INF e:{0 <..}. principal {(x, y). dist x y < e})"
 
 instance