Theory Overriding

section ‹ Polymorphic Overriding Operator ›

theory Overriding
  imports Main
begin

text ‹ We here use type classes to create the overriding operator and instantiate it for relations,
  partial function, and finite functions. ›

class oplus = 
  fixes oplus :: "'a ⇒ 'a ⇒ 'a" (infixl "⊕" 65)

class compatible = 
  fixes compatible :: "'a ⇒ 'a ⇒ bool" (infix "##" 60)
  assumes compatible_sym: "x ## y ⟹ y ## x"

unbundle lattice_syntax

class override = oplus + bot + compatible +
  assumes compatible_zero [simp]: "x ## ⊥"
  and override_idem [simp]: "P ⊕ P = P"
  and override_assoc: "P ⊕ (Q ⊕ R) = (P ⊕ Q) ⊕ R"
  and override_lzero [simp]: "⊥ ⊕ P = P"
  and override_comm: "P ## Q ⟹ P ⊕ Q = Q ⊕ P" 
  and override_compat: "⟦ P ## Q; (P ⊕ Q) ## R ⟧ ⟹ P ## R"
  and override_compatI: "⟦ P ## Q; P ## R; Q ## R ⟧ ⟹ (P ⊕ Q) ## R"
begin

lemma override_rzero [simp]: "P ⊕ ⊥ = P"
  by (metis compatible_zero override_comm override_lzero)

lemma override_compat': "⟦ P ## Q; (P ⊕ Q) ## R ⟧ ⟹ Q ## R"
  by (metis compatible_sym override_comm override_compat)

lemma override_compat_iff: "P ## Q ⟹ (P ⊕ Q) ## R ⟷ (P ## R) ∧ (Q ## R)"
  by (meson override_compat override_compatI override_compat')

end

end