Theory Restricted_Equality

✐‹creator "Kevin Kappelmann"›
subsection ‹Restricted Equality›
theory Restricted_Equality
  imports
    Binary_Relations_Order_Base
    Binary_Relation_Functions
    Equivalence_Relations
    Partial_Orders
begin

paragraph ‹Summary›
text ‹Introduces notations and theorems for restricted equalities.
An equality @{term "(=)"} can be restricted to only apply to a subset of its
elements. The restriction can be formulated, for example, by a predicate or a set.›

bundle eq_rel_restrict_syntax
begin
syntax
  "_eq_restrict_infix" :: "'a ⇒ 'b ⇒ 'a ⇒ bool" ("(_) =(⇘_⇙) (_)" [51,51,51] 50)
  "_eq_restrict" :: "'b ⇒ 'a ⇒ bool" ("'(=(⇘_⇙)')")
end
bundle no_eq_rel_restrict_syntax
begin
no_syntax
  "_eq_restrict_infix" :: "'a ⇒ 'b ⇒ 'a ⇒ bool" ("(_) =(⇘_⇙) (_)" [51,51,51] 50)
  "_eq_restrict" :: "'b ⇒ 'a ⇒ bool" ("'(=(⇘_⇙)')")
end
unbundle eq_rel_restrict_syntax

translations
  "(=⇘P⇙)" ⇌ "CONST rel_restrict_left (=) P"
  "x =⇘P⇙ y" ⇌ "CONST rel_restrict_left (=) P x y"

lemma in_dom_eq_restrict_eq [simp]: "in_dom (=⇘P⇙) = P" by auto
lemma in_codom_eq_restrict_eq [simp]: "in_codom (=⇘P⇙) = P" by auto
lemma in_field_eq_restrict_eq [simp]: "in_field (=⇘P⇙) = P" by auto


paragraph ‹Order Properties›

context
  fixes P :: "'a ⇒ bool"
begin

context
begin
lemma reflexive_on_eq_restrict: "reflexive_on P ((=⇘P⇙) :: 'a ⇒ _)" by auto
lemma transitive_eq_restrict: "transitive ((=⇘P⇙) :: 'a ⇒ _)" by auto
lemma symmetric_eq_restrict: "symmetric ((=⇘P⇙) :: 'a ⇒ _)" by auto
lemma antisymmetric_eq_restrict: "antisymmetric ((=⇘P⇙) :: 'a ⇒ _)" by auto
end

context
begin
lemma preorder_on_eq_restrict: "preorder_on P ((=⇘P⇙) :: 'a ⇒ _)"
  using reflexive_on_eq_restrict transitive_eq_restrict by auto
lemma partial_equivalence_rel_eq_restrict: "partial_equivalence_rel ((=⇘P⇙) :: 'a ⇒ _)"
  using symmetric_eq_restrict transitive_eq_restrict by auto
end

lemma partial_order_on_eq_restrict: "partial_order_on P ((=⇘P⇙) :: 'a ⇒ _)"
  using preorder_on_eq_restrict antisymmetric_eq_restrict by auto
lemma equivalence_rel_on_eq_restrict: "equivalence_rel_on P ((=⇘P⇙) :: 'a ⇒ _)"
  using partial_equivalence_rel_eq_restrict reflexive_on_eq_restrict by blast
end


end