# Theory Collection_Order

(* Title:      Containers/Collection_Order.thy
Author:     Andreas Lochbihler, KIT
René Thiemann, UIBK *)

theory Collection_Order
imports
Set_Linorder
Containers_Generator
Deriving.Compare_Instances
begin

chapter ‹Light-weight containers›
text_raw ‹\label{chapter:light-weight:containers}›

section ‹A linear order for code generation›

subsection ‹Optional comparators›

class ccompare =
fixes ccompare :: "'a comparator option"
assumes ccompare: "⋀ comp. ccompare = Some comp ⟹ comparator comp"
begin
abbreviation ccomp :: "'a comparator" where "ccomp ≡ the (ID ccompare)"
abbreviation cless :: "'a ⇒ 'a ⇒ bool" where "cless ≡ lt_of_comp (the (ID ccompare))"
abbreviation cless_eq :: "'a ⇒ 'a ⇒ bool" where "cless_eq ≡ le_of_comp (the (ID ccompare))"
end

lemma (in ccompare) ID_ccompare':
"⋀c. ID ccompare = Some c ⟹ comparator c"
unfolding ID_def id_apply using ccompare by simp

lemma (in ccompare) ID_ccompare:
"⋀c. ID ccompare = Some c ⟹ class.linorder (le_of_comp c) (lt_of_comp c)"
by (rule comparator.linorder[OF ID_ccompare'])

syntax "_CCOMPARE" :: "type => logic"  ("(1CCOMPARE/(1'(_')))")

parse_translation ‹
let
fun ccompare_tr [ty] =
(Syntax.const @{syntax_const "_constrain"} $Syntax.const @{const_syntax "ccompare"}$
(Syntax.const @{type_syntax option} $(Syntax.const @{type_syntax fun}$ ty $(Syntax.const @{type_syntax fun}$ ty \$ Syntax.const @{type_syntax order}))))
| ccompare_tr ts = raise TERM ("ccompare_tr", ts);
in [(@{syntax_const "_CCOMPARE"}, K ccompare_tr)] end
›

definition is_ccompare :: "'a :: ccompare itself ⇒ bool"
where "is_ccompare _ ⟷ ID CCOMPARE('a) ≠ None"

context ccompare
begin
lemma cless_eq_conv_cless:
fixes a b :: "'a"
assumes "ID CCOMPARE('a) ≠ None"
shows "cless_eq a b ⟷ cless a b ∨ a = b"
proof -
from assms interpret linorder cless_eq "cless :: 'a ⇒ 'a ⇒ bool"
show ?thesis by(rule le_less)
qed
end

subsection ‹Generator for the @{class ccompare}--class›

text ‹
This generator registers itself at the derive-manager for the class
@{class ccompare}. To be more precise, one can choose whether one does not want to
support a comparator by passing parameter "no", one wants to register an arbitrary type which
is already in class @{class compare} using parameter "compare", or
one wants to generate a new comparator by passing no parameter.
In the last case, one demands that the type is a datatype
and that all non-recursive types of that datatype already provide a comparator,
which can usually be achieved via "derive comparator type" or "derive compare type".

\begin{itemize}
\item \texttt{instantiation type :: (type,\ldots,type) (no) corder}
\item \texttt{instantiation datatype :: (type,\ldots,type) corder}
\item \texttt{instantiation datatype :: (compare,\ldots,compare) (compare) corder}
\end{itemize}

If the parameter "no" is not used, then the corresponding
@{const is_ccompare}-theorem is automatically generated and attributed with
\texttt{[simp, code-post]}.
›

text ‹
To create a new comparator, we just invoke the functionality provided by the generator.
The only difference is the boilerplate-code, which for the generator has to perform
the class instantiation for a comparator, whereas here we have to invoke the methods to
satisfy the corresponding locale for comparators.
›

text ‹
This generator can be used for arbitrary types, not just datatypes.
When passing no parameters, we get same limitation as for the order generator.
›

lemma corder_intro: "class.linorder le lt ⟹ a = Some (le, lt)⟹ a = Some (le',lt') ⟹
class.linorder le' lt'" by auto

lemma comparator_subst: "c1 = c2 ⟹ comparator c1 ⟹ comparator c2" by blast

lemma (in compare) compare_subst: "⋀ comp. compare = comp ⟹ comparator comp"
using comparator_compare by blast

ML_file ‹ccompare_generator.ML›

subsection ‹Instantiations for HOL types›

derive (linorder) compare_order
Enum.finite_1 Enum.finite_2 Enum.finite_3 natural String.literal
derive (compare) ccompare
unit bool nat int Enum.finite_1 Enum.finite_2 Enum.finite_3 integer natural char String.literal
derive (no) ccompare Enum.finite_4 Enum.finite_5

derive ccompare sum list option prod

derive (no) ccompare "fun"

lemma is_ccompare_fun [simp]: "¬ is_ccompare TYPE('a ⇒ 'b)"

instantiation set :: (ccompare) ccompare begin
definition "CCOMPARE('a set) =
map_option (λ c. comp_of_ords (ord.set_less_eq (le_of_comp c)) (ord.set_less (le_of_comp c))) (ID CCOMPARE('a))"
instance by(intro_classes)(auto simp add: ccompare_set_def intro: comp_of_ords linorder.set_less_eq_linorder ID_ccompare)
end

lemma is_ccompare_set [simp, code_post]:
"is_ccompare TYPE('a set) ⟷ is_ccompare TYPE('a :: ccompare)"

definition cless_eq_set :: "'a :: ccompare set ⇒ 'a set ⇒ bool"
where [simp, code del]: "cless_eq_set = le_of_comp (the (ID CCOMPARE('a set)))"

definition cless_set :: "'a :: ccompare set ⇒ 'a set ⇒ bool"
where [simp, code del]: "cless_set = lt_of_comp (the (ID CCOMPARE('a set)))"

lemma ccompare_set_code [code]:
"CCOMPARE('a :: ccompare set) =
(case ID CCOMPARE('a) of None ⇒ None | Some _ ⇒ Some (comp_of_ords cless_eq_set cless_set))"
by (clarsimp simp add: ccompare_set_def ID_Some split: option.split)

derive (no) ccompare Predicate.pred

subsection ‹Proper intervals›

class cproper_interval = ccompare +
fixes cproper_interval :: "'a option ⇒ 'a option ⇒ bool"
assumes cproper_interval:
"⟦ ID CCOMPARE('a) ≠ None; finite (UNIV :: 'a set) ⟧
⟹ class.proper_interval cless cproper_interval"
begin

lemma ID_ccompare_interval:
"⟦ ID CCOMPARE('a) = Some c; finite (UNIV :: 'a set) ⟧
⟹ class.linorder_proper_interval (le_of_comp c) (lt_of_comp c) cproper_interval"
using cproper_interval

end

instantiation unit :: cproper_interval begin
definition "cproper_interval = (proper_interval :: unit proper_interval)"
instance by intro_classes (simp add: compare_order_class.ord_defs cproper_interval_unit_def ccompare_unit_def ID_Some proper_interval_class.axioms)
end

instantiation bool :: cproper_interval begin
definition "cproper_interval = (proper_interval :: bool proper_interval)"
instance by(intro_classes)
(simp add: cproper_interval_bool_def ord_defs ccompare_bool_def ID_Some proper_interval_class.axioms)
end

instantiation nat :: cproper_interval begin
definition "cproper_interval = (proper_interval :: nat proper_interval)"
instance by intro_classes simp
end

instantiation int :: cproper_interval begin
definition "cproper_interval = (proper_interval :: int proper_interval)"
instance by intro_classes
(simp add: cproper_interval_int_def ord_defs ccompare_int_def ID_Some proper_interval_class.axioms)
end

instantiation integer :: cproper_interval begin
definition "cproper_interval = (proper_interval :: integer proper_interval)"
instance by intro_classes
(simp add: cproper_interval_integer_def ord_defs ccompare_integer_def ID_Some proper_interval_class.axioms)
end

instantiation natural :: cproper_interval begin
definition "cproper_interval = (proper_interval :: natural proper_interval)"
instance by intro_classes (simp add: cproper_interval_natural_def ord_defs ccompare_natural_def ID_Some proper_interval_class.axioms)
end

instantiation char :: cproper_interval begin
definition "cproper_interval = (proper_interval :: char proper_interval)"
instance by intro_classes (simp add: cproper_interval_char_def ord_defs ccompare_char_def ID_Some proper_interval_class.axioms)
end

instantiation Enum.finite_1 :: cproper_interval begin
definition "cproper_interval = (proper_interval :: Enum.finite_1 proper_interval)"
instance by intro_classes (simp add: cproper_interval_finite_1_def ord_defs ccompare_finite_1_def ID_Some proper_interval_class.axioms)
end

instantiation Enum.finite_2 :: cproper_interval begin
definition "cproper_interval = (proper_interval :: Enum.finite_2 proper_interval)"
instance by intro_classes (simp add: cproper_interval_finite_2_def ord_defs ccompare_finite_2_def ID_Some proper_interval_class.axioms)
end

instantiation Enum.finite_3 :: cproper_interval begin
definition "cproper_interval = (proper_interval :: Enum.finite_3 proper_interval)"
instance by intro_classes (simp add: cproper_interval_finite_3_def ord_defs ccompare_finite_3_def ID_Some proper_interval_class.axioms)
end

instantiation Enum.finite_4 :: cproper_interval begin
definition "(cproper_interval :: Enum.finite_4 proper_interval) _ _ = undefined"
instance by intro_classes(simp add: ord_defs ccompare_finite_4_def ID_None)
end

instantiation Enum.finite_5 :: cproper_interval begin
definition "(cproper_interval :: Enum.finite_5 proper_interval) _ _ = undefined"
instance by intro_classes(simp add: ord_defs ccompare_finite_5_def ID_None)
end

lemma lt_of_comp_sum: "lt_of_comp (comparator_sum ca cb) sx sy = (
case sx of Inl x ⇒ (case sy of Inl y ⇒ lt_of_comp ca x y | Inr y ⇒ True)
| Inr x ⇒ (case sy of Inl y ⇒ False | Inr y ⇒ lt_of_comp cb x y))"
by (simp add: lt_of_comp_def le_of_comp_def split: sum.split)

instantiation sum :: (cproper_interval, cproper_interval) cproper_interval begin
fun cproper_interval_sum :: "('a + 'b) proper_interval" where
"cproper_interval_sum None None ⟷ True"
| "cproper_interval_sum None (Some (Inl x)) ⟷ cproper_interval None (Some x)"
| "cproper_interval_sum None (Some (Inr y)) ⟷ True"
| "cproper_interval_sum (Some (Inl x)) None ⟷ True"
| "cproper_interval_sum (Some (Inl x)) (Some (Inl y)) ⟷ cproper_interval (Some x) (Some y)"
| "cproper_interval_sum (Some (Inl x)) (Some (Inr y)) ⟷ cproper_interval (Some x) None ∨ cproper_interval None (Some y)"
| "cproper_interval_sum (Some (Inr y)) None ⟷ cproper_interval (Some y) None"
| "cproper_interval_sum (Some (Inr y)) (Some (Inl x)) ⟷ False"
| "cproper_interval_sum (Some (Inr x)) (Some (Inr y)) ⟷ cproper_interval (Some x) (Some y)"
instance
proof
assume "ID CCOMPARE('a + 'b) ≠ None" "finite (UNIV :: ('a + 'b) set)"
then obtain c_a c_b
where A: "ID CCOMPARE('a) = Some c_a" "finite (UNIV :: 'a set)"
and B: "ID CCOMPARE('b) = Some c_b" "finite (UNIV :: 'b set)"
by(fastforce simp add: ccompare_sum_def ID_Some ID_None split: option.split_asm)
note [simp] = proper_interval.proper_interval_simps[OF cproper_interval]
lt_of_comp_sum ccompare_sum_def ID_Some
and [split] = sum.split
show "class.proper_interval cless (cproper_interval :: ('a + 'b) proper_interval)"
proof
fix y :: "'a + 'b"
show "cproper_interval None (Some y) = (∃z. cless z y)"
using A B by(cases y)(auto, case_tac z, auto)

fix x :: "'a + 'b"
show "cproper_interval (Some x) None = (∃z. cless x z)"
using A B by(cases x)(auto, case_tac z, auto)

show "cproper_interval (Some x) (Some y) = (∃z. cless x z ∧ cless z y)"
using A B by(cases x)(case_tac [!] y, auto, case_tac [!] z, auto)
qed simp
qed
end

lemma lt_of_comp_less_prod: "lt_of_comp (comparator_prod c_a c_b) =
less_prod (le_of_comp c_a) (lt_of_comp c_a) (lt_of_comp c_b)"
unfolding less_prod_def
by (intro ext, auto simp: lt_of_comp_def le_of_comp_def split: order.split_asm prod.split)

lemma lt_of_comp_prod: "lt_of_comp (comparator_prod c_a c_b) (x1,x2) (y1,y2) =
(lt_of_comp c_a x1 y1 ∨ le_of_comp c_a x1 y1 ∧ lt_of_comp c_b x2 y2)"
unfolding lt_of_comp_less_prod less_prod_def by simp

instantiation prod :: (cproper_interval, cproper_interval) cproper_interval begin
fun cproper_interval_prod :: "('a × 'b) proper_interval" where
"cproper_interval_prod None None ⟷ True"
| "cproper_interval_prod None (Some (y1, y2)) ⟷ cproper_interval None (Some y1) ∨ cproper_interval None (Some y2)"
| "cproper_interval_prod (Some (x1, x2)) None ⟷ cproper_interval (Some x1) None ∨ cproper_interval (Some x2) None"
| "cproper_interval_prod (Some (x1, x2)) (Some (y1, y2)) ⟷
cproper_interval (Some x1) (Some y1) ∨
cless x1 y1 ∧ (cproper_interval (Some x2) None ∨ cproper_interval None (Some y2)) ∨
¬ cless y1 x1 ∧ cproper_interval (Some x2) (Some y2)"
instance
proof
assume "ID CCOMPARE('a × 'b) ≠ None" "finite (UNIV :: ('a × 'b) set)"
then obtain c_a c_b
where A: "ID CCOMPARE('a) = Some c_a" "finite (UNIV :: 'a set)"
and B: "ID CCOMPARE('b) = Some c_b" "finite (UNIV :: 'b set)"
by(fastforce simp add: ccompare_prod_def ID_Some ID_None finite_prod split: option.split_asm)
interpret a: linorder "le_of_comp c_a" "lt_of_comp c_a" by(rule ID_ccompare)(rule A)
note [simp] = proper_interval.proper_interval_simps[OF cproper_interval]
ccompare_prod_def lt_of_comp_prod ID_Some
show "class.proper_interval cless (cproper_interval :: ('a × 'b) proper_interval)" using A B
by (unfold_locales, auto 4 4)
qed
end

instantiation list :: (ccompare) cproper_interval begin
definition cproper_interval_list :: "'a list proper_interval"
where "cproper_interval_list xso yso = undefined"
end

lemma infinite_UNIV_literal:
"infinite (UNIV :: String.literal set)"
by (fact infinite_literal)

instantiation String.literal :: cproper_interval begin
definition cproper_interval_literal :: "String.literal proper_interval"
where "cproper_interval_literal xso yso = undefined"
end

lemma lt_of_comp_option: "lt_of_comp (comparator_option c) sx sy = (
case sx of None ⇒ (case sy of None ⇒ False | Some y ⇒ True)
| Some x ⇒ (case sy of None ⇒ False | Some y ⇒ lt_of_comp c x y))"
by (simp add: lt_of_comp_def le_of_comp_def split: option.split)

instantiation option :: (cproper_interval) cproper_interval begin
fun cproper_interval_option :: "'a option proper_interval" where
"cproper_interval_option None None ⟷ True"
| "cproper_interval_option None (Some x) ⟷ x ≠ None"
| "cproper_interval_option (Some x) None ⟷ cproper_interval x None"
| "cproper_interval_option (Some x) (Some None) ⟷ False"
| "cproper_interval_option (Some x) (Some (Some y)) ⟷ cproper_interval x (Some y)"
instance
proof
assume "ID CCOMPARE('a option) ≠ None" "finite (UNIV :: 'a option set)"
then obtain c_a
where A: "ID CCOMPARE('a) = Some c_a" "finite (UNIV :: 'a set)"
by(auto simp add: ccompare_option_def ID_def split: option.split_asm)
note [simp] = proper_interval.proper_interval_simps[OF cproper_interval]
ccompare_option_def lt_of_comp_option ID_Some
show "class.proper_interval cless (cproper_interval :: 'a option proper_interval)" using A
proof(unfold_locales)
fix x y :: "'a option"
show "cproper_interval (Some x) None = (∃z. cless x z)" using A
by(cases x)(auto split: option.split intro: exI[where x="Some undefined"])

show "cproper_interval (Some x) (Some y) = (∃z. cless x z ∧ cless z y)" using A
by(cases x y rule: option.exhaust[case_product option.exhaust])(auto cong: option.case_cong split: option.split)
qed(auto split: option.splits)
qed
end

instantiation set :: (cproper_interval) cproper_interval begin
fun cproper_interval_set :: "'a set proper_interval" where
[code]: "cproper_interval_set None None ⟷ True"
| [code]: "cproper_interval_set None (Some B) ⟷ (B ≠ {})"
| [code]: "cproper_interval_set (Some A) None ⟷ (A ≠ UNIV)"
| cproper_interval_set_Some_Some [code del]: ― ‹Refine for concrete implementations›
"cproper_interval_set (Some A) (Some B) ⟷ finite (UNIV :: 'a set) ∧ (∃C. cless A C ∧ cless C B)"
instance
proof
assume "ID CCOMPARE('a set) ≠ None" "finite (UNIV :: 'a set set)"
then obtain c_a
where A: "ID CCOMPARE('a) = Some c_a" "finite (UNIV :: 'a set)"
by(auto simp add: ccompare_set_def ID_def Finite_Set.finite_set)
interpret a: linorder "le_of_comp c_a" "lt_of_comp c_a" by(rule ID_ccompare)(rule A)
note [simp] = proper_interval.proper_interval_simps[OF cproper_interval] ccompare_set_def
ID_Some lt_of_comp_of_ords
show "class.proper_interval cless (cproper_interval :: 'a set proper_interval)" using A
by (unfold_locales, auto)
qed

lemma Complement_cproper_interval_set_Complement:
fixes A B :: "'a set"
assumes corder: "ID CCOMPARE('a) ≠ None"
shows "cproper_interval (Some (- A)) (Some (- B)) = cproper_interval (Some B) (Some A)"
using assms
by(clarsimp simp add: ccompare_set_def ID_Some lt_of_comp_of_ords) (metis double_complement linorder.Compl_set_less_Compl[OF ID_ccompare])

end

instantiation "fun" :: (type, type) cproper_interval begin
text ‹No interval checks on functions needed because we have not defined an order on them.›
definition "cproper_interval = (undefined :: ('a ⇒ 'b) proper_interval)"