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 

115

9 
goal CTT.thy "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 

115

20 
val prems = goal CTT.thy

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 

115

38 
val prems = goal CTT.thy

359

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

104

43 
by (intr_tac prems);


44 
by (eresolve_tac [ProdE] 1);


45 
by (intr_tac prems);


46 


47 


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


49 

115

50 
val prems = goal CTT.thy

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 

115

68 
> goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A";

104

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 

115

100 
> val prems = goal CTT.thy

104

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 

115

177 
> val prems = goal CTT.thy

104

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 

115

207 
> val prems = goal CTT.thy

104

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!
