Theory MoreList
section‹MoreList›
theory MoreList
imports Main "HOL-Library.Multiset"
begin
text‹Theory contains some additional lemmas and functions for the
@{term List} datatype. Warning: some of these notions are obsolete
because they already exist in {\em List.thy} in similiar form.›
subsection‹@{term "last"} and @{term "butlast"} - last element of list and elements before it›
lemma listEqualsButlastAppendLast:
assumes "list ≠ []"
shows "list = (butlast list) @ [last list]"
using assms
by (induct list) auto
lemma lastListInList [simp]:
assumes "list ≠ []"
shows "last list ∈ set list"
using assms
by (induct list) auto
lemma butlastIsSubset:
shows "set (butlast list) ⊆ set list"
by (induct list) (auto split: if_split_asm)
lemma setListIsSetButlastAndLast:
shows "set list ⊆ set (butlast list) ∪ {last list}"
by (induct list) auto
lemma butlastAppend:
shows "butlast (list1 @ list2) = (if list2 = [] then butlast list1 else (list1 @ butlast list2))"
by (induct list1) auto
subsection‹@{term removeAll} - element removal›
lemma removeAll_multiset:
assumes "distinct a" "x ∈ set a"
shows "mset a = {#x#} + mset (removeAll x a)"
using assms
proof (induct a)
case (Cons y a')
thus ?case
proof (cases "x = y")
case True
with ‹distinct (y # a')› ‹x ∈ set (y # a')›
have "¬ x ∈ set a'"
by auto
hence "removeAll x a' = a'"
by (rule removeAll_id)
with ‹x = y› show ?thesis
by (simp add: union_commute)
next
case False
with ‹x ∈ set (y # a')›
have "x ∈ set a'"
by simp
with ‹distinct (y # a')›
have "x ≠ y" "distinct a'"
by auto
hence "mset a' = {#x#} + mset (removeAll x a')"
using ‹x ∈ set a'›
using Cons(1)
by simp
thus ?thesis
using ‹x ≠ y›
by (simp add: union_assoc)
qed
qed simp
lemma removeAll_map:
assumes "∀ x y. x ≠ y ⟶ f x ≠ f y"
shows "removeAll (f x) (map f a) = map f (removeAll x a)"
using assms
by (induct a arbitrary: x) auto
subsection‹@{term uniq} - no duplicate elements.›
text‹@{term "(uniq list)"} holds iff there are no repeated elements
in a list. Obsolete: same as @{term "distinct"} in {\em List.thy}.›
primrec uniq :: "'a list => bool"
where
"uniq [] = True" |
"uniq (h#t) = (h ∉ set t ∧ uniq t)"
lemma uniqDistinct:
"uniq l = distinct l"
by (induct l) auto
lemma uniqAppend:
assumes "uniq (l1 @ l2)"
shows "uniq l1" "uniq l2"
using assms
by (induct l1) auto
lemma uniqAppendIff:
"uniq (l1 @ l2) = (uniq l1 ∧ uniq l2 ∧ set l1 ∩ set l2 = {})" (is "?lhs = ?rhs")
by (induct l1) auto
lemma uniqAppendElement:
assumes "uniq l"
shows "e ∉ set l = uniq (l @ [e])"
using assms
by (induct l) (auto split: if_split_asm)
lemma uniqImpliesNotLastMemButlast:
assumes "uniq l"
shows "last l ∉ set (butlast l)"
proof (cases "l = []")
case True
thus ?thesis
using assms
by simp
next
case False
hence "l = butlast l @ [last l]"
by (rule listEqualsButlastAppendLast)
moreover
with ‹uniq l›
have "uniq (butlast l)"
using uniqAppend[of "butlast l" "[last l]"]
by simp
ultimately
show ?thesis
using assms
using uniqAppendElement[of "butlast l" "last l"]
by simp
qed
lemma uniqButlastNotUniqListImpliesLastMemButlast:
assumes "uniq (butlast l)" "¬ uniq l"
shows "last l ∈ set (butlast l)"
proof (cases "l = []")
case True
thus ?thesis
using assms
by auto
next
case False
hence "l = butlast l @ [(last l)]"
by (rule listEqualsButlastAppendLast)
thus ?thesis
using assms
using uniqAppendElement[of "butlast l" "last l"]
by auto
qed
lemma uniqRemdups:
shows "uniq (remdups x)"
by (induct x) auto
lemma uniqHeadTailSet:
assumes "uniq l"
shows "set (tl l) = (set l) - {hd l}"
using assms
by (induct l) auto
lemma uniqLengthEqCardSet:
assumes "uniq l"
shows "length l = card (set l)"
using assms
by (induct l) auto
lemma lengthGtOneTwoDistinctElements:
assumes
"uniq l" "length l > 1" "l ≠ []"
shows
"∃ a1 a2. a1 ∈ set l ∧ a2 ∈ set l ∧ a1 ≠ a2"
proof-
let ?a1 = "l ! 0"
let ?a2 = "l ! 1"
have "?a1 ∈ set l"
using nth_mem[of "0" "l"]
using assms
by simp
moreover
have "?a2 ∈ set l"
using nth_mem[of "1" "l"]
using assms
by simp
moreover
have "?a1 ≠ ?a2"
using nth_eq_iff_index_eq[of "l" "0" "1"]
using assms
by (auto simp add: uniqDistinct)
ultimately
show ?thesis
by auto
qed
subsection ‹@{term firstPos} - first position of an element›
text‹@{term "firstPos"} returns the zero-based index of the first
occurrence of an element int a list, or the length of the list if the
element does not occur.›
primrec firstPos :: "'a => 'a list => nat"
where
"firstPos a [] = 0" |
"firstPos a (h # t) = (if a = h then 0 else 1 + (firstPos a t))"
lemma firstPosEqualZero:
shows "(firstPos a (m # M') = 0) = (a = m)"
by (induct M') auto
lemma firstPosLeLength:
assumes "a ∈ set l"
shows "firstPos a l < length l"
using assms
by (induct l) auto
lemma firstPosAppend:
assumes "a ∈ set l"
shows "firstPos a l = firstPos a (l @ l')"
using assms
by (induct l) auto
lemma firstPosAppendNonMemberFirstMemberSecond:
assumes "a ∉ set l1" and "a ∈ set l2"
shows "firstPos a (l1 @ l2) = length l1 + firstPos a l2"
using assms
by (induct l1) auto
lemma firstPosDomainForElements:
shows "(0 ≤ firstPos a l ∧ firstPos a l < length l) = (a ∈ set l)" (is "?lhs = ?rhs")
by (induct l) auto
lemma firstPosEqual:
assumes "a ∈ set l" and "b ∈ set l"
shows "(firstPos a l = firstPos b l) = (a = b)" (is "?lhs = ?rhs")
proof-
{
assume "?lhs"
hence "?rhs"
using assms
proof (induct l)
case (Cons m l')
{
assume "a = m"
have "b = m"
proof-
from ‹a = m›
have "firstPos a (m # l') = 0"
by simp
with Cons
have "firstPos b (m # l') = 0"
by simp
with ‹b ∈ set (m # l')›
have "firstPos b (m # l') = 0"
by simp
thus ?thesis
using firstPosEqualZero[of "b" "m" "l'"]
by simp
qed
with ‹a = m›
have ?case
by simp
}
note * = this
moreover
{
assume "b = m"
have "a = m"
proof-
from ‹b = m›
have "firstPos b (m # l') = 0"
by simp
with Cons
have "firstPos a (m # l') = 0"
by simp
with ‹a ∈ set (m # l')›
have "firstPos a (m # l') = 0"
by simp
thus ?thesis
using firstPosEqualZero[of "a" "m" "l'"]
by simp
qed
with ‹b = m›
have ?case
by simp
}
note ** = this
moreover
{
assume Q: "a ≠ m" "b ≠ m"
from Q ‹a ∈ set (m # l')›
have "a ∈ set l'"
by simp
from Q ‹b ∈ set (m # l')›
have "b ∈ set l'"
by simp
from ‹a ∈ set l'› ‹b ∈ set l'› Cons
have "firstPos a l' = firstPos b l'"
by (simp split: if_split_asm)
with Cons
have ?case
by (simp split: if_split_asm)
}
note *** = this
moreover
{
have "a = m ∨ b = m ∨ a ≠ m ∧ b ≠ m"
by auto
}
ultimately
show ?thesis
proof (cases "a = m")
case True
thus ?thesis
by (rule *)
next
case False
thus ?thesis
proof (cases "b = m")
case True
thus ?thesis
by (rule **)
next
case False
with ‹a ≠ m› show ?thesis
by (rule ***)
qed
qed
qed simp
} thus ?thesis
by auto
qed
lemma firstPosLast:
assumes "l ≠ []" "uniq l"
shows "(firstPos x l = length l - 1) = (x = last l)"
using assms
by (induct l) auto
subsection‹@{term precedes} - ordering relation induced by @{term firstPos}›
definition precedes :: "'a => 'a => 'a list => bool"
where
"precedes a b l == (a ∈ set l ∧ b ∈ set l ∧ firstPos a l <= firstPos b l)"
lemma noElementsPrecedesFirstElement:
assumes "a ≠ b"
shows "¬ precedes a b (b # list)"
proof-
{
assume "precedes a b (b # list)"
hence "a ∈ set (b # list)" "firstPos a (b # list) <= 0"
unfolding precedes_def
by (auto split: if_split_asm)
hence "firstPos a (b # list) = 0"
by auto
with ‹a ≠ b›
have False
using firstPosEqualZero[of "a" "b" "list"]
by simp
}
thus ?thesis
by auto
qed
lemma lastPrecedesNoElement:
assumes "uniq l"
shows "¬(∃ a. a ≠ last l ∧ precedes (last l) a l)"
proof-
{
assume "¬ ?thesis"
then obtain "a"
where "precedes (last l) a l" "a ≠ last l"
by auto
hence "a ∈ set l" "last l ∈ set l" "firstPos (last l) l ≤ firstPos a l"
unfolding precedes_def
by auto
hence "length l - 1 ≤ firstPos a l"
using firstPosLast[of "l" "last l"]
using ‹uniq l›
by force
hence "firstPos a l = length l - 1"
using firstPosDomainForElements[of "a" "l"]
using ‹a ∈ set l›
by auto
hence "a = last l"
using firstPosLast[of "l" "last l"]
using ‹a ∈ set l› ‹last l ∈ set l›
using ‹uniq l›
using firstPosEqual[of "a" "l" "last l"]
by force
with ‹a ≠ last l›
have False
by simp
}
thus ?thesis
by auto
qed
lemma precedesAppend:
assumes "precedes a b l"
shows "precedes a b (l @ l')"
proof-
from ‹precedes a b l›
have "a ∈ set l" "b ∈ set l" "firstPos a l ≤ firstPos b l"
unfolding precedes_def
by (auto split: if_split_asm)
thus ?thesis
using firstPosAppend[of "a" "l" "l'"]
using firstPosAppend[of "b" "l" "l'"]
unfolding precedes_def
by simp
qed
lemma precedesMemberHeadMemberTail:
assumes "a ∈ set l1" and "b ∉ set l1" and "b ∈ set l2"
shows "precedes a b (l1 @ l2)"
proof-
from ‹a ∈ set l1›
have "firstPos a l1 < length l1"
using firstPosLeLength [of "a" "l1"]
by simp
moreover
from ‹a ∈ set l1›
have "firstPos a (l1 @ l2) = firstPos a l1"
using firstPosAppend[of "a" "l1" "l2"]
by simp
moreover
from ‹b ∉ set l1› ‹b ∈ set l2›
have "firstPos b (l1 @ l2) = length l1 + firstPos b l2"
by (rule firstPosAppendNonMemberFirstMemberSecond)
moreover
have "firstPos b l2 ≥ 0"
by auto
ultimately
show ?thesis
unfolding precedes_def
using ‹a ∈ set l1› ‹b ∈ set l2›
by simp
qed
lemma precedesReflexivity:
assumes "a ∈ set l"
shows "precedes a a l"
using assms
unfolding precedes_def
by simp
lemma precedesTransitivity:
assumes
"precedes a b l" and "precedes b c l"
shows
"precedes a c l"
using assms
unfolding precedes_def
by auto
lemma precedesAntisymmetry:
assumes
"a ∈ set l" and "b ∈ set l" and
"precedes a b l" and "precedes b a l"
shows
"a = b"
proof-
from assms
have "firstPos a l = firstPos b l"
unfolding precedes_def
by auto
thus ?thesis
using firstPosEqual[of "a" "l" "b"]
using assms
by simp
qed
lemma precedesTotalOrder:
assumes "a ∈ set l" and "b ∈ set l"
shows "a=b ∨ precedes a b l ∨ precedes b a l"
using assms
unfolding precedes_def
by auto
lemma precedesMap:
assumes "precedes a b list" and "∀ x y. x ≠ y ⟶ f x ≠ f y"
shows "precedes (f a) (f b) (map f list)"
using assms
proof (induct list)
case (Cons l list')
{
assume "a = l"
have ?case
proof-
from ‹a = l›
have "firstPos (f a) (map f (l # list')) = 0"
using firstPosEqualZero[of "f a" "f l" "map f list'"]
by simp
moreover
from ‹precedes a b (l # list')›
have "b ∈ set (l # list')"
unfolding precedes_def
by simp
hence "f b ∈ set (map f (l # list'))"
by auto
moreover
hence "firstPos (f b) (map f (l # list')) ≥ 0"
by auto
ultimately
show ?thesis
using ‹a = l› ‹f b ∈ set (map f (l # list'))›
unfolding precedes_def
by simp
qed
}
moreover
{
assume "b = l"
with ‹precedes a b (l # list')›
have "a = l"
using noElementsPrecedesFirstElement[of "a" "l" "list'"]
by auto
from ‹a = l› ‹b = l›
have ?case
unfolding precedes_def
by simp
}
moreover
{
assume "a ≠ l" "b ≠ l"
with ‹∀ x y. x ≠ y ⟶ f x ≠ f y›
have "f a ≠ f l" "f b ≠ f l"
by auto
from ‹precedes a b (l # list')›
have "b ∈ set(l # list')" "a ∈ set(l # list')" "firstPos a (l # list') ≤ firstPos b (l # list')"
unfolding precedes_def
by auto
with ‹a ≠ l› ‹b ≠ l›
have "a ∈ set list'" "b ∈ set list'" "firstPos a list' ≤ firstPos b list'"
by auto
hence "precedes a b list'"
unfolding precedes_def
by simp
with Cons
have "precedes (f a) (f b) (map f list')"
by simp
with ‹f a ≠ f l› ‹f b ≠ f l›
have ?case
unfolding precedes_def
by auto
}
ultimately
show ?case
by auto
next
case Nil
thus ?case
unfolding precedes_def
by simp
qed
lemma precedesFilter:
assumes "precedes a b list" and "f a" and "f b"
shows "precedes a b (filter f list)"
using assms
proof(induct list)
case (Cons l list')
show ?case
proof-
from ‹precedes a b (l # list')›
have "a ∈ set(l # list')" "b ∈ set(l # list')" "firstPos a (l # list') ≤ firstPos b (l # list')"
unfolding precedes_def
by auto
from ‹f a› ‹a ∈ set(l # list')›
have "a ∈ set(filter f (l # list'))"
by auto
moreover
from ‹f b› ‹b ∈ set(l # list')›
have "b ∈ set(filter f (l # list'))"
by auto
moreover
have "firstPos a (filter f (l # list')) ≤ firstPos b (filter f (l # list'))"
proof-
{
assume "a = l"
with ‹f a›
have "firstPos a (filter f (l # list')) = 0"
by auto
with ‹b ∈ set (filter f (l # list'))›
have ?thesis
by auto
}
moreover
{
assume "b = l"
with ‹precedes a b (l # list')›
have "a = b"
using noElementsPrecedesFirstElement[of "a" "b" "list'"]
by auto
hence ?thesis
by (simp add: precedesReflexivity)
}
moreover
{
assume "a ≠ l" "b ≠ l"
with ‹precedes a b (l # list')›
have "firstPos a list' ≤ firstPos b list'"
unfolding precedes_def
by auto
moreover
from ‹a ≠ l› ‹a ∈ set (l # list')›
have "a ∈ set list'"
by simp
moreover
from ‹b ≠ l› ‹b ∈ set (l # list')›
have "b ∈ set list'"
by simp
ultimately
have "precedes a b list'"
unfolding precedes_def
by simp
with ‹f a› ‹f b› Cons(1)
have "precedes a b (filter f list')"
by simp
with ‹a ≠ l› ‹b ≠ l›
have ?thesis
unfolding precedes_def
by auto
}
ultimately
show ?thesis
by blast
qed
ultimately
show ?thesis
unfolding precedes_def
by simp
qed
qed simp
definition
"precedesOrder list == {(a, b). precedes a b list ∧ a ≠ b}"
lemma transPrecedesOrder:
"trans (precedesOrder list)"
proof-
{
fix x y z
assume "precedes x y list" "x ≠ y" "precedes y z list" "y ≠ z"
hence "precedes x z list" "x ≠ z"
using precedesTransitivity[of "x" "y" "list" "z"]
using firstPosEqual[of "y" "list" "z"]
unfolding precedes_def
by auto
}
thus ?thesis
unfolding trans_def
unfolding precedesOrder_def
by blast
qed
lemma wellFoundedPrecedesOrder:
shows "wf (precedesOrder list)"
unfolding wf_eq_minimal
proof-
show "∀Q a. a:Q ⟶ (∃ aMin ∈ Q. ∀ a'. (a', aMin) ∈ precedesOrder list ⟶ a' ∉ Q)"
proof-
{
fix a :: "'a" and Q::"'a set"
assume "a ∈ Q"
let ?listQ = "filter (λ x. x ∈ Q) list"
have "∃ aMin ∈ Q. ∀ a'. (a', aMin) ∈ precedesOrder list ⟶ a' ∉ Q"
proof (cases "?listQ = []")
case True
let ?aMin = a
have "∀ a'. (a', ?aMin) ∈ precedesOrder list ⟶ a' ∉ Q"
proof-
{
fix a'
assume "(a', ?aMin) ∈ precedesOrder list"
hence "a ∈ set list"
unfolding precedesOrder_def
unfolding precedes_def
by simp
with ‹a ∈ Q›
have "a ∈ set ?listQ"
by (induct list) auto
with ‹?listQ = []›
have "False"
by simp
hence "a' ∉ Q"
by simp
}
thus ?thesis
by simp
qed
with ‹a ∈ Q› obtain aMin where "aMin ∈ Q" "∀ a'. (a', aMin) ∈ precedesOrder list ⟶ a' ∉ Q"
by auto
thus ?thesis
by auto
next
case False
let ?aMin = "hd ?listQ"
from False
have "?aMin ∈ Q"
by (induct list) auto
have "∀ a'. (a', ?aMin) ∈ precedesOrder list ⟶ a' ∉ Q"
proof
fix a'
{
assume "(a', ?aMin) ∈ precedesOrder list"
hence "a' ∈ set list" "precedes a' ?aMin list" "a' ≠ ?aMin"
unfolding precedesOrder_def
unfolding precedes_def
by auto
have "a' ∉ Q"
proof-
{
assume "a' ∈ Q"
with ‹?aMin ∈ Q› ‹precedes a' ?aMin list›
have "precedes a' ?aMin ?listQ"
using precedesFilter[of "a'" "?aMin" "list" "λ x. x ∈ Q"]
by blast
from ‹a' ≠ ?aMin›
have "¬ precedes a' (hd ?listQ) (hd ?listQ # tl ?listQ)"
by (rule noElementsPrecedesFirstElement)
with False ‹precedes a' ?aMin ?listQ›
have "False"
by auto
}
thus ?thesis
by auto
qed
} thus "(a', ?aMin) ∈ precedesOrder list ⟶ a' ∉ Q"
by simp
qed
with ‹?aMin ∈ Q›
show ?thesis
..
qed
}
thus ?thesis
by simp
qed
qed
subsection‹@{term isPrefix} - prefixes of list.›
text‹Check if a list is a prefix of another list. Obsolete: similiar
notion is defined in {\em List\_prefixes.thy}.›
definition
isPrefix :: "'a list => 'a list => bool"
where "isPrefix p t = (∃ s. p @ s = t)"
lemma prefixIsSubset:
assumes "isPrefix p l"
shows "set p ⊆ set l"
using assms
unfolding isPrefix_def
by auto
lemma uniqListImpliesUniqPrefix:
assumes "isPrefix p l" and "uniq l"
shows "uniq p"
proof-
from ‹isPrefix p l› obtain s
where "p @ s = l"
unfolding isPrefix_def
by auto
with ‹uniq l›
show ?thesis
using uniqAppend[of "p" "s"]
by simp
qed
lemma firstPosPrefixElement:
assumes "isPrefix p l" and "a ∈ set p"
shows "firstPos a p = firstPos a l"
proof-
from ‹isPrefix p l› obtain s
where "p @ s = l"
unfolding isPrefix_def
by auto
with ‹a ∈ set p›
show ?thesis
using firstPosAppend[of "a" "p" "s"]
by simp
qed
lemma laterInPrefixRetainsPrecedes:
assumes
"isPrefix p l" and "precedes a b l" and "b ∈ set p"
shows
"precedes a b p"
proof-
from ‹isPrefix p l› obtain s
where "p @ s = l"
unfolding isPrefix_def
by auto
from ‹precedes a b l›
have "a ∈ set l" "b ∈ set l" "firstPos a l ≤ firstPos b l"
unfolding precedes_def
by (auto split: if_split_asm)
from ‹p @ s = l› ‹b ∈ set p›
have "firstPos b l = firstPos b p"
using firstPosAppend [of "b" "p" "s"]
by simp
show ?thesis
proof (cases "a ∈ set p")
case True
from ‹p @ s = l› ‹a ∈ set p›
have "firstPos a l = firstPos a p"
using firstPosAppend [of "a" "p" "s"]
by simp
from ‹firstPos a l = firstPos a p› ‹firstPos b l = firstPos b p› ‹firstPos a l ≤ firstPos b l›
‹a ∈ set p› ‹b ∈ set p›
show ?thesis
unfolding precedes_def
by simp
next
case False
from ‹a ∉ set p› ‹a ∈ set l› ‹p @ s = l›
have "a ∈ set s"
by auto
with ‹a ∉ set p› ‹p @ s = l›
have "firstPos a l = length p + firstPos a s"
using firstPosAppendNonMemberFirstMemberSecond[of "a" "p" "s"]
by simp
moreover
from ‹b ∈ set p›
have "firstPos b p < length p"
by (rule firstPosLeLength)
ultimately
show ?thesis
using ‹firstPos b l = firstPos b p› ‹firstPos a l ≤ firstPos b l›
by simp
qed
qed
subsection‹@{term "minus_list_set"} - the set difference operation on two lists.›
lemma listDiffIff:
shows "(x ∈ set a ∧ x ∉ set b) = (x ∈ set (minus_list_set a b))"
by (induct a) auto
lemma listDiffDoubleRemoveAll:
assumes "x ∈ set a"
shows "minus_list_set b a = minus_list_set b (x # a)"
using assms
by (induct b) auto
lemma removeAllListDiff[simp]:
shows "removeAll x (minus_list_set a b) = minus_list_set (removeAll x a) b"
by (induct a) (auto simp add: minus_list_set_Cons1)
lemma listDiffRemoveAllNonMember:
assumes "x ∉ set a"
shows "minus_list_set a b = minus_list_set a (removeAll x b)"
using assms
proof (induct b arbitrary: a)
case (Cons y b')
from ‹x ∉ set a›
have "x ∉ set (removeAll y a)"
by auto
thus ?case
proof (cases "x = y")
case False
thus ?thesis
using Cons(2)
using Cons(1)[of "removeAll y a"]
using ‹x ∉ set (removeAll y a)›
by auto
next
case True
thus ?thesis
using Cons(1)[of "removeAll y a"]
using ‹x ∉ set a›
using ‹x ∉ set (removeAll y a)›
by auto
qed
qed simp
lemma listDiffMap:
assumes "∀ x y. x ≠ y ⟶ f x ≠ f y"
shows "map f (minus_list_set a b) = minus_list_set (map f a) (map f b)"
using assms
by (induct b arbitrary: a) (auto simp add: removeAll_map)
subsection‹@{term remdups} - removing duplicates›
lemma remdupsRemoveAllCommute[simp]:
shows "remdups (removeAll a list) = removeAll a (remdups list)"
by (induct list) auto
lemma remdupsAppend:
shows "remdups (a @ b) = remdups (minus_list_set a b) @ remdups b"
proof (induct a)
case (Cons x a')
thus ?case
using listDiffIff[of "x" "a'" "b"]
by (auto simp: minus_list_set_Cons1)
qed simp
lemma remdupsAppendSet:
shows "set (remdups (a @ b)) = set (remdups a @ remdups (minus_list_set b a))"
by simp
lemma remdupsAppendMultiSet:
shows "mset (remdups (a @ b)) = mset (remdups a @ remdups (minus_list_set b a))"
by (metis Diff_disjoint distinct_append distinct_remdups mset_set_set remdupsAppendSet
set_minus_list_set set_remdups)
lemma remdupsListDiff:
"remdups (minus_list_set a b) = minus_list_set (remdups a) (remdups b)"
by (simp add: minus_list_set_eq_filter remdups_filter)
definition
"multiset_le a b r == a = b ∨ (a, b) ∈ mult r"
lemma multisetEmptyLeI:
"multiset_le {#} a r"
unfolding multiset_le_def
using one_step_implies_mult[of "a" "{#}" r "{#}"]
by auto
lemma multisetUnionLessMono2:
shows
"trans r ⟹ (b1, b2) ∈ mult r ⟹ (a + b1, a + b2) ∈ mult r"
unfolding mult_def
apply (erule trancl_induct)
apply (blast intro: mult1_union transI)
apply (blast intro: mult1_union transI trancl_trans)
done
lemma multisetUnionLessMono1:
shows
"trans r ⟹ (a1, a2) ∈ mult r ⟹ (a1 + b, a2 + b) ∈ mult r"
by (metis multisetUnionLessMono2 union_commute)
lemma multisetUnionLeMono2:
assumes
"trans r"
"multiset_le b1 b2 r"
shows
"multiset_le (a + b1) (a + b2) r"
using assms
unfolding multiset_le_def
using multisetUnionLessMono2[of "r" "b1" "b2" "a"]
by auto
lemma multisetUnionLeMono1:
assumes
"trans r"
"multiset_le a1 a2 r"
shows
"multiset_le (a1 + b) (a2 + b) r"
using assms
unfolding multiset_le_def
using multisetUnionLessMono1[of "r" "a1" "a2" "b"]
by auto
lemma multisetLeTrans:
assumes
"trans r"
"multiset_le x y r"
"multiset_le y z r"
shows
"multiset_le x z r"
using assms
unfolding multiset_le_def
unfolding mult_def
by (blast intro: trancl_trans)
lemma multisetUnionLeMono:
assumes
"trans r"
"multiset_le a1 a2 r"
"multiset_le b1 b2 r"
shows
"multiset_le (a1 + b1) (a2 + b2) r"
using assms
using multisetUnionLeMono1[of "r" "a1" "a2" "b1"]
using multisetUnionLeMono2[of "r" "b1" "b2" "a2"]
using multisetLeTrans[of "r" "a1 + b1" "a2 + b1" "a2 + b2"]
by simp
lemma multisetLeListDiff:
assumes
"trans r"
shows
"multiset_le (mset (minus_list_set a b)) (mset a) r"
proof (induct a)
case Nil
thus ?case
unfolding multiset_le_def
by simp
next
case (Cons x a')
thus ?case
using assms
using multisetEmptyLeI[of "{#x#}" "r"]
using multisetUnionLeMono[of "r" "mset (minus_list_set a' b)" "mset a'" "{#}" "{#x#}"]
using multisetUnionLeMono1[of "r" "mset (minus_list_set a' b)" "mset a'" "{#x#}"]
by (simp add: minus_list_set_Cons1)
qed
subsection‹Single element lists›
lemma lengthOneCharacterisation:
shows "(length l = 1) = (l = [hd l])"
by (induct l) auto
lemma lengthOneImpliesOnlyElement:
assumes "length l = 1" and "a : set l"
shows "∀ a'. a' : set l ⟶ a' = a"
proof (cases l)
case (Cons literal' clause')
with assms
show ?thesis
by auto
qed simp
end