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