src/HOLCF/IOA/NTP/Lemmas.ML
author nipkow
Sat, 06 Dec 1997 16:48:39 +0100
changeset 4377 2cba48b0f1c4
parent 4372 b9852572af0f
child 4423 a129b817b58a
permissions -rw-r--r--
Cleaned up arithmetic mess.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     1
(*  Title:      HOL/IOA/NTP/Lemmas.ML
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     2
    ID:         $Id$
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     3
    Author:     Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     4
    Copyright   1994  TU Muenchen
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     5
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     6
*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     7
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     8
(* Logic *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     9
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    10
  by(fast_tac (claset() addDs prems) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    11
qed "imp_conj_lemma";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    12
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    13
goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    14
  by (Fast_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    15
qed "fork_lemma";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    16
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    17
goal HOL.thy "((A --> B) & (C --> B)) = ((A | C) --> B)";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    18
  by (Fast_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    19
qed "imp_or_lem";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    20
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    21
goal HOL.thy "(X = (~ Y)) = ((~X) = Y)";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    22
  by (Fast_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    23
qed "neg_flip";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    24
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    25
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    26
(* Sets *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    27
val set_lemmas =
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    28
   map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1]))
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    29
        ["f(x) : (UN x. {f(x)})",
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    30
         "f x y : (UN x y. {f x y})",
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    31
         "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})",
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    32
         "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"];
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    33
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    34
4377
2cba48b0f1c4 Cleaned up arithmetic mess.
nipkow
parents: 4372
diff changeset
    35
(* Arithmetic *)
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    36
4377
2cba48b0f1c4 Cleaned up arithmetic mess.
nipkow
parents: 4372
diff changeset
    37
goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
2cba48b0f1c4 Cleaned up arithmetic mess.
nipkow
parents: 4372
diff changeset
    38
by(asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1);
2cba48b0f1c4 Cleaned up arithmetic mess.
nipkow
parents: 4372
diff changeset
    39
by(Blast_tac 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    40
qed "pred_suc";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    41
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    42
4377
2cba48b0f1c4 Cleaned up arithmetic mess.
nipkow
parents: 4372
diff changeset
    43
Addsimps (hd_append :: set_lemmas);