src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47108 2a1953f0d20d
child 49197 e5224d887e12
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
     1
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
     2
header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
     3
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
     4
theory Cartesian_Euclidean_Space
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
     5
imports Finite_Cartesian_Product Integration
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
     6
begin
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
     7
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
     8
lemma delta_mult_idempotent:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
     9
  "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" by (cases "k=a", auto)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    10
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    11
lemma setsum_Plus:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    12
  "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow>
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    13
    (\<Sum>x\<in>A <+> B. g x) = (\<Sum>x\<in>A. g (Inl x)) + (\<Sum>x\<in>B. g (Inr x))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    14
  unfolding Plus_def
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    15
  by (subst setsum_Un_disjoint, auto simp add: setsum_reindex)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    16
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    17
lemma setsum_UNIV_sum:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    18
  fixes g :: "'a::finite + 'b::finite \<Rightarrow> _"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    19
  shows "(\<Sum>x\<in>UNIV. g x) = (\<Sum>x\<in>UNIV. g (Inl x)) + (\<Sum>x\<in>UNIV. g (Inr x))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    20
  apply (subst UNIV_Plus_UNIV [symmetric])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    21
  apply (rule setsum_Plus [OF finite finite])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    22
  done
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    23
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    24
lemma setsum_mult_product:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    25
  "setsum h {..<A * B :: nat} = (\<Sum>i\<in>{..<A}. \<Sum>j\<in>{..<B}. h (j + i * B))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    26
  unfolding sumr_group[of h B A, unfolded atLeast0LessThan, symmetric]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    27
proof (rule setsum_cong, simp, rule setsum_reindex_cong)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    28
  fix i show "inj_on (\<lambda>j. j + i * B) {..<B}" by (auto intro!: inj_onI)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    29
  show "{i * B..<i * B + B} = (\<lambda>j. j + i * B) ` {..<B}"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    30
  proof safe
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    31
    fix j assume "j \<in> {i * B..<i * B + B}"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    32
    thus "j \<in> (\<lambda>j. j + i * B) ` {..<B}"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    33
      by (auto intro!: image_eqI[of _ _ "j - i * B"])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    34
  qed simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    35
qed simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    36
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    37
subsection{* Basic componentwise operations on vectors. *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    38
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    39
instantiation vec :: (times, finite) times
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    40
begin
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    41
  definition "op * \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) * (y$i)))"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    42
  instance ..
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    43
end
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    44
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    45
instantiation vec :: (one, finite) one
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    46
begin
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    47
  definition "1 \<equiv> (\<chi> i. 1)"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    48
  instance ..
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    49
end
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    50
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    51
instantiation vec :: (ord, finite) ord
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    52
begin
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    53
  definition "x \<le> y \<longleftrightarrow> (\<forall>i. x$i \<le> y$i)"
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    54
  definition "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
    55
  instance ..
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    56
end
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    57
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    58
text{* The ordering on one-dimensional vectors is linear. *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    59
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    60
class cart_one = assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    61
begin
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    62
  subclass finite
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    63
  proof from UNIV_one show "finite (UNIV :: 'a set)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    64
      by (auto intro!: card_ge_0_finite) qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    65
end
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    66
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    67
instantiation vec :: (linorder,cart_one) linorder begin
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    68
instance proof
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    69
  guess a B using UNIV_one[where 'a='b] unfolding card_Suc_eq apply- by(erule exE)+
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    70
  hence *:"UNIV = {a}" by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    71
  have "\<And>P. (\<forall>i\<in>UNIV. P i) \<longleftrightarrow> P a" unfolding * by auto hence all:"\<And>P. (\<forall>i. P i) \<longleftrightarrow> P a" by auto
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    72
  fix x y z::"'a^'b::cart_one" note * = less_eq_vec_def less_vec_def all vec_eq_iff
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    73
  show "x\<le>x" "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" "x\<le>y \<or> y\<le>x" unfolding * by(auto simp only:field_simps)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    74
  { assume "x\<le>y" "y\<le>z" thus "x\<le>z" unfolding * by(auto simp only:field_simps) }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    75
  { assume "x\<le>y" "y\<le>x" thus "x=y" unfolding * by(auto simp only:field_simps) }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    76
qed end
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    77
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    78
text{* Constant Vectors *} 
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    79
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    80
definition "vec x = (\<chi> i. x)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    81
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    82
text{* Also the scalar-vector multiplication. *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    83
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    84
definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    85
  where "c *s x = (\<chi> i. c * (x$i))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    86
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    87
subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    88
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    89
method_setup vector = {*
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    90
let
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    91
  val ss1 = HOL_basic_ss addsimps [@{thm setsum_addf} RS sym,
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    92
  @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib},
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    93
  @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
    94
  val ss2 = @{simpset} addsimps
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    95
             [@{thm plus_vec_def}, @{thm times_vec_def},
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    96
              @{thm minus_vec_def}, @{thm uminus_vec_def},
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    97
              @{thm one_vec_def}, @{thm zero_vec_def}, @{thm vec_def},
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    98
              @{thm scaleR_vec_def},
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
    99
              @{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}]
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   100
 fun vector_arith_tac ths =
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   101
   simp_tac ss1
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   102
   THEN' (fn i => rtac @{thm setsum_cong2} i
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   103
         ORELSE rtac @{thm setsum_0'} i
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   104
         ORELSE simp_tac (HOL_basic_ss addsimps [@{thm vec_eq_iff}]) i)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   105
   (* THEN' TRY o clarify_tac HOL_cs  THEN' (TRY o rtac @{thm iffI}) *)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   106
   THEN' asm_full_simp_tac (ss2 addsimps ths)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   107
 in
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   108
  Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths)))
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   109
 end
42814
5af15f1e2ef6 simplified/unified method_setup/attribute_setup;
wenzelm
parents: 40786
diff changeset
   110
*} "lift trivial vector statements to real arith statements"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   111
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   112
lemma vec_0[simp]: "vec 0 = 0" by (vector zero_vec_def)
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   113
lemma vec_1[simp]: "vec 1 = 1" by (vector one_vec_def)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   114
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   115
lemma vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   116
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   117
lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   118
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   119
lemma vec_add: "vec(x + y) = vec x + vec y"  by (vector vec_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   120
lemma vec_sub: "vec(x - y) = vec x - vec y" by (vector vec_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   121
lemma vec_cmul: "vec(c * x) = c *s vec x " by (vector vec_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   122
lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   123
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   124
lemma vec_setsum: assumes fS: "finite S"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   125
  shows "vec(setsum f S) = setsum (vec o f) S"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   126
  apply (induct rule: finite_induct[OF fS])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   127
  apply (simp)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   128
  apply (auto simp add: vec_add)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   129
  done
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   130
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   131
text{* Obvious "component-pushing". *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   132
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   133
lemma vec_component [simp]: "vec x $ i = x"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   134
  by (vector vec_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   135
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   136
lemma vector_mult_component [simp]: "(x * y)$i = x$i * y$i"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   137
  by vector
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   138
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   139
lemma vector_smult_component [simp]: "(c *s y)$i = c * (y$i)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   140
  by vector
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   141
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   142
lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   143
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   144
lemmas vector_component =
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   145
  vec_component vector_add_component vector_mult_component
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   146
  vector_smult_component vector_minus_component vector_uminus_component
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   147
  vector_scaleR_component cond_component
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   148
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   149
subsection {* Some frequently useful arithmetic lemmas over vectors. *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   150
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   151
instance vec :: (semigroup_mult, finite) semigroup_mult
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   152
  by default (vector mult_assoc)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   153
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   154
instance vec :: (monoid_mult, finite) monoid_mult
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   155
  by default vector+
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   156
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   157
instance vec :: (ab_semigroup_mult, finite) ab_semigroup_mult
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   158
  by default (vector mult_commute)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   159
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   160
instance vec :: (ab_semigroup_idem_mult, finite) ab_semigroup_idem_mult
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   161
  by default (vector mult_idem)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   162
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   163
instance vec :: (comm_monoid_mult, finite) comm_monoid_mult
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   164
  by default vector
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   165
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   166
instance vec :: (semiring, finite) semiring
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   167
  by default (vector field_simps)+
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   168
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   169
instance vec :: (semiring_0, finite) semiring_0
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   170
  by default (vector field_simps)+
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   171
instance vec :: (semiring_1, finite) semiring_1
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   172
  by default vector
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   173
instance vec :: (comm_semiring, finite) comm_semiring
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   174
  by default (vector field_simps)+
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
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 :: (comm_semiring_0, finite) comm_semiring_0 ..
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   177
instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   178
instance vec :: (semiring_0_cancel, finite) semiring_0_cancel ..
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   179
instance vec :: (comm_semiring_0_cancel, finite) comm_semiring_0_cancel ..
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   180
instance vec :: (ring, finite) ring ..
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   181
instance vec :: (semiring_1_cancel, finite) semiring_1_cancel ..
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   182
instance vec :: (comm_semiring_1, finite) comm_semiring_1 ..
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   183
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   184
instance vec :: (ring_1, finite) ring_1 ..
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   185
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   186
instance vec :: (real_algebra, finite) real_algebra
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   187
  apply intro_classes
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   188
  apply (simp_all add: vec_eq_iff)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   189
  done
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
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 :: (real_algebra_1, finite) real_algebra_1 ..
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   192
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   193
lemma of_nat_index:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   194
  "(of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   195
  apply (induct n)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   196
  apply vector
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   197
  apply vector
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   198
  done
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   199
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   200
lemma one_index[simp]:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   201
  "(1 :: 'a::one ^'n)$i = 1" by vector
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   202
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   203
instance vec :: (semiring_char_0, finite) semiring_char_0
38621
d6cb7e625d75 more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents: 37678
diff changeset
   204
proof
d6cb7e625d75 more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents: 37678
diff changeset
   205
  fix m n :: nat
d6cb7e625d75 more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents: 37678
diff changeset
   206
  show "inj (of_nat :: nat \<Rightarrow> 'a ^ 'b)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   207
    by (auto intro!: injI simp add: vec_eq_iff of_nat_index)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   208
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   209
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45031
diff changeset
   210
instance vec :: (numeral, finite) numeral ..
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45031
diff changeset
   211
instance vec :: (semiring_numeral, finite) semiring_numeral ..
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45031
diff changeset
   212
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45031
diff changeset
   213
lemma numeral_index [simp]: "numeral w $ i = numeral w"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45031
diff changeset
   214
  by (induct w, simp_all only: numeral.simps vector_add_component one_index)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45031
diff changeset
   215
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45031
diff changeset
   216
lemma neg_numeral_index [simp]: "neg_numeral w $ i = neg_numeral w"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45031
diff changeset
   217
  by (simp only: neg_numeral_def vector_uminus_component numeral_index)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45031
diff changeset
   218
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   219
instance vec :: (comm_ring_1, finite) comm_ring_1 ..
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   220
instance vec :: (ring_char_0, finite) ring_char_0 ..
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   221
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   222
lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   223
  by (vector mult_assoc)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   224
lemma vector_sadd_rdistrib: "((a::'a::semiring) + b) *s x = a *s x + b *s x"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   225
  by (vector field_simps)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   226
lemma vector_add_ldistrib: "(c::'a::semiring) *s (x + y) = c *s x + c *s y"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   227
  by (vector field_simps)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   228
lemma vector_smult_lzero[simp]: "(0::'a::mult_zero) *s x = 0" by vector
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   229
lemma vector_smult_lid[simp]: "(1::'a::monoid_mult) *s x = x" by vector
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   230
lemma vector_ssub_ldistrib: "(c::'a::ring) *s (x - y) = c *s x - c *s y"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   231
  by (vector field_simps)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   232
lemma vector_smult_rneg: "(c::'a::ring) *s -x = -(c *s x)" by vector
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   233
lemma vector_smult_lneg: "- (c::'a::ring) *s x = -(c *s x)" by vector
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45031
diff changeset
   234
lemma vector_sneg_minus1: "-x = (-1::'a::ring_1) *s x" by vector
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   235
lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   236
lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   237
  by (vector field_simps)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   238
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   239
lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   240
  by (simp add: vec_eq_iff)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   241
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   242
lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   243
lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   244
  by vector
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   245
lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   246
  by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   247
lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   248
  by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   249
lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==>  a *s x = a *s y ==> (x = y)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   250
  by (metis vector_mul_lcancel)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   251
lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   252
  by (metis vector_mul_rcancel)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   253
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   254
lemma component_le_norm_cart: "\<bar>x$i\<bar> <= norm x"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   255
  apply (simp add: norm_vec_def)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   256
  apply (rule member_le_setL2, simp_all)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   257
  done
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   258
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   259
lemma norm_bound_component_le_cart: "norm x <= e ==> \<bar>x$i\<bar> <= e"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   260
  by (metis component_le_norm_cart order_trans)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   261
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   262
lemma norm_bound_component_lt_cart: "norm x < e ==> \<bar>x$i\<bar> < e"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   263
  by (metis component_le_norm_cart basic_trans_rules(21))
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   264
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   265
lemma norm_le_l1_cart: "norm x <= setsum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   266
  by (simp add: norm_vec_def setL2_le_setsum)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   267
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   268
lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   269
  unfolding scaleR_vec_def vector_scalar_mult_def by simp
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   270
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   271
lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   272
  unfolding dist_norm scalar_mult_eq_scaleR
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   273
  unfolding scaleR_right_diff_distrib[symmetric] by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   274
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   275
lemma setsum_component [simp]:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   276
  fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   277
  shows "(setsum f S)$i = setsum (\<lambda>x. (f x)$i) S"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   278
  by (cases "finite S", induct S set: finite, simp_all)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   279
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   280
lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)$i ) S)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   281
  by (simp add: vec_eq_iff)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   282
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   283
lemma setsum_cmul:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   284
  fixes f:: "'c \<Rightarrow> ('a::semiring_1)^'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   285
  shows "setsum (\<lambda>x. c *s f x) S = c *s setsum f S"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   286
  by (simp add: vec_eq_iff setsum_right_distrib)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   287
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   288
(* TODO: use setsum_norm_allsubsets_bound *)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   289
lemma setsum_norm_allsubsets_bound_cart:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   290
  fixes f:: "'a \<Rightarrow> real ^'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   291
  assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   292
  shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) *  e"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   293
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   294
  let ?d = "real CARD('n)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   295
  let ?nf = "\<lambda>x. norm (f x)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   296
  let ?U = "UNIV :: 'n set"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   297
  have th0: "setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x $ i\<bar>) ?U) P = setsum (\<lambda>i. setsum (\<lambda>x. \<bar>f x $ i\<bar>) P) ?U"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   298
    by (rule setsum_commute)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   299
  have th1: "2 * ?d * e = of_nat (card ?U) * (2 * e)" by (simp add: real_of_nat_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   300
  have "setsum ?nf P \<le> setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x $ i\<bar>) ?U) P"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   301
    apply (rule setsum_mono)    by (rule norm_le_l1_cart)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   302
  also have "\<dots> \<le> 2 * ?d * e"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   303
    unfolding th0 th1
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   304
  proof(rule setsum_bounded)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   305
    fix i assume i: "i \<in> ?U"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   306
    let ?Pp = "{x. x\<in> P \<and> f x $ i \<ge> 0}"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   307
    let ?Pn = "{x. x \<in> P \<and> f x $ i < 0}"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   308
    have thp: "P = ?Pp \<union> ?Pn" by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   309
    have thp0: "?Pp \<inter> ?Pn ={}" by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   310
    have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   311
    have Ppe:"setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pp \<le> e"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   312
      using component_le_norm_cart[of "setsum (\<lambda>x. f x) ?Pp" i]  fPs[OF PpP]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   313
      by (auto intro: abs_le_D1)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   314
    have Pne: "setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn \<le> e"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   315
      using component_le_norm_cart[of "setsum (\<lambda>x. - f x) ?Pn" i]  fPs[OF PnP]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   316
      by (auto simp add: setsum_negf intro: abs_le_D1)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   317
    have "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P = setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   318
      apply (subst thp)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   319
      apply (rule setsum_Un_zero)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   320
      using fP thp0 by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   321
    also have "\<dots> \<le> 2*e" using Pne Ppe by arith
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   322
    finally show "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P \<le> 2*e" .
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   323
  qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   324
  finally show ?thesis .
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   325
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   326
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   327
lemma if_distr: "(if P then f else g) $ i = (if P then f $ i else g $ i)" by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   328
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   329
lemma split_dimensions'[consumes 1]:
44129
286bd57858b9 simplified definition of class euclidean_space;
huffman
parents: 44077
diff changeset
   330
  assumes "k < DIM('a::euclidean_space^'b)"
286bd57858b9 simplified definition of class euclidean_space;
huffman
parents: 44077
diff changeset
   331
  obtains i j where "i < CARD('b::finite)" and "j < DIM('a::euclidean_space)" and "k = j + i * DIM('a::euclidean_space)"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   332
using split_times_into_modulo[OF assms[simplified]] .
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   333
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   334
lemma cart_euclidean_bound[intro]:
44129
286bd57858b9 simplified definition of class euclidean_space;
huffman
parents: 44077
diff changeset
   335
  assumes j:"j < DIM('a::euclidean_space)"
286bd57858b9 simplified definition of class euclidean_space;
huffman
parents: 44077
diff changeset
   336
  shows "j + \<pi>' (i::'b::finite) * DIM('a) < CARD('b) * DIM('a::euclidean_space)"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   337
  using linear_less_than_times[OF pi'_range j, of i] .
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   338
44129
286bd57858b9 simplified definition of class euclidean_space;
huffman
parents: 44077
diff changeset
   339
lemma (in euclidean_space) forall_CARD_DIM:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   340
  "(\<forall>i<CARD('b) * DIM('a). P i) \<longleftrightarrow> (\<forall>(i::'b::finite) j. j<DIM('a) \<longrightarrow> P (j + \<pi>' i * DIM('a)))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   341
   (is "?l \<longleftrightarrow> ?r")
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   342
proof (safe elim!: split_times_into_modulo)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   343
  fix i :: 'b and j assume "j < DIM('a)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   344
  note linear_less_than_times[OF pi'_range[of i] this]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   345
  moreover assume "?l"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   346
  ultimately show "P (j + \<pi>' i * DIM('a))" by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   347
next
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   348
  fix i j assume "i < CARD('b)" "j < DIM('a)" and "?r"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   349
  from `?r`[rule_format, OF `j < DIM('a)`, of "\<pi> i"] `i < CARD('b)`
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   350
  show "P (j + i * DIM('a))" by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   351
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   352
44129
286bd57858b9 simplified definition of class euclidean_space;
huffman
parents: 44077
diff changeset
   353
lemma (in euclidean_space) exists_CARD_DIM:
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   354
  "(\<exists>i<CARD('b) * DIM('a). P i) \<longleftrightarrow> (\<exists>i::'b::finite. \<exists>j<DIM('a). P (j + \<pi>' i * DIM('a)))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   355
  using forall_CARD_DIM[where 'b='b, of "\<lambda>x. \<not> P x"] by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   356
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   357
lemma forall_CARD:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   358
  "(\<forall>i<CARD('b). P i) \<longleftrightarrow> (\<forall>i::'b::finite. P (\<pi>' i))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   359
  using forall_CARD_DIM[where 'a=real, of P] by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   360
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   361
lemma exists_CARD:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   362
  "(\<exists>i<CARD('b). P i) \<longleftrightarrow> (\<exists>i::'b::finite. P (\<pi>' i))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   363
  using exists_CARD_DIM[where 'a=real, of P] by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   364
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   365
lemmas cart_simps = forall_CARD_DIM exists_CARD_DIM forall_CARD exists_CARD
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   366
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   367
lemma cart_euclidean_nth[simp]:
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   368
  fixes x :: "('a::euclidean_space, 'b::finite) vec"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   369
  assumes j:"j < DIM('a)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   370
  shows "x $$ (j + \<pi>' i * DIM('a)) = x $ i $$ j"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   371
  unfolding euclidean_component_def inner_vec_def basis_eq_pi'[OF j] if_distrib cond_application_beta
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   372
  by (simp add: setsum_cases)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   373
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   374
lemma real_euclidean_nth:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   375
  fixes x :: "real^'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   376
  shows "x $$ \<pi>' i = (x $ i :: real)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   377
  using cart_euclidean_nth[where 'a=real, of 0 x i] by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   378
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   379
lemmas nth_conv_component = real_euclidean_nth[symmetric]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   380
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   381
lemma mult_split_eq:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   382
  fixes A :: nat assumes "x < A" "y < A"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   383
  shows "x + i * A = y + j * A \<longleftrightarrow> x = y \<and> i = j"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   384
proof
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   385
  assume *: "x + i * A = y + j * A"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   386
  { fix x y i j assume "i < j" "x < A" and *: "x + i * A = y + j * A"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   387
    hence "x + i * A < Suc i * A" using `x < A` by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   388
    also have "\<dots> \<le> j * A" using `i < j` unfolding mult_le_cancel2 by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   389
    also have "\<dots> \<le> y + j * A" by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   390
    finally have "i = j" using * by simp }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   391
  note eq = this
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   392
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   393
  have "i = j"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   394
  proof (cases rule: linorder_cases)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   395
    assume "i < j" from eq[OF this `x < A` *] show "i = j" by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   396
  next
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   397
    assume "j < i" from eq[OF this `y < A` *[symmetric]] show "i = j" by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   398
  qed simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   399
  thus "x = y \<and> i = j" using * by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   400
qed simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   401
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   402
instance vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   403
proof
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   404
  fix x y::"'a^'b"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   405
  show "(x \<le> y) = (\<forall>i<DIM(('a, 'b) vec). x $$ i \<le> y $$ i)"
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   406
    unfolding less_eq_vec_def apply(subst eucl_le) by (simp add: cart_simps)
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   407
  show"(x < y) = (\<forall>i<DIM(('a, 'b) vec). x $$ i < y $$ i)"
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   408
    unfolding less_vec_def apply(subst eucl_less) by (simp add: cart_simps)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   409
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   410
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   411
subsection{* Basis vectors in coordinate directions. *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   412
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   413
definition "cart_basis k = (\<chi> i. if i = k then 1 else 0)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   414
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   415
lemma basis_component [simp]: "cart_basis k $ i = (if k=i then 1 else 0)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   416
  unfolding cart_basis_def by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   417
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   418
lemma norm_basis[simp]:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   419
  shows "norm (cart_basis k :: real ^'n) = 1"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   420
  apply (simp add: cart_basis_def norm_eq_sqrt_inner) unfolding inner_vec_def
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   421
  apply (vector delta_mult_idempotent)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   422
  using setsum_delta[of "UNIV :: 'n set" "k" "\<lambda>k. 1::real"] by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   423
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   424
lemma norm_basis_1: "norm(cart_basis 1 :: real ^'n::{finite,one}) = 1"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   425
  by (rule norm_basis)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   426
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   427
lemma vector_choose_size: "0 <= c ==> \<exists>(x::real^'n). norm x = c"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   428
  by (rule exI[where x="c *\<^sub>R cart_basis arbitrary"]) simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   429
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   430
lemma vector_choose_dist: assumes e: "0 <= e"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   431
  shows "\<exists>(y::real^'n). dist x y = e"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   432
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   433
  from vector_choose_size[OF e] obtain c:: "real ^'n"  where "norm c = e"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   434
    by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   435
  then have "dist x (x - c) = e" by (simp add: dist_norm)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   436
  then show ?thesis by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   437
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   438
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   439
lemma basis_inj[intro]: "inj (cart_basis :: 'n \<Rightarrow> real ^'n)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   440
  by (simp add: inj_on_def vec_eq_iff)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   441
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   442
lemma basis_expansion:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   443
  "setsum (\<lambda>i. (x$i) *s cart_basis i) UNIV = (x::('a::ring_1) ^'n)" (is "?lhs = ?rhs" is "setsum ?f ?S = _")
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   444
  by (auto simp add: vec_eq_iff if_distrib setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   445
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   446
lemma smult_conv_scaleR: "c *s x = scaleR c x"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   447
  unfolding vector_scalar_mult_def scaleR_vec_def by simp
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   448
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   449
lemma basis_expansion':
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   450
  "setsum (\<lambda>i. (x$i) *\<^sub>R cart_basis i) UNIV = x"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   451
  by (rule basis_expansion [where 'a=real, unfolded smult_conv_scaleR])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   452
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   453
lemma basis_expansion_unique:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   454
  "setsum (\<lambda>i. f i *s cart_basis i) UNIV = (x::('a::comm_ring_1) ^'n) \<longleftrightarrow> (\<forall>i. f i = x$i)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   455
  by (simp add: vec_eq_iff setsum_delta if_distrib cong del: if_weak_cong)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   456
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   457
lemma dot_basis:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   458
  shows "cart_basis i \<bullet> x = x$i" "x \<bullet> (cart_basis i) = (x$i)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   459
  by (auto simp add: inner_vec_def cart_basis_def cond_application_beta if_distrib setsum_delta
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   460
           cong del: if_weak_cong)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   461
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   462
lemma inner_basis:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   463
  fixes x :: "'a::{real_inner, real_algebra_1} ^ 'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   464
  shows "inner (cart_basis i) x = inner 1 (x $ i)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   465
    and "inner x (cart_basis i) = inner (x $ i) 1"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   466
  unfolding inner_vec_def cart_basis_def
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   467
  by (auto simp add: cond_application_beta if_distrib setsum_delta cong del: if_weak_cong)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   468
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   469
lemma basis_eq_0: "cart_basis i = (0::'a::semiring_1^'n) \<longleftrightarrow> False"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   470
  by (auto simp add: vec_eq_iff)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   471
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   472
lemma basis_nonzero:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   473
  shows "cart_basis k \<noteq> (0:: 'a::semiring_1 ^'n)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   474
  by (simp add: basis_eq_0)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   475
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   476
text {* some lemmas to map between Eucl and Cart *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   477
lemma basis_real_n[simp]:"(basis (\<pi>' i)::real^'a) = cart_basis i"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   478
  unfolding basis_vec_def using pi'_range[where 'n='a]
44166
d12d89a66742 modify euclidean_space class to include basis set
huffman
parents: 44165
diff changeset
   479
  by (auto simp: vec_eq_iff axis_def)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   480
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   481
subsection {* Orthogonality on cartesian products *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   482
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   483
lemma orthogonal_basis:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   484
  shows "orthogonal (cart_basis i) x \<longleftrightarrow> x$i = (0::real)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   485
  by (auto simp add: orthogonal_def inner_vec_def cart_basis_def if_distrib
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   486
                     cond_application_beta setsum_delta cong del: if_weak_cong)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   487
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   488
lemma orthogonal_basis_basis:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   489
  shows "orthogonal (cart_basis i :: real^'n) (cart_basis j) \<longleftrightarrow> i \<noteq> j"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   490
  unfolding orthogonal_basis[of i] basis_component[of j] by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   491
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   492
subsection {* Linearity on cartesian products *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   493
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   494
lemma linear_vmul_component:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   495
  assumes lf: "linear f"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   496
  shows "linear (\<lambda>x. f x $ k *\<^sub>R v)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   497
  using lf
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   498
  by (auto simp add: linear_def algebra_simps)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   499
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   500
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   501
subsection{* Adjoints on cartesian products *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   502
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   503
text {* TODO: The following lemmas about adjoints should hold for any
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   504
Hilbert space (i.e. complete inner product space).
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   505
(see \url{http://en.wikipedia.org/wiki/Hermitian_adjoint})
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   506
*}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   507
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   508
lemma adjoint_works_lemma:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   509
  fixes f:: "real ^'n \<Rightarrow> real ^'m"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   510
  assumes lf: "linear f"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   511
  shows "\<forall>x y. f x \<bullet> y = x \<bullet> adjoint f y"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   512
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   513
  let ?N = "UNIV :: 'n set"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   514
  let ?M = "UNIV :: 'm set"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   515
  have fN: "finite ?N" by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   516
  have fM: "finite ?M" by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   517
  {fix y:: "real ^ 'm"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   518
    let ?w = "(\<chi> i. (f (cart_basis i) \<bullet> y)) :: real ^ 'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   519
    {fix x
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   520
      have "f x \<bullet> y = f (setsum (\<lambda>i. (x$i) *\<^sub>R cart_basis i) ?N) \<bullet> y"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   521
        by (simp only: basis_expansion')
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   522
      also have "\<dots> = (setsum (\<lambda>i. (x$i) *\<^sub>R f (cart_basis i)) ?N) \<bullet> y"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   523
        unfolding linear_setsum[OF lf fN]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   524
        by (simp add: linear_cmul[OF lf])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   525
      finally have "f x \<bullet> y = x \<bullet> ?w"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   526
        apply (simp only: )
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   527
        apply (simp add: inner_vec_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] field_simps)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   528
        done}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   529
  }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   530
  then show ?thesis unfolding adjoint_def
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   531
    some_eq_ex[of "\<lambda>f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y"]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   532
    using choice_iff[of "\<lambda>a b. \<forall>x. f x \<bullet> a = x \<bullet> b "]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   533
    by metis
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   534
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   535
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   536
lemma adjoint_works:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   537
  fixes f:: "real ^'n \<Rightarrow> real ^'m"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   538
  assumes lf: "linear f"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   539
  shows "x \<bullet> adjoint f y = f x \<bullet> y"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   540
  using adjoint_works_lemma[OF lf] by metis
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   541
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   542
lemma adjoint_linear:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   543
  fixes f:: "real ^'n \<Rightarrow> real ^'m"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   544
  assumes lf: "linear f"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   545
  shows "linear (adjoint f)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   546
  unfolding linear_def vector_eq_ldot[where 'a="real^'n", symmetric] apply safe
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   547
  unfolding inner_simps smult_conv_scaleR adjoint_works[OF lf] by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   548
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   549
lemma adjoint_clauses:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   550
  fixes f:: "real ^'n \<Rightarrow> real ^'m"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   551
  assumes lf: "linear f"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   552
  shows "x \<bullet> adjoint f y = f x \<bullet> y"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   553
  and "adjoint f y \<bullet> x = y \<bullet> f x"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   554
  by (simp_all add: adjoint_works[OF lf] inner_commute)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   555
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   556
lemma adjoint_adjoint:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   557
  fixes f:: "real ^'n \<Rightarrow> real ^'m"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   558
  assumes lf: "linear f"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   559
  shows "adjoint (adjoint f) = f"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   560
  by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   561
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   562
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   563
subsection {* Matrix operations *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   564
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   565
text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   566
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   567
definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"  (infixl "**" 70)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   568
  where "m ** m' == (\<chi> i j. setsum (\<lambda>k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   569
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   570
definition matrix_vector_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'm"  (infixl "*v" 70)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   571
  where "m *v x \<equiv> (\<chi> i. setsum (\<lambda>j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   572
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   573
definition vector_matrix_mult :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n "  (infixl "v*" 70)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   574
  where "v v* m == (\<chi> j. setsum (\<lambda>i. ((m$i)$j) * (v$i)) (UNIV :: 'm set)) :: 'a^'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   575
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   576
definition "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   577
definition transpose where 
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   578
  "(transpose::'a^'n^'m \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A$j)$i))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   579
definition "(row::'m => 'a ^'n^'m \<Rightarrow> 'a ^'n) i A = (\<chi> j. ((A$i)$j))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   580
definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A$i)$j))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   581
definition "rows(A::'a^'n^'m) = { row i A | i. i \<in> (UNIV :: 'm set)}"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   582
definition "columns(A::'a^'n^'m) = { column i A | i. i \<in> (UNIV :: 'n set)}"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   583
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   584
lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   585
lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   586
  by (vector matrix_matrix_mult_def setsum_addf[symmetric] field_simps)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   587
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   588
lemma matrix_mul_lid:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   589
  fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   590
  shows "mat 1 ** A = A"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   591
  apply (simp add: matrix_matrix_mult_def mat_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   592
  apply vector
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   593
  by (auto simp only: if_distrib cond_application_beta setsum_delta'[OF finite]  mult_1_left mult_zero_left if_True UNIV_I)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   594
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   595
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   596
lemma matrix_mul_rid:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   597
  fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   598
  shows "A ** mat 1 = A"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   599
  apply (simp add: matrix_matrix_mult_def mat_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   600
  apply vector
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   601
  by (auto simp only: if_distrib cond_application_beta setsum_delta[OF finite]  mult_1_right mult_zero_right if_True UNIV_I cong: if_cong)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   602
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   603
lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   604
  apply (vector matrix_matrix_mult_def setsum_right_distrib setsum_left_distrib mult_assoc)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   605
  apply (subst setsum_commute)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   606
  apply simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   607
  done
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   608
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   609
lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   610
  apply (vector matrix_matrix_mult_def matrix_vector_mult_def setsum_right_distrib setsum_left_distrib mult_assoc)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   611
  apply (subst setsum_commute)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   612
  apply simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   613
  done
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   614
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   615
lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   616
  apply (vector matrix_vector_mult_def mat_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   617
  by (simp add: if_distrib cond_application_beta
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   618
    setsum_delta' cong del: if_weak_cong)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   619
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   620
lemma matrix_transpose_mul: "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   621
  by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult_commute)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   622
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   623
lemma matrix_eq:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   624
  fixes A B :: "'a::semiring_1 ^ 'n ^ 'm"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   625
  shows "A = B \<longleftrightarrow>  (\<forall>x. A *v x = B *v x)" (is "?lhs \<longleftrightarrow> ?rhs")
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   626
  apply auto
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   627
  apply (subst vec_eq_iff)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   628
  apply clarify
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   629
  apply (clarsimp simp add: matrix_vector_mult_def cart_basis_def if_distrib cond_application_beta vec_eq_iff cong del: if_weak_cong)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   630
  apply (erule_tac x="cart_basis ia" in allE)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   631
  apply (erule_tac x="i" in allE)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   632
  by (auto simp add: cart_basis_def if_distrib cond_application_beta setsum_delta[OF finite] cong del: if_weak_cong)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   633
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   634
lemma matrix_vector_mul_component:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   635
  shows "((A::real^_^_) *v x)$k = (A$k) \<bullet> x"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   636
  by (simp add: matrix_vector_mult_def inner_vec_def)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   637
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   638
lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   639
  apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   640
  apply (subst setsum_commute)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   641
  by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   642
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   643
lemma transpose_mat: "transpose (mat n) = mat n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   644
  by (vector transpose_def mat_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   645
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   646
lemma transpose_transpose: "transpose(transpose A) = A"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   647
  by (vector transpose_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   648
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   649
lemma row_transpose:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   650
  fixes A:: "'a::semiring_1^_^_"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   651
  shows "row i (transpose A) = column i A"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   652
  by (simp add: row_def column_def transpose_def vec_eq_iff)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   653
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   654
lemma column_transpose:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   655
  fixes A:: "'a::semiring_1^_^_"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   656
  shows "column i (transpose A) = row i A"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   657
  by (simp add: row_def column_def transpose_def vec_eq_iff)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   658
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   659
lemma rows_transpose: "rows(transpose (A::'a::semiring_1^_^_)) = columns A"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   660
by (auto simp add: rows_def columns_def row_transpose intro: set_eqI)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   661
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   662
lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A" by (metis transpose_transpose rows_transpose)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   663
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   664
text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   665
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   666
lemma matrix_mult_dot: "A *v x = (\<chi> i. A$i \<bullet> x)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   667
  by (simp add: matrix_vector_mult_def inner_vec_def)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   668
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   669
lemma matrix_mult_vsum: "(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\<lambda>i. (x$i) *s column i A) (UNIV:: 'n set)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   670
  by (simp add: matrix_vector_mult_def vec_eq_iff column_def mult_commute)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   671
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   672
lemma vector_componentwise:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   673
  "(x::'a::ring_1^'n) = (\<chi> j. setsum (\<lambda>i. (x$i) * (cart_basis i :: 'a^'n)$j) (UNIV :: 'n set))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   674
  apply (subst basis_expansion[symmetric])
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   675
  by (vector vec_eq_iff setsum_component)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   676
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   677
lemma linear_componentwise:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   678
  fixes f:: "real ^'m \<Rightarrow> real ^ _"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   679
  assumes lf: "linear f"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   680
  shows "(f x)$j = setsum (\<lambda>i. (x$i) * (f (cart_basis i)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs")
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   681
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   682
  let ?M = "(UNIV :: 'm set)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   683
  let ?N = "(UNIV :: 'n set)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   684
  have fM: "finite ?M" by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   685
  have "?rhs = (setsum (\<lambda>i.(x$i) *\<^sub>R f (cart_basis i) ) ?M)$j"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   686
    unfolding vector_smult_component[symmetric] smult_conv_scaleR
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   687
    unfolding setsum_component[of "(\<lambda>i.(x$i) *\<^sub>R f (cart_basis i :: real^'m))" ?M]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   688
    ..
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   689
  then show ?thesis unfolding linear_setsum_mul[OF lf fM, symmetric] basis_expansion' ..
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   690
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   691
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   692
text{* Inverse matrices  (not necessarily square) *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   693
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   694
definition "invertible(A::'a::semiring_1^'n^'m) \<longleftrightarrow> (\<exists>A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   695
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   696
definition "matrix_inv(A:: 'a::semiring_1^'n^'m) =
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   697
        (SOME A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   698
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   699
text{* Correspondence between matrices and linear operators. *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   700
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   701
definition matrix:: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   702
where "matrix f = (\<chi> i j. (f(cart_basis j))$i)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   703
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   704
lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::real ^ _))"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   705
  by (simp add: linear_def matrix_vector_mult_def vec_eq_iff field_simps setsum_right_distrib setsum_addf)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   706
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   707
lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::real ^ 'n)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   708
apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult_commute)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   709
apply clarify
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   710
apply (rule linear_componentwise[OF lf, symmetric])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   711
done
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   712
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   713
lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::real ^ 'n))" by (simp add: ext matrix_works)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   714
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   715
lemma matrix_of_matrix_vector_mul: "matrix(\<lambda>x. A *v (x :: real ^ 'n)) = A"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   716
  by (simp add: matrix_eq matrix_vector_mul_linear matrix_works)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   717
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   718
lemma matrix_compose:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   719
  assumes lf: "linear (f::real^'n \<Rightarrow> real^'m)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   720
  and lg: "linear (g::real^'m \<Rightarrow> real^_)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   721
  shows "matrix (g o f) = matrix g ** matrix f"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   722
  using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   723
  by (simp  add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   724
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   725
lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   726
  by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult_commute)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   727
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   728
lemma adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   729
  apply (rule adjoint_unique)
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   730
  apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   731
  apply (subst setsum_commute)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   732
  apply (auto simp add: mult_ac)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   733
  done
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   734
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   735
lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   736
  shows "matrix(adjoint f) = transpose(matrix f)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   737
  apply (subst matrix_vector_mul[OF lf])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   738
  unfolding adjoint_matrix matrix_of_matrix_vector_mul ..
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   739
44360
ea609ebdeebf section -> subsection
huffman
parents: 44282
diff changeset
   740
subsection {* lambda skolemization on cartesian products *}
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   741
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   742
(* FIXME: rename do choice_cart *)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   743
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   744
lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
37494
6e9f48cf6adf Make latex happy
hoelzl
parents: 37489
diff changeset
   745
   (\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))" (is "?lhs \<longleftrightarrow> ?rhs")
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   746
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   747
  let ?S = "(UNIV :: 'n set)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   748
  {assume H: "?rhs"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   749
    then have ?lhs by auto}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   750
  moreover
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   751
  {assume H: "?lhs"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   752
    then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   753
    let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   754
    {fix i
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   755
      from f have "P i (f i)" by metis
37494
6e9f48cf6adf Make latex happy
hoelzl
parents: 37489
diff changeset
   756
      then have "P i (?x $ i)" by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   757
    }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   758
    hence "\<forall>i. P i (?x$i)" by metis
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   759
    hence ?rhs by metis }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   760
  ultimately show ?thesis by metis
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   761
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   762
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   763
subsection {* Standard bases are a spanning set, and obviously finite. *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   764
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   765
lemma span_stdbasis:"span {cart_basis i :: real^'n | i. i \<in> (UNIV :: 'n set)} = UNIV"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   766
apply (rule set_eqI)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   767
apply auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   768
apply (subst basis_expansion'[symmetric])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   769
apply (rule span_setsum)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   770
apply simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   771
apply auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   772
apply (rule span_mul)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   773
apply (rule span_superset)
44170
510ac30f44c0 make Multivariate_Analysis work with separate set type
huffman
parents: 44167
diff changeset
   774
apply auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   775
done
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   776
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   777
lemma finite_stdbasis: "finite {cart_basis i ::real^'n |i. i\<in> (UNIV:: 'n set)}" (is "finite ?S")
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   778
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   779
  have eq: "?S = cart_basis ` UNIV" by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   780
  show ?thesis unfolding eq by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   781
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   782
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   783
lemma card_stdbasis: "card {cart_basis i ::real^'n |i. i\<in> (UNIV :: 'n set)} = CARD('n)" (is "card ?S = _")
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   784
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   785
  have eq: "?S = cart_basis ` UNIV" by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   786
  show ?thesis unfolding eq using card_image[OF basis_inj] by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   787
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   788
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   789
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   790
lemma independent_stdbasis_lemma:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   791
  assumes x: "(x::real ^ 'n) \<in> span (cart_basis ` S)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   792
  and iS: "i \<notin> S"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   793
  shows "(x$i) = 0"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   794
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   795
  let ?U = "UNIV :: 'n set"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   796
  let ?B = "cart_basis ` S"
44170
510ac30f44c0 make Multivariate_Analysis work with separate set type
huffman
parents: 44167
diff changeset
   797
  let ?P = "{(x::real^_). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x$i =0}"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   798
 {fix x::"real^_" assume xS: "x\<in> ?B"
44170
510ac30f44c0 make Multivariate_Analysis work with separate set type
huffman
parents: 44167
diff changeset
   799
   from xS have "x \<in> ?P" by auto}
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   800
 moreover
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   801
 have "subspace ?P"
44170
510ac30f44c0 make Multivariate_Analysis work with separate set type
huffman
parents: 44167
diff changeset
   802
   by (auto simp add: subspace_def)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   803
 ultimately show ?thesis
44521
083eedb37a37 simplify many proofs about subspace and span;
huffman
parents: 44457
diff changeset
   804
   using x span_induct[of x ?B ?P] iS by blast
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   805
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   806
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   807
lemma independent_stdbasis: "independent {cart_basis i ::real^'n |i. i\<in> (UNIV :: 'n set)}"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   808
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   809
  let ?I = "UNIV :: 'n set"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   810
  let ?b = "cart_basis :: _ \<Rightarrow> real ^'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   811
  let ?B = "?b ` ?I"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   812
  have eq: "{?b i|i. i \<in> ?I} = ?B"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   813
    by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   814
  {assume d: "dependent ?B"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   815
    then obtain k where k: "k \<in> ?I" "?b k \<in> span (?B - {?b k})"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   816
      unfolding dependent_def by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   817
    have eq1: "?B - {?b k} = ?B - ?b ` {k}"  by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   818
    have eq2: "?B - {?b k} = ?b ` (?I - {k})"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   819
      unfolding eq1
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   820
      apply (rule inj_on_image_set_diff[symmetric])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   821
      apply (rule basis_inj) using k(1) by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   822
    from k(2) have th0: "?b k \<in> span (?b ` (?I - {k}))" unfolding eq2 .
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   823
    from independent_stdbasis_lemma[OF th0, of k, simplified]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   824
    have False by simp}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   825
  then show ?thesis unfolding eq dependent_def ..
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   826
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   827
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   828
lemma vector_sub_project_orthogonal_cart: "(b::real^'n) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *s b) = 0"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   829
  unfolding inner_simps smult_conv_scaleR by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   830
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   831
lemma linear_eq_stdbasis_cart:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   832
  assumes lf: "linear (f::real^'m \<Rightarrow> _)" and lg: "linear g"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   833
  and fg: "\<forall>i. f (cart_basis i) = g(cart_basis i)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   834
  shows "f = g"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   835
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   836
  let ?U = "UNIV :: 'm set"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   837
  let ?I = "{cart_basis i:: real^'m|i. i \<in> ?U}"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   838
  {fix x assume x: "x \<in> (UNIV :: (real^'m) set)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   839
    from equalityD2[OF span_stdbasis]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   840
    have IU: " (UNIV :: (real^'m) set) \<subseteq> span ?I" by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   841
    from linear_eq[OF lf lg IU] fg x
44170
510ac30f44c0 make Multivariate_Analysis work with separate set type
huffman
parents: 44167
diff changeset
   842
    have "f x = g x" unfolding Ball_def mem_Collect_eq by metis}
44457
d366fa5551ef declare euclidean_simps [simp] at the point they are proved;
huffman
parents: 44452
diff changeset
   843
  then show ?thesis by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   844
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   845
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   846
lemma bilinear_eq_stdbasis_cart:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   847
  assumes bf: "bilinear (f:: real^'m \<Rightarrow> real^'n \<Rightarrow> _)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   848
  and bg: "bilinear g"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   849
  and fg: "\<forall>i j. f (cart_basis i) (cart_basis j) = g (cart_basis i) (cart_basis j)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   850
  shows "f = g"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   851
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   852
  from fg have th: "\<forall>x \<in> {cart_basis i| i. i\<in> (UNIV :: 'm set)}. \<forall>y\<in>  {cart_basis j |j. j \<in> (UNIV :: 'n set)}. f x y = g x y" by blast
44457
d366fa5551ef declare euclidean_simps [simp] at the point they are proved;
huffman
parents: 44452
diff changeset
   853
  from bilinear_eq[OF bf bg equalityD2[OF span_stdbasis] equalityD2[OF span_stdbasis] th] show ?thesis by blast
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   854
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   855
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   856
lemma left_invertible_transpose:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   857
  "(\<exists>(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   858
  by (metis matrix_transpose_mul transpose_mat transpose_transpose)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   859
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   860
lemma right_invertible_transpose:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   861
  "(\<exists>(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). B ** A = mat 1)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   862
  by (metis matrix_transpose_mul transpose_mat transpose_transpose)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   863
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   864
lemma matrix_left_invertible_injective:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   865
"(\<exists>B. (B::real^'m^'n) ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x y. A *v x = A *v y \<longrightarrow> x = y)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   866
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   867
  {fix B:: "real^'m^'n" and x y assume B: "B ** A = mat 1" and xy: "A *v x = A*v y"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   868
    from xy have "B*v (A *v x) = B *v (A*v y)" by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   869
    hence "x = y"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   870
      unfolding matrix_vector_mul_assoc B matrix_vector_mul_lid .}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   871
  moreover
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   872
  {assume A: "\<forall>x y. A *v x = A *v y \<longrightarrow> x = y"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   873
    hence i: "inj (op *v A)" unfolding inj_on_def by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   874
    from linear_injective_left_inverse[OF matrix_vector_mul_linear i]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   875
    obtain g where g: "linear g" "g o op *v A = id" by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   876
    have "matrix g ** A = mat 1"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   877
      unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
44165
d26a45f3c835 remove lemma stupid_ext
huffman
parents: 44140
diff changeset
   878
      using g(2) by (simp add: fun_eq_iff)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   879
    then have "\<exists>B. (B::real ^'m^'n) ** A = mat 1" by blast}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   880
  ultimately show ?thesis by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   881
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   882
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   883
lemma matrix_left_invertible_ker:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   884
  "(\<exists>B. (B::real ^'m^'n) ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x. A *v x = 0 \<longrightarrow> x = 0)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   885
  unfolding matrix_left_invertible_injective
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   886
  using linear_injective_0[OF matrix_vector_mul_linear, of A]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   887
  by (simp add: inj_on_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   888
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   889
lemma matrix_right_invertible_surjective:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   890
"(\<exists>B. (A::real^'n^'m) ** (B::real^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   891
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   892
  {fix B :: "real ^'m^'n"  assume AB: "A ** B = mat 1"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   893
    {fix x :: "real ^ 'm"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   894
      have "A *v (B *v x) = x"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   895
        by (simp add: matrix_vector_mul_lid matrix_vector_mul_assoc AB)}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   896
    hence "surj (op *v A)" unfolding surj_def by metis }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   897
  moreover
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   898
  {assume sf: "surj (op *v A)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   899
    from linear_surjective_right_inverse[OF matrix_vector_mul_linear sf]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   900
    obtain g:: "real ^'m \<Rightarrow> real ^'n" where g: "linear g" "op *v A o g = id"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   901
      by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   902
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   903
    have "A ** (matrix g) = mat 1"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   904
      unfolding matrix_eq  matrix_vector_mul_lid
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   905
        matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
44165
d26a45f3c835 remove lemma stupid_ext
huffman
parents: 44140
diff changeset
   906
      using g(2) unfolding o_def fun_eq_iff id_def
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   907
      .
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   908
    hence "\<exists>B. A ** (B::real^'m^'n) = mat 1" by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   909
  }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   910
  ultimately show ?thesis unfolding surj_def by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   911
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   912
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   913
lemma matrix_left_invertible_independent_columns:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   914
  fixes A :: "real^'n^'m"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   915
  shows "(\<exists>(B::real ^'m^'n). B ** A = mat 1) \<longleftrightarrow> (\<forall>c. setsum (\<lambda>i. c i *s column i A) (UNIV :: 'n set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   916
   (is "?lhs \<longleftrightarrow> ?rhs")
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   917
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   918
  let ?U = "UNIV :: 'n set"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   919
  {assume k: "\<forall>x. A *v x = 0 \<longrightarrow> x = 0"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   920
    {fix c i assume c: "setsum (\<lambda>i. c i *s column i A) ?U = 0"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   921
      and i: "i \<in> ?U"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   922
      let ?x = "\<chi> i. c i"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   923
      have th0:"A *v ?x = 0"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   924
        using c
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   925
        unfolding matrix_mult_vsum vec_eq_iff
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   926
        by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   927
      from k[rule_format, OF th0] i
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
   928
      have "c i = 0" by (vector vec_eq_iff)}
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   929
    hence ?rhs by blast}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   930
  moreover
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   931
  {assume H: ?rhs
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   932
    {fix x assume x: "A *v x = 0"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   933
      let ?c = "\<lambda>i. ((x$i ):: real)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   934
      from H[rule_format, of ?c, unfolded matrix_mult_vsum[symmetric], OF x]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   935
      have "x = 0" by vector}}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   936
  ultimately show ?thesis unfolding matrix_left_invertible_ker by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   937
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   938
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   939
lemma matrix_right_invertible_independent_rows:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   940
  fixes A :: "real^'n^'m"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   941
  shows "(\<exists>(B::real^'m^'n). A ** B = mat 1) \<longleftrightarrow> (\<forall>c. setsum (\<lambda>i. c i *s row i A) (UNIV :: 'm set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   942
  unfolding left_invertible_transpose[symmetric]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   943
    matrix_left_invertible_independent_columns
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   944
  by (simp add: column_transpose)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   945
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   946
lemma matrix_right_invertible_span_columns:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   947
  "(\<exists>(B::real ^'n^'m). (A::real ^'m^'n) ** B = mat 1) \<longleftrightarrow> span (columns A) = UNIV" (is "?lhs = ?rhs")
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   948
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   949
  let ?U = "UNIV :: 'm set"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   950
  have fU: "finite ?U" by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   951
  have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::real^'m). setsum (\<lambda>i. (x$i) *s column i A) ?U = y)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   952
    unfolding matrix_right_invertible_surjective matrix_mult_vsum surj_def
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   953
    apply (subst eq_commute) ..
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   954
  have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> span (columns A))" by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   955
  {assume h: ?lhs
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   956
    {fix x:: "real ^'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   957
        from h[unfolded lhseq, rule_format, of x] obtain y:: "real ^'m"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   958
          where y: "setsum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   959
        have "x \<in> span (columns A)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   960
          unfolding y[symmetric]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   961
          apply (rule span_setsum[OF fU])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   962
          apply clarify
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   963
          unfolding smult_conv_scaleR
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   964
          apply (rule span_mul)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   965
          apply (rule span_superset)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   966
          unfolding columns_def
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   967
          by blast}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   968
    then have ?rhs unfolding rhseq by blast}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   969
  moreover
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   970
  {assume h:?rhs
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   971
    let ?P = "\<lambda>(y::real ^'n). \<exists>(x::real^'m). setsum (\<lambda>i. (x$i) *s column i A) ?U = y"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   972
    {fix y have "?P y"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   973
      proof(rule span_induct_alt[of ?P "columns A", folded smult_conv_scaleR])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   974
        show "\<exists>x\<Colon>real ^ 'm. setsum (\<lambda>i. (x$i) *s column i A) ?U = 0"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   975
          by (rule exI[where x=0], simp)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   976
      next
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   977
        fix c y1 y2 assume y1: "y1 \<in> columns A" and y2: "?P y2"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   978
        from y1 obtain i where i: "i \<in> ?U" "y1 = column i A"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   979
          unfolding columns_def by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   980
        from y2 obtain x:: "real ^'m" where
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   981
          x: "setsum (\<lambda>i. (x$i) *s column i A) ?U = y2" by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   982
        let ?x = "(\<chi> j. if j = i then c + (x$i) else (x$j))::real^'m"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   983
        show "?P (c*s y1 + y2)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   984
          proof(rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib right_distrib cond_application_beta cong del: if_weak_cong)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   985
            fix j
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   986
            have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   987
           else (x$xa) * ((column xa A$j))) = (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))" using i(1)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   988
              by (simp add: field_simps)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   989
            have "setsum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   990
           else (x$xa) * ((column xa A$j))) ?U = setsum (\<lambda>xa. (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))) ?U"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   991
              apply (rule setsum_cong[OF refl])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   992
              using th by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   993
            also have "\<dots> = setsum (\<lambda>xa. if xa = i then c * ((column i A)$j) else 0) ?U + setsum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   994
              by (simp add: setsum_addf)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   995
            also have "\<dots> = c * ((column i A)$j) + setsum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   996
              unfolding setsum_delta[OF fU]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   997
              using i(1) by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   998
            finally show "setsum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
   999
           else (x$xa) * ((column xa A$j))) ?U = c * ((column i A)$j) + setsum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" .
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1000
          qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1001
        next
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1002
          show "y \<in> span (columns A)" unfolding h by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1003
        qed}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1004
    then have ?lhs unfolding lhseq ..}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1005
  ultimately show ?thesis by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1006
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1007
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1008
lemma matrix_left_invertible_span_rows:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1009
  "(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1010
  unfolding right_invertible_transpose[symmetric]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1011
  unfolding columns_transpose[symmetric]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1012
  unfolding matrix_right_invertible_span_columns
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1013
 ..
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1014
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1015
text {* The same result in terms of square matrices. *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1016
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1017
lemma matrix_left_right_inverse:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1018
  fixes A A' :: "real ^'n^'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1019
  shows "A ** A' = mat 1 \<longleftrightarrow> A' ** A = mat 1"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1020
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1021
  {fix A A' :: "real ^'n^'n" assume AA': "A ** A' = mat 1"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1022
    have sA: "surj (op *v A)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1023
      unfolding surj_def
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1024
      apply clarify
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1025
      apply (rule_tac x="(A' *v y)" in exI)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1026
      by (simp add: matrix_vector_mul_assoc AA' matrix_vector_mul_lid)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1027
    from linear_surjective_isomorphism[OF matrix_vector_mul_linear sA]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1028
    obtain f' :: "real ^'n \<Rightarrow> real ^'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1029
      where f': "linear f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1030
    have th: "matrix f' ** A = mat 1"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1031
      by (simp add: matrix_eq matrix_works[OF f'(1)] matrix_vector_mul_assoc[symmetric] matrix_vector_mul_lid f'(2)[rule_format])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1032
    hence "(matrix f' ** A) ** A' = mat 1 ** A'" by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1033
    hence "matrix f' = A'" by (simp add: matrix_mul_assoc[symmetric] AA' matrix_mul_rid matrix_mul_lid)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1034
    hence "matrix f' ** A = A' ** A" by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1035
    hence "A' ** A = mat 1" by (simp add: th)}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1036
  then show ?thesis by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1037
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1038
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1039
text {* Considering an n-element vector as an n-by-1 or 1-by-n matrix. *}
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1040
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1041
definition "rowvector v = (\<chi> i j. (v$j))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1042
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1043
definition "columnvector v = (\<chi> i j. (v$i))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1044
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1045
lemma transpose_columnvector:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1046
 "transpose(columnvector v) = rowvector v"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
  1047
  by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1048
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1049
lemma transpose_rowvector: "transpose(rowvector v) = columnvector v"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
  1050
  by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1051
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1052
lemma dot_rowvector_columnvector:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1053
  "columnvector (A *v v) = A ** columnvector v"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1054
  by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1055
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1056
lemma dot_matrix_product: "(x::real^'n) \<bullet> y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
  1057
  by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1058
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1059
lemma dot_matrix_vector_mul:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1060
  fixes A B :: "real ^'n ^'n" and x y :: "real ^'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1061
  shows "(A *v x) \<bullet> (B *v y) =
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1062
      (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1063
unfolding dot_matrix_product transpose_columnvector[symmetric]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1064
  dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1065
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1066
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1067
lemma infnorm_cart:"infnorm (x::real^'n) = Sup {abs(x$i) |i. i\<in> (UNIV :: 'n set)}"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1068
  unfolding infnorm_def apply(rule arg_cong[where f=Sup]) apply safe
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1069
  apply(rule_tac x="\<pi> i" in exI) defer
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1070
  apply(rule_tac x="\<pi>' i" in exI) unfolding nth_conv_component using pi'_range by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1071
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1072
lemma infnorm_set_image_cart:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1073
  "{abs(x$i) |i. i\<in> (UNIV :: _ set)} =
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1074
  (\<lambda>i. abs(x$i)) ` (UNIV)" by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1075
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1076
lemma infnorm_set_lemma_cart:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1077
  shows "finite {abs((x::'a::abs ^'n)$i) |i. i\<in> (UNIV :: 'n set)}"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1078
  and "{abs(x$i) |i. i\<in> (UNIV :: 'n::finite set)} \<noteq> {}"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1079
  unfolding  infnorm_set_image_cart
40786
0a54cfc9add3 gave more standard finite set rules simp and intro attribute
nipkow
parents: 39302
diff changeset
  1080
  by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1081
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1082
lemma component_le_infnorm_cart:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1083
  shows "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1084
  unfolding nth_conv_component
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1085
  using component_le_infnorm[of x] .
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1086
44647
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44571
diff changeset
  1087
lemma continuous_component:
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44571
diff changeset
  1088
  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x $ i)"
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44571
diff changeset
  1089
  unfolding continuous_def by (rule tendsto_vec_nth)
44213
6fb54701a11b add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
huffman
parents: 44211
diff changeset
  1090
44647
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44571
diff changeset
  1091
lemma continuous_on_component:
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44571
diff changeset
  1092
  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x $ i)"
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44571
diff changeset
  1093
  unfolding continuous_on_def by (fast intro: tendsto_vec_nth)
44213
6fb54701a11b add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
huffman
parents: 44211
diff changeset
  1094
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1095
lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
44233
aa74ce315bae add simp rules for isCont
huffman
parents: 44219
diff changeset
  1096
  by (simp add: Collect_all_eq closed_INT closed_Collect_le)
44213
6fb54701a11b add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
huffman
parents: 44211
diff changeset
  1097
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1098
lemma bounded_component_cart: "bounded s \<Longrightarrow> bounded ((\<lambda>x. x $ i) ` s)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1099
unfolding bounded_def
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1100
apply clarify
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1101
apply (rule_tac x="x $ i" in exI)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1102
apply (rule_tac x="e" in exI)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1103
apply clarify
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
  1104
apply (rule order_trans [OF dist_vec_nth_le], simp)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1105
done
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1106
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1107
lemma compact_lemma_cart:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1108
  fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1109
  assumes "bounded s" and "\<forall>n. f n \<in> s"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1110
  shows "\<forall>d.
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1111
        \<exists>l r. subseq r \<and>
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1112
        (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1113
proof
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1114
  fix d::"'n set" have "finite d" by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1115
  thus "\<exists>l::'a ^ 'n. \<exists>r. subseq r \<and>
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1116
      (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1117
  proof(induct d) case empty thus ?case unfolding subseq_def by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1118
  next case (insert k d)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1119
    have s': "bounded ((\<lambda>x. x $ k) ` s)" using `bounded s` by (rule bounded_component_cart)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1120
    obtain l1::"'a^'n" and r1 where r1:"subseq r1" and lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1121
      using insert(3) by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1122
    have f': "\<forall>n. f (r1 n) $ k \<in> (\<lambda>x. x $ k) ` s" using `\<forall>n. f n \<in> s` by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1123
    obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) $ k) ---> l2) sequentially"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1124
      using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1125
    def r \<equiv> "r1 \<circ> r2" have r:"subseq r"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1126
      using r1 and r2 unfolding r_def o_def subseq_def by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1127
    moreover
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1128
    def l \<equiv> "(\<chi> i. if i = k then l2 else l1$i)::'a^'n"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1129
    { fix e::real assume "e>0"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1130
      from lr1 `e>0` have N1:"eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially" by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1131
      from lr2 `e>0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) $ k) l2 < e) sequentially" by (rule tendstoD)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1132
      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) $ i) (l1 $ i) < e) sequentially"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1133
        by (rule eventually_subseq)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1134
      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) $ i) (l $ i) < e) sequentially"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1135
        using N1' N2 by (rule eventually_elim2, simp add: l_def r_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1136
    }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1137
    ultimately show ?case by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1138
  qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1139
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1140
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
  1141
instance vec :: (heine_borel, finite) heine_borel
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1142
proof
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1143
  fix s :: "('a ^ 'b) set" and f :: "nat \<Rightarrow> 'a ^ 'b"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1144
  assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1145
  then obtain l r where r: "subseq r"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1146
    and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) $ i) (l $ i) < e) sequentially"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1147
    using compact_lemma_cart [OF s f] by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1148
  let ?d = "UNIV::'b set"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1149
  { fix e::real assume "e>0"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1150
    hence "0 < e / (real_of_nat (card ?d))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1151
      using zero_less_card_finite using divide_pos_pos[of e, of "real_of_nat (card ?d)"] by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1152
    with l have "eventually (\<lambda>n. \<forall>i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))) sequentially"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1153
      by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1154
    moreover
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1155
    { fix n assume n: "\<forall>i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1156
      have "dist (f (r n)) l \<le> (\<Sum>i\<in>?d. dist (f (r n) $ i) (l $ i))"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
  1157
        unfolding dist_vec_def using zero_le_dist by (rule setL2_le_setsum)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1158
      also have "\<dots> < (\<Sum>i\<in>?d. e / (real_of_nat (card ?d)))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1159
        by (rule setsum_strict_mono) (simp_all add: n)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1160
      finally have "dist (f (r n)) l < e" by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1161
    }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1162
    ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1163
      by (rule eventually_elim1)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1164
  }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1165
  hence *:"((f \<circ> r) ---> l) sequentially" unfolding o_def tendsto_iff by simp
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1166
  with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1167
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1168
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1169
lemma interval_cart: fixes a :: "'a::ord^'n" shows
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1170
  "{a <..< b} = {x::'a^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}" and
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1171
  "{a .. b} = {x::'a^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
  1172
  by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1173
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1174
lemma mem_interval_cart: fixes a :: "'a::ord^'n" shows
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1175
  "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1176
  "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 44135
diff changeset
  1177
  using interval_cart[of a b] by(auto simp add: set_eq_iff less_vec_def less_eq_vec_def)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1178
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1179
lemma interval_eq_empty_cart: fixes a :: "real^'n" shows
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1180
 "({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1) and
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1181
 "({a  ..  b} = {} \<longleftrightarrow> (\<exists>i. b$i < a$i))" (is ?th2)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1182
proof-
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1183
  { fix i x assume as:"b$i \<le> a$i" and x:"x\<in>{a <..< b}"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1184
    hence "a $ i < x $ i \<and> x $ i < b $ i" unfolding mem_interval_cart by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1185
    hence "a$i < b$i" by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1186
    hence False using as by auto  }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1187
  moreover
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1188
  { assume as:"\<forall>i. \<not> (b$i \<le> a$i)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1189
    let ?x = "(1/2) *\<^sub>R (a + b)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1190
    { fix i
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1191
      have "a$i < b$i" using as[THEN spec[where x=i]] by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1192
      hence "a$i < ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i < b$i"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1193
        unfolding vector_smult_component and vector_add_component
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1194
        by auto  }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1195
    hence "{a <..< b} \<noteq> {}" using mem_interval_cart(1)[of "?x" a b] by auto  }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1196
  ultimately show ?th1 by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1197
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1198
  { fix i x assume as:"b$i < a$i" and x:"x\<in>{a .. b}"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1199
    hence "a $ i \<le> x $ i \<and> x $ i \<le> b $ i" unfolding mem_interval_cart by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1200
    hence "a$i \<le> b$i" by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1201
    hence False using as by auto  }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1202
  moreover
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1203
  { assume as:"\<forall>i. \<not> (b$i < a$i)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1204
    let ?x = "(1/2) *\<^sub>R (a + b)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1205
    { fix i
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1206
      have "a$i \<le> b$i" using as[THEN spec[where x=i]] by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1207
      hence "a$i \<le> ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i \<le> b$i"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1208
        unfolding vector_smult_component and vector_add_component
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1209
        by auto  }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1210
    hence "{a .. b} \<noteq> {}" using mem_interval_cart(2)[of "?x" a b] by auto  }
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1211
  ultimately show ?th2 by blast
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1212
qed
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1213
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1214
lemma interval_ne_empty_cart: fixes a :: "real^'n" shows
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1215
  "{a  ..  b} \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i \<le> b$i)" and
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1216
  "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i < b$i)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1217
  unfolding interval_eq_empty_cart[of a b] by (auto simp add: not_less not_le)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff changeset
  1218
    (* BH: Why doesn't just "auto" work here? *)