Up to index of Isabelle/HOLCF/IOA/ABP
theory Lemmas(* Title: HOLCF/IOA/ABP/Lemmas.thy ID: $Id: Lemmas.thy,v 1.7 2005/09/03 14:50:23 wenzelm Exp $ Author: Olaf Müller *) theory Lemmas imports Main begin end
theorem and_de_morgan_and_absorbe:
(¬ (A ∧ B)) = (¬ A ∧ B ∨ ¬ B)
theorem bool_if_impl_or:
(if C then A else B) --> A ∨ B
theorem exis_elim:
(∃x. x = P ∧ Q x) = Q P
theorem singleton_set:
(UN b. {x. x = f b}) = (UN b. {f b})
theorem de_morgan:
((A ∨ B) = False) = (¬ A ∧ ¬ B)
theorem hd_append:
hd (l @ m) = (if l ≠ [] then hd l else hd m)
theorem cons_not_nil:
l ≠ [] --> (∃x xs. l = x # xs)