src/HOL/HOLCF/IOA/NTP/Lemmas.thy

tuned;

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

theory Lemmas
imports Main
begin

subsubsection \<open>Logic\<close>

lemma neg_flip: "(X = (\<not> Y)) = ((\<not>X) = Y)"
  by blast


subsection \<open>Sets\<close>

lemma set_lemmas:
  "f(x) \<in> (\<Union>x. {f(x)})"
  "f x y \<in> (\<Union>x y. {f x y})"
  "\<And>a. (\<forall>x. a \<noteq> f(x)) \<Longrightarrow> a \<notin> (\<Union>x. {f(x)})"
  "\<And>a. (\<forall>x y. a \<noteq> f x y) \<Longrightarrow> a \<notin> (\<Union>x y. {f x y})"
  by auto


subsection \<open>Arithmetic\<close>

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