# Theory ODList

```(*<*)
(*
* Knowledge-based programs.
* (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
*
* Based on Florian Haftmann's DList.thy and Tobias Nipkow's msort proofs.
*)

theory ODList
imports
"HOL-Library.Multiset"
List_local
begin
(*>*)

text‹

Define a type of ordered distinct lists, intended to represent sets.

The advantage of this representation is that it is isomorphic to the
set of finite sets. Conversely it requires the carrier type to be a
linear order.  Note that this representation does not arise from a
quotient on lists: all the unsorted lists are junk.

›

context linorder
begin

text‹

"Absorbing" msort, a variant of Tobias Nipkow's proofs from 1992.

›

fun
merge :: "'a list ⇒ 'a list ⇒ 'a list"
where
"merge [] ys = ys"
| "merge xs [] = xs"
| "merge (x#xs) (y#ys) =
(if x = y then merge xs (y#ys)
else if x < y then x # merge xs (y#ys)
else y # merge (x#xs) ys)"

(*<*)
lemma set_merge[simp]:
"set (merge xs ys) = set (xs @ ys)"
by (induct xs ys rule: merge.induct) auto

lemma distinct_sorted_merge[simp]:
"⟦ distinct xs; distinct ys; sorted xs; sorted ys ⟧
⟹ distinct (merge xs ys) ∧ sorted (merge xs ys)"
by (induct xs ys rule: merge.induct) (auto)

lemma mset_merge [simp]:
"⟦ distinct (xs @ ys) ⟧ ⟹ mset (merge xs ys) = mset xs + mset ys"
by (induct xs ys rule: merge.induct) (simp_all add: ac_simps)
(*>*)

text‹The "absorbing" sort itself.›

fun msort :: "'a list ⇒ 'a list"
where
"msort [] = []"
| "msort [x] = [x]"
| "msort xs = merge (msort (take (size xs div 2) xs))
(msort (drop (size xs div 2) xs))"

(*<*)
lemma msort_distinct_sorted[simp]:
"distinct (msort xs) ∧ sorted (msort xs)"
by (induct xs rule: msort.induct) simp_all

lemma msort_set[simp]:
"set (msort xs) = set xs"
by (induct xs rule: msort.induct)
(simp_all, metis List.set_simps(2) append_take_drop_id set_append) (* thankyou sledgehammer! *)

lemma msort_remdups[simp]:
"remdups (msort xs) = msort xs"
by simp

lemma msort_idle[simp]:
"⟦ distinct xs; sorted xs ⟧ ⟹ msort xs = xs"
by (rule map_sorted_distinct_set_unique[where f=id]) (auto simp: map.id)

lemma mset_msort[simp]:
"distinct xs ⟹ mset (msort xs) = mset xs"
by (rule iffD1[OF set_eq_iff_mset_eq_distinct]) simp_all

lemma msort_sort[simp]:
"distinct xs ⟹ sort xs = msort xs"
(*>*)

end (* context linorder *)

section ‹The @{term "odlist"} type›

typedef (overloaded) ('a :: linorder) odlist = "{ x::'a list . sorted x ∧ distinct x }"
morphisms toList odlist_Abs by (auto iff: sorted_simps(1))

lemma distinct_toList[simp]: "distinct (toList xs)"
using toList by auto

lemma sorted_toList[simp]: "sorted (toList xs)"
using toList by auto

text‹

Code generator voodoo: this is the constructor for the abstract type.

›

definition
ODList :: "('a :: linorder) list ⇒ 'a odlist"
where
"ODList ≡ odlist_Abs ∘ msort"

lemma toList_ODList:
"toList (ODList xs) = msort xs"
unfolding ODList_def

lemma ODList_toList[simp, code abstype]:
"ODList (toList xs) = xs"
unfolding ODList_def
by (cases xs) (simp add: odlist_Abs_inverse)

text‹

Runtime cast from @{typ "'a list"} into @{typ "'a odlist"}. This is
just a renaming of @{term "ODList"} -- names are significant to the
code generator's abstract type machinery.

›

definition
fromList :: "('a :: linorder) list ⇒ 'a odlist"
where
"fromList ≡ ODList"

lemma toList_fromList[code abstract]:
"toList (fromList xs) = msort xs"
unfolding fromList_def

subsection‹Basic properties: equality, finiteness›

(*<*)
declare toList_inject[iff]
(*>*)

instantiation odlist :: (linorder) equal
(*<*)
begin

definition [code]:
"HOL.equal A B ⟷ odlist_equal (toList A) (toList B)"

instance

end
(*>*)

instance odlist :: ("{finite, linorder}") finite
(*<*)
proof
let ?ol = "UNIV :: 'a odlist set"
let ?s = "UNIV :: 'a set set"
have "finite ?s" by simp
moreover
have "?ol ⊆ range (odlist_Abs ∘ sorted_list_of_set)"
proof
fix x show "x ∈ range (odlist_Abs ∘ sorted_list_of_set)"
apply (cases x)
apply (rule range_eqI[where x="set (toList x)"])
apply (clarsimp simp: odlist_Abs_inject sorted_list_of_set_sort_remdups odlist_Abs_inverse distinct_remdups_id)
done
qed
ultimately show "finite ?ol" by (blast intro: finite_surj)
qed
(*>*)

subsection‹Constants›

definition
empty :: "('a :: linorder) odlist"
where
"empty ≡ ODList []"

lemma toList_empty[simp, code abstract]:
"toList empty = []"
unfolding empty_def by (simp add: toList_ODList)

subsection‹Operations›

subsubsection‹toSet›

definition
toSet :: "('a :: linorder) odlist ⇒ 'a set"
where
"toSet X = set (toList X)"

lemma toSet_empty[simp]:
"toSet empty = {}"
unfolding toSet_def empty_def by (simp add: toList_ODList)

lemma toSet_ODList[simp]:
"⟦ distinct xs; sorted xs ⟧ ⟹ toSet (ODList xs) = set xs"
unfolding toSet_def by (simp add: toList_ODList)

lemma toSet_fromList_set[simp]:
"toSet (fromList xs) = set xs"
unfolding toSet_def fromList_def

lemma toSet_inj[intro, simp]: "inj toSet"
apply (rule injI)
unfolding toSet_def
apply (case_tac x)
apply (case_tac y)
apply (auto iff: odlist_Abs_inject odlist_Abs_inverse sorted_distinct_set_unique)
done

lemma toSet_eq_iff:
"X = Y ⟷ toSet X = toSet Y"
by (blast dest: injD[OF toSet_inj])

definition
hd :: "('a :: linorder) odlist ⇒ 'a"
where
[code]: "hd ≡ List.hd ∘ toList"

lemma hd_toList: "toList xs = y # ys ⟹ ODList.hd xs = y"
unfolding hd_def by simp

subsubsection‹member›

definition
member :: "('a :: linorder) odlist ⇒ 'a ⇒ bool"
where
[code]: "member xs x ≡ List.member (toList xs) x"

lemma member_toSet[iff]:
"member xs x ⟷x ∈ toSet xs"
unfolding member_def toSet_def by (simp add: in_set_member)

subsubsection‹Filter›

definition
filter :: "(('a :: linorder) ⇒ bool) ⇒ 'a odlist ⇒ 'a odlist"
where
"filter P xs ≡ ODList (List.filter P (toList xs))"

lemma toList_filter[simp, code abstract]:
"toList (filter P xs) = List.filter P (toList xs)"
unfolding filter_def by (simp add: toList_ODList)

lemma toSet_filter[simp]:
"toSet (filter P xs) = { x ∈ toSet xs . P x }"
unfolding filter_def
apply simp
done

subsubsection‹All›

definition
odlist_all :: "('a :: linorder ⇒ bool) ⇒ 'a odlist ⇒ bool"
where
[code]: "odlist_all P xs ≡ list_all P (toList xs)"

lemma odlist_all_iff:
"odlist_all P xs ⟷ (∀x ∈ toSet xs. P x)"
unfolding odlist_all_def toSet_def by (simp only: list_all_iff)

lemma odlist_all_cong [fundef_cong]:
"xs = ys ⟹ (⋀x. x ∈ toSet ys ⟹ f x = g x) ⟹ odlist_all f xs = odlist_all g ys"

subsubsection‹Difference›

definition
difference :: "('a :: linorder) odlist ⇒ 'a odlist ⇒ 'a odlist"
where
"difference xs ys = ODList (List_local.difference (toList xs) (toList ys))"

lemma toList_difference[simp, code abstract]:
"toList (difference xs ys) = List_local.difference (toList xs) (toList ys)"
unfolding difference_def by (simp add: toList_ODList)

lemma toSet_difference[simp]:
"toSet (difference xs ys) = toSet xs - toSet ys"
unfolding difference_def
apply simp
done

subsubsection‹Intersection›

definition
intersect :: "('a :: linorder) odlist ⇒ 'a odlist ⇒ 'a odlist"
where
"intersect xs ys = ODList (List_local.intersection (toList xs) (toList ys))"

lemma toList_intersect[simp, code abstract]:
"toList (intersect xs ys) = List_local.intersection (toList xs) (toList ys)"
unfolding intersect_def by (simp add: toList_ODList)

lemma toSet_intersect[simp]:
"toSet (intersect xs ys) = toSet xs ∩ toSet ys"
unfolding intersect_def
apply simp
done

subsubsection‹Union›

definition
union :: "('a :: linorder) odlist ⇒ 'a odlist ⇒ 'a odlist"
where
"union xs ys = ODList (merge (toList xs) (toList ys))"

lemma toList_union[simp, code abstract]:
"toList (union xs ys) = merge (toList xs) (toList ys)"
unfolding union_def by (simp add: toList_ODList)

lemma toSet_union[simp]:
"toSet (union xs ys) = toSet xs ∪ toSet ys"
unfolding union_def
apply simp
done

definition
big_union :: "('b ⇒ ('a :: linorder) odlist) ⇒ 'b list ⇒ 'a odlist"
where
[code]: "big_union f X ≡ foldr (λa A. ODList.union (f a) A) X ODList.empty"

lemma toSet_big_union[simp]:
"toSet (big_union f X) = (⋃x ∈ set X. toSet (f x))"
proof -
{ fix X Y
have "toSet (foldr (λx A. ODList.union (f x) A) X Y) = toSet Y ∪ (⋃x ∈ set X. toSet (f x))"
by (induct X arbitrary: Y) auto }
thus ?thesis
unfolding big_union_def by simp
qed

subsubsection‹Case distinctions›

text‹

We construct ODLists out of lists, so talk in terms of those, not a
one-step constructor we don't use.

›

lemma distinct_sorted_induct [consumes 2, case_names Nil insert]:
assumes "distinct xs"
assumes "sorted xs"
assumes base: "P []"
assumes step: "⋀x xs. ⟦ distinct (x # xs); sorted (x # xs); P xs ⟧ ⟹ P (x # xs)"
shows "P xs"
using ‹distinct xs› ‹sorted xs› proof (induct xs)
case Nil from ‹P []› show ?case .
next
case (Cons x xs)
then have "distinct (x # xs)" and "sorted (x # xs)" and "P xs" by (simp_all)
with step show "P (x # xs)" .
qed

lemma odlist_induct [case_names empty insert, cases type: odlist]:
assumes empty: "⋀dxs. dxs = empty ⟹ P dxs"
assumes insrt: "⋀dxs x xs. ⟦ dxs = fromList (x # xs); distinct (x # xs); sorted (x # xs); P (fromList xs) ⟧
⟹ P dxs"
shows "P dxs"
proof (cases dxs)
case (odlist_Abs xs)
then have dxs: "dxs = ODList xs" and distinct: "distinct xs" and sorted: "sorted xs"
from ‹distinct xs› and ‹sorted xs› have "P (ODList xs)"
proof (induct xs rule: distinct_sorted_induct)
case Nil from empty show ?case by (simp add: empty_def)
next
case (insert x xs) thus ?case
apply -
apply (rule insrt)
apply (auto simp: fromList_def)
done
qed
with dxs show "P dxs" by simp
qed

lemma odlist_cases [case_names empty insert, cases type: odlist]:
assumes empty: "dxs = empty ⟹ P"
assumes insert: "⋀x xs. ⟦ dxs = fromList (x # xs); distinct (x # xs); sorted (x # xs) ⟧
⟹ P"
shows P
proof (cases dxs)
case (odlist_Abs xs)
then have dxs: "dxs = ODList xs" and distinct: "distinct xs" and sorted: "sorted xs"
show P proof (cases xs)
case Nil with dxs have "dxs = empty" by (simp add: empty_def)
with empty show P .
next
case (Cons y ys)
with dxs distinct sorted insert
show P by (simp add: fromList_def)
qed
qed

subsubsection‹Relations›

text‹

Relations, represented as a list of pairs.

›

type_synonym 'a odrelation = "('a × 'a) odlist"

subsubsection‹Image›

text‹

The output of @{term "List_local.image"} is not guaranteed to be
ordered or distinct. Also the relation need not be monomorphic.

›

definition
image :: "('a :: linorder × 'b :: linorder) odlist ⇒ 'a odlist ⇒ 'b odlist"
where
"image R xs = ODList (List_local.image (toList R) (toList xs))"

lemma toList_image[simp, code abstract]:
"toList (image R xs) = msort (List_local.image (toList R) (toList xs))"
unfolding image_def by (simp add: toList_ODList)

lemma toSet_image[simp]:
"toSet (image R xs) = toSet R `` toSet xs"
unfolding image_def by (simp add: toSet_def toList_ODList)

subsubsection‹Linear order›

text‹

Lexicographic ordering on lists. Executable, unlike in List.thy.

›

instantiation odlist :: (linorder) linorder
begin
print_context
fun
less_eq_list :: "'a list ⇒ 'a list ⇒ bool"
where
"less_eq_list [] ys = True"
| "less_eq_list xs [] = False"
| "less_eq_list (x # xs) (y # ys) = (x < y ∨ (x = y ∧ less_eq_list xs ys))"

lemma less_eq_list_nil_inv:
fixes xs :: "'a list"
shows "less_eq_list xs [] ⟹ xs = []"
by (cases xs) simp_all

lemma less_eq_list_cons_inv:
fixes x :: 'a
shows "less_eq_list (x # xs) yys ⟹ ∃y ys. yys = y # ys ∧ (x < y ∨ (x = y ∧ less_eq_list xs ys))"
by (cases yys) auto

lemma less_eq_list_refl:
fixes xs :: "'a list"
shows "less_eq_list xs xs"
by (induct xs) simp_all

lemma less_eq_list_trans:
fixes xs ys zs :: "'a list"
shows "⟦ less_eq_list xs ys; less_eq_list ys zs ⟧ ⟹ less_eq_list xs zs"
apply (induct xs ys arbitrary: zs rule: less_eq_list.induct)
apply simp
apply simp
apply clarsimp
apply (erule disjE)
apply (drule less_eq_list_cons_inv)
apply clarsimp
apply (erule disjE)
apply auto[1]
apply auto[1]
apply (auto dest: less_eq_list_cons_inv)
done

lemma less_eq_list_antisym:
fixes xs ys :: "'a list"
shows "⟦ less_eq_list xs ys; less_eq_list ys xs ⟧ ⟹ xs = ys"
by (induct xs ys rule: less_eq_list.induct) (auto dest: less_eq_list_nil_inv)

lemma less_eq_list_linear:
fixes xs ys :: "'a list"
shows "less_eq_list xs ys ∨ less_eq_list ys xs"
by (induct xs ys rule: less_eq_list.induct) auto

definition
less_eq_odlist :: "'a odlist ⇒ 'a odlist ⇒ bool"
where
"xs ≤ ys ≡ less_eq_list (toList xs) (toList ys)"

fun
less_list :: "'a list ⇒ 'a list ⇒ bool"
where
"less_list [] [] = False"
| "less_list [] ys = True"
| "less_list xs [] = False"
| "less_list (x # xs) (y # ys) = (x < y ∨ (x = y ∧ less_list xs ys))"

definition
less_odlist :: "'a odlist ⇒ 'a odlist ⇒ bool"
where
"xs < ys ≡ less_list (toList xs) (toList ys)"

lemma less_eq_list_not_le:
fixes xs ys :: "'a list"
shows "(less_list xs ys) = (less_eq_list xs ys ∧ ¬ less_eq_list ys xs)"
by (induct xs ys rule: less_list.induct) auto

instance
apply intro_classes
unfolding less_eq_odlist_def less_odlist_def
using less_eq_list_not_le less_eq_list_refl less_eq_list_trans less_eq_list_antisym
apply blast
using less_eq_list_not_le less_eq_list_refl less_eq_list_trans less_eq_list_antisym
apply blast
using less_eq_list_not_le less_eq_list_refl less_eq_list_trans less_eq_list_antisym
apply blast
using less_eq_list_not_le less_eq_list_refl less_eq_list_trans less_eq_list_antisym
apply blast
apply (rule less_eq_list_linear)
done

end

subsubsection‹Finite maps›

text‹

A few operations on finite maps.

Unlike the AssocList theory, ODLists give us canonical
representations, so we can order them. Our tabulate has the wrong type
(we want to take an odlist, not a list) so we can't use that
part of the framework.

›

definition
lookup :: "('a :: linorder × 'b :: linorder) odlist ⇒ ('a ⇀ 'b)"
where
[code]: "lookup = map_of ∘ toList"

text‹Specific to ODLists.›

definition
tabulate :: "('a :: linorder) odlist ⇒ ('a ⇒ 'b :: linorder) ⇒ ('a × 'b) odlist"
where
"tabulate ks f = ODList (List.map (λk. (k, f k)) (toList ks))"

definition (in order) mono_on :: "('a ⇒ 'b::order) ⇒ 'a set ⇒ bool" where
"mono_on f X ⟷ (∀x∈X. ∀y∈X. x ≤ y ⟶ f x ≤ f y)"

lemma (in order) mono_onI [intro?]:
fixes f :: "'a ⇒ 'b::order"
shows "(⋀x y. x ∈ X ⟹ y ∈ X ⟹ x ≤ y ⟹ f x ≤ f y) ⟹ mono_on f X"
unfolding mono_on_def by simp

lemma (in order) mono_onD [dest?]:
fixes f :: "'a ⇒ 'b::order"
shows "mono_on f X ⟹ x ∈ X ⟹ y ∈ X ⟹ x ≤ y ⟹ f x ≤ f y"
unfolding mono_on_def by simp

lemma (in order) mono_on_subset:
fixes f :: "'a ⇒ 'b::order"
shows "mono_on f X ⟹ Y ⊆ X ⟹ mono_on f Y"
unfolding mono_on_def by auto

lemma sorted_mono_map:
"⟦ sorted xs; mono_on f (set xs) ⟧ ⟹ sorted (List.map f xs)"
apply (induct xs)
apply simp
apply (simp)
apply (cut_tac X="insert a (set xs)" and Y="set xs" in mono_on_subset)
apply (auto dest: mono_onD)
done

lemma msort_map:
"⟦ distinct xs; sorted xs; inj_on f (set xs); mono_on f (set xs) ⟧ ⟹ msort (List.map f xs) = List.map f xs"
apply (rule msort_idle)
done

lemma tabulate_toList[simp, code abstract]:
"toList (tabulate ks f) = List.map (λk. (k, f k)) (toList ks)"
unfolding tabulate_def
apply (subst msort_map)
apply simp_all
apply (rule inj_onI)
apply simp
apply (rule mono_onI)
done

lemma lookup_tabulate[simp]:
"lookup (tabulate ks f) = (Some o f) |` toSet ks"
proof(induct ks rule: odlist_induct)
case (empty dxs) thus ?case unfolding tabulate_def lookup_def by (simp add: toList_ODList)
next
case (insert dxs x xs)
from insert have "map_of (List.map (λk. (k, f k)) xs) = map_of (msort (List.map (λk. (k, f k)) xs))"
apply (subst msort_map)
apply (auto intro: inj_onI)
apply (rule mono_onI)
done
also from insert have "... = lookup (tabulate (fromList xs) f)"
unfolding tabulate_def lookup_def
also from insert have "... = (Some ∘ f) |` toSet (fromList xs)"
by (simp only: toSet_fromList_set)
finally have IH: "map_of (List.map (λk. (k, f k)) xs) = (Some ∘ f) |` toSet (fromList xs)" .
from insert have "lookup (tabulate dxs f) = map_of (toList (ODList (List.map (λk. (k, f k)) (x # xs))))"
unfolding tabulate_def lookup_def by (simp add: toList_fromList)
also have "... = map_of (msort (List.map (λk. (k, f k)) (x # xs)))"
by (simp only: toList_ODList)
also from insert have "... = map_of (List.map (λk. (k, f k)) (x # xs))"
by (metis msort_idle tabulate_def tabulate_toList toList_ODList)
also with insert IH have "... = (Some ∘ f) |` toSet dxs"
by (auto simp add: restrict_map_def fun_eq_iff)
finally show ?case .
qed

(*<*)
end
(*>*)
```