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