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