Theory Polynomials.OAlist
section ‹Associative Lists with Sorted Keys›
theory OAlist
imports Deriving.Comparator
begin
text ‹We define the type of @{emph ‹ordered associative lists›} (oalist). An oalist is an associative
list (i.\,e. a list of pairs) such that the keys are distinct and sorted wrt. some linear
order relation, and no key is mapped to @{term 0}. The latter invariant allows to implement various
functions operating on oalists more efficiently.
The ordering of the keys in an oalist ‹xs› is encoded as an additional parameter of ‹xs›.
This means that oalists may be ordered wrt. different orderings, even if they are of the same type.
Operations operating on more than one oalists, like ‹map2_val›, typically ensure that the orderings
of their arguments are identical by re-ordering one argument wrt. the order relation of the other.
This, however, implies that equality of order relations must be effectively decidable if executable
code is to be generated.›
subsection ‹Preliminaries›
fun min_list_param :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a" where
"min_list_param rel (x # xs) = (case xs of [] ⇒ x | _ ⇒ (let m = min_list_param rel xs in if rel x m then x else m))"
lemma min_list_param_in:
assumes "xs ≠ []"
shows "min_list_param rel xs ∈ set xs"
using assms
proof (induct xs)
case Nil
thus ?case by simp
next
case (Cons x xs)
show ?case
proof (simp add: min_list_param.simps[of rel x xs] Let_def del: min_list_param.simps set_simps(2) split: list.split,
intro conjI impI allI, simp, simp)
fix y ys
assume xs: "xs = y # ys"
have "min_list_param rel (y # ys) = min_list_param rel xs" by (simp only: xs)
also have "... ∈ set xs" by (rule Cons(1), simp add: xs)
also have "... ⊆ set (x # y # ys)" by (auto simp: xs)
finally show "min_list_param rel (y # ys) ∈ set (x # y # ys)" .
qed
qed
lemma min_list_param_minimal:
assumes "transp rel" and "⋀x y. x ∈ set xs ⟹ y ∈ set xs ⟹ rel x y ∨ rel y x"
and "z ∈ set xs"
shows "rel (min_list_param rel xs) z"
using assms(2, 3)
proof (induct xs)
case Nil
from Nil(2) show ?case by simp
next
case (Cons x xs)
from Cons(3) have disj1: "z = x ∨ z ∈ set xs" by simp
have "x ∈ set (x # xs)" by simp
hence disj2: "rel x z ∨ rel z x" using Cons(3) by (rule Cons(2))
have *: "rel (min_list_param rel xs) z" if "z ∈ set xs" using _ that
proof (rule Cons(1))
fix a b
assume "a ∈ set xs" and "b ∈ set xs"
hence "a ∈ set (x # xs)" and "b ∈ set (x # xs)" by simp_all
thus "rel a b ∨ rel b a" by (rule Cons(2))
qed
show ?case
proof (simp add: min_list_param.simps[of rel x xs] Let_def del: min_list_param.simps set_simps(2) split: list.split,
intro conjI impI allI)
assume "xs = []"
with disj1 disj2 show "rel x z" by simp
next
fix y ys
assume "xs = y # ys" and "rel x (min_list_param rel (y # ys))"
hence "rel x (min_list_param rel xs)" by simp
from disj1 show "rel x z"
proof
assume "z = x"
thus ?thesis using disj2 by simp
next
assume "z ∈ set xs"
hence "rel (min_list_param rel xs) z" by (rule *)
with assms(1) ‹rel x (min_list_param rel xs)› show ?thesis by (rule transpD)
qed
next
fix y ys
assume xs: "xs = y # ys" and "¬ rel x (min_list_param rel (y # ys))"
from disj1 show "rel (min_list_param rel (y # ys)) z"
proof
assume "z = x"
have "min_list_param rel (y # ys) ∈ set (y # ys)" by (rule min_list_param_in, simp)
hence "min_list_param rel (y # ys) ∈ set (x # xs)" by (simp add: xs)
with ‹x ∈ set (x # xs)› have "rel x (min_list_param rel (y # ys)) ∨ rel (min_list_param rel (y # ys)) x"
by (rule Cons(2))
with ‹¬ rel x (min_list_param rel (y # ys))› have "rel (min_list_param rel (y # ys)) x" by simp
thus ?thesis by (simp only: ‹z = x›)
next
assume "z ∈ set xs"
hence "rel (min_list_param rel xs) z" by (rule *)
thus ?thesis by (simp only: xs)
qed
qed
qed
definition comp_of_ord :: "('a ⇒ 'a ⇒ bool) ⇒ 'a comparator" where
"comp_of_ord le x y = (if le x y then if x = y then Eq else Lt else Gt)"
lemma comp_of_ord_eq_comp_of_ords:
assumes "antisymp le"
shows "comp_of_ord le = comp_of_ords le (λx y. le x y ∧ ¬ le y x)"
by (intro ext, auto simp: comp_of_ord_def comp_of_ords_def intro: assms antisympD)
lemma comparator_converse:
assumes "comparator cmp"
shows "comparator (λx y. cmp y x)"
proof -
from assms interpret comp?: comparator cmp .
show ?thesis by (unfold_locales, auto simp: comp.eq comp.sym intro: comp_trans)
qed
lemma comparator_composition:
assumes "comparator cmp" and "inj f"
shows "comparator (λx y. cmp (f x) (f y))"
proof -
from assms(1) interpret comp?: comparator cmp .
from assms(2) have *: "x = y" if "f x = f y" for x y using that by (rule injD)
show ?thesis by (unfold_locales, auto simp: comp.sym comp.eq * intro: comp_trans)
qed
subsection ‹Type ‹key_order››
typedef 'a key_order = "{compare :: 'a comparator. comparator compare}"
morphisms key_compare Abs_key_order
proof -
from well_order_on obtain r where "well_order_on (UNIV::'a set) r" ..
hence "linear_order r" by (simp only: well_order_on_def)
hence lin: "(x, y) ∈ r ∨ (y, x) ∈ r" for x y
by (metis Diff_iff Linear_order_in_diff_Id UNIV_I ‹well_order r› well_order_on_Field)
have antisym: "(x, y) ∈ r ⟹ (y, x) ∈ r ⟹ x = y" for x y
by (meson ‹linear_order r› antisymD linear_order_on_def partial_order_on_def)
have trans: "(x, y) ∈ r ⟹ (y, z) ∈ r ⟹ (x, z) ∈ r" for x y z
by (meson ‹linear_order r› linear_order_on_def order_on_defs(1) partial_order_on_def trans_def)
define comp where "comp = (λx y. if (x, y) ∈ r then if (y, x) ∈ r then Eq else Lt else Gt)"
show ?thesis
proof (rule, simp)
show "comparator comp"
proof (standard, simp_all add: comp_def split: if_splits, intro impI)
fix x y
assume "(x, y) ∈ r" and "(y, x) ∈ r"
thus "x = y" by (rule antisym)
next
fix x y
assume "(x, y) ∉ r"
with lin show "(y, x) ∈ r" by blast
next
fix x y z
assume "(y, x) ∉ r" and "(z, y) ∉ r"
assume "(x, y) ∈ r" and "(y, z) ∈ r"
hence "(x, z) ∈ r" by (rule trans)
moreover have "(z, x) ∉ r"
proof
assume "(z, x) ∈ r"
with ‹(x, z) ∈ r› have "x = z" by (rule antisym)
from ‹(z, y) ∉ r› ‹(x, y) ∈ r› show False unfolding ‹x = z› ..
qed
ultimately show "(z, x) ∉ r ∧ ((z, x) ∉ r ⟶ (x, z) ∈ r)" by simp
qed
qed
qed
lemma comparator_key_compare [simp, intro!]: "comparator (key_compare ko)"
using key_compare[of ko] by simp
instantiation key_order :: (type) equal
begin
definition equal_key_order :: "'a key_order ⇒ 'a key_order ⇒ bool" where "equal_key_order = (=)"
instance by (standard, simp add: equal_key_order_def)
end
setup_lifting type_definition_key_order
instantiation key_order :: (type) uminus
begin
lift_definition uminus_key_order :: "'a key_order ⇒ 'a key_order" is "λc x y. c y x"
by (fact comparator_converse)
instance ..
end
lift_definition le_of_key_order :: "'a key_order ⇒ 'a ⇒ 'a ⇒ bool" is "λcmp. le_of_comp cmp" .
lift_definition lt_of_key_order :: "'a key_order ⇒ 'a ⇒ 'a ⇒ bool" is "λcmp. lt_of_comp cmp" .
definition key_order_of_ord :: "('a ⇒ 'a ⇒ bool) ⇒ 'a key_order"
where "key_order_of_ord ord = Abs_key_order (comp_of_ord ord)"
lift_definition key_order_of_le :: "'a::linorder key_order" is comparator_of
by (fact comparator_of)