doc-src/Logics/CTT-eg.txt
author paulson
Fri Feb 16 18:00:47 1996 +0100 (1996-02-16)
changeset 1512 ce37c64244c0
parent 359 b5a2e9503a7a
child 5151 1e944fe5ce96
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
(**** CTT examples -- process using Doc/tout CTT-eg.txt  ****)
lcp@104
     2
lcp@104
     3
Pretty.setmargin 72;  (*existing macros just allow this margin*)
lcp@104
     4
print_depth 0;
lcp@104
     5
lcp@104
     6
lcp@104
     7
(*** Type inference, from CTT/ex/typechk.ML ***)
lcp@104
     8
lcp@115
     9
goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A";
lcp@104
    10
by (resolve_tac [ProdI] 1);
lcp@104
    11
by (eresolve_tac [NE] 2);
lcp@104
    12
by (resolve_tac [NI0] 2);
lcp@104
    13
by (assume_tac 2);
lcp@104
    14
by (resolve_tac [NF] 1);
lcp@104
    15
lcp@104
    16
lcp@104
    17
lcp@104
    18
(*** Logical reasoning, from CTT/ex/elim.ML ***)
lcp@104
    19
lcp@115
    20
val prems = goal CTT.thy
lcp@104
    21
    "[| A type;  \
lcp@104
    22
\       !!x. x:A ==> B(x) type;       \
lcp@104
    23
\       !!x. x:A ==> C(x) type;       \
lcp@104
    24
\       p: SUM x:A. B(x) + C(x)       \
lcp@104
    25
\    |] ==>  ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))";
lcp@104
    26
by (resolve_tac (prems RL [SumE]) 1);
lcp@104
    27
by (eresolve_tac [PlusE] 1);
lcp@104
    28
by (resolve_tac [PlusI_inl] 1);
lcp@104
    29
by (resolve_tac [SumI] 1);
lcp@104
    30
by (assume_tac 1);
lcp@104
    31
by (assume_tac 1);
lcp@104
    32
by (typechk_tac prems);
lcp@104
    33
by (pc_tac prems 1);
lcp@104
    34
lcp@104
    35
lcp@104
    36
(*** Currying, from CTT/ex/elim.ML ***)
lcp@104
    37
lcp@115
    38
val prems = goal CTT.thy
lcp@359
    39
    "[| A type; !!x. x:A ==> B(x) type; 			\
lcp@359
    40
\               !!z. z: (SUM x:A. B(x)) ==> C(z) type 		\
lcp@359
    41
\    |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).	\
lcp@359
    42
\                     (PROD x:A . PROD y:B(x) . C(<x,y>))";
lcp@104
    43
by (intr_tac prems);
lcp@104
    44
by (eresolve_tac [ProdE] 1);
lcp@104
    45
by (intr_tac prems);
lcp@104
    46
lcp@104
    47
lcp@104
    48
(*** Axiom of Choice ***)
lcp@104
    49
lcp@115
    50
val prems = goal CTT.thy   
lcp@104
    51
    "[| A type;  !!x. x:A ==> B(x) type;  \
lcp@104
    52
\       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type  \
lcp@359
    53
\    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).    \
lcp@359
    54
\                        (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
lcp@104
    55
by (intr_tac prems);
lcp@104
    56
by (eresolve_tac [ProdE RS SumE_fst] 1);
lcp@104
    57
by (assume_tac 1);
lcp@104
    58
by (resolve_tac [replace_type] 1);
lcp@104
    59
by (resolve_tac [subst_eqtyparg] 1);
lcp@104
    60
by (resolve_tac [ProdC] 1);
lcp@104
    61
by (typechk_tac (SumE_fst::prems));
lcp@104
    62
by (eresolve_tac [ProdE RS SumE_snd] 1);
lcp@104
    63
by (typechk_tac prems);
lcp@104
    64
lcp@104
    65
lcp@104
    66
lcp@104
    67
lcp@115
    68
> goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A";
lcp@104
    69
Level 0
lcp@104
    70
lam n. rec(n,0,%x y. x) : ?A
lcp@104
    71
 1. lam n. rec(n,0,%x y. x) : ?A
lcp@104
    72
> by (resolve_tac [ProdI] 1);
lcp@104
    73
Level 1
lcp@104
    74
lam n. rec(n,0,%x y. x) : PROD x:?A1. ?B1(x)
lcp@104
    75
 1. ?A1 type
lcp@104
    76
 2. !!n. n : ?A1 ==> rec(n,0,%x y. x) : ?B1(n)
lcp@104
    77
> by (eresolve_tac [NE] 2);
lcp@104
    78
Level 2
lcp@104
    79
lam n. rec(n,0,%x y. x) : PROD x:N. ?C2(x,x)
lcp@104
    80
 1. N type
lcp@104
    81
 2. !!n. 0 : ?C2(n,0)
lcp@104
    82
 3. !!n x y. [| x : N; y : ?C2(n,x) |] ==> x : ?C2(n,succ(x))
lcp@104
    83
> by (resolve_tac [NI0] 2);
lcp@104
    84
Level 3
lcp@104
    85
lam n. rec(n,0,%x y. x) : N --> N
lcp@104
    86
 1. N type
lcp@104
    87
 2. !!n x y. [| x : N; y : N |] ==> x : N
lcp@104
    88
> by (assume_tac 2);
lcp@104
    89
Level 4
lcp@104
    90
lam n. rec(n,0,%x y. x) : N --> N
lcp@104
    91
 1. N type
lcp@104
    92
> by (resolve_tac [NF] 1);
lcp@104
    93
Level 5
lcp@104
    94
lam n. rec(n,0,%x y. x) : N --> N
lcp@104
    95
No subgoals!
lcp@104
    96
lcp@104
    97
lcp@104
    98
lcp@104
    99
lcp@115
   100
> val prems = goal CTT.thy
lcp@104
   101
#     "[| A type;  \
lcp@104
   102
# \       !!x. x:A ==> B(x) type;       \
lcp@104
   103
# \       !!x. x:A ==> C(x) type;       \
lcp@104
   104
# \       p: SUM x:A. B(x) + C(x)       \
lcp@104
   105
# \    |] ==>  ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))";
lcp@104
   106
Level 0
lcp@104
   107
?a : (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   108
 1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   109
> by (resolve_tac (prems RL [SumE]) 1);
lcp@104
   110
Level 1
lcp@104
   111
split(p,?c1) : (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   112
 1. !!x y.
lcp@104
   113
       [| x : A; y : B(x) + C(x) |] ==>
lcp@104
   114
       ?c1(x,y) : (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   115
> by (eresolve_tac [PlusE] 1);
lcp@104
   116
Level 2
lcp@104
   117
split(p,%x y. when(y,?c2(x,y),?d2(x,y)))
lcp@104
   118
: (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   119
 1. !!x y xa.
lcp@104
   120
       [| x : A; xa : B(x) |] ==>
lcp@104
   121
       ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   122
 2. !!x y ya.
lcp@104
   123
       [| x : A; ya : C(x) |] ==>
lcp@104
   124
       ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   125
> by (resolve_tac [PlusI_inl] 1);
lcp@104
   126
Level 3
lcp@104
   127
split(p,%x y. when(y,%xa. inl(?a3(x,y,xa)),?d2(x,y)))
lcp@104
   128
: (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   129
 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a3(x,y,xa) : SUM x:A. B(x)
lcp@104
   130
 2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type
lcp@104
   131
 3. !!x y ya.
lcp@104
   132
       [| x : A; ya : C(x) |] ==>
lcp@104
   133
       ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   134
> by (resolve_tac [SumI] 1);
lcp@104
   135
Level 4
lcp@104
   136
split(p,%x y. when(y,%xa. inl(<?a4(x,y,xa),?b4(x,y,xa)>),?d2(x,y)))
lcp@104
   137
: (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   138
 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a4(x,y,xa) : A
lcp@104
   139
 2. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(?a4(x,y,xa))
lcp@104
   140
 3. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type
lcp@104
   141
 4. !!x y ya.
lcp@104
   142
       [| x : A; ya : C(x) |] ==>
lcp@104
   143
       ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   144
> by (assume_tac 1);
lcp@104
   145
Level 5
lcp@104
   146
split(p,%x y. when(y,%xa. inl(<x,?b4(x,y,xa)>),?d2(x,y)))
lcp@104
   147
: (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   148
 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(x)
lcp@104
   149
 2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type
lcp@104
   150
 3. !!x y ya.
lcp@104
   151
       [| x : A; ya : C(x) |] ==>
lcp@104
   152
       ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   153
> by (assume_tac 1);
lcp@104
   154
Level 6
lcp@104
   155
split(p,%x y. when(y,%xa. inl(<x,xa>),?d2(x,y)))
lcp@104
   156
: (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   157
 1. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type
lcp@104
   158
 2. !!x y ya.
lcp@104
   159
       [| x : A; ya : C(x) |] ==>
lcp@104
   160
       ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   161
> by (typechk_tac prems);
lcp@104
   162
Level 7
lcp@104
   163
split(p,%x y. when(y,%xa. inl(<x,xa>),?d2(x,y)))
lcp@104
   164
: (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   165
 1. !!x y ya.
lcp@104
   166
       [| x : A; ya : C(x) |] ==>
lcp@104
   167
       ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   168
> by (pc_tac prems 1);
lcp@104
   169
Level 8
lcp@104
   170
split(p,%x y. when(y,%xa. inl(<x,xa>),%y. inr(<x,y>)))
lcp@104
   171
: (SUM x:A. B(x)) + (SUM x:A. C(x))
lcp@104
   172
No subgoals!
lcp@104
   173
lcp@104
   174
lcp@104
   175
lcp@104
   176
lcp@115
   177
> val prems = goal CTT.thy
lcp@104
   178
#     "[| A type; !!x. x:A ==> B(x) type; \
lcp@104
   179
# \               !!z. z: (SUM x:A. B(x)) ==> C(z) type |] \
lcp@104
   180
# \    ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \
lcp@104
   181
# \         --> (PROD x:A . PROD y:B(x) . C(<x,y>))";
lcp@104
   182
Level 0
lcp@104
   183
?a : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))
lcp@104
   184
 1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->
lcp@104
   185
         (PROD x:A. PROD y:B(x). C(<x,y>))
lcp@104
   186
> by (intr_tac prems);
lcp@104
   187
Level 1
lcp@104
   188
lam x xa xb. ?b7(x,xa,xb)
lcp@104
   189
: (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))
lcp@104
   190
 1. !!uu x y.
lcp@104
   191
       [| uu : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) |] ==>
lcp@104
   192
       ?b7(uu,x,y) : C(<x,y>)
lcp@104
   193
> by (eresolve_tac [ProdE] 1);
lcp@104
   194
Level 2
lcp@104
   195
lam x xa xb. x ` <xa,xb>
lcp@104
   196
: (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))
lcp@104
   197
 1. !!uu x y. [| x : A; y : B(x) |] ==> <x,y> : SUM x:A. B(x)
lcp@104
   198
> by (intr_tac prems);
lcp@104
   199
Level 3
lcp@104
   200
lam x xa xb. x ` <xa,xb>
lcp@104
   201
: (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))
lcp@104
   202
No subgoals!
lcp@104
   203
lcp@104
   204
lcp@104
   205
lcp@104
   206
lcp@115
   207
> val prems = goal CTT.thy
lcp@104
   208
#     "[| A type;  !!x. x:A ==> B(x) type;  \
lcp@104
   209
# \       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type  \
lcp@104
   210
# \    |] ==> ?a :    (PROD x:A. SUM y:B(x). C(x,y))    \
lcp@104
   211
# \               --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
lcp@104
   212
Level 0
lcp@104
   213
?a : (PROD x:A. SUM y:B(x). C(x,y)) -->
lcp@104
   214
     (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
lcp@104
   215
 1. ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->
lcp@104
   216
         (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
lcp@104
   217
> by (intr_tac prems);
lcp@104
   218
Level 1
lcp@104
   219
lam x. <lam xa. ?b7(x,xa),lam xa. ?b8(x,xa)>
lcp@104
   220
: (PROD x:A. SUM y:B(x). C(x,y)) -->
lcp@104
   221
  (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
lcp@104
   222
 1. !!uu x.
lcp@104
   223
       [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
lcp@104
   224
       ?b7(uu,x) : B(x)
lcp@104
   225
 2. !!uu x.
lcp@104
   226
       [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
lcp@104
   227
       ?b8(uu,x) : C(x,(lam x. ?b7(uu,x)) ` x)
lcp@104
   228
> by (eresolve_tac [ProdE RS SumE_fst] 1);
lcp@104
   229
Level 2
lcp@104
   230
lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
lcp@104
   231
: (PROD x:A. SUM y:B(x). C(x,y)) -->
lcp@104
   232
  (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
lcp@104
   233
 1. !!uu x. x : A ==> x : A
lcp@104
   234
 2. !!uu x.
lcp@104
   235
       [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
lcp@104
   236
       ?b8(uu,x) : C(x,(lam x. fst(uu ` x)) ` x)
lcp@104
   237
> by (assume_tac 1);
lcp@104
   238
Level 3
lcp@104
   239
lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
lcp@104
   240
: (PROD x:A. SUM y:B(x). C(x,y)) -->
lcp@104
   241
  (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
lcp@104
   242
 1. !!uu x.
lcp@104
   243
       [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
lcp@104
   244
       ?b8(uu,x) : C(x,(lam x. fst(uu ` x)) ` x)
lcp@104
   245
> by (resolve_tac [replace_type] 1);
lcp@104
   246
Level 4
lcp@104
   247
lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
lcp@104
   248
: (PROD x:A. SUM y:B(x). C(x,y)) -->
lcp@104
   249
  (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
lcp@104
   250
 1. !!uu x.
lcp@104
   251
       [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
lcp@104
   252
       C(x,(lam x. fst(uu ` x)) ` x) = ?A13(uu,x)
lcp@104
   253
 2. !!uu x.
lcp@104
   254
       [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
lcp@104
   255
       ?b8(uu,x) : ?A13(uu,x)
lcp@104
   256
> by (resolve_tac [subst_eqtyparg] 1);
lcp@104
   257
Level 5
lcp@104
   258
lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
lcp@104
   259
: (PROD x:A. SUM y:B(x). C(x,y)) -->
lcp@104
   260
  (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
lcp@104
   261
 1. !!uu x.
lcp@104
   262
       [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
lcp@104
   263
       (lam x. fst(uu ` x)) ` x = ?c14(uu,x) : ?A14(uu,x)
lcp@104
   264
 2. !!uu x z.
lcp@104
   265
       [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;
lcp@104
   266
          z : ?A14(uu,x) |] ==>
lcp@104
   267
       C(x,z) type
lcp@104
   268
 3. !!uu x.
lcp@104
   269
       [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
lcp@104
   270
       ?b8(uu,x) : C(x,?c14(uu,x))
lcp@104
   271
> by (resolve_tac [ProdC] 1);
lcp@104
   272
Level 6
lcp@104
   273
lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
lcp@104
   274
: (PROD x:A. SUM y:B(x). C(x,y)) -->
lcp@104
   275
  (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
lcp@104
   276
 1. !!uu x.
lcp@104
   277
       [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> x : ?A15(uu,x)
lcp@104
   278
 2. !!uu x xa.
lcp@104
   279
       [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;
lcp@104
   280
          xa : ?A15(uu,x) |] ==>
lcp@104
   281
       fst(uu ` xa) : ?B15(uu,x,xa)
lcp@104
   282
 3. !!uu x z.
lcp@104
   283
       [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;
lcp@104
   284
          z : ?B15(uu,x,x) |] ==>
lcp@104
   285
       C(x,z) type
lcp@104
   286
 4. !!uu x.
lcp@104
   287
       [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
lcp@104
   288
       ?b8(uu,x) : C(x,fst(uu ` x))
lcp@104
   289
> by (typechk_tac (SumE_fst::prems));
lcp@104
   290
Level 7
lcp@104
   291
lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
lcp@104
   292
: (PROD x:A. SUM y:B(x). C(x,y)) -->
lcp@104
   293
  (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
lcp@104
   294
 1. !!uu x.
lcp@104
   295
       [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
lcp@104
   296
       ?b8(uu,x) : C(x,fst(uu ` x))
lcp@104
   297
> by (eresolve_tac [ProdE RS SumE_snd] 1);
lcp@104
   298
Level 8
lcp@104
   299
lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>
lcp@104
   300
: (PROD x:A. SUM y:B(x). C(x,y)) -->
lcp@104
   301
  (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
lcp@104
   302
 1. !!uu x. x : A ==> x : A
lcp@104
   303
 2. !!uu x. x : A ==> B(x) type
lcp@104
   304
 3. !!uu x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type
lcp@104
   305
> by (typechk_tac prems);
lcp@104
   306
Level 9
lcp@104
   307
lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>
lcp@104
   308
: (PROD x:A. SUM y:B(x). C(x,y)) -->
lcp@104
   309
  (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
lcp@104
   310
No subgoals!