(*  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