src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
author blanchet
Fri, 01 Aug 2014 14:43:57 +0200
changeset 57743 0af2d5dfb0ac
parent 57512 cc97b347b301
child 58877 262572d90bc6
permissions -rw-r--r--
pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35253
68dd8b51c6b8 tuned headers;
wenzelm
parents: 35113
diff changeset
     1
(*  Title:      HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
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
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     5
header {* Definition of finite Cartesian product types. *}
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
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    14
subsection {* Finite Cartesian products, with indexing and lambdas. *}
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
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    30
parse_translation {*
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
34290
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    44
*}
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
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    59
subsection {* Group operations and class instances *}
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
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57418
diff changeset
    98
  by default (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
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57418
diff changeset
   101
  by default (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
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   104
  by default (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
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   107
  by default (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
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   110
  by default (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
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   113
  by default (simp add: vec_eq_iff)
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
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 52143
diff changeset
   118
  by default (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
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   121
  by default (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
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   124
subsection {* Real vector space *}
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
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   135
  by default (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
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   140
subsection {* Topological space *}
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
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   145
definition
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]:
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   199
  assumes "((\<lambda>x. f x) ---> a) net"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   200
  shows "((\<lambda>x. f x $ i) ---> a $ i) net"
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:
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   215
  assumes "\<And>i. ((\<lambda>x. f x $ i) ---> a $ i) net"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   216
  shows "((\<lambda>x. f x) ---> a) net"
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"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   227
    by (rule eventually_elim1, simp add: S)
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]:
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   231
  assumes "\<And>i. ((\<lambda>x. f x i) ---> a i) net"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   232
  shows "((\<lambda>x. \<chi> i. f x i) ---> (\<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"
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   241
    using `open S` unfolding open_vec_def by auto
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"
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   246
    using A `a = z $ i` by simp
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}"
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   255
    hence "\<forall>i. open ((\<lambda>x. x $ i) ` {x})" by (fast intro: open_image_vec_nth)   
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
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   262
subsection {* Metric space *}
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   263
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   264
instantiation vec :: (metric_space, finite) metric_space
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   265
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   266
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   267
definition
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   268
  "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
   269
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   270
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
   271
  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
   272
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   273
instance proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   274
  fix x y :: "'a ^ 'b"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   275
  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
   276
    unfolding dist_vec_def
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   277
    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
   278
next
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   279
  fix x y z :: "'a ^ 'b"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   280
  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
   281
    unfolding dist_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   282
    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
   283
    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
   284
    done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   285
next
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   286
  fix S :: "('a ^ 'b) set"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   287
  show "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
   288
  proof
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   289
    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
   290
    proof
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   291
      fix x assume "x \<in> S"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   292
      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
   293
        and S: "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   294
        using `open S` and `x \<in> S` unfolding open_vec_def by metis
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   295
      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
   296
        using A unfolding open_dist by simp
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   297
      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
   298
        by (rule finite_set_choice [OF finite])
44630
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   299
      then obtain r where r1: "\<forall>i. 0 < r i"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   300
        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
   301
      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
   302
        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
   303
      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
   304
    qed
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   305
  next
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   306
    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
   307
    proof (unfold open_vec_def, rule)
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   308
      fix x assume "x \<in> S"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   309
      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
   310
        using * by fast
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   311
      def r \<equiv> "\<lambda>i::'b. e / sqrt (of_nat CARD('b))"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   312
      from `0 < e` have r: "\<forall>i. 0 < r i"
56541
0e3abadbef39 made divide_pos_pos a simp rule
nipkow
parents: 54230
diff changeset
   313
        unfolding r_def by simp_all
44630
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   314
      from `0 < e` have e: "e = setL2 r UNIV"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   315
        unfolding r_def by (simp add: setL2_constant)
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   316
      def A \<equiv> "\<lambda>i. {y. dist (x $ i) y < r i}"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   317
      have "\<forall>i. open (A i) \<and> x $ i \<in> A i"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   318
        unfolding A_def by (simp add: open_ball r)
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   319
      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
   320
        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
   321
      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
   322
        (\<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
   323
    qed
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   324
  qed
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   325
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   326
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   327
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   328
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   329
lemma Cauchy_vec_nth:
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   330
  "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
   331
  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
   332
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   333
lemma vec_CauchyI:
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   334
  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
   335
  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
   336
  shows "Cauchy (\<lambda>n. X n)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   337
proof (rule metric_CauchyI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   338
  fix r :: real assume "0 < r"
56541
0e3abadbef39 made divide_pos_pos a simp rule
nipkow
parents: 54230
diff changeset
   339
  hence "0 < r / of_nat CARD('n)" (is "0 < ?s") by simp
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   340
  def N \<equiv> "\<lambda>i. LEAST N. \<forall>m\<ge>N. \<forall>n\<ge>N. 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
   341
  def M \<equiv> "Max (range N)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   342
  have "\<And>i. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. 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
   343
    using X `0 < ?s` by (rule metric_CauchyD)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   344
  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
   345
    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
   346
  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
   347
    unfolding M_def by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   348
  {
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   349
    fix m n :: nat
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   350
    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
   351
    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
   352
      unfolding dist_vec_def ..
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   353
    also have "\<dots> \<le> setsum (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   354
      by (rule setL2_le_setsum [OF zero_le_dist])
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   355
    also have "\<dots> < setsum (\<lambda>i::'n. ?s) UNIV"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   356
      by (rule setsum_strict_mono, simp_all add: M `M \<le> m` `M \<le> n`)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   357
    also have "\<dots> = r"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   358
      by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   359
    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
   360
  }
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   361
  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
   362
    by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   363
  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
   364
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   365
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   366
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
   367
proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   368
  fix X :: "nat \<Rightarrow> 'a ^ 'b" assume "Cauchy X"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   369
  have "\<And>i. (\<lambda>n. X n $ 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
   370
    using Cauchy_vec_nth [OF `Cauchy X`]
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   371
    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   372
  hence "X ----> vec_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))"
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   373
    by (simp add: vec_tendstoI)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   374
  then show "convergent X"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   375
    by (rule convergentI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   376
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   377
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   378
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   379
subsection {* Normed vector space *}
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   380
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   381
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
   382
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   383
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   384
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
   385
44141
0697c01ff3ea follow standard naming scheme for sgn_vec_def
huffman
parents: 44136
diff changeset
   386
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
   387
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   388
instance proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   389
  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
   390
  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
   391
    unfolding norm_vec_def
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   392
    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
   393
  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
   394
    unfolding norm_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   395
    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
   396
    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
   397
    done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   398
  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
   399
    unfolding norm_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   400
    by (simp add: setL2_right_distrib)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   401
  show "sgn x = scaleR (inverse (norm x)) x"
44141
0697c01ff3ea follow standard naming scheme for sgn_vec_def
huffman
parents: 44136
diff changeset
   402
    by (rule sgn_vec_def)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   403
  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
   404
    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
   405
    by (simp add: dist_norm)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   406
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   407
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   408
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   409
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   410
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
   411
unfolding norm_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   412
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
   413
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
   414
lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   415
apply default
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   416
apply (rule vector_add_component)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   417
apply (rule vector_scaleR_component)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   418
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
   419
done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   420
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   421
instance vec :: (banach, finite) banach ..
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   422
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   423
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   424
subsection {* Inner product space *}
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   425
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   426
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
   427
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   428
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   429
definition "inner x y = setsum (\<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
   430
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   431
instance proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   432
  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
   433
  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
   434
    unfolding inner_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   435
    by (simp add: inner_commute)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   436
  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
   437
    unfolding inner_vec_def
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56541
diff changeset
   438
    by (simp add: inner_add_left setsum.distrib)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   439
  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
   440
    unfolding inner_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   441
    by (simp add: setsum_right_distrib)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   442
  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
   443
    unfolding inner_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   444
    by (simp add: setsum_nonneg)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   445
  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
   446
    unfolding inner_vec_def
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   447
    by (simp add: vec_eq_iff setsum_nonneg_eq_0_iff)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   448
  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
   449
    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
   450
    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
   451
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   452
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   453
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   454
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   455
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   456
subsection {* Euclidean space *}
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   457
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   458
text {* Vectors pointing along a single axis. *}
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   459
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   460
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
   461
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   462
lemma axis_nth [simp]: "axis i x $ i = x"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   463
  unfolding axis_def by simp
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   464
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   465
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
   466
  unfolding axis_def vec_eq_iff by auto
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   467
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   468
lemma inner_axis_axis:
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   469
  "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
   470
  unfolding inner_vec_def
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   471
  apply (cases "i = j")
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   472
  apply clarsimp
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56541
diff changeset
   473
  apply (subst setsum.remove [of _ j], simp_all)
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56541
diff changeset
   474
  apply (rule setsum.neutral, simp add: axis_def)
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56541
diff changeset
   475
  apply (rule setsum.neutral, simp add: axis_def)
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   476
  done
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   477
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   478
lemma setsum_single:
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   479
  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
   480
  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
   481
  shows "(\<Sum>i\<in>A. f i) = y"
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56541
diff changeset
   482
  apply (subst setsum.remove [OF assms(1,2)])
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56541
diff changeset
   483
  apply (simp add: setsum.neutral assms(3,4))
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   484
  done
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   485
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   486
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
   487
  unfolding inner_vec_def
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   488
  apply (rule_tac k=i in setsum_single)
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   489
  apply simp_all
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   490
  apply (simp add: axis_def)
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   491
  done
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   492
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   493
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
   494
begin
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   495
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   496
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
   497
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   498
instance proof
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   499
  show "(Basis :: ('a ^ 'b) set) \<noteq> {}"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   500
    unfolding Basis_vec_def by simp
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   501
next
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   502
  show "finite (Basis :: ('a ^ 'b) set)"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   503
    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
   504
next
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   505
  fix u v :: "'a ^ 'b"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   506
  assume "u \<in> Basis" and "v \<in> Basis"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   507
  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
   508
    unfolding Basis_vec_def
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   509
    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
   510
next
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   511
  fix x :: "'a ^ 'b"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   512
  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
   513
    unfolding Basis_vec_def
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   514
    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
   515
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
   516
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 50252
diff changeset
   517
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
   518
  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
   519
  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
   520
     apply simp
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   521
    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
   522
   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
   523
  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
   524
     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
   525
  done
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   526
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   527
end
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   528
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   529
end