289 |
289 |
290 values [random_dseq 2, 2, 15] 6 "{(M::int list list, n, m). matrix M n m}" |
290 values [random_dseq 2, 2, 15] 6 "{(M::int list list, n, m). matrix M n m}" |
291 |
291 |
292 definition "scalar_product v w = (\<Sum> (x, y)\<leftarrow>zip v w. x * y)" |
292 definition "scalar_product v w = (\<Sum> (x, y)\<leftarrow>zip v w. x * y)" |
293 |
293 |
294 definition mv :: "('a \<Colon> semiring_0) list list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
294 definition mv :: "('a :: semiring_0) list list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
295 where [simp]: "mv M v = map (scalar_product v) M" |
295 where [simp]: "mv M v = map (scalar_product v) M" |
296 text {* |
296 text {* |
297 This defines the matrix vector multiplication. To work properly @{term |
297 This defines the matrix vector multiplication. To work properly @{term |
298 "matrix M m n \<and> length v = n"} must hold. |
298 "matrix M m n \<and> length v = n"} must hold. |
299 *} |
299 *} |
304 (* |
304 (* |
305 lemma sparsify_length: "(i, x) \<in> set (sparsify xs) \<Longrightarrow> i < length xs" |
305 lemma sparsify_length: "(i, x) \<in> set (sparsify xs) \<Longrightarrow> i < length xs" |
306 by (auto simp: sparsify_def set_zip) |
306 by (auto simp: sparsify_def set_zip) |
307 |
307 |
308 lemma listsum_sparsify[simp]: |
308 lemma listsum_sparsify[simp]: |
309 fixes v :: "('a \<Colon> semiring_0) list" |
309 fixes v :: "('a :: semiring_0) list" |
310 assumes "length w = length v" |
310 assumes "length w = length v" |
311 shows "(\<Sum>x\<leftarrow>sparsify w. (\<lambda>(i, x). v ! i) x * snd x) = scalar_product v w" |
311 shows "(\<Sum>x\<leftarrow>sparsify w. (\<lambda>(i, x). v ! i) x * snd x) = scalar_product v w" |
312 (is "(\<Sum>x\<leftarrow>_. ?f x) = _") |
312 (is "(\<Sum>x\<leftarrow>_. ?f x) = _") |
313 unfolding sparsify_def scalar_product_def |
313 unfolding sparsify_def scalar_product_def |
314 using assms listsum_map_filter[where f="?f" and P="\<lambda> i. snd i \<noteq> (0::'a)"] |
314 using assms listsum_map_filter[where f="?f" and P="\<lambda> i. snd i \<noteq> (0::'a)"] |
315 by (simp add: listsum_setsum) |
315 by (simp add: listsum_setsum) |
316 *) |
316 *) |
317 definition [simp]: "unzip w = (map fst w, map snd w)" |
317 definition [simp]: "unzip w = (map fst w, map snd w)" |
318 |
318 |
319 primrec insert :: "('a \<Rightarrow> 'b \<Colon> linorder) => 'a \<Rightarrow> 'a list => 'a list" where |
319 primrec insert :: "('a \<Rightarrow> 'b :: linorder) => 'a \<Rightarrow> 'a list => 'a list" where |
320 "insert f x [] = [x]" | |
320 "insert f x [] = [x]" | |
321 "insert f x (y # ys) = (if f y < f x then y # insert f x ys else x # y # ys)" |
321 "insert f x (y # ys) = (if f y < f x then y # insert f x ys else x # y # ys)" |
322 |
322 |
323 primrec sort :: "('a \<Rightarrow> 'b \<Colon> linorder) \<Rightarrow> 'a list => 'a list" where |
323 primrec sort :: "('a \<Rightarrow> 'b :: linorder) \<Rightarrow> 'a list => 'a list" where |
324 "sort f [] = []" | |
324 "sort f [] = []" | |
325 "sort f (x # xs) = insert f x (sort f xs)" |
325 "sort f (x # xs) = insert f x (sort f xs)" |
326 |
326 |
327 definition |
327 definition |
328 "length_permutate M = (unzip o sort (length o snd)) (zip [0 ..< length M] M)" |
328 "length_permutate M = (unzip o sort (length o snd)) (zip [0 ..< length M] M)" |