Theory Lib

(*  Title:       Lib.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke
*)

section "Generic functions and lemmas"

theory Lib
imports Main
begin

definition
  TT :: "'a ⇒ bool"
where
  "TT = (λ_. True)"

lemma TT_True [intro, simp]: "TT a"
  unfolding TT_def by simp

lemma in_set_tl: "x ∈ set (tl xs) ⟹ x ∈ set xs"
  by (metis Nil_tl insert_iff list.collapse set_simps(2))

lemma nat_le_eq_or_lt [elim]:
    fixes x :: nat
  assumes "x ≤ y"
      and eq: "x = y ⟹ P x y"
      and lt: "x < y ⟹ P x y"
    shows "P x y"
  using assms unfolding nat_less_le by auto

lemma disjoint_commute:
  "(A ∩ B = {}) ⟹ (B ∩ A = {})"
  by auto

definition
  default :: "('i ⇒ 's) ⇒ ('i ⇒ 's option) ⇒ ('i ⇒ 's)"
where
  "default df f = (λi. case f i of None ⇒ df i | Some s ⇒ s)"

end