Theory Deriving.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 
    License:     LGPL
*)
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