Theory Predicates_Lattice

✐‹creator "Kevin Kappelmann"›
subsection ‹Lattice›
theory Predicates_Lattice
  imports
    HOL_Syntax_Bundles_Lattices
    HOL.Boolean_Algebras
begin

lemma inf_predI [intro]:
  assumes "P x"
  and "Q x"
  shows "(P ⊓ Q) x"
  using assms by (intro inf1I)

lemma inf_predE [elim]:
  assumes "(P ⊓ Q) x"
  obtains "P x" "Q x"
  using assms by (rule inf1E)

lemma inf_predD:
  assumes "(P ⊓ Q) x"
  shows "P x" and "Q x"
  using assms by auto


end