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