src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45694 4a8743618257
child 49674 dbadb4d03cbc
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
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
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 44681
diff changeset
    16
typedef (open) ('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 {*
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    31
let
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    32
  fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    33
  fun finite_vec_tr [t, u as Free (x, _)] =
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 41413
diff changeset
    34
        if Lexicon.is_tid x then
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    35
          vec t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const @{class_syntax finite})
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    36
        else vec t u
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    37
    | finite_vec_tr [t, u] = vec t u
34290
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    38
in
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    39
  [(@{syntax_const "_finite_vec"}, finite_vec_tr)]
34290
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    40
end
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    41
*}
1edf0f223c6e added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents: 34289
diff changeset
    42
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    43
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
    44
  by (simp add: vec_nth_inject [symmetric] fun_eq_iff)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
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_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
    47
  by (simp add: vec_lambda_inverse)
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_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
    50
  by (auto simp add: vec_eq_iff)
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_eta: "(\<chi> i. (g$i)) = g"
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    53
  by (simp add: vec_eq_iff)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    54
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    55
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    56
subsection {* Group operations and class instances *}
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    57
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    58
instantiation vec :: (zero, finite) zero
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    59
begin
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    60
  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
    61
  instance ..
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    62
end
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    63
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    64
instantiation vec :: (plus, finite) plus
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    65
begin
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    66
  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
    67
  instance ..
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    68
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    69
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    70
instantiation vec :: (minus, finite) minus
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    71
begin
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    72
  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
    73
  instance ..
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    74
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    75
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    76
instantiation vec :: (uminus, finite) uminus
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    77
begin
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    78
  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
    79
  instance ..
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    80
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    81
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    82
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
    83
  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
    84
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    85
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
    86
  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
    87
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    88
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
    89
  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
    90
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
    91
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
    92
  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
    93
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    94
instance vec :: (semigroup_add, finite) semigroup_add
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    95
  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
    96
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    97
instance vec :: (ab_semigroup_add, finite) ab_semigroup_add
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    98
  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
    99
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   100
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
   101
  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
   102
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   103
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
   104
  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
   105
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   106
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
   107
  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
   108
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   109
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
   110
  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
   111
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   112
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
   113
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   114
instance vec :: (group_add, finite) group_add
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   115
  by default (simp_all add: vec_eq_iff diff_minus)
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 :: (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
   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
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
subsection {* Real vector space *}
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   122
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   123
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
   124
begin
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
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
   127
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   128
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
   129
  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
   130
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   131
instance
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   132
  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
   133
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   134
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   135
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
subsection {* Topological space *}
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   138
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   139
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
   140
begin
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
definition
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   143
  "open (S :: ('a ^ 'b) set) \<longleftrightarrow>
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   144
    (\<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
   145
      (\<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
   146
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   147
instance proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   148
  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
   149
    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
   150
next
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   151
  fix S T :: "('a ^ 'b) set"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   152
  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
   153
    unfolding open_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   154
    apply clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   155
    apply (drule (1) bspec)+
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   156
    apply (clarify, rename_tac Sa Ta)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   157
    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
   158
    apply (simp add: open_Int)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   159
    done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   160
next
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   161
  fix K :: "('a ^ 'b) set set"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   162
  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
   163
    unfolding open_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   164
    apply clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   165
    apply (drule (1) bspec)
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 clarify
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   168
    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
   169
    apply fast
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   170
    done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   171
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   172
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   173
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   174
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   175
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
   176
  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
   177
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   178
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
   179
  unfolding open_vec_def
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   180
  apply clarify
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   181
  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
   182
  done
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   183
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   184
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
   185
  unfolding closed_open vimage_Compl [symmetric]
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   186
  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
   187
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   188
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
   189
proof -
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   190
  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
   191
  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
   192
    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
   193
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   194
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   195
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
   196
  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
   197
  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
   198
proof (rule topological_tendstoI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   199
  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
   200
  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
   201
    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
   202
  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
   203
    by (rule topological_tendstoD)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   204
  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
   205
    by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   206
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   207
44631
6820684c7a58 generalize lemma isCont_vec_nth
huffman
parents: 44630
diff changeset
   208
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
   209
  unfolding isCont_def by (rule tendsto_vec_nth)
6820684c7a58 generalize lemma isCont_vec_nth
huffman
parents: 44630
diff changeset
   210
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   211
lemma eventually_Ball_finite: (* TODO: move *)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   212
  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
   213
  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
   214
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
   215
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   216
lemma eventually_all_finite: (* TODO: move *)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   217
  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
   218
  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
   219
  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
   220
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
   221
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   222
lemma vec_tendstoI:
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   223
  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
   224
  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
   225
proof (rule topological_tendstoI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   226
  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
   227
  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
   228
    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
   229
    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
   230
  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
   231
    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
   232
  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
   233
    by (rule eventually_all_finite)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   234
  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
   235
    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
   236
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   237
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   238
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
   239
  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
   240
  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
   241
  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
   242
44571
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   243
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
   244
proof (rule openI)
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   245
  fix a assume "a \<in> (\<lambda>x. x $ i) ` S"
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   246
  then obtain z where "a = z $ i" and "z \<in> S" ..
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   247
  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
   248
    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
   249
    using `open S` unfolding open_vec_def by auto
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   250
  hence "A i \<subseteq> (\<lambda>x. x $ i) ` S"
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   251
    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
   252
      simp_all)
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   253
  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
   254
    using A `a = z $ i` by simp
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   255
  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
   256
qed
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   257
44571
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   258
instance vec :: (perfect_space, finite) perfect_space
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   259
proof
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   260
  fix x :: "'a ^ 'b" show "\<not> open {x}"
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   261
  proof
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   262
    assume "open {x}"
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   263
    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
   264
    hence "\<forall>i. open {x $ i}" by simp
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   265
    thus "False" by (simp add: not_open_singleton)
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   266
  qed
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   267
qed
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   268
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   269
bd91b77c4cd6 move class perfect_space into RealVector.thy;
huffman
parents: 44282
diff changeset
   270
subsection {* Metric space *}
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   271
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   272
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
   273
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   274
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   275
definition
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   276
  "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
   277
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   278
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
   279
  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
   280
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   281
instance proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   282
  fix x y :: "'a ^ 'b"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   283
  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
   284
    unfolding dist_vec_def
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   285
    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
   286
next
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   287
  fix x y z :: "'a ^ 'b"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   288
  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
   289
    unfolding dist_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   290
    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
   291
    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
   292
    done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   293
next
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   294
  fix S :: "('a ^ 'b) set"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   295
  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
   296
  proof
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   297
    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
   298
    proof
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   299
      fix x assume "x \<in> S"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   300
      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
   301
        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
   302
        using `open S` and `x \<in> S` unfolding open_vec_def by metis
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   303
      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
   304
        using A unfolding open_dist by simp
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   305
      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
   306
        by (rule finite_set_choice [OF finite])
44630
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   307
      then obtain r where r1: "\<forall>i. 0 < r i"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   308
        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
   309
      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
   310
        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
   311
      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
   312
    qed
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   313
  next
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   314
    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
   315
    proof (unfold open_vec_def, rule)
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   316
      fix x assume "x \<in> S"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   317
      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
   318
        using * by fast
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   319
      def r \<equiv> "\<lambda>i::'b. e / sqrt (of_nat CARD('b))"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   320
      from `0 < e` have r: "\<forall>i. 0 < r i"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   321
        unfolding r_def by (simp_all add: divide_pos_pos)
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   322
      from `0 < e` have e: "e = setL2 r UNIV"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   323
        unfolding r_def by (simp add: setL2_constant)
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   324
      def A \<equiv> "\<lambda>i. {y. dist (x $ i) y < r i}"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   325
      have "\<forall>i. open (A i) \<and> x $ i \<in> A i"
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   326
        unfolding A_def by (simp add: open_ball r)
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   327
      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
   328
        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
   329
      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
   330
        (\<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
   331
    qed
d08cb39b628a convert proof to Isar-style
huffman
parents: 44571
diff changeset
   332
  qed
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   333
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   334
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   335
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   336
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   337
lemma Cauchy_vec_nth:
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   338
  "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
   339
  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
   340
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   341
lemma vec_CauchyI:
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   342
  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
   343
  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
   344
  shows "Cauchy (\<lambda>n. X n)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   345
proof (rule metric_CauchyI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   346
  fix r :: real assume "0 < r"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   347
  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
   348
    by (simp add: divide_pos_pos)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   349
  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
   350
  def M \<equiv> "Max (range N)"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   351
  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
   352
    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
   353
  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
   354
    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
   355
  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
   356
    unfolding M_def by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   357
  {
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   358
    fix m n :: nat
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   359
    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
   360
    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
   361
      unfolding dist_vec_def ..
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   362
    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
   363
      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
   364
    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
   365
      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
   366
    also have "\<dots> = r"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   367
      by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   368
    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
   369
  }
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   370
  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
   371
    by simp
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   372
  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
   373
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   374
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   375
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
   376
proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   377
  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
   378
  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
   379
    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
   380
    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
   381
  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
   382
    by (simp add: vec_tendstoI)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   383
  then show "convergent X"
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   384
    by (rule convergentI)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   385
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   386
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
subsection {* Normed vector space *}
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   389
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   390
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
   391
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   392
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   393
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
   394
44141
0697c01ff3ea follow standard naming scheme for sgn_vec_def
huffman
parents: 44136
diff changeset
   395
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
   396
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   397
instance proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   398
  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
   399
  show "0 \<le> norm x"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   400
    unfolding norm_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   401
    by (rule setL2_nonneg)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   402
  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
   403
    unfolding norm_vec_def
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   404
    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
   405
  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
   406
    unfolding norm_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   407
    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
   408
    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
   409
    done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   410
  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
   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 (simp add: setL2_right_distrib)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   413
  show "sgn x = scaleR (inverse (norm x)) x"
44141
0697c01ff3ea follow standard naming scheme for sgn_vec_def
huffman
parents: 44136
diff changeset
   414
    by (rule sgn_vec_def)
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   415
  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
   416
    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
   417
    by (simp add: dist_norm)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   418
qed
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
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   421
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   422
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
   423
unfolding norm_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   424
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
   425
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
   426
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
   427
apply default
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   428
apply (rule vector_add_component)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   429
apply (rule vector_scaleR_component)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   430
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
   431
done
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   432
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   433
instance vec :: (banach, finite) banach ..
36591
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
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   436
subsection {* Inner product space *}
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   437
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   438
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
   439
begin
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   440
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   441
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
   442
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   443
instance proof
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   444
  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
   445
  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
   446
    unfolding inner_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   447
    by (simp add: inner_commute)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   448
  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
   449
    unfolding inner_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   450
    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
   451
  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
   452
    unfolding inner_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   453
    by (simp add: setsum_right_distrib)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   454
  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
   455
    unfolding inner_vec_def
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   456
    by (simp add: setsum_nonneg)
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   457
  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
   458
    unfolding inner_vec_def
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   459
    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
   460
  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
   461
    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
   462
    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
   463
qed
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   464
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   465
end
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   466
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   467
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   468
subsection {* Euclidean space *}
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   469
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   470
text {* Vectors pointing along a single axis. *}
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   471
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   472
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
   473
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   474
lemma axis_nth [simp]: "axis i x $ i = x"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   475
  unfolding axis_def by simp
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   476
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   477
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
   478
  unfolding axis_def vec_eq_iff by auto
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   479
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   480
lemma inner_axis_axis:
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   481
  "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
   482
  unfolding inner_vec_def
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   483
  apply (cases "i = j")
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   484
  apply clarsimp
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   485
  apply (subst setsum_diff1' [where a=j], simp_all)
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   486
  apply (rule setsum_0', simp add: axis_def)
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   487
  apply (rule setsum_0', simp add: axis_def)
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   488
  done
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   489
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   490
lemma setsum_single:
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   491
  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
   492
  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
   493
  shows "(\<Sum>i\<in>A. f i) = y"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   494
  apply (subst setsum_diff1' [OF assms(1,2)])
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   495
  apply (simp add: setsum_0' assms(3,4))
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   496
  done
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   497
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   498
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
   499
  unfolding inner_vec_def
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   500
  apply (rule_tac k=i in setsum_single)
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   501
  apply simp_all
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   502
  apply (simp add: axis_def)
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   503
  done
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   504
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   505
text {* A bijection between @{text "'n::finite"} and @{text "{..<CARD('n)}"} *}
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   506
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   507
definition vec_bij_nat :: "nat \<Rightarrow> ('n::finite)" where
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   508
  "vec_bij_nat = (SOME p. bij_betw p {..<CARD('n)} (UNIV::'n set) )"
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   509
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   510
abbreviation "\<pi> \<equiv> vec_bij_nat"
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   511
definition "\<pi>' = inv_into {..<CARD('n)} (\<pi>::nat \<Rightarrow> ('n::finite))"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   512
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   513
lemma bij_betw_pi:
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   514
  "bij_betw \<pi> {..<CARD('n::finite)} (UNIV::('n::finite) set)"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   515
  using ex_bij_betw_nat_finite[of "UNIV::'n set"]
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   516
  by (auto simp: vec_bij_nat_def atLeast0LessThan
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   517
    intro!: someI_ex[of "\<lambda>x. bij_betw x {..<CARD('n)} (UNIV::'n set)"])
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   518
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   519
lemma bij_betw_pi'[intro]: "bij_betw \<pi>' (UNIV::'n set) {..<CARD('n::finite)}"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   520
  using bij_betw_inv_into[OF bij_betw_pi] unfolding \<pi>'_def by auto
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   521
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   522
lemma pi'_inj[intro]: "inj \<pi>'"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   523
  using bij_betw_pi' unfolding bij_betw_def by auto
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   524
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   525
lemma pi'_range[intro]: "\<And>i::'n. \<pi>' i < CARD('n::finite)"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   526
  using bij_betw_pi' unfolding bij_betw_def by auto
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   527
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   528
lemma \<pi>\<pi>'[simp]: "\<And>i::'n::finite. \<pi> (\<pi>' i) = i"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   529
  using bij_betw_pi by (auto intro!: f_inv_into_f simp: \<pi>'_def bij_betw_def)
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   530
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   531
lemma \<pi>'\<pi>[simp]: "\<And>i. i\<in>{..<CARD('n::finite)} \<Longrightarrow> \<pi>' (\<pi> i::'n) = i"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   532
  using bij_betw_pi by (auto intro!: inv_into_f_eq simp: \<pi>'_def bij_betw_def)
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   533
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   534
lemma \<pi>\<pi>'_alt[simp]: "\<And>i. i<CARD('n::finite) \<Longrightarrow> \<pi>' (\<pi> i::'n) = i"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   535
  by auto
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   536
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   537
lemma \<pi>_inj_on: "inj_on (\<pi>::nat\<Rightarrow>'n::finite) {..<CARD('n)}"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   538
  using bij_betw_pi[where 'n='n] by (simp add: bij_betw_def)
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   539
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   540
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
   541
begin
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   542
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   543
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
   544
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   545
definition "dimension (t :: ('a ^ 'b) itself) = CARD('b) * DIM('a)"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   546
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   547
definition "basis i =
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   548
  (if i < (CARD('b) * DIM('a))
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   549
  then axis (\<pi>(i div DIM('a))) (basis (i mod DIM('a)))
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   550
  else 0)"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   551
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   552
lemma basis_eq:
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   553
  assumes "i < CARD('b)" and "j < DIM('a)"
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   554
  shows "basis (j + i * DIM('a)) = axis (\<pi> i) (basis j)"
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   555
proof -
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   556
  have "j + i * DIM('a) <  DIM('a) * (i + 1)" using assms by (auto simp: field_simps)
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   557
  also have "\<dots> \<le> DIM('a) * CARD('b)" using assms unfolding mult_le_cancel1 by auto
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   558
  finally show ?thesis
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   559
    unfolding basis_vec_def using assms by (auto simp: vec_eq_iff not_less field_simps)
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   560
qed
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   561
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   562
lemma basis_eq_pi':
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   563
  assumes "j < DIM('a)"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   564
  shows "basis (j + \<pi>' i * DIM('a)) $ k = (if k = i then basis j else 0)"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   565
  apply (subst basis_eq)
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   566
  using pi'_range assms by (simp_all add: axis_def)
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   567
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   568
lemma split_times_into_modulo[consumes 1]:
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   569
  fixes k :: nat
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   570
  assumes "k < A * B"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   571
  obtains i j where "i < A" and "j < B" and "k = j + i * B"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   572
proof
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   573
  have "A * B \<noteq> 0"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   574
  proof assume "A * B = 0" with assms show False by simp qed
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   575
  hence "0 < B" by auto
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   576
  thus "k mod B < B" using `0 < B` by auto
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   577
next
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   578
  have "k div B * B \<le> k div B * B + k mod B" by (rule le_add1)
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   579
  also have "... < A * B" using assms by simp
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   580
  finally show "k div B < A" by auto
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   581
qed simp
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   582
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   583
lemma linear_less_than_times:
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   584
  fixes i j A B :: nat assumes "i < B" "j < A"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   585
  shows "j + i * A < B * A"
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   586
proof -
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   587
  have "i * A + j < (Suc i)*A" using `j < A` by simp
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   588
  also have "\<dots> \<le> B * A" using `i < B` unfolding mult_le_cancel2 by simp
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   589
  finally show ?thesis by simp
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   590
qed
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   591
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   592
lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   593
  by (rule dimension_vec_def)
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   594
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   595
instance proof
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   596
  show "(Basis :: ('a ^ 'b) set) \<noteq> {}"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   597
    unfolding Basis_vec_def by simp
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   598
next
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   599
  show "finite (Basis :: ('a ^ 'b) set)"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   600
    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
   601
next
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   602
  fix u v :: "'a ^ 'b"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   603
  assume "u \<in> Basis" and "v \<in> Basis"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   604
  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
   605
    unfolding Basis_vec_def
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   606
    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
   607
next
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   608
  fix x :: "'a ^ 'b"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   609
  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
   610
    unfolding Basis_vec_def
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   611
    by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff)
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   612
next
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   613
  show "DIM('a ^ 'b) = card (Basis :: ('a ^ 'b) set)"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   614
    unfolding Basis_vec_def dimension_vec_def dimension_def
44215
786876687ef8 remove duplicate lemma disjoint_iff
huffman
parents: 44166
diff changeset
   615
    by (simp add: card_UN_disjoint [unfolded disjoint_iff_not_equal]
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   616
      axis_eq_axis nonzero_Basis)
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   617
next
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   618
  show "basis ` {..<DIM('a ^ 'b)} = (Basis :: ('a ^ 'b) set)"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   619
    unfolding Basis_vec_def
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   620
    apply auto
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   621
    apply (erule split_times_into_modulo)
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   622
    apply (simp add: basis_eq axis_eq_axis)
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   623
    apply (erule Basis_elim)
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   624
    apply (simp add: image_def basis_vec_def axis_eq_axis)
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   625
    apply (rule rev_bexI, simp)
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   626
    apply (erule linear_less_than_times [OF pi'_range])
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   627
    apply simp
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   628
    done
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   629
next
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   630
  show "basis ` {DIM('a ^ 'b)..} = {0::'a ^ 'b}"
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   631
    by (auto simp add: image_def basis_vec_def)
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   632
qed
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   633
36591
df38e0c5c123 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 36590
diff changeset
   634
end
44135
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   635
18b4ab6854f1 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents: 42290
diff changeset
   636
end