wneuper/isa: doc-src/Logics/CTT-eg.txt@20e3616b2d9c

     1 (**** CTT examples -- process using Doc/tout CTT-eg.txt  ****)

     3 Pretty.setmargin 72;  (*existing macros just allow this margin*)

     4 print_depth 0;

     7 (*** Type inference, from CTT/ex/typechk.ML ***)

     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);

    18 (*** Logical reasoning, from CTT/ex/elim.ML ***)

    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);

    36 (*** Currying, from CTT/ex/elim.ML ***)

    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);

    48 (*** Axiom of Choice ***)

    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);

    69 STOP_HERE;

    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!

   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!

   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!

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 5151	1e944fe5ce96
permissions	-rw-r--r--