111 NI_succ "a : N ==> succ(a) : N" |
111 NI_succ "a : N ==> succ(a) : N" |
112 NI_succL "a = b : N ==> succ(a) = succ(b) : N" |
112 NI_succL "a = b : N ==> succ(a) = succ(b) : N" |
113 |
113 |
114 NE |
114 NE |
115 "[| p: N; a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] |
115 "[| p: N; a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] |
116 ==> rec(p, a, %u v.b(u,v)) : C(p)" |
116 ==> rec(p, a, %u v. b(u,v)) : C(p)" |
117 |
117 |
118 NEL |
118 NEL |
119 "[| p = q : N; a = c : C(0); |
119 "[| p = q : N; a = c : C(0); |
120 !!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u)) |] |
120 !!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u)) |] |
121 ==> rec(p, a, %u v.b(u,v)) = rec(q,c,d) : C(p)" |
121 ==> rec(p, a, %u v. b(u,v)) = rec(q,c,d) : C(p)" |
122 |
122 |
123 NC0 |
123 NC0 |
124 "[| a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] |
124 "[| a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] |
125 ==> rec(0, a, %u v.b(u,v)) = a : C(0)" |
125 ==> rec(0, a, %u v. b(u,v)) = a : C(0)" |
126 |
126 |
127 NC_succ |
127 NC_succ |
128 "[| p: N; a: C(0); |
128 "[| p: N; a: C(0); |
129 !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==> |
129 !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==> |
130 rec(succ(p), a, %u v.b(u,v)) = b(p, rec(p, a, %u v.b(u,v))) : C(succ(p))" |
130 rec(succ(p), a, %u v. b(u,v)) = b(p, rec(p, a, %u v. b(u,v))) : C(succ(p))" |
131 |
131 |
132 (*The fourth Peano axiom. See page 91 of Martin-Lof's book*) |
132 (*The fourth Peano axiom. See page 91 of Martin-Lof's book*) |
133 zero_ne_succ |
133 zero_ne_succ |
134 "[| a: N; 0 = succ(a) : N |] ==> 0: F" |
134 "[| a: N; 0 = succ(a) : N |] ==> 0: F" |
135 |
135 |
136 |
136 |
137 (*The Product of a family of types*) |
137 (*The Product of a family of types*) |
138 |
138 |
139 ProdF "[| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A.B(x) type" |
139 ProdF "[| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type" |
140 |
140 |
141 ProdFL |
141 ProdFL |
142 "[| A = C; !!x. x:A ==> B(x) = D(x) |] ==> |
142 "[| A = C; !!x. x:A ==> B(x) = D(x) |] ==> |
143 PROD x:A.B(x) = PROD x:C.D(x)" |
143 PROD x:A. B(x) = PROD x:C. D(x)" |
144 |
144 |
145 ProdI |
145 ProdI |
146 "[| A type; !!x. x:A ==> b(x):B(x)|] ==> lam x.b(x) : PROD x:A.B(x)" |
146 "[| A type; !!x. x:A ==> b(x):B(x)|] ==> lam x. b(x) : PROD x:A. B(x)" |
147 |
147 |
148 ProdIL |
148 ProdIL |
149 "[| A type; !!x. x:A ==> b(x) = c(x) : B(x)|] ==> |
149 "[| A type; !!x. x:A ==> b(x) = c(x) : B(x)|] ==> |
150 lam x.b(x) = lam x.c(x) : PROD x:A.B(x)" |
150 lam x. b(x) = lam x. c(x) : PROD x:A. B(x)" |
151 |
151 |
152 ProdE "[| p : PROD x:A.B(x); a : A |] ==> p`a : B(a)" |
152 ProdE "[| p : PROD x:A. B(x); a : A |] ==> p`a : B(a)" |
153 ProdEL "[| p=q: PROD x:A.B(x); a=b : A |] ==> p`a = q`b : B(a)" |
153 ProdEL "[| p=q: PROD x:A. B(x); a=b : A |] ==> p`a = q`b : B(a)" |
154 |
154 |
155 ProdC |
155 ProdC |
156 "[| a : A; !!x. x:A ==> b(x) : B(x)|] ==> |
156 "[| a : A; !!x. x:A ==> b(x) : B(x)|] ==> |
157 (lam x.b(x)) ` a = b(a) : B(a)" |
157 (lam x. b(x)) ` a = b(a) : B(a)" |
158 |
158 |
159 ProdC2 |
159 ProdC2 |
160 "p : PROD x:A.B(x) ==> (lam x. p`x) = p : PROD x:A.B(x)" |
160 "p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x)" |
161 |
161 |
162 |
162 |
163 (*The Sum of a family of types*) |
163 (*The Sum of a family of types*) |
164 |
164 |
165 SumF "[| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A.B(x) type" |
165 SumF "[| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type" |
166 SumFL |
166 SumFL |
167 "[| A = C; !!x. x:A ==> B(x) = D(x) |] ==> SUM x:A.B(x) = SUM x:C.D(x)" |
167 "[| A = C; !!x. x:A ==> B(x) = D(x) |] ==> SUM x:A. B(x) = SUM x:C. D(x)" |
168 |
168 |
169 SumI "[| a : A; b : B(a) |] ==> <a,b> : SUM x:A.B(x)" |
169 SumI "[| a : A; b : B(a) |] ==> <a,b> : SUM x:A. B(x)" |
170 SumIL "[| a=c:A; b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A.B(x)" |
170 SumIL "[| a=c:A; b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A. B(x)" |
171 |
171 |
172 SumE |
172 SumE |
173 "[| p: SUM x:A.B(x); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] |
173 "[| p: SUM x:A. B(x); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] |
174 ==> split(p, %x y.c(x,y)) : C(p)" |
174 ==> split(p, %x y. c(x,y)) : C(p)" |
175 |
175 |
176 SumEL |
176 SumEL |
177 "[| p=q : SUM x:A.B(x); |
177 "[| p=q : SUM x:A. B(x); |
178 !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)|] |
178 !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)|] |
179 ==> split(p, %x y.c(x,y)) = split(q, % x y.d(x,y)) : C(p)" |
179 ==> split(p, %x y. c(x,y)) = split(q, % x y. d(x,y)) : C(p)" |
180 |
180 |
181 SumC |
181 SumC |
182 "[| a: A; b: B(a); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] |
182 "[| a: A; b: B(a); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] |
183 ==> split(<a,b>, %x y.c(x,y)) = c(a,b) : C(<a,b>)" |
183 ==> split(<a,b>, %x y. c(x,y)) = c(a,b) : C(<a,b>)" |
184 |
184 |
185 fst_def "fst(a) == split(a, %x y.x)" |
185 fst_def "fst(a) == split(a, %x y. x)" |
186 snd_def "snd(a) == split(a, %x y.y)" |
186 snd_def "snd(a) == split(a, %x y. y)" |
187 |
187 |
188 |
188 |
189 (*The sum of two types*) |
189 (*The sum of two types*) |
190 |
190 |
191 PlusF "[| A type; B type |] ==> A+B type" |
191 PlusF "[| A type; B type |] ==> A+B type" |
198 PlusI_inrL "[| A type; b = d : B |] ==> inr(b) = inr(d) : A+B" |
198 PlusI_inrL "[| A type; b = d : B |] ==> inr(b) = inr(d) : A+B" |
199 |
199 |
200 PlusE |
200 PlusE |
201 "[| p: A+B; !!x. x:A ==> c(x): C(inl(x)); |
201 "[| p: A+B; !!x. x:A ==> c(x): C(inl(x)); |
202 !!y. y:B ==> d(y): C(inr(y)) |] |
202 !!y. y:B ==> d(y): C(inr(y)) |] |
203 ==> when(p, %x.c(x), %y.d(y)) : C(p)" |
203 ==> when(p, %x. c(x), %y. d(y)) : C(p)" |
204 |
204 |
205 PlusEL |
205 PlusEL |
206 "[| p = q : A+B; !!x. x: A ==> c(x) = e(x) : C(inl(x)); |
206 "[| p = q : A+B; !!x. x: A ==> c(x) = e(x) : C(inl(x)); |
207 !!y. y: B ==> d(y) = f(y) : C(inr(y)) |] |
207 !!y. y: B ==> d(y) = f(y) : C(inr(y)) |] |
208 ==> when(p, %x.c(x), %y.d(y)) = when(q, %x.e(x), %y.f(y)) : C(p)" |
208 ==> when(p, %x. c(x), %y. d(y)) = when(q, %x. e(x), %y. f(y)) : C(p)" |
209 |
209 |
210 PlusC_inl |
210 PlusC_inl |
211 "[| a: A; !!x. x:A ==> c(x): C(inl(x)); |
211 "[| a: A; !!x. x:A ==> c(x): C(inl(x)); |
212 !!y. y:B ==> d(y): C(inr(y)) |] |
212 !!y. y:B ==> d(y): C(inr(y)) |] |
213 ==> when(inl(a), %x.c(x), %y.d(y)) = c(a) : C(inl(a))" |
213 ==> when(inl(a), %x. c(x), %y. d(y)) = c(a) : C(inl(a))" |
214 |
214 |
215 PlusC_inr |
215 PlusC_inr |
216 "[| b: B; !!x. x:A ==> c(x): C(inl(x)); |
216 "[| b: B; !!x. x:A ==> c(x): C(inl(x)); |
217 !!y. y:B ==> d(y): C(inr(y)) |] |
217 !!y. y:B ==> d(y): C(inr(y)) |] |
218 ==> when(inr(b), %x.c(x), %y.d(y)) = d(b) : C(inr(b))" |
218 ==> when(inr(b), %x. c(x), %y. d(y)) = d(b) : C(inr(b))" |
219 |
219 |
220 |
220 |
221 (*The type Eq*) |
221 (*The type Eq*) |
222 |
222 |
223 EqF "[| A type; a : A; b : A |] ==> Eq(A,a,b) type" |
223 EqF "[| A type; a : A; b : A |] ==> Eq(A,a,b) type" |