Theory Predicate_Functions

✐‹creator "Kevin Kappelmann"›
subsection ‹Functions on Predicates›
theory Predicate_Functions
  imports
    Functions_Base
begin

definition "pred_map f (P :: 'a ⇒ bool) x ≡ P (f x)"

lemma pred_map_eq [simp]: "pred_map f P x = P (f x)"
  unfolding pred_map_def by simp

lemma comp_eq_pred_map [simp]: "P ∘ f = pred_map f P"
  by (intro ext) simp

subsubsection ‹Collection›

consts pred_collect :: "'a ⇒ ('b ⇒ 'c) ⇒ 'd"

open_bundle pred_collect_syntax
begin
no_notation disj  (infixr ‹|› 30)
syntax "_pred_collect" :: ‹idt ⇒ idt ⇒ 'a ⇒ 'b ⇒ 'c› ("(⦇_ : _ |/ _⦈)")
syntax_consts "_pred_collect" ⇌ pred_collect
translations
  "⦇x : R | P⦈" ⇌ "CONST pred_collect R (λx. P)"
end

definition "pred_collect_pred :: ('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ 'a ⇒ bool ≡ (⊓)"
adhoc_overloading pred_collect ⇌ pred_collect_pred

lemma pred_collectI [intro]:
  assumes "P x"
  and "P x ⟹ Q x"
  shows "⦇x : P | Q x⦈ x"
  using assms unfolding pred_collect_pred_def by auto

lemma pred_collectE [elim]:
  assumes "⦇x : P | Q x⦈ x"
  obtains "P x" "Q x"
  using assms unfolding pred_collect_pred_def by auto

lemma pred_collect_eq_inf: "pred_collect = (⊓)"
  by (intro ext) auto

subsubsection ‹Conditional Predicate›

consts pred_if :: "bool ⇒ 'a ⇒ 'a"

open_bundle pred_if_syntax
begin
notation pred_if (infixr ‹⟶⇩p› 30)
end

definition "pred_if_rel B P x ≡ B ⟶ P x"
adhoc_overloading pred_if ⇌ pred_if_rel

lemma pred_if_eq_pred_if_pred:
  assumes "B"
  shows "(B ⟶⇩p P) = P"
  unfolding pred_if_rel_def using assms by blast

lemma pred_if_eq_top_if_not_pred:
  assumes "¬B"
  shows "(B ⟶⇩p P) = ⊤"
  unfolding pred_if_rel_def using assms by fastforce

corollary pred_if_True_eq_self [simp]: "(True ⟶⇩p P) = P"
  by (simp add: pred_if_eq_pred_if_pred)
corollary pred_if_False_eq_top [simp]: "(False ⟶⇩p P) = ⊤"
  by (simp add: pred_if_eq_top_if_not_pred)

lemma pred_if_if_impI [intro]:
  assumes "B ⟹ P x"
  shows "(B ⟶⇩p P) x"
   using assms by (cases B) simp_all

lemma pred_if_if_not_pred:
  assumes "¬B"
  shows "(B ⟶⇩p P) x"
  using assms by simp

lemma pred_ifE [elim]:
  assumes "(B ⟶⇩p P) x"
  obtains "¬B" | "B" "P x"
  using assms by (cases B) simp

lemma pred_ifD:
  assumes "(B ⟶⇩p P) x"
  and "B"
  shows "P x"
  using assms by blast

end