src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
author huffman
Thu, 29 Apr 2010 09:17:25 -0700
changeset 36591 df38e0c5c123
parent 36590 2cdaae32b682
child 36660 1cc4ab4b7ff7
permissions -rw-r--r--
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
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
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
     8
imports Inner_Product L2_Norm Numeral_Type
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     9
begin
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    10
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    11
subsection {* Finite Cartesian products, with indexing and lambdas. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    12
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    13
typedef (open Cart)
34291
4e896680897e finite annotation on cartesian product is now implicit.
hoelzl
parents: 34290
diff changeset
    14
  ('a, 'b) cart = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    15
  morphisms Cart_nth Cart_lambda ..
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    16
35254
0f17eda72e60 binder notation for default print_mode -- to avoid strange output if "xsymbols" is not active;
wenzelm
parents: 35253
diff changeset
    17
notation
0f17eda72e60 binder notation for default print_mode -- to avoid strange output if "xsymbols" is not active;
wenzelm
parents: 35253
diff changeset
    18
  Cart_nth (infixl "$" 90) and
0f17eda72e60 binder notation for default print_mode -- to avoid strange output if "xsymbols" is not active;
wenzelm
parents: 35253
diff changeset
    19
  Cart_lambda (binder "\<chi>" 10)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    20
34290
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    21
(*
34291
4e896680897e finite annotation on cartesian product is now implicit.
hoelzl
parents: 34290
diff changeset
    22
  Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than
4e896680897e finite annotation on cartesian product is now implicit.
hoelzl
parents: 34290
diff changeset
    23
  the finite type class write "cart 'b 'n"
34290
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    24
*)
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    25
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    26
syntax "_finite_cart" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15)
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    27
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    28
parse_translation {*
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    29
let
35397
69e2c0839091 more precise syntax antiquotations;
wenzelm
parents: 35254
diff changeset
    30
  fun cart t u = Syntax.const @{type_syntax cart} $ t $ u;
34290
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    31
  fun finite_cart_tr [t, u as Free (x, _)] =
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 34964
diff changeset
    32
        if Syntax.is_tid x then
35397
69e2c0839091 more precise syntax antiquotations;
wenzelm
parents: 35254
diff changeset
    33
          cart t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const @{class_syntax finite})
34290
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    34
        else cart t u
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    35
    | finite_cart_tr [t, u] = cart t u
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    36
in
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 34964
diff changeset
    37
  [(@{syntax_const "_finite_cart"}, finite_cart_tr)]
34290
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    38
end
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    39
*}
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    40
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    41
lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)"
35253
68dd8b51c6b8 tuned headers;
wenzelm
parents: 35113
diff changeset
    42
  by (auto intro: ext)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    43
34291
4e896680897e finite annotation on cartesian product is now implicit.
hoelzl
parents: 34290
diff changeset
    44
lemma Cart_eq: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    45
  by (simp add: Cart_nth_inject [symmetric] expand_fun_eq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    46
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    47
lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    48
  by (simp add: Cart_lambda_inverse)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    49
34291
4e896680897e finite annotation on cartesian product is now implicit.
hoelzl
parents: 34290
diff changeset
    50
lemma Cart_lambda_unique: "(\<forall>i. f$i = g i) \<longleftrightarrow> Cart_lambda g = f"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    51
  by (auto simp add: Cart_eq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    52
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    53
lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    54
  by (simp add: Cart_eq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    55
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    56
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    57
subsection {* Group operations and class instances *}
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
instantiation cart :: (zero,finite) zero
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    60
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    61
  definition vector_zero_def : "0 \<equiv> (\<chi> i. 0)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    62
  instance ..
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    63
end
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    64
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    65
instantiation cart :: (plus,finite) plus
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    66
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    67
  definition  vector_add_def : "op + \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) + (y$i)))"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    68
  instance ..
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    69
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    70
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    71
instantiation cart :: (minus,finite) minus
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    72
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    73
  definition vector_minus_def : "op - \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) - (y$i)))"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    74
  instance ..
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    75
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    76
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    77
instantiation cart :: (uminus,finite) uminus
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    78
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    79
  definition vector_uminus_def : "uminus \<equiv> (\<lambda> x.  (\<chi> i. - (x$i)))"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    80
  instance ..
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    81
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    82
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    83
lemma zero_index [simp]: "0 $ i = 0"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    84
  unfolding vector_zero_def by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    85
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    86
lemma vector_add_component [simp]: "(x + y)$i = x$i + y$i"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    87
  unfolding vector_add_def by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    88
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    89
lemma vector_minus_component [simp]: "(x - y)$i = x$i - y$i"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    90
  unfolding vector_minus_def by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    91
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    92
lemma vector_uminus_component [simp]: "(- x)$i = - (x$i)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    93
  unfolding vector_uminus_def by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    94
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    95
instance cart :: (semigroup_add, finite) semigroup_add
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    96
  by default (simp add: Cart_eq add_assoc)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    97
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    98
instance cart :: (ab_semigroup_add, finite) ab_semigroup_add
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    99
  by default (simp add: Cart_eq add_commute)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   100
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   101
instance cart :: (monoid_add, finite) monoid_add
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   102
  by default (simp_all add: Cart_eq)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   103
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   104
instance cart :: (comm_monoid_add, finite) comm_monoid_add
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   105
  by default (simp add: Cart_eq)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   106
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   107
instance cart :: (cancel_semigroup_add, finite) cancel_semigroup_add
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   108
  by default (simp_all add: Cart_eq)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   109
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   110
instance cart :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   111
  by default (simp add: Cart_eq)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   112
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   113
instance cart :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   114
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   115
instance cart :: (group_add, finite) group_add
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   116
  by default (simp_all add: Cart_eq diff_minus)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   117
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   118
instance cart :: (ab_group_add, finite) ab_group_add
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   119
  by default (simp_all add: Cart_eq)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   120
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   121
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   122
subsection {* Real vector space *}
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
instantiation cart :: (real_vector, finite) real_vector
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   125
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   126
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   127
definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   128
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   129
lemma vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   130
  unfolding vector_scaleR_def by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   131
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   132
instance
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   133
  by default (simp_all add: Cart_eq scaleR_left_distrib scaleR_right_distrib)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   134
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   135
end
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
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   138
subsection {* Topological space *}
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
instantiation cart :: (topological_space, finite) topological_space
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   141
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   142
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   143
definition open_vector_def:
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   144
  "open (S :: ('a ^ 'b) set) \<longleftrightarrow>
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   145
    (\<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
   146
      (\<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
   147
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   148
instance proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   149
  show "open (UNIV :: ('a ^ 'b) set)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   150
    unfolding open_vector_def by auto
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   151
next
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   152
  fix S T :: "('a ^ 'b) set"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   153
  assume "open S" "open T" thus "open (S \<inter> T)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   154
    unfolding open_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   155
    apply clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   156
    apply (drule (1) bspec)+
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   157
    apply (clarify, rename_tac Sa Ta)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   158
    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
   159
    apply (simp add: open_Int)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   160
    done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   161
next
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   162
  fix K :: "('a ^ 'b) set set"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   163
  assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   164
    unfolding open_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   165
    apply clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   166
    apply (drule (1) bspec)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   167
    apply (drule (1) bspec)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   168
    apply clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   169
    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
   170
    apply fast
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   171
    done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   172
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   173
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   174
end
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
lemma open_vector_box: "\<forall>i. open (S i) \<Longrightarrow> open {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
   177
unfolding open_vector_def by auto
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   178
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   179
lemma open_vimage_Cart_nth: "open S \<Longrightarrow> open ((\<lambda>x. x $ i) -` S)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   180
unfolding open_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   181
apply clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   182
apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   183
done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   184
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   185
lemma closed_vimage_Cart_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) -` S)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   186
unfolding closed_open vimage_Compl [symmetric]
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   187
by (rule open_vimage_Cart_nth)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   188
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   189
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
   190
proof -
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   191
  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
   192
  thus "\<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
   193
    by (simp add: closed_INT closed_vimage_Cart_nth)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   194
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   195
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   196
lemma tendsto_Cart_nth [tendsto_intros]:
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   197
  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
   198
  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
   199
proof (rule topological_tendstoI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   200
  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
   201
  then have "open ((\<lambda>y. y $ i) -` S)" "a \<in> ((\<lambda>y. y $ i) -` S)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   202
    by (simp_all add: open_vimage_Cart_nth)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   203
  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
   204
    by (rule topological_tendstoD)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   205
  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
   206
    by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   207
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   208
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   209
lemma eventually_Ball_finite: (* TODO: move *)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   210
  assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   211
  shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   212
using assms by (induct set: finite, simp, simp add: eventually_conj)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   213
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   214
lemma eventually_all_finite: (* TODO: move *)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   215
  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   216
  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   217
  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   218
using eventually_Ball_finite [of UNIV P] assms by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   219
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   220
lemma tendsto_vector:
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   221
  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
   222
  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
   223
proof (rule topological_tendstoI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   224
  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
   225
  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
   226
    and S: "\<And>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
   227
    unfolding open_vector_def by metis
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   228
  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
   229
    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
   230
  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
   231
    by (rule eventually_all_finite)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   232
  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
   233
    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
   234
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   235
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   236
lemma tendsto_Cart_lambda [tendsto_intros]:
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   237
  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
   238
  shows "((\<lambda>x. \<chi> i. f x i) ---> (\<chi> i. a i)) net"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   239
using assms by (simp add: tendsto_vector)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   240
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   241
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   242
subsection {* Metric *}
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   243
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   244
(* TODO: move somewhere else *)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   245
lemma finite_choice: "finite A \<Longrightarrow> \<forall>x\<in>A. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x\<in>A. P x (f x)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   246
apply (induct set: finite, simp_all)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   247
apply (clarify, rename_tac y)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   248
apply (rule_tac x="f(x:=y)" in exI, simp)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   249
done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   250
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   251
instantiation cart :: (metric_space, finite) metric_space
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   252
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   253
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   254
definition dist_vector_def:
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   255
  "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
   256
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   257
lemma dist_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   258
unfolding dist_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   259
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
   260
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   261
instance proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   262
  fix x y :: "'a ^ 'b"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   263
  show "dist x y = 0 \<longleftrightarrow> x = y"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   264
    unfolding dist_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   265
    by (simp add: setL2_eq_0_iff Cart_eq)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   266
next
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   267
  fix x y z :: "'a ^ 'b"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   268
  show "dist x y \<le> dist x z + dist y z"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   269
    unfolding dist_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   270
    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
   271
    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
   272
    done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   273
next
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   274
  (* FIXME: long proof! *)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   275
  fix S :: "('a ^ 'b) set"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   276
  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   277
    unfolding open_vector_def open_dist
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   278
    apply safe
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   279
     apply (drule (1) bspec)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   280
     apply clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   281
     apply (subgoal_tac "\<exists>e>0. \<forall>i y. dist y (x$i) < e \<longrightarrow> y \<in> A i")
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   282
      apply clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   283
      apply (rule_tac x=e in exI, clarify)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   284
      apply (drule spec, erule mp, clarify)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   285
      apply (drule spec, drule spec, erule mp)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   286
      apply (erule le_less_trans [OF dist_nth_le])
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   287
     apply (subgoal_tac "\<forall>i\<in>UNIV. \<exists>e>0. \<forall>y. dist y (x$i) < e \<longrightarrow> y \<in> A i")
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   288
      apply (drule finite_choice [OF finite], clarify)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   289
      apply (rule_tac x="Min (range f)" in exI, simp)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   290
     apply clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   291
     apply (drule_tac x=i in spec, clarify)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   292
     apply (erule (1) bspec)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   293
    apply (drule (1) bspec, clarify)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   294
    apply (subgoal_tac "\<exists>r. (\<forall>i::'b. 0 < r i) \<and> e = setL2 r UNIV")
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   295
     apply clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   296
     apply (rule_tac x="\<lambda>i. {y. dist y (x$i) < r i}" in exI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   297
     apply (rule conjI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   298
      apply clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   299
      apply (rule conjI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   300
       apply (clarify, rename_tac y)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   301
       apply (rule_tac x="r i - dist y (x$i)" in exI, rule conjI, simp)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   302
       apply clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   303
       apply (simp only: less_diff_eq)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   304
       apply (erule le_less_trans [OF dist_triangle])
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   305
      apply simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   306
     apply clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   307
     apply (drule spec, erule mp)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   308
     apply (simp add: dist_vector_def setL2_strict_mono)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   309
    apply (rule_tac x="\<lambda>i. e / sqrt (of_nat CARD('b))" in exI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   310
    apply (simp add: divide_pos_pos setL2_constant)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   311
    done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   312
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   313
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   314
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   315
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   316
lemma LIMSEQ_Cart_nth:
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   317
  "(X ----> a) \<Longrightarrow> (\<lambda>n. X n $ i) ----> a $ i"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   318
unfolding LIMSEQ_conv_tendsto by (rule tendsto_Cart_nth)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   319
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   320
lemma LIM_Cart_nth:
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   321
  "(f -- x --> y) \<Longrightarrow> (\<lambda>x. f x $ i) -- x --> y $ i"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   322
unfolding LIM_conv_tendsto by (rule tendsto_Cart_nth)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   323
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   324
lemma Cauchy_Cart_nth:
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   325
  "Cauchy (\<lambda>n. X n) \<Longrightarrow> Cauchy (\<lambda>n. X n $ i)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   326
unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_nth_le])
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   327
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   328
lemma LIMSEQ_vector:
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   329
  assumes "\<And>i. (\<lambda>n. X n $ i) ----> (a $ i)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   330
  shows "X ----> a"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   331
using assms unfolding LIMSEQ_conv_tendsto by (rule tendsto_vector)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   332
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   333
lemma Cauchy_vector:
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"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   339
  then have "0 < r / of_nat CARD('n)" (is "0 < ?s")
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   340
    by (simp add: divide_pos_pos)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   341
  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
   342
  def M \<equiv> "Max (range N)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   343
  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
   344
    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
   345
  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
   346
    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
   347
  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
   348
    unfolding M_def by simp
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
    fix m n :: nat
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   351
    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
   352
    have "dist (X m) (X n) = setL2 (\<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
   353
      unfolding dist_vector_def ..
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   354
    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
   355
      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
   356
    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
   357
      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
   358
    also have "\<dots> = r"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   359
      by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   360
    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
   361
  }
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   362
  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
   363
    by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   364
  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
   365
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   366
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   367
instance cart :: (complete_space, finite) complete_space
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   368
proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   369
  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
   370
  have "\<And>i. (\<lambda>n. X n $ i) ----> lim (\<lambda>n. X n $ i)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   371
    using Cauchy_Cart_nth [OF `Cauchy X`]
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   372
    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   373
  hence "X ----> Cart_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   374
    by (simp add: LIMSEQ_vector)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   375
  then show "convergent X"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   376
    by (rule convergentI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   377
qed
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
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   380
subsection {* Normed vector space *}
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   381
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   382
instantiation cart :: (real_normed_vector, finite) real_normed_vector
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   383
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   384
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   385
definition norm_vector_def:
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   386
  "norm x = setL2 (\<lambda>i. norm (x$i)) UNIV"
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
definition vector_sgn_def:
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   389
  "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   390
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   391
instance proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   392
  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
   393
  show "0 \<le> norm x"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   394
    unfolding norm_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   395
    by (rule setL2_nonneg)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   396
  show "norm x = 0 \<longleftrightarrow> x = 0"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   397
    unfolding norm_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   398
    by (simp add: setL2_eq_0_iff Cart_eq)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   399
  show "norm (x + y) \<le> norm x + norm y"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   400
    unfolding norm_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   401
    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
   402
    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
   403
    done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   404
  show "norm (scaleR a x) = \<bar>a\<bar> * norm x"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   405
    unfolding norm_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   406
    by (simp add: setL2_right_distrib)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   407
  show "sgn x = scaleR (inverse (norm x)) x"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   408
    by (rule vector_sgn_def)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   409
  show "dist x y = norm (x - y)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   410
    unfolding dist_vector_def norm_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   411
    by (simp add: dist_norm)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   412
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   413
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   414
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   415
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   416
lemma norm_nth_le: "norm (x $ i) \<le> norm x"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   417
unfolding norm_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   418
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
   419
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   420
interpretation Cart_nth: bounded_linear "\<lambda>x. x $ i"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   421
apply default
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   422
apply (rule vector_add_component)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   423
apply (rule vector_scaleR_component)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   424
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
   425
done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   426
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   427
instance cart :: (banach, finite) banach ..
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   428
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   429
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   430
subsection {* Inner product space *}
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   431
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   432
instantiation cart :: (real_inner, finite) real_inner
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   433
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   434
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   435
definition inner_vector_def:
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   436
  "inner x y = setsum (\<lambda>i. inner (x$i) (y$i)) UNIV"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   437
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   438
instance proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   439
  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
   440
  show "inner x y = inner y x"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   441
    unfolding inner_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   442
    by (simp add: inner_commute)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   443
  show "inner (x + y) z = inner x z + inner y z"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   444
    unfolding inner_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   445
    by (simp add: inner_add_left setsum_addf)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   446
  show "inner (scaleR r x) y = r * inner x y"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   447
    unfolding inner_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   448
    by (simp add: setsum_right_distrib)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   449
  show "0 \<le> inner x x"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   450
    unfolding inner_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   451
    by (simp add: setsum_nonneg)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   452
  show "inner x x = 0 \<longleftrightarrow> x = 0"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   453
    unfolding inner_vector_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   454
    by (simp add: Cart_eq setsum_nonneg_eq_0_iff)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   455
  show "norm x = sqrt (inner x x)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   456
    unfolding inner_vector_def norm_vector_def setL2_def
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   457
    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
   458
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   459
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   460
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   461
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   462
end