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