src/HOL/IOA/ABP/Lemmas.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1894 c2c8279d40f0
permissions -rw-r--r--
Dep. on Provers/nat_transitive
mueller@1139
     1
(*  Title:      HOL/IOA/example/Lemmas.ML
nipkow@1050
     2
    ID:         $Id$
mueller@1139
     3
    Author:     Tobias Nipkow & Konrad Slind
mueller@1139
     4
    Copyright   1994  TU Muenchen
nipkow@1050
     5
nipkow@1050
     6
*)
nipkow@1050
     7
nipkow@1050
     8
(* Logic *)
nipkow@1050
     9
nipkow@1050
    10
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
berghofe@1894
    11
  by(fast_tac (!claset addDs prems) 1);
nipkow@1050
    12
qed "imp_conj_lemma";
nipkow@1050
    13
nipkow@1050
    14
goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
berghofe@1894
    15
by (Fast_tac 1);
nipkow@1050
    16
val and_de_morgan_and_absorbe = result();
nipkow@1050
    17
nipkow@1050
    18
goal HOL.thy "(if C then A else B) --> (A|B)";
nipkow@1050
    19
by (rtac (expand_if RS ssubst) 1);
berghofe@1894
    20
by (Fast_tac 1);
nipkow@1050
    21
val bool_if_impl_or = result();
nipkow@1050
    22
nipkow@1050
    23
(* Sets *)
nipkow@1050
    24
nipkow@1050
    25
val set_lemmas =
berghofe@1894
    26
   map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1]))
nipkow@1050
    27
        ["f(x) : (UN x. {f(x)})",
nipkow@1050
    28
         "f x y : (UN x y. {f x y})",
nipkow@1050
    29
         "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})",
nipkow@1050
    30
         "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"];
nipkow@1050
    31
nipkow@1050
    32
(* 2 Lemmas to add to set_lemmas ... , used also for action handling, 
nipkow@1050
    33
   namely for Intersections and the empty list (compatibility of IOA!)  *)
nipkow@1050
    34
goal Set.thy "(UN b.{x.x=f(b)})= (UN b.{f(b)})"; 
nipkow@1050
    35
 by (rtac set_ext 1);
berghofe@1894
    36
 by (Fast_tac 1);
nipkow@1050
    37
val singleton_set =result();
nipkow@1050
    38
nipkow@1050
    39
goal HOL.thy "((A|B)=False) = ((~A)&(~B))";
berghofe@1894
    40
 by (Fast_tac 1);
nipkow@1050
    41
val de_morgan = result();
nipkow@1050
    42
nipkow@1050
    43
(* Lists *)
nipkow@1050
    44
clasohm@1266
    45
val list_ss = simpset_of "List";
clasohm@1266
    46
nipkow@1050
    47
goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
nipkow@1050
    48
by (List.list.induct_tac "l" 1);
nipkow@1050
    49
by (simp_tac list_ss 1);
nipkow@1050
    50
by (simp_tac list_ss 1);
nipkow@1050
    51
val hd_append =result();
nipkow@1050
    52
nipkow@1050
    53
goal List.thy "l ~= [] --> (? x xs. l = (x#xs))";
nipkow@1050
    54
 by (List.list.induct_tac "l" 1);
nipkow@1050
    55
 by (simp_tac list_ss 1);
berghofe@1894
    56
 by (Fast_tac 1);
clasohm@1465
    57
qed"cons_not_nil";