Theory ODList

(*<*)
(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *
 * 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"
  by (simp add: properties_for_sort)
(*>*)

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
  by (simp add: odlist_Abs_inverse)

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
  by (simp add: toList_ODList)

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
  by standard (simp add: equal_odlist_def)

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
  by (simp add: toList_ODList)

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])

subsubsection‹head›

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
  apply (simp add: toSet_def)
  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"
  by (simp add: odlist_all_iff)

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
  apply (simp add: toSet_def)
  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
  apply (simp add: toSet_def)
  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
  apply (simp add: toSet_def)
  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"
    by (simp_all add: ODList_def)
  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"
    by (simp_all add: ODList_def)
  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)
   apply (simp add: distinct_map)
  apply (simp add: sorted_mono_map)
  done

lemma tabulate_toList[simp, code abstract]:
  "toList (tabulate ks f) = List.map (λk. (k, f k)) (toList ks)"
  unfolding tabulate_def
  apply (simp add: toList_ODList)
  apply (subst msort_map)
  apply simp_all
   apply (rule inj_onI)
   apply simp
  apply (rule mono_onI)
  apply (simp add: less_eq_prod_def less_le)
  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)
    apply (simp add: less_eq_prod_def less_le)
    done
  also from insert have "... = lookup (tabulate (fromList xs) f)"
    unfolding tabulate_def lookup_def
    by (simp add: toList_ODList toList_fromList)
  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
(*>*)