doc-src/Logics/ZF-rules.txt
author nipkow
Fri, 17 Nov 1995 12:08:04 +0100
changeset 1337 ad834f39d878
parent 104 d8205bb279a7
permissions -rw-r--r--
README -> README.html
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%%%% RULES.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
\idx{empty_set}    ~(x:0)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
\idx{union_iff}    A:Union(C) <-> (EX B:C. A:B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
\idx{power_set}    A : Pow(B) <-> A <= B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
\idx{infinity}     0:Inf & (ALL y:Inf. succ(y): Inf)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
\idx{foundation}   A=0 | (EX x:A. ALL y:x. ~ y:A)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
\idx{replacement}  (!!x y z.[| x:A; P(x,y); P(x,z) |] ==> y=z) ==>
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
                   y : PrimReplace(A,P) <-> (EX x:A. P(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
\idx{Replace_def}  Replace(A,P) == PrimReplace(A, %x y. (EX!z.P(x,z)) & P(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
\idx{RepFun_def}   RepFun(A,f) == Replace(A, %x u. u=f(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
\idx{Collect_def}  Collect(A,P) == \{ y . x:A, x=y & P(x)\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
\idx{the_def}      The(P) == Union(\{y . x:\{0\}, P(y)\})
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
\idx{Upair_def}    Upair(a,b) == 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
                   \{y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
\idx{Inter_def}    Inter(A) == \{ x:Union(A) . ALL y:A. x:y\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
\idx{Un_def}       A Un  B  == Union(Upair(A,B))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
\idx{Int_def}      A Int B  == Inter(Upair(A,B))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
\idx{Diff_def}     A - B    == \{ x:A . ~(x:B) \}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
\idx{cons_def}     cons(a,A) == Upair(a,a) Un A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
\idx{succ_def}     succ(i) == cons(i,i)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
\idx{Pair_def}     <a,b>  == \{\{a,a\}, \{a,b\}\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
\idx{fst_def}      fst(A) == THE x. EX y. A=<x,y>
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
\idx{snd_def}      snd(A) == THE y. EX x. A=<x,y>
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
\idx{split_def}    split(p,c) == THE y. EX a b. p=<a,b> & y=c(a,b)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
\idx{Sigma_def}    Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
\idx{domain_def}   domain(r) == \{a:Union(Union(r)) . EX b. <a,b> : r\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
\idx{range_def}    range(r) == \{b:Union(Union(r)) . EX a. <a,b> : r\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
\idx{field_def}    field(r) == domain(r) Un range(r)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
\idx{image_def}    r``A == \{y : range(r) . EX x:A. <x,y> : r\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
\idx{vimage_def}   r -`` A == \{x : domain(r) . EX y:A. <x,y> : r\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
\idx{lam_def}      Lambda(A,f) == RepFun(A, %x. <x,f(x)>)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
\idx{apply_def}    f`a == THE y. <a,y> : f
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
\idx{restrict_def} restrict(f,A) == lam x:A.f`x
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
\idx{Pi_def}       Pi(A,B)  == \{f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
\idx{subset_def}         A <= B == ALL x:A. x:B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
\idx{strict_subset_def}  A <! B   == A <=B & ~(A=B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
\idx{extension}          A = B <-> A <= B & B <= A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
\idx{Ball_def}   Ball(A,P) == ALL x. x:A --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
\idx{Bex_def}    Bex(A,P) == EX x. x:A & P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
%%%% LEMMAS.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
\idx{ballI}       [| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
\idx{bspec}       [| ALL x:A. P(x);  x: A |] ==> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
\idx{ballE}       [| ALL x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
\idx{ball_cong}   [| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
            (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
\idx{bexI}        [| P(x);  x: A |] ==> EX x:A. P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
\idx{bexCI}       [| ALL x:A. ~P(x) ==> P(a);  a: A |] ==> EX x:A.P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
\idx{bexE}        [| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q |] ==> Q
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
\idx{bex_cong}    [| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
            (EX x:A. P(x)) <-> (EX x:A'. P'(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
\idx{subsetI}       (!!x.x:A ==> x:B) ==> A <= B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
\idx{subsetD}       [| A <= B;  c:A |] ==> c:B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
\idx{subsetCE}      [| A <= B;  ~(c:A) ==> P;  c:B ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
\idx{subset_refl}   A <= A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
\idx{subset_trans}  [| A<=B;  B<=C |] ==> A<=C
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
\idx{equalityI}     [| A <= B;  B <= A |] ==> A = B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
\idx{equalityD1}    A = B ==> A<=B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
\idx{equalityD2}    A = B ==> B<=A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
\idx{equalityE}     [| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
\idx{emptyE}          a:0 ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
\idx{empty_subsetI}   0 <= A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
\idx{equals0I}        [| !!y. y:A ==> False |] ==> A=0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
\idx{equals0D}        [| A=0;  a:A |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
\idx{PowI}            A <= B ==> A : Pow(B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
\idx{PowD}            A : Pow(B)  ==>  A<=B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
\idx{ReplaceI}      [| x: A;  P(x,b);  !!y. P(x,y) ==> y=b |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
              b : \{y. x:A, P(x,y)\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
\idx{ReplaceE}      [| b : \{y. x:A, P(x,y)\};  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
                 !!x. [| x: A;  P(x,b);  ALL y. P(x,y)-->y=b |] ==> R 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
              |] ==> R
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
\idx{Replace_cong}  [| A=B;  !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
              \{y. x:A, P(x,y)\} = \{y. x:B, Q(x,y)\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
\idx{RepFunI}       [| a : A |] ==> f(a) : RepFun(A,f)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
\idx{RepFunE}       [| b : RepFun(A, %x.f(x));  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
                 !!x.[| x:A;  b=f(x) |] ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
\idx{RepFun_cong}   [| A=B;  !!x. x:B ==> f(x)=g(x) |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
              RepFun(A, %x.f(x)) = RepFun(B, %x.g(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
\idx{separation}     x : Collect(A,P) <-> x:A & P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
\idx{CollectI}       [| a:A;  P(a) |] ==> a : \{x:A. P(x)\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
\idx{CollectE}       [| a : \{x:A. P(x)\};  [| a:A; P(a) |] ==> R |] ==> R
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
\idx{CollectD1}      a : \{x:A. P(x)\} ==> a:A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   110
\idx{CollectD2}      a : \{x:A. P(x)\} ==> P(a)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   111
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
\idx{Collect_cong}   [| A=B;  !!x. x:B ==> P(x) <-> Q(x) |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
               \{x:A. P(x)\} = \{x:B. Q(x)\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
\idx{UnionI}    [| B: C;  A: B |] ==> A: Union(C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
\idx{UnionE}    [| A : Union(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
\idx{InterI}    [| !!x. x: C ==> A: x;  c:C |] ==> A : Inter(C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
\idx{InterD}    [| A : Inter(C);  B : C |] ==> A : B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
\idx{InterE}    [| A : Inter(C);  A:B ==> R;  ~ B:C ==> R |] ==> R
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
\idx{UN_I}      [| a: A;  b: B(a) |] ==> b: (UN x:A. B(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
\idx{UN_E}      [| b : (UN x:A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R |] ==> R
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
\idx{INT_I}     [| !!x. x: A ==> b: B(x);  a: A |] ==> b: (INT x:A. B(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
\idx{INT_E}     [| b : (INT x:A. B(x));  a: A |] ==> b : B(a)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
%%%% UPAIR.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
\idx{pairing}      a:Upair(b,c) <-> (a=b | a=c)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
\idx{UpairI1}      a : Upair(a,b)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
\idx{UpairI2}      b : Upair(a,b)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
\idx{UpairE}       [| a : Upair(b,c);  a = b ==> P;  a = c ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
\idx{UnI1}         c : A ==> c : A Un B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
\idx{UnI2}         c : B ==> c : A Un B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   138
\idx{UnCI}         (~c : B ==> c : A) ==> c : A Un B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
\idx{UnE}          [| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
\idx{IntI}         [| c : A;  c : B |] ==> c : A Int B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
\idx{IntD1}        c : A Int B ==> c : A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
\idx{IntD2}        c : A Int B ==> c : B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
\idx{IntE}         [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
\idx{DiffI}        [| c : A;  ~ c : B |] ==> c : A - B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
\idx{DiffD1}       c : A - B ==> c : A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
\idx{DiffD2}       [| c : A - B;  c : B |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
\idx{DiffE}        [| c : A - B;  [| c:A; ~ c:B |] ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   151
\idx{consI1}       a : cons(a,B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
\idx{consI2}       a : B ==> a : cons(b,B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
\idx{consCI}       (~ a:B ==> a=b) ==> a: cons(b,B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
\idx{consE}        [| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   155
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
\idx{singletonI}   a : \{a\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
\idx{singletonE}   [| a : \{b\}; a=b ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
\idx{succI1}       i : succ(i)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
\idx{succI2}       i : j ==> i : succ(j)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
\idx{succCI}       (~ i:j ==> i=j) ==> i: succ(j)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
\idx{succE}        [| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
\idx{succ_neq_0}   [| succ(n)=0 |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
\idx{succ_inject}  succ(m) = succ(n) ==> m=n
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   165
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   166
\idx{the_equality}     [| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
\idx{theI}             EX! x. P(x) ==> P(THE x. P(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
\idx{mem_anti_sym}     [| a:b;  b:a |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   170
\idx{mem_anti_refl}    a:a ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
%%% SUBSET.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
\idx{Union_upper}       B:A ==> B <= Union(A)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
\idx{Union_least}       [| !!x. x:A ==> x<=C |] ==> Union(A) <= C
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   177
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
\idx{Inter_lower}       B:A ==> Inter(A) <= B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
\idx{Inter_greatest}    [| a:A;  !!x. x:A ==> C<=x |] ==> C <= Inter(A)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
\idx{Un_upper1}         A <= A Un B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
\idx{Un_upper2}         B <= A Un B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
\idx{Un_least}          [| A<=C;  B<=C |] ==> A Un B <= C
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
\idx{Int_lower1}        A Int B <= A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
\idx{Int_lower2}        A Int B <= B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
\idx{Int_greatest}      [| C<=A;  C<=B |] ==> C <= A Int B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   188
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
\idx{Diff_subset}       A-B <= A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
\idx{Diff_contains}     [| C<=A;  C Int B = 0 |] ==> C <= A-B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
\idx{Collect_subset}    Collect(A,P) <= A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   193
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
%%% PAIR.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   195
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
\idx{Pair_inject1}    <a,b> = <c,d> ==> a=c
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
\idx{Pair_inject2}    <a,b> = <c,d> ==> b=d
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
\idx{Pair_inject}     [| <a,b> = <c,d>;  [| a=c; b=d |] ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
\idx{Pair_neq_0}      <a,b>=0 ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   200
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
\idx{fst_conv}        fst(<a,b>) = a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
\idx{snd_conv}        snd(<a,b>) = b
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
\idx{split_conv}      split(<a,b>, %x y.c(x,y)) = c(a,b)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
\idx{SigmaI}    [| a:A;  b:B(a) |] ==> <a,b> : (SUM x:A. B(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
\idx{SigmaE}    [| c: (SUM x:A. B(x));  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
             !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
          |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
\idx{SigmaE2}   [| <a,b> : (SUM x:A. B(x));    
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
             [| a:A;  b:B(a) |] ==> P   
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
          |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
%%% DOMRANGE.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   217
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
\idx{domainI}        <a,b>: r ==> a : domain(r)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
\idx{domainE}        [| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
\idx{domain_subset}  domain(Sigma(A,B)) <= A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
\idx{rangeI}         <a,b>: r ==> b : range(r)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
\idx{rangeE}         [| b : range(r);  !!x. <x,b>: r ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
\idx{range_subset}   range(A*B) <= B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   226
\idx{fieldI1}        <a,b>: r ==> a : field(r)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
\idx{fieldI2}        <a,b>: r ==> b : field(r)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
\idx{fieldCI}        (~ <c,a>:r ==> <a,b>: r) ==> a : field(r)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
\idx{fieldE}         [| a : field(r);  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   231
                  !!x. <a,x>: r ==> P;  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   232
                  !!x. <x,a>: r ==> P      
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
               |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   234
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   235
\idx{field_subset}   field(A*A) <= A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
\idx{imageI}         [| <a,b>: r;  a:A |] ==> b : r``A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   238
\idx{imageE}         [| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   240
\idx{vimageI}        [| <a,b>: r;  b:B |] ==> a : r-``B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
\idx{vimageE}        [| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   243
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
%%% FUNC.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   245
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   246
\idx{fun_is_rel}       f: (PROD x:A.B(x)) ==> f <= Sigma(A,B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   247
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   248
\idx{apply_equality}   [| <a,b>: f;  f: (PROD x:A.B(x)) |] ==> f`a = b
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   249
\idx{apply_equality2}  [| <a,b>: f;  <a,c>: f;  f: (PROD x:A.B(x)) |] ==> b=c
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   250
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   251
\idx{apply_type}       [| f: (PROD x:A.B(x));  a:A |] ==> f`a : B(a)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   252
\idx{apply_Pair}       [| f: (PROD x:A.B(x));  a:A |] ==> <a,f`a>: f
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   253
\idx{apply_iff}        [| f: (PROD x:A.B(x));  a:A |] ==> <a,b>: f <-> f`a = b
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   254
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   255
\idx{domain_type}      [| <a,b> : f;  f: (PROD x:A.B(x)) |] ==> a : A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   256
\idx{range_type}       [| <a,b> : f;  f: (PROD x:A.B(x)) |] ==> b : B(a)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   257
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   258
\idx{Pi_type}          [| f: A->C;  !!x. x:A ==> f`x : B(x) |] ==> f: Pi(A,B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
\idx{domain_of_fun}    f : Pi(A,B) ==> domain(f)=A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
\idx{range_of_fun}     f : Pi(A,B) ==> f: A->range(f)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
\idx{fun_extension}    [| f : (PROD x:A.B(x));  g: (PROD x:A.D(x));  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   263
                    !!x. x:A ==> f`x = g`x       
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
                 |] ==> f=g
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   266
\idx{lamI}             a:A ==> <a,b(a)> : (lam x:A. b(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   267
\idx{lamE}             [| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   268
                 |] ==>  P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   269
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   270
\idx{lam_type}         [| !!x. x:A ==> b(x): B(x) |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   271
                 (lam x:A.b(x)) : (PROD x:A.B(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   273
\idx{beta_conv}        a : A ==> (lam x:A.b(x)) ` a = b(a)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   274
\idx{eta_conv}         f : (PROD x:A.B(x)) ==> (lam x:A. f`x) = f
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   275
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   276
\idx{lam_theI}         (!!x. x:A ==> EX! y. Q(x,y)) ==> EX h. ALL x:A. Q(x, h`x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   277
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   278
\idx{restrict_conv}          a : A ==> restrict(f,A) ` a = f`a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   279
\idx{restrict_type}          [| !!x. x:A ==> f`x: B(x) |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   280
                       restrict(f,A) : (PROD x:A.B(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   281
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   282
\idx{fun_empty}              0: 0->0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   283
\idx{fun_single}             \{<a,b>\} : \{a\} -> \{b\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   284
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   285
\idx{fun_disjoint_Un}        [| f: A->B;  g: C->D;  A Int C = 0  |] ==>  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   286
                       (f Un g) : (A Un C) -> (B Un D)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   287
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   288
\idx{fun_disjoint_apply1}    [| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   289
                       (f Un g)`a = f`a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   290
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   291
\idx{fun_disjoint_apply2}    [| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   292
                       (f Un g)`c = g`c
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   293
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   294
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   295
%%% SIMPDATA.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   296
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   297
  a\in a 		& \bimp &  False\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   298
  a\in \emptyset 	& \bimp &  False\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   299
  a \in A \union B 	& \bimp &  a\in A \disj a\in B\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   300
  a \in A \inter B 	& \bimp &  a\in A \conj a\in B\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
  a \in A-B 		& \bimp &  a\in A \conj \neg (a\in B)\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
  a \in {\tt cons}(b,B) & \bimp &  a=b \disj a\in B\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
  i \in {\tt succ}(j) 	& \bimp &  i=j \disj i\in j\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   304
  A\in \bigcup(C) 	& \bimp &  (\exists B. B\in C \conj A\in B)\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
  A\in \bigcap(C) 	& \bimp &  (\forall B. B\in C \imp A\in B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   306
	\qquad (\exists B. B\in C)\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   307
  a \in {\tt Collect}(A,P) 	& \bimp &  a\in A \conj P(a)\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   308
  b \in {\tt RepFun}(A,f) 	& \bimp &  (\exists x. x\in A \conj b=f(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   309
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   310
equalities.ML perm.ML plus.ML nat.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
----------------------------------------------------------------
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
equalities.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   314
\idx{Int_absorb}         A Int A = A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   315
\idx{Int_commute}        A Int B = B Int A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   316
\idx{Int_assoc}          (A Int B) Int C  =  A Int (B Int C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   317
\idx{Int_Un_distrib}     (A Un B) Int C  =  (A Int C) Un (B Int C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
\idx{Un_absorb}          A Un A = A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   320
\idx{Un_commute}         A Un B = B Un A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   321
\idx{Un_assoc}           (A Un B) Un C  =  A Un (B Un C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   322
\idx{Un_Int_distrib}     (A Int B) Un C  =  (A Un C) Int (B Un C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   323
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   324
\idx{Diff_cancel}        A-A = 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   325
\idx{Diff_disjoint}      A Int (B-A) = 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   326
\idx{Diff_partition}     A<=B ==> A Un (B-A) = B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   327
\idx{double_complement}  [| A<=B; B<= C |] ==> (B - (C-A)) = A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   328
\idx{Diff_Un}            A - (B Un C) = (A-B) Int (A-C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   329
\idx{Diff_Int}           A - (B Int C) = (A-B) Un (A-C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   330
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   331
\idx{Union_Un_distrib}   Union(A Un B) = Union(A) Un Union(B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   332
\idx{Inter_Un_distrib}   [| a:A;  b:B |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   333
                   Inter(A Un B) = Inter(A) Int Inter(B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   334
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
\idx{Int_Union_RepFun}   A Int Union(B) = (UN C:B. A Int C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   337
\idx{Un_Inter_RepFun}    b:B ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   338
                   A Un Inter(B) = (INT C:B. A Un C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   339
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
\idx{SUM_Un_distrib1}    (SUM x:A Un B. C(x)) = 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
                   (SUM x:A. C(x)) Un (SUM x:B. C(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   342
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   343
\idx{SUM_Un_distrib2}    (SUM x:C. A(x) Un B(x)) =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   344
                   (SUM x:C. A(x)) Un (SUM x:C. B(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   345
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   346
\idx{SUM_Int_distrib1}   (SUM x:A Int B. C(x)) =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   347
                   (SUM x:A. C(x)) Int (SUM x:B. C(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   348
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   349
\idx{SUM_Int_distrib2}   (SUM x:C. A(x) Int B(x)) =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   350
                   (SUM x:C. A(x)) Int (SUM x:C. B(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   351
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   352
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   353
----------------------------------------------------------------
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   354
perm.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   355
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
\idx{comp_def}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
        r O s == \{xz : domain(s)*range(r) . 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   358
                  EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r\}),
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
\idx{id_def}                    (*the identity function for A*)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
        id(A) == (lam x:A. x)),
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   361
\idx{inj_def} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   362
        inj(A,B) == 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   363
            \{ f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x\}),
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   364
\idx{surj_def} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   365
        surj(A,B) == \{ f: A->B . ALL y:B. EX x:A. f`x=y\}),
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   366
\idx{bij_def}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
        bij(A,B) == inj(A,B) Int surj(A,B))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   368
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   369
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   370
\idx{surj_is_fun}        f: surj(A,B) ==> f: A->B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
\idx{fun_is_surj}        f : Pi(A,B) ==> f: surj(A,range(f))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   373
\idx{inj_is_fun}         f: inj(A,B) ==> f: A->B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   374
\idx{inj_equality}       [| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   376
\idx{bij_is_fun}         f: bij(A,B) ==> f: A->B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   377
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   378
\idx{inj_converse_surj}  f: inj(A,B) ==> converse(f): surj(range(f), A)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   379
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   380
\idx{left_inverse}       [| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   381
\idx{right_inverse}      [| f: inj(A,B);  b: range(f) |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   382
                   f`(converse(f)`b) = b
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   383
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   384
\idx{inj_converse_inj}   f: inj(A,B) ==> converse(f): inj(range(f), A)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   385
\idx{bij_converse_bij}   f: bij(A,B) ==> converse(f): bij(B,A)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   386
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   387
\idx{comp_type}          [| s<=A*B;  r<=B*C |] ==> (r O s) <= A*C
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   388
\idx{comp_assoc}         (r O s) O t = r O (s O t)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   389
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   390
\idx{left_comp_id}       r<=A*B ==> id(B) O r = r
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   391
\idx{right_comp_id}      r<=A*B ==> r O id(A) = r
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   392
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   393
\idx{comp_func}          [| g: A->B;  f: B->C |] ==> (f O g) : A->C
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   394
\idx{comp_func_apply}    [| g: A->B;  f: B->C;  a:A |] ==> (f O g)`a = f`(g`a)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   395
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   396
\idx{comp_inj}      [| g: inj(A,B);   f: inj(B,C)  |] ==> (f O g) : inj(A,C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   397
\idx{comp_surj}     [| g: surj(A,B);  f: surj(B,C) |] ==> (f O g) : surj(A,C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   398
\idx{comp_bij}      [| g: bij(A,B);  f: bij(B,C) |] ==> (f O g) : bij(A,C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   399
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   400
\idx{left_comp_inverse}     f: inj(A,B) ==> converse(f) O f = id(A)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   401
\idx{right_comp_inverse}    f: surj(A,B) ==> f O converse(f) = id(B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   402
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   403
\idx{bij_disjoint_Un}   
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   404
    [| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   405
    (f Un g) : bij(A Un C, B Un D)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   406
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   407
\idx{restrict_bij}  [| f: inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   409
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   410
----------------------------------------------------------------
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   411
plus.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   412
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
\idx{plus_def}      A+B == \{0\}*A Un \{\{0\}\}*B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   414
\idx{Inl_def}       Inl(a) == < 0 ,a>
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   415
\idx{Inr_def}       Inr(b) == <\{0\},b>
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   416
\idx{when_def}      when(u,c,d) == 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   417
                THE y. EX z.(u=Inl(z) & y=c(z)) | (u=Inr(z) & y=d(z))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   418
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   419
\idx{plus_InlI}     a : A ==> Inl(a) : A+B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   420
\idx{plus_InrI}     b : B ==> Inr(b) : A+B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   421
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   422
\idx{Inl_inject}    Inl(a) = Inl(b) ==>  a=b
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   423
\idx{Inr_inject}    Inr(a) = Inr(b) ==> a=b
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   424
\idx{Inl_neq_Inr}   Inl(a)=Inr(b) ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   425
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   426
\idx{plusE2}        u: A+B ==> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   427
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   428
\idx{when_Inl_conv} when(Inl(a),c,d) = c(a)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   429
\idx{when_Inr_conv} when(Inr(b),c,d) = d(b)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   430
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
\idx{when_type}     [| u: A+B; 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   432
                 !!x. x: A ==> c(x): C(Inl(x));   
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   433
                 !!y. y: B ==> d(y): C(Inr(y)) 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   434
              |] ==> when(u,c,d) : C(u)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   435
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   436
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   437
----------------------------------------------------------------
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   438
nat.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   439
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   440
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   441
\idx{nat_def}       nat == lfp(lam r: Pow(Inf). \{0\} Un RepFun(r,succ))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
\idx{nat_case_def}  nat_case(n,a,b) == 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   443
                THE y. n=0 & y=a | (EX x. n=succ(x) & y=b(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
\idx{nat_rec_def}   nat_rec(k,a,b) == 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   445
                transrec(nat, k, %n f. nat_case(n, a, %m. b(m, f`m)))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   446
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   447
\idx{nat_0_I}       0 : nat
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   448
\idx{nat_succ_I}    n : nat ==> succ(n) : nat
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   449
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   450
\idx{nat_induct}        
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   451
    [| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   452
    |] ==> P(n)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   453
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   454
\idx{nat_case_0_conv}       nat_case(0,a,b) = a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   455
\idx{nat_case_succ_conv}    nat_case(succ(m),a,b) = b(m)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   456
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   457
\idx{nat_case_type}     
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   458
    [| n: nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m))  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   459
    |] ==> nat_case(n,a,b) : C(n)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   460
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   461
\idx{nat_rec_0_conv}        nat_rec(0,a,b) = a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   462
\idx{nat_rec_succ_conv}     m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   463
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   464
\idx{nat_rec_type}      
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   465
    [| n: nat;  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   466
       a: C(0);  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   467
       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   468
    |] ==> nat_rec(n,a,b) : C(n)