src/HOLCF/IOA/NTP/Lemmas.ML
author nipkow
Thu Oct 12 18:38:23 2000 +0200 (2000-10-12)
changeset 10212 33fe2d701ddd
parent 5656 f8389824189b
child 10215 1ead773b365e
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title:      HOL/IOA/NTP/Lemmas.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Konrad Slind
     4     Copyright   1994  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 & C) = ((A --> B) & (A --> C))";
    15   by (Fast_tac 1);
    16 qed "fork_lemma";
    17 
    18 goal HOL.thy "((A --> B) & (C --> B)) = ((A | C) --> B)";
    19   by (Fast_tac 1);
    20 qed "imp_or_lem";
    21 
    22 goal HOL.thy "(X = (~ Y)) = ((~X) = Y)";
    23   by (Fast_tac 1);
    24 qed "neg_flip";
    25 
    26 
    27 (* Sets *)
    28 val set_lemmas =
    29    map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1]))
    30         ["f(x) : (UN x. {f(x)})",
    31          "f x y : (UN x y. {f x y})",
    32          "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})",
    33          "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"];
    34 
    35 
    36 (* Arithmetic *)
    37 
    38 goal Arithmetic.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
    39 by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
    40 qed "pred_suc";
    41 
    42 
    43 Addsimps (hd_append :: set_lemmas);