theory WB_List_More
imports Nested_Multisets_Ordinals.Multiset_More "HOL-Library.Finite_Map"
"HOL-Eisbach.Eisbach"
"HOL-Eisbach.Eisbach_Tools"
begin
text ‹This theory contains various lemmas that have been used in the formalisation. Some of them
could probably be moved to the Isabelle distribution or
\<^theory>‹Nested_Multisets_Ordinals.Multiset_More›.
›
text ‹More Sledgehammer parameters›
section ‹Various Lemmas›
subsection ‹Not-Related to Refinement or lists›
text ‹
Unlike clarify/auto/simp, this does not split tuple of the form \<^term>‹∃T. P T› in the assumption.
After calling it, as the variable are not quantified anymore, the simproc does not trigger,
allowing to safely call auto/simp/...
›
method normalize_goal =
(match premises in
J[thin]: ‹∃x. _› ⇒ ‹rule exE[OF J]›
¦ J[thin]: ‹_ ∧ _› ⇒ ‹rule conjE[OF J]›
)
text ‹Close to the theorem @{thm [source] nat_less_induct} (@{thm nat_less_induct}), but with a
separation between the zero and non-zero case.›
lemma nat_less_induct_case[case_names 0 Suc]:
assumes
‹P 0› and
‹⋀n. (∀m < Suc n. P m) ⟹ P (Suc n)›
shows ‹P n›
apply (induction rule: nat_less_induct)
by (rename_tac n, case_tac n) (auto intro: assms)
text ‹This is only proved in simple cases by auto. In assumptions, nothing happens, and
the theorem @{thm [source] if_split_asm} can blow up goals (because of other if-expressions either
in the context or as simplification rules).›
lemma if_0_1_ge_0[simp]:
‹0 < (if P then a else (0::nat)) ⟷ P ∧ 0 < a›
by auto
lemma bex_lessI: "P j ⟹ j < n ⟹ ∃j<n. P j"
by auto
lemma bex_gtI: "P j ⟹ j > n ⟹ ∃j>n. P j"
by auto
lemma bex_geI: "P j ⟹ j ≥ n ⟹ ∃j≥n. P j"
by auto
lemma bex_leI: "P j ⟹ j ≤ n ⟹ ∃j≤n. P j"
by auto
text ‹Bounded function have not yet been defined in Isabelle.›
definition bounded :: "('a ⇒ 'b::ord) ⇒ bool" where
‹bounded f ⟷ (∃b. ∀n. f n ≤ b)›
abbreviation unbounded :: ‹('a ⇒ 'b::ord) ⇒ bool› where
‹unbounded f ≡ ¬ bounded f›
lemma not_bounded_nat_exists_larger:
fixes f :: ‹nat ⇒ nat›
assumes unbound: ‹unbounded f›
shows ‹∃n. f n > m ∧ n > n⇩0›
proof (rule ccontr)
assume H: ‹¬ ?thesis›
have ‹finite {f n|n. n ≤ n⇩0}›
by auto
have ‹⋀n. f n ≤ Max ({f n|n. n ≤ n⇩0} ∪ {m})›
apply (case_tac ‹n ≤ n⇩0›)
apply (metis (mono_tags, lifting) Max_ge Un_insert_right ‹finite {f n |n. n ≤ n⇩0}›
finite_insert insertCI mem_Collect_eq sup_bot.right_neutral)
by (metis (no_types, lifting) H Max_less_iff Un_insert_right ‹finite {f n |n. n ≤ n⇩0}›
finite_insert insertI1 insert_not_empty leI sup_bot.right_neutral)
then show False
using unbound unfolding bounded_def by auto
qed
text ‹A function is bounded iff its product with a non-zero constant is bounded. The non-zero
condition is needed only for the reverse implication (see for example @{term ‹k = (0::nat)›} and
@{term ‹f = (λi. i)›} for a counter-example).›
lemma bounded_const_product:
fixes k :: nat and f :: ‹nat ⇒ nat›
assumes ‹k > 0›
shows ‹bounded f ⟷ bounded (λi. k * f i)›
unfolding bounded_def apply (rule iffI)
using mult_le_mono2 apply blast
by (metis Suc_leI add.right_neutral assms mult.commute mult_0_right mult_Suc_right mult_le_mono
nat_mult_le_cancel1)
lemma bounded_const_add:
fixes k :: nat and f :: ‹nat ⇒ nat›
assumes ‹k > 0›
shows ‹bounded f ⟷ bounded (λi. k + f i)›
unfolding bounded_def apply (rule iffI)
using nat_add_left_cancel_le apply blast
using add_leE by blast
text ‹This lemma is not used, but here to show that property that can be expected from
@{term bounded} holds.›
lemma bounded_finite_linorder:
fixes f :: ‹'a::finite ⇒ 'b :: {linorder}›
shows ‹bounded f›
proof -
have ‹finite (f ` UNIV)›
by simp
then have ‹⋀x. f x ≤ Max (f ` UNIV)›
by (auto intro: Max_ge)
then show ?thesis
unfolding bounded_def by blast
qed
section ‹More Lists›
subsection ‹set, nth, tl›
lemma ex_geI: ‹P n ⟹ n ≥ m ⟹ ∃n≥m. P n›
by auto
lemma Ball_atLeastLessThan_iff: ‹(∀L∈{a..<b}. P L) ⟷ (∀L. L ≥ a ∧ L < b ⟶ P L) ›
unfolding set_nths by auto
lemma nth_in_set_tl: ‹i > 0 ⟹ i < length xs ⟹ xs ! i ∈ set (tl xs)›
by (cases xs) auto
lemma tl_drop_def: ‹tl N = drop 1 N›
by (cases N) auto
lemma in_set_remove1D:
‹a ∈ set (remove1 x xs) ⟹ a ∈ set xs›
by (meson notin_set_remove1)
lemma take_length_takeWhile_eq_takeWhile:
‹take (length (takeWhile P xs)) xs = takeWhile P xs›
by (induction xs) auto
lemma fold_cons_replicate: ‹fold (λ_ xs. a # xs) [0..<n] xs = replicate n a @ xs›
by (induction n) auto
lemma Collect_minus_single_Collect: ‹{x. P x} - {a} = {x . P x ∧ x ≠ a}›
by auto
lemma in_set_image_subsetD: ‹ f ` A ⊆ B ⟹ x ∈ A ⟹f x ∈ B›
by blast
lemma mset_tl:
‹mset (tl xs) = remove1_mset (hd xs) (mset xs)›
by (cases xs) auto
lemma hd_list_update_If:
‹outl' ≠ [] ⟹ hd (outl'[i := w]) = (if i = 0 then w else hd outl')›
by (cases outl') (auto split: nat.splits)
lemma list_update_id':
‹x = xs ! i ⟹ xs[i := x] = xs›
by auto
text ‹
This lemma is not general enough to move to Isabelle, but might be interesting in other
cases.›
lemma set_Collect_Pair_to_fst_snd:
‹{((a, b), (a', b')). P a b a' b'} = {(e, f). P (fst e) (snd e) (fst f) (snd f)}›
by auto
lemma butlast_Nil_iff: ‹butlast xs = [] ⟷ length xs = 1 ∨ length xs = 0›
by (cases xs) auto
lemma Set_remove_diff_insert: ‹a ∈ B - A ⟹ B - Set.remove a A = insert a (B - A)›
by auto
lemma Set_insert_diff_remove: ‹B - insert a A = Set.remove a (B - A)›
by auto
lemma Set_remove_insert: ‹a ∉ A' ⟹ Set.remove a (insert a A') = A'›
by (auto simp: Set.remove_def)
lemma diff_eq_insertD:
‹B - A = insert a A' ⟹ a ∈ B›
by auto
lemma in_set_tlD: ‹x ∈ set (tl xs) ⟹ x ∈ set xs›
by (cases xs) auto
text ‹This lemmma is only useful if \<^term>‹set xs› can be simplified (which also means that this
simp-rule should not be used...)›
lemma (in -) in_list_in_setD: ‹xs = it @ x # σ ⟹ x ∈ set xs›
by auto
lemma Collect_eq_comp': ‹ {(x, y). P x y} O {(c, a). c = f a} = {(x, a). P x (f a)}›
by auto
lemma (in -) filter_disj_eq:
‹{x ∈ A. P x ∨ Q x} = {x ∈ A. P x} ∪ {x ∈ A. Q x}›
by auto
lemma zip_cong:
‹(⋀i. i < min (length xs) (length ys) ⟹ (xs ! i, ys ! i) = (xs' ! i, ys' ! i)) ⟹
length xs = length xs' ⟹ length ys = length ys' ⟹ zip xs ys = zip xs' ys'›
proof (induction xs arbitrary: xs' ys' ys)
case Nil
then show ?case by auto
next
case (Cons x xs xs' ys' ys) note IH = this(1) and eq = this(2) and p = this(3-)
thm IH
have ‹zip xs (tl ys) = zip (tl xs') (tl ys')› for i
apply (rule IH)
subgoal for i
using p eq[of ‹Suc i›] by (auto simp: nth_tl)
subgoal using p by auto
subgoal using p by auto
done
moreover have ‹hd xs' = x› ‹hd ys = hd ys'› if ‹ys ≠ []›
using eq[of 0] that p[symmetric] apply (auto simp: hd_conv_nth)
apply (subst hd_conv_nth)
apply auto
apply (subst hd_conv_nth)
apply auto
done
ultimately show ?case
using p by (cases xs'; cases ys'; cases ys)
auto
qed
lemma zip_cong2:
‹(⋀i. i < min (length xs) (length ys) ⟹ (xs ! i, ys ! i) = (xs' ! i, ys' ! i)) ⟹
length xs = length xs' ⟹ length ys ≤ length ys' ⟹ length ys ≥ length xs ⟹
zip xs ys = zip xs' ys'›
proof (induction xs arbitrary: xs' ys' ys)
case Nil
then show ?case by auto
next
case (Cons x xs xs' ys' ys) note IH = this(1) and eq = this(2) and p = this(3-)
have ‹zip xs (tl ys) = zip (tl xs') (tl ys')› for i
apply (rule IH)
subgoal for i
using p eq[of ‹Suc i›] by (auto simp: nth_tl)
subgoal using p by auto
subgoal using p by auto
subgoal using p by auto
done
moreover have ‹hd xs' = x› ‹hd ys = hd ys'› if ‹ys ≠ []›
using eq[of 0] that p apply (auto simp: hd_conv_nth)
apply (subst hd_conv_nth)
apply auto
apply (subst hd_conv_nth)
apply auto
done
ultimately show ?case
using p by (cases xs'; cases ys'; cases ys)
auto
qed
subsection ‹List Updates›
lemma tl_update_swap:
‹i ≥ 1 ⟹ tl (N[i := C]) = (tl N)[i-1 := C]›
by (auto simp: drop_Suc[of 0, symmetric, simplified] drop_update_swap)
lemma tl_update_0[simp]: ‹tl (N[0 := x]) = tl N›
by (cases N) auto
declare nth_list_update[simp]
text ‹
This a version of @{thm nth_list_update} with a different condition (\<^term>‹j›
instead of \<^term>‹i›). This is more useful in some cases.
›
lemma nth_list_update_le'[simp]:
"j < length xs ⟹ (xs[i:=x])!j = (if i = j then x else xs!j)"
by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
subsection ‹Take and drop›
lemma take_2_if:
‹take 2 C = (if C = [] then [] else if length C = 1 then [hd C] else [C!0, C!1])›
by (cases C; cases ‹tl C›) auto
lemma in_set_take_conv_nth:
‹x ∈ set (take n xs) ⟷ (∃m<min n (length xs). xs ! m = x)›
by (metis in_set_conv_nth length_take min.commute min.strict_boundedE nth_take)
lemma in_set_dropI:
‹m < length xs ⟹ m ≥ n ⟹ xs ! m ∈ set (drop n xs)›
unfolding in_set_conv_nth
by (rule exI[of _ ‹m - n›]) auto
lemma in_set_drop_conv_nth:
‹x ∈ set (drop n xs) ⟷ (∃m ≥ n. m < length xs ∧ xs ! m = x)›
apply (rule iffI)
subgoal
apply (subst (asm) in_set_conv_nth)
apply clarsimp
apply (rule_tac x = ‹n+i› in exI)
apply (auto)
done
subgoal
by (auto intro: in_set_dropI)
done
text ‹Taken from 🗏‹~~/src/HOL/Word/Word.thy››
lemma atd_lem: ‹take n xs = t ⟹ drop n xs = d ⟹ xs = t @ d›
by (auto intro: append_take_drop_id [symmetric])
lemma drop_take_drop_drop:
‹j ≥ i ⟹ drop i xs = take (j - i) (drop i xs) @ drop j xs›
apply (induction ‹j - i› arbitrary: j i)
subgoal by auto
subgoal by (auto simp add: atd_lem)
done
lemma in_set_conv_iff:
‹x ∈ set (take n xs) ⟷ (∃i < n. i < length xs ∧ xs ! i = x)›
apply (induction n)
subgoal by auto
subgoal for n
apply (cases ‹Suc n < length xs›)
subgoal by (auto simp: take_Suc_conv_app_nth less_Suc_eq dest: in_set_takeD)
subgoal
apply (cases ‹n < length xs›)
subgoal
apply (auto simp: in_set_conv_nth)
by (rule_tac x=i in exI; auto; fail)+
subgoal
apply (auto simp: take_Suc_conv_app_nth dest: in_set_takeD)
by (rule_tac x=i in exI; auto; fail)+
done
done
done
lemma distinct_in_set_take_iff:
‹distinct D ⟹ b < length D ⟹ D ! b ∈ set (take a D) ⟷ b < a›
apply (induction a arbitrary: b)
subgoal by simp
subgoal for a
by (cases ‹Suc a < length D›)
(auto simp: take_Suc_conv_app_nth nth_eq_iff_index_eq)
done
lemma in_set_distinct_take_drop_iff:
assumes
‹distinct D› and
‹b < length D›
shows ‹D ! b ∈ set (take (a - init) (drop init D)) ⟷ (init ≤ b ∧ b < a)›
using assms apply (auto 5 5 simp: distinct_in_set_take_iff in_set_conv_iff
nth_eq_iff_index_eq dest: in_set_takeD)
by (metis add_diff_cancel_left' diff_less_mono le_iff_add)
subsection ‹Replicate›
lemma list_eq_replicate_iff_nempty:
‹n > 0 ⟹ xs = replicate n x ⟷ n = length xs ∧ set xs = {x}›
by (metis length_replicate neq0_conv replicate_length_same set_replicate singletonD)
lemma list_eq_replicate_iff:
‹xs = replicate n x ⟷ (n = 0 ∧ xs = []) ∨ (n = length xs ∧ set xs = {x})›
by (cases n) (auto simp: list_eq_replicate_iff_nempty simp del: replicate.simps)
subsection ‹List intervals (@{term upt})›
text ‹
The simplification rules are not very handy, because theorem @{thm [source] upt.simps(2)}
(i.e.\ @{thm upt.simps(2)}) leads to a case distinction, that we usually do not want if the
condition is not already in the context.
›
lemma upt_Suc_le_append: ‹¬i ≤ j ⟹ [i..<Suc j] = []›
by auto
lemmas upt_simps[simp] = upt_Suc_append upt_Suc_le_append
declare upt.simps(2)[simp del]
text ‹The counterpart for this lemma when @{term ‹i > n-m›} is theorem @{thm [source] take_all}. It
is close to theorem @{thm take_upt}, but seems more general.›
lemma take_upt_bound_minus[simp]:
assumes ‹i ≤ n - m›
shows ‹take i [m..<n] = [m ..<m+i]›
using assms by (induction i) auto
lemma append_cons_eq_upt:
assumes ‹A @ B = [m..<n]›
shows ‹A = [m ..<m+length A]› and ‹B = [m + length A..<n]›
proof -
have ‹take (length A) (A @ B) = A› by auto
moreover {
have ‹length A ≤ n - m› using assms linear calculation by fastforce
then have ‹take (length A) [m..<n] = [m ..<m+length A]› by auto }
ultimately show ‹A = [m ..<m+length A]› using assms by auto
show ‹B = [m + length A..<n]› using assms by (metis append_eq_conv_conj drop_upt)
qed
text ‹The converse of theorem @{thm [source] append_cons_eq_upt} does not hold, for example if @
{term ‹B:: nat list›} is empty and @{term ‹A :: nat list›} is @{term ‹[0]›}:›
lemma ‹A @ B = [m..< n] ⟷ A = [m ..<m+length A] ∧ B = [m + length A..<n]›
oops
text ‹A more restrictive version holds:›
lemma ‹B ≠ [] ⟹ A @ B = [m..< n] ⟷ A = [m ..<m+length A] ∧ B = [m + length A..<n]›
(is ‹?P ⟹ ?A = ?B›)
proof
assume ?A then show ?B by (auto simp add: append_cons_eq_upt)
next
assume ?P and ?B
then show ?A using append_eq_conv_conj by fastforce
qed
lemma append_cons_eq_upt_length_i:
assumes ‹A @ i # B = [m..<n]›
shows ‹A = [m ..<i]›
proof -
have ‹A = [m ..< m + length A]› using assms append_cons_eq_upt by auto
have ‹(A @ i # B) ! (length A) = i› by auto
moreover have ‹n - m = length (A @ i # B)›
using assms length_upt by presburger
then have ‹[m..<n] ! (length A) = m + length A› by simp
ultimately have ‹i = m + length A› using assms by auto
then show ?thesis using ‹A = [m ..< m + length A]› by auto
qed
lemma append_cons_eq_upt_length:
assumes ‹A @ i # B = [m..<n]›
shows ‹length A = i - m›
using assms
proof (induction A arbitrary: m)
case Nil
then show ?case by (metis append_Nil diff_is_0_eq list.size(3) order_refl upt_eq_Cons_conv)
next
case (Cons a A)
then have A: ‹A @ i # B = [m + 1..<n]› by (metis append_Cons upt_eq_Cons_conv)
then have ‹m < i› by (metis Cons.prems append_cons_eq_upt_length_i upt_eq_Cons_conv)
with Cons.IH[OF A] show ?case by auto
qed
lemma append_cons_eq_upt_length_i_end:
assumes ‹A @ i # B = [m..<n]›
shows ‹B = [Suc i ..<n]›
proof -
have ‹B = [Suc m + length A..<n]› using assms append_cons_eq_upt[of ‹A @ [i]› B m n] by auto
have ‹(A @ i # B) ! (length A) = i› by auto
moreover have ‹n - m = length (A @ i # B)›
using assms length_upt by auto
then have ‹[m..<n]! (length A) = m + length A› by simp
ultimately have ‹i = m + length A› using assms by auto
then show ?thesis using ‹B = [Suc m + length A..<n]› by auto
qed
lemma Max_n_upt: ‹Max (insert 0 {Suc 0..<n}) = n - Suc 0›
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n) note IH = this
have i: ‹insert 0 {Suc 0..<Suc n} = insert 0 {Suc 0..< n} ∪ {n}› by auto
show ?case using IH unfolding i by auto
qed
lemma upt_decomp_lt:
assumes H: ‹xs @ i # ys @ j # zs = [m ..< n]›
shows ‹i < j›
proof -
have xs: ‹xs = [m ..< i]› and ys: ‹ys = [Suc i ..< j]› and zs: ‹zs = [Suc j ..< n]›
using H by (auto dest: append_cons_eq_upt_length_i append_cons_eq_upt_length_i_end)
show ?thesis
by (metis append_cons_eq_upt_length_i_end assms lessI less_trans self_append_conv2
upt_eq_Cons_conv upt_rec ys)
qed
lemma nths_upt_upto_Suc: ‹aa < length xs ⟹ nths xs {0..<Suc aa} = nths xs {0..<aa} @ [xs ! aa]›
by (simp add: atLeast0LessThan take_Suc_conv_app_nth)
text ‹The following two lemmas are useful as simp rules for case-distinction. The case
@{term ‹length l = 0›} is already simplified by default.›
lemma length_list_Suc_0:
‹length W = Suc 0 ⟷ (∃L. W = [L])›
apply (cases W)
apply (simp; fail)
apply (rename_tac a W', case_tac W')
apply auto
done
lemma length_list_2: ‹length S = 2 ⟷ (∃a b. S = [a, b])›
apply (cases S)
apply (simp; fail)
apply (rename_tac a S')
apply (case_tac S')
by simp_all
lemma finite_bounded_list:
fixes b :: nat
shows ‹finite {xs. length xs < s ∧ (∀i< length xs. xs ! i < b)}› (is ‹finite (?S s)›)
proof -
have H: ‹finite {xs. set xs ⊆ {0..<b} ∧ length xs ≤ s}›
by (rule finite_lists_length_le[of ‹{0..<b}› ‹s›]) auto
show ?thesis
by (rule finite_subset[OF _ H]) (auto simp: in_set_conv_nth)
qed
lemma last_in_set_dropWhile:
assumes ‹∃L ∈ set (xs @ [x]). ¬P L›
shows ‹x ∈ set (dropWhile P (xs @ [x]))›
using assms by (induction xs) auto
lemma mset_drop_upto: ‹mset (drop a N) = {#N!i. i ∈# mset_set {a..<length N}#}›
proof (induction N arbitrary: a)
case Nil
then show ?case by simp
next
case (Cons c N)
have upt: ‹{0..<Suc (length N)} = insert 0 {1..<Suc (length N)}›
by auto
then have H: ‹mset_set {0..<Suc (length N)} = add_mset 0 (mset_set {1..<Suc (length N)})›
unfolding upt by auto
have mset_case_Suc: ‹{#case x of 0 ⇒ c | Suc x ⇒ N ! x . x ∈# mset_set {Suc a..<Suc b}#} =
{#N ! (x-1) . x ∈# mset_set {Suc a..<Suc b}#}› for a b
by (rule image_mset_cong) (auto split: nat.splits)
have Suc_Suc: ‹{Suc a..<Suc b} = Suc ` {a..<b}› for a b
by auto
then have mset_set_Suc_Suc: ‹mset_set {Suc a..<Suc b} = {#Suc n. n ∈# mset_set {a..<b}#}› for a b
unfolding Suc_Suc by (subst image_mset_mset_set[symmetric]) auto
have *: ‹{#N ! (x-Suc 0) . x ∈# mset_set {Suc a..<Suc b}#} = {#N ! x . x ∈# mset_set {a..<b}#}›
for a b
by (auto simp add: mset_set_Suc_Suc)
show ?case
apply (cases a)
using Cons[of 0] Cons by (auto simp: nth_Cons drop_Cons H mset_case_Suc *)
qed
lemma last_list_update_to_last:
‹last (xs[x := last xs]) = last xs›
by (metis last_list_update list_update.simps(1))
lemma take_map_nth_alt_def: ‹take n xs = map ((!) xs) [0..<min n (length xs)]›
proof (induction xs rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc x xs) note IH = this
show ?case
proof (cases ‹n < length (xs @ [x])›)
case True
then show ?thesis
using IH by (auto simp: min_def nth_append)
next
case False
have [simp]:
‹map (λa. if a < length xs then xs ! a else [x] ! (a - length xs)) [0..<length xs] =
map (λa. xs ! a) [0..<length xs]› for xs and x :: 'b
by (rule map_cong) auto
show ?thesis
using IH False by (auto simp: nth_append min_def)
qed
qed
subsection ‹Lexicographic Ordering›
lemma lexn_Suc:
‹(x # xs, y # ys) ∈ lexn r (Suc n) ⟷
(length xs = n ∧ length ys = n) ∧ ((x, y) ∈ r ∨ (x = y ∧ (xs, ys) ∈ lexn r n))›
by (auto simp: map_prod_def image_iff lex_prod_def)
lemma lexn_n:
‹n > 0 ⟹ (x # xs, y # ys) ∈ lexn r n ⟷
(length xs = n-1 ∧ length ys = n-1) ∧ ((x, y) ∈ r ∨ (x = y ∧ (xs, ys) ∈ lexn r (n - 1)))›
apply (cases n)
apply simp
by (auto simp: map_prod_def image_iff lex_prod_def)
text ‹
There is some subtle point in the previous theorem explaining ∗‹why› it is useful. The term
@{term ‹1::nat›} is converted to @{term ‹Suc 0::nat›}, but @{term ‹2::nat›} is not, meaning
that @{term ‹1::nat›} is automatically simplified by default allowing the use of the default
simplification rule @{thm [source] lexn.simps}. However, for 2 one additional simplification rule
is required (see the proof of the theorem above).
›
lemma lexn2_conv:
‹([a, b], [c, d]) ∈ lexn r 2 ⟷ (a, c) ∈ r ∨ (a = c ∧ (b, d) ∈r)›
by (auto simp: lexn_n simp del: lexn.simps(2))
lemma lexn3_conv:
‹([a, b, c], [a', b', c']) ∈ lexn r 3 ⟷
(a, a') ∈ r ∨ (a = a' ∧ (b, b') ∈ r) ∨ (a = a' ∧ b = b' ∧ (c, c') ∈ r)›
by (auto simp: lexn_n simp del: lexn.simps(2))
lemma prepend_same_lexn:
assumes irrefl: ‹irrefl R›
shows ‹(A @ B, A @ C) ∈ lexn R n ⟷ (B, C) ∈ lexn R (n - length A)› (is ‹?A ⟷ ?B›)
proof
assume ?A
then obtain xys x xs y ys where
len_B: ‹length B = n - length A› and
len_C: ‹length C = n - length A› and
AB: ‹A @ B = xys @ x # xs› and
AC: ‹A @ C = xys @ y # ys› and
xy: ‹(x, y) ∈ R›
by (auto simp: lexn_conv)
have x_neq_y: ‹x ≠ y›
using xy irrefl by (auto simp add: irrefl_def)
then have ‹B = drop (length A) xys @ x # xs›
using arg_cong[OF AB, of ‹drop (length A)›]
apply (cases ‹length A - length xys›)
apply (auto; fail)
by (metis AB AC nth_append nth_append_length zero_less_Suc zero_less_diff)
moreover have ‹C = drop (length A) xys @ y # ys›
using arg_cong[OF AC, of ‹drop (length A)›] x_neq_y
apply (cases ‹length A - length xys›)
apply (auto; fail)
by (metis AB AC nth_append nth_append_length zero_less_Suc zero_less_diff)
ultimately show ?B
using len_B[symmetric] len_C[symmetric] xy
by (auto simp: lexn_conv)
next
assume ?B
then obtain xys x xs y ys where
len_B: ‹length B = n - length A› and
len_C: ‹length C = n - length A› and
AB: ‹B = xys @ x # xs› and
AC: ‹C = xys @ y # ys› and
xy: ‹(x, y) ∈ R›
by (auto simp: lexn_conv)
define Axys where ‹Axys = A @ xys›
have ‹A @ B = Axys @ x # xs›
using AB Axys_def by auto
moreover have ‹A @ C = Axys @ y # ys›
using AC Axys_def by auto
moreover have ‹Suc (length Axys + length xs) = n› and
‹length ys = length xs›
using len_B len_C AB AC Axys_def by auto
ultimately show ?A
using len_B[symmetric] len_C[symmetric] xy
by (auto simp: lexn_conv)
qed
lemma append_same_lexn:
assumes irrefl: ‹irrefl R›
shows ‹(B @ A , C @ A) ∈ lexn R n ⟷ (B, C) ∈ lexn R (n - length A)› (is ‹?A ⟷ ?B›)
proof
assume ?A
then obtain xys x xs y ys where
len_B: ‹n = length B + length A› and
len_C: ‹n = length C + length A› and
AB: ‹B @ A = xys @ x # xs› and
AC: ‹C @ A = xys @ y # ys› and
xy: ‹(x, y) ∈ R›
by (auto simp: lexn_conv)
have x_neq_y: ‹x ≠ y›
using xy irrefl by (auto simp add: irrefl_def)
have len_C_B: ‹length C = length B›
using len_B len_C by simp
have len_B_xys: ‹length B > length xys›
apply (rule ccontr)
using arg_cong[OF AB, of ‹take (length B)›] arg_cong[OF AB, of ‹drop (length B)›]
arg_cong[OF AC, of ‹drop (length C)›] x_neq_y len_C_B
by auto
then have B: ‹B = xys @ x # take (length B - Suc (length xys)) xs›
using arg_cong[OF AB, of ‹take (length B)›]
by (cases ‹length B - length xys›) simp_all
have C: ‹C = xys @ y # take (length C - Suc (length xys)) ys›
using arg_cong[OF AC, of ‹take (length C)›] x_neq_y len_B_xys unfolding len_C_B[symmetric]
by (cases ‹length C - length xys›) auto
show ?B
using len_B[symmetric] len_C[symmetric] xy B C
by (auto simp: lexn_conv)
next
assume ?B
then obtain xys x xs y ys where
len_B: ‹length B = n - length A› and
len_C: ‹length C = n - length A› and
AB: ‹B = xys @ x # xs› and
AC: ‹C = xys @ y # ys› and
xy: ‹(x, y) ∈ R›
by (auto simp: lexn_conv)
define Ays Axs where ‹Ays = ys @ A› and‹Axs = xs @ A›
have ‹B @ A = xys @ x # Axs›
using AB Axs_def by auto
moreover have ‹C @ A = xys @ y # Ays›
using AC Ays_def by auto
moreover have ‹Suc (length xys + length Axs) = n› and
‹length Ays = length Axs›
using len_B len_C AB AC Axs_def Ays_def by auto
ultimately show ?A
using len_B[symmetric] len_C[symmetric] xy
by (auto simp: lexn_conv)
qed
lemma irrefl_less_than [simp]: ‹irrefl less_than›
by (auto simp: irrefl_def)
subsection ‹Remove›
subsubsection ‹More lemmas about remove›
lemma distinct_remove1_last_butlast:
‹distinct xs ⟹ xs ≠ [] ⟹ remove1 (last xs) xs = butlast xs›
by (metis append_Nil2 append_butlast_last_id distinct_butlast not_distinct_conv_prefix
remove1.simps(2) remove1_append)
lemma remove1_Nil_iff:
‹remove1 x xs = [] ⟷ xs = [] ∨ xs = [x]›
by (cases xs) auto
lemma removeAll_upt:
‹removeAll k [a..<b] = (if k ≥ a ∧ k < b then [a..<k] @ [Suc k..<b] else [a..<b])›
by (induction b) auto
lemma remove1_upt:
‹remove1 k [a..<b] = (if k ≥ a ∧ k < b then [a..<k] @ [Suc k..<b] else [a..<b])›
by (subst distinct_remove1_removeAll) (auto simp: removeAll_upt)
lemma sorted_removeAll: ‹sorted C ⟹ sorted (removeAll k C)›
by (metis map_ident removeAll_filter_not_eq sorted_filter)
lemma distinct_remove1_rev: ‹distinct xs ⟹ remove1 x (rev xs) = rev (remove1 x xs)›
using split_list[of x xs]
by (cases ‹x ∈ set xs›) (auto simp: remove1_append remove1_idem)
subsubsection ‹Remove under condition›
text ‹This function removes the first element such that the condition @{term f} holds. It
generalises @{term List.remove1}.›
fun remove1_cond where
‹remove1_cond f [] = []› |
‹remove1_cond f (C' # L) = (if f C' then L else C' # remove1_cond f L)›
lemma ‹remove1 x xs = remove1_cond ((=) x) xs›
by (induction xs) auto
lemma mset_map_mset_remove1_cond:
‹mset (map mset (remove1_cond (λL. mset L = mset a) C)) =
remove1_mset (mset a) (mset (map mset C))›
by (induction C) auto
text ‹We can also generalise @{term List.removeAll}, which is close to @{term List.filter}:›
fun removeAll_cond :: ‹('a ⇒ bool) ⇒ 'a list ⇒ 'a list› where
‹removeAll_cond f [] = []› |
‹removeAll_cond f (C' # L) = (if f C' then removeAll_cond f L else C' # removeAll_cond f L)›
lemma removeAll_removeAll_cond: ‹removeAll x xs = removeAll_cond ((=) x) xs›
by (induction xs) auto
lemma removeAll_cond_filter: ‹removeAll_cond P xs = filter (λx. ¬P x) xs›
by (induction xs) auto
lemma mset_map_mset_removeAll_cond:
‹mset (map mset (removeAll_cond (λb. mset b = mset a) C))
= removeAll_mset (mset a) (mset (map mset C))›
by (induction C) auto
lemma count_mset_count_list:
‹count (mset xs) x = count_list xs x›
by (induction xs) auto
lemma length_removeAll_count_list:
‹length (removeAll x xs) = length xs - count_list xs x›
proof -
have ‹length (removeAll x xs) = size (removeAll_mset x (mset xs))›
by auto
also have ‹… = size (mset xs) - count (mset xs) x›
by (metis count_le_replicate_mset_subset_eq le_refl size_Diff_submset size_replicate_mset)
also have ‹ … = length xs - count_list xs x›
unfolding count_mset_count_list by simp
finally show ?thesis .
qed
lemma removeAll_notin: ‹a ∉# A ⟹ removeAll_mset a A = A›
using count_inI by force
subsubsection ‹Filter›
lemma distinct_filter_eq_if:
‹distinct C ⟹ length (filter ((=) L) C) = (if L ∈ set C then 1 else 0)›
by (induction C) auto
lemma length_filter_update_true:
assumes ‹i < length xs› and ‹P (xs ! i)›
shows ‹length (filter P (xs[i := x])) = length (filter P xs) - (if P x then 0 else 1)›
apply (subst (5) append_take_drop_id[of i, symmetric])
using assms upd_conv_take_nth_drop[of i xs x] Cons_nth_drop_Suc[of i xs, symmetric]
unfolding filter_append length_append
by simp
lemma length_filter_update_false:
assumes ‹i < length xs› and ‹¬P (xs ! i)›
shows ‹length (filter P (xs[i := x])) = length (filter P xs) + (if P x then 1 else 0)›
apply (subst (5) append_take_drop_id[of i, symmetric])
using assms upd_conv_take_nth_drop[of i xs x] Cons_nth_drop_Suc[of i xs, symmetric]
unfolding filter_append length_append
by simp
lemma mset_set_mset_set_minus_id_iff:
assumes ‹finite A›
shows ‹mset_set A = mset_set (A - B) ⟷ (∀b ∈ B. b ∉ A)›
proof -
have f1: "mset_set A = mset_set (A - B) ⟷ A - B = A"
using assms by (metis (no_types) finite_Diff finite_set_mset_mset_set)
then show ?thesis
by blast
qed
lemma mset_set_eq_mset_set_more_conds:
‹finite {x. P x} ⟹ mset_set {x. P x} = mset_set {x. Q x ∧ P x} ⟷ (∀x. P x ⟶ Q x)›
(is ‹?F ⟹ ?A ⟷ ?B›)
proof -
assume ?F
then have ‹?A ⟷ (∀x ∈ {x. P x}. x ∈ {x. Q x ∧ P x})›
by (subst mset_set_eq_iff) auto
also have ‹… ⟷ (∀x. P x ⟶ Q x)›
by blast
finally show ?thesis .
qed
lemma count_list_filter: ‹count_list xs x = length (filter ((=) x) xs)›
by (induction xs) auto
lemma sum_length_filter_compl': ‹length [x←xs . ¬ P x] + length (filter P xs) = length xs›
using sum_length_filter_compl[of P xs] by auto
subsection ‹Sorting›
text ‹See @{thm sorted_distinct_set_unique}.›
lemma sorted_mset_unique:
fixes xs :: ‹'a :: linorder list›
shows ‹sorted xs ⟹ sorted ys ⟹ mset xs = mset ys ⟹ xs = ys›
using properties_for_sort by auto
lemma insort_upt: ‹insort k [a..<b] =
(if k < a then k # [a..<b]
else if k < b then [a..<k] @ k # [k ..<b]
else [a..<b] @ [k])›
proof -
have H: ‹k < Suc b ⟹ ¬ k < a ⟹ {a..<b} = {a..<k} ∪ {k..<b}› for a b :: nat
by (simp add: ivl_disj_un_two(3))
show ?thesis
apply (induction b)
apply (simp; fail)
apply (case_tac ‹¬k < a ∧ k < Suc b›)
apply (rule sorted_mset_unique)
apply ((auto simp add: sorted_append sorted_insort ac_simps mset_set_Union
dest!: H; fail)+)[2]
apply (auto simp: insort_is_Cons sorted_insort_is_snoc sorted_append mset_set_Union
ac_simps dest: H; fail)+
done
qed
lemma removeAll_insert_removeAll: ‹removeAll k (insort k xs) = removeAll k xs›
by (simp add: filter_insort_triv removeAll_filter_not_eq)
lemma filter_sorted: ‹sorted xs ⟹ sorted (filter P xs)›
by (metis list.map_ident sorted_filter)
lemma removeAll_insort:
‹sorted xs ⟹ k ≠ k' ⟹ removeAll k' (insort k xs) = insort k (removeAll k' xs)›
by (simp add: filter_insort removeAll_filter_not_eq)
subsection ‹Distinct Multisets›
lemma distinct_mset_remdups_mset_id: ‹distinct_mset C ⟹ remdups_mset C = C›
by (induction C) auto
lemma notin_add_mset_remdups_mset:
‹a ∉# A ⟹ add_mset a (remdups_mset A) = remdups_mset (add_mset a A)›
by auto
lemma distinct_mset_image_mset:
‹distinct_mset (image_mset f (mset xs)) ⟷ distinct (map f xs)›
apply (subst mset_map[symmetric])
apply (subst distinct_mset_mset_distinct)
..
lemma distinct_image_mset_not_equal:
assumes
LL': ‹L ≠ L'› and
dist: ‹distinct_mset (image_mset f M)› and
L: ‹L ∈# M› and
L': ‹L' ∈# M› and
fLL'[simp]: ‹f L = f L'›
shows ‹False›
proof -
obtain M1 where M1: ‹M = add_mset L M1›
using multi_member_split[OF L] by blast
obtain M2 where M2: ‹M1 = add_mset L' M2›
using multi_member_split[of L' M1] LL' L' unfolding M1 by (auto simp: add_mset_eq_add_mset)
show False
using dist unfolding M1 M2 by auto
qed
subsection ‹Set of Distinct Multisets›
definition distinct_mset_set :: ‹'a multiset set ⇒ bool› where
‹distinct_mset_set Σ ⟷ (∀S ∈ Σ. distinct_mset S)›
lemma distinct_mset_set_empty[simp]: ‹distinct_mset_set {}›
unfolding distinct_mset_set_def by auto
lemma distinct_mset_set_singleton[iff]: ‹distinct_mset_set {A} ⟷ distinct_mset A›
unfolding distinct_mset_set_def by auto
lemma distinct_mset_set_insert[iff]:
‹distinct_mset_set (insert S Σ) ⟷ (distinct_mset S ∧ distinct_mset_set Σ)›
unfolding distinct_mset_set_def by auto
lemma distinct_mset_set_union[iff]:
‹distinct_mset_set (Σ ∪ Σ') ⟷ (distinct_mset_set Σ ∧ distinct_mset_set Σ')›
unfolding distinct_mset_set_def by auto
lemma in_distinct_mset_set_distinct_mset:
‹a ∈ Σ ⟹ distinct_mset_set Σ ⟹ distinct_mset a›
unfolding distinct_mset_set_def by auto
lemma distinct_mset_remdups_mset[simp]: ‹distinct_mset (remdups_mset S)›
using count_remdups_mset_eq_1 unfolding distinct_mset_def by metis
lemma distinct_mset_mset_set: ‹distinct_mset (mset_set A)›
unfolding distinct_mset_def count_mset_set_if by (auto simp: not_in_iff)
lemma distinct_mset_filter_mset_set[simp]: ‹distinct_mset {#a ∈# mset_set A. P a#}›
by (simp add: distinct_mset_filter distinct_mset_mset_set)
lemma distinct_mset_set_distinct: ‹distinct_mset_set (mset ` set Cs) ⟷ (∀c∈ set Cs. distinct c)›
unfolding distinct_mset_set_def by auto
subsection ‹Sublists›
lemma nths_single_if: ‹nths l {n} = (if n < length l then [l!n] else [])›
proof -
have [simp]: ‹0 < n ⟹ {j. Suc j = n} = {n-1}› for n
by auto
show ?thesis
apply (induction l arbitrary: n)
subgoal by (auto simp: nths_def)
subgoal by (auto simp: nths_Cons)
done
qed
lemma atLeastLessThan_Collect: ‹{a..<b} = {j. j ≥ a ∧ j < b}›
by auto
lemma mset_nths_subset_mset: ‹mset (nths xs A) ⊆# mset xs›
apply (induction xs arbitrary: A)
subgoal by auto
subgoal for a xs A
using subset_mset.add_increasing2[of ‹add_mset _ {#}› ‹mset (nths xs {j. Suc j ∈ A})›
‹mset xs›]
by (auto simp: nths_Cons)
done
lemma nths_id_iff:
‹nths xs A = xs ⟷ {0..<length xs} ⊆ A ›
proof -
have ‹{j. Suc j ∈ A} = (λj. j-1) ` (A - {0})› for A
using DiffI by (fastforce simp: image_iff)
have 1: ‹{0..<b} ⊆ {j. Suc j ∈ A} ⟷ (∀x. x-1 < b ⟶ x ≠ 0 ⟶ x ∈ A)›
for A :: ‹nat set› and b :: nat
by auto
have [simp]: ‹{0..<b} ⊆ {j. Suc j ∈ A} ⟷ (∀x. x-1 < b ⟶ x ∈ A)›
if ‹0 ∈ A› for A :: ‹nat set› and b :: nat
using that unfolding 1 by auto
have [simp]: ‹nths xs {j. Suc j ∈ A} = a # xs ⟷ False›
for a :: 'a and xs :: ‹'a list› and A :: ‹nat set›
using mset_nths_subset_mset[of xs ‹{j. Suc j ∈ A}›] by auto
show ?thesis
apply (induction xs arbitrary: A)
subgoal by auto
subgoal
by (auto 5 5 simp: nths_Cons) fastforce
done
qed
lemma nts_upt_length[simp]: ‹nths xs {0..<length xs} = xs›
by (auto simp: nths_id_iff)
lemma nths_shift_lemma':
‹map fst [p←zip xs [i..<i + n]. snd p + b ∈ A] = map fst [p←zip xs [0..<n]. snd p + b + i ∈ A]›
proof (induct xs arbitrary: i n b)
case Nil
then show ?case by simp
next
case (Cons a xs)
have 1: ‹map fst [p←zip (a # xs) (i # [Suc i..<i + n]). snd p + b ∈ A] =
(if i + b ∈ A then a#map fst [p←zip xs [Suc i..<i + n]. snd p + b ∈ A]
else map fst [p←zip xs [Suc i..<i + n]. snd p + b ∈A])›
by simp
have 2: ‹map fst [p←zip (a # xs) [0..<n] . snd p + b + i ∈ A] =
(if i + b ∈ A then a # map fst [p←zip xs [1..<n]. snd p + b + i ∈ A]
else map fst [p←zip (xs) [1..<n] . snd p + b + i ∈ A])›
if ‹n > 0›
by (subst upt_conv_Cons) (use that in ‹auto simp: ac_simps›)
show ?case
proof (cases n)
case 0
then show ?thesis by simp
next
case n: (Suc m)
then have i_n_m: ‹i + n = Suc i + m›
by auto
have 3: ‹map fst [p←zip xs [Suc i..<i+n] . snd p + b ∈ A] =
map fst [p←zip xs [0..<m] . snd p + b + Suc i ∈ A]›
using Cons[of b ‹Suc i› m] unfolding i_n_m .
have 4: ‹map fst [p←zip xs [1..<n] . snd p + b + i ∈ A] =
map fst [p←zip xs [0..<m] . Suc (snd p + b + i) ∈ A]›
using Cons[of ‹b+i› 1 m] unfolding n Suc_eq_plus1_left add.commute[of 1]
by (simp_all add: ac_simps)
show ?thesis
apply (subst upt_conv_Cons)
using n apply (simp; fail)
apply (subst 1)
apply (subst 2)
using n apply (simp; fail)
apply (subst 3)
apply (subst 3)
apply (subst 4)
apply (subst 4)
by force
qed
qed
lemma nths_Cons_upt_Suc: ‹nths (a # xs) {0..<Suc n} = a # nths xs {0..<n}›
unfolding nths_def
apply (subst upt_conv_Cons)
apply simp
using nths_shift_lemma'[of 0 ‹{0..<Suc n}› ‹xs› 1 ‹length xs›]
by (simp_all add: ac_simps)
lemma nths_empty_iff: ‹nths xs A = [] ⟷ {..<length xs} ∩ A = {}›
proof (induction xs arbitrary: A)
case Nil
then show ?case by auto
next
case (Cons a xs) note IH = this(1)
have ‹(∀x<length xs. x ≠ 0 ⟶ x ∉ A)›
if a1: ‹{..<length xs} ∩ {j. Suc j ∈ A} = {}›
proof (intro allI impI)
fix nn
assume nn: ‹nn < length xs› ‹nn ≠ 0›
moreover have "∀n. Suc n ∉ A ∨ ¬ n < length xs"
using a1 by blast
then show "nn ∉ A"
using nn
by (metis (no_types) lessI less_trans list_decode.cases)
qed
show ?case
proof (cases ‹0 ∈ A›)
case True
then show ?thesis by (subst nths_Cons) auto
next
case False
then show ?thesis
by (subst nths_Cons) (use less_Suc_eq_0_disj IH in auto)
qed
qed
lemma nths_upt_Suc:
assumes ‹i < length xs›
shows ‹nths xs {i..<length xs} = xs!i # nths xs {Suc i..<length xs}›
proof -
have upt: ‹{i..<k} = {j. i ≤ j ∧ j < k}› for i k :: nat
by auto
show ?thesis
using assms
proof (induction xs arbitrary: i)
case Nil
then show ?case by simp
next
case (Cons a xs i) note IH = this(1) and i_le = this(2)
have [simp]: ‹i - Suc 0 ≤ j ⟷ i ≤ Suc j› if ‹i > 0› for j
using that by auto
show ?case
using IH[of ‹i-1›] i_le
by (auto simp add: nths_Cons upt)
qed
qed
lemma nths_upt_Suc':
assumes ‹i < b› and ‹b <= length xs›
shows ‹nths xs {i..<b} = xs!i # nths xs {Suc i..<b}›
proof -
have S1: ‹{j. i ≤ Suc j ∧ j < b - Suc 0} = {j. i ≤ Suc j ∧ Suc j < b}› for i b
by auto
have S2: ‹{j. i ≤ j ∧ j < b - Suc 0} = {j. i ≤ j ∧ Suc j < b}› for i b
by auto
have upt: ‹{i..<k} = {j. i ≤ j ∧ j < k}› for i k :: nat
by auto
show ?thesis
using assms
proof (induction xs arbitrary: i b)
case Nil
then show ?case by simp
next
case (Cons a xs i) note IH = this(1) and i_le = this(2,3)
have [simp]: ‹i - Suc 0 ≤ j ⟷ i ≤ Suc j› if ‹i > 0› for j
using that by auto
have ‹i - Suc 0 < b - Suc 0 ∨ (i = 0)›
using i_le by linarith
moreover have ‹b - Suc 0 ≤ length xs ∨ xs = []›
using i_le by auto
ultimately show ?case
using IH[of ‹i-1› ‹b-1›] i_le
apply (subst nths_Cons)
apply (subst nths_Cons)
by (auto simp: upt S1 S2)
qed
qed
lemma Ball_set_nths: ‹(∀L∈set (nths xs A). P L) ⟷ (∀i ∈ A ∩ {0..<length xs}. P (xs ! i)) ›
unfolding set_nths by fastforce
subsection ‹Product Case›
text ‹The splitting of tuples is done for sizes strictly less than 8. As we want to manipulate
tuples of size 8, here is some more setup for larger sizes.›
lemma prod_cases8 [cases type]:
obtains (fields) a b c d e f g h where "y = (a, b, c, d, e, f, g, h)"
by (cases y, cases ‹snd y›) auto
lemma prod_induct8 [case_names fields, induct type]:
"(⋀a b c d e f g h. P (a, b, c, d, e, f, g, h)) ⟹ P x"
by (cases x) blast
lemma prod_cases9 [cases type]:
obtains (fields) a b c d e f g h i where "y = (a, b, c, d, e, f, g, h, i)"
by (cases y, cases ‹snd y›) auto
lemma prod_induct9 [case_names fields, induct type]:
"(⋀a b c d e f g h i. P (a, b, c, d, e, f, g, h, i)) ⟹ P x"
by (cases x) blast
lemma prod_cases10 [cases type]:
obtains (fields) a b c d e f g h i j where "y = (a, b, c, d, e, f, g, h, i, j)"
by (cases y, cases ‹snd y›) auto
lemma prod_induct10 [case_names fields, induct type]:
"(⋀a b c d e f g h i j. P (a, b, c, d, e, f, g, h, i, j)) ⟹ P x"
by (cases x) blast
lemma prod_cases11 [cases type]:
obtains (fields) a b c d e f g h i j k where "y = (a, b, c, d, e, f, g, h, i, j, k)"
by (cases y, cases ‹snd y›) auto
lemma prod_induct11 [case_names fields, induct type]:
"(⋀a b c d e f g h i j k. P (a, b, c, d, e, f, g, h, i, j, k)) ⟹ P x"
by (cases x) blast
lemma prod_cases12 [cases type]:
obtains (fields) a b c d e f g h i j k l where "y = (a, b, c, d, e, f, g, h, i, j, k, l)"
by (cases y, cases ‹snd y›) auto
lemma prod_induct12 [case_names fields, induct type]:
"(⋀a b c d e f g h i j k l. P (a, b, c, d, e, f, g, h, i, j, k, l)) ⟹ P x"
by (cases x) blast
lemma prod_cases13 [cases type]:
obtains (fields) a b c d e f g h i j k l m where "y = (a, b, c, d, e, f, g, h, i, j, k, l, m)"
by (cases y, cases ‹snd y›) auto
lemma prod_induct13 [case_names fields, induct type]:
"(⋀a b c d e f g h i j k l m. P (a, b, c, d, e, f, g, h, i, j, k, l, m)) ⟹ P x"
by (cases x) blast
lemma prod_cases14 [cases type]:
obtains (fields) a b c d e f g h i j k l m n where "y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n)"
by (cases y, cases ‹snd y›) auto
lemma prod_induct14 [case_names fields, induct type]:
"(⋀a b c d e f g h i j k l m n. P (a, b, c, d, e, f, g, h, i, j, k, l, m, n)) ⟹ P x"
by (cases x) blast
lemma prod_cases15 [cases type]:
obtains (fields) a b c d e f g h i j k l m n p where
"y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p)"
by (cases y, cases ‹snd y›) auto
lemma prod_induct15 [case_names fields, induct type]:
"(⋀a b c d e f g h i j k l m n p. P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p)) ⟹ P x"
by (cases x) blast
lemma prod_cases16 [cases type]:
obtains (fields) a b c d e f g h i j k l m n p q where
"y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q)"
by (cases y, cases ‹snd y›) auto
lemma prod_induct16 [case_names fields, induct type]:
"(⋀a b c d e f g h i j k l m n p q. P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q)) ⟹ P x"
by (cases x) blast
lemma prod_cases17 [cases type]:
obtains (fields) a b c d e f g h i j k l m n p q r where
"y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r)"
by (cases y, cases ‹snd y›) auto
lemma prod_induct17 [case_names fields, induct type]:
"(⋀a b c d e f g h i j k l m n p q r. P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r)) ⟹ P x"
by (cases x) blast
lemma prod_cases18 [cases type]:
obtains (fields) a b c d e f g h i j k l m n p q r s where
"y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s)"
by (cases y, cases ‹snd y›) auto
lemma prod_induct18 [case_names fields, induct type]:
"(⋀a b c d e f g h i j k l m n p q r s. P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s)) ⟹ P x"
by (cases x) blast
lemma prod_cases19 [cases type]:
obtains (fields) a b c d e f g h i j k l m n p q r s t where
"y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t)"
by (cases y, cases ‹snd y›) auto
lemma prod_induct19 [case_names fields, induct type]:
"(⋀a b c d e f g h i j k l m n p q r s t.
P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t)) ⟹ P x"
by (cases x) blast
lemma prod_cases20 [cases type]:
obtains (fields) a b c d e f g h i j k l m n p q r s t u where
"y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t, u)"
by (cases y, cases ‹snd y›) auto
lemma prod_induct20 [case_names fields, induct type]:
"(⋀a b c d e f g h i j k l m n p q r s t u.
P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t, u)) ⟹ P x"
by (cases x) blast
lemma prod_cases21 [cases type]:
obtains (fields) a b c d e f g h i j k l m n p q r s t u v where
"y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t, u, v)"
by (cases y, cases ‹snd y›) auto
lemma prod_induct21 [case_names fields, induct type]:
"(⋀a b c d e f g h i j k l m n p q r s t u v.
P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t, u, v)) ⟹ P x"
by (cases x) (blast 43)
lemma prod_cases22 [cases type]:
obtains (fields) a b c d e f g h i j k l m n p q r s t u v w where
"y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t, u, v, w)"
by (cases y, cases ‹snd y›) auto
lemma prod_induct22 [case_names fields, induct type]:
"(⋀a b c d e f g h i j k l m n p q r s t u v w.
P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t, u, v, w)) ⟹ P x"
by (cases x) (blast 43)
lemma prod_cases23 [cases type]:
obtains (fields) a b c d e f g h i j k l m n p q r s t u v w x where
"y = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t, u, v, w, x)"
by (cases y, cases ‹snd y›) auto
lemma prod_induct23 [case_names fields, induct type]:
"(⋀a b c d e f g h i j k l m n p q r s t u v w y.
P (a, b, c, d, e, f, g, h, i, j, k, l, m, n, p, q, r, s, t, u, v, w, y)) ⟹ P x"
by (cases x) (blast 43)
subsection ‹More about @{term list_all2} and @{term map}›
text ‹
More properties on the relator \<^term>‹list_all2› and \<^term>‹map›. These theorems are
mostly used during the refinement and especially the lifting from a deterministic relator to
its list version.
›
lemma list_all2_op_eq_map_right_iff: ‹list_all2 (λL. (=) (f L)) a aa ⟷ aa = map f a ›
apply (induction a arbitrary: aa)
apply (auto; fail)
by (rename_tac aa, case_tac aa) (auto)
lemma list_all2_op_eq_map_right_iff': ‹list_all2 (λL L'. L' = f L) a aa ⟷ aa = map f a›
apply (induction a arbitrary: aa)
apply (auto; fail)
by (rename_tac aa, case_tac aa) auto
lemma list_all2_op_eq_map_left_iff: ‹list_all2 (λL' L. L' = (f L)) a aa ⟷ a = map f aa›
apply (induction a arbitrary: aa)
apply (auto; fail)
by (rename_tac aa, case_tac aa) (auto)
lemma list_all2_op_eq_map_map_right_iff:
‹list_all2 (list_all2 (λL. (=) (f L))) xs' x ⟷ x = map (map f) xs'› for x
apply (induction xs' arbitrary: x)
apply (auto; fail)
apply (case_tac x)
by (auto simp: list_all2_op_eq_map_right_iff)
lemma list_all2_op_eq_map_map_left_iff:
‹list_all2 (list_all2 (λL' L. L' = f L)) xs' x ⟷ xs' = map (map f) x›
apply (induction xs' arbitrary: x)
apply (auto; fail)
apply (rename_tac x, case_tac x)
by (auto simp: list_all2_op_eq_map_left_iff)
lemma list_all2_conj:
‹list_all2 (λx y. P x y ∧ Q x y) xs ys ⟷ list_all2 P xs ys ∧ list_all2 Q xs ys›
by (auto simp: list_all2_conv_all_nth)
lemma list_all2_replicate:
‹(bi, b) ∈ R' ⟹ list_all2 (λx x'. (x, x') ∈ R') (replicate n bi) (replicate n b)›
by (induction n) auto
subsection ‹Multisets›
text ‹We have a lit of lemmas about multisets. Some of them have already moved to
\<^theory>‹Nested_Multisets_Ordinals.Multiset_More›, but others are too specific (especially the
\<^term>‹distinct_mset› property, which roughly corresponds to finite sets).
›
notation image_mset (infixr "`#" 90)
lemma in_multiset_nempty: ‹L ∈# D ⟹ D ≠ {#}›
by auto
text ‹The definition and the correctness theorem are from the multiset theory
@{file ‹~~/src/HOL/Library/Multiset.thy›}, but a name is necessary to refer to them:›
definition union_mset_list where
‹union_mset_list xs ys ≡ case_prod append (fold (λx (ys, zs). (remove1 x ys, x # zs)) xs (ys, []))›
lemma union_mset_list:
‹mset xs ∪# mset ys = mset (union_mset_list xs ys)›
proof -
have ‹⋀zs. mset (case_prod append (fold (λx (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
(mset xs ∪# mset ys) + mset zs›
by (induct xs arbitrary: ys) (simp_all add: multiset_eq_iff)
then show ?thesis by (simp add: union_mset_list_def)
qed
lemma union_mset_list_Nil[simp]: ‹union_mset_list [] bi = bi›
by (auto simp: union_mset_list_def)
lemma size_le_Suc_0_iff: ‹size M ≤ Suc 0 ⟷ ((∃a b. M = {#a#}) ∨ M = {#})›
using size_1_singleton_mset by (auto simp: le_Suc_eq)
lemma size_2_iff: ‹size M = 2 ⟷ (∃a b. M = {#a, b#})›
by (metis One_nat_def Suc_1 Suc_pred empty_not_add_mset nonempty_has_size size_Diff_singleton
size_eq_Suc_imp_eq_union size_single union_single_eq_diff union_single_eq_member)
lemma subset_eq_mset_single_iff: ‹x2 ⊆# {#L#} ⟷ x2 = {#} ∨ x2 = {#L#}›
by (metis single_is_union subset_mset.add_diff_inverse subset_mset.eq_refl subset_mset.zero_le)
lemma mset_eq_size_2:
‹mset xs = {#a, b#} ⟷ xs = [a, b] ∨ xs = [b, a]›
by (cases xs) (auto simp: add_mset_eq_add_mset Diff_eq_empty_iff_mset subset_eq_mset_single_iff)
lemma butlast_list_update:
‹w < length xs ⟹ butlast (xs[w := last xs]) = take w xs @ butlast (last xs # drop (Suc w) xs)›
by (induction xs arbitrary: w) (auto split: nat.splits if_splits simp: upd_conv_take_nth_drop)
lemma mset_butlast_remove1_mset: ‹xs ≠ [] ⟹ mset (butlast xs) = remove1_mset (last xs) (mset xs)›
apply (subst(2) append_butlast_last_id[of xs, symmetric])
apply assumption
apply (simp only: mset_append)
by auto
lemma distinct_mset_mono: ‹D' ⊆# D ⟹ distinct_mset D ⟹ distinct_mset D'›
by (metis distinct_mset_union subset_mset.le_iff_add)
lemma distinct_mset_mono_strict: ‹D' ⊂# D ⟹ distinct_mset D ⟹ distinct_mset D'›
using distinct_mset_mono by auto
lemma subset_mset_trans_add_mset:
‹D ⊆# D' ⟹ D ⊆# add_mset L D'›
by (metis add_mset_remove_trivial diff_subset_eq_self subset_mset.dual_order.trans)
lemma subset_add_mset_notin_subset: ‹L ∉# E ⟹ E ⊆# add_mset L D ⟷ E ⊆# D›
by (meson subset_add_mset_notin_subset_mset subset_mset_trans_add_mset)
lemma remove1_mset_empty_iff: ‹remove1_mset L N = {#} ⟷ N = {#L#} ∨ N = {#}›
by (cases ‹L ∈# N›; cases N) auto
lemma distinct_subseteq_iff :
assumes dist: "distinct_mset M" and fin: "distinct_mset N"
shows "set_mset M ⊆ set_mset N ⟷ M ⊆# N"
proof
assume "set_mset M ⊆ set_mset N"
then show "M ⊆# N"
using dist fin by auto
next
assume "M ⊆# N"
then show "set_mset M ⊆ set_mset N"
by (metis set_mset_mono)
qed
lemma distinct_set_mset_eq_iff:
assumes ‹distinct_mset M› ‹distinct_mset N›
shows ‹set_mset M = set_mset N ⟷ M = N›
using assms distinct_mset_set_mset_ident by fastforce
lemma (in -) distinct_mset_union2:
‹distinct_mset (A + B) ⟹ distinct_mset B›
using distinct_mset_union[of B A]
by (auto simp: ac_simps)
lemma in_remove1_msetI: ‹x ≠ a ⟹ x ∈# M ⟹ x ∈# remove1_mset a M›
by (simp add: in_remove1_mset_neq)
lemma count_multi_member_split:
‹count M a ≥ n ⟹ ∃M'. M = replicate_mset n a + M'›
apply (induction n arbitrary: M)
subgoal by auto
subgoal premises IH for n M
using IH(1)[of ‹remove1_mset a M›] IH(2)
apply (cases ‹n ≤ count M a - Suc 0›)
apply (auto dest!: Suc_le_D)
by (metis count_greater_zero_iff insert_DiffM zero_less_Suc)
done
lemma count_image_mset_multi_member_split:
‹count (image_mset f M) L ≥ Suc 0 ⟹ ∃K. f K = L ∧ K ∈# M›
by auto
lemma count_image_mset_multi_member_split_2:
assumes count: ‹count (image_mset f M) L ≥ 2›
shows ‹∃K K' M'. f K = L ∧ K ∈# M ∧ f K' = L ∧ K' ∈# remove1_mset K M ∧
M = {#K, K'#} + M'›
proof -
obtain K where
K: ‹f K = L› ‹K ∈# M›
using count_image_mset_multi_member_split[of f M L] count by fastforce
then obtain K' where
K': ‹f K' = L› ‹K' ∈# remove1_mset K M›
using count_image_mset_multi_member_split[of f ‹remove1_mset K M› L] count
by (auto dest!: multi_member_split)
moreover have ‹∃M'. M = {#K, K'#} + M'›
using multi_member_split[of K M] multi_member_split[of K' ‹remove1_mset K M›] K K'
by (auto dest!: multi_member_split)
then show ?thesis
using K K' by blast
qed
lemma minus_notin_trivial: "L ∉# A ⟹ A - add_mset L B = A - B"
by (metis diff_intersect_left_idem inter_add_right1)
lemma minus_notin_trivial2: ‹b ∉# A ⟹ A - add_mset e (add_mset b B) = A - add_mset e B›
by (subst add_mset_commute) (auto simp: minus_notin_trivial)
lemma diff_union_single_conv3: ‹a ∉# I ⟹ remove1_mset a (I + J) = I + remove1_mset a J›
by (metis diff_union_single_conv remove_1_mset_id_iff_notin union_iff)
lemma filter_union_or_split:
‹{#L ∈# C. P L ∨ Q L#} = {#L ∈# C. P L#} + {#L ∈# C. ¬P L ∧ Q L#}›
by (induction C) auto
lemma subset_mset_minus_eq_add_mset_noteq: ‹A ⊂# C ⟹ A - B ≠ C›
by (auto simp: dest: in_diffD)
lemma minus_eq_id_forall_notin_mset:
‹A - B = A ⟷ (∀L ∈# B. L ∉# A)›
by (induction A)
(auto dest!: multi_member_split simp: subset_mset_minus_eq_add_mset_noteq)
lemma in_multiset_minus_notin_snd[simp]: ‹a ∉# B ⟹ a ∈# A - B ⟷ a ∈# A›
by (metis count_greater_zero_iff count_inI in_diff_count)
lemma distinct_mset_in_diff:
‹distinct_mset C ⟹ a ∈# C - D ⟷ a ∈# C ∧ a ∉# D›
by (meson distinct_mem_diff_mset in_multiset_minus_notin_snd)
lemma diff_le_mono2_mset: ‹A ⊆# B ⟹ C - B ⊆# C - A›
apply (auto simp: subseteq_mset_def ac_simps)
by (simp add: diff_le_mono2)
lemma subseteq_remove1[simp]: ‹C ⊆# C' ⟹ remove1_mset L C ⊆# C'›
by (meson diff_subset_eq_self subset_mset.dual_order.trans)
lemma filter_mset_cong2:
"(⋀x. x ∈# M ⟹ f x = g x) ⟹ M = N ⟹ filter_mset f M = filter_mset g N"
by (hypsubst, rule filter_mset_cong, simp)
lemma filter_mset_cong_inner_outer:
assumes
M_eq: ‹(⋀x. x ∈# M ⟹ f x = g x)› and
notin: ‹(⋀x. x ∈# N - M ⟹ ¬g x)› and
MN: ‹M ⊆# N›
shows ‹filter_mset f M = filter_mset g N›
proof -
define NM where ‹NM = N - M›
have N: ‹N = M + NM›
unfolding NM_def using MN by simp
have ‹filter_mset g NM = {#}›
using notin unfolding NM_def[symmetric] by (auto simp: filter_mset_empty_conv)
moreover have ‹filter_mset f M = filter_mset g M›
by (rule filter_mset_cong) (use M_eq in auto)
ultimately show ?thesis
unfolding N by simp
qed
lemma notin_filter_mset:
‹K ∉# C ⟹ filter_mset P C = filter_mset (λL. P L ∧ L ≠ K) C›
by (rule filter_mset_cong) auto
lemma distinct_mset_add_mset_filter:
assumes ‹distinct_mset C› and ‹L ∈# C› and ‹¬P L›
shows ‹add_mset L (filter_mset P C) = filter_mset (λx. P x ∨ x = L) C›
using assms
proof (induction C)
case empty
then show ?case by simp
next
case (add x C) note dist = this(2) and LC = this(3) and P[simp] = this(4) and _ = this
then have IH: ‹L ∈# C ⟹ add_mset L (filter_mset P C) = {#x ∈# C. P x ∨ x = L#}› by auto
show ?case
proof (cases ‹x = L›)
case [simp]: True
have ‹filter_mset P C = {#x ∈# C. P x ∨ x = L#}›
by (rule filter_mset_cong2) (use dist in auto)
then show ?thesis
by auto
next
case False
then show ?thesis
using IH LC by auto
qed
qed
lemma set_mset_set_mset_eq_iff: ‹set_mset A = set_mset B ⟷ (∀a∈#A. a ∈# B) ∧ (∀a∈#B. a ∈# A)›
by blast
lemma remove1_mset_union_distrib:
‹remove1_mset a (M ∪# N) = remove1_mset a M ∪# remove1_mset a N›
by (auto simp: multiset_eq_iff)
lemma member_add_mset: ‹a ∈# add_mset x xs ⟷ a = x ∨ a ∈# xs›
by simp
lemma sup_union_right_if:
‹N ∪# add_mset x M =
(if x ∉# N then add_mset x (N ∪# M) else add_mset x (remove1_mset x N ∪# M))›
by (auto simp: sup_union_right2)
lemma same_mset_distinct_iff:
‹mset M = mset M' ⟹ distinct M ⟷ distinct M'›
by (auto simp: distinct_mset_mset_distinct[symmetric] simp del: distinct_mset_mset_distinct)
lemma inj_on_image_mset_eq_iff:
assumes inj: ‹inj_on f (set_mset (M + M'))›
shows ‹image_mset f M' = image_mset f M ⟷ M' = M› (is ‹?A = ?B›)
proof
assume ?B
then show ?A by auto
next
assume ?A
then show ?B
using inj
proof(induction M arbitrary: M')
case empty
then show ?case by auto
next
case (add x M) note IH = this(1) and H = this(2) and inj = this(3)
obtain M1 x' where
M': ‹M' = add_mset x' M1› and
f_xx': ‹f x' = f x› and
M1_M: ‹image_mset f M1 = image_mset f M›
using H by (auto dest!: msed_map_invR)
moreover have ‹M1 = M›
apply (rule IH[OF M1_M])
using inj by (auto simp: M')
moreover have ‹x = x'›
using inj f_xx' by (auto simp: M')
ultimately show ?case by fast
qed
qed
lemma inj_image_mset_eq_iff:
assumes inj: ‹inj f›
shows ‹image_mset f M' = image_mset f M ⟷ M' = M›
using inj_on_image_mset_eq_iff[of f M' M] assms
by (simp add: inj_eq multiset.inj_map)
lemma singleton_eq_image_mset_iff: ‹{#a#} = f `# NE' ⟷ (∃b. NE' = {#b#} ∧ f b = a)›
by (cases NE') auto
lemma image_mset_If_eq_notin:
‹C ∉# A ⟹ {#f (if x = C then a x else b x). x ∈# A#} = {# f(b x). x ∈# A #}›
by (induction A) auto
lemma finite_mset_set_inter:
‹finite A ⟹ finite B ⟹ mset_set (A ∩ B) = mset_set A ∩# mset_set B›
apply (induction A rule: finite_induct)
subgoal by auto
subgoal for a A
apply (cases ‹a ∈ B›; cases ‹a ∈# mset_set B›)
using multi_member_split[of a ‹mset_set B›]
by (auto simp: mset_set.insert_remove)
done
lemma distinct_mset_inter_remdups_mset:
assumes dist: ‹distinct_mset A›
shows ‹A ∩# remdups_mset B = A ∩# B›
proof -
have [simp]: ‹A' ∩# remove1_mset a (remdups_mset Aa) = A' ∩# Aa›
if
‹A' ∩# remdups_mset Aa = A' ∩# Aa› and
‹a ∉# A'› and
‹a ∈# Aa›
for A' Aa :: ‹'a multiset› and a
by (metis insert_DiffM inter_add_right1 set_mset_remdups_mset that)
show ?thesis
using dist
apply (induction A)
subgoal by auto
subgoal for a A'
apply (cases ‹a ∈# B›)
using multi_member_split[of a ‹B›] multi_member_split[of a ‹A›]
by (auto simp: mset_set.insert_remove)
done
qed
lemma mset_butlast_update_last[simp]:
‹w < length xs ⟹ mset (butlast (xs[w := last (xs)])) = remove1_mset (xs ! w) (mset xs)›
by (cases ‹xs = []›)
(auto simp add: last_list_update_to_last mset_butlast_remove1_mset mset_update)
lemma in_multiset_ge_Max: ‹a ∈# N ⟹ a > Max (insert 0 (set_mset N)) ⟹ False›
by (simp add: leD)
lemma distinct_mset_set_mset_remove1_mset:
‹distinct_mset M ⟹ set_mset (remove1_mset c M) = set_mset M - {c}›
by (cases ‹c ∈# M›) (auto dest!: multi_member_split simp: add_mset_eq_add_mset)
lemma distinct_count_msetD:
‹distinct xs ⟹ count (mset xs) a = (if a ∈ set xs then 1 else 0)›
unfolding distinct_count_atmost_1 by auto
lemma filter_mset_and_implied:
‹(⋀ia. ia ∈# xs ⟹ Q ia ⟹ P ia) ⟹ {#ia ∈# xs. P ia ∧ Q ia#} = {#ia ∈# xs. Q ia#}›
by (rule filter_mset_cong2) auto
lemma filter_mset_eq_add_msetD: ‹filter_mset P xs = add_mset a A ⟹ a ∈# xs ∧ P a›
by (induction xs arbitrary: A)
(auto split: if_splits simp: add_mset_eq_add_mset)
lemma filter_mset_eq_add_msetD': ‹add_mset a A = filter_mset P xs ⟹ a ∈# xs ∧ P a›
using filter_mset_eq_add_msetD[of P xs a A] by auto
lemma image_filter_replicate_mset:
‹{#Ca ∈# replicate_mset m C. P Ca#} = (if P C then replicate_mset m C else {#})›
by (induction m) auto
lemma size_Union_mset_image_mset:
‹size (⋃# A) = (∑i ∈# A. size i)›
by (induction A) auto
lemma image_mset_minus_inj_on:
‹inj_on f (set_mset A ∪ set_mset B) ⟹ f `# (A - B) = f `# A - f `# B›
apply (induction A arbitrary: B)
subgoal by auto
subgoal for x A B
apply (cases ‹x ∈# B›)
apply (auto dest!: multi_member_split)
apply (subst diff_add_mset_swap)
apply auto
done
done
lemma filter_mset_mono_subset:
‹A ⊆# B ⟹ (⋀x. x ∈# A ⟹ P x ⟹ Q x) ⟹ filter_mset P A ⊆# filter_mset Q B›
by (metis multiset_filter_mono multiset_filter_mono2 subset_mset.order_trans)
lemma mset_inter_empty_set_mset: ‹M ∩# xc = {#} ⟷ set_mset M ∩ set_mset xc = {}›
by (induction xc) auto
lemma sum_mset_mset_set_sum_set:
‹(∑A ∈# mset_set As. f A) = (∑A ∈ As. f A)›
apply (cases ‹finite As›)
by (induction As rule: finite_induct) auto
lemma sum_mset_sum_count:
‹(∑A ∈# As. f A) = (∑A ∈ set_mset As. count As A * f A)›
proof (induction As)
case empty
then show ?case by auto
next
case (add x As)
define n where ‹n = count As x›
define As' where ‹As' ≡ removeAll_mset x As›
have As: ‹As = As' + replicate_mset n x›
by (auto simp: As'_def n_def intro!: multiset_eqI)
have [simp]: ‹set_mset As' - {x} = set_mset As'› ‹count As' x = 0› ‹x ∉# As'›
unfolding As'_def
by auto
have ‹ (∑A∈set_mset As'.
(if x = A then Suc (count (As' + replicate_mset n x) A)
else count (As' + replicate_mset n x) A) *
f A) =
(∑A∈set_mset As'.
(count (As' + replicate_mset n x) A) *
f A)›
by (rule sum.cong) auto
then show ?case using add by (auto simp: As sum.insert_remove)
qed
lemma sum_mset_inter_restrict:
‹(∑ x ∈# filter_mset P M. f x) = (∑ x ∈# M. if P x then f x else 0)›
by (induction M) auto
lemma mset_set_subset_iff:
‹mset_set A ⊆# I ⟷ infinite A ∨ A ⊆ set_mset I›
by (metis finite_set_mset finite_set_mset_mset_set mset_set.infinite mset_set_set_mset_subseteq
set_mset_mono subset_imp_msubset_mset_set subset_mset.bot.extremum subset_mset.dual_order.trans)
lemma sumset_diff_constant_left:
assumes ‹⋀x. x ∈# A ⟹ f x ≤ n›
shows ‹(∑x∈# A . n - f x) = size A * n - (∑x∈# A . f x)›
proof -
have ‹size A * n ≥ (∑x∈# A . f x)›
if ‹⋀x. x ∈# A ⟹ f x ≤ n› for A
using that
by (induction A) (force simp: ac_simps)+
then show ?thesis
using assms
by (induction A) (auto simp: ac_simps)
qed
lemma mset_set_eq_mset_iff: ‹finite x ⟹ mset_set x = mset xs ⟷ distinct xs ∧ x = set xs›
apply (auto simp flip: distinct_mset_mset_distinct eq_commute[of _ ‹mset_set _›]
simp: distinct_mset_mset_set mset_set_set)
apply (metis finite_set_mset_mset_set set_mset_mset)
apply (metis finite_set_mset_mset_set set_mset_mset)
done
lemma distinct_mset_iff:
‹¬distinct_mset C ⟷ (∃a C'. C = add_mset a (add_mset a C'))›
by (metis (no_types, hide_lams) One_nat_def
count_add_mset distinct_mset_add_mset distinct_mset_def
member_add_mset mset_add not_in_iff)
lemma diff_add_mset_remove1: ‹NO_MATCH {#} N ⟹ M - add_mset a N = remove1_mset a (M - N)›
by auto
section ‹Finite maps and multisets›
subsubsection ‹Finite sets and multisets›
abbreviation mset_fset :: ‹'a fset ⇒ 'a multiset› where
‹mset_fset N ≡ mset_set (fset N)›
definition fset_mset :: ‹'a multiset ⇒ 'a fset› where
‹fset_mset N ≡ Abs_fset (set_mset N)›
lemma fset_mset_mset_fset: ‹fset_mset (mset_fset N) = N›
by (auto simp: fset.fset_inverse fset_mset_def)
lemma mset_fset_fset_mset[simp]:
‹mset_fset (fset_mset N) = remdups_mset N›
by (auto simp: fset.fset_inverse fset_mset_def Abs_fset_inverse remdups_mset_def)
lemma in_mset_fset_fmember[simp]: ‹x ∈# mset_fset N ⟷ x |∈| N›
by (auto simp: fmember.rep_eq)
lemma in_fset_mset_mset[simp]: ‹x |∈| fset_mset N ⟷ x ∈# N›
by (auto simp: fmember.rep_eq fset_mset_def Abs_fset_inverse)
lemma distinct_mset_subset_iff_remdups:
‹distinct_mset a ⟹ a ⊆# b ⟷ a ⊆# remdups_mset b›
by (simp add: distinct_mset_inter_remdups_mset subset_mset.le_iff_inf)
subsubsection ‹Finite map and multisets›
text ‹Roughly the same as \<^term>‹ran› and \<^term>‹dom›, but with duplication in the content (unlike their
finite sets counterpart) while still working on finite domains (unlike a function mapping).
Remark that \<^term>‹dom_m› (the keys) does not contain duplicates, but we keep for symmetry (and for
easier use of multiset operators as in the definition of \<^term>‹ran_m›).
›
definition dom_m where
‹dom_m N = mset_fset (fmdom N)›
definition ran_m where
‹ran_m N = the `# fmlookup N `# dom_m N›
lemma dom_m_fmdrop[simp]: ‹dom_m (fmdrop C N) = remove1_mset C (dom_m N)›
unfolding dom_m_def
by (cases ‹C |∈| fmdom N›)
(auto simp: mset_set.remove fmember.rep_eq)
lemma dom_m_fmdrop_All: ‹dom_m (fmdrop C N) = removeAll_mset C (dom_m N)›
unfolding dom_m_def
by (cases ‹C |∈| fmdom N›)
(auto simp: mset_set.remove fmember.rep_eq)
lemma dom_m_fmupd[simp]: ‹dom_m (fmupd k C N) = add_mset k (remove1_mset k (dom_m N))›
unfolding dom_m_def
by (cases ‹k |∈| fmdom N›)
(auto simp: mset_set.remove fmember.rep_eq mset_set.insert_remove)
lemma distinct_mset_dom: ‹distinct_mset (dom_m N)›
by (simp add: distinct_mset_mset_set dom_m_def)
lemma in_dom_m_lookup_iff: ‹C ∈# dom_m N' ⟷ fmlookup N' C ≠ None›
by (auto simp: dom_m_def fmdom.rep_eq fmlookup_dom'_iff)
lemma in_dom_in_ran_m[simp]: ‹i ∈# dom_m N ⟹ the (fmlookup N i) ∈# ran_m N›
by (auto simp: ran_m_def)
lemma fmupd_same[simp]:
‹x1 ∈# dom_m x1aa ⟹ fmupd x1 (the (fmlookup x1aa x1)) x1aa = x1aa›
by (metis fmap_ext fmupd_lookup in_dom_m_lookup_iff option.collapse)
lemma ran_m_fmempty[simp]: ‹ran_m fmempty = {#}› and
dom_m_fmempty[simp]: ‹dom_m fmempty = {#}›
by (auto simp: ran_m_def dom_m_def)
lemma fmrestrict_set_fmupd:
‹a ∈ xs ⟹ fmrestrict_set xs (fmupd a C N) = fmupd a C (fmrestrict_set xs N)›
‹a ∉ xs ⟹ fmrestrict_set xs (fmupd a C N) = fmrestrict_set xs N›
by (auto simp: fmfilter_alt_defs)
lemma fset_fmdom_fmrestrict_set:
‹fset (fmdom (fmrestrict_set xs N)) = fset (fmdom N) ∩ xs›
by (auto simp: fmfilter_alt_defs)
lemma dom_m_fmrestrict_set: ‹dom_m (fmrestrict_set (set xs) N) = mset xs ∩# dom_m N›
using fset_fmdom_fmrestrict_set[of ‹set xs› N] distinct_mset_dom[of N]
distinct_mset_inter_remdups_mset[of ‹mset_fset (fmdom N)› ‹mset xs›]
by (auto simp: dom_m_def fset_mset_mset_fset finite_mset_set_inter multiset_inter_commute
remdups_mset_def)
lemma dom_m_fmrestrict_set': ‹dom_m (fmrestrict_set xs N) = mset_set (xs ∩ set_mset (dom_m N))›
using fset_fmdom_fmrestrict_set[of ‹xs› N] distinct_mset_dom[of N]
by (auto simp: dom_m_def fset_mset_mset_fset finite_mset_set_inter multiset_inter_commute
remdups_mset_def)
lemma indom_mI: ‹fmlookup m x = Some y ⟹ x ∈# dom_m m›
by (drule fmdomI) (auto simp: dom_m_def fmember.rep_eq)
lemma fmupd_fmdrop_id:
assumes ‹k |∈| fmdom N'›
shows ‹fmupd k (the (fmlookup N' k)) (fmdrop k N') = N'›
proof -
have [simp]: ‹map_upd k (the (fmlookup N' k))
(λx. if x ≠ k then fmlookup N' x else None) =
map_upd k (the (fmlookup N' k))
(fmlookup N')›
by (auto intro!: ext simp: map_upd_def)
have [simp]: ‹map_upd k (the (fmlookup N' k)) (fmlookup N') = fmlookup N'›
using assms
by (auto intro!: ext simp: map_upd_def)
have [simp]: ‹finite (dom (λx. if x = k then None else fmlookup N' x))›
by (subst dom_if) auto
show ?thesis
apply (auto simp: fmupd_def fmupd.abs_eq[symmetric])
unfolding fmlookup_drop
apply (simp add: fmlookup_inverse)
done
qed
lemma fm_member_split: ‹k |∈| fmdom N' ⟹ ∃N'' v. N' = fmupd k v N'' ∧ the (fmlookup N' k) = v ∧
k |∉| fmdom N''›
by (rule exI[of _ ‹fmdrop k N'›])
(auto simp: fmupd_fmdrop_id)
lemma ‹fmdrop k (fmupd k va N'') = fmdrop k N''›
by (simp add: fmap_ext)
lemma fmap_ext_fmdom:
‹(fmdom N = fmdom N') ⟹ (⋀ x. x |∈| fmdom N ⟹ fmlookup N x = fmlookup N' x) ⟹
N = N'›
by (rule fmap_ext)
(case_tac ‹x |∈| fmdom N›, auto simp: fmdom_notD)
lemma fmrestrict_set_insert_in:
‹xa ∈ fset (fmdom N) ⟹
fmrestrict_set (insert xa l1) N = fmupd xa (the (fmlookup N xa)) (fmrestrict_set l1 N)›
apply (rule fmap_ext_fmdom)
apply (auto simp: fset_fmdom_fmrestrict_set fmember.rep_eq notin_fset dest: fmdom_notD; fail)[]
apply (auto simp: fmlookup_dom_iff; fail)
done
lemma fmrestrict_set_insert_notin:
‹xa ∉ fset (fmdom N) ⟹
fmrestrict_set (insert xa l1) N = fmrestrict_set l1 N›
by (rule fmap_ext_fmdom)
(auto simp: fset_fmdom_fmrestrict_set fmember.rep_eq notin_fset dest: fmdom_notD)
lemma fmrestrict_set_insert_in_dom_m[simp]:
‹xa ∈# dom_m N ⟹
fmrestrict_set (insert xa l1) N = fmupd xa (the (fmlookup N xa)) (fmrestrict_set l1 N)›
by (simp add: fmrestrict_set_insert_in dom_m_def)
lemma fmrestrict_set_insert_notin_dom_m[simp]:
‹xa ∉# dom_m N ⟹
fmrestrict_set (insert xa l1) N = fmrestrict_set l1 N›
by (simp add: fmrestrict_set_insert_notin dom_m_def)
lemma fmlookup_restrict_set_id: ‹fset (fmdom N) ⊆ A ⟹ fmrestrict_set A N = N›
by (metis fmap_ext fmdom'_alt_def fmdom'_notD fmlookup_restrict_set subset_iff)
lemma fmlookup_restrict_set_id': ‹set_mset (dom_m N) ⊆ A ⟹ fmrestrict_set A N = N›
by (rule fmlookup_restrict_set_id)
(auto simp: dom_m_def)
lemma ran_m_mapsto_upd:
assumes
NC: ‹C ∈# dom_m N›
shows ‹ran_m (fmupd C C' N) =
add_mset C' (remove1_mset (the (fmlookup N C)) (ran_m N))›
proof -
define N' where
‹N' = fmdrop C N›
have N_N': ‹dom_m N = add_mset C (dom_m N')›
using NC unfolding N'_def by auto
have ‹C ∉# dom_m N'›
using NC distinct_mset_dom[of N] unfolding N_N' by auto
then show ?thesis
by (auto simp: N_N' ran_m_def mset_set.insert_remove image_mset_remove1_mset_if
intro!: image_mset_cong)
qed
lemma ran_m_mapsto_upd_notin:
assumes
NC: ‹C ∉# dom_m N›
shows ‹ran_m (fmupd C C' N) = add_mset C' (ran_m N)›
using NC
by (auto simp: ran_m_def mset_set.insert_remove image_mset_remove1_mset_if
intro!: image_mset_cong split: if_splits)
lemma ran_m_fmdrop:
‹C ∈# dom_m N ⟹ ran_m (fmdrop C N) = remove1_mset (the (fmlookup N C)) (ran_m N)›
using distinct_mset_dom[of N]
by (cases ‹fmlookup N C›)
(auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›]
dest!: multi_member_split
intro!: filter_mset_cong2 image_mset_cong2)
lemma ran_m_fmdrop_notin:
‹C ∉# dom_m N ⟹ ran_m (fmdrop C N) = ran_m N›
using distinct_mset_dom[of N]
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›]
dest!: multi_member_split
intro!: filter_mset_cong2 image_mset_cong2)
lemma ran_m_fmdrop_If:
‹ran_m (fmdrop C N) = (if C ∈# dom_m N then remove1_mset (the (fmlookup N C)) (ran_m N) else ran_m N)›
using distinct_mset_dom[of N]
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›]
dest!: multi_member_split
intro!: filter_mset_cong2 image_mset_cong2)
subsubsection ‹Compact domain for finite maps›
text ‹\<^term>‹packed› is a predicate to indicate that the domain of finite mapping starts at
\<^term>‹1::nat› and does not contain holes. We used it in the SAT solver for the mapping from
indexes to clauses, to ensure that there not holes and therefore giving an upper bound on the
highest key.
TODO KILL!
›
definition Max_dom where
‹Max_dom N = Max (set_mset (add_mset 0 (dom_m N)))›
definition packed where
‹packed N ⟷ dom_m N = mset [1..<Suc (Max_dom N)]›
text ‹Marking this rule as simp is not compatible with unfolding the definition of packed when
marked as:›
lemma Max_dom_empty: ‹dom_m b = {#} ⟹ Max_dom b = 0›
by (auto simp: Max_dom_def)
lemma Max_dom_fmempty: ‹Max_dom fmempty = 0›
by (auto simp: Max_dom_empty)
lemma packed_empty[simp]: ‹packed fmempty›
by (auto simp: packed_def Max_dom_empty)
lemma packed_Max_dom_size:
assumes p: ‹packed N›
shows ‹Max_dom N = size (dom_m N)›
proof -
have 1: ‹dom_m N = mset [1..<Suc (Max_dom N)]›
using p unfolding packed_def Max_dom_def[symmetric] .
have ‹size (dom_m N) = size (mset [1..<Suc (Max_dom N)])›
unfolding 1 ..
also have ‹… = length [1..<Suc (Max_dom N)]›
unfolding size_mset ..
also have ‹… = Max_dom N›
unfolding length_upt by simp
finally show ?thesis
by simp
qed
lemma Max_dom_le:
‹L ∈# dom_m N ⟹ L ≤ Max_dom N›
by (auto simp: Max_dom_def)
lemma remove1_mset_ge_Max_some: ‹a > Max_dom b ⟹ remove1_mset a (dom_m b) = dom_m b›
by (auto simp: Max_dom_def remove_1_mset_id_iff_notin
dest!: multi_member_split)
lemma Max_dom_fmupd_irrel:
‹(a :: 'a :: {zero,linorder}) > Max_dom M ⟹ Max_dom (fmupd a C M) = max a (Max_dom M)›
by (cases ‹dom_m M›)
(auto simp: Max_dom_def remove1_mset_ge_Max_some ac_simps)
lemma Max_dom_alt_def: ‹Max_dom b = Max (insert 0 (set_mset (dom_m b)))›
unfolding Max_dom_def by auto
lemma Max_insert_Suc_Max_dim_dom[simp]:
‹Max (insert (Suc (Max_dom b)) (set_mset (dom_m b))) = Suc (Max_dom b)›
unfolding Max_dom_alt_def
by (cases ‹set_mset (dom_m b) = {}›) auto
lemma size_dom_m_Max_dom:
‹size (dom_m N) ≤ Suc (Max_dom N)›
proof -
have ‹dom_m N ⊆# mset_set {0..< Suc (Max_dom N)}›
apply (rule distinct_finite_set_mset_subseteq_iff[THEN iffD1])
subgoal by (auto simp: distinct_mset_dom)
subgoal by auto
subgoal by (auto dest: Max_dom_le)
done
from size_mset_mono[OF this] show ?thesis by auto
qed
lemma Max_atLeastLessThan_plus: ‹Max {(a::nat) ..< a+n} = (if n = 0 then Max {} else a+n - 1)›
apply (induction n arbitrary: a)
subgoal by auto
subgoal for n a
by (cases n)
(auto simp: image_Suc_atLeastLessThan[symmetric] mono_Max_commute[symmetric] mono_def
atLeastLessThanSuc
simp del: image_Suc_atLeastLessThan)
done
lemma Max_atLeastLessThan: ‹Max {(a::nat) ..< b} = (if b ≤ a then Max {} else b - 1)›
using Max_atLeastLessThan_plus[of a ‹b-a›]
by auto
lemma Max_insert_Max_dom_into_packed:
‹Max (insert (Max_dom bc) {Suc 0..<Max_dom bc}) = Max_dom bc›
by (cases ‹Max_dom bc›; cases ‹Max_dom bc - 1›)
(auto simp: Max_dom_empty Max_atLeastLessThan)
lemma packed0_fmud_Suc_Max_dom: ‹packed b ⟹ packed (fmupd (Suc (Max_dom b)) C b)›
by (auto simp: packed_def remove1_mset_ge_Max_some Max_dom_fmupd_irrel max_def)
lemma ge_Max_dom_notin_dom_m: ‹a > Max_dom ao ⟹ a ∉# dom_m ao›
by (auto simp: Max_dom_def)
lemma packed_in_dom_mI: ‹packed bc ⟹ j ≤ Max_dom bc ⟹ 0 < j ⟹ j ∈# dom_m bc›
by (auto simp: packed_def)
lemma mset_fset_empty_iff: ‹mset_fset a = {#} ⟷ a = fempty›
by (cases a) (auto simp: mset_set_empty_iff)
lemma dom_m_empty_iff[iff]:
‹dom_m NU = {#} ⟷ NU = fmempty›
by (cases NU) (auto simp: dom_m_def mset_fset_empty_iff mset_set.insert_remove)
lemma nat_power_div_base:
fixes k :: nat
assumes "0 < m" "0 < k"
shows "k ^ m div k = (k::nat) ^ (m - Suc 0)"
proof -
have eq: "k ^ m = k ^ ((m - Suc 0) + Suc 0)"
by (simp add: assms)
show ?thesis
using assms by (simp only: power_add eq) auto
qed
end