author wenzelm Wed, 28 Feb 2018 13:37:33 +0100 changeset 67731 184c293f0a33 parent 67730 f91c437f6f68 child 67732 39d80006fc29
clarified use of vec type syntax;
```--- 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"
@@ -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"
@@ -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"
@@ -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```