Theory Lifted_Predicates

(*<*)
theory Lifted_Predicates
imports
  HOL_Basis
begin

(*>*)
section‹ Point-free notation \label{sec:lifted_predicates} ›

text‹

Typically we define predicates as functions of a state. The following
provide a somewhat comfortable point-free imitation of Isabelle/HOL's
operators.

›

type_synonym 's pred = "'s ⇒ bool"

abbreviation (input)
  pred_K :: "'b ⇒ 'a ⇒ 'b" ("⟨_⟩") where
  "⟨f⟩ ≡ λs. f"

abbreviation (input)
  pred_not :: "'a pred ⇒ 'a pred" ("❙¬ _" [40] 40) where
  "❙¬a ≡ λs. ¬a s"

abbreviation (input)
  pred_conj :: "'a pred ⇒ 'a pred ⇒ 'a pred" (infixr "❙∧" 35) where
  "a ❙∧ b ≡ λs. a s ∧ b s"

abbreviation (input)
  pred_disj :: "'a pred ⇒ 'a pred ⇒ 'a pred" (infixr "❙∨" 30) where
  "a ❙∨ b ≡ λs. a s ∨ b s"

abbreviation (input)
  pred_implies :: "'a pred ⇒ 'a pred ⇒ 'a pred" (infixr "❙⟶" 25) where
  "a ❙⟶ b ≡ λs. a s ⟶ b s"

abbreviation (input)
  pred_iff :: "'a pred ⇒ 'a pred ⇒ 'a pred" (infixr "❙⟷" 25) where
  "a ❙⟷ b ≡ λs. a s ⟷ b s"

abbreviation (input)
  pred_eq :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ 'a pred" (infix "❙=" 40) where
  "a ❙= b ≡ λs. a s = b s"

abbreviation (input)
  pred_neq :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ 'a pred" (infix "❙≠" 40) where
  "a ❙≠ b ≡ λs. a s ≠ b s"

abbreviation (input)
  pred_If :: "'a pred ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" ("(If (_)/ Then (_)/ Else (_))" [0, 0, 10] 10)
  where "If P Then x Else y ≡ λs. if P s then x s else y s"

abbreviation (input)
  pred_less :: "('a ⇒ 'b::ord) ⇒ ('a ⇒ 'b) ⇒ 'a pred" (infix "❙<" 40) where
  "a ❙< b ≡ λs. a s < b s"

abbreviation (input)
  pred_less_eq :: "('a ⇒ 'b::ord) ⇒ ('a ⇒ 'b) ⇒ 'a pred" (infix "❙≤" 40) where
  "a ❙≤ b ≡ λs. a s ≤ b s"

abbreviation (input)
  pred_greater :: "('a ⇒ 'b::ord) ⇒ ('a ⇒ 'b) ⇒ 'a pred" (infix "❙>" 40) where
  "a ❙> b ≡ λs. a s > b s"

abbreviation (input)
  pred_greater_eq :: "('a ⇒ 'b::ord) ⇒ ('a ⇒ 'b) ⇒ 'a pred" (infix "❙≥" 40) where
  "a ❙≥ b ≡ λs. a s ≥ b s"

abbreviation (input)
  pred_plus :: "('a ⇒ 'b::plus) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" (infixl "❙+" 65) where
  "a ❙+ b ≡ λs. a s + b s"

abbreviation (input)
  pred_minus :: "('a ⇒ 'b::minus) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" (infixl "❙-" 65) where
  "a ❙- b ≡ λs. a s - b s"

abbreviation (input)
  pred_times :: "('a ⇒ 'b::times) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" (infixl "❙*" 65) where
  "a ❙* b ≡ λs. a s * b s"

abbreviation (input)
  pred_all :: "('b ⇒ 'a pred) ⇒ 'a pred" (binder "❙∀" 10) where
  "❙∀x. P x ≡ λs. ∀x. P x s"

abbreviation (input)
  pred_ex :: "('b ⇒ 'a pred) ⇒ 'a pred" (binder "❙∃" 10) where
  "❙∃x. P x ≡ λs. ∃x. P x s"

(* this one is applicative-functor ish *)
abbreviation (input)
  pred_app :: "('a ⇒ 'b ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'c" (infixl "❙$" 100) where
  "f ❙$ g ≡ λs. f s (g s)"

(* this one is monadic postcondition ish *)
abbreviation (input)
  pred_app' :: "('b ⇒ 'a ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'c" (infixl "❙$❙$" 100) where
  "f ❙$❙$ g ≡ λs. f (g s) s"

abbreviation (input)
  pred_member :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b set) ⇒ 'a pred" (infix "❙∈" 40) where
  "a ❙∈ b ≡ λs. a s ∈ b s"

abbreviation (input)
  pred_subseteq :: "('a ⇒ 'b set) ⇒ ('a ⇒ 'b set) ⇒ 'a pred" (infix "❙⊆" 50) where
  "A ❙⊆ B ≡ λs. A s ⊆ B s"

abbreviation (input)
  pred_union :: "('a ⇒ 'b set) ⇒ ('a ⇒ 'b set) ⇒ 'a ⇒ 'b set" (infixl "❙∪" 65) where
  "a ❙∪ b ≡ λs. a s ∪ b s"

abbreviation (input)
  pred_inter :: "('a ⇒ 'b set) ⇒ ('a ⇒ 'b set) ⇒ 'a ⇒ 'b set" (infixl "❙∩" 65) where
  "a ❙∩ b ≡ λs. a s ∩ b s"

abbreviation (input)
  pred_conjoin :: "'a pred list ⇒ 'a pred" where
  "pred_conjoin xs ≡ foldr (❙∧) xs ⟨True⟩"

abbreviation (input)
  pred_disjoin :: "'a pred list ⇒ 'a pred" where
  "pred_disjoin xs ≡ foldr (❙∨) xs ⟨False⟩"

abbreviation (input)
  pred_min :: "('a ⇒ 'b::ord) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" where
  "pred_min x y ≡ λs. min (x s) (y s)"

abbreviation (input)
  pred_max :: "('a ⇒ 'b::ord) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" where
  "pred_max x y ≡ λs. max (x s) (y s)"

abbreviation (input)
  NULL :: "('a ⇒ 'b option) ⇒ 'a pred" where
  "NULL a ≡ λs. a s = None"

abbreviation (input)
  EMPTY :: "('a ⇒ 'b set) ⇒ 'a pred" where
  "EMPTY a ≡ λs. a s = {}"

abbreviation (input)
  LIST_NULL :: "('a ⇒ 'b list) ⇒ 'a pred" where
  "LIST_NULL a ≡ λs. a s = []"

abbreviation (input)
  SIZE :: "('a ⇒ 'b::size) ⇒ 'a ⇒ nat" where
  "SIZE a ≡ λs. size (a s)"

abbreviation (input)
  SET :: "('a ⇒ 'b list) ⇒ 'a ⇒ 'b set" where
  "SET a ≡ λs. set (a s)"

abbreviation (input)
  pred_singleton :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b set" where
  "pred_singleton x ≡ λs. {x s}"

abbreviation (input)
  pred_list_nth :: "('a ⇒ 'b list) ⇒ ('a ⇒ nat) ⇒ 'a ⇒ 'b" (infixl "❙!" 150) where
  "xs ❙! i ≡ λs. xs s ! i s"

abbreviation (input)
  pred_list_append :: "('a ⇒ 'b list) ⇒ ('a ⇒ 'b list) ⇒ 'a ⇒ 'b list" (infixr "❙@" 65) where
  "xs ❙@ ys ≡ λs. xs s @ ys s"

abbreviation (input)
  FST :: "'a pred ⇒ ('a × 'b) pred" where
  "FST P ≡ λs. P (fst s)"

abbreviation (input)
  SND :: "'b pred ⇒ ('a × 'b) pred" where
  "SND P ≡ λs. P (snd s)"

abbreviation (input)
  pred_pair :: "('a ⇒ 'b) ⇒ ('a ⇒ 'c) ⇒ 'a ⇒ 'b × 'c" (infixr "❙⊗" 60) where
  "a ❙⊗ b ≡ λs. (a s, b s)"
(*<*)

end
(*>*)