0
|
1 |
(* Title: CTT/ctt.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1991 University of Cambridge
|
|
5 |
|
|
6 |
Tactics and lemmas for ctt.thy (Constructive Type Theory)
|
|
7 |
*)
|
|
8 |
|
|
9 |
open CTT;
|
|
10 |
|
|
11 |
signature CTT_RESOLVE =
|
|
12 |
sig
|
|
13 |
val add_mp_tac: int -> tactic
|
|
14 |
val ASSUME: (int -> tactic) -> int -> tactic
|
|
15 |
val basic_defs: thm list
|
|
16 |
val comp_rls: thm list
|
|
17 |
val element_rls: thm list
|
|
18 |
val elimL_rls: thm list
|
|
19 |
val elim_rls: thm list
|
|
20 |
val eqintr_tac: tactic
|
|
21 |
val equal_tac: thm list -> tactic
|
|
22 |
val formL_rls: thm list
|
|
23 |
val form_rls: thm list
|
|
24 |
val form_tac: tactic
|
|
25 |
val intrL2_rls: thm list
|
|
26 |
val intrL_rls: thm list
|
|
27 |
val intr_rls: thm list
|
|
28 |
val intr_tac: thm list -> tactic
|
|
29 |
val mp_tac: int -> tactic
|
|
30 |
val NE_tac: string -> int -> tactic
|
|
31 |
val pc_tac: thm list -> int -> tactic
|
|
32 |
val PlusE_tac: string -> int -> tactic
|
|
33 |
val reduction_rls: thm list
|
|
34 |
val replace_type: thm
|
|
35 |
val routine_rls: thm list
|
|
36 |
val routine_tac: thm list -> thm list -> int -> tactic
|
|
37 |
val safe_brls: (bool * thm) list
|
|
38 |
val safestep_tac: thm list -> int -> tactic
|
|
39 |
val safe_tac: thm list -> int -> tactic
|
|
40 |
val step_tac: thm list -> int -> tactic
|
|
41 |
val subst_eqtyparg: thm
|
|
42 |
val subst_prodE: thm
|
|
43 |
val SumE_fst: thm
|
|
44 |
val SumE_snd: thm
|
|
45 |
val SumE_tac: string -> int -> tactic
|
|
46 |
val SumIL2: thm
|
|
47 |
val test_assume_tac: int -> tactic
|
|
48 |
val typechk_tac: thm list -> tactic
|
|
49 |
val unsafe_brls: (bool * thm) list
|
|
50 |
end;
|
|
51 |
|
|
52 |
|
|
53 |
structure CTT_Resolve : CTT_RESOLVE =
|
|
54 |
struct
|
|
55 |
|
|
56 |
(*Formation rules*)
|
|
57 |
val form_rls = [NF, ProdF, SumF, PlusF, EqF, FF, TF]
|
|
58 |
and formL_rls = [ProdFL, SumFL, PlusFL, EqFL];
|
|
59 |
|
|
60 |
|
|
61 |
(*Introduction rules
|
|
62 |
OMITTED: EqI, because its premise is an eqelem, not an elem*)
|
|
63 |
val intr_rls = [NI0, NI_succ, ProdI, SumI, PlusI_inl, PlusI_inr, TI]
|
|
64 |
and intrL_rls = [NI_succL, ProdIL, SumIL, PlusI_inlL, PlusI_inrL];
|
|
65 |
|
|
66 |
|
|
67 |
(*Elimination rules
|
|
68 |
OMITTED: EqE, because its conclusion is an eqelem, not an elem
|
|
69 |
TE, because it does not involve a constructor *)
|
|
70 |
val elim_rls = [NE, ProdE, SumE, PlusE, FE]
|
|
71 |
and elimL_rls = [NEL, ProdEL, SumEL, PlusEL, FEL];
|
|
72 |
|
|
73 |
(*OMITTED: eqC are TC because they make rewriting loop: p = un = un = ... *)
|
|
74 |
val comp_rls = [NC0, NC_succ, ProdC, SumC, PlusC_inl, PlusC_inr];
|
|
75 |
|
|
76 |
(*rules with conclusion a:A, an elem judgement*)
|
|
77 |
val element_rls = intr_rls @ elim_rls;
|
|
78 |
|
|
79 |
(*Definitions are (meta)equality axioms*)
|
|
80 |
val basic_defs = [fst_def,snd_def];
|
|
81 |
|
|
82 |
(*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
|
|
83 |
val SumIL2 = prove_goal CTT.thy
|
|
84 |
"[| c=a : A; d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)"
|
|
85 |
(fn prems=>
|
|
86 |
[ (resolve_tac [sym_elem] 1),
|
|
87 |
(resolve_tac [SumIL] 1),
|
|
88 |
(ALLGOALS (resolve_tac [sym_elem])),
|
|
89 |
(ALLGOALS (resolve_tac prems)) ]);
|
|
90 |
|
|
91 |
val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL];
|
|
92 |
|
|
93 |
(*Exploit p:Prod(A,B) to create the assumption z:B(a).
|
|
94 |
A more natural form of product elimination. *)
|
|
95 |
val subst_prodE = prove_goal CTT.thy
|
|
96 |
"[| p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z) \
|
|
97 |
\ |] ==> c(p`a): C(p`a)"
|
|
98 |
(fn prems=>
|
|
99 |
[ (REPEAT (resolve_tac (prems@[ProdE]) 1)) ]);
|
|
100 |
|
|
101 |
(** Tactics for type checking **)
|
|
102 |
|
|
103 |
fun is_rigid_elem (Const("Elem",_) $ a $ _) = not (is_Var (head_of a))
|
|
104 |
| is_rigid_elem _ = false;
|
|
105 |
|
|
106 |
(*Try solving a:A by assumption provided a is rigid!*)
|
|
107 |
val test_assume_tac = SUBGOAL(fn (prem,i) =>
|
|
108 |
if is_rigid_elem (Logic.strip_assums_concl prem)
|
|
109 |
then assume_tac i else no_tac);
|
|
110 |
|
|
111 |
fun ASSUME tf i = test_assume_tac i ORELSE tf i;
|
|
112 |
|
|
113 |
|
|
114 |
(*For simplification: type formation and checking,
|
|
115 |
but no equalities between terms*)
|
|
116 |
val routine_rls = form_rls @ formL_rls @ [refl_type] @ element_rls;
|
|
117 |
|
|
118 |
fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
|
|
119 |
|
|
120 |
|
|
121 |
(*Solve all subgoals "A type" using formation rules. *)
|
|
122 |
val form_tac = REPEAT_FIRST (filt_resolve_tac(form_rls) 1);
|
|
123 |
|
|
124 |
|
|
125 |
(*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
|
|
126 |
fun typechk_tac thms =
|
|
127 |
let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3
|
|
128 |
in REPEAT_FIRST (ASSUME tac) end;
|
|
129 |
|
|
130 |
|
|
131 |
(*Solve a:A (a flexible, A rigid) by introduction rules.
|
|
132 |
Cannot use stringtrees (filt_resolve_tac) since
|
|
133 |
goals like ?a:SUM(A,B) have a trivial head-string *)
|
|
134 |
fun intr_tac thms =
|
|
135 |
let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1
|
|
136 |
in REPEAT_FIRST (ASSUME tac) end;
|
|
137 |
|
|
138 |
|
|
139 |
(*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
|
|
140 |
fun equal_tac thms =
|
|
141 |
let val rls = thms @ form_rls @ element_rls @ intrL_rls @
|
|
142 |
elimL_rls @ [refl_elem]
|
|
143 |
in REPEAT_FIRST (ASSUME (filt_resolve_tac rls 3)) end;
|
|
144 |
|
|
145 |
(*** Simplification ***)
|
|
146 |
|
|
147 |
(*To simplify the type in a goal*)
|
|
148 |
val replace_type = prove_goal CTT.thy
|
|
149 |
"[| B = A; a : A |] ==> a : B"
|
|
150 |
(fn prems=>
|
|
151 |
[ (resolve_tac [equal_types] 1),
|
|
152 |
(resolve_tac [sym_type] 2),
|
|
153 |
(ALLGOALS (resolve_tac prems)) ]);
|
|
154 |
|
|
155 |
(*Simplify the parameter of a unary type operator.*)
|
|
156 |
val subst_eqtyparg = prove_goal CTT.thy
|
|
157 |
"a=c : A ==> (!!z.z:A ==> B(z) type) ==> B(a)=B(c)"
|
|
158 |
(fn prems=>
|
|
159 |
[ (resolve_tac [subst_typeL] 1),
|
|
160 |
(resolve_tac [refl_type] 2),
|
|
161 |
(ALLGOALS (resolve_tac prems)),
|
|
162 |
(assume_tac 1) ]);
|
|
163 |
|
|
164 |
(*Make a reduction rule for simplification.
|
|
165 |
A goal a=c becomes b=c, by virtue of a=b *)
|
|
166 |
fun resolve_trans rl = rl RS trans_elem;
|
|
167 |
|
|
168 |
(*Simplification rules for Constructive Type Theory*)
|
|
169 |
val reduction_rls = map resolve_trans comp_rls;
|
|
170 |
|
|
171 |
(*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
|
|
172 |
Uses other intro rules to avoid changing flexible goals.*)
|
|
173 |
val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1));
|
|
174 |
|
|
175 |
(** Tactics that instantiate CTT-rules.
|
|
176 |
Vars in the given terms will be incremented!
|
|
177 |
The (resolve_tac [EqE] i) lets them apply to equality judgements. **)
|
|
178 |
|
|
179 |
fun NE_tac (sp: string) i =
|
|
180 |
TRY (resolve_tac [EqE] i) THEN res_inst_tac [ ("p",sp) ] NE i;
|
|
181 |
|
|
182 |
fun SumE_tac (sp: string) i =
|
|
183 |
TRY (resolve_tac [EqE] i) THEN res_inst_tac [ ("p",sp) ] SumE i;
|
|
184 |
|
|
185 |
fun PlusE_tac (sp: string) i =
|
|
186 |
TRY (resolve_tac [EqE] i) THEN res_inst_tac [ ("p",sp) ] PlusE i;
|
|
187 |
|
|
188 |
(** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **)
|
|
189 |
|
|
190 |
(*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
|
|
191 |
fun add_mp_tac i =
|
|
192 |
resolve_tac [subst_prodE] i THEN assume_tac i THEN assume_tac i;
|
|
193 |
|
|
194 |
(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
|
|
195 |
fun mp_tac i = eresolve_tac [subst_prodE] i THEN assume_tac i;
|
|
196 |
|
|
197 |
(*"safe" when regarded as predicate calculus rules*)
|
|
198 |
val safe_brls = sort lessb
|
|
199 |
[ (true,FE), (true,asm_rl),
|
|
200 |
(false,ProdI), (true,SumE), (true,PlusE) ];
|
|
201 |
|
|
202 |
val unsafe_brls =
|
|
203 |
[ (false,PlusI_inl), (false,PlusI_inr), (false,SumI),
|
|
204 |
(true,subst_prodE) ];
|
|
205 |
|
|
206 |
(*0 subgoals vs 1 or more*)
|
|
207 |
val (safe0_brls, safep_brls) =
|
|
208 |
partition (apl(0,op=) o subgoals_of_brl) safe_brls;
|
|
209 |
|
|
210 |
fun safestep_tac thms i =
|
|
211 |
form_tac ORELSE
|
|
212 |
resolve_tac thms i ORELSE
|
|
213 |
biresolve_tac safe0_brls i ORELSE mp_tac i ORELSE
|
|
214 |
DETERM (biresolve_tac safep_brls i);
|
|
215 |
|
|
216 |
fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i);
|
|
217 |
|
|
218 |
fun step_tac thms = safestep_tac thms ORELSE' biresolve_tac unsafe_brls;
|
|
219 |
|
|
220 |
(*Fails unless it solves the goal!*)
|
|
221 |
fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms);
|
|
222 |
|
|
223 |
(** The elimination rules for fst/snd **)
|
|
224 |
|
|
225 |
val SumE_fst = prove_goal CTT.thy
|
|
226 |
"p : Sum(A,B) ==> fst(p) : A"
|
|
227 |
(fn prems=>
|
|
228 |
[ (rewrite_goals_tac basic_defs),
|
|
229 |
(resolve_tac elim_rls 1),
|
|
230 |
(REPEAT (pc_tac prems 1)),
|
|
231 |
(fold_tac basic_defs) ]);
|
|
232 |
|
|
233 |
(*The first premise must be p:Sum(A,B) !!*)
|
|
234 |
val SumE_snd = prove_goal CTT.thy
|
|
235 |
"[| p: Sum(A,B); A type; !!x. x:A ==> B(x) type \
|
|
236 |
\ |] ==> snd(p) : B(fst(p))"
|
|
237 |
(fn prems=>
|
|
238 |
[ (rewrite_goals_tac basic_defs),
|
|
239 |
(resolve_tac elim_rls 1),
|
|
240 |
(resolve_tac prems 1),
|
|
241 |
(resolve_tac [replace_type] 1),
|
|
242 |
(resolve_tac [subst_eqtyparg] 1), (*like B(x) equality formation?*)
|
|
243 |
(resolve_tac comp_rls 1),
|
|
244 |
(typechk_tac prems),
|
|
245 |
(fold_tac basic_defs) ]);
|
|
246 |
|
|
247 |
end;
|
|
248 |
|
|
249 |
open CTT_Resolve;
|