Theory OAlist_Poly_Mapping
section ‹Ordered Associative Lists for Polynomials›
theory OAlist_Poly_Mapping
imports PP_Type MPoly_Type_Class_Ordered OAlist
begin
text ‹We introduce a dedicated type for ordered associative lists (oalists) representing polynomials.
To that end, we require the order relation the oalists are sorted wrt. to be admissible term orders,
and furthermore sort the lists @{emph ‹descending›} rather than @{emph ‹ascending›}, because this
allows to implement various operations more efficiently.
For technical reasons, we must restrict the type of terms to types embeddable into
@{typ "(nat, nat) pp × nat"}, though. All types we are interested in meet this requirement.›
lemma comparator_lexicographic:
fixes f::"'a ⇒ 'b" and g::"'a ⇒ 'c"
assumes "comparator c1" and "comparator c2" and "⋀x y. f x = f y ⟹ g x = g y ⟹ x = y"
shows "comparator (λx y. case c1 (f x) (f y) of Eq ⇒ c2 (g x) (g y) | val ⇒ val)"
(is "comparator ?c3")
proof -
from assms(1) interpret c1: comparator c1 .
from assms(2) interpret c2: comparator c2 .
show ?thesis
proof
fix x y :: 'a
show "invert_order (?c3 x y) = ?c3 y x"
by (simp add: c1.eq c2.eq split: order.split,
metis invert_order.simps(1) invert_order.simps(2) c1.sym c2.sym order.distinct(5))
next
fix x y :: 'a
assume "?c3 x y = Eq"
hence "f x = f y" and "g x = g y" by (simp_all add: c1.eq c2.eq split: order.splits if_split_asm)
thus "x = y" by (rule assms(3))
next
fix x y z :: 'a
assume "?c3 x y = Lt"
hence d1: "c1 (f x) (f y) = Lt ∨ (c1 (f x) (f y) = Eq ∧ c2 (g x) (g y) = Lt)"
by (simp split: order.splits)
assume "?c3 y z = Lt"
hence d2: "c1 (f y) (f z) = Lt ∨ (c1 (f y) (f z) = Eq ∧ c2 (g y) (g z) = Lt)"
by (simp split: order.splits)
from d1 show "?c3 x z = Lt"
proof
assume 1: "c1 (f x) (f y) = Lt"
from d2 show ?thesis
proof
assume "c1 (f y) (f z) = Lt"
with 1 have "c1 (f x) (f z) = Lt" by (rule c1.comp_trans)
thus ?thesis by simp
next
assume "c1 (f y) (f z) = Eq ∧ c2 (g y) (g z) = Lt"
hence "f z = f y" and "c2 (g y) (g z) = Lt" by (simp_all add: c1.eq)
with 1 show ?thesis by simp
qed
next
assume "c1 (f x) (f y) = Eq ∧ c2 (g x) (g y) = Lt"
hence 1: "f x = f y" and 2: "c2 (g x) (g y) = Lt" by (simp_all add: c1.eq)
from d2 show ?thesis
proof
assume "c1 (f y) (f z) = Lt"
thus ?thesis by (simp add: 1)
next
assume "c1 (f y) (f z) = Eq ∧ c2 (g y) (g z) = Lt"
hence 3: "f y = f z" and "c2 (g y) (g z) = Lt" by (simp_all add: c1.eq)
from 2 this(2) have "c2 (g x) (g z) = Lt" by (rule c2.comp_trans)
thus ?thesis by (simp add: 1 3)
qed
qed
qed
qed
class nat_term =
fixes rep_nat_term :: "'a ⇒ ((nat, nat) pp × nat)"
and splus :: "'a ⇒ 'a ⇒ 'a"
assumes rep_nat_term_inj: "rep_nat_term x = rep_nat_term y ⟹ x = y"
and full_component: "snd (rep_nat_term x) = i ⟹ (∃y. rep_nat_term y = (t, i))"
and splus_term: "rep_nat_term (splus x y) = pprod.splus (fst (rep_nat_term x)) (rep_nat_term y)"
begin
definition "lex_comp_aux = (λx y. case comp_of_ord lex_pp (fst (rep_nat_term x)) (fst (rep_nat_term y)) of
Eq ⇒ comparator_of (snd (rep_nat_term x)) (snd (rep_nat_term y)) | val ⇒ val)"
lemma full_componentE:
assumes "snd (rep_nat_term x) = i"
obtains y where "rep_nat_term y = (t, i)"
proof -
from assms have "∃y. rep_nat_term y = (t, i)" by (rule full_component)
then obtain y where "rep_nat_term y = (t, i)" ..
thus ?thesis ..
qed
end
class nat_pp_term = nat_term + zero + plus +
assumes rep_nat_term_zero: "rep_nat_term 0 = (0, 0)"
and splus_pp_term: "splus = (+)"
definition nat_term_comp :: "'a::nat_term comparator ⇒ bool"
where "nat_term_comp cmp ⟷
(∀u v. snd (rep_nat_term u) = snd (rep_nat_term v) ⟶ fst (rep_nat_term u) = 0 ⟶ cmp u v ≠ Gt) ∧
(∀u v. fst (rep_nat_term u) = fst (rep_nat_term v) ⟶ snd (rep_nat_term u) < snd (rep_nat_term v) ⟶ cmp u v = Lt) ∧
(∀t u v. cmp u v = Lt ⟶ cmp (splus t u) (splus t v) = Lt) ∧
(∀u v a b. fst (rep_nat_term u) = fst (rep_nat_term a) ⟶ fst (rep_nat_term v) = fst (rep_nat_term b) ⟶
snd (rep_nat_term u) = snd (rep_nat_term v) ⟶ snd (rep_nat_term a) = snd (rep_nat_term b) ⟶
cmp a b = Lt ⟶ cmp u v = Lt)"
lemma nat_term_compI:
assumes "⋀u v. snd (rep_nat_term u) = snd (rep_nat_term v) ⟹ fst (rep_nat_term u) = 0 ⟹ cmp u v ≠ Gt"
and "⋀u v. fst (rep_nat_term u) = fst (rep_nat_term v) ⟹ snd (rep_nat_term u) < snd (rep_nat_term v) ⟹ cmp u v = Lt"
and "⋀t u v. cmp u v = Lt ⟹ cmp (splus t u) (splus t v) = Lt"
and "⋀u v a b. fst (rep_nat_term u) = fst (rep_nat_term a) ⟹ fst (rep_nat_term v) = fst (rep_nat_term b) ⟹
snd (rep_nat_term u) = snd (rep_nat_term v) ⟹ snd (rep_nat_term a) = snd (rep_nat_term b) ⟹
cmp a b = Lt ⟹ cmp u v = Lt"
shows "nat_term_comp cmp"
unfolding nat_term_comp_def fst_conv snd_conv using assms by blast
lemma nat_term_compD1:
assumes "nat_term_comp cmp" and "snd (rep_nat_term u) = snd (rep_nat_term v)" and "fst (rep_nat_term u) = 0"
shows "cmp u v ≠ Gt"
using assms unfolding nat_term_comp_def fst_conv by blast
lemma nat_term_compD2:
assumes "nat_term_comp cmp" and "fst (rep_nat_term u) = fst (rep_nat_term v)" and "snd (rep_nat_term u) < snd (rep_nat_term v)"
shows "cmp u v = Lt"
using assms unfolding nat_term_comp_def fst_conv snd_conv by blast
lemma nat_term_compD3:
assumes "nat_term_comp cmp" and "cmp u v = Lt"
shows "cmp (splus t u) (splus t v) = Lt"
using assms unfolding nat_term_comp_def snd_conv by blast
lemma nat_term_compD4:
assumes "nat_term_comp cmp" and "fst (rep_nat_term u) = fst (rep_nat_term a)"
and "fst (rep_nat_term v) = fst (rep_nat_term b)" and "snd (rep_nat_term u) = snd (rep_nat_term v)"
and "snd (rep_nat_term a) = snd (rep_nat_term b)" and "cmp a b = Lt"
shows "cmp u v = Lt"
using assms unfolding nat_term_comp_def snd_conv by blast
lemma nat_term_compD1':
assumes "comparator cmp" and "nat_term_comp cmp" and "snd (rep_nat_term u) ≤ snd (rep_nat_term v)"
and "fst (rep_nat_term u) = 0"
shows "cmp u v ≠ Gt"
proof (cases "snd (rep_nat_term u) = snd (rep_nat_term v)")
case True
with assms(2) show ?thesis using assms(4) by (rule nat_term_compD1)
next
from assms(1) interpret cmp: comparator cmp .
case False
with assms(3) have a: "snd (rep_nat_term u) < snd (rep_nat_term v)" by simp
from refl obtain w::'a where eq: "rep_nat_term w = (0, snd (rep_nat_term v))" by (rule full_componentE)
have "cmp u w = Lt" by (rule nat_term_compD2, fact assms(2), simp_all add: eq assms(4) a)
moreover have "cmp w v ≠ Gt" by (rule nat_term_compD1, fact assms(2), simp_all add: eq)
ultimately show "cmp u v ≠ Gt" by (simp add: cmp.nGt_le_conv cmp.Lt_lt_conv)
qed
lemma nat_term_compD4':
assumes "comparator cmp" and "nat_term_comp cmp" and "fst (rep_nat_term u) = fst (rep_nat_term a)"
and "fst (rep_nat_term v) = fst (rep_nat_term b)" and "snd (rep_nat_term u) = snd (rep_nat_term v)"
and "snd (rep_nat_term a) = snd (rep_nat_term b)"
shows "cmp u v = cmp a b"
proof -
from assms(1) interpret cmp: comparator cmp .
show ?thesis
proof (cases "cmp a b")
case Eq
hence "fst (rep_nat_term u) = fst (rep_nat_term v)" by (simp add: cmp.eq assms(3, 4))
hence "rep_nat_term u = rep_nat_term v" using assms(5) by (rule prod_eqI)
hence "u = v" by (rule rep_nat_term_inj)
thus ?thesis by (simp add: Eq)
next
case Lt
with assms(2, 3, 4, 5, 6) have "cmp u v = Lt" by (rule nat_term_compD4)
thus ?thesis by (simp add: Lt)
next
case Gt
hence "cmp b a = Lt" by (simp only: cmp.Gt_lt_conv cmp.Lt_lt_conv)
with assms(2, 4, 3) assms(5, 6)[symmetric] have "cmp v u = Lt" by (rule nat_term_compD4)
hence "cmp u v = Gt" by (simp only: cmp.Gt_lt_conv cmp.Lt_lt_conv)
thus ?thesis by (simp add: Gt)
qed
qed
lemma nat_term_compD4'':
assumes "comparator cmp" and "nat_term_comp cmp" and "fst (rep_nat_term u) = fst (rep_nat_term a)"
and "fst (rep_nat_term v) = fst (rep_nat_term b)" and "snd (rep_nat_term u) ≤ snd (rep_nat_term v)"
and "snd (rep_nat_term a) = snd (rep_nat_term b)" and "cmp a b ≠ Gt"
shows "cmp u v ≠ Gt"
proof (cases "snd (rep_nat_term u) = snd (rep_nat_term v)")
case True
with assms(1, 2, 3, 4) have "cmp u v = cmp a b" using assms(6) by (rule nat_term_compD4')
thus ?thesis using assms(7) by simp
next
case False
from assms(1) interpret cmp: comparator cmp .
from refl obtain w::'a where w: "rep_nat_term w = (fst (rep_nat_term u), snd (rep_nat_term v))"
by (rule full_componentE)
have 1: "fst (rep_nat_term w) = fst (rep_nat_term a)" and 2: "snd (rep_nat_term w) = snd (rep_nat_term v)"
by (simp_all add: w assms(3))
from False assms(5) have *: "snd (rep_nat_term u) < snd (rep_nat_term v)" by simp
have "cmp u w = Lt" by (rule nat_term_compD2, fact assms(2), simp_all add: * w)
moreover from assms(1, 2) 1 assms(4) 2 assms(6) have "cmp w v = cmp a b" by (rule nat_term_compD4')
ultimately show ?thesis using assms(7) by (metis cmp.nGt_le_conv cmp.nLt_le_conv cmp.comp_trans)
qed
lemma comparator_lex_comp_aux: "comparator (lex_comp_aux::'a::nat_term comparator)"
unfolding lex_comp_aux_def
proof (rule comparator_composition)
from lex_pp_antisym have as: "antisymp lex_pp" by (rule antisympI)
have "comparator (comp_of_ord (lex_pp::(nat, nat) pp ⇒ _))"
unfolding comp_of_ord_eq_comp_of_ords[OF as]
by (rule comp_of_ords, unfold_locales,
auto simp: lex_pp_refl intro: lex_pp_trans lex_pp_lin' elim!: lex_pp_antisym)
thus "comparator (λx y::((nat, nat) pp × nat). case comp_of_ord lex_pp (fst x) (fst y) of
Eq ⇒ comparator_of (snd x) (snd y) | val ⇒ val)"
using comparator_of prod_eqI by (rule comparator_lexicographic)
next
from rep_nat_term_inj show "inj rep_nat_term" by (rule injI)
qed
lemma nat_term_comp_lex_comp_aux: "nat_term_comp (lex_comp_aux::'a::nat_term comparator)"
proof -
from lex_pp_antisym have as: "antisymp lex_pp" by (rule antisympI)
interpret lex: comparator "comp_of_ord (lex_pp::(nat, nat) pp ⇒ _)"
unfolding comp_of_ord_eq_comp_of_ords[OF as]
by (rule comp_of_ords, unfold_locales,
auto simp: lex_pp_refl intro: lex_pp_trans lex_pp_lin' elim!: lex_pp_antisym)
show ?thesis
proof (rule nat_term_compI)
fix u v :: 'a
assume 1: "snd (rep_nat_term u) = snd (rep_nat_term v)" and 2: "fst (rep_nat_term u) = 0"
show "lex_comp_aux u v ≠ Gt"
by (simp add: lex_comp_aux_def 1 2 split: order.split, simp add: comp_of_ord_def lex_pp_zero_min)
next
fix u v :: 'a
assume 1: "fst (rep_nat_term u) = fst (rep_nat_term v)" and 2: "snd (rep_nat_term u) < snd (rep_nat_term v)"
show "lex_comp_aux u v = Lt"
by (simp add: lex_comp_aux_def 1 split: order.split, simp add: comparator_of_def 2)
next
fix t u v :: 'a
show "lex_comp_aux u v = Lt ⟹ lex_comp_aux (splus t u) (splus t v) = Lt"
by (auto simp: lex_comp_aux_def splus_term pprod.splus_def comp_of_ord_def lex_pp_refl
split: order.splits if_splits intro: lex_pp_plus_monotone')
next
fix u v a b :: 'a
assume "fst (rep_nat_term u) = fst (rep_nat_term a)" and "fst (rep_nat_term v) = fst (rep_nat_term b)"
and "snd (rep_nat_term a) = snd (rep_nat_term b)" and "lex_comp_aux a b = Lt"
thus "lex_comp_aux u v = Lt" by (simp add: lex_comp_aux_def split: order.splits)
qed
qed
typedef (overloaded) 'a nat_term_order =
"{cmp::'a::nat_term comparator. comparator cmp ∧ nat_term_comp cmp}"
morphisms nat_term_compare Abs_nat_term_order
proof (rule, simp)
from comparator_lex_comp_aux nat_term_comp_lex_comp_aux
show "comparator lex_comp_aux ∧ nat_term_comp lex_comp_aux" ..
qed
lemma nat_term_compare_Abs_nat_term_order_id:
assumes "comparator cmp" and "nat_term_comp cmp"
shows "nat_term_compare (Abs_nat_term_order cmp) = cmp"
by (rule Abs_nat_term_order_inverse, simp add: assms)
instantiation nat_term_order :: (type) equal
begin
definition equal_nat_term_order :: "'a nat_term_order ⇒ 'a nat_term_order ⇒ bool" where "equal_nat_term_order = (=)"
instance by (standard, simp add: equal_nat_term_order_def)
end
definition nat_term_compare_inv :: "'a nat_term_order ⇒ 'a::nat_term comparator"
where "nat_term_compare_inv to = (λx y. nat_term_compare to y x)"
definition key_order_of_nat_term_order :: "'a nat_term_order ⇒ 'a::nat_term key_order"
where key_order_of_nat_term_order_def [code del]:
"key_order_of_nat_term_order to = Abs_key_order (nat_term_compare to)"
definition key_order_of_nat_term_order_inv :: "'a nat_term_order ⇒ 'a::nat_term key_order"
where key_order_of_nat_term_order_inv_def [code del]:
"key_order_of_nat_term_order_inv to = Abs_key_order (nat_term_compare_inv to)"
definition le_of_nat_term_order :: "'a nat_term_order ⇒ 'a ⇒ 'a::nat_term ⇒ bool"
where "le_of_nat_term_order to = le_of_key_order (key_order_of_nat_term_order to)"
definition lt_of_nat_term_order :: "'a nat_term_order ⇒ 'a ⇒ 'a::nat_term ⇒ bool"
where "lt_of_nat_term_order to = lt_of_key_order (key_order_of_nat_term_order to)"
definition nat_term_order_of_le :: "'a::{linorder,nat_term} nat_term_order"
where "nat_term_order_of_le = Abs_nat_term_order (comparator_of)"
lemma comparator_nat_term_compare: "comparator (nat_term_compare to)"
using nat_term_compare by blast
lemma nat_term_comp_nat_term_compare: "nat_term_comp (nat_term_compare to)"
using nat_term_compare by blast
lemma nat_term_compare_splus: "nat_term_compare to (splus t u) (splus t v) = nat_term_compare to u v"
proof -
from comparator_nat_term_compare interpret cmp: comparator "nat_term_compare to" .
show ?thesis
proof (cases "nat_term_compare to u v")
case Eq
hence "splus t u = splus t v" by (simp add: cmp.eq)
thus ?thesis by (simp add: cmp.eq Eq)
next
case Lt
moreover from nat_term_comp_nat_term_compare this have "nat_term_compare to (splus t u) (splus t v) = Lt"
by (rule nat_term_compD3)
ultimately show ?thesis by simp
next
case Gt
hence "nat_term_compare to v u = Lt" using cmp.Gt_lt_conv cmp.Lt_lt_conv by auto
with nat_term_comp_nat_term_compare have "nat_term_compare to (splus t v) (splus t u) = Lt"
by (rule nat_term_compD3)
hence "nat_term_compare to (splus t u) (splus t v) = Gt" using cmp.Gt_lt_conv cmp.Lt_lt_conv by auto
with Gt show ?thesis by simp
qed
qed
lemma nat_term_compare_conv: "nat_term_compare to = key_compare (key_order_of_nat_term_order to)"
unfolding key_order_of_nat_term_order_def
by (rule sym, rule Abs_key_order_inverse, simp add: comparator_nat_term_compare)
lemma comparator_nat_term_compare_inv: "comparator (nat_term_compare_inv to)"
unfolding nat_term_compare_inv_def using comparator_nat_term_compare by (rule comparator_converse)
lemma nat_term_compare_inv_conv: "nat_term_compare_inv to = key_compare (key_order_of_nat_term_order_inv to)"
unfolding key_order_of_nat_term_order_inv_def
by (rule sym, rule Abs_key_order_inverse, simp add: comparator_nat_term_compare_inv)
lemma nat_term_compare_inv_alt [code_unfold]: "nat_term_compare_inv to x y = nat_term_compare to y x"
by (simp only: nat_term_compare_inv_def)
lemma le_of_nat_term_order [code]: "le_of_nat_term_order to x y = (nat_term_compare to x y ≠ Gt)"
by (simp add: le_of_key_order_alt le_of_nat_term_order_def nat_term_compare_conv)
lemma lt_of_nat_term_order [code]: "lt_of_nat_term_order to x y = (nat_term_compare to x y = Lt)"
by (simp add: lt_of_key_order_alt lt_of_nat_term_order_def nat_term_compare_conv)
lemma le_of_nat_term_order_alt:
"le_of_nat_term_order to = (λu v. ko.le (key_order_of_nat_term_order_inv to) v u)"
by (intro ext, simp add: le_of_comp_def nat_term_compare_inv_conv[symmetric] le_of_nat_term_order_def
le_of_key_order_def nat_term_compare_conv[symmetric] nat_term_compare_inv_alt)
lemma lt_of_nat_term_order_alt:
"lt_of_nat_term_order to = (λu v. ko.lt (key_order_of_nat_term_order_inv to) v u)"
by (intro ext, simp add: lt_of_comp_def nat_term_compare_inv_conv[symmetric] lt_of_nat_term_order_def
lt_of_key_order_def nat_term_compare_conv[symmetric] nat_term_compare_inv_alt)
lemma linorder_le_of_nat_term_order: "class.linorder (le_of_nat_term_order to) (lt_of_nat_term_order to)"
unfolding le_of_nat_term_order_alt lt_of_nat_term_order_alt using ko.linorder
by (rule linorder.dual_linorder)
lemma le_of_nat_term_order_zero_min: "le_of_nat_term_order to 0 (t::'a::nat_pp_term)"
unfolding le_of_nat_term_order
by (rule nat_term_compD1', fact comparator_nat_term_compare, fact nat_term_comp_nat_term_compare, simp_all add: rep_nat_term_zero)
lemma le_of_nat_term_order_plus_monotone:
assumes "le_of_nat_term_order to s (t::'a::nat_pp_term)"
shows "le_of_nat_term_order to (u + s) (u + t)"
using assms by (simp add: le_of_nat_term_order splus_pp_term[symmetric] nat_term_compare_splus)