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