doc-src/Logics/CTT-eg.txt
author paulson
Thu Jul 16 11:50:01 1998 +0200 (1998-07-16)
changeset 5151 1e944fe5ce96
parent 359 b5a2e9503a7a
permissions -rw-r--r--
Got rid of obsolete "goal" commands.
Also inserted spaces after all periods
     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!