# HG changeset patch # User immler # Date 1519833934 -3600 # Node ID 7b0b0a02b303649475fb11d066bc675c79c6bb0c # Parent 346cb74e79f637e241dcd690915890e8a40cbabe# Parent 39d80006fc29a6ed6ec19a98660c4b67c51c6e3b merged diff -r 346cb74e79f6 -r 7b0b0a02b303 src/HOL/Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Feb 28 15:53:05 2018 +0100 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Feb 28 17:05:34 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 \ a} = {x :: (real,'n::finite) vec. x$k < a}" (is "?LE") + "interior {x. x$k \ a} = {x :: (real^'n). x$k < a}" (is "?LE") and interior_halfspace_component_ge [simp]: - "interior {x. x$k \ a} = {x :: (real,'n::finite) vec. x$k > a}" (is "?GE") + "interior {x. x$k \ a} = {x :: (real^'n). x$k > a}" (is "?GE") proof - have "axis k (1::real) \ 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 \ a}" (is "?LE") + "closure {x. x$k < a} = {x :: (real^'n). x$k \ a}" (is "?LE") and closure_halfspace_component_gt [simp]: - "closure {x. x$k > a} = {x :: (real,'n::finite) vec. x$k \ a}" (is "?GE") + "closure {x. x$k > a} = {x :: (real^'n). x$k \ a}" (is "?GE") proof - have "axis k (1::real) \ 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) \ 0" by (simp add: axis_def vec_eq_iff) @@ -773,7 +773,7 @@ assumes "\i j. abs(A$i$j) \ B" shows "onorm(( *v) A) \ 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) \ (\i\UNIV. \(A *v x) $ i\)" by (rule norm_le_l1_cart) also have "\ \ (\i::'m \UNIV. real (CARD('n)) * B * norm x)" diff -r 346cb74e79f6 -r 7b0b0a02b303 src/HOL/Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Feb 28 15:53:05 2018 +0100 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Feb 28 17:05:34 2018 +0100 @@ -15,7 +15,7 @@ subsection \Finite Cartesian products, with indexing and lambdas.\ -typedef ('a, 'b) vec = "UNIV :: (('b::finite) \ 'a) set" +typedef ('a, 'b) vec = "UNIV :: ('b::finite \ '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" -*) - -syntax "_finite_vec" :: "type \ type \ type" ("(_ ^/ _)" [15, 16] 15) - +text \ + Concrete syntax for \('a, 'b) vec\: + \<^item> \'a^'b\ becomes \('a, 'b::finite) vec\ + \<^item> \'a^'b::_\ becomes \('a, 'b) vec\ without extra sort-constraint +\ +syntax "_vec_type" :: "type \ type \ type" (infixl "^" 15) parse_translation \ let fun vec t u = Syntax.const @{type_syntax vec} $ t $ u; @@ -53,7 +52,7 @@ else vec t u | _ => vec t u) in - [(@{syntax_const "_finite_vec"}, K finite_vec_tr)] + [(@{syntax_const "_vec_type"}, K finite_vec_tr)] end \ @@ -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) (\_. 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 \ ('a, 'b) vec) filter) = + "(uniformity :: (('a^'b::_) \ ('a^'b::_)) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})" instance