src/ZF/upair.thy
author paulson
Fri Jan 03 15:01:55 1997 +0100 (1997-01-03)
changeset 2469 b50b8c0eec01
parent 124 858ab9a9b047
child 2872 ac81a17f86f8
permissions -rw-r--r--
Implicit simpsets and clasets for FOL and ZF
paulson@2469
     1
(*  Title:      ZF/upair.thy
paulson@2469
     2
    ID:         $Id$
paulson@2469
     3
    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
paulson@2469
     4
    Copyright   1993  University of Cambridge
paulson@2469
     5
paulson@2469
     6
Definitions involving unordered pairing
paulson@2469
     7
*)
paulson@2469
     8
paulson@2469
     9
upair = ZF +
clasohm@124
    10
paulson@2469
    11
defs
paulson@2469
    12
  (* Definite descriptions -- via Replace over the set "1" *)
paulson@2469
    13
  the_def       "The(P)    == Union({y . x:{0}, P(y)})"
paulson@2469
    14
  if_def        "if(P,a,b) == THE z. P & z=a | ~P & z=b"
paulson@2469
    15
paulson@2469
    16
  (*Set difference; binary union and intersection*)
paulson@2469
    17
  Diff_def      "A - B    == { x:A . ~(x:B) }"
paulson@2469
    18
  Un_def        "A Un  B  == Union(Upair(A,B))"
paulson@2469
    19
  Int_def       "A Int B  == Inter(Upair(A,B))"
paulson@2469
    20
paulson@2469
    21
end