Theory Reverse_Implies

✐‹creator "Kevin Kappelmann"›
theory Reverse_Implies
  imports Binary_Relation_Functions
begin

definition "rev_implies ≡ (⟶)¯"

open_bundle rev_implies_syntax
begin
notation rev_implies (infixr ‹⟵› 25)
end

lemma rev_imp_eq_imp_inv [simp]: "(⟵) = (⟶)¯"
  unfolding rev_implies_def by simp

lemma rev_impI [intro!]:
  assumes "Q ⟹ P"
  shows "P ⟵ Q"
  using assms by auto

lemma rev_impD [dest!]:
  assumes "P ⟵ Q"
  shows "Q ⟹ P"
  using assms by auto

lemma rev_imp_iff_imp: "(P ⟵ Q) ⟷ (Q ⟶ P)" by auto

end