equal
deleted
inserted
replaced
117 apply(case_tac xs) apply simp |
117 apply(case_tac xs) apply simp |
118 apply auto |
118 apply auto |
119 done |
119 done |
120 |
120 |
121 lemma iprod_uminus[simp]: "\<langle>-xs,ys\<rangle> = -\<langle>xs,ys\<rangle>" |
121 lemma iprod_uminus[simp]: "\<langle>-xs,ys\<rangle> = -\<langle>xs,ys\<rangle>" |
122 by(simp add: iprod_def uminus_listsum_map o_def split_def map_zip_map list_uminus_def) |
122 by(simp add: iprod_def uminus_sum_list_map o_def split_def map_zip_map list_uminus_def) |
123 |
123 |
124 lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>" |
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) |
125 apply(induct xs arbitrary: ys zs) |
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) |