# Theory Lemmas

Up to index of Isabelle/HOLCF/IOA/ABP

theory Lemmas
imports Main
uses [Lemmas.ML]
begin

    (*  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)