src/HOL/HOLCF/IOA/ABP/Lemmas.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 35174 src/HOLCF/IOA/ABP/Lemmas.thy@e15040ae75d7
child 40945 b8703f63bfb2
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
mueller@3072
     1
(*  Title:      HOLCF/IOA/ABP/Lemmas.thy
wenzelm@12218
     2
    Author:     Olaf Müller
mueller@3072
     3
*)
mueller@3072
     4
wenzelm@17244
     5
theory Lemmas
wenzelm@17244
     6
imports Main
wenzelm@17244
     7
begin
wenzelm@17244
     8
wenzelm@19738
     9
subsection {* Logic *}
wenzelm@19738
    10
wenzelm@19738
    11
lemma and_de_morgan_and_absorbe: "(~(A&B)) = ((~A)&B| ~B)"
wenzelm@19738
    12
  by blast
wenzelm@19738
    13
wenzelm@19738
    14
lemma bool_if_impl_or: "(if C then A else B) --> (A|B)"
wenzelm@19738
    15
  by auto
wenzelm@19738
    16
wenzelm@19738
    17
lemma exis_elim: "(? x. x=P & Q(x)) = Q(P)"
wenzelm@19738
    18
  by blast
wenzelm@19738
    19
wenzelm@19738
    20
wenzelm@19738
    21
subsection {* Sets *}
wenzelm@19738
    22
wenzelm@19738
    23
lemma set_lemmas:
wenzelm@19738
    24
    "f(x) : (UN x. {f(x)})"
wenzelm@19738
    25
    "f x y : (UN x y. {f x y})"
wenzelm@19738
    26
    "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})"
wenzelm@19738
    27
    "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"
wenzelm@19738
    28
  by auto
wenzelm@19738
    29
wenzelm@19738
    30
text {* 2 Lemmas to add to @{text "set_lemmas"}, used also for action handling, 
wenzelm@19738
    31
   namely for Intersections and the empty list (compatibility of IOA!). *}
wenzelm@19738
    32
lemma singleton_set: "(UN b.{x. x=f(b)})= (UN b.{f(b)})"
wenzelm@19738
    33
  by blast
wenzelm@19738
    34
wenzelm@19738
    35
lemma de_morgan: "((A|B)=False) = ((~A)&(~B))"
wenzelm@19738
    36
  by blast
wenzelm@19738
    37
wenzelm@19738
    38
wenzelm@19738
    39
subsection {* Lists *}
wenzelm@19738
    40
wenzelm@19738
    41
lemma cons_not_nil: "l ~= [] --> (? x xs. l = (x#xs))"
wenzelm@19738
    42
  by (induct l) simp_all
wenzelm@19738
    43
wenzelm@17244
    44
end