Theory Utility
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