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 "list_diff"} - the set difference operation on two lists.›
primrec list_diff :: "'a list ⇒ 'a list ⇒ 'a list"
where
"list_diff x [] = x" |
"list_diff x (y#ys) = list_diff (removeAll y x) ys"
lemma [simp]:
shows "list_diff [] y = []"
by (induct y) auto
lemma [simp]:
shows "list_diff (x # xs) y = (if x ∈ set y then list_diff xs y else x # list_diff xs y)"
proof (induct y arbitrary: xs)
case (Cons y ys)
thus ?case
proof (cases "x = y")
case True
thus ?thesis
by simp
next
case False
thus ?thesis
proof (cases "x ∈ set ys")
case True
thus ?thesis
using Cons
by simp
next
case False
thus ?thesis
using Cons
by simp
qed
qed
qed simp
lemma listDiffIff:
shows "(x ∈ set a ∧ x ∉ set b) = (x ∈ set (list_diff a b))"
by (induct a) auto
lemma listDiffDoubleRemoveAll:
assumes "x ∈ set a"
shows "list_diff b a = list_diff b (x # a)"
using assms
by (induct b) auto
lemma removeAllListDiff[simp]:
shows "removeAll x (list_diff a b) = list_diff (removeAll x a) b"
by (induct a) auto
lemma listDiffRemoveAllNonMember:
assumes "x ∉ set a"
shows "list_diff a b = list_diff 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 (list_diff a b) = list_diff (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 (list_diff a b) @ remdups b"
proof (induct a)
case (Cons x a')
thus ?case
using listDiffIff[of "x" "a'" "b"]
by auto
qed simp
lemma remdupsAppendSet:
shows "set (remdups (a @ b)) = set (remdups a @ remdups (list_diff b a))"
proof (induct a)
case Nil
thus ?case
by auto
next
case (Cons x a')
thus ?case
proof (cases "x ∈ set a'")
case True
thus ?thesis
using Cons
using listDiffDoubleRemoveAll[of "x" "a'" "b"]
by simp
next
case False
thus ?thesis
proof (cases "x ∈ set b")
case True
show ?thesis
proof-
have "set (remdups (x # a') @ remdups (list_diff b (x # a'))) =
set (x # remdups a' @ remdups (list_diff b (x # a')))"
using ‹x ∉ set a'›
by auto
also have "… = set (x # remdups a' @ remdups (list_diff (removeAll x b) a'))"
by auto
also have "… = set (x # remdups a' @ remdups (removeAll x (list_diff b a')))"
by simp
also have "… = set (remdups a' @ x # remdups (removeAll x (list_diff b a')))"
by simp
also have "… = set (remdups a' @ x # removeAll x (remdups (list_diff b a')))"
by (simp only: remdupsRemoveAllCommute)
also have "… = set (remdups a') ∪ set (x # removeAll x (remdups (list_diff b a')))"
by simp
also have "… = set (remdups a') ∪ {x} ∪ set (removeAll x (remdups (list_diff b a')))"
by auto
also have "… = set (remdups a') ∪ set (remdups (list_diff b a'))"
proof-
from ‹x ∉ set a'› ‹x ∈ set b›
have "x ∈ set (list_diff b a')"
using listDiffIff[of "x" "b" "a'"]
by simp
hence "x ∈ set (remdups (list_diff b a'))"
by auto
thus ?thesis
by auto
qed
also have "… = set (remdups (a' @ b))"
using Cons(1)
by simp
also have "… = set (remdups ((x # a') @ b))"
using ‹x ∈ set b›
by simp
finally show ?thesis
by simp
qed
next
case False
thus ?thesis
proof-
have "set (remdups (x # a') @ remdups (list_diff b (x # a'))) =
set (x # (remdups a') @ remdups (list_diff b (x # a')))"
using ‹x ∉ set a'›
by auto
also have "… = set (x # remdups a' @ remdups (list_diff (removeAll x b) a'))"
by auto
also have "… = set (x # remdups a' @ remdups (list_diff b a'))"
using ‹x ∉ set b›
by auto
also have "… = {x} ∪ set (remdups (a' @ b))"
using Cons(1)
by simp
also have "… = set (remdups ((x # a') @ b))"
by auto
finally show ?thesis
by simp
qed
qed
qed
qed
lemma remdupsAppendMultiSet:
shows "mset (remdups (a @ b)) = mset (remdups a @ remdups (list_diff b a))"
proof (induct a)
case Nil
thus ?case
by auto
next
case (Cons x a')
thus ?case
proof (cases "x ∈ set a'")
case True
thus ?thesis
using Cons
using listDiffDoubleRemoveAll[of "x" "a'" "b"]
by simp
next
case False
thus ?thesis
proof (cases "x ∈ set b")
case True
show ?thesis
proof-
have "mset (remdups (x # a') @ remdups (list_diff b (x # a'))) =
mset (x # remdups a' @ remdups (list_diff b (x # a')))"
proof-
have "remdups (x # a') = x # remdups a'"
using ‹x ∉ set a'›
by auto
thus ?thesis
by simp
qed
also have "… = mset (x # remdups a' @ remdups (list_diff (removeAll x b) a'))"
by auto
also have "… = mset (x # remdups a' @ remdups (removeAll x (list_diff b a')))"
by simp
also have "… = mset (remdups a' @ x # remdups (removeAll x (list_diff b a')))"
by (simp add: union_assoc)
also have "… = mset (remdups a' @ x # removeAll x (remdups (list_diff b a')))"
by (simp only: remdupsRemoveAllCommute)
also have "… = mset (remdups a') + mset (x # removeAll x (remdups (list_diff b a')))"
by simp
also have "… = mset (remdups a') + {#x#} + mset (removeAll x (remdups (list_diff b a')))"
by simp
also have "… = mset (remdups a') + mset (remdups (list_diff b a'))"
proof-
from ‹x ∉ set a'› ‹x ∈ set b›
have "x ∈ set (list_diff b a')"
using listDiffIff[of "x" "b" "a'"]
by simp
hence "x ∈ set (remdups (list_diff b a'))"
by auto
thus ?thesis
using removeAll_multiset[of "remdups (list_diff b a')" "x"]
by (simp add: union_assoc)
qed
also have "… = mset (remdups (a' @ b))"
using Cons(1)
by simp
also have "… = mset (remdups ((x # a') @ b))"
using ‹x ∈ set b›
by simp
finally show ?thesis
by simp
qed
next
case False
thus ?thesis
proof-
have "mset (remdups (x # a') @ remdups (list_diff b (x # a'))) =
mset (x # remdups a' @ remdups (list_diff b (x # a')))"
proof-
have "remdups (x # a') = x # remdups a'"
using ‹x ∉ set a'›
by auto
thus ?thesis
by simp
qed
also have "… = mset (x # remdups a' @ remdups (list_diff (removeAll x b) a'))"
by auto
also have "… = mset (x # remdups a' @ remdups (list_diff b a'))"
using ‹x ∉ set b›
using removeAll_id[of "x" "b"]
by simp
also have "… = {#x#} + mset (remdups (a' @ b))"
using Cons(1)
by (simp add: union_commute)
also have "… = mset (remdups ((x # a') @ b))"
using ‹x ∉ set a'› ‹x ∉ set b›
by (auto simp add: union_commute)
finally show ?thesis
by simp
qed
qed
qed
qed
lemma remdupsListDiff:
"remdups (list_diff a b) = list_diff (remdups a) (remdups b)"
proof(induct a)
case Nil
thus ?case
by simp
next
case (Cons x a')
thus ?case
using listDiffIff[of "x" "a'" "b"]
by auto
qed
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 (list_diff 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 (list_diff a' b)" "mset a'" "{#}" "{#x#}"]
using multisetUnionLeMono1[of "r" "mset (list_diff a' b)" "mset a'" "{#x#}"]
by auto
qed
subsection‹Levi's lemma›
text‹Obsolete: these two lemmas are already proved as @{term
append_eq_append_conv2} and @{term append_eq_Cons_conv}.›
lemma FullLevi:
shows "(x @ y = z @ w) =
(x = z ∧ y = w ∨
(∃ t. z @ t = x ∧ t @ y = w) ∨
(∃ t. x @ t = z ∧ t @ w = y))" (is "?lhs = ?rhs")
proof
assume "?rhs"
thus "?lhs"
by auto
next
assume "?lhs"
thus "?rhs"
proof (induct x arbitrary: z)
case (Cons a x')
show ?case
proof (cases "z = []")
case True
with ‹(a # x') @ y = z @ w›
obtain t where "z @ t = a # x'" "t @ y = w"
by auto
thus ?thesis
by auto
next
case False
then obtain b and z' where "z = b # z'"
by (auto simp add: neq_Nil_conv)
with ‹(a # x') @ y = z @ w›
have "x' @ y = z' @ w" "a = b"
by auto
with Cons(1)[of "z'"]
have "x' = z' ∧ y = w ∨ (∃t. z' @ t = x' ∧ t @ y = w) ∨ (∃t. x' @ t = z' ∧ t @ w = y)"
by simp
with ‹a = b› ‹z = b # z'›
show ?thesis
by auto
qed
qed simp
qed
lemma SimpleLevi:
shows "(p @ s = a # list) =
( p = [] ∧ s = a # list ∨
(∃ t. p = a # t ∧ t @ s = list))"
by (induct p) auto
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