Theory Collection_Order
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"
by(clarsimp simp add: ID_ccompare)
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)"
by(simp add: is_ccompare_def ccompare_fun_def ID_None)
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)"
by(simp add: is_ccompare_def ccompare_set_def ID_def)
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
by(simp add: ID_ccompare class.linorder_proper_interval_def)
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"
instance by(intro_classes)(simp add: infinite_UNIV_listI)
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"
instance by(intro_classes)(simp add: infinite_UNIV_literal)
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]:
"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)"
instance by(intro_classes)(simp add: ccompare_fun_def ID_None)
end
end