src/HOLCF/IOA/ABP/Lemmas.ML
author wenzelm
Tue Dec 16 17:58:03 1997 +0100 (1997-12-16)
changeset 4423 a129b817b58a
parent 4098 71e05eb27fb6
child 4833 2e53109d4bc8
permissions -rw-r--r--
expandshort;
     1 (*  Title:      HOLCF/IOA/ABP/Lemmas.ML
     2     ID:         $Id$
     3     Author:     Olaf Mueller
     4     Copyright   1995  TU Muenchen
     5 
     6 *)
     7 
     8 (* Logic *)
     9 
    10 val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    11   by (fast_tac (claset() addDs prems) 1);
    12 qed "imp_conj_lemma";
    13 
    14 goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
    15 by (Fast_tac 1);
    16 val and_de_morgan_and_absorbe = result();
    17 
    18 goal HOL.thy "(if C then A else B) --> (A|B)";
    19 by (stac expand_if 1);
    20 by (Fast_tac 1);
    21 val bool_if_impl_or = result();
    22 
    23 (* Sets *)
    24 
    25 val set_lemmas =
    26    map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1]))
    27         ["f(x) : (UN x. {f(x)})",
    28          "f x y : (UN x y. {f x y})",
    29          "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})",
    30          "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"];
    31 
    32 (* 2 Lemmas to add to set_lemmas ... , used also for action handling, 
    33    namely for Intersections and the empty list (compatibility of IOA!)  *)
    34 goal Set.thy "(UN b.{x. x=f(b)})= (UN b.{f(b)})"; 
    35  by (rtac set_ext 1);
    36  by (Fast_tac 1);
    37 val singleton_set =result();
    38 
    39 goal HOL.thy "((A|B)=False) = ((~A)&(~B))";
    40  by (Fast_tac 1);
    41 val de_morgan = result();
    42 
    43 (* Lists *)
    44 
    45 val list_ss = simpset_of List.thy;
    46 
    47 goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
    48 by (List.list.induct_tac "l" 1);
    49 by (simp_tac list_ss 1);
    50 by (simp_tac list_ss 1);
    51 val hd_append =result();
    52 
    53 goal List.thy "l ~= [] --> (? x xs. l = (x#xs))";
    54  by (List.list.induct_tac "l" 1);
    55  by (simp_tac list_ss 1);
    56  by (Fast_tac 1);
    57 qed"cons_not_nil";