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"
    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]: ― ‹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)"
instance by(intro_classes)(simp add: ccompare_fun_def ID_None)
end

end