equal
deleted
inserted
replaced
126 apply (simp add: o_def split_def) |
126 apply (simp add: o_def split_def) |
127 apply(case_tac ys) |
127 apply(case_tac ys) |
128 apply simp |
128 apply simp |
129 apply(case_tac zs) |
129 apply(case_tac zs) |
130 apply (simp) |
130 apply (simp) |
131 apply(simp add: left_distrib) |
131 apply(simp add: distrib_right) |
132 done |
132 done |
133 |
133 |
134 lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>" |
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) |
135 apply(induct xs arbitrary: ys zs) |
136 apply (simp add: o_def split_def) |
136 apply (simp add: o_def split_def) |
144 lemma iprod_assoc: "\<langle>x *\<^sub>s xs, ys\<rangle> = x * \<langle>xs,ys\<rangle>" |
144 lemma iprod_assoc: "\<langle>x *\<^sub>s xs, ys\<rangle> = x * \<langle>xs,ys\<rangle>" |
145 apply(induct xs arbitrary: ys) |
145 apply(induct xs arbitrary: ys) |
146 apply simp |
146 apply simp |
147 apply(case_tac ys) |
147 apply(case_tac ys) |
148 apply (simp) |
148 apply (simp) |
149 apply (simp add: right_distrib mult_assoc) |
149 apply (simp add: distrib_left mult_assoc) |
150 done |
150 done |
151 |
151 |
152 end |
152 end |