src/HOL/Analysis/Finite_Cartesian_Product.thy
author nipkow
Mon, 17 Oct 2016 11:46:22 +0200
changeset 64267 b9a1486e79be
parent 63918 6bf55e6e0b75
child 66281 6ad54b84ca5d
permissions -rw-r--r--
setsum -> sum
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63627
6ddb43c6b711 rename HOL-Multivariate_Analysis to HOL-Analysis.
hoelzl
parents: 63040
diff changeset
     1
(*  Title:      HOL/Analysis/Finite_Cartesian_Product.thy
35253
68dd8b51c6b8 tuned headers;
wenzelm
parents: 35113
diff changeset
     2
    Author:     Amine Chaieb, University of Cambridge
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     3
*)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     4
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
     5
section \<open>Definition of finite Cartesian product types.\<close>
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     6
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     7
theory Finite_Cartesian_Product
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 39302
diff changeset
     8
imports
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
     9
  Euclidean_Space
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 39302
diff changeset
    10
  L2_Norm
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 39302
diff changeset
    11
  "~~/src/HOL/Library/Numeral_Type"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    12
begin
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    13
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
    14
subsection \<open>Finite Cartesian products, with indexing and lambdas.\<close>
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    15
49834
b27bbb021df1 discontinued obsolete typedef (open) syntax;
wenzelm
parents: 49674
diff changeset
    16
typedef ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    17
  morphisms vec_nth vec_lambda ..
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    18
35254
0f17eda72e60 binder notation for default print_mode -- to avoid strange output if "xsymbols" is not active;
wenzelm
parents: 35253
diff changeset
    19
notation
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    20
  vec_nth (infixl "$" 90) and
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    21
  vec_lambda (binder "\<chi>" 10)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    22
34290
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    23
(*
34291
4e896680897e finite annotation on cartesian product is now implicit.
hoelzl
parents: 34290
diff changeset
    24
  Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    25
  the finite type class write "vec 'b 'n"
34290
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    26
*)
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    27
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    28
syntax "_finite_vec" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15)
34290
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    29
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
    30
parse_translation \<open>
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51002
diff changeset
    31
  let
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51002
diff changeset
    32
    fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51002
diff changeset
    33
    fun finite_vec_tr [t, u] =
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51002
diff changeset
    34
      (case Term_Position.strip_positions u of
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51002
diff changeset
    35
        v as Free (x, _) =>
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51002
diff changeset
    36
          if Lexicon.is_tid x then
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51002
diff changeset
    37
            vec t (Syntax.const @{syntax_const "_ofsort"} $ v $
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51002
diff changeset
    38
              Syntax.const @{class_syntax finite})
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51002
diff changeset
    39
          else vec t u
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51002
diff changeset
    40
      | _ => vec t u)
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51002
diff changeset
    41
  in
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51002
diff changeset
    42
    [(@{syntax_const "_finite_vec"}, K finite_vec_tr)]
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51002
diff changeset
    43
  end
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
    44
\<close>
34290
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    45
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    46
lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    47
  by (simp add: vec_nth_inject [symmetric] fun_eq_iff)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    48
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    49
lemma vec_lambda_beta [simp]: "vec_lambda g $ i = g i"
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    50
  by (simp add: vec_lambda_inverse)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    51
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    52
lemma vec_lambda_unique: "(\<forall>i. f$i = g i) \<longleftrightarrow> vec_lambda g = f"
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    53
  by (auto simp add: vec_eq_iff)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    54
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    55
lemma vec_lambda_eta: "(\<chi> i. (g$i)) = g"
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    56
  by (simp add: vec_eq_iff)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    57
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    58
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
    59
subsection \<open>Group operations and class instances\<close>
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    60
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    61
instantiation vec :: (zero, finite) zero
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    62
begin
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    63
  definition "0 \<equiv> (\<chi> i. 0)"
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    64
  instance ..
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    65
end
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    66
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    67
instantiation vec :: (plus, finite) plus
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    68
begin
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    69
  definition "op + \<equiv> (\<lambda> x y. (\<chi> i. x$i + y$i))"
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    70
  instance ..
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    71
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    72
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    73
instantiation vec :: (minus, finite) minus
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    74
begin
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    75
  definition "op - \<equiv> (\<lambda> x y. (\<chi> i. x$i - y$i))"
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    76
  instance ..
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    77
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    78
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    79
instantiation vec :: (uminus, finite) uminus
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    80
begin
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    81
  definition "uminus \<equiv> (\<lambda> x. (\<chi> i. - (x$i)))"
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    82
  instance ..
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    83
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    84
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    85
lemma zero_index [simp]: "0 $ i = 0"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    86
  unfolding zero_vec_def by simp
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    87
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    88
lemma vector_add_component [simp]: "(x + y)$i = x$i + y$i"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    89
  unfolding plus_vec_def by simp
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    90
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    91
lemma vector_minus_component [simp]: "(x - y)$i = x$i - y$i"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    92
  unfolding minus_vec_def by simp
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    93
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    94
lemma vector_uminus_component [simp]: "(- x)$i = - (x$i)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    95
  unfolding uminus_vec_def by simp
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    96
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    97
instance vec :: (semigroup_add, finite) semigroup_add
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 60420
diff changeset
    98
  by standard (simp add: vec_eq_iff add.assoc)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    99
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   100
instance vec :: (ab_semigroup_add, finite) ab_semigroup_add
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 60420
diff changeset
   101
  by standard (simp add: vec_eq_iff add.commute)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   102
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   103
instance vec :: (monoid_add, finite) monoid_add
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 60420
diff changeset
   104
  by standard (simp_all add: vec_eq_iff)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   105
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   106
instance vec :: (comm_monoid_add, finite) comm_monoid_add
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 60420
diff changeset
   107
  by standard (simp add: vec_eq_iff)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   108
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   109
instance vec :: (cancel_semigroup_add, finite) cancel_semigroup_add
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 60420
diff changeset
   110
  by standard (simp_all add: vec_eq_iff)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   111
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   112
instance vec :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 60420
diff changeset
   113
  by standard (simp_all add: vec_eq_iff diff_diff_eq)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   114
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   115
instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   116
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   117
instance vec :: (group_add, finite) group_add
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 60420
diff changeset
   118
  by standard (simp_all add: vec_eq_iff)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   119
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   120
instance vec :: (ab_group_add, finite) ab_group_add
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 60420
diff changeset
   121
  by standard (simp_all add: vec_eq_iff)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   122
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   123
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
   124
subsection \<open>Real vector space\<close>
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   125
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   126
instantiation vec :: (real_vector, finite) real_vector
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   127
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   128
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   129
definition "scaleR \<equiv> (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   130
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   131
lemma vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   132
  unfolding scaleR_vec_def by simp
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   133
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   134
instance
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 60420
diff changeset
   135
  by standard (simp_all add: vec_eq_iff scaleR_left_distrib scaleR_right_distrib)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   136
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   137
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   138
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   139
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
   140
subsection \<open>Topological space\<close>
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   141
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   142
instantiation vec :: (topological_space, finite) topological_space
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   143
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   144
62101
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   145
definition [code del]:
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   146
  "open (S :: ('a ^ 'b) set) \<longleftrightarrow>
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   147
    (\<forall>x\<in>S. \<exists>A. (\<forall>i. open (A i) \<and> x$i \<in> A i) \<and>
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   148
      (\<forall>y. (\<forall>i. y$i \<in> A i) \<longrightarrow> y \<in> S))"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   149
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   150
instance proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   151
  show "open (UNIV :: ('a ^ 'b) set)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   152
    unfolding open_vec_def by auto
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   153
next
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   154
  fix S T :: "('a ^ 'b) set"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   155
  assume "open S" "open T" thus "open (S \<inter> T)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   156
    unfolding open_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   157
    apply clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   158
    apply (drule (1) bspec)+
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   159
    apply (clarify, rename_tac Sa Ta)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   160
    apply (rule_tac x="\<lambda>i. Sa i \<inter> Ta i" in exI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   161
    apply (simp add: open_Int)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   162
    done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   163
next
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   164
  fix K :: "('a ^ 'b) set set"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   165
  assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   166
    unfolding open_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   167
    apply clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   168
    apply (drule (1) bspec)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   169
    apply (drule (1) bspec)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   170
    apply clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   171
    apply (rule_tac x=A in exI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   172
    apply fast
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   173
    done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   174
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   175
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   176
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   177
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   178
lemma open_vector_box: "\<forall>i. open (S i) \<Longrightarrow> open {x. \<forall>i. x $ i \<in> S i}"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   179
  unfolding open_vec_def by auto
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   180
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   181
lemma open_vimage_vec_nth: "open S \<Longrightarrow> open ((\<lambda>x. x $ i) -` S)"
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   182
  unfolding open_vec_def
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   183
  apply clarify
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   184
  apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp)
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   185
  done
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   186
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   187
lemma closed_vimage_vec_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) -` S)"
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   188
  unfolding closed_open vimage_Compl [symmetric]
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   189
  by (rule open_vimage_vec_nth)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   190
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   191
lemma closed_vector_box: "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   192
proof -
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   193
  have "{x. \<forall>i. x $ i \<in> S i} = (\<Inter>i. (\<lambda>x. x $ i) -` S i)" by auto
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   194
  thus "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   195
    by (simp add: closed_INT closed_vimage_vec_nth)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   196
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   197
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   198
lemma tendsto_vec_nth [tendsto_intros]:
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   199
  assumes "((\<lambda>x. f x) \<longlongrightarrow> a) net"
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   200
  shows "((\<lambda>x. f x $ i) \<longlongrightarrow> a $ i) net"
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   201
proof (rule topological_tendstoI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   202
  fix S assume "open S" "a $ i \<in> S"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   203
  then have "open ((\<lambda>y. y $ i) -` S)" "a \<in> ((\<lambda>y. y $ i) -` S)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   204
    by (simp_all add: open_vimage_vec_nth)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   205
  with assms have "eventually (\<lambda>x. f x \<in> (\<lambda>y. y $ i) -` S) net"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   206
    by (rule topological_tendstoD)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   207
  then show "eventually (\<lambda>x. f x $ i \<in> S) net"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   208
    by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   209
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   210
44631
6820684c7a58 generalize lemma isCont_vec_nth
huffman
parents: 44630
diff changeset
   211
lemma isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a"
6820684c7a58 generalize lemma isCont_vec_nth
huffman
parents: 44630
diff changeset
   212
  unfolding isCont_def by (rule tendsto_vec_nth)
6820684c7a58 generalize lemma isCont_vec_nth
huffman
parents: 44630
diff changeset
   213
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   214
lemma vec_tendstoI:
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   215
  assumes "\<And>i. ((\<lambda>x. f x $ i) \<longlongrightarrow> a $ i) net"
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   216
  shows "((\<lambda>x. f x) \<longlongrightarrow> a) net"
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   217
proof (rule topological_tendstoI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   218
  fix S assume "open S" and "a \<in> S"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   219
  then obtain A where A: "\<And>i. open (A i)" "\<And>i. a $ i \<in> A i"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   220
    and S: "\<And>y. \<forall>i. y $ i \<in> A i \<Longrightarrow> y \<in> S"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   221
    unfolding open_vec_def by metis
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   222
  have "\<And>i. eventually (\<lambda>x. f x $ i \<in> A i) net"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   223
    using assms A by (rule topological_tendstoD)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   224
  hence "eventually (\<lambda>x. \<forall>i. f x $ i \<in> A i) net"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   225
    by (rule eventually_all_finite)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   226
  thus "eventually (\<lambda>x. f x \<in> S) net"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61169
diff changeset
   227
    by (rule eventually_mono, simp add: S)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   228
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   229
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   230
lemma tendsto_vec_lambda [tendsto_intros]:
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   231
  assumes "\<And>i. ((\<lambda>x. f x i) \<longlongrightarrow> a i) net"
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   232
  shows "((\<lambda>x. \<chi> i. f x i) \<longlongrightarrow> (\<chi> i. a i)) net"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   233
  using assms by (simp add: vec_tendstoI)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   234
44571
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   235
lemma open_image_vec_nth: assumes "open S" shows "open ((\<lambda>x. x $ i) ` S)"
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   236
proof (rule openI)
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   237
  fix a assume "a \<in> (\<lambda>x. x $ i) ` S"
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   238
  then obtain z where "a = z $ i" and "z \<in> S" ..
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   239
  then obtain A where A: "\<forall>i. open (A i) \<and> z $ i \<in> A i"
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   240
    and S: "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
   241
    using \<open>open S\<close> unfolding open_vec_def by auto
44571
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   242
  hence "A i \<subseteq> (\<lambda>x. x $ i) ` S"
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   243
    by (clarsimp, rule_tac x="\<chi> j. if j = i then x else z $ j" in image_eqI,
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   244
      simp_all)
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   245
  hence "open (A i) \<and> a \<in> A i \<and> A i \<subseteq> (\<lambda>x. x $ i) ` S"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
   246
    using A \<open>a = z $ i\<close> by simp
44571
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   247
  then show "\<exists>T. open T \<and> a \<in> T \<and> T \<subseteq> (\<lambda>x. x $ i) ` S" by - (rule exI)
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   248
qed
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   249
44571
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   250
instance vec :: (perfect_space, finite) perfect_space
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   251
proof
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   252
  fix x :: "'a ^ 'b" show "\<not> open {x}"
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   253
  proof
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   254
    assume "open {x}"
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   255
    hence "\<forall>i. open ((\<lambda>x. x $ i) ` {x})" by (fast intro: open_image_vec_nth)
44571
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   256
    hence "\<forall>i. open {x $ i}" by simp
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   257
    thus "False" by (simp add: not_open_singleton)
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   258
  qed
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   259
qed
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   260
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   261
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
   262
subsection \<open>Metric space\<close>
62101
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   263
(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   264
62101
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   265
instantiation vec :: (metric_space, finite) dist
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   266
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   267
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   268
definition
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   269
  "dist x y = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   270
62101
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   271
instance ..
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   272
end
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   273
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   274
instantiation vec :: (metric_space, finite) uniformity_dist
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   275
begin
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   276
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   277
definition [code del]:
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   278
  "(uniformity :: (('a, 'b) vec \<times> ('a, 'b) vec) filter) =
62101
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   279
    (INF e:{0 <..}. principal {(x, y). dist x y < e})"
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   280
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   281
instance
62101
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   282
  by standard (rule uniformity_vec_def)
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   283
end
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   284
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   285
declare uniformity_Abort[where 'a="'a :: metric_space ^ 'b :: finite", code]
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   286
62101
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   287
instantiation vec :: (metric_space, finite) metric_space
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   288
begin
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   289
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   290
lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   291
  unfolding dist_vec_def by (rule member_le_setL2) simp_all
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   292
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   293
instance proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   294
  fix x y :: "'a ^ 'b"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   295
  show "dist x y = 0 \<longleftrightarrow> x = y"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   296
    unfolding dist_vec_def
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   297
    by (simp add: setL2_eq_0_iff vec_eq_iff)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   298
next
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   299
  fix x y z :: "'a ^ 'b"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   300
  show "dist x y \<le> dist x z + dist y z"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   301
    unfolding dist_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   302
    apply (rule order_trans [OF _ setL2_triangle_ineq])
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   303
    apply (simp add: setL2_mono dist_triangle2)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   304
    done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   305
next
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   306
  fix S :: "('a ^ 'b) set"
62101
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   307
  have *: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
44630
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   308
  proof
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   309
    assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   310
    proof
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   311
      fix x assume "x \<in> S"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   312
      obtain A where A: "\<forall>i. open (A i)" "\<forall>i. x $ i \<in> A i"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   313
        and S: "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
   314
        using \<open>open S\<close> and \<open>x \<in> S\<close> unfolding open_vec_def by metis
44630
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   315
      have "\<forall>i\<in>UNIV. \<exists>r>0. \<forall>y. dist y (x $ i) < r \<longrightarrow> y \<in> A i"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   316
        using A unfolding open_dist by simp
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   317
      hence "\<exists>r. \<forall>i\<in>UNIV. 0 < r i \<and> (\<forall>y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i)"
44681
49ef76b4a634 remove duplicate lemma finite_choice in favor of finite_set_choice
huffman
parents: 44631
diff changeset
   318
        by (rule finite_set_choice [OF finite])
44630
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   319
      then obtain r where r1: "\<forall>i. 0 < r i"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   320
        and r2: "\<forall>i y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i" by fast
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   321
      have "0 < Min (range r) \<and> (\<forall>y. dist y x < Min (range r) \<longrightarrow> y \<in> S)"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   322
        by (simp add: r1 r2 S le_less_trans [OF dist_vec_nth_le])
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   323
      thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" ..
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   324
    qed
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   325
  next
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   326
    assume *: "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" show "open S"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   327
    proof (unfold open_vec_def, rule)
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   328
      fix x assume "x \<in> S"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   329
      then obtain e where "0 < e" and S: "\<forall>y. dist y x < e \<longrightarrow> y \<in> S"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   330
        using * by fast
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62397
diff changeset
   331
      define r where [abs_def]: "r i = e / sqrt (of_nat CARD('b))" for i :: 'b
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
   332
      from \<open>0 < e\<close> have r: "\<forall>i. 0 < r i"
56541
0e3abadbef39 made divide_pos_pos a simp rule
nipkow
parents: 54230
diff changeset
   333
        unfolding r_def by simp_all
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
   334
      from \<open>0 < e\<close> have e: "e = setL2 r UNIV"
44630
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   335
        unfolding r_def by (simp add: setL2_constant)
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62397
diff changeset
   336
      define A where "A i = {y. dist (x $ i) y < r i}" for i
44630
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   337
      have "\<forall>i. open (A i) \<and> x $ i \<in> A i"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   338
        unfolding A_def by (simp add: open_ball r)
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   339
      moreover have "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   340
        by (simp add: A_def S dist_vec_def e setL2_strict_mono dist_commute)
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   341
      ultimately show "\<exists>A. (\<forall>i. open (A i) \<and> x $ i \<in> A i) \<and>
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   342
        (\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S)" by metis
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   343
    qed
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   344
  qed
62101
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   345
  show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   346
    unfolding * eventually_uniformity_metric
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61973
diff changeset
   347
    by (simp del: split_paired_All add: dist_vec_def dist_commute)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   348
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   349
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   350
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   351
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   352
lemma Cauchy_vec_nth:
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   353
  "Cauchy (\<lambda>n. X n) \<Longrightarrow> Cauchy (\<lambda>n. X n $ i)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   354
  unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_vec_nth_le])
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   355
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   356
lemma vec_CauchyI:
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   357
  fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   358
  assumes X: "\<And>i. Cauchy (\<lambda>n. X n $ i)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   359
  shows "Cauchy (\<lambda>n. X n)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   360
proof (rule metric_CauchyI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   361
  fix r :: real assume "0 < r"
56541
0e3abadbef39 made divide_pos_pos a simp rule
nipkow
parents: 54230
diff changeset
   362
  hence "0 < r / of_nat CARD('n)" (is "0 < ?s") by simp
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62397
diff changeset
   363
  define N where "N i = (LEAST N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s)" for i
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62397
diff changeset
   364
  define M where "M = Max (range N)"
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   365
  have "\<And>i. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
   366
    using X \<open>0 < ?s\<close> by (rule metric_CauchyD)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   367
  hence "\<And>i. \<forall>m\<ge>N i. \<forall>n\<ge>N i. dist (X m $ i) (X n $ i) < ?s"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   368
    unfolding N_def by (rule LeastI_ex)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   369
  hence M: "\<And>i. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m $ i) (X n $ i) < ?s"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   370
    unfolding M_def by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   371
  {
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   372
    fix m n :: nat
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   373
    assume "M \<le> m" "M \<le> n"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   374
    have "dist (X m) (X n) = setL2 (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   375
      unfolding dist_vec_def ..
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
   376
    also have "\<dots> \<le> sum (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
   377
      by (rule setL2_le_sum [OF zero_le_dist])
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
   378
    also have "\<dots> < sum (\<lambda>i::'n. ?s) UNIV"
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
   379
      by (rule sum_strict_mono, simp_all add: M \<open>M \<le> m\<close> \<open>M \<le> n\<close>)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   380
    also have "\<dots> = r"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   381
      by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   382
    finally have "dist (X m) (X n) < r" .
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   383
  }
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   384
  hence "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   385
    by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   386
  then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" ..
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   387
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   388
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   389
instance vec :: (complete_space, finite) complete_space
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   390
proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   391
  fix X :: "nat \<Rightarrow> 'a ^ 'b" assume "Cauchy X"
61969
e01015e49041 more symbols;
wenzelm
parents: 61810
diff changeset
   392
  have "\<And>i. (\<lambda>n. X n $ i) \<longlonglongrightarrow> lim (\<lambda>n. X n $ i)"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
   393
    using Cauchy_vec_nth [OF \<open>Cauchy X\<close>]
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   394
    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
61969
e01015e49041 more symbols;
wenzelm
parents: 61810
diff changeset
   395
  hence "X \<longlonglongrightarrow> vec_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   396
    by (simp add: vec_tendstoI)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   397
  then show "convergent X"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   398
    by (rule convergentI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   399
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   400
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   401
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
   402
subsection \<open>Normed vector space\<close>
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   403
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   404
instantiation vec :: (real_normed_vector, finite) real_normed_vector
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   405
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   406
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   407
definition "norm x = setL2 (\<lambda>i. norm (x$i)) UNIV"
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   408
44141
0697c01ff3ea follow standard naming scheme for sgn_vec_def
huffman
parents: 44136
diff changeset
   409
definition "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   410
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   411
instance proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   412
  fix a :: real and x y :: "'a ^ 'b"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   413
  show "norm x = 0 \<longleftrightarrow> x = 0"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   414
    unfolding norm_vec_def
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   415
    by (simp add: setL2_eq_0_iff vec_eq_iff)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   416
  show "norm (x + y) \<le> norm x + norm y"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   417
    unfolding norm_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   418
    apply (rule order_trans [OF _ setL2_triangle_ineq])
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   419
    apply (simp add: setL2_mono norm_triangle_ineq)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   420
    done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   421
  show "norm (scaleR a x) = \<bar>a\<bar> * norm x"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   422
    unfolding norm_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   423
    by (simp add: setL2_right_distrib)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   424
  show "sgn x = scaleR (inverse (norm x)) x"
44141
0697c01ff3ea follow standard naming scheme for sgn_vec_def
huffman
parents: 44136
diff changeset
   425
    by (rule sgn_vec_def)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   426
  show "dist x y = norm (x - y)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   427
    unfolding dist_vec_def norm_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   428
    by (simp add: dist_norm)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   429
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   430
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   431
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   432
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   433
lemma norm_nth_le: "norm (x $ i) \<le> norm x"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   434
unfolding norm_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   435
by (rule member_le_setL2) simp_all
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   436
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
   437
lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 60420
diff changeset
   438
apply standard
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   439
apply (rule vector_add_component)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   440
apply (rule vector_scaleR_component)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   441
apply (rule_tac x="1" in exI, simp add: norm_nth_le)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   442
done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   443
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   444
instance vec :: (banach, finite) banach ..
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   445
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   446
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
   447
subsection \<open>Inner product space\<close>
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   448
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   449
instantiation vec :: (real_inner, finite) real_inner
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   450
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   451
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
   452
definition "inner x y = sum (\<lambda>i. inner (x$i) (y$i)) UNIV"
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   453
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   454
instance proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   455
  fix r :: real and x y z :: "'a ^ 'b"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   456
  show "inner x y = inner y x"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   457
    unfolding inner_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   458
    by (simp add: inner_commute)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   459
  show "inner (x + y) z = inner x z + inner y z"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   460
    unfolding inner_vec_def
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
   461
    by (simp add: inner_add_left sum.distrib)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   462
  show "inner (scaleR r x) y = r * inner x y"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   463
    unfolding inner_vec_def
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
   464
    by (simp add: sum_distrib_left)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   465
  show "0 \<le> inner x x"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   466
    unfolding inner_vec_def
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
   467
    by (simp add: sum_nonneg)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   468
  show "inner x x = 0 \<longleftrightarrow> x = 0"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   469
    unfolding inner_vec_def
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
   470
    by (simp add: vec_eq_iff sum_nonneg_eq_0_iff)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   471
  show "norm x = sqrt (inner x x)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   472
    unfolding inner_vec_def norm_vec_def setL2_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   473
    by (simp add: power2_norm_eq_inner)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   474
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   475
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   476
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   477
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   478
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
   479
subsection \<open>Euclidean space\<close>
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   480
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59815
diff changeset
   481
text \<open>Vectors pointing along a single axis.\<close>
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   482
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   483
definition "axis k x = (\<chi> i. if i = k then x else 0)"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   484
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   485
lemma axis_nth [simp]: "axis i x $ i = x"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   486
  unfolding axis_def by simp
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   487
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   488
lemma axis_eq_axis: "axis i x = axis j y \<longleftrightarrow> x = y \<and> i = j \<or> x = 0 \<and> y = 0"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   489
  unfolding axis_def vec_eq_iff by auto
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   490
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   491
lemma inner_axis_axis:
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   492
  "inner (axis i x) (axis j y) = (if i = j then inner x y else 0)"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   493
  unfolding inner_vec_def
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   494
  apply (cases "i = j")
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   495
  apply clarsimp
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
   496
  apply (subst sum.remove [of _ j], simp_all)
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
   497
  apply (rule sum.neutral, simp add: axis_def)
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
   498
  apply (rule sum.neutral, simp add: axis_def)
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   499
  done
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   500
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
   501
lemma sum_single:
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   502
  assumes "finite A" and "k \<in> A" and "f k = y"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   503
  assumes "\<And>i. i \<in> A \<Longrightarrow> i \<noteq> k \<Longrightarrow> f i = 0"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   504
  shows "(\<Sum>i\<in>A. f i) = y"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
   505
  apply (subst sum.remove [OF assms(1,2)])
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
   506
  apply (simp add: sum.neutral assms(3,4))
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   507
  done
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   508
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   509
lemma inner_axis: "inner x (axis i y) = inner (x $ i) y"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   510
  unfolding inner_vec_def
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
   511
  apply (rule_tac k=i in sum_single)
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   512
  apply simp_all
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   513
  apply (simp add: axis_def)
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   514
  done
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   515
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   516
instantiation vec :: (euclidean_space, finite) euclidean_space
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   517
begin
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   518
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   519
definition "Basis = (\<Union>i. \<Union>u\<in>Basis. {axis i u})"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   520
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   521
instance proof
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   522
  show "(Basis :: ('a ^ 'b) set) \<noteq> {}"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   523
    unfolding Basis_vec_def by simp
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   524
next
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   525
  show "finite (Basis :: ('a ^ 'b) set)"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   526
    unfolding Basis_vec_def by simp
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   527
next
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   528
  fix u v :: "'a ^ 'b"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   529
  assume "u \<in> Basis" and "v \<in> Basis"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   530
  thus "inner u v = (if u = v then 1 else 0)"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   531
    unfolding Basis_vec_def
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   532
    by (auto simp add: inner_axis_axis axis_eq_axis inner_Basis)
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   533
next
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   534
  fix x :: "'a ^ 'b"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   535
  show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   536
    unfolding Basis_vec_def
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   537
    by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50252
diff changeset
   538
qed
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50252
diff changeset
   539
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50252
diff changeset
   540
lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50252
diff changeset
   541
  apply (simp add: Basis_vec_def)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50252
diff changeset
   542
  apply (subst card_UN_disjoint)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50252
diff changeset
   543
     apply simp
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   544
    apply simp
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50252
diff changeset
   545
   apply (auto simp: axis_eq_axis) [1]
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50252
diff changeset
   546
  apply (subst card_UN_disjoint)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50252
diff changeset
   547
     apply (auto simp: axis_eq_axis)
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50252
diff changeset
   548
  done
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   549
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   550
end
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   551
62397
5ae24f33d343 Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents: 62102
diff changeset
   552
lemma cart_eq_inner_axis: "a $ i = inner a (axis i 1)"
5ae24f33d343 Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents: 62102
diff changeset
   553
  by (simp add: inner_axis)
5ae24f33d343 Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents: 62102
diff changeset
   554
5ae24f33d343 Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents: 62102
diff changeset
   555
lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis"
5ae24f33d343 Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents: 62102
diff changeset
   556
  by (auto simp add: Basis_vec_def axis_eq_axis)
5ae24f33d343 Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents: 62102
diff changeset
   557
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   558
end