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