(*<*) (* * 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 (*>*)