Theory Containers.Collection_Eq

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

section ‹A type class for optional equality testing›

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

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)"


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

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')]

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.

\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}

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
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)

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)


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)