Theory Reverse_Implies

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

definition "rev_implies ≡ (⟶)¯"

bundle rev_implies_syntax begin notation rev_implies (infixr "⟵" 25) end
bundle no_rev_implies_syntax begin no_notation rev_implies (infixr "⟵" 25) end
unbundle rev_implies_syntax

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