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

consts pred_if :: "bool  'a  'a"

bundle pred_if_syntax begin notation (output) pred_if (infixl "" 50) end
bundle no_pred_if_syntax begin no_notation (output) pred_if (infixl "" 50) end
unbundle pred_if_syntax

definition "pred_if_pred B P x  B  P x"
adhoc_overloading pred_if pred_if_pred

lemma pred_if_eq_pred_if_pred [simp]:
  assumes "B"
  shows "(pred_if B P) = P"
  unfolding pred_if_pred_def using assms by blast

lemma pred_if_eq_top_if_not_pred [simp]:
  assumes "¬B"
  shows "(pred_if B P) = (λ_. True)"
  unfolding pred_if_pred_def using assms by blast

lemma pred_if_if_impI [intro]:
  assumes "B  P x"
  shows "(pred_if B P) x"
  unfolding pred_if_pred_def using assms by blast

lemma pred_ifE [elim]:
  assumes "(pred_if B P) x"
  obtains "¬B" | "B" "P x"
  using assms unfolding pred_if_pred_def by blast

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


end