src/HOLCF/IOA/ABP/Lemmas.ML
author paulson
Thu Feb 19 18:24:08 2004 +0100 (2004-02-19)
changeset 14401 477380c74c1d
parent 13524 604d0f3622d6
child 14981 e73f8140af78
permissions -rw-r--r--
removal of the legacy ML structure List
mueller@3072
     1
(*  Title:      HOLCF/IOA/ABP/Lemmas.ML
mueller@3072
     2
    ID:         $Id$
wenzelm@12218
     3
    Author:     Olaf Müller
wenzelm@12218
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
mueller@3072
     5
*)
mueller@3072
     6
mueller@3072
     7
(* Logic *)
mueller@3072
     8
mueller@3072
     9
goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
mueller@3072
    10
by (Fast_tac 1);
mueller@3072
    11
val and_de_morgan_and_absorbe = result();
mueller@3072
    12
mueller@3072
    13
goal HOL.thy "(if C then A else B) --> (A|B)";
nipkow@4833
    14
by (stac split_if 1);
mueller@3072
    15
by (Fast_tac 1);
mueller@3072
    16
val bool_if_impl_or = result();
mueller@3072
    17
mueller@3072
    18
(* Sets *)
mueller@3072
    19
mueller@3072
    20
val set_lemmas =
mueller@3072
    21
   map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1]))
mueller@3072
    22
        ["f(x) : (UN x. {f(x)})",
mueller@3072
    23
         "f x y : (UN x y. {f x y})",
mueller@3072
    24
         "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})",
mueller@3072
    25
         "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"];
mueller@3072
    26
mueller@3072
    27
(* 2 Lemmas to add to set_lemmas ... , used also for action handling, 
mueller@3072
    28
   namely for Intersections and the empty list (compatibility of IOA!)  *)
wenzelm@3852
    29
goal Set.thy "(UN b.{x. x=f(b)})= (UN b.{f(b)})"; 
mueller@3072
    30
 by (rtac set_ext 1);
mueller@3072
    31
 by (Fast_tac 1);
mueller@3072
    32
val singleton_set =result();
mueller@3072
    33
mueller@3072
    34
goal HOL.thy "((A|B)=False) = ((~A)&(~B))";
mueller@3072
    35
 by (Fast_tac 1);
mueller@3072
    36
val de_morgan = result();
mueller@3072
    37
mueller@3072
    38
(* Lists *)
mueller@3072
    39
paulson@14401
    40
Goal "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
berghofe@5192
    41
by (induct_tac "l" 1);
paulson@14401
    42
by (Simp_tac 1);
paulson@14401
    43
by (Simp_tac 1);
mueller@3072
    44
val hd_append =result();
mueller@3072
    45
paulson@14401
    46
Goal "l ~= [] --> (? x xs. l = (x#xs))";
berghofe@5192
    47
 by (induct_tac "l" 1);
paulson@14401
    48
 by (Simp_tac 1);
mueller@3072
    49
 by (Fast_tac 1);
mueller@3072
    50
qed"cons_not_nil";