wenzelm@17441
|
1 |
(* Title: CTT/CTT.thy
|
clasohm@0
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
clasohm@0
|
3 |
Copyright 1993 University of Cambridge
|
clasohm@0
|
4 |
*)
|
clasohm@0
|
5 |
|
wenzelm@17441
|
6 |
header {* Constructive Type Theory *}
|
clasohm@0
|
7 |
|
wenzelm@17441
|
8 |
theory CTT
|
wenzelm@17441
|
9 |
imports Pure
|
wenzelm@17441
|
10 |
begin
|
wenzelm@17441
|
11 |
|
wenzelm@49906
|
12 |
ML_file "~~/src/Provers/typedsimp.ML"
|
wenzelm@39814
|
13 |
setup Pure_Thy.old_appl_syntax_setup
|
wenzelm@26956
|
14 |
|
wenzelm@17441
|
15 |
typedecl i
|
wenzelm@17441
|
16 |
typedecl t
|
wenzelm@17441
|
17 |
typedecl o
|
clasohm@0
|
18 |
|
clasohm@0
|
19 |
consts
|
clasohm@0
|
20 |
(*Types*)
|
wenzelm@17441
|
21 |
F :: "t"
|
wenzelm@17441
|
22 |
T :: "t" (*F is empty, T contains one element*)
|
clasohm@0
|
23 |
contr :: "i=>i"
|
clasohm@0
|
24 |
tt :: "i"
|
clasohm@0
|
25 |
(*Natural numbers*)
|
clasohm@0
|
26 |
N :: "t"
|
clasohm@0
|
27 |
succ :: "i=>i"
|
clasohm@0
|
28 |
rec :: "[i, i, [i,i]=>i] => i"
|
clasohm@0
|
29 |
(*Unions*)
|
wenzelm@17441
|
30 |
inl :: "i=>i"
|
wenzelm@17441
|
31 |
inr :: "i=>i"
|
clasohm@0
|
32 |
when :: "[i, i=>i, i=>i]=>i"
|
clasohm@0
|
33 |
(*General Sum and Binary Product*)
|
clasohm@0
|
34 |
Sum :: "[t, i=>t]=>t"
|
wenzelm@17441
|
35 |
fst :: "i=>i"
|
wenzelm@17441
|
36 |
snd :: "i=>i"
|
clasohm@0
|
37 |
split :: "[i, [i,i]=>i] =>i"
|
clasohm@0
|
38 |
(*General Product and Function Space*)
|
clasohm@0
|
39 |
Prod :: "[t, i=>t]=>t"
|
wenzelm@14765
|
40 |
(*Types*)
|
wenzelm@22808
|
41 |
Plus :: "[t,t]=>t" (infixr "+" 40)
|
clasohm@0
|
42 |
(*Equality type*)
|
clasohm@0
|
43 |
Eq :: "[t,i,i]=>t"
|
clasohm@0
|
44 |
eq :: "i"
|
clasohm@0
|
45 |
(*Judgements*)
|
clasohm@0
|
46 |
Type :: "t => prop" ("(_ type)" [10] 5)
|
paulson@10467
|
47 |
Eqtype :: "[t,t]=>prop" ("(_ =/ _)" [10,10] 5)
|
clasohm@0
|
48 |
Elem :: "[i, t]=>prop" ("(_ /: _)" [10,10] 5)
|
paulson@10467
|
49 |
Eqelem :: "[i,i,t]=>prop" ("(_ =/ _ :/ _)" [10,10,10] 5)
|
clasohm@0
|
50 |
Reduce :: "[i,i]=>prop" ("Reduce[_,_]")
|
clasohm@0
|
51 |
(*Types*)
|
wenzelm@14765
|
52 |
|
clasohm@0
|
53 |
(*Functions*)
|
clasohm@0
|
54 |
lambda :: "(i => i) => i" (binder "lam " 10)
|
wenzelm@22808
|
55 |
app :: "[i,i]=>i" (infixl "`" 60)
|
clasohm@0
|
56 |
(*Natural numbers*)
|
wenzelm@41558
|
57 |
Zero :: "i" ("0")
|
clasohm@0
|
58 |
(*Pairing*)
|
clasohm@0
|
59 |
pair :: "[i,i]=>i" ("(1<_,/_>)")
|
clasohm@0
|
60 |
|
wenzelm@14765
|
61 |
syntax
|
wenzelm@19761
|
62 |
"_PROD" :: "[idt,t,t]=>t" ("(3PROD _:_./ _)" 10)
|
wenzelm@19761
|
63 |
"_SUM" :: "[idt,t,t]=>t" ("(3SUM _:_./ _)" 10)
|
wenzelm@19761
|
64 |
translations
|
wenzelm@35054
|
65 |
"PROD x:A. B" == "CONST Prod(A, %x. B)"
|
wenzelm@35054
|
66 |
"SUM x:A. B" == "CONST Sum(A, %x. B)"
|
wenzelm@14765
|
67 |
|
wenzelm@19761
|
68 |
abbreviation
|
wenzelm@21404
|
69 |
Arrow :: "[t,t]=>t" (infixr "-->" 30) where
|
wenzelm@19761
|
70 |
"A --> B == PROD _:A. B"
|
wenzelm@21404
|
71 |
abbreviation
|
wenzelm@21404
|
72 |
Times :: "[t,t]=>t" (infixr "*" 50) where
|
wenzelm@19761
|
73 |
"A * B == SUM _:A. B"
|
clasohm@0
|
74 |
|
wenzelm@21210
|
75 |
notation (xsymbols)
|
wenzelm@21524
|
76 |
lambda (binder "\<lambda>\<lambda>" 10) and
|
wenzelm@21404
|
77 |
Elem ("(_ /\<in> _)" [10,10] 5) and
|
wenzelm@21404
|
78 |
Eqelem ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
|
wenzelm@21404
|
79 |
Arrow (infixr "\<longrightarrow>" 30) and
|
wenzelm@19761
|
80 |
Times (infixr "\<times>" 50)
|
wenzelm@17441
|
81 |
|
wenzelm@21210
|
82 |
notation (HTML output)
|
wenzelm@21524
|
83 |
lambda (binder "\<lambda>\<lambda>" 10) and
|
wenzelm@21404
|
84 |
Elem ("(_ /\<in> _)" [10,10] 5) and
|
wenzelm@21404
|
85 |
Eqelem ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
|
wenzelm@19761
|
86 |
Times (infixr "\<times>" 50)
|
wenzelm@17441
|
87 |
|
paulson@10467
|
88 |
syntax (xsymbols)
|
wenzelm@21524
|
89 |
"_PROD" :: "[idt,t,t] => t" ("(3\<Pi> _\<in>_./ _)" 10)
|
wenzelm@21524
|
90 |
"_SUM" :: "[idt,t,t] => t" ("(3\<Sigma> _\<in>_./ _)" 10)
|
paulson@10467
|
91 |
|
kleing@14565
|
92 |
syntax (HTML output)
|
wenzelm@21524
|
93 |
"_PROD" :: "[idt,t,t] => t" ("(3\<Pi> _\<in>_./ _)" 10)
|
wenzelm@21524
|
94 |
"_SUM" :: "[idt,t,t] => t" ("(3\<Sigma> _\<in>_./ _)" 10)
|
kleing@14565
|
95 |
|
clasohm@0
|
96 |
(*Reduction: a weaker notion than equality; a hack for simplification.
|
clasohm@0
|
97 |
Reduce[a,b] means either that a=b:A for some A or else that "a" and "b"
|
clasohm@0
|
98 |
are textually identical.*)
|
clasohm@0
|
99 |
|
clasohm@0
|
100 |
(*does not verify a:A! Sound because only trans_red uses a Reduce premise
|
clasohm@0
|
101 |
No new theorems can be proved about the standard judgements.*)
|
wenzelm@52445
|
102 |
axiomatization where
|
wenzelm@52445
|
103 |
refl_red: "\<And>a. Reduce[a,a]" and
|
wenzelm@52445
|
104 |
red_if_equal: "\<And>a b A. a = b : A ==> Reduce[a,b]" and
|
wenzelm@52445
|
105 |
trans_red: "\<And>a b c A. [| a = b : A; Reduce[b,c] |] ==> a = c : A" and
|
clasohm@0
|
106 |
|
clasohm@0
|
107 |
(*Reflexivity*)
|
clasohm@0
|
108 |
|
wenzelm@52445
|
109 |
refl_type: "\<And>A. A type ==> A = A" and
|
wenzelm@52445
|
110 |
refl_elem: "\<And>a A. a : A ==> a = a : A" and
|
clasohm@0
|
111 |
|
clasohm@0
|
112 |
(*Symmetry*)
|
clasohm@0
|
113 |
|
wenzelm@52445
|
114 |
sym_type: "\<And>A B. A = B ==> B = A" and
|
wenzelm@52445
|
115 |
sym_elem: "\<And>a b A. a = b : A ==> b = a : A" and
|
clasohm@0
|
116 |
|
clasohm@0
|
117 |
(*Transitivity*)
|
clasohm@0
|
118 |
|
wenzelm@52445
|
119 |
trans_type: "\<And>A B C. [| A = B; B = C |] ==> A = C" and
|
wenzelm@52445
|
120 |
trans_elem: "\<And>a b c A. [| a = b : A; b = c : A |] ==> a = c : A" and
|
clasohm@0
|
121 |
|
wenzelm@52445
|
122 |
equal_types: "\<And>a A B. [| a : A; A = B |] ==> a : B" and
|
wenzelm@52445
|
123 |
equal_typesL: "\<And>a b A B. [| a = b : A; A = B |] ==> a = b : B" and
|
clasohm@0
|
124 |
|
clasohm@0
|
125 |
(*Substitution*)
|
clasohm@0
|
126 |
|
wenzelm@52445
|
127 |
subst_type: "\<And>a A B. [| a : A; !!z. z:A ==> B(z) type |] ==> B(a) type" and
|
wenzelm@52445
|
128 |
subst_typeL: "\<And>a c A B D. [| a = c : A; !!z. z:A ==> B(z) = D(z) |] ==> B(a) = D(c)" and
|
clasohm@0
|
129 |
|
wenzelm@52445
|
130 |
subst_elem: "\<And>a b A B. [| a : A; !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a)" and
|
wenzelm@17441
|
131 |
subst_elemL:
|
wenzelm@52445
|
132 |
"\<And>a b c d A B. [| a=c : A; !!z. z:A ==> b(z)=d(z) : B(z) |] ==> b(a)=d(c) : B(a)" and
|
clasohm@0
|
133 |
|
clasohm@0
|
134 |
|
clasohm@0
|
135 |
(*The type N -- natural numbers*)
|
clasohm@0
|
136 |
|
wenzelm@52445
|
137 |
NF: "N type" and
|
wenzelm@52445
|
138 |
NI0: "0 : N" and
|
wenzelm@52445
|
139 |
NI_succ: "\<And>a. a : N ==> succ(a) : N" and
|
wenzelm@52445
|
140 |
NI_succL: "\<And>a b. a = b : N ==> succ(a) = succ(b) : N" and
|
clasohm@0
|
141 |
|
wenzelm@17441
|
142 |
NE:
|
wenzelm@52445
|
143 |
"\<And>p a b C. [| p: N; a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |]
|
wenzelm@52445
|
144 |
==> rec(p, a, %u v. b(u,v)) : C(p)" and
|
clasohm@0
|
145 |
|
wenzelm@17441
|
146 |
NEL:
|
wenzelm@52445
|
147 |
"\<And>p q a b c d C. [| p = q : N; a = c : C(0);
|
wenzelm@17441
|
148 |
!!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u)) |]
|
wenzelm@52445
|
149 |
==> rec(p, a, %u v. b(u,v)) = rec(q,c,d) : C(p)" and
|
clasohm@0
|
150 |
|
wenzelm@17441
|
151 |
NC0:
|
wenzelm@52445
|
152 |
"\<And>a b C. [| a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |]
|
wenzelm@52445
|
153 |
==> rec(0, a, %u v. b(u,v)) = a : C(0)" and
|
clasohm@0
|
154 |
|
wenzelm@17441
|
155 |
NC_succ:
|
wenzelm@52445
|
156 |
"\<And>p a b C. [| p: N; a: C(0);
|
wenzelm@17441
|
157 |
!!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==>
|
wenzelm@52445
|
158 |
rec(succ(p), a, %u v. b(u,v)) = b(p, rec(p, a, %u v. b(u,v))) : C(succ(p))" and
|
clasohm@0
|
159 |
|
clasohm@0
|
160 |
(*The fourth Peano axiom. See page 91 of Martin-Lof's book*)
|
wenzelm@17441
|
161 |
zero_ne_succ:
|
wenzelm@52445
|
162 |
"\<And>a. [| a: N; 0 = succ(a) : N |] ==> 0: F" and
|
clasohm@0
|
163 |
|
clasohm@0
|
164 |
|
clasohm@0
|
165 |
(*The Product of a family of types*)
|
clasohm@0
|
166 |
|
wenzelm@52445
|
167 |
ProdF: "\<And>A B. [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type" and
|
clasohm@0
|
168 |
|
wenzelm@17441
|
169 |
ProdFL:
|
wenzelm@52445
|
170 |
"\<And>A B C D. [| A = C; !!x. x:A ==> B(x) = D(x) |] ==>
|
wenzelm@52445
|
171 |
PROD x:A. B(x) = PROD x:C. D(x)" and
|
clasohm@0
|
172 |
|
wenzelm@17441
|
173 |
ProdI:
|
wenzelm@52445
|
174 |
"\<And>b A B. [| A type; !!x. x:A ==> b(x):B(x)|] ==> lam x. b(x) : PROD x:A. B(x)" and
|
clasohm@0
|
175 |
|
wenzelm@17441
|
176 |
ProdIL:
|
wenzelm@52445
|
177 |
"\<And>b c A B. [| A type; !!x. x:A ==> b(x) = c(x) : B(x)|] ==>
|
wenzelm@52445
|
178 |
lam x. b(x) = lam x. c(x) : PROD x:A. B(x)" and
|
clasohm@0
|
179 |
|
wenzelm@52445
|
180 |
ProdE: "\<And>p a A B. [| p : PROD x:A. B(x); a : A |] ==> p`a : B(a)" and
|
wenzelm@52445
|
181 |
ProdEL: "\<And>p q a b A B. [| p=q: PROD x:A. B(x); a=b : A |] ==> p`a = q`b : B(a)" and
|
clasohm@0
|
182 |
|
wenzelm@17441
|
183 |
ProdC:
|
wenzelm@52445
|
184 |
"\<And>a b A B. [| a : A; !!x. x:A ==> b(x) : B(x)|] ==>
|
wenzelm@52445
|
185 |
(lam x. b(x)) ` a = b(a) : B(a)" and
|
clasohm@0
|
186 |
|
wenzelm@17441
|
187 |
ProdC2:
|
wenzelm@52445
|
188 |
"\<And>p A B. p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x)" and
|
clasohm@0
|
189 |
|
clasohm@0
|
190 |
|
clasohm@0
|
191 |
(*The Sum of a family of types*)
|
clasohm@0
|
192 |
|
wenzelm@52445
|
193 |
SumF: "\<And>A B. [| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type" and
|
wenzelm@17441
|
194 |
SumFL:
|
wenzelm@52445
|
195 |
"\<And>A B C D. [| A = C; !!x. x:A ==> B(x) = D(x) |] ==> SUM x:A. B(x) = SUM x:C. D(x)" and
|
clasohm@0
|
196 |
|
wenzelm@52445
|
197 |
SumI: "\<And>a b A B. [| a : A; b : B(a) |] ==> <a,b> : SUM x:A. B(x)" and
|
wenzelm@52445
|
198 |
SumIL: "\<And>a b c d A B. [| a=c:A; b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A. B(x)" and
|
clasohm@0
|
199 |
|
wenzelm@17441
|
200 |
SumE:
|
wenzelm@52445
|
201 |
"\<And>p c A B C. [| p: SUM x:A. B(x); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |]
|
wenzelm@52445
|
202 |
==> split(p, %x y. c(x,y)) : C(p)" and
|
clasohm@0
|
203 |
|
wenzelm@17441
|
204 |
SumEL:
|
wenzelm@52445
|
205 |
"\<And>p q c d A B C. [| p=q : SUM x:A. B(x);
|
wenzelm@17441
|
206 |
!!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)|]
|
wenzelm@52445
|
207 |
==> split(p, %x y. c(x,y)) = split(q, % x y. d(x,y)) : C(p)" and
|
clasohm@0
|
208 |
|
wenzelm@17441
|
209 |
SumC:
|
wenzelm@52445
|
210 |
"\<And>a b c A B C. [| a: A; b: B(a); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |]
|
wenzelm@52445
|
211 |
==> split(<a,b>, %x y. c(x,y)) = c(a,b) : C(<a,b>)" and
|
clasohm@0
|
212 |
|
wenzelm@52445
|
213 |
fst_def: "\<And>a. fst(a) == split(a, %x y. x)" and
|
wenzelm@52445
|
214 |
snd_def: "\<And>a. snd(a) == split(a, %x y. y)" and
|
clasohm@0
|
215 |
|
clasohm@0
|
216 |
|
clasohm@0
|
217 |
(*The sum of two types*)
|
clasohm@0
|
218 |
|
wenzelm@52445
|
219 |
PlusF: "\<And>A B. [| A type; B type |] ==> A+B type" and
|
wenzelm@52445
|
220 |
PlusFL: "\<And>A B C D. [| A = C; B = D |] ==> A+B = C+D" and
|
clasohm@0
|
221 |
|
wenzelm@52445
|
222 |
PlusI_inl: "\<And>a A B. [| a : A; B type |] ==> inl(a) : A+B" and
|
wenzelm@52445
|
223 |
PlusI_inlL: "\<And>a c A B. [| a = c : A; B type |] ==> inl(a) = inl(c) : A+B" and
|
clasohm@0
|
224 |
|
wenzelm@52445
|
225 |
PlusI_inr: "\<And>b A B. [| A type; b : B |] ==> inr(b) : A+B" and
|
wenzelm@52445
|
226 |
PlusI_inrL: "\<And>b d A B. [| A type; b = d : B |] ==> inr(b) = inr(d) : A+B" and
|
clasohm@0
|
227 |
|
wenzelm@17441
|
228 |
PlusE:
|
wenzelm@52445
|
229 |
"\<And>p c d A B C. [| p: A+B; !!x. x:A ==> c(x): C(inl(x));
|
wenzelm@17441
|
230 |
!!y. y:B ==> d(y): C(inr(y)) |]
|
wenzelm@52445
|
231 |
==> when(p, %x. c(x), %y. d(y)) : C(p)" and
|
clasohm@0
|
232 |
|
wenzelm@17441
|
233 |
PlusEL:
|
wenzelm@52445
|
234 |
"\<And>p q c d e f A B C. [| p = q : A+B; !!x. x: A ==> c(x) = e(x) : C(inl(x));
|
wenzelm@17441
|
235 |
!!y. y: B ==> d(y) = f(y) : C(inr(y)) |]
|
wenzelm@52445
|
236 |
==> when(p, %x. c(x), %y. d(y)) = when(q, %x. e(x), %y. f(y)) : C(p)" and
|
clasohm@0
|
237 |
|
wenzelm@17441
|
238 |
PlusC_inl:
|
wenzelm@52445
|
239 |
"\<And>a c d A C. [| a: A; !!x. x:A ==> c(x): C(inl(x));
|
wenzelm@17441
|
240 |
!!y. y:B ==> d(y): C(inr(y)) |]
|
wenzelm@52445
|
241 |
==> when(inl(a), %x. c(x), %y. d(y)) = c(a) : C(inl(a))" and
|
clasohm@0
|
242 |
|
wenzelm@17441
|
243 |
PlusC_inr:
|
wenzelm@52445
|
244 |
"\<And>b c d A B C. [| b: B; !!x. x:A ==> c(x): C(inl(x));
|
wenzelm@17441
|
245 |
!!y. y:B ==> d(y): C(inr(y)) |]
|
wenzelm@52445
|
246 |
==> when(inr(b), %x. c(x), %y. d(y)) = d(b) : C(inr(b))" and
|
clasohm@0
|
247 |
|
clasohm@0
|
248 |
|
clasohm@0
|
249 |
(*The type Eq*)
|
clasohm@0
|
250 |
|
wenzelm@52445
|
251 |
EqF: "\<And>a b A. [| A type; a : A; b : A |] ==> Eq(A,a,b) type" and
|
wenzelm@52445
|
252 |
EqFL: "\<And>a b c d A B. [| A=B; a=c: A; b=d : A |] ==> Eq(A,a,b) = Eq(B,c,d)" and
|
wenzelm@52445
|
253 |
EqI: "\<And>a b A. a = b : A ==> eq : Eq(A,a,b)" and
|
wenzelm@52445
|
254 |
EqE: "\<And>p a b A. p : Eq(A,a,b) ==> a = b : A" and
|
clasohm@0
|
255 |
|
clasohm@0
|
256 |
(*By equality of types, can prove C(p) from C(eq), an elimination rule*)
|
wenzelm@52445
|
257 |
EqC: "\<And>p a b A. p : Eq(A,a,b) ==> p = eq : Eq(A,a,b)" and
|
clasohm@0
|
258 |
|
clasohm@0
|
259 |
(*The type F*)
|
clasohm@0
|
260 |
|
wenzelm@52445
|
261 |
FF: "F type" and
|
wenzelm@52445
|
262 |
FE: "\<And>p C. [| p: F; C type |] ==> contr(p) : C" and
|
wenzelm@52445
|
263 |
FEL: "\<And>p q C. [| p = q : F; C type |] ==> contr(p) = contr(q) : C" and
|
clasohm@0
|
264 |
|
clasohm@0
|
265 |
(*The type T
|
clasohm@0
|
266 |
Martin-Lof's book (page 68) discusses elimination and computation.
|
clasohm@0
|
267 |
Elimination can be derived by computation and equality of types,
|
clasohm@0
|
268 |
but with an extra premise C(x) type x:T.
|
clasohm@0
|
269 |
Also computation can be derived from elimination. *)
|
clasohm@0
|
270 |
|
wenzelm@52445
|
271 |
TF: "T type" and
|
wenzelm@52445
|
272 |
TI: "tt : T" and
|
wenzelm@52445
|
273 |
TE: "\<And>p c C. [| p : T; c : C(tt) |] ==> c : C(p)" and
|
wenzelm@52445
|
274 |
TEL: "\<And>p q c d C. [| p = q : T; c = d : C(tt) |] ==> c = d : C(p)" and
|
wenzelm@52445
|
275 |
TC: "\<And>p. p : T ==> p = tt : T"
|
wenzelm@17441
|
276 |
|
wenzelm@19761
|
277 |
|
wenzelm@19761
|
278 |
subsection "Tactics and derived rules for Constructive Type Theory"
|
wenzelm@19761
|
279 |
|
wenzelm@19761
|
280 |
(*Formation rules*)
|
wenzelm@19761
|
281 |
lemmas form_rls = NF ProdF SumF PlusF EqF FF TF
|
wenzelm@19761
|
282 |
and formL_rls = ProdFL SumFL PlusFL EqFL
|
wenzelm@19761
|
283 |
|
wenzelm@19761
|
284 |
(*Introduction rules
|
wenzelm@19761
|
285 |
OMITTED: EqI, because its premise is an eqelem, not an elem*)
|
wenzelm@19761
|
286 |
lemmas intr_rls = NI0 NI_succ ProdI SumI PlusI_inl PlusI_inr TI
|
wenzelm@19761
|
287 |
and intrL_rls = NI_succL ProdIL SumIL PlusI_inlL PlusI_inrL
|
wenzelm@19761
|
288 |
|
wenzelm@19761
|
289 |
(*Elimination rules
|
wenzelm@19761
|
290 |
OMITTED: EqE, because its conclusion is an eqelem, not an elem
|
wenzelm@19761
|
291 |
TE, because it does not involve a constructor *)
|
wenzelm@19761
|
292 |
lemmas elim_rls = NE ProdE SumE PlusE FE
|
wenzelm@19761
|
293 |
and elimL_rls = NEL ProdEL SumEL PlusEL FEL
|
wenzelm@19761
|
294 |
|
wenzelm@19761
|
295 |
(*OMITTED: eqC are TC because they make rewriting loop: p = un = un = ... *)
|
wenzelm@19761
|
296 |
lemmas comp_rls = NC0 NC_succ ProdC SumC PlusC_inl PlusC_inr
|
wenzelm@19761
|
297 |
|
wenzelm@19761
|
298 |
(*rules with conclusion a:A, an elem judgement*)
|
wenzelm@19761
|
299 |
lemmas element_rls = intr_rls elim_rls
|
wenzelm@19761
|
300 |
|
wenzelm@19761
|
301 |
(*Definitions are (meta)equality axioms*)
|
wenzelm@19761
|
302 |
lemmas basic_defs = fst_def snd_def
|
wenzelm@19761
|
303 |
|
wenzelm@19761
|
304 |
(*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
|
wenzelm@19761
|
305 |
lemma SumIL2: "[| c=a : A; d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)"
|
wenzelm@19761
|
306 |
apply (rule sym_elem)
|
wenzelm@19761
|
307 |
apply (rule SumIL)
|
wenzelm@19761
|
308 |
apply (rule_tac [!] sym_elem)
|
wenzelm@19761
|
309 |
apply assumption+
|
wenzelm@19761
|
310 |
done
|
wenzelm@19761
|
311 |
|
wenzelm@19761
|
312 |
lemmas intrL2_rls = NI_succL ProdIL SumIL2 PlusI_inlL PlusI_inrL
|
wenzelm@19761
|
313 |
|
wenzelm@19761
|
314 |
(*Exploit p:Prod(A,B) to create the assumption z:B(a).
|
wenzelm@19761
|
315 |
A more natural form of product elimination. *)
|
wenzelm@19761
|
316 |
lemma subst_prodE:
|
wenzelm@19761
|
317 |
assumes "p: Prod(A,B)"
|
wenzelm@19761
|
318 |
and "a: A"
|
wenzelm@19761
|
319 |
and "!!z. z: B(a) ==> c(z): C(z)"
|
wenzelm@19761
|
320 |
shows "c(p`a): C(p`a)"
|
wenzelm@41774
|
321 |
apply (rule assms ProdE)+
|
wenzelm@19761
|
322 |
done
|
wenzelm@19761
|
323 |
|
wenzelm@19761
|
324 |
|
wenzelm@19761
|
325 |
subsection {* Tactics for type checking *}
|
wenzelm@19761
|
326 |
|
wenzelm@19761
|
327 |
ML {*
|
wenzelm@19761
|
328 |
|
wenzelm@19761
|
329 |
local
|
wenzelm@19761
|
330 |
|
wenzelm@19761
|
331 |
fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not(is_Var (head_of a))
|
wenzelm@19761
|
332 |
| is_rigid_elem (Const("CTT.Eqelem",_) $ a $ _ $ _) = not(is_Var (head_of a))
|
wenzelm@19761
|
333 |
| is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a))
|
wenzelm@19761
|
334 |
| is_rigid_elem _ = false
|
wenzelm@19761
|
335 |
|
wenzelm@19761
|
336 |
in
|
wenzelm@19761
|
337 |
|
wenzelm@19761
|
338 |
(*Try solving a:A or a=b:A by assumption provided a is rigid!*)
|
wenzelm@19761
|
339 |
val test_assume_tac = SUBGOAL(fn (prem,i) =>
|
wenzelm@19761
|
340 |
if is_rigid_elem (Logic.strip_assums_concl prem)
|
wenzelm@19761
|
341 |
then assume_tac i else no_tac)
|
wenzelm@19761
|
342 |
|
wenzelm@19761
|
343 |
fun ASSUME tf i = test_assume_tac i ORELSE tf i
|
wenzelm@19761
|
344 |
|
wenzelm@19761
|
345 |
end;
|
wenzelm@19761
|
346 |
|
wenzelm@19761
|
347 |
*}
|
wenzelm@19761
|
348 |
|
wenzelm@19761
|
349 |
(*For simplification: type formation and checking,
|
wenzelm@19761
|
350 |
but no equalities between terms*)
|
wenzelm@19761
|
351 |
lemmas routine_rls = form_rls formL_rls refl_type element_rls
|
wenzelm@19761
|
352 |
|
wenzelm@19761
|
353 |
ML {*
|
wenzelm@19761
|
354 |
local
|
wenzelm@27208
|
355 |
val equal_rls = @{thms form_rls} @ @{thms element_rls} @ @{thms intrL_rls} @
|
wenzelm@27208
|
356 |
@{thms elimL_rls} @ @{thms refl_elem}
|
wenzelm@19761
|
357 |
in
|
wenzelm@19761
|
358 |
|
wenzelm@19761
|
359 |
fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
|
wenzelm@19761
|
360 |
|
wenzelm@19761
|
361 |
(*Solve all subgoals "A type" using formation rules. *)
|
wenzelm@27208
|
362 |
val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac @{thms form_rls} 1));
|
wenzelm@19761
|
363 |
|
wenzelm@19761
|
364 |
(*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
|
wenzelm@19761
|
365 |
fun typechk_tac thms =
|
wenzelm@27208
|
366 |
let val tac = filt_resolve_tac (thms @ @{thms form_rls} @ @{thms element_rls}) 3
|
wenzelm@19761
|
367 |
in REPEAT_FIRST (ASSUME tac) end
|
wenzelm@19761
|
368 |
|
wenzelm@19761
|
369 |
(*Solve a:A (a flexible, A rigid) by introduction rules.
|
wenzelm@19761
|
370 |
Cannot use stringtrees (filt_resolve_tac) since
|
wenzelm@19761
|
371 |
goals like ?a:SUM(A,B) have a trivial head-string *)
|
wenzelm@19761
|
372 |
fun intr_tac thms =
|
wenzelm@27208
|
373 |
let val tac = filt_resolve_tac(thms @ @{thms form_rls} @ @{thms intr_rls}) 1
|
wenzelm@19761
|
374 |
in REPEAT_FIRST (ASSUME tac) end
|
wenzelm@19761
|
375 |
|
wenzelm@19761
|
376 |
(*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
|
wenzelm@19761
|
377 |
fun equal_tac thms =
|
wenzelm@19761
|
378 |
REPEAT_FIRST (ASSUME (filt_resolve_tac (thms @ equal_rls) 3))
|
wenzelm@17441
|
379 |
|
clasohm@0
|
380 |
end
|
wenzelm@19761
|
381 |
|
wenzelm@19761
|
382 |
*}
|
wenzelm@19761
|
383 |
|
wenzelm@19761
|
384 |
|
wenzelm@19761
|
385 |
subsection {* Simplification *}
|
wenzelm@19761
|
386 |
|
wenzelm@19761
|
387 |
(*To simplify the type in a goal*)
|
wenzelm@19761
|
388 |
lemma replace_type: "[| B = A; a : A |] ==> a : B"
|
wenzelm@19761
|
389 |
apply (rule equal_types)
|
wenzelm@19761
|
390 |
apply (rule_tac [2] sym_type)
|
wenzelm@19761
|
391 |
apply assumption+
|
wenzelm@19761
|
392 |
done
|
wenzelm@19761
|
393 |
|
wenzelm@19761
|
394 |
(*Simplify the parameter of a unary type operator.*)
|
wenzelm@19761
|
395 |
lemma subst_eqtyparg:
|
wenzelm@23467
|
396 |
assumes 1: "a=c : A"
|
wenzelm@23467
|
397 |
and 2: "!!z. z:A ==> B(z) type"
|
wenzelm@19761
|
398 |
shows "B(a)=B(c)"
|
wenzelm@19761
|
399 |
apply (rule subst_typeL)
|
wenzelm@19761
|
400 |
apply (rule_tac [2] refl_type)
|
wenzelm@23467
|
401 |
apply (rule 1)
|
wenzelm@23467
|
402 |
apply (erule 2)
|
wenzelm@19761
|
403 |
done
|
wenzelm@19761
|
404 |
|
wenzelm@19761
|
405 |
(*Simplification rules for Constructive Type Theory*)
|
wenzelm@19761
|
406 |
lemmas reduction_rls = comp_rls [THEN trans_elem]
|
wenzelm@19761
|
407 |
|
wenzelm@19761
|
408 |
ML {*
|
wenzelm@19761
|
409 |
(*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
|
wenzelm@19761
|
410 |
Uses other intro rules to avoid changing flexible goals.*)
|
wenzelm@27208
|
411 |
val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac (@{thm EqI} :: @{thms intr_rls}) 1))
|
wenzelm@19761
|
412 |
|
wenzelm@19761
|
413 |
(** Tactics that instantiate CTT-rules.
|
wenzelm@19761
|
414 |
Vars in the given terms will be incremented!
|
wenzelm@19761
|
415 |
The (rtac EqE i) lets them apply to equality judgements. **)
|
wenzelm@19761
|
416 |
|
wenzelm@27208
|
417 |
fun NE_tac ctxt sp i =
|
wenzelm@27239
|
418 |
TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i
|
wenzelm@19761
|
419 |
|
wenzelm@27208
|
420 |
fun SumE_tac ctxt sp i =
|
wenzelm@27239
|
421 |
TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i
|
wenzelm@19761
|
422 |
|
wenzelm@27208
|
423 |
fun PlusE_tac ctxt sp i =
|
wenzelm@27239
|
424 |
TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i
|
wenzelm@19761
|
425 |
|
wenzelm@19761
|
426 |
(** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **)
|
wenzelm@19761
|
427 |
|
wenzelm@19761
|
428 |
(*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
|
wenzelm@19761
|
429 |
fun add_mp_tac i =
|
wenzelm@27208
|
430 |
rtac @{thm subst_prodE} i THEN assume_tac i THEN assume_tac i
|
wenzelm@19761
|
431 |
|
wenzelm@19761
|
432 |
(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
|
wenzelm@27208
|
433 |
fun mp_tac i = etac @{thm subst_prodE} i THEN assume_tac i
|
wenzelm@19761
|
434 |
|
wenzelm@19761
|
435 |
(*"safe" when regarded as predicate calculus rules*)
|
wenzelm@19761
|
436 |
val safe_brls = sort (make_ord lessb)
|
wenzelm@27208
|
437 |
[ (true, @{thm FE}), (true,asm_rl),
|
wenzelm@27208
|
438 |
(false, @{thm ProdI}), (true, @{thm SumE}), (true, @{thm PlusE}) ]
|
wenzelm@19761
|
439 |
|
wenzelm@19761
|
440 |
val unsafe_brls =
|
wenzelm@27208
|
441 |
[ (false, @{thm PlusI_inl}), (false, @{thm PlusI_inr}), (false, @{thm SumI}),
|
wenzelm@27208
|
442 |
(true, @{thm subst_prodE}) ]
|
wenzelm@19761
|
443 |
|
wenzelm@19761
|
444 |
(*0 subgoals vs 1 or more*)
|
wenzelm@19761
|
445 |
val (safe0_brls, safep_brls) =
|
wenzelm@19761
|
446 |
List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls
|
wenzelm@19761
|
447 |
|
wenzelm@19761
|
448 |
fun safestep_tac thms i =
|
wenzelm@19761
|
449 |
form_tac ORELSE
|
wenzelm@19761
|
450 |
resolve_tac thms i ORELSE
|
wenzelm@19761
|
451 |
biresolve_tac safe0_brls i ORELSE mp_tac i ORELSE
|
wenzelm@19761
|
452 |
DETERM (biresolve_tac safep_brls i)
|
wenzelm@19761
|
453 |
|
wenzelm@19761
|
454 |
fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i)
|
wenzelm@19761
|
455 |
|
wenzelm@19761
|
456 |
fun step_tac thms = safestep_tac thms ORELSE' biresolve_tac unsafe_brls
|
wenzelm@19761
|
457 |
|
wenzelm@19761
|
458 |
(*Fails unless it solves the goal!*)
|
wenzelm@19761
|
459 |
fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms)
|
wenzelm@19761
|
460 |
*}
|
wenzelm@19761
|
461 |
|
wenzelm@49906
|
462 |
ML_file "rew.ML"
|
wenzelm@19761
|
463 |
|
wenzelm@19761
|
464 |
|
wenzelm@19761
|
465 |
subsection {* The elimination rules for fst/snd *}
|
wenzelm@19761
|
466 |
|
wenzelm@19761
|
467 |
lemma SumE_fst: "p : Sum(A,B) ==> fst(p) : A"
|
wenzelm@19761
|
468 |
apply (unfold basic_defs)
|
wenzelm@19761
|
469 |
apply (erule SumE)
|
wenzelm@19761
|
470 |
apply assumption
|
wenzelm@19761
|
471 |
done
|
wenzelm@19761
|
472 |
|
wenzelm@19761
|
473 |
(*The first premise must be p:Sum(A,B) !!*)
|
wenzelm@19761
|
474 |
lemma SumE_snd:
|
wenzelm@19761
|
475 |
assumes major: "p: Sum(A,B)"
|
wenzelm@19761
|
476 |
and "A type"
|
wenzelm@19761
|
477 |
and "!!x. x:A ==> B(x) type"
|
wenzelm@19761
|
478 |
shows "snd(p) : B(fst(p))"
|
wenzelm@19761
|
479 |
apply (unfold basic_defs)
|
wenzelm@19761
|
480 |
apply (rule major [THEN SumE])
|
wenzelm@19761
|
481 |
apply (rule SumC [THEN subst_eqtyparg, THEN replace_type])
|
wenzelm@26391
|
482 |
apply (tactic {* typechk_tac @{thms assms} *})
|
wenzelm@19761
|
483 |
done
|
wenzelm@19761
|
484 |
|
wenzelm@19761
|
485 |
end
|