Quelle  Overriding.thy

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