Theory List_Utilities
chapter ‹ List Utility Theorems ›
theory List_Utilities
imports
"HOL-Combinatorics.List_Permutation"
begin
text ‹ Throughout our work it will be necessary to reuse common lemmas
regarding lists and multisets. These results are proved in the
following section and reused by subsequent lemmas and theorems. ›
section ‹ Multisets ›
lemma length_sub_mset:
assumes "mset Ψ ⊆# mset Γ"
and "length Ψ >= length Γ"
shows "mset Ψ = mset Γ"
using assms
by (metis
append_Nil2
append_eq_append_conv
leD
linorder_neqE_nat
mset_le_perm_append
perm_length
size_mset
size_mset_mono)
lemma set_exclusion_mset_simplify:
assumes "¬ (∃ ψ ∈ set Ψ. ψ ∈ set Σ)"
and "mset Ψ ⊆# mset (Σ @ Γ)"
shows "mset Ψ ⊆# mset Γ"
using assms
proof (induct Σ)
case Nil
then show ?case by simp
next
case (Cons σ Σ)
then show ?case
by (cases "σ ∈ set Ψ",
fastforce,
metis
add.commute
add_mset_add_single
diff_single_trivial
in_multiset_in_set
mset.simps(2)
notin_set_remove1
remove_hd
subset_eq_diff_conv
union_code
append_Cons)
qed
lemma image_mset_cons_homomorphism:
"image_mset mset (image_mset ((#) φ) Φ) = image_mset ((+) {# φ #}) (image_mset mset Φ)"
by (induct Φ, simp+)
lemma image_mset_append_homomorphism:
"image_mset mset (image_mset ((@) Δ) Φ) = image_mset ((+) (mset Δ)) (image_mset mset Φ)"
by (induct Φ, simp+)
lemma image_mset_add_collapse:
fixes A B :: "'a multiset"
shows "image_mset ((+) A) (image_mset ((+) B) X) = image_mset ((+) (A + B)) X"
by (induct X, simp, simp)
lemma remove1_remdups_removeAll: "remove1 x (remdups A) = remdups (removeAll x A)"
proof (induct A)
case Nil
then show ?case by simp
next
case (Cons a A)
then show ?case
by (cases "a = x", (simp add: Cons)+)
qed
lemma mset_remdups:
assumes "mset A = mset B"
shows "mset (remdups A) = mset (remdups B)"
proof -
have "∀ B. mset A = mset B ⟶ mset (remdups A) = mset (remdups B)"
proof (induct A)
case Nil
then show ?case by simp
next
case (Cons a A)
{
fix B
assume "mset (a # A) = mset B"
hence "mset A = mset (remove1 a B)"
by (metis add_mset_add_mset_same_iff
list.set_intros(1)
mset.simps(2)
mset_eq_setD
perm_remove)
hence "mset (remdups A) = mset (remdups (remove1 a B))"
using Cons.hyps by blast
hence "mset (remdups (a # (remdups A))) = mset (remdups (a # (remdups (remove1 a B))))"
by (metis mset_eq_setD set_eq_iff_mset_remdups_eq list.simps(15))
hence " mset (remdups (a # (removeAll a (remdups A))))
= mset (remdups (a # (removeAll a (remdups (remove1 a B)))))"
by (metis insert_Diff_single list.set(2) set_eq_iff_mset_remdups_eq set_removeAll)
hence " mset (remdups (a # (remdups (removeAll a A))))
= mset (remdups (a # (remdups (removeAll a (remove1 a B)))))"
by (metis distinct_remdups distinct_remove1_removeAll remove1_remdups_removeAll)
hence "mset (remdups (remdups (a # A))) = mset (remdups (remdups (a # (remove1 a B))))"
by (metis ‹mset A = mset (remove1 a B)›
list.set(2)
mset_eq_setD
set_eq_iff_mset_remdups_eq)
hence "mset (remdups (a # A)) = mset (remdups (a # (remove1 a B)))"
by (metis remdups_remdups)
hence "mset (remdups (a # A)) = mset (remdups B)"
using ‹mset (a # A) = mset B› mset_eq_setD set_eq_iff_mset_remdups_eq by blast
}
then show ?case by simp
qed
thus ?thesis using assms by blast
qed
lemma mset_mset_map_snd_remdups:
assumes "mset (map mset A) = mset (map mset B)"
shows "mset (map (mset ∘ (map snd) ∘ remdups) A) = mset (map (mset ∘ (map snd) ∘ remdups) B)"
proof -
{
fix B :: "('a × 'b) list list"
fix b :: "('a × 'b) list"
assume "b ∈ set B"
hence " mset (map (mset ∘ (map snd) ∘ remdups) (b # (remove1 b B)))
= mset (map (mset ∘ (map snd) ∘ remdups) B)"
proof (induct B)
case Nil
then show ?case by simp
next
case (Cons b' B)
then show ?case
by (cases "b = b'", simp+)
qed
}
note ♢ = this
have
"∀ B :: ('a × 'b) list list.
mset (map mset A) = mset (map mset B)
⟶ mset (map (mset ∘ (map snd) ∘ remdups) A) = mset (map (mset ∘ (map snd) ∘ remdups) B)"
proof (induct A)
case Nil
then show ?case by simp
next
case (Cons a A)
{
fix B
assume ♠: "mset (map mset (a # A)) = mset (map mset B)"
hence "mset a ∈# mset (map mset B)"
by (simp,
metis ♠
image_set
list.set_intros(1)
list.simps(9)
mset_eq_setD)
from this obtain b where †:
"b ∈ set B"
"mset a = mset b"
by auto
with ♠ have "mset (map mset A) = mset (remove1 (mset b) (map mset B))"
by (simp add: union_single_eq_diff)
moreover have "mset B = mset (b # remove1 b B)" using † by simp
hence "mset (map mset B) = mset (map mset (b # (remove1 b B)))"
by (simp,
metis image_mset_add_mset
mset.simps(2)
mset_remove1)
ultimately have "mset (map mset A) = mset (map mset (remove1 b B))"
by simp
hence " mset (map (mset ∘ (map snd) ∘ remdups) A)
= mset (map (mset ∘ (map snd) ∘ remdups) (remove1 b B))"
using Cons.hyps by blast
moreover have "(mset ∘ (map snd) ∘ remdups) a = (mset ∘ (map snd) ∘ remdups) b"
using †(2) mset_remdups by fastforce
ultimately have
" mset (map (mset ∘ (map snd) ∘ remdups) (a # A))
= mset (map (mset ∘ (map snd) ∘ remdups) (b # (remove1 b B)))"
by simp
moreover have
" mset (map (mset ∘ (map snd) ∘ remdups) (b # (remove1 b B)))
= mset (map (mset ∘ (map snd) ∘ remdups) B)"
using †(1) ♢ by blast
ultimately have
" mset (map (mset ∘ (map snd) ∘ remdups) (a # A))
= mset (map (mset ∘ (map snd) ∘ remdups) B)"
by simp
}
then show ?case by blast
qed
thus ?thesis using assms by blast
qed
lemma mset_remdups_append_msub:
"mset (remdups A) ⊆# mset (remdups (B @ A))"
proof -
have "∀ B. mset (remdups A) ⊆# mset (remdups (B @ A))"
proof (induct A)
case Nil
then show ?case by simp
next
case (Cons a A)
{
fix B
have †: "mset (remdups (B @ (a # A))) = mset (remdups (a # (B @ A)))"
by (induct B, simp+)
have "mset (remdups (a # A)) ⊆# mset (remdups (B @ (a # A)))"
proof (cases "a ∈ set B ∧ a ∉ set A")
case True
hence †: "mset (remove1 a (remdups (B @ A))) = mset (remdups ((removeAll a B) @ A))"
by (simp add: remove1_remdups_removeAll)
hence " (add_mset a (mset (remdups A)) ⊆# mset (remdups (B @ A)))
= (mset (remdups A) ⊆# mset (remdups ((removeAll a B) @ A)))"
using True
by (simp add: insert_subset_eq_iff)
then show ?thesis
by (metis † Cons True
Un_insert_right
list.set(2)
mset.simps(2)
mset_subset_eq_insertD
remdups.simps(2)
set_append
set_eq_iff_mset_remdups_eq
set_mset_mset set_remdups)
next
case False
then show ?thesis using † Cons by simp
qed
}
thus ?case by blast
qed
thus ?thesis by blast
qed
section ‹ List Mapping ›
text ‹ The following notation for permutations is slightly nicer when
formatted in \LaTeX. ›
notation perm (infix "⇌" 50)
lemma map_monotonic:
assumes "mset A ⊆# mset B"
shows "mset (map f A) ⊆# mset (map f B)"
by (simp add: assms image_mset_subseteq_mono)
lemma perm_map_perm_list_exists:
assumes "A ⇌ map f B"
shows "∃ B'. A = map f B' ∧ B' ⇌ B"
proof -
have "∀B. A ⇌ map f B ⟶ (∃ B'. A = map f B' ∧ B' ⇌ B)"
proof (induct A)
case Nil
then show ?case by simp
next
case (Cons a A)
{
fix B
assume "a # A ⇌ map f B"
from this obtain b where b:
"b ∈ set B"
"f b = a"
by (metis
(full_types)
imageE
list.set_intros(1)
set_map
set_mset_mset)
hence "A ⇌ (remove1 (f b) (map f B))"
"B ⇌ b # remove1 b B"
by (metis
‹a # A ⇌ map f B›
perm_remove_perm
remove_hd,
meson b(1) perm_remove)
hence "A ⇌ (map f (remove1 b B))"
by (metis (no_types)
list.simps(9)
mset_map
mset_remove1
remove_hd)
from this obtain B' where B':
"A = map f B'"
"B' ⇌ (remove1 b B)"
using Cons.hyps by blast
with b have "a # A = map f (b # B')"
by simp
moreover have "B ⇌ b # B'"
by (metis B'(2) ‹mset B = mset (b # remove1 b B)› mset.simps(2))
ultimately have "∃B'. a # A = map f B' ∧ B' ⇌ B"
by (meson perm_sym)
}
thus ?case by blast
qed
with assms show ?thesis by blast
qed
lemma mset_sub_map_list_exists:
assumes "mset Φ ⊆# mset (map f Γ)"
shows "∃ Φ'. mset Φ' ⊆# mset Γ ∧ Φ = (map f Φ')"
proof -
have "∀ Φ. mset Φ ⊆# mset (map f Γ)
⟶ (∃ Φ'. mset Φ' ⊆# mset Γ ∧ Φ = (map f Φ'))"
proof (induct Γ)
case Nil
then show ?case by simp
next
case (Cons γ Γ)
{
fix Φ
assume "mset Φ ⊆# mset (map f (γ # Γ))"
have "∃Φ'. mset Φ' ⊆# mset (γ # Γ) ∧ Φ = map f Φ'"
proof cases
assume "f γ ∈ set Φ"
hence "f γ # (remove1 (f γ) Φ) ⇌ Φ"
by force
with ‹mset Φ ⊆# mset (map f (γ # Γ))›
have "mset (remove1 (f γ) Φ) ⊆# mset (map f Γ)"
by (metis
insert_subset_eq_iff
list.simps(9)
mset.simps(2)
mset_remove1
remove_hd)
from this Cons obtain Φ' where Φ':
"mset Φ' ⊆# mset Γ"
"remove1 (f γ) Φ = map f Φ'"
by blast
hence "mset (γ # Φ') ⊆# mset (γ # Γ)"
and "f γ # (remove1 (f γ) Φ) = map f (γ # Φ')"
by simp+
hence "Φ ⇌ map f (γ # Φ')"
using ‹f γ ∈ set Φ› perm_remove
by metis
from this obtain Φ'' where Φ'':
"Φ = map f Φ''"
"Φ'' ⇌ γ # Φ'"
using perm_map_perm_list_exists
by blast
hence "mset Φ'' ⊆# mset (γ # Γ)"
by (metis ‹mset (γ # Φ') ⊆# mset (γ # Γ)›)
thus ?thesis using Φ'' by blast
next
assume "f γ ∉ set Φ"
have "mset Φ - {#f γ#} = mset Φ"
by (metis (no_types)
‹f γ ∉ set Φ›
diff_single_trivial
set_mset_mset)
moreover
have "mset (map f (γ # Γ))
= add_mset (f γ) (image_mset f (mset Γ))"
by simp
ultimately have "mset Φ ⊆# mset (map f Γ)"
by (metis (no_types)
Diff_eq_empty_iff_mset
‹mset Φ ⊆# mset (map f (γ # Γ))›
add_mset_add_single
cancel_ab_semigroup_add_class.diff_right_commute
diff_diff_add mset_map)
with Cons show ?thesis
by (metis
mset_le_perm_append
perm_append_single
subset_mset.order_trans)
qed
}
thus ?case using Cons by blast
qed
thus ?thesis using assms by blast
qed
section ‹ Laws for Searching a List ›
lemma find_Some_predicate:
assumes "find P Ψ = Some ψ"
shows "P ψ"
using assms
proof (induct Ψ)
case Nil
then show ?case by simp
next
case (Cons ω Ψ)
then show ?case by (cases "P ω", fastforce+)
qed
lemma find_Some_set_membership:
assumes "find P Ψ = Some ψ"
shows "ψ ∈ set Ψ"
using assms
proof (induct Ψ)
case Nil
then show ?case by simp
next
case (Cons ω Ψ)
then show ?case by (cases "P ω", fastforce+)
qed
section ‹ Permutations ›
lemma perm_count_list:
assumes "Φ ⇌ Ψ"
shows "count_list Φ φ = count_list Ψ φ"
using assms
proof (induct Φ arbitrary: Ψ)
case Nil
then show ?case
by blast
next
case (Cons χ Φ Ψ)
hence ♢: "count_list Φ φ = count_list (remove1 χ Ψ) φ"
by (metis mset_remove1 remove_hd)
show ?case
proof cases
assume "χ = φ"
hence "count_list (χ # Φ) φ = count_list Φ φ + 1" by simp
with ♢ have "count_list (χ # Φ) φ = count_list (remove1 χ Ψ) φ + 1"
by simp
moreover
have "χ ∈ set Ψ"
by (metis Cons.prems list.set_intros(1) set_mset_mset)
hence "count_list (remove1 χ Ψ) φ + 1 = count_list Ψ φ"
using ‹χ = φ›
by (induct Ψ, simp, auto)
ultimately show ?thesis by simp
next
assume "χ ≠ φ"
with ♢ have "count_list (χ # Φ) φ = count_list (remove1 χ Ψ) φ"
by simp
moreover have "count_list (remove1 χ Ψ) φ = count_list Ψ φ"
using ‹χ ≠ φ›
by (induct Ψ, simp+)
ultimately show ?thesis by simp
qed
qed
lemma count_list_append:
"count_list (A @ B) a = count_list A a + count_list B a"
by (induct A, simp, simp)
lemma concat_remove1:
assumes "Ψ ∈ set ℒ"
shows "concat ℒ ⇌ Ψ @ concat (remove1 Ψ ℒ)"
using assms
by (induct ℒ, simp, simp, metis)
lemma concat_set_membership_mset_containment:
assumes "concat Γ ⇌ Λ"
and "Φ ∈ set Γ"
shows "mset Φ ⊆# mset Λ"
using assms
by (induct Γ, simp, simp, metis concat_remove1 mset_le_perm_append)
lemma (in comm_monoid_add) perm_list_summation:
assumes "Ψ ⇌ Φ"
shows "(∑ψ'←Ψ. f ψ') = (∑φ'←Φ. f φ')"
using assms
proof (induct Ψ arbitrary: Φ)
case Nil
then show ?case by auto
next
case (Cons ψ Ψ Φ)
hence "(∑ψ' ← Ψ. f ψ') = (∑φ' ← (remove1 ψ Φ). f φ')"
by (metis mset_remove1 remove_hd)
moreover have "ψ ∈ set Φ"
by (metis Cons.prems list.set_intros(1) set_mset_mset)
hence "(∑φ' ← (ψ # (remove1 ψ Φ)). f φ') = (∑φ'←Φ. f φ')"
proof (induct Φ)
case Nil
then show ?case by auto
next
case (Cons φ Φ)
show ?case
proof cases
assume "φ = ψ"
then show ?thesis by simp
next
assume "φ ≠ ψ"
hence "ψ ∈ set Φ"
using Cons.prems by auto
hence "(∑φ' ← (ψ # (remove1 ψ Φ)). f φ') = (∑φ'←Φ. f φ')"
using Cons.hyps by blast
hence "(∑φ'←(φ # Φ). f φ')
= (∑φ' ← (ψ # φ # (remove1 ψ Φ)). f φ')"
by (simp add: add.left_commute)
moreover
have "(ψ # (φ # (remove1 ψ Φ))) = (ψ # (remove1 ψ (φ # Φ)))"
using ‹φ ≠ ψ› by simp
ultimately show ?thesis
by simp
qed
qed
ultimately show ?case
by simp
qed
section ‹ List Duplicates ›
primrec duplicates :: "'a list ⇒ 'a set"
where
"duplicates [] = {}"
| "duplicates (x # xs) =
(if (x ∈ set xs)
then insert x (duplicates xs)
else duplicates xs)"
lemma duplicates_subset:
"duplicates Φ ⊆ set Φ"
by (induct Φ, simp, auto)
lemma duplicates_alt_def:
"duplicates xs = {x. count_list xs x ≥ 2}"
proof (induct xs)
case Nil
then show ?case by simp
next
case (Cons x xs)
assume inductive_hypothesis: "duplicates xs = {x. 2 ≤ count_list xs x}"
then show ?case
proof cases
assume "x ∈ set xs"
hence "count_list (x # xs) x ≥ 2"
by (simp, induct xs, simp, simp, blast)
hence "{y. 2 ≤ count_list (x # xs) y}
= insert x {y. 2 ≤ count_list xs y}"
by (simp, blast)
thus ?thesis using inductive_hypothesis ‹x ∈ set xs›
by simp
next
assume "x ∉ set xs"
hence "{y. 2 ≤ count_list (x # xs) y} = {y. 2 ≤ count_list xs y}"
by (simp, auto)
thus ?thesis using inductive_hypothesis ‹x ∉ set xs›
by simp
qed
qed
section ‹ List Subtraction ›
primrec list_subtract :: "'a list ⇒ 'a list ⇒ 'a list" (infixl "⊖" 70)
where
"xs ⊖ [] = xs"
| "xs ⊖ (y # ys) = (remove1 y (xs ⊖ ys))"
lemma list_subtract_mset_homomorphism [simp]:
"mset (A ⊖ B) = mset A - mset B"
by (induct B, simp, simp)
lemma list_subtract_empty [simp]:
"[] ⊖ Φ = []"
by (induct Φ, simp, simp)
lemma list_subtract_remove1_cons_perm:
"Φ ⊖ (φ # Λ) ⇌ (remove1 φ Φ) ⊖ Λ"
by (induct Λ, simp, simp add: add_mset_commute)
lemma list_subtract_cons:
assumes "φ ∉ set Λ"
shows "(φ # Φ) ⊖ Λ = φ # (Φ ⊖ Λ)"
using assms
by (induct Λ, simp, simp, blast)
lemma list_subtract_cons_absorb:
assumes "count_list Φ φ ≥ count_list Λ φ"
shows "φ # (Φ ⊖ Λ) ⇌ (φ # Φ) ⊖ Λ"
using assms
proof (induct Λ arbitrary: Φ)
case Nil
then show ?case using list_subtract_cons by fastforce
next
case (Cons ψ Λ Φ)
then show ?case
proof cases
assume "φ = ψ"
hence "φ ∈ set Φ"
using Cons.prems count_notin by force
hence "Φ ⇌ φ # (remove1 ψ Φ)"
unfolding ‹φ = ψ›
by force
thus ?thesis using perm_count_list
by (metis
(no_types, lifting)
Cons.hyps
Cons.prems
‹φ = ψ›
add_le_cancel_right
add_mset_diff_bothsides
count_list.simps(2)
list_subtract_mset_homomorphism
mset.simps(2))
next
assume "φ ≠ ψ"
hence "count_list (ψ # Λ) φ = count_list Λ φ"
by simp
moreover have "count_list Φ φ = count_list (remove1 ψ Φ) φ"
proof (induct Φ)
case Nil
then show ?case by simp
next
case (Cons φ' Φ)
show ?case
proof cases
assume "φ' = φ"
with ‹φ ≠ ψ›
have "count_list (φ' # Φ) φ = 1 + count_list Φ φ"
"count_list (remove1 ψ (φ' # Φ)) φ
= 1 + count_list (remove1 ψ Φ) φ"
by simp+
with Cons show ?thesis by linarith
next
assume "φ' ≠ φ"
with Cons show ?thesis by (cases "φ' = ψ", simp+)
qed
qed
ultimately show ?thesis
using ‹count_list (ψ # Λ) φ ≤ count_list Φ φ›
by (metis
Cons.hyps
‹φ ≠ ψ›
list_subtract_remove1_cons_perm
mset.simps(2)
remove1.simps(2))
qed
qed
lemma list_subtract_cons_remove1_perm:
assumes "φ ∈ set Λ"
shows "(φ # Φ) ⊖ Λ ⇌ Φ ⊖ (remove1 φ Λ)"
using assms
by (metis
list_subtract_mset_homomorphism
list_subtract_remove1_cons_perm
perm_remove
remove_hd)
lemma list_subtract_removeAll_perm:
assumes "count_list Φ φ ≤ count_list Λ φ"
shows "Φ ⊖ Λ ⇌ (removeAll φ Φ) ⊖ (removeAll φ Λ)"
using assms
proof (induct Φ arbitrary: Λ)
case Nil
then show ?case by auto
next
case (Cons ξ Φ Λ)
hence "Φ ⊖ Λ ⇌ (removeAll φ Φ) ⊖ (removeAll φ Λ)"
by (metis add_leE count_list.simps(2))
show ?case
proof cases
assume "ξ = φ"
hence "count_list Φ φ < count_list Λ φ"
using ‹count_list (ξ # Φ) φ ≤ count_list Λ φ›
by auto
hence "count_list Φ φ ≤ count_list (remove1 φ Λ) φ"
by (induct Λ, simp, auto)
hence "Φ ⊖ (remove1 φ Λ)
⇌ removeAll φ Φ ⊖ removeAll φ (remove1 φ Λ)"
using Cons.hyps by blast
hence "Φ ⊖ (remove1 φ Λ) ⇌ removeAll φ Φ ⊖ removeAll φ Λ"
by (simp add: filter_remove1 removeAll_filter_not_eq)
moreover have "φ ∈ set Λ" and "φ ∈ set (φ # Φ)"
using ‹ξ = φ›
‹count_list (ξ # Φ) φ ≤ count_list Λ φ›
gr_implies_not0
by fastforce+
hence "(φ # Φ) ⊖ Λ ⇌ (remove1 φ (φ # Φ)) ⊖ (remove1 φ Λ)"
by (metis list_subtract_cons_remove1_perm remove_hd)
hence "(φ # Φ) ⊖ Λ ⇌ Φ ⊖ (remove1 φ Λ)" by simp
ultimately show ?thesis using ‹ξ = φ› by auto
next
assume "ξ ≠ φ"
show ?thesis
proof cases
assume "ξ ∈ set Λ"
hence "(ξ # Φ) ⊖ Λ ⇌ Φ ⊖ remove1 ξ Λ"
by (meson list_subtract_cons_remove1_perm)
moreover have "count_list Λ φ = count_list (remove1 ξ Λ) φ"
by (metis
count_list.simps(2)
‹ξ ≠ φ›
‹ξ ∈ set Λ›
perm_count_list
perm_remove)
hence "count_list Φ φ ≤ count_list (remove1 ξ Λ) φ"
using ‹ξ ≠ φ› ‹count_list (ξ # Φ) φ ≤ count_list Λ φ› by auto
hence "Φ ⊖ remove1 ξ Λ
⇌ (removeAll φ Φ) ⊖ (removeAll φ (remove1 ξ Λ))"
using Cons.hyps by blast
moreover
have "(removeAll φ Φ) ⊖ (removeAll φ (remove1 ξ Λ)) ⇌
(removeAll φ Φ) ⊖ (remove1 ξ (removeAll φ Λ))"
by (induct Λ,
simp,
metis
‹ξ ≠ φ›
list_subtract.simps(2)
mset_remove1
remove1.simps(2)
removeAll.simps(2))
hence "(removeAll φ Φ) ⊖ (removeAll φ (remove1 ξ Λ)) ⇌
(removeAll φ (ξ # Φ)) ⊖ (removeAll φ Λ)"
by (metis
‹ξ ∈ set Λ›
‹ξ ≠ φ›
list_subtract_cons_remove1_perm
member_remove removeAll.simps(2)
remove_code(1))
ultimately show ?thesis
by presburger
next
assume "ξ ∉ set Λ"
hence "(ξ # Φ) ⊖ Λ ⇌ ξ # (Φ ⊖ Λ)"
by fastforce
hence "(ξ # Φ) ⊖ Λ ⇌ ξ # ((removeAll φ Φ) ⊖ (removeAll φ Λ))"
using ‹Φ ⊖ Λ ⇌ removeAll φ Φ ⊖ removeAll φ Λ›
by simp
hence "(ξ # Φ) ⊖ Λ ⇌ (ξ # (removeAll φ Φ)) ⊖ (removeAll φ Λ)"
by (simp add: ‹ξ ∉ set Λ› list_subtract_cons)
thus ?thesis using ‹ξ ≠ φ› by auto
qed
qed
qed
lemma list_subtract_permute:
assumes "Φ ⇌ Ψ"
shows "Φ ⊖ Λ ⇌ Ψ ⊖ Λ"
using assms
by simp
lemma append_perm_list_subtract_intro:
assumes "A ⇌ B @ C"
shows "A ⊖ C ⇌ B"
proof -
from ‹A ⇌ B @ C› have "mset (A ⊖ C) = mset B"
by simp
thus ?thesis by blast
qed
lemma list_subtract_concat:
assumes "Ψ ∈ set ℒ"
shows "concat (ℒ ⊖ [Ψ]) ⇌ (concat ℒ) ⊖ Ψ"
using assms
by (simp add: concat_remove1)
lemma (in comm_monoid_add) listSubstract_multisubset_list_summation:
assumes "mset Ψ ⊆# mset Φ"
shows "(∑ψ←Ψ. f ψ) + (∑φ'←(Φ ⊖ Ψ). f φ') = (∑φ'←Φ. f φ')"
proof -
have "∀ Φ. mset Ψ ⊆# mset Φ
⟶ (∑ψ'←Ψ. f ψ') + (∑φ'←(Φ ⊖ Ψ). f φ') = (∑φ'←Φ. f φ')"
proof(induct Ψ)
case Nil
then show ?case
by simp
next
case (Cons ψ Ψ)
{
fix Φ
assume hypothesis: "mset (ψ # Ψ) ⊆# mset Φ"
hence "mset Ψ ⊆# mset (remove1 ψ Φ)"
by (metis append_Cons mset_le_perm_append perm_remove_perm remove_hd)
hence
"(∑ψ' ← Ψ. f ψ') + (∑φ'←((remove1 ψ Φ) ⊖ Ψ). f φ')
= (∑φ'← (remove1 ψ Φ). f φ')"
using Cons.hyps by blast
moreover have "(remove1 ψ Φ) ⊖ Ψ ⇌ Φ ⊖ (ψ # Ψ)"
by (meson list_subtract_remove1_cons_perm perm_sym)
hence "(∑φ'←((remove1 ψ Φ) ⊖ Ψ). f φ') = (∑φ'←(Φ ⊖ (ψ # Ψ)). f φ')"
using perm_list_summation by blast
ultimately have
"(∑ψ' ← Ψ. f ψ') + (∑φ'←(Φ ⊖ (ψ # Ψ)). f φ')
= (∑φ'← (remove1 ψ Φ). f φ')"
by simp
hence
"(∑ψ' ← (ψ # Ψ). f ψ') + (∑φ'←(Φ ⊖ (ψ # Ψ)). f φ')
= (∑φ'← (ψ # (remove1 ψ Φ)). f φ')"
by (simp add: add.assoc)
moreover have "ψ ∈ set Φ"
by (metis
append_Cons
hypothesis
list.set_intros(1)
mset_le_perm_append
perm_set_eq)
hence "(ψ # (remove1 ψ Φ)) ⇌ Φ"
by auto
hence "(∑φ' ← (ψ # (remove1 ψ Φ)). f φ') = (∑φ'←Φ. f φ')"
using perm_list_summation by blast
ultimately have
"(∑ψ' ← (ψ # Ψ). f ψ') + (∑φ'←(Φ ⊖ (ψ # Ψ)). f φ')
= (∑φ'←Φ. f φ')"
by simp
}
then show ?case
by blast
qed
with assms show ?thesis by blast
qed
lemma list_subtract_set_difference_lower_bound:
"set Γ - set Φ ⊆ set (Γ ⊖ Φ)"
using subset_Diff_insert
by (induct Φ, simp, fastforce)
lemma list_subtract_set_trivial_upper_bound:
"set (Γ ⊖ Φ) ⊆ set Γ"
by (induct Φ,
simp,
simp,
meson
dual_order.trans
set_remove1_subset)
lemma list_subtract_msub_eq:
assumes "mset Φ ⊆# mset Γ"
and "length (Γ ⊖ Φ) = m"
shows "length Γ = m + length Φ"
using assms
proof -
have "∀ Γ. mset Φ ⊆# mset Γ
⟶ length (Γ ⊖ Φ) = m --> length Γ = m + length Φ"
proof (induct Φ)
case Nil
then show ?case by simp
next
case (Cons φ Φ)
{
fix Γ :: "'a list"
assume "mset (φ # Φ) ⊆# mset Γ"
"length (Γ ⊖ (φ # Φ)) = m"
moreover from this have
"mset Φ ⊆# mset (remove1 φ Γ)"
"mset (Γ ⊖ (φ # Φ)) = mset ((remove1 φ Γ) ⊖ Φ)"
by (metis
append_Cons
mset_le_perm_append
perm_remove_perm
remove_hd,
simp)
ultimately have "length (remove1 φ Γ) = m + length Φ"
using Cons.hyps
by (metis mset_eq_length)
hence "length (φ # (remove1 φ Γ)) = m + length (φ # Φ)"
by simp
moreover have "φ ∈ set Γ"
by (metis
‹mset (Γ ⊖ (φ # Φ)) = mset (remove1 φ Γ ⊖ Φ)›
‹mset (φ # Φ) ⊆# mset Γ›
‹mset Φ ⊆# mset (remove1 φ Γ)›
add_diff_cancel_left'
add_right_cancel
eq_iff
impossible_Cons
list_subtract_mset_homomorphism
mset_subset_eq_exists_conv
remove1_idem size_mset)
hence "length (φ # (remove1 φ Γ)) = length Γ"
by (metis
One_nat_def
Suc_pred
length_Cons
length_pos_if_in_set
length_remove1)
ultimately have "length Γ = m + length (φ # Φ)" by simp
}
thus ?case by blast
qed
thus ?thesis using assms by blast
qed
lemma list_subtract_not_member:
assumes "b ∉ set A"
shows "A ⊖ B = A ⊖ (remove1 b B)"
using assms
by (induct B,
simp,
simp,
metis
add_mset_add_single
diff_subset_eq_self
insert_DiffM2
insert_subset_eq_iff
list_subtract_mset_homomorphism
remove1_idem
set_mset_mset)
lemma list_subtract_monotonic:
assumes "mset A ⊆# mset B"
shows "mset (A ⊖ C) ⊆# mset (B ⊖ C)"
by (simp,
meson
assms
subset_eq_diff_conv
subset_mset.dual_order.refl
subset_mset.order_trans)
lemma map_list_subtract_mset_containment:
"mset ((map f A) ⊖ (map f B)) ⊆# mset (map f (A ⊖ B))"
by (induct B, simp, simp,
metis
diff_subset_eq_self
diff_zero
image_mset_add_mset
image_mset_subseteq_mono
image_mset_union
subset_eq_diff_conv
subset_eq_diff_conv)
lemma map_list_subtract_mset_equivalence:
assumes "mset B ⊆# mset A"
shows "mset ((map f A) ⊖ (map f B)) = mset (map f (A ⊖ B))"
using assms
by (induct B, simp, simp add: image_mset_Diff)
lemma msub_list_subtract_elem_cons_msub:
assumes "mset Ξ ⊆# mset Γ"
and "ψ ∈ set (Γ ⊖ Ξ)"
shows "mset (ψ # Ξ) ⊆# mset Γ"
proof -
have "∀ Γ. mset Ξ ⊆# mset Γ
⟶ ψ ∈ set (Γ ⊖ Ξ) --> mset (ψ # Ξ) ⊆# mset Γ"
proof(induct Ξ)
case Nil
then show ?case by simp
next
case (Cons ξ Ξ)
{
fix Γ
assume
"mset (ξ # Ξ) ⊆# mset Γ"
"ψ ∈ set (Γ ⊖ (ξ # Ξ))"
hence
"ξ ∈ set Γ"
"mset Ξ ⊆# mset (remove1 ξ Γ)"
"ψ ∈ set ((remove1 ξ Γ) ⊖ Ξ)"
by (simp,
metis
ex_mset
list.set_intros(1)
mset.simps(2)
mset_eq_setD
subset_mset.le_iff_add
union_mset_add_mset_left,
metis
list_subtract.simps(1)
list_subtract.simps(2)
list_subtract_monotonic
remove_hd,
simp,
metis
list_subtract_remove1_cons_perm
perm_set_eq)
with Cons.hyps have
"mset Γ = mset (ξ # (remove1 ξ Γ))"
"mset (ψ # Ξ) ⊆# mset (remove1 ξ Γ)"
by (simp, blast)
hence "mset (ψ # ξ # Ξ) ⊆# mset Γ"
by (simp,
metis
add_mset_commute
mset_subset_eq_add_mset_cancel)
}
then show ?case by auto
qed
thus ?thesis using assms by blast
qed
section ‹ Tuple Lists ›
lemma remove1_pairs_list_projections_fst:
assumes "(γ,σ) ∈# mset Φ"
shows "mset (map fst (remove1 (γ, σ) Φ)) = mset (map fst Φ) - {# γ #}"
using assms
proof (induct Φ)
case Nil
then show ?case by simp
next
case (Cons φ Φ)
assume "(γ, σ) ∈# mset (φ # Φ)"
show ?case
proof (cases "φ = (γ, σ)")
assume "φ = (γ, σ)"
then show ?thesis by simp
next
assume "φ ≠ (γ, σ)"
then have "add_mset φ (mset Φ - {#(γ, σ)#})
= add_mset φ (mset Φ) - {#(γ, σ)#}"
by force
then have "add_mset (fst φ) (image_mset fst (mset Φ - {#(γ, σ)#}))
= add_mset (fst φ) (image_mset fst (mset Φ)) - {#γ#}"
by (metis (no_types) Cons.prems
add_mset_remove_trivial
fst_conv
image_mset_add_mset
insert_DiffM mset.simps(2))
with ‹φ ≠ (γ, σ)› show ?thesis
by simp
qed
qed
lemma remove1_pairs_list_projections_snd:
assumes "(γ,σ) ∈# mset Φ"
shows "mset (map snd (remove1 (γ, σ) Φ)) = mset (map snd Φ) - {# σ #}"
using assms
proof (induct Φ)
case Nil
then show ?case by simp
next
case (Cons φ Φ)
assume "(γ, σ) ∈# mset (φ # Φ)"
show ?case
proof (cases "φ = (γ, σ)")
assume "φ = (γ, σ)"
then show ?thesis by simp
next
assume "φ ≠ (γ, σ)"
then have "add_mset (snd φ) (image_mset snd (mset Φ - {#(γ, σ)#}))
= image_mset snd (mset (φ # Φ) - {#(γ, σ)#})"
by auto
moreover have "add_mset (snd φ) (image_mset snd (mset Φ))
= add_mset σ (image_mset snd (mset (φ # Φ) - {#(γ, σ)#}))"
by (metis (no_types)
Cons.prems
image_mset_add_mset
insert_DiffM
mset.simps(2)
snd_conv)
ultimately
have "add_mset (snd φ) (image_mset snd (mset Φ - {#(γ, σ)#}))
= add_mset (snd φ) (image_mset snd (mset Φ)) - {#σ#}"
by simp
with ‹φ ≠ (γ, σ)› show ?thesis
by simp
qed
qed
lemma triple_list_exists:
assumes "mset (map snd Ψ) ⊆# mset Σ"
and "mset Σ ⊆# mset (map snd Δ)"
shows "∃ Ω. map (λ (ψ, σ, _). (ψ, σ)) Ω = Ψ ∧
mset (map (λ (_, σ, γ). (γ, σ)) Ω) ⊆# mset Δ"
using assms(1)
proof (induct Ψ)
case Nil
then show ?case by fastforce
next
case (Cons ψ Ψ)
from Cons obtain Ω where Ω:
"map (λ (ψ, σ, _). (ψ, σ)) Ω = Ψ"
"mset (map (λ (_, σ, γ). (γ, σ)) Ω) ⊆# mset Δ"
by (metis
(no_types, lifting)
diff_subset_eq_self
list.set_intros(1)
remove1_pairs_list_projections_snd
remove_hd
set_mset_mset
subset_mset.dual_order.trans
surjective_pairing)
let ?Δ⇩Ω = "map (λ (_, σ, γ). (γ, σ)) Ω"
let ?ψ = "fst ψ"
let ?σ = "snd ψ"
from Cons.prems have "add_mset ?σ (image_mset snd (mset Ψ)) ⊆# mset Σ"
by simp
then have "mset Σ - {#?σ#} - image_mset snd (mset Ψ)
≠ mset Σ - image_mset snd (mset Ψ)"
by (metis
(no_types)
insert_subset_eq_iff
mset_subset_eq_insertD
multi_drop_mem_not_eq
subset_mset.diff_add
subset_mset_def)
hence "?σ ∈# mset Σ - mset (map snd Ψ)"
using diff_single_trivial by fastforce
have "mset (map snd (ψ # Ψ)) ⊆# mset (map snd Δ)"
by (meson
Cons.prems
‹mset Σ ⊆# mset (map snd Δ)›
subset_mset.dual_order.trans)
then have
"mset (map snd Δ) - mset (map snd (ψ # Ψ)) + ({#} + {#snd ψ#})
= mset (map snd Δ) + ({#} + {#snd ψ#})
- add_mset (snd ψ) (mset (map snd Ψ))"
by (metis
(no_types)
list.simps(9)
mset.simps(2)
mset_subset_eq_multiset_union_diff_commute)
then have
"mset (map snd Δ) - mset (map snd (ψ # Ψ)) + ({#} + {#snd ψ#})
= mset (map snd Δ) - mset (map snd Ψ)"
by auto
hence "?σ ∈# mset (map snd Δ) - mset (map snd Ψ)"
using add_mset_remove_trivial_eq by fastforce
moreover have "snd ∘ (λ (ψ, σ, _). (ψ, σ)) = snd ∘ (λ (_, σ, γ). (γ, σ))"
by auto
hence "map snd (?Δ⇩Ω) = map snd (map (λ (ψ, σ, _). (ψ, σ)) Ω)"
by fastforce
hence "map snd (?Δ⇩Ω) = map snd Ψ"
using Ω(1) by simp
ultimately have "?σ ∈# mset (map snd Δ) - mset (map snd ?Δ⇩Ω)"
by simp
hence "?σ ∈# image_mset snd (mset Δ - mset ?Δ⇩Ω)"
using Ω(2) by (metis image_mset_Diff mset_map)
hence "?σ ∈ snd ` set_mset (mset Δ - mset ?Δ⇩Ω)"
by (metis in_image_mset)
from this obtain ρ where ρ:
"snd ρ = ?σ" "ρ ∈# mset Δ - mset ?Δ⇩Ω"
using imageE by auto
from this obtain γ where
"(γ, ?σ) = ρ"
by (metis prod.collapse)
with ρ(2) have γ: "(γ, ?σ) ∈# mset Δ - mset ?Δ⇩Ω" by auto
let ?Ω = "(?ψ, ?σ, γ) # Ω"
have "map (λ (ψ, σ, _). (ψ, σ)) ?Ω = ψ # Ψ"
using Ω(1) by simp
moreover
have A: "(γ, snd ψ) = (case (snd ψ, γ) of (a, c) ⇒ (c, a))"
by auto
have B: "mset (map (λ(b, a, c). (c, a)) Ω)
+ {# case (snd ψ, γ) of (a, c) ⇒ (c, a) #}
= mset (map (λ(b, a, c). (c, a)) ((fst ψ, snd ψ, γ) # Ω))"
by simp
obtain mm
:: "('c × 'a) multiset
⇒ ('c × 'a) multiset
⇒ ('c × 'a) multiset"
where "∀x0 x1. (∃v2. x0 = x1 + v2) = (x0 = x1 + mm x0 x1)"
by moura
then have "mset Δ = mset (map (λ(b, a, c). (c, a)) Ω)
+ mm (mset Δ) (mset (map (λ(b, a, c). (c, a)) Ω))"
by (metis Ω(2) subset_mset.le_iff_add)
then have "mset (map (λ (_, σ, γ). (γ, σ)) ?Ω) ⊆# mset Δ"
using A B by
(metis
γ
add_diff_cancel_left'
single_subset_iff
subset_mset.add_le_cancel_left)
ultimately show ?case by meson
qed
section ‹ List Intersection ›
primrec list_intersect :: "'a list => 'a list => 'a list" (infixl "❙∩" 60)
where
"_ ❙∩ [] = []"
| "xs ❙∩ (y # ys) =
(if (y ∈ set xs)
then (y # (remove1 y xs ❙∩ ys))
else (xs ❙∩ ys))"
lemma list_intersect_mset_homomorphism [simp]:
"mset (Φ ❙∩ Ψ) = mset Φ ∩# mset Ψ"
proof -
have "∀ Φ. mset (Φ ❙∩ Ψ) = mset Φ ∩# mset Ψ"
proof (induct Ψ)
case Nil
then show ?case by simp
next
case (Cons ψ Ψ)
{
fix Φ
have "mset (Φ ❙∩ ψ # Ψ) = mset Φ ∩# mset (ψ # Ψ)"
using Cons.hyps
by (cases "ψ ∈ set Φ",
simp add: inter_add_right2,
simp add: inter_add_right1)
}
then show ?case by blast
qed
thus ?thesis by simp
qed
lemma list_intersect_left_empty [simp]: "[] ❙∩ Φ = []" by (induct Φ, simp+)
lemma list_diff_intersect_comp:
"mset Φ = mset (Φ ⊖ Ψ) + mset (Φ ❙∩ Ψ)"
by (metis
diff_intersect_left_idem
list_intersect_mset_homomorphism
list_subtract_mset_homomorphism
subset_mset.inf_le1
subset_mset.le_imp_diff_is_add)
lemma list_intersect_left_project: "mset (Φ ❙∩ Ψ) ⊆# mset Φ"
by simp
lemma list_intersect_right_project: "mset (Φ ❙∩ Ψ) ⊆# mset Ψ"
by simp
end