1 (* Title: Subst/Unify |
|
2 ID: $Id$ |
|
3 Author: Konrad Slind, Cambridge University Computer Laboratory |
|
4 Copyright 1997 University of Cambridge |
|
5 |
|
6 Unification algorithm |
|
7 *) |
|
8 |
|
9 (*--------------------------------------------------------------------------- |
|
10 * This file defines a nested unification algorithm, then proves that it |
|
11 * terminates, then proves 2 correctness theorems: that when the algorithm |
|
12 * succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution. |
|
13 * Although the proofs may seem long, they are actually quite direct, in that |
|
14 * the correctness and termination properties are not mingled as much as in |
|
15 * previous proofs of this algorithm. |
|
16 * |
|
17 * Our approach for nested recursive functions is as follows: |
|
18 * |
|
19 * 0. Prove the wellfoundedness of the termination relation. |
|
20 * 1. Prove the non-nested termination conditions. |
|
21 * 2. Eliminate (0) and (1) from the recursion equations and the |
|
22 * induction theorem. |
|
23 * 3. Prove the nested termination conditions by using the induction |
|
24 * theorem from (2) and by using the recursion equations from (2). |
|
25 * These are constrained by the nested termination conditions, but |
|
26 * things work out magically (by wellfoundedness of the termination |
|
27 * relation). |
|
28 * 4. Eliminate the nested TCs from the results of (2). |
|
29 * 5. Prove further correctness properties using the results of (4). |
|
30 * |
|
31 * Deeper nestings require iteration of steps (3) and (4). |
|
32 *---------------------------------------------------------------------------*) |
|
33 |
|
34 (*--------------------------------------------------------------------------- |
|
35 * The non-nested TC plus the wellfoundedness of unifyRel. |
|
36 *---------------------------------------------------------------------------*) |
|
37 Tfl.tgoalw Unify.thy [] unify.simps; |
|
38 (* Wellfoundedness of unifyRel *) |
|
39 by (simp_tac (simpset() addsimps [unifyRel_def, |
|
40 wf_inv_image, wf_lex_prod, wf_finite_psubset, |
|
41 wf_measure]) 1); |
|
42 (* TC *) |
|
43 by Safe_tac; |
|
44 by (simp_tac (simpset() addsimps [finite_psubset_def, finite_vars_of, |
|
45 lex_prod_def, measure_def, inv_image_def]) 1); |
|
46 by (rtac (monotone_vars_of RS (subset_iff_psubset_eq RS iffD1) RS disjE) 1); |
|
47 by (Blast_tac 1); |
|
48 by (asm_simp_tac (simpset() addsimps [less_eq, less_add_Suc1]) 1); |
|
49 qed "tc0"; |
|
50 |
|
51 |
|
52 (*--------------------------------------------------------------------------- |
|
53 * Termination proof. |
|
54 *---------------------------------------------------------------------------*) |
|
55 |
|
56 Goalw [unifyRel_def, measure_def] "trans unifyRel"; |
|
57 by (REPEAT (resolve_tac [trans_inv_image, trans_lex_prod, |
|
58 trans_finite_psubset, trans_less_than, |
|
59 trans_inv_image] 1)); |
|
60 qed "trans_unifyRel"; |
|
61 |
|
62 |
|
63 (*--------------------------------------------------------------------------- |
|
64 * The following lemma is used in the last step of the termination proof for |
|
65 * the nested call in Unify. Loosely, it says that unifyRel doesn't care |
|
66 * about term structure. |
|
67 *---------------------------------------------------------------------------*) |
|
68 Goalw [unifyRel_def,lex_prod_def, inv_image_def] |
|
69 "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel ==> \ |
|
70 \ ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel"; |
|
71 by (asm_full_simp_tac (simpset() addsimps [measure_def, |
|
72 less_eq, inv_image_def,add_assoc]) 1); |
|
73 by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \ |
|
74 \ (vars_of D Un vars_of E Un vars_of F)) = \ |
|
75 \ (vars_of A Un (vars_of B Un vars_of C) Un \ |
|
76 \ (vars_of D Un (vars_of E Un vars_of F)))" 1); |
|
77 by (Blast_tac 2); |
|
78 by (Asm_simp_tac 1); |
|
79 qed "Rassoc"; |
|
80 |
|
81 |
|
82 (*--------------------------------------------------------------------------- |
|
83 * This lemma proves the nested termination condition for the base cases |
|
84 * 3, 4, and 6. |
|
85 *---------------------------------------------------------------------------*) |
|
86 Goal "~(Var x <: M) ==> \ |
|
87 \ ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel \ |
|
88 \ & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel"; |
|
89 by (case_tac "Var x = M" 1); |
|
90 by (hyp_subst_tac 1); |
|
91 by (Simp_tac 1); |
|
92 by (case_tac "x: (vars_of N1 Un vars_of N2)" 1); |
|
93 (*uterm_less case*) |
|
94 by (asm_simp_tac |
|
95 (simpset() addsimps [less_eq, unifyRel_def, lex_prod_def, |
|
96 measure_def, inv_image_def]) 1); |
|
97 by (Blast_tac 1); |
|
98 (*finite_psubset case*) |
|
99 by (simp_tac |
|
100 (simpset() addsimps [unifyRel_def, lex_prod_def, |
|
101 measure_def, inv_image_def]) 1); |
|
102 by (simp_tac (simpset() addsimps [finite_psubset_def, finite_vars_of, |
|
103 psubset_def]) 1); |
|
104 by (Blast_tac 1); |
|
105 (** LEVEL 9 **) |
|
106 (*Final case, also finite_psubset*) |
|
107 by (simp_tac |
|
108 (simpset() addsimps [finite_vars_of, unifyRel_def, finite_psubset_def, |
|
109 lex_prod_def, measure_def, inv_image_def]) 1); |
|
110 by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N2")] Var_elim 1); |
|
111 by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N1")] Var_elim 3); |
|
112 by (ALLGOALS (asm_simp_tac(simpset() addsimps [srange_iff, vars_iff_occseq]))); |
|
113 by (REPEAT_FIRST (resolve_tac [conjI, disjI1, psubsetI])); |
|
114 by (ALLGOALS (asm_full_simp_tac |
|
115 (simpset() addsimps [srange_iff]))); |
|
116 by (ALLGOALS |
|
117 (fast_tac (claset() addEs [Var_intro RS disjE] |
|
118 addss (simpset() addsimps [srange_iff])))); |
|
119 qed "var_elimR"; |
|
120 |
|
121 |
|
122 (*--------------------------------------------------------------------------- |
|
123 * Eliminate tc0 from the recursion equations and the induction theorem. |
|
124 *---------------------------------------------------------------------------*) |
|
125 val wfr = tc0 RS conjunct1 |
|
126 and tc = tc0 RS conjunct2; |
|
127 val unifyRules0 = map (rule_by_tactic (rtac wfr 1 THEN TRY(rtac tc 1))) |
|
128 unify.simps; |
|
129 |
|
130 val unifyInduct0 = [wfr,tc] MRS unify.induct; |
|
131 |
|
132 |
|
133 (*--------------------------------------------------------------------------- |
|
134 * The nested TC. Proved by recursion induction. |
|
135 *---------------------------------------------------------------------------*) |
|
136 val [_,_,tc3] = unify.tcs; |
|
137 goalw_cterm [] (cterm_of (sign_of Unify.thy) (HOLogic.mk_Trueprop tc3)); |
|
138 (*--------------------------------------------------------------------------- |
|
139 * The extracted TC needs the scope of its quantifiers adjusted, so our |
|
140 * first step is to restrict the scopes of N1 and N2. |
|
141 *---------------------------------------------------------------------------*) |
|
142 by (subgoal_tac "!M1 M2 theta. \ |
|
143 \ unify(M1, M2) = Some theta --> \ |
|
144 \ (!N1 N2. ((N1<|theta, N2<|theta), (Comb M1 N1, Comb M2 N2)) : unifyRel)" 1); |
|
145 by (Blast_tac 1); |
|
146 by (rtac allI 1); |
|
147 by (rtac allI 1); |
|
148 (* Apply induction *) |
|
149 by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1); |
|
150 by (ALLGOALS |
|
151 (asm_simp_tac (simpset() addsimps (var_elimR::unifyRules0)))); |
|
152 (*Const-Const case*) |
|
153 by (simp_tac |
|
154 (simpset() addsimps [unifyRel_def, lex_prod_def, measure_def, |
|
155 inv_image_def, less_eq]) 1); |
|
156 (** LEVEL 7 **) |
|
157 (*Comb-Comb case*) |
|
158 by (asm_simp_tac (simpset() addsplits [option.split]) 1); |
|
159 by (strip_tac 1); |
|
160 by (rtac (trans_unifyRel RS transD) 1); |
|
161 by (Blast_tac 1); |
|
162 by (simp_tac (HOL_ss addsimps [subst_Comb RS sym]) 1); |
|
163 by (rtac Rassoc 1); |
|
164 by (Blast_tac 1); |
|
165 qed_spec_mp "unify_TC"; |
|
166 |
|
167 |
|
168 (*--------------------------------------------------------------------------- |
|
169 * Now for elimination of nested TC from unify.simps and induction. |
|
170 *---------------------------------------------------------------------------*) |
|
171 |
|
172 (*Desired rule, copied from the theory file. Could it be made available?*) |
|
173 Goal "unify(Comb M1 N1, Comb M2 N2) = \ |
|
174 \ (case unify(M1,M2) \ |
|
175 \ of None => None \ |
|
176 \ | Some theta => (case unify(N1 <| theta, N2 <| theta) \ |
|
177 \ of None => None \ |
|
178 \ | Some sigma => Some (theta <> sigma)))"; |
|
179 by (asm_simp_tac (simpset() addsimps (unify_TC::unifyRules0) |
|
180 addsplits [option.split]) 1); |
|
181 qed "unifyCombComb"; |
|
182 |
|
183 |
|
184 val unifyRules = rev (unifyCombComb :: tl (rev unifyRules0)); |
|
185 |
|
186 Addsimps unifyRules; |
|
187 |
|
188 bind_thm ("unifyInduct", |
|
189 rule_by_tactic |
|
190 (ALLGOALS (full_simp_tac (simpset() addsimps [unify_TC]))) |
|
191 unifyInduct0); |
|
192 |
|
193 |
|
194 (*--------------------------------------------------------------------------- |
|
195 * Correctness. Notice that idempotence is not needed to prove that the |
|
196 * algorithm terminates and is not needed to prove the algorithm correct, |
|
197 * if you are only interested in an MGU. This is in contrast to the |
|
198 * approach of M&W, who used idempotence and MGU-ness in the termination proof. |
|
199 *---------------------------------------------------------------------------*) |
|
200 |
|
201 Goal "!theta. unify(M,N) = Some theta --> MGUnifier theta M N"; |
|
202 by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1); |
|
203 by (ALLGOALS Asm_simp_tac); |
|
204 (*Const-Const case*) |
|
205 by (simp_tac (simpset() addsimps [MGUnifier_def,Unifier_def]) 1); |
|
206 (*Const-Var case*) |
|
207 by (stac mgu_sym 1); |
|
208 by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1); |
|
209 (*Var-M case*) |
|
210 by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1); |
|
211 (*Comb-Var case*) |
|
212 by (stac mgu_sym 1); |
|
213 by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1); |
|
214 (** LEVEL 8 **) |
|
215 (*Comb-Comb case*) |
|
216 by (asm_simp_tac (simpset() addsplits [option.split]) 1); |
|
217 by (strip_tac 1); |
|
218 by (asm_full_simp_tac |
|
219 (simpset() addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1); |
|
220 by (Safe_tac THEN rename_tac "theta sigma gamma" 1); |
|
221 by (eres_inst_tac [("x","gamma")] allE 1 THEN mp_tac 1); |
|
222 by (etac exE 1 THEN rename_tac "delta" 1); |
|
223 by (eres_inst_tac [("x","delta")] allE 1); |
|
224 by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1); |
|
225 (*Proving the subgoal*) |
|
226 by (full_simp_tac (simpset() addsimps [subst_eq_iff]) 2 |
|
227 THEN blast_tac (claset() addIs [trans,sym] delrules [impCE]) 2); |
|
228 by (blast_tac (claset() addIs [subst_trans, subst_cong, |
|
229 comp_assoc RS subst_sym]) 1); |
|
230 qed_spec_mp "unify_gives_MGU"; |
|
231 |
|
232 |
|
233 (*--------------------------------------------------------------------------- |
|
234 * Unify returns idempotent substitutions, when it succeeds. |
|
235 *---------------------------------------------------------------------------*) |
|
236 Goal "!theta. unify(M,N) = Some theta --> Idem theta"; |
|
237 by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1); |
|
238 by (ALLGOALS |
|
239 (asm_simp_tac |
|
240 (simpset() addsimps [Var_Idem] addsplits [option.split]))); |
|
241 (*Comb-Comb case*) |
|
242 by Safe_tac; |
|
243 by (REPEAT (dtac spec 1 THEN mp_tac 1)); |
|
244 by (safe_tac (claset() addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU])); |
|
245 by (rtac Idem_comp 1); |
|
246 by (atac 1); |
|
247 by (atac 1); |
|
248 by (best_tac (claset() addss (simpset() addsimps |
|
249 [MoreGeneral_def, subst_eq_iff, Idem_def])) 1); |
|
250 qed_spec_mp "unify_gives_Idem"; |
|
251 |
|