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.
     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 CTT.thy "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 CTT.thy
    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 CTT.thy
    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 CTT.thy   
    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 > goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A";
    69 Level 0
    70 lam n. rec(n,0,%x y. x) : ?A
    71  1. lam n. rec(n,0,%x y. x) : ?A
    72 > by (resolve_tac [ProdI] 1);
    73 Level 1
    74 lam n. rec(n,0,%x y. x) : PROD x:?A1. ?B1(x)
    75  1. ?A1 type
    76  2. !!n. n : ?A1 ==> rec(n,0,%x y. x) : ?B1(n)
    77 > by (eresolve_tac [NE] 2);
    78 Level 2
    79 lam n. rec(n,0,%x y. x) : PROD x:N. ?C2(x,x)
    80  1. N type
    81  2. !!n. 0 : ?C2(n,0)
    82  3. !!n x y. [| x : N; y : ?C2(n,x) |] ==> x : ?C2(n,succ(x))
    83 > by (resolve_tac [NI0] 2);
    84 Level 3
    85 lam n. rec(n,0,%x y. x) : N --> N
    86  1. N type
    87  2. !!n x y. [| x : N; y : N |] ==> x : N
    88 > by (assume_tac 2);
    89 Level 4
    90 lam n. rec(n,0,%x y. x) : N --> N
    91  1. N type
    92 > by (resolve_tac [NF] 1);
    93 Level 5
    94 lam n. rec(n,0,%x y. x) : N --> N
    95 No subgoals!
    96 
    97 
    98 
    99 
   100 > val prems = goal CTT.thy
   101 #     "[| A type;  \
   102 # \       !!x. x:A ==> B(x) type;       \
   103 # \       !!x. x:A ==> C(x) type;       \
   104 # \       p: SUM x:A. B(x) + C(x)       \
   105 # \    |] ==>  ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))";
   106 Level 0
   107 ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))
   108  1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))
   109 > by (resolve_tac (prems RL [SumE]) 1);
   110 Level 1
   111 split(p,?c1) : (SUM x:A. B(x)) + (SUM x:A. C(x))
   112  1. !!x y.
   113        [| x : A; y : B(x) + C(x) |] ==>
   114        ?c1(x,y) : (SUM x:A. B(x)) + (SUM x:A. C(x))
   115 > by (eresolve_tac [PlusE] 1);
   116 Level 2
   117 split(p,%x y. when(y,?c2(x,y),?d2(x,y)))
   118 : (SUM x:A. B(x)) + (SUM x:A. C(x))
   119  1. !!x y xa.
   120        [| x : A; xa : B(x) |] ==>
   121        ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))
   122  2. !!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 (resolve_tac [PlusI_inl] 1);
   126 Level 3
   127 split(p,%x y. when(y,%xa. inl(?a3(x,y,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) |] ==> ?a3(x,y,xa) : SUM x:A. B(x)
   130  2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type
   131  3. !!x y ya.
   132        [| x : A; ya : C(x) |] ==>
   133        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
   134 > by (resolve_tac [SumI] 1);
   135 Level 4
   136 split(p,%x y. when(y,%xa. inl(<?a4(x,y,xa),?b4(x,y,xa)>),?d2(x,y)))
   137 : (SUM x:A. B(x)) + (SUM x:A. C(x))
   138  1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a4(x,y,xa) : A
   139  2. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(?a4(x,y,xa))
   140  3. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type
   141  4. !!x y ya.
   142        [| x : A; ya : C(x) |] ==>
   143        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
   144 > by (assume_tac 1);
   145 Level 5
   146 split(p,%x y. when(y,%xa. inl(<x,?b4(x,y,xa)>),?d2(x,y)))
   147 : (SUM x:A. B(x)) + (SUM x:A. C(x))
   148  1. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(x)
   149  2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type
   150  3. !!x y ya.
   151        [| x : A; ya : C(x) |] ==>
   152        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
   153 > by (assume_tac 1);
   154 Level 6
   155 split(p,%x y. when(y,%xa. inl(<x,xa>),?d2(x,y)))
   156 : (SUM x:A. B(x)) + (SUM x:A. C(x))
   157  1. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type
   158  2. !!x y ya.
   159        [| x : A; ya : C(x) |] ==>
   160        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
   161 > by (typechk_tac prems);
   162 Level 7
   163 split(p,%x y. when(y,%xa. inl(<x,xa>),?d2(x,y)))
   164 : (SUM x:A. B(x)) + (SUM x:A. C(x))
   165  1. !!x y ya.
   166        [| x : A; ya : C(x) |] ==>
   167        ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
   168 > by (pc_tac prems 1);
   169 Level 8
   170 split(p,%x y. when(y,%xa. inl(<x,xa>),%y. inr(<x,y>)))
   171 : (SUM x:A. B(x)) + (SUM x:A. C(x))
   172 No subgoals!
   173 
   174 
   175 
   176 
   177 > val prems = goal CTT.thy
   178 #     "[| A type; !!x. x:A ==> B(x) type; \
   179 # \               !!z. z: (SUM x:A. B(x)) ==> C(z) type |] \
   180 # \    ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \
   181 # \         --> (PROD x:A . PROD y:B(x) . C(<x,y>))";
   182 Level 0
   183 ?a : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))
   184  1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->
   185          (PROD x:A. PROD y:B(x). C(<x,y>))
   186 > by (intr_tac prems);
   187 Level 1
   188 lam x xa xb. ?b7(x,xa,xb)
   189 : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))
   190  1. !!uu x y.
   191        [| uu : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) |] ==>
   192        ?b7(uu,x,y) : C(<x,y>)
   193 > by (eresolve_tac [ProdE] 1);
   194 Level 2
   195 lam x xa xb. x ` <xa,xb>
   196 : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))
   197  1. !!uu x y. [| x : A; y : B(x) |] ==> <x,y> : SUM x:A. B(x)
   198 > by (intr_tac prems);
   199 Level 3
   200 lam x xa xb. x ` <xa,xb>
   201 : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))
   202 No subgoals!
   203 
   204 
   205 
   206 
   207 > val prems = goal CTT.thy
   208 #     "[| A type;  !!x. x:A ==> B(x) type;  \
   209 # \       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type  \
   210 # \    |] ==> ?a :    (PROD x:A. SUM y:B(x). C(x,y))    \
   211 # \               --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
   212 Level 0
   213 ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->
   214      (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
   215  1. ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->
   216          (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
   217 > by (intr_tac prems);
   218 Level 1
   219 lam x. <lam xa. ?b7(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        ?b7(uu,x) : B(x)
   225  2. !!uu x.
   226        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
   227        ?b8(uu,x) : C(x,(lam x. ?b7(uu,x)) ` x)
   228 > by (eresolve_tac [ProdE RS SumE_fst] 1);
   229 Level 2
   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. x : A ==> x : A
   234  2. !!uu x.
   235        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
   236        ?b8(uu,x) : C(x,(lam x. fst(uu ` x)) ` x)
   237 > by (assume_tac 1);
   238 Level 3
   239 lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
   240 : (PROD x:A. SUM y:B(x). C(x,y)) -->
   241   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
   242  1. !!uu x.
   243        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
   244        ?b8(uu,x) : C(x,(lam x. fst(uu ` x)) ` x)
   245 > by (resolve_tac [replace_type] 1);
   246 Level 4
   247 lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
   248 : (PROD x:A. SUM y:B(x). C(x,y)) -->
   249   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
   250  1. !!uu x.
   251        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
   252        C(x,(lam x. fst(uu ` x)) ` x) = ?A13(uu,x)
   253  2. !!uu x.
   254        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
   255        ?b8(uu,x) : ?A13(uu,x)
   256 > by (resolve_tac [subst_eqtyparg] 1);
   257 Level 5
   258 lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
   259 : (PROD x:A. SUM y:B(x). C(x,y)) -->
   260   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
   261  1. !!uu x.
   262        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
   263        (lam x. fst(uu ` x)) ` x = ?c14(uu,x) : ?A14(uu,x)
   264  2. !!uu x z.
   265        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;
   266           z : ?A14(uu,x) |] ==>
   267        C(x,z) type
   268  3. !!uu x.
   269        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
   270        ?b8(uu,x) : C(x,?c14(uu,x))
   271 > by (resolve_tac [ProdC] 1);
   272 Level 6
   273 lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
   274 : (PROD x:A. SUM y:B(x). C(x,y)) -->
   275   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
   276  1. !!uu x.
   277        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> x : ?A15(uu,x)
   278  2. !!uu x xa.
   279        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;
   280           xa : ?A15(uu,x) |] ==>
   281        fst(uu ` xa) : ?B15(uu,x,xa)
   282  3. !!uu x z.
   283        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;
   284           z : ?B15(uu,x,x) |] ==>
   285        C(x,z) type
   286  4. !!uu x.
   287        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
   288        ?b8(uu,x) : C(x,fst(uu ` x))
   289 > by (typechk_tac (SumE_fst::prems));
   290 Level 7
   291 lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
   292 : (PROD x:A. SUM y:B(x). C(x,y)) -->
   293   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
   294  1. !!uu x.
   295        [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
   296        ?b8(uu,x) : C(x,fst(uu ` x))
   297 > by (eresolve_tac [ProdE RS SumE_snd] 1);
   298 Level 8
   299 lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>
   300 : (PROD x:A. SUM y:B(x). C(x,y)) -->
   301   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
   302  1. !!uu x. x : A ==> x : A
   303  2. !!uu x. x : A ==> B(x) type
   304  3. !!uu x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type
   305 > by (typechk_tac prems);
   306 Level 9
   307 lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>
   308 : (PROD x:A. SUM y:B(x). C(x,y)) -->
   309   (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
   310 No subgoals!