src/HOL/Modules.thy
author wenzelm
Mon, 12 Apr 2021 14:14:47 +0200
changeset 73563 55b66a45bc94
parent 70817 dd675800469d
child 80932 261cd8722677
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
68189
6163c90694ef tuned headers;
wenzelm
parents: 68074
diff changeset
     1
(*  Title:      HOL/Modules.thy
6163c90694ef tuned headers;
wenzelm
parents: 68074
diff changeset
     2
    Author:     Amine Chaieb, University of Cambridge
6163c90694ef tuned headers;
wenzelm
parents: 68074
diff changeset
     3
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
6163c90694ef tuned headers;
wenzelm
parents: 68074
diff changeset
     4
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
6163c90694ef tuned headers;
wenzelm
parents: 68074
diff changeset
     5
    Author:     Johannes Hölzl, VU Amsterdam
6163c90694ef tuned headers;
wenzelm
parents: 68074
diff changeset
     6
    Author:     Fabian Immler, TUM
68072
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
     7
*)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
     8
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
     9
section \<open>Modules\<close>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    10
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    11
text \<open>Bases of a linear algebra based on modules (i.e. vector spaces of rings). \<close>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    12
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    13
theory Modules
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    14
  imports Hull
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    15
begin
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    16
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    17
subsection \<open>Locale for additive functions\<close>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    18
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    19
locale additive =
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    20
  fixes f :: "'a::ab_group_add \<Rightarrow> 'b::ab_group_add"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    21
  assumes add: "f (x + y) = f x + f y"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    22
begin
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    23
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    24
lemma zero: "f 0 = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    25
proof -
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    26
  have "f 0 = f (0 + 0)" by simp
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    27
  also have "\<dots> = f 0 + f 0" by (rule add)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    28
  finally show "f 0 = 0" by simp
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    29
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    30
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    31
lemma minus: "f (- x) = - f x"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    32
proof -
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    33
  have "f (- x) + f x = f (- x + x)" by (rule add [symmetric])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    34
  also have "\<dots> = - f x + f x" by (simp add: zero)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    35
  finally show "f (- x) = - f x" by (rule add_right_imp_eq)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    36
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    37
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    38
lemma diff: "f (x - y) = f x - f y"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    39
  using add [of x "- y"] by (simp add: minus)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    40
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    41
lemma sum: "f (sum g A) = (\<Sum>x\<in>A. f (g x))"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    42
  by (induct A rule: infinite_finite_induct) (simp_all add: zero add)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    43
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    44
end
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    45
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    46
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    47
text \<open>Modules form the central spaces in linear algebra. They are a generalization from vector
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    48
spaces by replacing the scalar field by a scalar ring.\<close>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    49
locale module =
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    50
  fixes scale :: "'a::comm_ring_1 \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
70817
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70802
diff changeset
    51
  assumes scale_right_distrib [algebra_simps, algebra_split_simps]:
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70802
diff changeset
    52
      "a *s (x + y) = a *s x + a *s y"
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70802
diff changeset
    53
    and scale_left_distrib [algebra_simps, algebra_split_simps]:
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70802
diff changeset
    54
      "(a + b) *s x = a *s x + b *s x"
68072
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    55
    and scale_scale [simp]: "a *s (b *s x) = (a * b) *s x"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    56
    and scale_one [simp]: "1 *s x = x"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    57
begin
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    58
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    59
lemma scale_left_commute: "a *s (b *s x) = b *s (a *s x)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    60
  by (simp add: mult.commute)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    61
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    62
lemma scale_zero_left [simp]: "0 *s x = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    63
  and scale_minus_left [simp]: "(- a) *s x = - (a *s x)"
70817
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70802
diff changeset
    64
  and scale_left_diff_distrib [algebra_simps, algebra_split_simps]:
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70802
diff changeset
    65
    "(a - b) *s x = a *s x - b *s x"
68072
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    66
  and scale_sum_left: "(sum f A) *s x = (\<Sum>a\<in>A. (f a) *s x)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    67
proof -
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    68
  interpret s: additive "\<lambda>a. a *s x"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    69
    by standard (rule scale_left_distrib)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    70
  show "0 *s x = 0" by (rule s.zero)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    71
  show "(- a) *s x = - (a *s x)" by (rule s.minus)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    72
  show "(a - b) *s x = a *s x - b *s x" by (rule s.diff)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    73
  show "(sum f A) *s x = (\<Sum>a\<in>A. (f a) *s x)" by (rule s.sum)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    74
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    75
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    76
lemma scale_zero_right [simp]: "a *s 0 = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    77
  and scale_minus_right [simp]: "a *s (- x) = - (a *s x)"
70817
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70802
diff changeset
    78
  and scale_right_diff_distrib [algebra_simps, algebra_split_simps]: 
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70802
diff changeset
    79
    "a *s (x - y) = a *s x - a *s y"
68072
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    80
  and scale_sum_right: "a *s (sum f A) = (\<Sum>x\<in>A. a *s (f x))"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    81
proof -
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    82
  interpret s: additive "\<lambda>x. a *s x"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    83
    by standard (rule scale_right_distrib)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    84
  show "a *s 0 = 0" by (rule s.zero)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    85
  show "a *s (- x) = - (a *s x)" by (rule s.minus)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    86
  show "a *s (x - y) = a *s x - a *s y" by (rule s.diff)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    87
  show "a *s (sum f A) = (\<Sum>x\<in>A. a *s (f x))" by (rule s.sum)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    88
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    89
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    90
lemma sum_constant_scale: "(\<Sum>x\<in>A. y) = scale (of_nat (card A)) y"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    91
  by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
    92
70802
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
    93
end
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
    94
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
    95
setup \<open>Sign.add_const_constraint (\<^const_name>\<open>divide\<close>, SOME \<^typ>\<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>)\<close>
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
    96
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
    97
context module
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
    98
begin
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
    99
70817
dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents: 70802
diff changeset
   100
lemma [field_simps, field_split_simps]:
70802
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
   101
  shows scale_left_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a + b) *s x = a *s x + b *s x"
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
   102
    and scale_right_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a *s (x + y) = a *s x + a *s y"
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
   103
    and scale_left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a - b) *s x = a *s x - b *s x"
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
   104
    and scale_right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a *s (x - y) = a *s x - a *s y"
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
   105
  by (rule scale_left_distrib scale_right_distrib scale_left_diff_distrib scale_right_diff_distrib)+
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
   106
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
   107
end
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
   108
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
   109
setup \<open>Sign.add_const_constraint (\<^const_name>\<open>divide\<close>, SOME \<^typ>\<open>'a::divide \<Rightarrow> 'a \<Rightarrow> 'a\<close>)\<close>
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
   110
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
   111
68072
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   112
section \<open>Subspace\<close>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   113
70802
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
   114
context module
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
   115
begin
160eaf566bcb formally augmented corresponding rules for field_simps
haftmann
parents: 69064
diff changeset
   116
68072
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   117
definition subspace :: "'b set \<Rightarrow> bool"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   118
  where "subspace S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>x\<in>S. \<forall>y\<in>S. x + y \<in> S) \<and> (\<forall>c. \<forall>x\<in>S. c *s x \<in> S)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   119
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   120
lemma subspaceI:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   121
  "0 \<in> S \<Longrightarrow> (\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S) \<Longrightarrow> (\<And>c x. x \<in> S \<Longrightarrow> c *s x \<in> S) \<Longrightarrow> subspace S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   122
  by (auto simp: subspace_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   123
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   124
lemma subspace_UNIV[simp]: "subspace UNIV"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   125
  by (simp add: subspace_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   126
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   127
lemma subspace_single_0[simp]: "subspace {0}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   128
  by (simp add: subspace_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   129
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   130
lemma subspace_0: "subspace S \<Longrightarrow> 0 \<in> S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   131
  by (metis subspace_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   132
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   133
lemma subspace_add: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   134
  by (metis subspace_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   135
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   136
lemma subspace_scale: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> c *s x \<in> S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   137
  by (metis subspace_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   138
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   139
lemma subspace_neg: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> - x \<in> S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   140
  by (metis scale_minus_left scale_one subspace_scale)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   141
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   142
lemma subspace_diff: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   143
  by (metis diff_conv_add_uminus subspace_add subspace_neg)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   144
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   145
lemma subspace_sum: "subspace A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<in> A) \<Longrightarrow> sum f B \<in> A"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   146
  by (induct B rule: infinite_finite_induct) (auto simp add: subspace_add subspace_0)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   147
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   148
lemma subspace_Int: "(\<And>i. i \<in> I \<Longrightarrow> subspace (s i)) \<Longrightarrow> subspace (\<Inter>i\<in>I. s i)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   149
  by (auto simp: subspace_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   150
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   151
lemma subspace_Inter: "\<forall>s \<in> f. subspace s \<Longrightarrow> subspace (\<Inter>f)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   152
  unfolding subspace_def by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   153
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   154
lemma subspace_inter: "subspace A \<Longrightarrow> subspace B \<Longrightarrow> subspace (A \<inter> B)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   155
  by (simp add: subspace_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   156
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   157
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   158
section \<open>Span: subspace generated by a set\<close>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   159
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   160
definition span :: "'b set \<Rightarrow> 'b set"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   161
  where span_explicit: "span b = {(\<Sum>a\<in>t. r a *s  a) | t r. finite t \<and> t \<subseteq> b}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   162
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   163
lemma span_explicit':
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   164
  "span b = {(\<Sum>v | f v \<noteq> 0. f v *s v) | f. finite {v. f v \<noteq> 0} \<and> (\<forall>v. f v \<noteq> 0 \<longrightarrow> v \<in> b)}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   165
  unfolding span_explicit
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   166
proof safe
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   167
  fix t r assume "finite t" "t \<subseteq> b"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   168
  then show "\<exists>f. (\<Sum>a\<in>t. r a *s a) = (\<Sum>v | f v \<noteq> 0. f v *s v) \<and> finite {v. f v \<noteq> 0} \<and> (\<forall>v. f v \<noteq> 0 \<longrightarrow> v \<in> b)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   169
    by (intro exI[of _ "\<lambda>v. if v \<in> t then r v else 0"]) (auto intro!: sum.mono_neutral_cong_right)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   170
next
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   171
  fix f :: "'b \<Rightarrow> 'a" assume "finite {v. f v \<noteq> 0}" "(\<forall>v. f v \<noteq> 0 \<longrightarrow> v \<in> b)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   172
  then show "\<exists>t r. (\<Sum>v | f v \<noteq> 0. f v *s v) = (\<Sum>a\<in>t. r a *s a) \<and> finite t \<and> t \<subseteq> b"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   173
    by (intro exI[of _ "{v. f v \<noteq> 0}"] exI[of _ f]) auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   174
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   175
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   176
lemma span_alt:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   177
  "span B = {(\<Sum>x | f x \<noteq> 0. f x *s x) | f. {x. f x \<noteq> 0} \<subseteq> B \<and> finite {x. f x \<noteq> 0}}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   178
  unfolding span_explicit' by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   179
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   180
lemma span_finite:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   181
  assumes fS: "finite S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   182
  shows "span S = range (\<lambda>u. \<Sum>v\<in>S. u v *s v)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   183
  unfolding span_explicit
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   184
proof safe
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   185
  fix t r assume "t \<subseteq> S" then show "(\<Sum>a\<in>t. r a *s a) \<in> range (\<lambda>u. \<Sum>v\<in>S. u v *s v)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   186
    by (intro image_eqI[of _ _ "\<lambda>a. if a \<in> t then r a else 0"])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   187
       (auto simp: if_distrib[of "\<lambda>r. r *s a" for a] sum.If_cases fS Int_absorb1)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   188
next
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   189
  show "\<exists>t r. (\<Sum>v\<in>S. u v *s v) = (\<Sum>a\<in>t. r a *s a) \<and> finite t \<and> t \<subseteq> S" for u
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   190
    by (intro exI[of _ u] exI[of _ S]) (auto intro: fS)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   191
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   192
68073
fad29d2a17a5 merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents: 68072
diff changeset
   193
lemma span_induct_alt [consumes 1, case_names base step, induct set: span]:
68072
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   194
  assumes x: "x \<in> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   195
  assumes h0: "h 0" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *s x + y)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   196
  shows "h x"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   197
  using x unfolding span_explicit
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   198
proof safe
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   199
  fix t r assume "finite t" "t \<subseteq> S" then show "h (\<Sum>a\<in>t. r a *s a)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   200
    by (induction t) (auto intro!: hS h0)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   201
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   202
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   203
lemma span_mono: "A \<subseteq> B \<Longrightarrow> span A \<subseteq> span B"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   204
  by (auto simp: span_explicit)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   205
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   206
lemma span_base: "a \<in> S \<Longrightarrow> a \<in> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   207
  by (auto simp: span_explicit intro!: exI[of _ "{a}"] exI[of _ "\<lambda>_. 1"])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   208
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   209
lemma span_superset: "S \<subseteq> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   210
  by (auto simp: span_base)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   211
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   212
lemma span_zero: "0 \<in> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   213
  by (auto simp: span_explicit intro!: exI[of _ "{}"])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   214
68074
8d50467f7555 fixed HOL-Analysis
immler
parents: 68073
diff changeset
   215
lemma span_UNIV[simp]: "span UNIV = UNIV"
68072
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   216
  by (auto intro: span_base)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   217
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   218
lemma span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   219
  unfolding span_explicit
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   220
proof safe
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   221
  fix tx ty rx ry assume *: "finite tx" "finite ty" "tx \<subseteq> S" "ty \<subseteq> S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   222
  have [simp]: "(tx \<union> ty) \<inter> tx = tx" "(tx \<union> ty) \<inter> ty = ty"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   223
    by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   224
  show "\<exists>t r. (\<Sum>a\<in>tx. rx a *s a) + (\<Sum>a\<in>ty. ry a *s a) = (\<Sum>a\<in>t. r a *s a) \<and> finite t \<and> t \<subseteq> S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   225
    apply (intro exI[of _ "tx \<union> ty"])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   226
    apply (intro exI[of _ "\<lambda>a. (if a \<in> tx then rx a else 0) + (if a \<in> ty then ry a else 0)"])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   227
    apply (auto simp: * scale_left_distrib sum.distrib if_distrib[of "\<lambda>r. r *s a" for a] sum.If_cases)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   228
    done
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   229
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   230
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   231
lemma span_scale: "x \<in> span S \<Longrightarrow> c *s x \<in> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   232
  unfolding span_explicit
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   233
proof safe
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   234
  fix t r assume *: "finite t" "t \<subseteq> S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   235
  show "\<exists>t' r'. c *s (\<Sum>a\<in>t. r a *s a) = (\<Sum>a\<in>t'. r' a *s a) \<and> finite t' \<and> t' \<subseteq> S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   236
    by (intro exI[of _ t] exI[of _ "\<lambda>a. c * r a"]) (auto simp: * scale_sum_right)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   237
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   238
68073
fad29d2a17a5 merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents: 68072
diff changeset
   239
lemma subspace_span [iff]: "subspace (span S)"
68072
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   240
  by (auto simp: subspace_def span_zero span_add span_scale)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   241
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   242
lemma span_neg: "x \<in> span S \<Longrightarrow> - x \<in> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   243
  by (metis subspace_neg subspace_span)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   244
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   245
lemma span_diff: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   246
  by (metis subspace_span subspace_diff)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   247
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   248
lemma span_sum: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> span S) \<Longrightarrow> sum f A \<in> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   249
  by (rule subspace_sum, rule subspace_span)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   250
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   251
lemma span_minimal: "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> span S \<subseteq> T"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   252
  by (auto simp: span_explicit intro!: subspace_sum subspace_scale)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   253
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   254
lemma span_def: "span S = subspace hull S" 
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   255
  by (intro hull_unique[symmetric] span_superset subspace_span span_minimal)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   256
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   257
lemma span_unique:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   258
  "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> (\<And>T'. S \<subseteq> T' \<Longrightarrow> subspace T' \<Longrightarrow> T \<subseteq> T') \<Longrightarrow> span S = T"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   259
  unfolding span_def by (rule hull_unique)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   260
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   261
lemma span_subspace_induct[consumes 2]:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   262
  assumes x: "x \<in> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   263
    and P: "subspace P"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   264
    and SP: "\<And>x. x \<in> S \<Longrightarrow> x \<in> P"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   265
  shows "x \<in> P"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   266
proof -
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   267
  from SP have SP': "S \<subseteq> P"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   268
    by (simp add: subset_eq)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   269
  from x hull_minimal[where S=subspace, OF SP' P, unfolded span_def[symmetric]]
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   270
  show "x \<in> P"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   271
    by (metis subset_eq)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   272
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   273
68073
fad29d2a17a5 merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents: 68072
diff changeset
   274
lemma (in module) span_induct[consumes 1, case_names base step, induct set: span]:
68072
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   275
  assumes x: "x \<in> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   276
    and P: "subspace (Collect P)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   277
    and SP: "\<And>x. x \<in> S \<Longrightarrow> P x"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   278
  shows "P x"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   279
  using P SP span_subspace_induct x by fastforce
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   280
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   281
lemma span_empty[simp]: "span {} = {0}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   282
  by (rule span_unique) (auto simp add: subspace_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   283
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   284
lemma span_subspace: "A \<subseteq> B \<Longrightarrow> B \<subseteq> span A \<Longrightarrow> subspace B \<Longrightarrow> span A = B"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   285
  by (metis order_antisym span_def hull_minimal)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   286
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   287
lemma span_span: "span (span A) = span A"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   288
  unfolding span_def hull_hull ..
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   289
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   290
(* TODO: proof generally for subspace: *)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   291
lemma span_add_eq: assumes x: "x \<in> span S" shows "x + y \<in> span S \<longleftrightarrow> y \<in> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   292
proof
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   293
  assume *: "x + y \<in> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   294
  have "(x + y) - x \<in> span S" using * x by (rule span_diff)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   295
  then show "y \<in> span S" by simp
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   296
qed (intro span_add x)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   297
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   298
lemma span_add_eq2: assumes y: "y \<in> span S" shows "x + y \<in> span S \<longleftrightarrow> x \<in> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   299
  using span_add_eq[of y S x] y by (auto simp: ac_simps)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   300
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   301
lemma span_singleton: "span {x} = range (\<lambda>k. k *s x)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   302
  by (auto simp: span_finite)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   303
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   304
lemma span_Un: "span (S \<union> T) = {x + y | x y. x \<in> span S \<and> y \<in> span T}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   305
proof safe
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   306
  fix x assume "x \<in> span (S \<union> T)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   307
  then obtain t r where t: "finite t" "t \<subseteq> S \<union> T" and x: "x = (\<Sum>a\<in>t. r a *s a)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   308
    by (auto simp: span_explicit)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   309
  moreover have "t \<inter> S \<union> (t - S) = t" by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   310
  ultimately show "\<exists>xa y. x = xa + y \<and> xa \<in> span S \<and> y \<in> span T"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   311
    unfolding x
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   312
    apply (rule_tac exI[of _ "\<Sum>a\<in>t \<inter> S. r a *s a"])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   313
    apply (rule_tac exI[of _ "\<Sum>a\<in>t - S. r a *s a"])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   314
    apply (subst sum.union_inter_neutral[symmetric])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   315
    apply (auto intro!: span_sum span_scale intro: span_base)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   316
    done
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   317
next
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   318
  fix x y assume"x \<in> span S" "y \<in> span T" then show "x + y \<in> span (S \<union> T)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   319
    using span_mono[of S "S \<union> T"] span_mono[of T "S \<union> T"]
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   320
    by (auto intro!: span_add)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   321
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   322
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   323
lemma span_insert: "span (insert a S) = {x. \<exists>k. (x - k *s a) \<in> span S}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   324
proof -
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   325
  have "span ({a} \<union> S) = {x. \<exists>k. (x - k *s a) \<in> span S}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   326
    unfolding span_Un span_singleton
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   327
    apply (auto simp add: set_eq_iff)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   328
    subgoal for y k by (auto intro!: exI[of _ "k"])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   329
    subgoal for y k by (rule exI[of _ "k *s a"], rule exI[of _ "y - k *s a"]) auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   330
    done
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   331
  then show ?thesis by simp
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   332
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   333
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   334
lemma span_breakdown:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   335
  assumes bS: "b \<in> S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   336
    and aS: "a \<in> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   337
  shows "\<exists>k. a - k *s b \<in> span (S - {b})"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   338
  using assms span_insert [of b "S - {b}"]
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   339
  by (simp add: insert_absorb)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   340
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   341
lemma span_breakdown_eq: "x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. x - k *s a \<in> span S)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   342
  by (simp add: span_insert)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   343
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   344
lemmas span_clauses = span_base span_zero span_add span_scale
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   345
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   346
lemma span_eq_iff[simp]: "span s = s \<longleftrightarrow> subspace s"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   347
  unfolding span_def by (rule hull_eq) (rule subspace_Inter)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   348
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   349
lemma span_eq: "span S = span T \<longleftrightarrow> S \<subseteq> span T \<and> T \<subseteq> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   350
  by (metis span_minimal span_subspace span_superset subspace_span)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   351
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   352
lemma eq_span_insert_eq:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   353
  assumes "(x - y) \<in> span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   354
    shows "span(insert x S) = span(insert y S)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   355
proof -
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   356
  have *: "span(insert x S) \<subseteq> span(insert y S)" if "(x - y) \<in> span S" for x y
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   357
  proof -
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   358
    have 1: "(r *s x - r *s y) \<in> span S" for r
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   359
      by (metis scale_right_diff_distrib span_scale that)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   360
    have 2: "(z - k *s y) - k *s (x - y) = z - k *s x" for  z k
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   361
      by (simp add: scale_right_diff_distrib)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   362
  show ?thesis
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   363
    apply (clarsimp simp add: span_breakdown_eq)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   364
    by (metis 1 2 diff_add_cancel scale_right_diff_distrib span_add_eq)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   365
  qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   366
  show ?thesis
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   367
    apply (intro subset_antisym * assms)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   368
    using assms subspace_neg subspace_span minus_diff_eq by force
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   369
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   370
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   371
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   372
section \<open>Dependent and independent sets\<close>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   373
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   374
definition dependent :: "'b set \<Rightarrow> bool"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   375
  where dependent_explicit: "dependent s \<longleftrightarrow> (\<exists>t u. finite t \<and> t \<subseteq> s \<and> (\<Sum>v\<in>t. u v *s v) = 0 \<and> (\<exists>v\<in>t. u v \<noteq> 0))"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   376
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   377
abbreviation "independent s \<equiv> \<not> dependent s"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   378
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   379
lemma dependent_mono: "dependent B \<Longrightarrow> B \<subseteq> A \<Longrightarrow> dependent A"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   380
  by (auto simp add: dependent_explicit)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   381
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   382
lemma independent_mono: "independent A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> independent B"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   383
  by (auto intro: dependent_mono)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   384
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   385
lemma dependent_zero: "0 \<in> A \<Longrightarrow> dependent A"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   386
  by (auto simp: dependent_explicit intro!: exI[of _ "\<lambda>i. 1"] exI[of _ "{0}"])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   387
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   388
lemma independent_empty[intro]: "independent {}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   389
  by (simp add: dependent_explicit)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   390
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   391
lemma independent_explicit_module:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   392
  "independent s \<longleftrightarrow> (\<forall>t u v. finite t \<longrightarrow> t \<subseteq> s \<longrightarrow> (\<Sum>v\<in>t. u v *s v) = 0 \<longrightarrow> v \<in> t \<longrightarrow> u v = 0)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   393
  unfolding dependent_explicit by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   394
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   395
lemma independentD: "independent s \<Longrightarrow> finite t \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (\<Sum>v\<in>t. u v *s v) = 0 \<Longrightarrow> v \<in> t \<Longrightarrow> u v = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   396
  by (simp add: independent_explicit_module)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   397
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   398
lemma independent_Union_directed:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   399
  assumes directed: "\<And>c d. c \<in> C \<Longrightarrow> d \<in> C \<Longrightarrow> c \<subseteq> d \<or> d \<subseteq> c"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   400
  assumes indep: "\<And>c. c \<in> C \<Longrightarrow> independent c"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   401
  shows "independent (\<Union>C)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   402
proof
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   403
  assume "dependent (\<Union>C)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   404
  then obtain u v S where S: "finite S" "S \<subseteq> \<Union>C" "v \<in> S" "u v \<noteq> 0" "(\<Sum>v\<in>S. u v *s v) = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   405
    by (auto simp: dependent_explicit)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   406
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   407
  have "S \<noteq> {}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   408
    using \<open>v \<in> S\<close> by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   409
  have "\<exists>c\<in>C. S \<subseteq> c"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   410
    using \<open>finite S\<close> \<open>S \<noteq> {}\<close> \<open>S \<subseteq> \<Union>C\<close>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   411
  proof (induction rule: finite_ne_induct)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   412
    case (insert i I)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   413
    then obtain c d where cd: "c \<in> C" "d \<in> C" and iI: "I \<subseteq> c" "i \<in> d"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   414
      by blast
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   415
    from directed[OF cd] cd have "c \<union> d \<in> C"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   416
      by (auto simp: sup.absorb1 sup.absorb2)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   417
    with iI show ?case
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   418
      by (intro bexI[of _ "c \<union> d"]) auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   419
  qed auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   420
  then obtain c where "c \<in> C" "S \<subseteq> c"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   421
    by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   422
  have "dependent c"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   423
    unfolding dependent_explicit
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   424
    by (intro exI[of _ S] exI[of _ u] bexI[of _ v] conjI) fact+
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   425
  with indep[OF \<open>c \<in> C\<close>] show False
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   426
    by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   427
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   428
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   429
lemma dependent_finite:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   430
  assumes "finite S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   431
  shows "dependent S \<longleftrightarrow> (\<exists>u. (\<exists>v \<in> S. u v \<noteq> 0) \<and> (\<Sum>v\<in>S. u v *s v) = 0)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   432
    (is "?lhs = ?rhs")
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   433
proof
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   434
  assume ?lhs
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   435
  then obtain T u v
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   436
    where "finite T" "T \<subseteq> S" "v\<in>T" "u v \<noteq> 0" "(\<Sum>v\<in>T. u v *s v) = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   437
    by (force simp: dependent_explicit)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   438
  with assms show ?rhs
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   439
    apply (rule_tac x="\<lambda>v. if v \<in> T then u v else 0" in exI)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   440
    apply (auto simp: sum.mono_neutral_right)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   441
    done
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   442
next
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   443
  assume ?rhs  with assms show ?lhs
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   444
    by (fastforce simp add: dependent_explicit)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   445
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   446
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   447
lemma dependent_alt:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   448
  "dependent B \<longleftrightarrow>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   449
    (\<exists>X. finite {x. X x \<noteq> 0} \<and> {x. X x \<noteq> 0} \<subseteq> B \<and> (\<Sum>x|X x \<noteq> 0. X x *s x) = 0 \<and> (\<exists>x. X x \<noteq> 0))"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   450
  unfolding dependent_explicit
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   451
  apply safe
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   452
  subgoal for S u v
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   453
    apply (intro exI[of _ "\<lambda>x. if x \<in> S then u x else 0"])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   454
    apply (subst sum.mono_neutral_cong_left[where T=S])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   455
    apply (auto intro!: sum.mono_neutral_cong_right cong: rev_conj_cong)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   456
    done
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   457
  apply auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   458
  done
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   459
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   460
lemma independent_alt:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   461
  "independent B \<longleftrightarrow>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   462
    (\<forall>X. finite {x. X x \<noteq> 0} \<longrightarrow> {x. X x \<noteq> 0} \<subseteq> B \<longrightarrow> (\<Sum>x|X x \<noteq> 0. X x *s x) = 0 \<longrightarrow> (\<forall>x. X x = 0))"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   463
  unfolding dependent_alt by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   464
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   465
lemma independentD_alt:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   466
  "independent B \<Longrightarrow> finite {x. X x \<noteq> 0} \<Longrightarrow> {x. X x \<noteq> 0} \<subseteq> B \<Longrightarrow> (\<Sum>x|X x \<noteq> 0. X x *s x) = 0 \<Longrightarrow> X x = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   467
  unfolding independent_alt by blast
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   468
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   469
lemma independentD_unique:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   470
  assumes B: "independent B"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   471
    and X: "finite {x. X x \<noteq> 0}" "{x. X x \<noteq> 0} \<subseteq> B"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   472
    and Y: "finite {x. Y x \<noteq> 0}" "{x. Y x \<noteq> 0} \<subseteq> B"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   473
    and "(\<Sum>x | X x \<noteq> 0. X x *s x) = (\<Sum>x| Y x \<noteq> 0. Y x *s x)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   474
  shows "X = Y"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   475
proof -
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   476
  have "X x - Y x = 0" for x
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   477
    using B
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   478
  proof (rule independentD_alt)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   479
    have "{x. X x - Y x \<noteq> 0} \<subseteq> {x. X x \<noteq> 0} \<union> {x. Y x \<noteq> 0}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   480
      by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   481
    then show "finite {x. X x - Y x \<noteq> 0}" "{x. X x - Y x \<noteq> 0} \<subseteq> B"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   482
      using X Y by (auto dest: finite_subset)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   483
    then have "(\<Sum>x | X x - Y x \<noteq> 0. (X x - Y x) *s x) = (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. (X v - Y v) *s v)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   484
      using X Y by (intro sum.mono_neutral_cong_left) auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   485
    also have "\<dots> = (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. X v *s v) - (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. Y v *s v)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   486
      by (simp add: scale_left_diff_distrib sum_subtractf assms)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   487
    also have "(\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. X v *s v) = (\<Sum>v\<in>{S. X S \<noteq> 0}. X v *s v)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   488
      using X Y by (intro sum.mono_neutral_cong_right) auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   489
    also have "(\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. Y v *s v) = (\<Sum>v\<in>{S. Y S \<noteq> 0}. Y v *s v)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   490
      using X Y by (intro sum.mono_neutral_cong_right) auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   491
    finally show "(\<Sum>x | X x - Y x \<noteq> 0. (X x - Y x) *s x) = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   492
      using assms by simp
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   493
  qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   494
  then show ?thesis
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   495
    by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   496
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   497
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   498
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   499
section \<open>Representation of a vector on a specific basis\<close>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   500
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   501
definition representation :: "'b set \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'a"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   502
  where "representation basis v =
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   503
    (if independent basis \<and> v \<in> span basis then
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   504
      SOME f. (\<forall>v. f v \<noteq> 0 \<longrightarrow> v \<in> basis) \<and> finite {v. f v \<noteq> 0} \<and> (\<Sum>v\<in>{v. f v \<noteq> 0}. f v *s v) = v
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   505
    else (\<lambda>b. 0))"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   506
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   507
lemma unique_representation:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   508
  assumes basis: "independent basis"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   509
    and in_basis: "\<And>v. f v \<noteq> 0 \<Longrightarrow> v \<in> basis" "\<And>v. g v \<noteq> 0 \<Longrightarrow> v \<in> basis"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   510
    and [simp]: "finite {v. f v \<noteq> 0}" "finite {v. g v \<noteq> 0}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   511
    and eq: "(\<Sum>v\<in>{v. f v \<noteq> 0}. f v *s v) = (\<Sum>v\<in>{v. g v \<noteq> 0}. g v *s v)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   512
  shows "f = g"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   513
proof (rule ext, rule ccontr)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   514
  fix v assume ne: "f v \<noteq> g v"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   515
  have "dependent basis"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   516
    unfolding dependent_explicit
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   517
  proof (intro exI conjI)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   518
    have *: "{v. f v - g v \<noteq> 0} \<subseteq> {v. f v \<noteq> 0} \<union> {v. g v \<noteq> 0}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   519
      by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   520
    show "finite {v. f v - g v \<noteq> 0}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   521
      by (rule finite_subset[OF *]) simp
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   522
    show "\<exists>v\<in>{v. f v - g v \<noteq> 0}. f v - g v \<noteq> 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   523
      by (rule bexI[of _ v]) (auto simp: ne)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   524
    have "(\<Sum>v | f v - g v \<noteq> 0. (f v - g v) *s v) = 
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   525
        (\<Sum>v\<in>{v. f v \<noteq> 0} \<union> {v. g v \<noteq> 0}. (f v - g v) *s v)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   526
      by (intro sum.mono_neutral_cong_left *) auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   527
    also have "... =
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   528
        (\<Sum>v\<in>{v. f v \<noteq> 0} \<union> {v. g v \<noteq> 0}. f v *s v) - (\<Sum>v\<in>{v. f v \<noteq> 0} \<union> {v. g v \<noteq> 0}. g v *s v)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   529
      by (simp add: algebra_simps sum_subtractf)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   530
    also have "... = (\<Sum>v | f v \<noteq> 0. f v *s v) - (\<Sum>v | g v \<noteq> 0. g v *s v)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   531
      by (intro arg_cong2[where f= "(-)"] sum.mono_neutral_cong_right) auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   532
    finally show "(\<Sum>v | f v - g v \<noteq> 0. (f v - g v) *s v) = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   533
      by (simp add: eq)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   534
    show "{v. f v - g v \<noteq> 0} \<subseteq> basis"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   535
      using in_basis * by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   536
  qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   537
  with basis show False by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   538
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   539
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   540
lemma
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   541
  shows representation_ne_zero: "\<And>b. representation basis v b \<noteq> 0 \<Longrightarrow> b \<in> basis"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   542
    and finite_representation: "finite {b. representation basis v b \<noteq> 0}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   543
    and sum_nonzero_representation_eq:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   544
      "independent basis \<Longrightarrow> v \<in> span basis \<Longrightarrow> (\<Sum>b | representation basis v b \<noteq> 0. representation basis v b *s b) = v"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   545
proof -
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   546
  { assume basis: "independent basis" and v: "v \<in> span basis"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   547
    define p where "p f \<longleftrightarrow>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   548
      (\<forall>v. f v \<noteq> 0 \<longrightarrow> v \<in> basis) \<and> finite {v. f v \<noteq> 0} \<and> (\<Sum>v\<in>{v. f v \<noteq> 0}. f v *s v) = v" for f
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   549
    obtain t r where *: "finite t" "t \<subseteq> basis" "(\<Sum>b\<in>t. r b *s b) = v"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   550
      using \<open>v \<in> span basis\<close> by (auto simp: span_explicit)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   551
    define f where "f b = (if b \<in> t then r b else 0)" for b
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   552
    have "p f"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   553
      using * by (auto simp: p_def f_def intro!: sum.mono_neutral_cong_left)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   554
    have *: "representation basis v = Eps p" by (simp add: p_def[abs_def] representation_def basis v)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   555
    from someI[of p f, OF \<open>p f\<close>] have "p (representation basis v)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   556
      unfolding * . }
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   557
  note * = this
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   558
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   559
  show "representation basis v b \<noteq> 0 \<Longrightarrow> b \<in> basis" for b
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   560
    using * by (cases "independent basis \<and> v \<in> span basis") (auto simp: representation_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   561
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   562
  show "finite {b. representation basis v b \<noteq> 0}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   563
    using * by (cases "independent basis \<and> v \<in> span basis") (auto simp: representation_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   564
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   565
  show "independent basis \<Longrightarrow> v \<in> span basis \<Longrightarrow> (\<Sum>b | representation basis v b \<noteq> 0. representation basis v b *s b) = v"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   566
    using * by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   567
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   568
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   569
lemma sum_representation_eq:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   570
  "(\<Sum>b\<in>B. representation basis v b *s b) = v"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   571
  if "independent basis" "v \<in> span basis" "finite B" "basis \<subseteq> B"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   572
proof -
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   573
  have "(\<Sum>b\<in>B. representation basis v b *s b) =
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   574
      (\<Sum>b | representation basis v b \<noteq> 0. representation basis v b *s b)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   575
    apply (rule sum.mono_neutral_cong)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   576
        apply (rule finite_representation)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   577
       apply fact
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   578
    subgoal for b
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   579
      using that representation_ne_zero[of basis v b]
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   580
      by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   581
    subgoal by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   582
    subgoal by simp
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   583
    done
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   584
  also have "\<dots> = v"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   585
    by (rule sum_nonzero_representation_eq; fact)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   586
  finally show ?thesis .
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   587
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   588
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   589
lemma representation_eqI:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   590
  assumes basis: "independent basis" and b: "v \<in> span basis"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   591
    and ne_zero: "\<And>b. f b \<noteq> 0 \<Longrightarrow> b \<in> basis"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   592
    and finite: "finite {b. f b \<noteq> 0}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   593
    and eq: "(\<Sum>b | f b \<noteq> 0. f b *s b) = v"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   594
  shows "representation basis v = f"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   595
  by (rule unique_representation[OF basis])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   596
     (auto simp: representation_ne_zero finite_representation
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   597
       sum_nonzero_representation_eq[OF basis b] ne_zero finite eq)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   598
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   599
lemma representation_basis:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   600
  assumes basis: "independent basis" and b: "b \<in> basis"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   601
  shows "representation basis b = (\<lambda>v. if v = b then 1 else 0)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   602
proof (rule unique_representation[OF basis])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   603
  show "representation basis b v \<noteq> 0 \<Longrightarrow> v \<in> basis" for v
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   604
    using representation_ne_zero .
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   605
  show "finite {v. representation basis b v \<noteq> 0}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   606
    using finite_representation .
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   607
  show "(if v = b then 1 else 0) \<noteq> 0 \<Longrightarrow> v \<in> basis" for v
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   608
    by (cases "v = b") (auto simp: b)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   609
  have *: "{v. (if v = b then 1 else 0 :: 'a) \<noteq> 0} = {b}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   610
    by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   611
  show "finite {v. (if v = b then 1 else 0) \<noteq> 0}" unfolding * by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   612
  show "(\<Sum>v | representation basis b v \<noteq> 0. representation basis b v *s v) =
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   613
    (\<Sum>v | (if v = b then 1 else 0::'a) \<noteq> 0. (if v = b then 1 else 0) *s v)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   614
    unfolding * sum_nonzero_representation_eq[OF basis span_base[OF b]] by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   615
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   616
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   617
lemma representation_zero: "representation basis 0 = (\<lambda>b. 0)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   618
proof cases
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   619
  assume basis: "independent basis" show ?thesis
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   620
    by (rule representation_eqI[OF basis span_zero]) auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   621
qed (simp add: representation_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   622
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   623
lemma representation_diff:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   624
  assumes basis: "independent basis" and v: "v \<in> span basis" and u: "u \<in> span basis"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   625
  shows "representation basis (u - v) = (\<lambda>b. representation basis u b - representation basis v b)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   626
proof (rule representation_eqI[OF basis span_diff[OF u v]])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   627
  let ?R = "representation basis"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   628
  note finite_representation[simp] u[simp] v[simp]
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   629
  have *: "{b. ?R u b - ?R v b \<noteq> 0} \<subseteq> {b. ?R u b \<noteq> 0} \<union> {b. ?R v b \<noteq> 0}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   630
    by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   631
  then show "?R u b - ?R v b \<noteq> 0 \<Longrightarrow> b \<in> basis" for b
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   632
    by (auto dest: representation_ne_zero)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   633
  show "finite {b. ?R u b - ?R v b \<noteq> 0}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   634
    by (intro finite_subset[OF *]) simp_all
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   635
  have "(\<Sum>b | ?R u b - ?R v b \<noteq> 0. (?R u b - ?R v b) *s b) =
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   636
      (\<Sum>b\<in>{b. ?R u b \<noteq> 0} \<union> {b. ?R v b \<noteq> 0}. (?R u b - ?R v b) *s b)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   637
    by (intro sum.mono_neutral_cong_left *) auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   638
  also have "... =
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   639
      (\<Sum>b\<in>{b. ?R u b \<noteq> 0} \<union> {b. ?R v b \<noteq> 0}. ?R u b *s b) - (\<Sum>b\<in>{b. ?R u b \<noteq> 0} \<union> {b. ?R v b \<noteq> 0}. ?R v b *s b)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   640
    by (simp add: algebra_simps sum_subtractf)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   641
  also have "... = (\<Sum>b | ?R u b \<noteq> 0. ?R u b *s b) - (\<Sum>b | ?R v b \<noteq> 0. ?R v b *s b)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   642
    by (intro arg_cong2[where f= "(-)"] sum.mono_neutral_cong_right) auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   643
  finally show "(\<Sum>b | ?R u b - ?R v b \<noteq> 0. (?R u b - ?R v b) *s b) = u - v"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   644
    by (simp add: sum_nonzero_representation_eq[OF basis])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   645
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   646
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   647
lemma representation_neg:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   648
  "independent basis \<Longrightarrow> v \<in> span basis \<Longrightarrow> representation basis (- v) = (\<lambda>b. - representation basis v b)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   649
  using representation_diff[of basis v 0] by (simp add: representation_zero span_zero)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   650
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   651
lemma representation_add:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   652
  "independent basis \<Longrightarrow> v \<in> span basis \<Longrightarrow> u \<in> span basis \<Longrightarrow>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   653
    representation basis (u + v) = (\<lambda>b. representation basis u b + representation basis v b)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   654
  using representation_diff[of basis "-v" u] by (simp add: representation_neg representation_diff span_neg)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   655
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   656
lemma representation_sum:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   657
  "independent basis \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> v i \<in> span basis) \<Longrightarrow>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   658
    representation basis (sum v I) = (\<lambda>b. \<Sum>i\<in>I. representation basis (v i) b)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   659
  by (induction I rule: infinite_finite_induct)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   660
     (auto simp: representation_zero representation_add span_sum)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   661
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   662
lemma representation_scale:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   663
  assumes basis: "independent basis" and v: "v \<in> span basis"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   664
  shows "representation basis (r *s v) = (\<lambda>b. r * representation basis v b)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   665
proof (rule representation_eqI[OF basis span_scale[OF v]])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   666
  let ?R = "representation basis"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   667
  note finite_representation[simp] v[simp]
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   668
  have *: "{b. r * ?R v b \<noteq> 0} \<subseteq> {b. ?R v b \<noteq> 0}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   669
    by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   670
  then show "r * representation basis v b \<noteq> 0 \<Longrightarrow> b \<in> basis" for b
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   671
    using representation_ne_zero by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   672
  show "finite {b. r * ?R v b \<noteq> 0}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   673
    by (intro finite_subset[OF *]) simp_all
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   674
  have "(\<Sum>b | r * ?R v b \<noteq> 0. (r * ?R v b) *s b) = (\<Sum>b\<in>{b. ?R v b \<noteq> 0}. (r * ?R v b) *s b)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   675
    by (intro sum.mono_neutral_cong_left *) auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   676
  also have "... = r *s (\<Sum>b | ?R v b \<noteq> 0. ?R v b *s b)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   677
    by (simp add: scale_scale[symmetric] scale_sum_right del: scale_scale)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   678
  finally show "(\<Sum>b | r * ?R v b \<noteq> 0. (r * ?R v b) *s b) = r *s v"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   679
    by (simp add: sum_nonzero_representation_eq[OF basis])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   680
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   681
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   682
lemma representation_extend:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   683
  assumes basis: "independent basis" and v: "v \<in> span basis'" and basis': "basis' \<subseteq> basis"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   684
  shows "representation basis v = representation basis' v"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   685
proof (rule representation_eqI[OF basis])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   686
  show v': "v \<in> span basis" using span_mono[OF basis'] v by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   687
  have *: "independent basis'" using basis' basis by (auto intro: dependent_mono)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   688
  show "representation basis' v b \<noteq> 0 \<Longrightarrow> b \<in> basis" for b
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   689
    using representation_ne_zero basis' by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   690
  show "finite {b. representation basis' v b \<noteq> 0}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   691
    using finite_representation .
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   692
  show "(\<Sum>b | representation basis' v b \<noteq> 0. representation basis' v b *s b) = v"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   693
    using sum_nonzero_representation_eq[OF * v] .
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   694
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   695
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   696
text \<open>The set \<open>B\<close> is the maximal independent set for \<open>span B\<close>, or \<open>A\<close> is the minimal spanning set\<close>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   697
lemma spanning_subset_independent:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   698
  assumes BA: "B \<subseteq> A"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   699
    and iA: "independent A"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   700
    and AsB: "A \<subseteq> span B"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   701
  shows "A = B"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   702
proof (intro antisym[OF _ BA] subsetI)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   703
  have iB: "independent B" using independent_mono [OF iA BA] .
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   704
  fix v assume "v \<in> A"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   705
  with AsB have "v \<in> span B" by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   706
  let ?RB = "representation B v" and ?RA = "representation A v"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   707
  have "?RB v = 1"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   708
    unfolding representation_extend[OF iA \<open>v \<in> span B\<close> BA, symmetric] representation_basis[OF iA \<open>v \<in> A\<close>] by simp
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   709
  then show "v \<in> B"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   710
    using representation_ne_zero[of B v v] by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   711
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   712
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   713
end
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   714
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   715
(* We need to introduce more specific modules, where the ring structure gets more and more finer,
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   716
  i.e. Bezout rings & domains, division rings, fields *)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   717
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   718
text \<open>A linear function is a mapping between two modules over the same ring.\<close>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   719
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   720
locale module_hom = m1: module s1 + m2: module s2
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   721
    for s1 :: "'a::comm_ring_1 \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*a" 75)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   722
    and s2 :: "'a::comm_ring_1 \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr "*b" 75) +
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   723
  fixes f :: "'b \<Rightarrow> 'c"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   724
  assumes add: "f (b1 + b2) = f b1 + f b2"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   725
    and scale: "f (r *a b) = r *b f b"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   726
begin
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   727
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   728
lemma zero[simp]: "f 0 = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   729
  using scale[of 0 0] by simp
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   730
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   731
lemma neg: "f (- x) = - f x"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   732
  using scale [where r="-1"] by (metis add add_eq_0_iff zero)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   733
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   734
lemma diff: "f (x - y) = f x - f y"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   735
  by (metis diff_conv_add_uminus add neg)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   736
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   737
lemma sum: "f (sum g S) = (\<Sum>a\<in>S. f (g a))"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   738
proof (induct S rule: infinite_finite_induct)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   739
  case (insert x F)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   740
  have "f (sum g (insert x F)) = f (g x + sum g F)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   741
    using insert.hyps by simp
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   742
  also have "\<dots> = f (g x) + f (sum g F)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   743
    using add by simp
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   744
  also have "\<dots> = (\<Sum>a\<in>insert x F. f (g a))"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   745
    using insert.hyps by simp
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   746
  finally show ?case .
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   747
qed simp_all
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   748
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   749
lemma inj_on_iff_eq_0:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   750
  assumes s: "m1.subspace s"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   751
  shows "inj_on f s \<longleftrightarrow> (\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   752
proof -
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   753
  have "inj_on f s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. f x - f y = 0 \<longrightarrow> x - y = 0)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   754
    by (simp add: inj_on_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   755
  also have "\<dots> \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. f (x - y) = 0 \<longrightarrow> x - y = 0)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   756
    by (simp add: diff)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   757
  also have "\<dots> \<longleftrightarrow> (\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0)" (is "?l = ?r")(* TODO: sledgehammer! *)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   758
  proof safe
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   759
    fix x assume ?l assume "x \<in> s" "f x = 0" with \<open>?l\<close>[rule_format, of x 0] s show "x = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   760
      by (auto simp: m1.subspace_0)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   761
  next
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   762
    fix x y assume ?r assume "x \<in> s" "y \<in> s" "f (x - y) = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   763
    with \<open>?r\<close>[rule_format, of "x - y"] s
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   764
    show "x - y = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   765
      by (auto simp: m1.subspace_diff)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   766
  qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   767
  finally show ?thesis
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   768
    by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   769
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   770
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   771
lemma inj_iff_eq_0: "inj f = (\<forall>x. f x = 0 \<longrightarrow> x = 0)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   772
  by (rule inj_on_iff_eq_0[OF m1.subspace_UNIV, unfolded ball_UNIV])
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   773
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   774
lemma subspace_image: assumes S: "m1.subspace S" shows "m2.subspace (f ` S)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   775
  unfolding m2.subspace_def
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   776
proof safe
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   777
  show "0 \<in> f ` S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   778
    by (rule image_eqI[of _ _ 0]) (auto simp: S m1.subspace_0)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   779
  show "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> f x + f y \<in> f ` S" for x y
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   780
    by (rule image_eqI[of _ _ "x + y"]) (auto simp: S m1.subspace_add add)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   781
  show "x \<in> S \<Longrightarrow> r *b f x \<in> f ` S" for r x
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   782
    by (rule image_eqI[of _ _ "r *a x"]) (auto simp: S m1.subspace_scale scale)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   783
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   784
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   785
lemma subspace_vimage: "m2.subspace S \<Longrightarrow> m1.subspace (f -` S)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   786
  by (simp add: vimage_def add scale m1.subspace_def m2.subspace_0 m2.subspace_add m2.subspace_scale)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   787
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   788
lemma subspace_kernel: "m1.subspace {x. f x = 0}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   789
  using subspace_vimage[OF m2.subspace_single_0] by (simp add: vimage_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   790
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   791
lemma span_image: "m2.span (f ` S) = f ` (m1.span S)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   792
proof (rule m2.span_unique)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   793
  show "f ` S \<subseteq> f ` m1.span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   794
    by (rule image_mono, rule m1.span_superset)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   795
  show "m2.subspace (f ` m1.span S)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   796
    using m1.subspace_span by (rule subspace_image)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   797
next
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   798
  fix T assume "f ` S \<subseteq> T" and "m2.subspace T" then show "f ` m1.span S \<subseteq> T"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   799
    unfolding image_subset_iff_subset_vimage by (metis subspace_vimage m1.span_minimal)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   800
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   801
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   802
lemma dependent_inj_imageD:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   803
  assumes d: "m2.dependent (f ` s)" and i: "inj_on f (m1.span s)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   804
  shows "m1.dependent s"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   805
proof -
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   806
  have [intro]: "inj_on f s"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   807
    using \<open>inj_on f (m1.span s)\<close> m1.span_superset by (rule inj_on_subset)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   808
  from d obtain s' r v where *: "finite s'" "s' \<subseteq> s" "(\<Sum>v\<in>f ` s'. r v *b v) = 0" "v \<in> s'" "r (f v) \<noteq> 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   809
    by (auto simp: m2.dependent_explicit subset_image_iff dest!: finite_imageD intro: inj_on_subset)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   810
  have "f (\<Sum>v\<in>s'. r (f v) *a v) = (\<Sum>v\<in>s'. r (f v) *b f v)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   811
    by (simp add: sum scale)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   812
  also have "... = (\<Sum>v\<in>f ` s'. r v *b v)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   813
    using \<open>s' \<subseteq> s\<close> by (subst sum.reindex) (auto dest!: finite_imageD intro: inj_on_subset)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   814
  finally have "f (\<Sum>v\<in>s'. r (f v) *a v) = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   815
    by (simp add: *)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   816
  with \<open>s' \<subseteq> s\<close> have "(\<Sum>v\<in>s'. r (f v) *a v) = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   817
    by (intro inj_onD[OF i] m1.span_zero m1.span_sum m1.span_scale) (auto intro: m1.span_base)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   818
  then show "m1.dependent s"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   819
    using \<open>finite s'\<close> \<open>s' \<subseteq> s\<close> \<open>v \<in> s'\<close> \<open>r (f v) \<noteq> 0\<close> by (force simp add: m1.dependent_explicit)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   820
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   821
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   822
lemma eq_0_on_span:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   823
  assumes f0: "\<And>x. x \<in> b \<Longrightarrow> f x = 0" and x: "x \<in> m1.span b" shows "f x = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   824
  using m1.span_induct[OF x subspace_kernel] f0 by simp
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   825
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   826
lemma independent_injective_image: "m1.independent s \<Longrightarrow> inj_on f (m1.span s) \<Longrightarrow> m2.independent (f ` s)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   827
  using dependent_inj_imageD[of s] by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   828
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   829
lemma inj_on_span_independent_image:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   830
  assumes ifB: "m2.independent (f ` B)" and f: "inj_on f B" shows "inj_on f (m1.span B)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   831
  unfolding inj_on_iff_eq_0[OF m1.subspace_span] unfolding m1.span_explicit'
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   832
proof safe
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   833
  fix r assume fr: "finite {v. r v \<noteq> 0}" and r: "\<forall>v. r v \<noteq> 0 \<longrightarrow> v \<in> B"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   834
    and eq0: "f (\<Sum>v | r v \<noteq> 0. r v *a v) = 0"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   835
  have "0 = (\<Sum>v | r v \<noteq> 0. r v *b f v)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   836
    using eq0 by (simp add: sum scale)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   837
  also have "... = (\<Sum>v\<in>f ` {v. r v \<noteq> 0}. r (the_inv_into B f v) *b v)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   838
    using r by (subst sum.reindex) (auto simp: the_inv_into_f_f[OF f] intro!: inj_on_subset[OF f] sum.cong)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   839
  finally have "r v \<noteq> 0 \<Longrightarrow> r (the_inv_into B f (f v)) = 0" for v
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   840
    using fr r ifB[unfolded m2.independent_explicit_module, rule_format,
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   841
        of "f ` {v. r v \<noteq> 0}" "\<lambda>v. r (the_inv_into B f v)"]
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   842
    by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   843
  then have "r v = 0" for v
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   844
    using the_inv_into_f_f[OF f] r by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   845
  then show "(\<Sum>v | r v \<noteq> 0. r v *a v) = 0" by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   846
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   847
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   848
lemma inj_on_span_iff_independent_image: "m2.independent (f ` B) \<Longrightarrow> inj_on f (m1.span B) \<longleftrightarrow> inj_on f B"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   849
  using inj_on_span_independent_image[of B] inj_on_subset[OF _ m1.span_superset, of f B] by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   850
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   851
lemma subspace_linear_preimage: "m2.subspace S \<Longrightarrow> m1.subspace {x. f x \<in> S}"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   852
  by (simp add: add scale m1.subspace_def m2.subspace_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   853
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   854
lemma spans_image: "V \<subseteq> m1.span B \<Longrightarrow> f ` V \<subseteq> m2.span (f ` B)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   855
  by (metis image_mono span_image)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   856
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   857
text \<open>Relation between bases and injectivity/surjectivity of map.\<close>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   858
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   859
lemma spanning_surjective_image:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   860
  assumes us: "UNIV \<subseteq> m1.span S"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   861
    and sf: "surj f"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   862
  shows "UNIV \<subseteq> m2.span (f ` S)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   863
proof -
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   864
  have "UNIV \<subseteq> f ` UNIV"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   865
    using sf by (auto simp add: surj_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   866
  also have " \<dots> \<subseteq> m2.span (f ` S)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   867
    using spans_image[OF us] .
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   868
  finally show ?thesis .
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   869
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   870
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   871
lemmas independent_inj_on_image = independent_injective_image
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   872
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   873
lemma independent_inj_image:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   874
  "m1.independent S \<Longrightarrow> inj f \<Longrightarrow> m2.independent (f ` S)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   875
  using independent_inj_on_image[of S] by (auto simp: subset_inj_on)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   876
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   877
end
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   878
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   879
lemma module_hom_iff:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   880
  "module_hom s1 s2  f \<longleftrightarrow>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   881
    module s1 \<and> module s2 \<and>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   882
    (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (s1 c x) = s2 c (f x))"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   883
  by (simp add: module_hom_def module_hom_axioms_def)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   884
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   885
locale module_pair = m1: module s1 + m2: module s2
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   886
  for s1 :: "'a :: comm_ring_1 \<Rightarrow> 'b \<Rightarrow> 'b :: ab_group_add"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   887
  and s2 :: "'a :: comm_ring_1 \<Rightarrow> 'c \<Rightarrow> 'c :: ab_group_add"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   888
begin
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   889
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   890
lemma module_hom_zero: "module_hom s1 s2 (\<lambda>x. 0)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   891
  by (simp add: module_hom_iff m1.module_axioms m2.module_axioms)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   892
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   893
lemma module_hom_add: "module_hom s1 s2 f \<Longrightarrow> module_hom s1 s2 g \<Longrightarrow> module_hom s1 s2 (\<lambda>x. f x + g x)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   894
  by (simp add: module_hom_iff module.scale_right_distrib)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   895
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   896
lemma module_hom_sub: "module_hom s1 s2 f \<Longrightarrow> module_hom s1 s2 g \<Longrightarrow> module_hom s1 s2 (\<lambda>x. f x - g x)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   897
  by (simp add: module_hom_iff module.scale_right_diff_distrib)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   898
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   899
lemma module_hom_neg: "module_hom s1 s2 f \<Longrightarrow> module_hom s1 s2 (\<lambda>x. - f x)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   900
  by (simp add: module_hom_iff module.scale_minus_right)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   901
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   902
lemma module_hom_scale: "module_hom s1 s2 f \<Longrightarrow> module_hom s1 s2 (\<lambda>x. s2 c (f x))"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   903
  by (simp add: module_hom_iff module.scale_scale module.scale_right_distrib ac_simps)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   904
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   905
lemma module_hom_compose_scale:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   906
  "module_hom s1 s2 (\<lambda>x. s2 (f x) (c))"
69064
5840724b1d71 Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents: 68189
diff changeset
   907
  if "module_hom s1 (*) f"
68072
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   908
proof -
69064
5840724b1d71 Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents: 68189
diff changeset
   909
  interpret mh: module_hom s1 "(*)" f by fact
68072
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   910
  show ?thesis
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   911
    by unfold_locales (simp_all add: mh.add mh.scale m2.scale_left_distrib)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   912
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   913
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   914
lemma bij_module_hom_imp_inv_module_hom: "module_hom scale1 scale2 f \<Longrightarrow> bij f \<Longrightarrow>
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   915
  module_hom scale2 scale1 (inv f)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   916
  by (auto simp: module_hom_iff bij_is_surj bij_is_inj surj_f_inv_f
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   917
      intro!: Hilbert_Choice.inv_f_eq)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   918
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   919
lemma module_hom_sum: "(\<And>i. i \<in> I \<Longrightarrow> module_hom s1 s2 (f i)) \<Longrightarrow> (I = {} \<Longrightarrow> module s1 \<and> module s2) \<Longrightarrow> module_hom s1 s2 (\<lambda>x. \<Sum>i\<in>I. f i x)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   920
  apply (induction I rule: infinite_finite_induct)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   921
  apply (auto intro!: module_hom_zero module_hom_add)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   922
  using m1.module_axioms m2.module_axioms by blast
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   923
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   924
lemma module_hom_eq_on_span: "f x = g x"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   925
  if "module_hom s1 s2 f" "module_hom s1 s2 g"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   926
  and "(\<And>x. x \<in> B \<Longrightarrow> f x = g x)" "x \<in> m1.span B"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   927
proof -
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   928
  interpret module_hom s1 s2 "\<lambda>x. f x - g x"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   929
    by (rule module_hom_sub that)+
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   930
  from eq_0_on_span[OF _ that(4)] that(3) show ?thesis by auto
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   931
qed
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   932
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   933
end
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   934
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   935
context module begin
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   936
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   937
lemma module_hom_scale_self[simp]:
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   938
  "module_hom scale scale (\<lambda>x. scale c x)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   939
  using module_axioms module_hom_iff scale_left_commute scale_right_distrib by blast
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   940
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   941
lemma module_hom_scale_left[simp]:
69064
5840724b1d71 Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents: 68189
diff changeset
   942
  "module_hom (*) scale (\<lambda>r. scale r x)"
68072
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   943
  by unfold_locales (auto simp: algebra_simps)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   944
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   945
lemma module_hom_id: "module_hom scale scale id"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   946
  by (simp add: module_hom_iff module_axioms)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   947
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   948
lemma module_hom_ident: "module_hom scale scale (\<lambda>x. x)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   949
  by (simp add: module_hom_iff module_axioms)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   950
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   951
lemma module_hom_uminus: "module_hom scale scale uminus"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   952
  by (simp add: module_hom_iff module_axioms)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   953
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   954
end
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   955
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   956
lemma module_hom_compose: "module_hom s1 s2 f \<Longrightarrow> module_hom s2 s3 g \<Longrightarrow> module_hom s1 s3 (g o f)"
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   957
  by (auto simp: module_hom_iff)
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   958
493b818e8e10 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff changeset
   959
end