104

1 
(**** CTT examples  process using Doc/tout CTTeg.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 

5151

9 
Goal "lam n. rec(n, 0, %x y. x) : ?A";

104

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 

5151

20 
val prems = Goal

104

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 

5151

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)). \

359

42 
\ (PROD x:A . PROD y:B(x) . C(<x,y>))";

104

43 
by (intr_tac prems);


44 
by (eresolve_tac [ProdE] 1);


45 
by (intr_tac prems);


46 


47 


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


49 

5151

50 
val prems = Goal

104

51 
"[ A type; !!x. x:A ==> B(x) type; \


52 
\ !!x y.[ x:A; y:B(x) ] ==> C(x,y) type \

359

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

104

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 

5151

68 


69 
STOP_HERE;

104

70 


71 

5151

72 
> val prems = Goal

104

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 

5151

149 
> val prems = Goal

104

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 

5151

179 
> val prems = Goal

104

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!
