Theory Containers.Collection_Eq

(*  Title:      Containers/Collection_Eq.thy
    Author:     Andreas Lochbihler, KIT
                René Thiemann, UIBK *)
theory Collection_Eq imports
  Containers_Auxiliary
  Containers_Generator
  Deriving.Equality_Instances
begin

section ‹A type class for optional equality testing›

class ceq =
  fixes ceq :: "('a ⇒ 'a ⇒ bool) option"
  assumes ceq: "ceq = Some eq ⟹ eq = (=)"
begin

lemma ceq_equality: "ceq = Some eq ⟹ equality eq"
  by (drule ceq, rule Equality_Generator.equalityI, simp)

lemma ID_ceq: "ID ceq = Some eq ⟹ eq = (=)"
unfolding ID_def id_apply by(rule ceq)

abbreviation ceq' :: "'a ⇒ 'a ⇒ bool" where "ceq' ≡ the (ID ceq)"

end

syntax "_CEQ" :: "type => logic"  (‹(1CEQ/(1'(_')))›)

syntax_consts "_CEQ" == ceq

parse_translation ‹
let
  fun ceq_tr [ty] =
     (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "ceq"} $
       (Syntax.const @{type_syntax option} $ 
         (Syntax.const @{type_syntax fun} $ ty $ 
           (Syntax.const @{type_syntax fun} $ ty $ Syntax.const @{type_syntax bool}))))
    | ceq_tr ts = raise TERM ("ceq_tr", ts);
in [(@{syntax_const "_CEQ"}, K ceq_tr)] end
›

typed_print_translation ‹
let
  fun ceq_tr' ctxt
    (Type (@{type_name option}, [Type (@{type_name fun}, [T, _])])) ts =
    Term.list_comb (Syntax.const @{syntax_const "_CEQ"} $ Syntax_Phases.term_of_typ ctxt T, ts)
  | ceq_tr' _ _ _ = raise Match;
in [(@{const_syntax ceq}, ceq_tr')]
end
›

definition is_ceq :: "'a :: ceq itself ⇒ bool"
where "is_ceq _ ⟷ ID CEQ('a) ≠ None"

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

text ‹
This generator registers itself at the derive-manager for the class @{class ceq}.
To be more precise, one can choose whether one wants to take @{term "(=)"} as function
for @{term ceq} by passing "eq" as parameter, 
whether equality should not be supported by passing "no" as parameter,
or whether an own definition for equality should be derived by not passing
any parameters. The last possibility only works for datatypes.

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

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


text ‹
This generator can be used for arbitrary types, not just datatypes. 
›

lemma equality_subst: "c1 = c2 ⟹ equality c1 ⟹ equality c2" by blast

ML_file ‹ceq_generator.ML›

subsection ‹Type class instances for HOL types›

derive (eq) ceq unit
lemma [code]: "CEQ(unit) = Some (λ_ _. True)"
  unfolding ceq_unit_def by (simp, intro ext, auto)
derive (eq) ceq
  bool
  nat
  int
  Enum.finite_1
  Enum.finite_2
  Enum.finite_3
  Enum.finite_4
  Enum.finite_5
  integer
  natural
  char
  String.literal
derive ceq sum prod list option
derive (no) ceq "fun"

lemma is_ceq_fun [simp]: "¬ is_ceq TYPE('a ⇒ 'b)"
  by(simp add: is_ceq_def ceq_fun_def ID_None) 

definition set_eq :: "'a set ⇒ 'a set ⇒ bool" 
where [code del]: "set_eq = (=)"

lemma set_eq_code:
  shows [code]: "set_eq A B ⟷ A ⊆ B ∧ B ⊆ A"
  and [code_unfold]: "(=) = set_eq"
unfolding set_eq_def by blast+

instantiation set :: (ceq) ceq begin
definition "CEQ('a set) = (case ID CEQ('a) of None ⇒ None | Some _ ⇒ Some set_eq)"
instance by(intro_classes)(simp add: ceq_set_def set_eq_def split: option.splits)
end

lemma is_ceq_set [simp, code_post]: "is_ceq TYPE('a set) ⟷ is_ceq TYPE('a :: ceq)"
by(simp add: is_ceq_def ceq_set_def ID_None ID_Some split: option.split)

lemma ID_ceq_set_not_None_iff [simp]: "ID CEQ('a set) ≠ None ⟷ ID CEQ('a :: ceq) ≠ None"
by(simp add: ceq_set_def ID_def split: option.splits)

text ‹Instantiation for @{typ "'a Predicate.pred"}›

context fixes eq :: "'a ⇒ 'a ⇒ bool" begin

definition member_pred :: "'a Predicate.pred ⇒ 'a ⇒ bool"
where "member_pred P x ⟷ (∃y. eq x y ∧ Predicate.eval P y)"

definition member_seq :: "'a Predicate.seq ⇒ 'a ⇒ bool"
where "member_seq xp = member_pred (Predicate.pred_of_seq xp)"

lemma member_seq_code [code]: 
  "member_seq seq.Empty x ⟷ False"
  "member_seq (seq.Insert y P) x ⟷ eq x y ∨ member_pred P x"
  "member_seq (seq.Join Q xq) x ⟷ member_pred Q x ∨ member_seq xq x"
by(auto simp add: member_seq_def member_pred_def)

lemma member_pred_code [code]:
  "member_pred (Predicate.Seq f) = member_seq (f ())"
by(simp add: member_seq_def Seq_def)

definition leq_pred :: "'a Predicate.pred ⇒ 'a Predicate.pred ⇒ bool"
where "leq_pred P Q ⟷ (∀x. Predicate.eval P x ⟶ (∃y. eq x y ∧ Predicate.eval Q y))"

definition leq_seq :: "'a Predicate.seq ⇒ 'a Predicate.pred ⇒ bool"
where "leq_seq xp Q ⟷ leq_pred (Predicate.pred_of_seq xp) Q"

lemma leq_seq_code [code]:
  "leq_seq seq.Empty Q ⟷ True"
  "leq_seq (seq.Insert x P) Q ⟷ member_pred Q x ∧ leq_pred P Q"
  "leq_seq (seq.Join P xp) Q ⟷ leq_pred P Q ∧ leq_seq xp Q"
by(auto simp add: leq_seq_def leq_pred_def member_pred_def)

lemma leq_pred_code [code]:
  "leq_pred (Predicate.Seq f) Q ⟷ leq_seq (f ()) Q"
by(simp add: leq_seq_def Seq_def)

definition predicate_eq :: "'a Predicate.pred ⇒ 'a Predicate.pred ⇒ bool"
where "predicate_eq P Q ⟷ leq_pred P Q ∧ leq_pred Q P"

context assumes eq: "eq = (=)" begin

lemma member_pred_eq: "member_pred = Predicate.eval"
unfolding fun_eq_iff member_pred_def by(simp add: eq)

lemma member_seq_eq: "member_seq = Predicate.member"
by(simp add: member_seq_def fun_eq_iff eval_member member_pred_eq)

lemma leq_pred_eq: "leq_pred = (≤)"
unfolding fun_eq_iff leq_pred_def by(auto simp add: eq less_eq_pred_def)

lemma predicate_eq_eq: "predicate_eq = (=)"
unfolding predicate_eq_def fun_eq_iff by(auto simp add: leq_pred_eq)

end
end

instantiation Predicate.pred :: (ceq) ceq begin
definition "CEQ('a Predicate.pred) = map_option predicate_eq (ID CEQ('a))"
instance by(intro_classes)(auto simp add: ceq_pred_def predicate_eq_eq dest: ID_ceq)
end

end