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