author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 63882  018998c00003 
child 66453  cc19f7ca2ed6 
permissions  rwrr 
30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
27487
diff
changeset

1 
(* Author: Tobias Nipkow, 2007 *) 
26166  2 

60500  3 
section \<open>Lists as vectors\<close> 
26166  4 

5 
theory ListVector 

30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
27487
diff
changeset

6 
imports List Main 
26166  7 
begin 
8 

60500  9 
text\<open>\noindent 
26166  10 
A vectorspace like structure of lists and arithmetic operations on them. 
60500  11 
Is only a vector space if restricted to lists of the same length.\<close> 
26166  12 

60500  13 
text\<open>Multiplication with a scalar:\<close> 
26166  14 

15 
abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70) 

16 
where "x *\<^sub>s xs \<equiv> map (op * x) xs" 

17 

18 
lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs" 

19 
by (induct xs) simp_all 

20 

61585  21 
subsection \<open>\<open>+\<close> and \<open>\<close>\<close> 
26166  22 

23 
fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" 

24 
where 

25 
"zipwith0 f [] [] = []"  

26 
"zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys"  

27 
"zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []"  

28 
"zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys" 

29 

27109  30 
instantiation list :: ("{zero, plus}") plus 
31 
begin 

32 

33 
definition 

34 
list_add_def: "op + = zipwith0 (op +)" 

35 

36 
instance .. 

37 

38 
end 

39 

40 
instantiation list :: ("{zero, uminus}") uminus 

41 
begin 

26166  42 

27109  43 
definition 
44 
list_uminus_def: "uminus = map uminus" 

45 

46 
instance .. 

47 

48 
end 

26166  49 

27109  50 
instantiation list :: ("{zero,minus}") minus 
51 
begin 

52 

53 
definition 

54 
list_diff_def: "op  = zipwith0 (op )" 

55 

56 
instance .. 

57 

58 
end 

26166  59 

60 
lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys" 

61 
by(induct ys) simp_all 

62 

63 
lemma list_add_Nil[simp]: "[] + xs = (xs::'a::monoid_add list)" 

64 
by (induct xs) (auto simp:list_add_def) 

65 

66 
lemma list_add_Nil2[simp]: "xs + [] = (xs::'a::monoid_add list)" 

67 
by (induct xs) (auto simp:list_add_def) 

68 

69 
lemma list_add_Cons[simp]: "(x#xs) + (y#ys) = (x+y)#(xs+ys)" 

70 
by(auto simp:list_add_def) 

71 

72 
lemma list_diff_Nil[simp]: "[]  xs = (xs::'a::group_add list)" 

73 
by (induct xs) (auto simp:list_diff_def list_uminus_def) 

74 

75 
lemma list_diff_Nil2[simp]: "xs  [] = (xs::'a::group_add list)" 

76 
by (induct xs) (auto simp:list_diff_def) 

77 

78 
lemma list_diff_Cons_Cons[simp]: "(x#xs)  (y#ys) = (xy)#(xsys)" 

79 
by (induct xs) (auto simp:list_diff_def) 

80 

81 
lemma list_uminus_Cons[simp]: "(x#xs) = (x)#(xs)" 

82 
by (induct xs) (auto simp:list_uminus_def) 

83 

84 
lemma self_list_diff: 

85 
"xs  xs = replicate (length(xs::'a::group_add list)) 0" 

86 
by(induct xs) simp_all 

87 

88 
lemma list_add_assoc: fixes xs :: "'a::monoid_add list" 

89 
shows "(xs+ys)+zs = xs+(ys+zs)" 

90 
apply(induct xs arbitrary: ys zs) 

91 
apply simp 

92 
apply(case_tac ys) 

93 
apply(simp) 

94 
apply(simp) 

95 
apply(case_tac zs) 

96 
apply(simp) 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
49962
diff
changeset

97 
apply(simp add: add.assoc) 
26166  98 
done 
99 

100 
subsection "Inner product" 

101 

102 
definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" ("\<langle>_,_\<rangle>") where 

103 
"\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)" 

104 

105 
lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0" 

49961  106 
by(simp add: iprod_def) 
26166  107 

108 
lemma iprod_Nil2[simp]: "\<langle>xs,[]\<rangle> = 0" 

49961  109 
by(simp add: iprod_def) 
26166  110 

111 
lemma iprod_Cons[simp]: "\<langle>x#xs,y#ys\<rangle> = x*y + \<langle>xs,ys\<rangle>" 

49961  112 
by(simp add: iprod_def) 
26166  113 

114 
lemma iprod0_if_coeffs0: "\<forall>c\<in>set cs. c = 0 \<Longrightarrow> \<langle>cs,xs\<rangle> = 0" 

115 
apply(induct cs arbitrary:xs) 

116 
apply simp 

117 
apply(case_tac xs) apply simp 

118 
apply auto 

119 
done 

120 

121 
lemma iprod_uminus[simp]: "\<langle>xs,ys\<rangle> = \<langle>xs,ys\<rangle>" 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
61585
diff
changeset

122 
by(simp add: iprod_def uminus_sum_list_map o_def split_def map_zip_map list_uminus_def) 
26166  123 

124 
lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>" 

125 
apply(induct xs arbitrary: ys zs) 

126 
apply (simp add: o_def split_def) 

127 
apply(case_tac ys) 

128 
apply simp 

129 
apply(case_tac zs) 

130 
apply (simp) 

49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
49961
diff
changeset

131 
apply(simp add: distrib_right) 
26166  132 
done 
133 

134 
lemma iprod_left_diff_distrib: "\<langle>xs  ys, zs\<rangle> = \<langle>xs,zs\<rangle>  \<langle>ys,zs\<rangle>" 

135 
apply(induct xs arbitrary: ys zs) 

136 
apply (simp add: o_def split_def) 

137 
apply(case_tac ys) 

138 
apply simp 

139 
apply(case_tac zs) 

140 
apply (simp) 

49961  141 
apply(simp add: left_diff_distrib) 
26166  142 
done 
143 

144 
lemma iprod_assoc: "\<langle>x *\<^sub>s xs, ys\<rangle> = x * \<langle>xs,ys\<rangle>" 

145 
apply(induct xs arbitrary: ys) 

146 
apply simp 

147 
apply(case_tac ys) 

148 
apply (simp) 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
49962
diff
changeset

149 
apply (simp add: distrib_left mult.assoc) 
26166  150 
done 
151 

49961  152 
end 