(* Title: Executable Matrix Operations on Matrices of Arbitrary Dimensions Author: Christian Sternagel <christian.sternagel@uibk.ac.at> René Thiemann <rene.thiemann@uibk.ac.at> Maintainer: Christian Sternagel and René Thiemann License: LGPL *) (* Copyright 2010 Christian Sternagel, René Thiemann This file is part of IsaFoR/CeTA. IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with IsaFoR/CeTA. If not, see <http://www.gnu.org/licenses/>. *) section ‹Utility Functions and Lemmas› theory Utility imports Main begin subsection ‹Miscellaneous› lemma ballI2[Pure.intro]: assumes "⋀x y. (x, y) ∈ A ⟹ P x y" shows "∀(x, y)∈A. P x y" using assms by auto lemma infinite_imp_elem: "¬ finite A ⟹ ∃ x. x ∈ A" by (cases "A = {}", auto) lemma infinite_imp_many_elems: "infinite A ⟹ ∃ xs. set xs ⊆ A ∧ length xs = n ∧ distinct xs" proof (induct n arbitrary: A) case (Suc n) from infinite_imp_elem[OF Suc(2)] obtain x where x: "x ∈ A" by auto from Suc(2) have "infinite (A - {x})" by auto from Suc(1)[OF this] obtain xs where "set xs ⊆ A - {x}" and "length xs = n" and "distinct xs" by auto with x show ?case by (intro exI[of _ "x # xs"], auto) qed auto lemma inf_pigeonhole_principle: assumes "∀k::nat. ∃i<n::nat. f k i" shows "∃i<n. ∀k. ∃k'≥k. f k' i" proof - have nfin: "~ finite (UNIV :: nat set)" by auto have fin: "finite ({i. i < n})" by auto from pigeonhole_infinite_rel[OF nfin fin] assms obtain i where i: "i < n" and nfin: "¬ finite {a. f a i}" by auto show ?thesis proof (intro exI conjI, rule i, intro allI) fix k have "finite {a. f a i ∧ a < k}" by auto with nfin have "¬ finite ({a. f a i} - {a. f a i ∧ a < k})" by auto from infinite_imp_elem[OF this] obtain a where "f a i" and "a ≥ k" by auto thus "∃ k' ≥ k. f k' i" by force qed qed lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (λ i. f (Suc i)) [0 ..< n]" by (induct n arbitrary: f, auto) lemma map_upt_add: "map f [0 ..< n + m] = map f [0 ..< n] @ map (λ i. f (i + n)) [0 ..< m]" proof (induct n arbitrary: f) case (Suc n f) have "map f [0 ..< Suc n + m] = map f [0 ..< Suc (n+m)]" by simp also have "… = f 0 # map (λ i. f (Suc i)) [0 ..< n + m]" unfolding map_upt_Suc .. finally show ?case unfolding Suc map_upt_Suc by simp qed simp lemma map_upt_split: assumes i: "i < n" shows "map f [0 ..< n] = map f [0 ..< i] @ f i # map (λ j. f (j + Suc i)) [0 ..< n - Suc i]" proof - from i have "n = i + Suc 0 + (n - Suc i)" by arith hence id: "[0 ..< n] = [0 ..< i + Suc 0 + (n - Suc i)]" by simp show ?thesis unfolding id unfolding map_upt_add by auto qed lemma all_Suc_conv: "(∀i<Suc n. P i) ⟷ P 0 ∧ (∀i<n. P (Suc i))" (is "?l = ?r") proof assume ?l thus ?r by auto next assume ?r show ?l proof (intro allI impI) fix i assume "i < Suc n" with ‹?r› show "P i" by (cases i, auto) qed qed lemma ex_Suc_conv: "(∃i<Suc n. P i) ⟷ P 0 ∨ (∃i<n. P (Suc i))" (is "?l = ?r") using all_Suc_conv[of n "λi. ¬ P i"] by blast fun sorted_list_subset :: "'a :: linorder list ⇒ 'a list ⇒ 'a option" where "sorted_list_subset (a # as) (b # bs) = (if a = b then sorted_list_subset as (b # bs) else if a > b then sorted_list_subset (a # as) bs else Some a)" | "sorted_list_subset [] _ = None" | "sorted_list_subset (a # _) [] = Some a" lemma sorted_list_subset: assumes "sorted as" and "sorted bs" shows "(sorted_list_subset as bs = None) = (set as ⊆ set bs)" using assms proof (induct rule: sorted_list_subset.induct) case (2 bs) thus ?case by auto next case (3 a as) thus ?case by auto next case (1 a as b bs) from 1(3) have sas: "sorted as" and a: "⋀ a'. a' ∈ set as ⟹ a ≤ a'" by (auto) from 1(4) have sbs: "sorted bs" and b: "⋀ b'. b' ∈ set bs ⟹ b ≤ b'" by (auto) show ?case proof (cases "a = b") case True from 1(1)[OF this sas 1(4)] True show ?thesis by auto next case False note oFalse = this show ?thesis proof (cases "a > b") case True with a b have "b ∉ set as" by force with 1(2)[OF False True 1(3) sbs] False True show ?thesis by auto next case False with oFalse have "a < b" by auto with a b have "a ∉ set bs" by force with oFalse False show ?thesis by auto qed qed qed lemma zip_nth_conv: "length xs = length ys ⟹ zip xs ys = map (λ i. (xs ! i, ys ! i)) [0 ..< length ys]" proof (induct xs arbitrary: ys, simp) case (Cons x xs) then obtain y yys where ys: "ys = y # yys" by (cases ys, auto) with Cons have len: "length xs = length yys" by simp show ?case unfolding ys by (simp del: upt_Suc add: map_upt_Suc, unfold Cons(1)[OF len], simp) qed lemma nth_map_conv: assumes "length xs = length ys" and "∀i<length xs. f (xs ! i) = g (ys ! i)" shows "map f xs = map g ys" using assms proof (induct xs arbitrary: ys) case (Cons x xs) thus ?case proof (induct ys) case (Cons y ys) have "∀i<length xs. f (xs ! i) = g (ys ! i)" proof (intro allI impI) fix i assume "i < length xs" thus "f (xs ! i) = g (ys ! i)" using Cons(4) by force qed with Cons show ?case by auto qed simp qed simp lemma sum_list_0: "⟦⋀ x. x ∈ set xs ⟹ x = 0⟧ ⟹ sum_list xs = 0" by (induct xs, auto) lemma foldr_foldr_concat: "foldr (foldr f) m a = foldr f (concat m) a" proof (induct m arbitrary: a) case Nil show ?case by simp next case (Cons v m a) show ?case unfolding concat.simps foldr_Cons o_def Cons unfolding foldr_append by simp qed lemma sum_list_double_concat: fixes f :: "'b ⇒ 'c ⇒ 'a :: comm_monoid_add" and g as bs shows "sum_list (concat (map (λ i. map (λ j. f i j + g i j) as) bs)) = sum_list (concat (map (λ i. map (λ j. f i j) as) bs)) + sum_list (concat (map (λ i. map (λ j. g i j) as) bs))" proof (induct bs) case Nil thus ?case by simp next case (Cons b bs) have id: "(∑j←as. f b j + g b j) = sum_list (map (f b) as) + sum_list (map (g b) as)" by (induct as, auto simp: ac_simps) show ?case unfolding list.map concat.simps sum_list_append unfolding Cons unfolding id by (simp add: ac_simps) qed fun max_list :: "nat list ⇒ nat" where "max_list [] = 0" | "max_list (x # xs) = max x (max_list xs)" lemma max_list: "x ∈ set xs ⟹ x ≤ max_list xs" by (induct xs) auto lemma max_list_mem: "xs ≠ [] ⟹ max_list xs ∈ set xs" proof (induct xs) case (Cons x xs) show ?case proof (cases "x ≥ max_list xs") case True thus ?thesis by auto next case False hence max: "max_list xs > x" by auto hence nil: "xs ≠ []" by (cases xs, auto) from max have max: "max x (max_list xs) = max_list xs" by auto from Cons(1)[OF nil] max show ?thesis by auto qed qed simp lemma max_list_set: "max_list xs = (if set xs = {} then 0 else (THE x. x ∈ set xs ∧ (∀ y ∈ set xs. y ≤ x)))" proof (cases "xs = []") case True thus ?thesis by simp next case False note p = max_list_mem[OF this] max_list[of _ xs] from False have id: "(set xs = {}) = False" by simp show ?thesis unfolding id if_False proof (rule the_equality[symmetric], intro conjI ballI, rule p, rule p) fix x assume "x ∈ set xs ∧ (∀ y ∈ set xs. y ≤ x)" hence mem: "x ∈ set xs" and le: "⋀ y. y ∈ set xs ⟹ y ≤ x" by auto from max_list[OF mem] le[OF max_list_mem[OF False]] show "x = max_list xs" by simp qed qed lemma max_list_eq_set: "set xs = set ys ⟹ max_list xs = max_list ys" unfolding max_list_set by simp lemma all_less_two: "(∀ i < Suc (Suc 0). P i) = (P 0 ∧ P (Suc 0))" (is "?l = ?r") proof assume ?r show ?l proof(intro allI impI) fix i assume "i < Suc (Suc 0)" hence "i = 0 ∨ i = Suc 0" by auto with ‹?r› show "P i" by auto qed qed auto text ‹Induction over a finite set of natural numbers.› lemma bound_nat_induct[consumes 1]: assumes "n ∈ {l..u}" and "P l" and "⋀n. ⟦P n; n ∈ {l..<u}⟧ ⟹ P (Suc n)" shows "P n" using assms proof (induct n) case (Suc n) thus ?case by (cases "Suc n = l") auto qed simp end