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