(* Title: HOL/HOLCF/IOA/ABP/Lemmas.thy
Author: Olaf Müller
*)
theory Lemmas
imports Main
begin
subsection \<open>Logic\<close>
lemma and_de_morgan_and_absorbe: "(\<not>(A\<and>B)) = ((\<not>A)\<and>B\<or> \<not>B)"
by blast
lemma bool_if_impl_or: "(if C then A else B) \<longrightarrow> (A\<or>B)"
by auto
lemma exis_elim: "(\<exists>x. x=P \<and> Q(x)) = Q(P)"
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) ==> a \<notin> (\<Union>x y. {f x y})"
by auto
text \<open>2 Lemmas to add to \<open>set_lemmas\<close>, used also for action handling,
namely for Intersections and the empty list (compatibility of IOA!).\<close>
lemma singleton_set: "(\<Union>b.{x. x=f(b)}) = (\<Union>b.{f(b)})"
by blast
lemma de_morgan: "((A\<or>B)=False) = ((\<not>A)\<and>(\<not>B))"
by blast
subsection \<open>Lists\<close>
lemma cons_not_nil: "l \<noteq> [] \<longrightarrow> (\<exists>x xs. l = (x#xs))"
by (induct l) simp_all
end