Theory Lemmas

(*  Title:      HOL/HOLCF/IOA/NTP/Lemmas.thy
    Author:     Tobias Nipkow & Konrad Slind
*)

theory Lemmas
imports Main
begin

subsubsection ‹Logic›

lemma neg_flip: "(X = (¬ Y)) = ((¬X) = Y)"
  by blast


subsection ‹Sets›

lemma set_lemmas:
  "f(x) ∈ (⋃x. {f(x)})"
  "f x y ∈ (⋃x y. {f x y})"
  "⋀a. (∀x. a ≠ f(x)) ⟹ a ∉ (⋃x. {f(x)})"
  "⋀a. (∀x y. a ≠ f x y) ⟹ a ∉ (⋃x y. {f x y})"
  by auto


subsection ‹Arithmetic›

lemma pred_suc: "0<x ==> (x - 1 = y) = (x = Suc(y))"
  by (simp add: diff_Suc split: nat.split)

lemmas [simp] = hd_append set_lemmas

end