src/HOLCF/IOA/NTP/Lemmas.thy
author wenzelm
Thu, 22 Nov 2007 14:51:34 +0100
changeset 25456 6f79698f294d
parent 19739 c58ef2aa5430
child 35174 e15040ae75d7
permissions -rw-r--r--
tuned;
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.thy
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
*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     5
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     6
theory Lemmas
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     7
imports Main
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     8
begin
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     9
19739
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    10
subsubsection {* Logic *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    11
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    12
lemma neg_flip: "(X = (~ Y)) = ((~X) = Y)"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    13
  by blast
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    14
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    15
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    16
subsection {* Sets *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    17
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    18
lemma set_lemmas:
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    19
  "f(x) : (UN x. {f(x)})"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    20
  "f x y : (UN x y. {f x y})"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    21
  "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    22
  "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    23
  by auto
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    24
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    25
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    26
subsection {* Arithmetic *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    27
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    28
lemma pred_suc: "0<x ==> (x - 1 = y) = (x = Suc(y))"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    29
  by (simp add: diff_Suc split add: nat.split)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    30
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    31
lemmas [simp] = hd_append set_lemmas
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    32
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    33
end