|
lcp@104
|
1 |
(**** CTT examples -- process using Doc/tout CTT-eg.txt ****)
|
|
lcp@104
|
2 |
|
|
lcp@104
|
3 |
Pretty.setmargin 72; (*existing macros just allow this margin*)
|
|
lcp@104
|
4 |
print_depth 0;
|
|
lcp@104
|
5 |
|
|
lcp@104
|
6 |
|
|
lcp@104
|
7 |
(*** Type inference, from CTT/ex/typechk.ML ***)
|
|
lcp@104
|
8 |
|
|
lcp@115
|
9 |
goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A";
|
|
lcp@104
|
10 |
by (resolve_tac [ProdI] 1);
|
|
lcp@104
|
11 |
by (eresolve_tac [NE] 2);
|
|
lcp@104
|
12 |
by (resolve_tac [NI0] 2);
|
|
lcp@104
|
13 |
by (assume_tac 2);
|
|
lcp@104
|
14 |
by (resolve_tac [NF] 1);
|
|
lcp@104
|
15 |
|
|
lcp@104
|
16 |
|
|
lcp@104
|
17 |
|
|
lcp@104
|
18 |
(*** Logical reasoning, from CTT/ex/elim.ML ***)
|
|
lcp@104
|
19 |
|
|
lcp@115
|
20 |
val prems = goal CTT.thy
|
|
lcp@104
|
21 |
"[| A type; \
|
|
lcp@104
|
22 |
\ !!x. x:A ==> B(x) type; \
|
|
lcp@104
|
23 |
\ !!x. x:A ==> C(x) type; \
|
|
lcp@104
|
24 |
\ p: SUM x:A. B(x) + C(x) \
|
|
lcp@104
|
25 |
\ |] ==> ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))";
|
|
lcp@104
|
26 |
by (resolve_tac (prems RL [SumE]) 1);
|
|
lcp@104
|
27 |
by (eresolve_tac [PlusE] 1);
|
|
lcp@104
|
28 |
by (resolve_tac [PlusI_inl] 1);
|
|
lcp@104
|
29 |
by (resolve_tac [SumI] 1);
|
|
lcp@104
|
30 |
by (assume_tac 1);
|
|
lcp@104
|
31 |
by (assume_tac 1);
|
|
lcp@104
|
32 |
by (typechk_tac prems);
|
|
lcp@104
|
33 |
by (pc_tac prems 1);
|
|
lcp@104
|
34 |
|
|
lcp@104
|
35 |
|
|
lcp@104
|
36 |
(*** Currying, from CTT/ex/elim.ML ***)
|
|
lcp@104
|
37 |
|
|
lcp@115
|
38 |
val prems = goal CTT.thy
|
|
lcp@359
|
39 |
"[| A type; !!x. x:A ==> B(x) type; \
|
|
lcp@359
|
40 |
\ !!z. z: (SUM x:A. B(x)) ==> C(z) type \
|
|
lcp@359
|
41 |
\ |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \
|
|
lcp@359
|
42 |
\ (PROD x:A . PROD y:B(x) . C(<x,y>))";
|
|
lcp@104
|
43 |
by (intr_tac prems);
|
|
lcp@104
|
44 |
by (eresolve_tac [ProdE] 1);
|
|
lcp@104
|
45 |
by (intr_tac prems);
|
|
lcp@104
|
46 |
|
|
lcp@104
|
47 |
|
|
lcp@104
|
48 |
(*** Axiom of Choice ***)
|
|
lcp@104
|
49 |
|
|
lcp@115
|
50 |
val prems = goal CTT.thy
|
|
lcp@104
|
51 |
"[| A type; !!x. x:A ==> B(x) type; \
|
|
lcp@104
|
52 |
\ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \
|
|
lcp@359
|
53 |
\ |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \
|
|
lcp@359
|
54 |
\ (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
|
|
lcp@104
|
55 |
by (intr_tac prems);
|
|
lcp@104
|
56 |
by (eresolve_tac [ProdE RS SumE_fst] 1);
|
|
lcp@104
|
57 |
by (assume_tac 1);
|
|
lcp@104
|
58 |
by (resolve_tac [replace_type] 1);
|
|
lcp@104
|
59 |
by (resolve_tac [subst_eqtyparg] 1);
|
|
lcp@104
|
60 |
by (resolve_tac [ProdC] 1);
|
|
lcp@104
|
61 |
by (typechk_tac (SumE_fst::prems));
|
|
lcp@104
|
62 |
by (eresolve_tac [ProdE RS SumE_snd] 1);
|
|
lcp@104
|
63 |
by (typechk_tac prems);
|
|
lcp@104
|
64 |
|
|
lcp@104
|
65 |
|
|
lcp@104
|
66 |
|
|
lcp@104
|
67 |
|
|
lcp@115
|
68 |
> goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A";
|
|
lcp@104
|
69 |
Level 0
|
|
lcp@104
|
70 |
lam n. rec(n,0,%x y. x) : ?A
|
|
lcp@104
|
71 |
1. lam n. rec(n,0,%x y. x) : ?A
|
|
lcp@104
|
72 |
> by (resolve_tac [ProdI] 1);
|
|
lcp@104
|
73 |
Level 1
|
|
lcp@104
|
74 |
lam n. rec(n,0,%x y. x) : PROD x:?A1. ?B1(x)
|
|
lcp@104
|
75 |
1. ?A1 type
|
|
lcp@104
|
76 |
2. !!n. n : ?A1 ==> rec(n,0,%x y. x) : ?B1(n)
|
|
lcp@104
|
77 |
> by (eresolve_tac [NE] 2);
|
|
lcp@104
|
78 |
Level 2
|
|
lcp@104
|
79 |
lam n. rec(n,0,%x y. x) : PROD x:N. ?C2(x,x)
|
|
lcp@104
|
80 |
1. N type
|
|
lcp@104
|
81 |
2. !!n. 0 : ?C2(n,0)
|
|
lcp@104
|
82 |
3. !!n x y. [| x : N; y : ?C2(n,x) |] ==> x : ?C2(n,succ(x))
|
|
lcp@104
|
83 |
> by (resolve_tac [NI0] 2);
|
|
lcp@104
|
84 |
Level 3
|
|
lcp@104
|
85 |
lam n. rec(n,0,%x y. x) : N --> N
|
|
lcp@104
|
86 |
1. N type
|
|
lcp@104
|
87 |
2. !!n x y. [| x : N; y : N |] ==> x : N
|
|
lcp@104
|
88 |
> by (assume_tac 2);
|
|
lcp@104
|
89 |
Level 4
|
|
lcp@104
|
90 |
lam n. rec(n,0,%x y. x) : N --> N
|
|
lcp@104
|
91 |
1. N type
|
|
lcp@104
|
92 |
> by (resolve_tac [NF] 1);
|
|
lcp@104
|
93 |
Level 5
|
|
lcp@104
|
94 |
lam n. rec(n,0,%x y. x) : N --> N
|
|
lcp@104
|
95 |
No subgoals!
|
|
lcp@104
|
96 |
|
|
lcp@104
|
97 |
|
|
lcp@104
|
98 |
|
|
lcp@104
|
99 |
|
|
lcp@115
|
100 |
> val prems = goal CTT.thy
|
|
lcp@104
|
101 |
# "[| A type; \
|
|
lcp@104
|
102 |
# \ !!x. x:A ==> B(x) type; \
|
|
lcp@104
|
103 |
# \ !!x. x:A ==> C(x) type; \
|
|
lcp@104
|
104 |
# \ p: SUM x:A. B(x) + C(x) \
|
|
lcp@104
|
105 |
# \ |] ==> ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))";
|
|
lcp@104
|
106 |
Level 0
|
|
lcp@104
|
107 |
?a : (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
108 |
1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
109 |
> by (resolve_tac (prems RL [SumE]) 1);
|
|
lcp@104
|
110 |
Level 1
|
|
lcp@104
|
111 |
split(p,?c1) : (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
112 |
1. !!x y.
|
|
lcp@104
|
113 |
[| x : A; y : B(x) + C(x) |] ==>
|
|
lcp@104
|
114 |
?c1(x,y) : (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
115 |
> by (eresolve_tac [PlusE] 1);
|
|
lcp@104
|
116 |
Level 2
|
|
lcp@104
|
117 |
split(p,%x y. when(y,?c2(x,y),?d2(x,y)))
|
|
lcp@104
|
118 |
: (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
119 |
1. !!x y xa.
|
|
lcp@104
|
120 |
[| x : A; xa : B(x) |] ==>
|
|
lcp@104
|
121 |
?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
122 |
2. !!x y ya.
|
|
lcp@104
|
123 |
[| x : A; ya : C(x) |] ==>
|
|
lcp@104
|
124 |
?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
125 |
> by (resolve_tac [PlusI_inl] 1);
|
|
lcp@104
|
126 |
Level 3
|
|
lcp@104
|
127 |
split(p,%x y. when(y,%xa. inl(?a3(x,y,xa)),?d2(x,y)))
|
|
lcp@104
|
128 |
: (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
129 |
1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a3(x,y,xa) : SUM x:A. B(x)
|
|
lcp@104
|
130 |
2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type
|
|
lcp@104
|
131 |
3. !!x y ya.
|
|
lcp@104
|
132 |
[| x : A; ya : C(x) |] ==>
|
|
lcp@104
|
133 |
?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
134 |
> by (resolve_tac [SumI] 1);
|
|
lcp@104
|
135 |
Level 4
|
|
lcp@104
|
136 |
split(p,%x y. when(y,%xa. inl(<?a4(x,y,xa),?b4(x,y,xa)>),?d2(x,y)))
|
|
lcp@104
|
137 |
: (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
138 |
1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a4(x,y,xa) : A
|
|
lcp@104
|
139 |
2. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(?a4(x,y,xa))
|
|
lcp@104
|
140 |
3. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type
|
|
lcp@104
|
141 |
4. !!x y ya.
|
|
lcp@104
|
142 |
[| x : A; ya : C(x) |] ==>
|
|
lcp@104
|
143 |
?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
144 |
> by (assume_tac 1);
|
|
lcp@104
|
145 |
Level 5
|
|
lcp@104
|
146 |
split(p,%x y. when(y,%xa. inl(<x,?b4(x,y,xa)>),?d2(x,y)))
|
|
lcp@104
|
147 |
: (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
148 |
1. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(x)
|
|
lcp@104
|
149 |
2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type
|
|
lcp@104
|
150 |
3. !!x y ya.
|
|
lcp@104
|
151 |
[| x : A; ya : C(x) |] ==>
|
|
lcp@104
|
152 |
?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
153 |
> by (assume_tac 1);
|
|
lcp@104
|
154 |
Level 6
|
|
lcp@104
|
155 |
split(p,%x y. when(y,%xa. inl(<x,xa>),?d2(x,y)))
|
|
lcp@104
|
156 |
: (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
157 |
1. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type
|
|
lcp@104
|
158 |
2. !!x y ya.
|
|
lcp@104
|
159 |
[| x : A; ya : C(x) |] ==>
|
|
lcp@104
|
160 |
?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
161 |
> by (typechk_tac prems);
|
|
lcp@104
|
162 |
Level 7
|
|
lcp@104
|
163 |
split(p,%x y. when(y,%xa. inl(<x,xa>),?d2(x,y)))
|
|
lcp@104
|
164 |
: (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
165 |
1. !!x y ya.
|
|
lcp@104
|
166 |
[| x : A; ya : C(x) |] ==>
|
|
lcp@104
|
167 |
?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
168 |
> by (pc_tac prems 1);
|
|
lcp@104
|
169 |
Level 8
|
|
lcp@104
|
170 |
split(p,%x y. when(y,%xa. inl(<x,xa>),%y. inr(<x,y>)))
|
|
lcp@104
|
171 |
: (SUM x:A. B(x)) + (SUM x:A. C(x))
|
|
lcp@104
|
172 |
No subgoals!
|
|
lcp@104
|
173 |
|
|
lcp@104
|
174 |
|
|
lcp@104
|
175 |
|
|
lcp@104
|
176 |
|
|
lcp@115
|
177 |
> val prems = goal CTT.thy
|
|
lcp@104
|
178 |
# "[| A type; !!x. x:A ==> B(x) type; \
|
|
lcp@104
|
179 |
# \ !!z. z: (SUM x:A. B(x)) ==> C(z) type |] \
|
|
lcp@104
|
180 |
# \ ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \
|
|
lcp@104
|
181 |
# \ --> (PROD x:A . PROD y:B(x) . C(<x,y>))";
|
|
lcp@104
|
182 |
Level 0
|
|
lcp@104
|
183 |
?a : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))
|
|
lcp@104
|
184 |
1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->
|
|
lcp@104
|
185 |
(PROD x:A. PROD y:B(x). C(<x,y>))
|
|
lcp@104
|
186 |
> by (intr_tac prems);
|
|
lcp@104
|
187 |
Level 1
|
|
lcp@104
|
188 |
lam x xa xb. ?b7(x,xa,xb)
|
|
lcp@104
|
189 |
: (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))
|
|
lcp@104
|
190 |
1. !!uu x y.
|
|
lcp@104
|
191 |
[| uu : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) |] ==>
|
|
lcp@104
|
192 |
?b7(uu,x,y) : C(<x,y>)
|
|
lcp@104
|
193 |
> by (eresolve_tac [ProdE] 1);
|
|
lcp@104
|
194 |
Level 2
|
|
lcp@104
|
195 |
lam x xa xb. x ` <xa,xb>
|
|
lcp@104
|
196 |
: (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))
|
|
lcp@104
|
197 |
1. !!uu x y. [| x : A; y : B(x) |] ==> <x,y> : SUM x:A. B(x)
|
|
lcp@104
|
198 |
> by (intr_tac prems);
|
|
lcp@104
|
199 |
Level 3
|
|
lcp@104
|
200 |
lam x xa xb. x ` <xa,xb>
|
|
lcp@104
|
201 |
: (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))
|
|
lcp@104
|
202 |
No subgoals!
|
|
lcp@104
|
203 |
|
|
lcp@104
|
204 |
|
|
lcp@104
|
205 |
|
|
lcp@104
|
206 |
|
|
lcp@115
|
207 |
> val prems = goal CTT.thy
|
|
lcp@104
|
208 |
# "[| A type; !!x. x:A ==> B(x) type; \
|
|
lcp@104
|
209 |
# \ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \
|
|
lcp@104
|
210 |
# \ |] ==> ?a : (PROD x:A. SUM y:B(x). C(x,y)) \
|
|
lcp@104
|
211 |
# \ --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
|
|
lcp@104
|
212 |
Level 0
|
|
lcp@104
|
213 |
?a : (PROD x:A. SUM y:B(x). C(x,y)) -->
|
|
lcp@104
|
214 |
(SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
|
|
lcp@104
|
215 |
1. ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->
|
|
lcp@104
|
216 |
(SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
|
|
lcp@104
|
217 |
> by (intr_tac prems);
|
|
lcp@104
|
218 |
Level 1
|
|
lcp@104
|
219 |
lam x. <lam xa. ?b7(x,xa),lam xa. ?b8(x,xa)>
|
|
lcp@104
|
220 |
: (PROD x:A. SUM y:B(x). C(x,y)) -->
|
|
lcp@104
|
221 |
(SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
|
|
lcp@104
|
222 |
1. !!uu x.
|
|
lcp@104
|
223 |
[| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
|
|
lcp@104
|
224 |
?b7(uu,x) : B(x)
|
|
lcp@104
|
225 |
2. !!uu x.
|
|
lcp@104
|
226 |
[| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
|
|
lcp@104
|
227 |
?b8(uu,x) : C(x,(lam x. ?b7(uu,x)) ` x)
|
|
lcp@104
|
228 |
> by (eresolve_tac [ProdE RS SumE_fst] 1);
|
|
lcp@104
|
229 |
Level 2
|
|
lcp@104
|
230 |
lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
|
|
lcp@104
|
231 |
: (PROD x:A. SUM y:B(x). C(x,y)) -->
|
|
lcp@104
|
232 |
(SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
|
|
lcp@104
|
233 |
1. !!uu x. x : A ==> x : A
|
|
lcp@104
|
234 |
2. !!uu x.
|
|
lcp@104
|
235 |
[| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
|
|
lcp@104
|
236 |
?b8(uu,x) : C(x,(lam x. fst(uu ` x)) ` x)
|
|
lcp@104
|
237 |
> by (assume_tac 1);
|
|
lcp@104
|
238 |
Level 3
|
|
lcp@104
|
239 |
lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
|
|
lcp@104
|
240 |
: (PROD x:A. SUM y:B(x). C(x,y)) -->
|
|
lcp@104
|
241 |
(SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
|
|
lcp@104
|
242 |
1. !!uu x.
|
|
lcp@104
|
243 |
[| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
|
|
lcp@104
|
244 |
?b8(uu,x) : C(x,(lam x. fst(uu ` x)) ` x)
|
|
lcp@104
|
245 |
> by (resolve_tac [replace_type] 1);
|
|
lcp@104
|
246 |
Level 4
|
|
lcp@104
|
247 |
lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
|
|
lcp@104
|
248 |
: (PROD x:A. SUM y:B(x). C(x,y)) -->
|
|
lcp@104
|
249 |
(SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
|
|
lcp@104
|
250 |
1. !!uu x.
|
|
lcp@104
|
251 |
[| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
|
|
lcp@104
|
252 |
C(x,(lam x. fst(uu ` x)) ` x) = ?A13(uu,x)
|
|
lcp@104
|
253 |
2. !!uu x.
|
|
lcp@104
|
254 |
[| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
|
|
lcp@104
|
255 |
?b8(uu,x) : ?A13(uu,x)
|
|
lcp@104
|
256 |
> by (resolve_tac [subst_eqtyparg] 1);
|
|
lcp@104
|
257 |
Level 5
|
|
lcp@104
|
258 |
lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
|
|
lcp@104
|
259 |
: (PROD x:A. SUM y:B(x). C(x,y)) -->
|
|
lcp@104
|
260 |
(SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
|
|
lcp@104
|
261 |
1. !!uu x.
|
|
lcp@104
|
262 |
[| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
|
|
lcp@104
|
263 |
(lam x. fst(uu ` x)) ` x = ?c14(uu,x) : ?A14(uu,x)
|
|
lcp@104
|
264 |
2. !!uu x z.
|
|
lcp@104
|
265 |
[| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;
|
|
lcp@104
|
266 |
z : ?A14(uu,x) |] ==>
|
|
lcp@104
|
267 |
C(x,z) type
|
|
lcp@104
|
268 |
3. !!uu x.
|
|
lcp@104
|
269 |
[| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
|
|
lcp@104
|
270 |
?b8(uu,x) : C(x,?c14(uu,x))
|
|
lcp@104
|
271 |
> by (resolve_tac [ProdC] 1);
|
|
lcp@104
|
272 |
Level 6
|
|
lcp@104
|
273 |
lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
|
|
lcp@104
|
274 |
: (PROD x:A. SUM y:B(x). C(x,y)) -->
|
|
lcp@104
|
275 |
(SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
|
|
lcp@104
|
276 |
1. !!uu x.
|
|
lcp@104
|
277 |
[| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> x : ?A15(uu,x)
|
|
lcp@104
|
278 |
2. !!uu x xa.
|
|
lcp@104
|
279 |
[| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;
|
|
lcp@104
|
280 |
xa : ?A15(uu,x) |] ==>
|
|
lcp@104
|
281 |
fst(uu ` xa) : ?B15(uu,x,xa)
|
|
lcp@104
|
282 |
3. !!uu x z.
|
|
lcp@104
|
283 |
[| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;
|
|
lcp@104
|
284 |
z : ?B15(uu,x,x) |] ==>
|
|
lcp@104
|
285 |
C(x,z) type
|
|
lcp@104
|
286 |
4. !!uu x.
|
|
lcp@104
|
287 |
[| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
|
|
lcp@104
|
288 |
?b8(uu,x) : C(x,fst(uu ` x))
|
|
lcp@104
|
289 |
> by (typechk_tac (SumE_fst::prems));
|
|
lcp@104
|
290 |
Level 7
|
|
lcp@104
|
291 |
lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
|
|
lcp@104
|
292 |
: (PROD x:A. SUM y:B(x). C(x,y)) -->
|
|
lcp@104
|
293 |
(SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
|
|
lcp@104
|
294 |
1. !!uu x.
|
|
lcp@104
|
295 |
[| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
|
|
lcp@104
|
296 |
?b8(uu,x) : C(x,fst(uu ` x))
|
|
lcp@104
|
297 |
> by (eresolve_tac [ProdE RS SumE_snd] 1);
|
|
lcp@104
|
298 |
Level 8
|
|
lcp@104
|
299 |
lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>
|
|
lcp@104
|
300 |
: (PROD x:A. SUM y:B(x). C(x,y)) -->
|
|
lcp@104
|
301 |
(SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
|
|
lcp@104
|
302 |
1. !!uu x. x : A ==> x : A
|
|
lcp@104
|
303 |
2. !!uu x. x : A ==> B(x) type
|
|
lcp@104
|
304 |
3. !!uu x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type
|
|
lcp@104
|
305 |
> by (typechk_tac prems);
|
|
lcp@104
|
306 |
Level 9
|
|
lcp@104
|
307 |
lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>
|
|
lcp@104
|
308 |
: (PROD x:A. SUM y:B(x). C(x,y)) -->
|
|
lcp@104
|
309 |
(SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
|
|
lcp@104
|
310 |
No subgoals!
|