Theory Predicates_Order

✐‹creator "Kevin Kappelmann"›
subsection ‹Orders›
theory Predicates_Order
  imports
    HOL.Orderings
begin

lemma le_predI [intro]:
  assumes "⋀x. P x ⟹ Q x"
  shows "P ≤ Q"
  using assms by (rule predicate1I)

lemma le_predD [dest]:
  assumes "P ≤ Q"
  and "P x"
  shows "Q x"
  using assms by (rule predicate1D)

lemma le_predE:
  assumes "P ≤ Q"
  and "P x"
  obtains "Q x"
  using assms by blast

declare le_boolD[dest] and le_boolI[intro]

end