# Theory Equality_Generator

```(*  Title:       Deriving class instances for datatypes
Author:      Christian Sternagel and René Thiemann  <christian.sternagel|rene.thiemann@uibk.ac.at>
Maintainer:  Christian Sternagel and René Thiemann
*)
section ‹Checking Equality Without "="›

theory Equality_Generator
imports
"../Generator_Aux"
"../Derive_Manager"
begin

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
constructors.›

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

end
```