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