section ‹Auxiliary Results›
theory Simplex_Auxiliary
imports
"HOL-Library.Permutation"
"HOL-Library.Mapping"
begin
lemma map_reindex:
assumes "∀ i < length l. g (l ! i) = f i"
shows "map f [0..<length l] = map g l"
using assms
by (induct l rule: rev_induct) (auto simp add: nth_append split: if_splits)
lemma map_parametrize_idx:
"map f l = map (λi. f (l ! i)) [0..<length l]"
by (induct l rule: rev_induct) (auto simp add: nth_append)
lemma last_tl:
assumes "length l > 1"
shows "last (tl l) = last l"
using assms
by (induct l) auto
lemma hd_tl:
assumes "length l > 1"
shows "hd (tl l) = l ! 1"
using assms
by (induct l) (auto simp add: hd_conv_nth)
lemma butlast_empty_conv_length:
shows "(butlast l = []) = (length l ≤ 1)"
by (induct l) (auto split: if_splits)
lemma butlast_nth:
assumes "n + 1 < length l"
shows "butlast l ! n = l ! n"
using assms
by (induct l rule: rev_induct) (auto simp add: nth_append)
lemma last_take_conv_nth:
assumes "0 < n" "n ≤ length l"
shows "last (take n l) = l ! (n - 1)"
using assms
by (cases "l = []") (auto simp add: last_conv_nth min_def)
lemma tl_nth:
assumes "l ≠ []"
shows "tl l ! n = l ! (n + 1)"
using assms
by (induct l) auto
lemma interval_3split:
assumes "i < n"
shows "[0..<n] = [0..<i] @ [i] @ [i+1..<n]"
proof-
have "[0..<n] = [0..<i + 1] @ [i + 1..<n]"
using upt_add_eq_append[of 0 "i + 1" "n - i - 1"]
using ‹i < n›
by (auto simp del: upt_Suc)
then show ?thesis
by simp
qed
abbreviation "list_min l ≡ foldl min (hd l) (tl l)"
lemma list_min_Min[simp]: "l ≠ [] ⟹ list_min l = Min (set l)"
proof (induct l rule: rev_induct)
case (snoc a l')
then show ?case
by (cases "l' = []") (auto simp add: ac_simps)
qed simp
definition min_satisfying :: "(('a::linorder) ⇒ bool) ⇒ 'a list ⇒ 'a option" where
"min_satisfying P l ≡
let xs = filter P l in
if xs = [] then None else Some (list_min xs)"
lemma min_satisfying_None:
"min_satisfying P l = None ⟶
(∀ x ∈ set l. ¬ P x)"
unfolding min_satisfying_def Let_def
by (simp add: filter_empty_conv)
lemma min_satisfying_Some:
"min_satisfying P l = Some x ⟶
x ∈ set l ∧ P x ∧ (∀ x' ∈ set l. x' < x ⟶ ¬ P x')"
proof (safe)
let ?xs = "filter P l"
assume "min_satisfying P l = Some x"
then have "set ?xs ≠ {}" "x = Min (set ?xs)"
unfolding min_satisfying_def Let_def
by (auto split: if_splits simp add: filter_empty_conv)
then show "x ∈ set l" "P x"
using Min_in[of "set ?xs"]
by simp_all
fix x'
assume "x' ∈ set l" "P x'" "x' < x"
have "x' ∉ set ?xs"
proof (rule ccontr)
assume "¬ ?thesis"
then have "x' ≥ x"
using ‹x = Min (set ?xs)›
by simp
then show False
using ‹x' < x›
by simp
qed
then show "False"
using ‹x' ∈ set l› ‹P x'›
by simp
qed
lemma min_element:
fixes k :: nat
assumes "∃ (m::nat). P m"
shows "∃ mm. P mm ∧ (∀ m'. m' < mm ⟶ ¬ P m')"
proof-
from assms obtain m where "P m"
by auto
show ?thesis
proof (cases "∀m'<m. ¬ P m'")
case True
then show ?thesis
using ‹P m›
by auto
next
case False
then show ?thesis
proof (induct m)
case 0
then show ?case
by auto
next
case (Suc m')
then show ?case
by (cases "¬ (∀m'a<m'. ¬ P m'a)") auto
qed
qed
qed
lemma finite_fun_args:
assumes "finite A" "∀ a ∈ A. finite (B a)"
shows "finite {f. (∀ a. if a ∈ A then f a ∈ B a else f a = f0 a)}" (is "finite (?F A)")
using assms
proof (induct)
case empty
have "?F {} = {λ x. f0 x}"
by auto
then show ?case
by auto
next
case (insert a A')
then have "finite (?F A')"
by auto
let ?f = "λ f. {f'. (∀ a'. if a = a' then f' a ∈ B a else f' a' = f a')}"
have "∀ f ∈ ?F A'. finite (?f f)"
proof
fix f
assume "f ∈ ?F A'"
then have "?f f = (λ b. f (a := b)) ` B a"
by (force split: if_splits)
then show "finite (?f f)"
using ‹∀a∈insert a A'. finite (B a)›
by auto
qed
then have "finite (⋃ (?f ` (?F A')))"
using ‹finite (?F A')›
by auto
moreover
have "?F (insert a A') = ⋃ (?f ` (?F A'))"
proof
show "?F (insert a A') ⊆ ⋃ (?f ` (?F A'))"
proof
fix f
assume "f ∈ ?F (insert a A')"
then have "f ∈ ?f (f (a := f0 a))" "f (a := f0 a) ∈ ?F A'"
using ‹a ∉ A'›
by auto
then show "f ∈ ⋃ (?f ` (?F A'))"
by blast
qed
next
show "⋃ (?f ` (?F A')) ⊆ ?F (insert a A')"
proof
fix f
assume "f ∈ ⋃ (?f ` (?F A'))"
then obtain f0 where "f0 ∈ ?F A'" "f ∈ ?f f0"
by auto
then show "f ∈ ?F (insert a A')"
using ‹a ∉ A'›
by (force split: if_splits)
qed
qed
ultimately
show ?case
by simp
qed
lemma foldl_mapping_update:
assumes "X ∈ set l" "distinct (map f l)"
shows "Mapping.lookup (foldl (λm a. Mapping.update (f a) (g a) m) i l) (f X) = Some (g X)"
using assms
proof(induct l rule:rev_induct)
case Nil
then show ?case
by simp
next
case (snoc h t)
show ?case
proof (cases "f h = f X")
case True
then show ?thesis using snoc by (auto simp: lookup_update)
next
case False
show ?thesis by (simp add: lookup_update' False, rule snoc, insert False snoc, auto)
qed
qed
end