1(*  Title:      HOL/HOLCF/IOA/NTP/Lemmas.thy
2    Author:     Tobias Nipkow & Konrad Slind
3*)
4
5theory Lemmas
6imports Main
7begin
8
9subsubsection \<open>Logic\<close>
10
11lemma neg_flip: "(X = (\<not> Y)) = ((\<not>X) = Y)"
12  by blast
13
14
15subsection \<open>Sets\<close>
16
17lemma set_lemmas:
18  "f(x) \<in> (\<Union>x. {f(x)})"
19  "f x y \<in> (\<Union>x y. {f x y})"
20  "\<And>a. (\<forall>x. a \<noteq> f(x)) \<Longrightarrow> a \<notin> (\<Union>x. {f(x)})"
21  "\<And>a. (\<forall>x y. a \<noteq> f x y) \<Longrightarrow> a \<notin> (\<Union>x y. {f x y})"
22  by auto
23
24
25subsection \<open>Arithmetic\<close>
26
27lemma pred_suc: "0<x ==> (x - 1 = y) = (x = Suc(y))"
28  by (simp add: diff_Suc split: nat.split)
29
30lemmas [simp] = hd_append set_lemmas
31
32end
33