Theory CIMP_pred

(*<*)
(*
 * Copyright 2015, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

theory CIMP_pred
imports
  Main
begin

(* Extra HOL *)

lemma triv: "P ⟹ P"
by simp

lemma always_eventually_pigeonhole:
  "(∀i. ∃n≥i. ∃m≤k. P m n) ⟷ (∃m≤k::nat. ∀i::nat. ∃n≥i. P m n)"
proof(induct k)
  case (Suc k) then show ?case
    apply (auto 8 0)
    using le_SucI apply blast
    apply (metis (full_types) le_Suc_eq nat_le_linear order_trans)
    done
qed simp

(*>*)
section‹ Point-free notation ›

text‹

\label{sec:cimp-lifted-predicates}

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

›

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

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

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

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

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

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

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

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

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

abbreviation (input)
  pred_If :: "('a ⇒ bool) ⇒ ('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 ⇒ bool" (infix ‹❙<› 40) where
  "a ❙< b ≡ λs. a s < b s"

abbreviation (input)
  pred_le :: "('a ⇒ 'b::ord) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ bool" (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)
  fun_fanout :: "('a ⇒ 'b) ⇒ ('a ⇒ 'c) ⇒ 'a ⇒ 'b × 'c" (infix ‹❙⨝› 35) where
  "f ❙⨝ g ≡ λx. (f x, g x)"

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

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

abbreviation (input)
  pred_app :: "('b ⇒ 'a ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'c" (infixl ‹❙$› 100) where
  "f ❙$ g ≡ λs. f (g s) s"

abbreviation (input)
  pred_subseteq :: "('a ⇒ 'b set) ⇒ ('a ⇒ 'b set) ⇒ 'a ⇒ bool" (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"

text‹

More application specific.

›

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

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

abbreviation (input)
  pred_is_none :: "('a ⇒ 'b option) ⇒ 'a ⇒ bool" (‹NULL _› [40] 40) where
  "NULL a ≡ λs. a s = None"

abbreviation (input)
  pred_empty :: "('a ⇒ 'b set) ⇒ 'a ⇒ bool" (‹EMPTY _› [40] 40) where
  "EMPTY a ≡ λs. a s = {}"

abbreviation (input)
  pred_list_null :: "('a ⇒ 'b list) ⇒ 'a ⇒ bool" (‹LIST'_NULL _› [40] 40) where
  "LIST_NULL a ≡ λs. a 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)
  pred_pair :: "('a ⇒ 'b) ⇒ ('a ⇒ 'c) ⇒ 'a ⇒ 'b × 'c" (infixr ‹❙⊗› 60) where
  "a ❙⊗ b ≡ λs. (a s, b s)"

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

end
(*>*)