1(*  Title:      HOL/HOLCF/IOA/ABP/Lemmas.thy
2    Author:     Olaf M��ller
3*)
4
5theory Lemmas
6imports Main
7begin
8
9subsection \<open>Logic\<close>
10
11lemma and_de_morgan_and_absorbe: "(\<not>(A\<and>B)) = ((\<not>A)\<and>B\<or> \<not>B)"
12  by blast
13
14lemma bool_if_impl_or: "(if C then A else B) \<longrightarrow> (A\<or>B)"
15  by auto
16
17lemma exis_elim: "(\<exists>x. x=P \<and> Q(x)) = Q(P)"
18  by blast
19
20
21subsection \<open>Sets\<close>
22
23lemma set_lemmas:
24    "f(x) \<in> (\<Union>x. {f(x)})"
25    "f x y \<in> (\<Union>x y. {f x y})"
26    "\<And>a. (\<forall>x. a \<noteq> f(x)) \<Longrightarrow> a \<notin> (\<Union>x. {f(x)})"
27    "\<And>a. (\<forall>x y. a \<noteq> f x y) ==> a \<notin> (\<Union>x y. {f x y})"
28  by auto
29
30text \<open>2 Lemmas to add to \<open>set_lemmas\<close>, used also for action handling, 
31   namely for Intersections and the empty list (compatibility of IOA!).\<close>
32lemma singleton_set: "(\<Union>b.{x. x=f(b)}) = (\<Union>b.{f(b)})"
33  by blast
34
35lemma de_morgan: "((A\<or>B)=False) = ((\<not>A)\<and>(\<not>B))"
36  by blast
37
38
39subsection \<open>Lists\<close>
40
41lemma cons_not_nil: "l \<noteq> [] \<longrightarrow> (\<exists>x xs. l = (x#xs))"
42  by (induct l) simp_all
43
44end
45