src/HOLCF/IOA/ABP/Lemmas.ML
changeset 3072 a31419014be5
child 3852 e694c660055b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Wed Apr 30 11:24:14 1997 +0200
     1.3 @@ -0,0 +1,57 @@
     1.4 +(*  Title:      HOLCF/IOA/ABP/Lemmas.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Olaf Mueller
     1.7 +    Copyright   1995  TU Muenchen
     1.8 +
     1.9 +*)
    1.10 +
    1.11 +(* Logic *)
    1.12 +
    1.13 +val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    1.14 +  by(fast_tac (!claset addDs prems) 1);
    1.15 +qed "imp_conj_lemma";
    1.16 +
    1.17 +goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
    1.18 +by (Fast_tac 1);
    1.19 +val and_de_morgan_and_absorbe = result();
    1.20 +
    1.21 +goal HOL.thy "(if C then A else B) --> (A|B)";
    1.22 +by (rtac (expand_if RS ssubst) 1);
    1.23 +by (Fast_tac 1);
    1.24 +val bool_if_impl_or = result();
    1.25 +
    1.26 +(* Sets *)
    1.27 +
    1.28 +val set_lemmas =
    1.29 +   map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1]))
    1.30 +        ["f(x) : (UN x. {f(x)})",
    1.31 +         "f x y : (UN x y. {f x y})",
    1.32 +         "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})",
    1.33 +         "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"];
    1.34 +
    1.35 +(* 2 Lemmas to add to set_lemmas ... , used also for action handling, 
    1.36 +   namely for Intersections and the empty list (compatibility of IOA!)  *)
    1.37 +goal Set.thy "(UN b.{x.x=f(b)})= (UN b.{f(b)})"; 
    1.38 + by (rtac set_ext 1);
    1.39 + by (Fast_tac 1);
    1.40 +val singleton_set =result();
    1.41 +
    1.42 +goal HOL.thy "((A|B)=False) = ((~A)&(~B))";
    1.43 + by (Fast_tac 1);
    1.44 +val de_morgan = result();
    1.45 +
    1.46 +(* Lists *)
    1.47 +
    1.48 +val list_ss = simpset_of "List";
    1.49 +
    1.50 +goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
    1.51 +by (List.list.induct_tac "l" 1);
    1.52 +by (simp_tac list_ss 1);
    1.53 +by (simp_tac list_ss 1);
    1.54 +val hd_append =result();
    1.55 +
    1.56 +goal List.thy "l ~= [] --> (? x xs. l = (x#xs))";
    1.57 + by (List.list.induct_tac "l" 1);
    1.58 + by (simp_tac list_ss 1);
    1.59 + by (Fast_tac 1);
    1.60 +qed"cons_not_nil";