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