Theory Landau_Symbols.Group_Sort
section ‹Sorting and grouping factors›
theory Group_Sort
imports Main "HOL-Library.Multiset"
begin
text ‹
For the reification of products of powers of primitive functions such as
@{term "λx. x * ln x ^2"} into a canonical form, we need to be able to sort the factors
according to the growth of the primitive function it contains and merge terms with the same
function by adding their exponents. The following locale defines such an operation in a
general setting; we can then instantiate it for our setting.
The locale takes as parameters a key function @{term "f"} that sends list elements into a
linear ordering that determines the sorting order, a @{term "merge"} function to merge to
equivalent (w.r.t. @{term "f"}) elements into one, and a list reduction function @{term "g"}
that reduces a list to a single value. This function must be invariant w.r.t. the order of
list elements and be compatible with merging of equivalent elements. In our case, this list
reduction function will be the product of all list elements.
›
locale groupsort =
fixes f :: "'a ⇒ ('b::linorder)"
fixes merge :: "'a ⇒ 'a ⇒ 'a"
fixes g :: "'a list ⇒ 'c"
assumes f_merge: "f x = f y ⟹ f (merge x y) = f x"
assumes g_cong: "mset xs = mset ys ⟹ g xs = g ys"
assumes g_merge: "f x = f y ⟹ g [x,y] = g [merge x y]"
assumes g_append_cong: "g xs1 = g xs2 ⟹ g ys1 = g ys2 ⟹ g (xs1 @ ys1) = g (xs2 @ ys2)"
begin
context
begin
private function part_aux ::
"'b ⇒ 'a list ⇒ ('a list) × ('a list) × ('a list) ⇒ ('a list) × ('a list) × ('a list)"
where
"part_aux p [] (ls, eq, gs) = (ls, eq, gs)"
| "f x < p ⟹ part_aux p (x#xs) (ls, eq, gs) = part_aux p xs (x#ls, eq, gs)"
| "f x > p ⟹ part_aux p (x#xs) (ls, eq, gs) = part_aux p xs (ls, eq, x#gs)"
| "f x = p ⟹ part_aux p (x#xs) (ls, eq, gs) = part_aux p xs (ls, eq@[x], gs)"
proof (clarify, goal_cases)
case prems: (1 P p xs ls eq gs)
show ?case
proof (cases xs)
fix x xs' assume "xs = x # xs'"
thus ?thesis using prems by (cases "f x" p rule: linorder_cases) auto
qed (auto intro: prems(1))
qed simp_all
termination by (relation "Wellfounded.measure (size ∘ fst ∘ snd)") simp_all
private lemma groupsort_locale: "groupsort f merge g" by unfold_locales
private lemmas part_aux_induct = part_aux.induct[split_format (complete), OF groupsort_locale]
private definition part where "part p xs = part_aux (f p) xs ([], [p], [])"
private lemma part:
"part p xs = (rev (filter (λx. f x < f p) xs),
p # filter (λx. f x = f p) xs, rev (filter (λx. f x > f p) xs))"
proof-
{
fix p xs ls eq gs
have "fst (part_aux p xs (ls, eq, gs)) = rev (filter (λx. f x < p) xs) @ ls"
by (induction p xs ls eq gs rule: part_aux_induct) simp_all
} note A = this
{
fix p xs ls eq gs
have "snd (snd (part_aux p xs (ls, eq, gs))) = rev (filter (λx. f x > p) xs) @ gs"
by (induction p xs ls eq gs rule: part_aux_induct) simp_all
} note B = this
{
fix p xs ls eq gs
have "fst (snd (part_aux p xs (ls, eq, gs))) = eq @ filter (λx. f x = p) xs"
by (induction p xs ls eq gs rule: part_aux_induct) auto
} note C = this
note ABC = A B C
from ABC[of "f p" xs "[]" "[p]" "[]"] show ?thesis unfolding part_def
by (intro prod_eqI) simp_all
qed
private function sort :: "'a list ⇒ 'a list" where
"sort [] = []"
| "sort (x#xs) = (case part x xs of (ls, eq, gs) ⇒ sort ls @ eq @ sort gs)"
by pat_completeness simp_all
termination by (relation "Wellfounded.measure length") (simp_all add: part less_Suc_eq_le)
private lemma filter_mset_union:
assumes "⋀x. x ∈# A ⟹ P x ⟹ Q x ⟹ False"
shows "filter_mset P A + filter_mset Q A = filter_mset (λx. P x ∨ Q x) A" (is "?lhs = ?rhs")
using assms by (auto simp add: count_eq_zero_iff intro!: multiset_eqI) blast
private lemma multiset_of_sort: "mset (sort xs) = mset xs"
proof (induction xs rule: sort.induct)
case (2 x xs)
let ?M = "λoper. {#y:# mset xs. oper (f y) (f x)#}"
from 2 have "mset (sort (x#xs)) = ?M (<) + ?M (=) + ?M (>) + {#x#}"
by (simp add: part Multiset.union_assoc mset_filter)
also have "?M (<) + ?M (=) + ?M (>) = mset xs"
by ((subst filter_mset_union, force)+, subst multiset_eq_iff, force)
finally show ?case by simp
qed simp
private lemma g_sort: "g (sort xs) = g xs"
by (intro g_cong multiset_of_sort)
private lemma set_sort: "set (sort xs) = set xs"
using arg_cong[OF multiset_of_sort[of xs], of "set_mset"] by (simp only: set_mset_mset)
private lemma sorted_all_equal: "(⋀x. x ∈ set xs ⟹ x = y) ⟹ sorted xs"
by (induction xs) (auto)
private lemma sorted_sort: "sorted (map f (sort xs))"
apply (induction xs rule: sort.induct)
apply simp
apply (simp only: sorted_append sort.simps part map_append split)
apply (intro conjI TrueI)
using sorted_map_same by (auto simp: set_sort)
private fun group where
"group [] = []"
| "group (x#xs) = (case partition (λy. f y = f x) xs of (xs', xs'') ⇒
fold merge xs' x # group xs'')"
private lemma f_fold_merge: "(⋀y. y ∈ set xs ⟹ f y = f x) ⟹ f (fold merge xs x) = f x"
by (induction xs rule: rev_induct) (auto simp: f_merge)
private lemma f_group: "x ∈ set (group xs) ⟹ ∃x'∈set xs. f x = f x'"
proof (induction xs rule: group.induct)
case (2 x' xs)
hence "x = fold merge [y←xs . f y = f x'] x' ∨ x ∈ set (group [xa←xs . f xa ≠ f x'])"
by (auto simp: o_def)
thus ?case
proof
assume "x = fold merge [y←xs . f y = f x'] x'"
also have "f ... = f x'" by (rule f_fold_merge) simp
finally show ?thesis by simp
next
assume "x ∈ set (group [xa←xs . f xa ≠ f x'])"
from 2(1)[OF _ this] have "∃x'∈set [xa←xs . f xa ≠ f x']. f x = f x'" by (simp add: o_def)
thus ?thesis by force
qed
qed simp
private lemma sorted_group: "sorted (map f xs) ⟹ sorted (map f (group xs))"
proof (induction xs rule: group.induct)
case (2 x xs)
{
fix x' assume x': "x' ∈ set (group [y←xs . f y ≠ f x])"
with f_group obtain x'' where x'': "x'' ∈ set xs" "f x' = f x''" by force
have "f (fold merge [y←xs . f y = f x] x) = f x"
by (subst f_fold_merge) simp_all
also from 2(2) x'' have "... ≤ f x'" by (auto)
finally have "f (fold merge [y←xs . f y = f x] x) ≤ f x'" .
}
moreover from 2(2) have "sorted (map f (group [xa←xs . f xa ≠ f x]))"
by (intro 2 sorted_filter) (simp_all add: o_def)
ultimately show ?case by (simp add: o_def)
qed simp_all
private lemma distinct_group: "distinct (map f (group xs))"
proof (induction xs rule: group.induct)
case (2 x xs)
have "distinct (map f (group [xa←xs . f xa ≠ f x]))" by (intro 2) (simp_all add: o_def)
moreover have "f (fold merge [y←xs . f y = f x] x) ∉ set (map f (group [xa←xs . f xa ≠ f x]))"
by (rule notI, subst (asm) f_fold_merge) (auto dest: f_group)
ultimately show ?case by (simp add: o_def)
qed simp
private lemma g_fold_same:
assumes "⋀z. z ∈ set xs ⟹ f z = f x"
shows "g (fold merge xs x # ys) = g (x#xs@ys)"
using assms
proof (induction xs arbitrary: x)
case (Cons y xs)
have "g (x # y # xs @ ys) = g (y # x # xs @ ys)" by (intro g_cong) (auto simp: add_ac)
also have "y # x # xs @ ys = [y,x] @ xs @ ys" by simp
also from Cons.prems have "g ... = g ([merge y x] @ xs @ ys)"
by (intro g_append_cong g_merge) auto
also have "[merge y x] @ xs @ ys = merge y x # xs @ ys" by simp
also from Cons.prems have "g ... = g (fold merge xs (merge y x) # ys)"
by (intro Cons.IH[symmetric]) (auto simp: f_merge)
also have "... = g (fold merge (y # xs) x # ys)" by simp
finally show ?case by simp
qed simp
private lemma g_group: "g (group xs) = g xs"
proof (induction xs rule: group.induct)
case (2 x xs)
have "g (group (x#xs)) = g (fold merge [y←xs . f y = f x] x # group [xa←xs . f xa ≠ f x])"
by (simp add: o_def)
also have "... = g (x # [y←xs . f y = f x] @ group [y←xs . f y ≠ f x])"
by (intro g_fold_same) simp_all
also have "... = g ((x # [y←xs . f y = f x]) @ group [y←xs . f y ≠ f x])" (is "_ = ?A") by simp
also from 2 have "g (group [y←xs . f y ≠ f x]) = g [y←xs . f y ≠ f x]" by (simp add: o_def)
hence "?A = g ((x # [y←xs . f y = f x]) @ [y←xs . f y ≠ f x])"
by (intro g_append_cong) simp_all
also have "... = g (x#xs)" by (intro g_cong) (simp_all)
finally show ?case .
qed simp
function group_part_aux ::
"'b ⇒ 'a list ⇒ ('a list) × 'a × ('a list) ⇒ ('a list) × 'a × ('a list)"
where
"group_part_aux p [] (ls, eq, gs) = (ls, eq, gs)"
| "f x < p ⟹ group_part_aux p (x#xs) (ls, eq, gs) = group_part_aux p xs (x#ls, eq, gs)"
| "f x > p ⟹ group_part_aux p (x#xs) (ls, eq, gs) = group_part_aux p xs (ls, eq, x#gs)"
| "f x = p ⟹ group_part_aux p (x#xs) (ls, eq, gs) = group_part_aux p xs (ls, merge x eq, gs)"
proof (clarify, goal_cases)
case prems: (1 P p xs ls eq gs)
show ?case
proof (cases xs)
fix x xs' assume "xs = x # xs'"
thus ?thesis using prems by (cases "f x" p rule: linorder_cases) auto
qed (auto intro: prems(1))
qed simp_all
termination by (relation "Wellfounded.measure (size ∘ fst ∘ snd)") simp_all
private lemmas group_part_aux_induct =
group_part_aux.induct[split_format (complete), OF groupsort_locale]
definition group_part where "group_part p xs = group_part_aux (f p) xs ([], p, [])"
private lemma group_part:
"group_part p xs = (rev (filter (λx. f x < f p) xs),
fold merge (filter (λx. f x = f p) xs) p, rev (filter (λx. f x > f p) xs))"
proof-
{
fix p xs ls eq gs
have "fst (group_part_aux p xs (ls, eq, gs)) = rev (filter (λx. f x < p) xs) @ ls"
by (induction p xs ls eq gs rule: group_part_aux_induct) simp_all
} note A = this
{
fix p xs ls eq gs
have "snd (snd (group_part_aux p xs (ls, eq, gs))) = rev (filter (λx. f x > p) xs) @ gs"
by (induction p xs ls eq gs rule: group_part_aux_induct) simp_all
} note B = this
{
fix p xs ls eq gs
have "fst (snd (group_part_aux p xs (ls, eq, gs))) =
fold merge (filter (λx. f x = p) xs) eq"
by (induction p xs ls eq gs rule: group_part_aux_induct) auto
} note C = this
note ABC = A B C
from ABC[of "f p" xs "[]" "p" "[]"] show ?thesis unfolding group_part_def
by (intro prod_eqI) simp_all
qed
function group_sort :: "'a list ⇒ 'a list" where
"group_sort [] = []"
| "group_sort (x#xs) = (case group_part x xs of (ls, eq, gs) ⇒ group_sort ls @ eq # group_sort gs)"
by pat_completeness simp_all
termination by (relation "Wellfounded.measure length") (simp_all add: group_part less_Suc_eq_le)
private lemma group_append:
assumes "⋀x y. x ∈ set xs ⟹ y ∈ set ys ⟹ f x ≠ f y"
shows "group (xs @ ys) = group xs @ group ys"
using assms
proof (induction xs arbitrary: ys rule: length_induct)
case (1 xs')
hence IH: "⋀x xs ys. length xs < length xs' ⟹ (⋀x y. x ∈ set xs ⟹ y ∈ set ys ⟹ f x ≠ f y)
⟹ group (xs @ ys) = group xs @ group ys" by blast
show ?case
proof (cases xs')
case (Cons x xs)
note [simp] = this
have "group (xs' @ ys) = fold merge [y←xs@ys . f y = f x] x #
group ([xa←xs . f xa ≠ f x] @ [xa←ys . f xa ≠ f x])" by (simp add: o_def)
also from 1(2) have "[y←xs@ys . f y = f x] = [y←xs . f y = f x]"
by (force simp: filter_empty_conv)
also from 1(2) have "[xa←ys . f xa ≠ f x] = ys" by (force simp: filter_id_conv)
also have "group ([xa←xs . f xa ≠ f x] @ ys) =
group [xa←xs . f xa ≠ f x] @ group ys" using 1(2)
by (intro IH) (simp_all add: less_Suc_eq_le)
finally show ?thesis by (simp add: o_def)
qed simp
qed
private lemma group_empty_iff [simp]: "group xs = [] ⟷ xs = []"
by (induction xs rule: group.induct) auto
lemma group_sort_correct: "group_sort xs = group (sort xs)"
proof (induction xs rule: group_sort.induct)
case (2 x xs)
have "group_sort (x#xs) =
group_sort (rev [xa←xs . f xa < f x]) @ group (x#[xa←xs . f xa = f x]) @
group_sort (rev [xa←xs . f x < f xa])" by (simp add: group_part)
also have "group_sort (rev [xa←xs . f xa < f x]) = group (sort (rev [xa←xs . f xa < f x]))"
by (rule 2) (simp_all add: group_part)
also have "group_sort (rev [xa←xs . f xa > f x]) = group (sort (rev [xa←xs . f xa > f x]))"
by (rule 2) (simp_all add: group_part)
also have "group (x#[xa←xs . f xa = f x]) @ group (sort (rev [xa←xs . f xa > f x])) =
group ((x#[xa←xs . f xa = f x]) @ sort (rev [xa←xs . f xa > f x]))"
by (intro group_append[symmetric]) (auto simp: set_sort)
also have "group (sort (rev [xa←xs . f xa < f x])) @ ... =
group (sort (rev [xa←xs . f xa < f x]) @ (x#[xa←xs . f xa = f x]) @
sort (rev [xa←xs . f xa > f x]))"
by (intro group_append[symmetric]) (auto simp: set_sort)
also have "sort (rev [xa←xs . f xa < f x]) @ (x#[xa←xs . f xa = f x]) @
sort (rev [xa←xs . f xa > f x]) = sort (x # xs)" by (simp add: part)
finally show ?case .
qed simp
lemma sorted_group_sort: "sorted (map f (group_sort xs))"
by (auto simp: group_sort_correct intro!: sorted_group sorted_sort)
lemma distinct_group_sort: "distinct (map f (group_sort xs))"
by (simp add: group_sort_correct distinct_group)
lemma g_group_sort: "g (group_sort xs) = g xs"
by (simp add: group_sort_correct g_group g_sort)
lemmas [simp del] = group_sort.simps group_part_aux.simps
end
end
end