Theory Deriving.Equality_Generator

(*  Title:       Deriving class instances for datatypes
    Author:      Christian Sternagel and René Thiemann  <christian.sternagel|>
    Maintainer:  Christian Sternagel and René Thiemann 
    License:     LGPL
section ‹Checking Equality Without "="›

theory Equality_Generator

typedecl ('a,'b,'c,'z)type

text ‹In the following, we define a generator which for a given datatype @{typ "('a,'b,'c,'z)type"}
  constructs an equality-test function of type 
  @{typ "('a  'a  bool)  ('b  'b  bool)  ('c  'c  bool)  ('z  'z  bool)  
    (('a,'b,'c,'z)type  ('a,'b,'c,'z)type  bool)"}.
  These functions are essential to synthesize conditional equality functions in the container framework,
  where a strict membership in the @{class equal}-class must not be enforced.

hide_type "type"

text ‹Just a constant to define conjunction on lists of booleans, which will
  be used to merge the results when having compared the arguments of identical

definition list_all_eq :: "bool list  bool" where
  "list_all_eq = list_all id "

subsection ‹Improved Code for Non-Lazy Languages›

text ‹The following equations will eliminate all occurrences of @{term list_all_eq}
  in the generated code of the equality functions.›

lemma list_all_eq_unfold: 
  "list_all_eq [] = True"
  "list_all_eq [b] = b"
  "list_all_eq (b1 # b2 # bs) = (b1  list_all_eq (b2 # bs))"
  unfolding list_all_eq_def
  by auto

lemma list_all_eq: "list_all_eq bs  ( b  set bs. b)" 
  unfolding list_all_eq_def list_all_iff by auto  

subsection ‹Partial Equality Property›

text ‹We require a partial property which can be used in inductive proofs.›

type_synonym 'a equality = "'a  'a  bool"

definition pequality :: "'a equality  'a  bool"
  "pequality aeq x  ( y. aeq x y  x = y)"

lemma pequalityD: "pequality aeq x  aeq x y  x = y"
  unfolding pequality_def by auto

lemma pequalityI: "( y. aeq x y  x = y)  pequality aeq x"
  unfolding pequality_def by auto

subsection ‹Global equality property›

definition equality :: "'a equality  bool" where
  "equality aeq  ( x. pequality aeq x)"

lemma equalityD2: "equality aeq  pequality aeq x"
  unfolding equality_def by blast

lemma equalityI2: "( x. pequality aeq x)  equality aeq" 
  unfolding equality_def by blast
lemma equalityD: "equality aeq  aeq x y  x = y"
  by (rule pequalityD[OF equalityD2])

lemma equalityI: "( x y. aeq x y  x = y)  equality aeq"
  by (intro equalityI2 pequalityI)

lemma equality_imp_eq:
  "equality aeq  aeq = (=)" 
  by (intro ext, auto dest: equalityD)

lemma eq_equality: "equality (=)"
  by (rule equalityI, simp)

lemma equality_def': "equality f = (f = (=))" 
  using equality_imp_eq eq_equality by blast

subsection ‹The Generator›

ML_file ‹equality_generator.ML›

hide_fact (open) equalityI