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