|
1 (*--------------------------------------------------------------------------- |
|
2 * This file defines a nested unification algorithm, then proves that it |
|
3 * terminates, then proves 2 correctness theorems: that when the algorithm |
|
4 * succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution. |
|
5 * Although the proofs may seem long, they are actually quite direct, in that |
|
6 * the correctness and termination properties are not mingled as much as in |
|
7 * previous proofs of this algorithm. |
|
8 * |
|
9 * Our approach for nested recursive functions is as follows: |
|
10 * |
|
11 * 0. Prove the wellfoundedness of the termination relation. |
|
12 * 1. Prove the non-nested termination conditions. |
|
13 * 2. Eliminate (0) and (1) from the recursion equations and the |
|
14 * induction theorem. |
|
15 * 3. Prove the nested termination conditions by using the induction |
|
16 * theorem from (2) and by using the recursion equations from (2). |
|
17 * These are constrained by the nested termination conditions, but |
|
18 * things work out magically (by wellfoundedness of the termination |
|
19 * relation). |
|
20 * 4. Eliminate the nested TCs from the results of (2). |
|
21 * 5. Prove further correctness properties using the results of (4). |
|
22 * |
|
23 * Deeper nestings require iteration of steps (3) and (4). |
|
24 *---------------------------------------------------------------------------*) |
|
25 |
|
26 (* This is just a wrapper for the definition mechanism. *) |
|
27 local fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[]))); |
|
28 in |
|
29 fun Rfunc thy R eqs = |
|
30 let val read = term_of o cread thy; |
|
31 in Tfl.Rfunction thy (read R) (read eqs) |
|
32 end |
|
33 end; |
|
34 |
|
35 (*--------------------------------------------------------------------------- |
|
36 * The algorithm. |
|
37 *---------------------------------------------------------------------------*) |
|
38 val {theory,induction,rules,tcs} = |
|
39 Rfunc Unify.thy "R" |
|
40 "(Unify(Const m, Const n) = (if (m=n) then Subst[] else Fail)) & \ |
|
41 \ (Unify(Const m, Comb M N) = Fail) & \ |
|
42 \ (Unify(Const m, Var v) = Subst[(v,Const m)]) & \ |
|
43 \ (Unify(Var v, M) = (if (Var v <: M) then Fail else Subst[(v,M)])) & \ |
|
44 \ (Unify(Comb M N, Const x) = Fail) & \ |
|
45 \ (Unify(Comb M N, Var v) = (if (Var v <: Comb M N) then Fail \ |
|
46 \ else Subst[(v,Comb M N)])) & \ |
|
47 \ (Unify(Comb M1 N1, Comb M2 N2) = \ |
|
48 \ (case Unify(M1,M2) \ |
|
49 \ of Fail => Fail \ |
|
50 \ | Subst theta => (case Unify(N1 <| theta, N2 <| theta) \ |
|
51 \ of Fail => Fail \ |
|
52 \ | Subst sigma => Subst (theta <> sigma))))"; |
|
53 |
|
54 open Unify; |
|
55 |
|
56 (*--------------------------------------------------------------------------- |
|
57 * A slightly augmented strip_tac. |
|
58 *---------------------------------------------------------------------------*) |
|
59 fun my_strip_tac i = |
|
60 CHANGED (strip_tac i |
|
61 THEN REPEAT ((etac exE ORELSE' etac conjE) i) |
|
62 THEN TRY (hyp_subst_tac i)); |
|
63 |
|
64 (*--------------------------------------------------------------------------- |
|
65 * A slightly augmented fast_tac for sets. It handles the case where the |
|
66 * top connective is "=". |
|
67 *---------------------------------------------------------------------------*) |
|
68 fun my_fast_set_tac i = (TRY(rtac set_ext i) THEN fast_tac set_cs i); |
|
69 |
|
70 |
|
71 (*--------------------------------------------------------------------------- |
|
72 * Wellfoundedness of proper subset on finite sets. |
|
73 *---------------------------------------------------------------------------*) |
|
74 goalw Unify.thy [R0_def] "wf(R0)"; |
|
75 by (rtac ((wf_subset RS mp) RS mp) 1); |
|
76 by (rtac wf_measure 1); |
|
77 by(simp_tac(!simpset addsimps[measure_def,inv_image_def,symmetric less_def])1); |
|
78 by (my_strip_tac 1); |
|
79 by (forward_tac[ssubset_card] 1); |
|
80 by (fast_tac set_cs 1); |
|
81 val wf_R0 = result(); |
|
82 |
|
83 |
|
84 (*--------------------------------------------------------------------------- |
|
85 * Tactic for selecting and working on the first projection of R. |
|
86 *---------------------------------------------------------------------------*) |
|
87 fun R0_tac thms i = |
|
88 (simp_tac (!simpset addsimps (thms@[R_def,lex_prod_def, |
|
89 measure_def,inv_image_def,point_to_prod_def])) i THEN |
|
90 REPEAT (rtac exI i) THEN |
|
91 REPEAT ((rtac conjI THEN' rtac refl) i) THEN |
|
92 rtac disjI1 i THEN |
|
93 simp_tac (!simpset addsimps [R0_def,finite_vars_of]) i); |
|
94 |
|
95 |
|
96 |
|
97 (*--------------------------------------------------------------------------- |
|
98 * Tactic for selecting and working on the second projection of R. |
|
99 *---------------------------------------------------------------------------*) |
|
100 fun R1_tac thms i = |
|
101 (simp_tac (!simpset addsimps (thms@[R_def,lex_prod_def, |
|
102 measure_def,inv_image_def,point_to_prod_def])) i THEN |
|
103 REPEAT (rtac exI i) THEN |
|
104 REPEAT ((rtac conjI THEN' rtac refl) i) THEN |
|
105 rtac disjI2 i THEN |
|
106 asm_simp_tac (!simpset addsimps [R1_def,rprod_def]) i); |
|
107 |
|
108 |
|
109 (*--------------------------------------------------------------------------- |
|
110 * The non-nested TC plus the wellfoundedness of R. |
|
111 *---------------------------------------------------------------------------*) |
|
112 Tfl.tgoalw Unify.thy [] rules; |
|
113 by (rtac conjI 1); |
|
114 (* TC *) |
|
115 by (my_strip_tac 1); |
|
116 by (cut_facts_tac [monotone_vars_of] 1); |
|
117 by (asm_full_simp_tac(!simpset addsimps [subseteq_iff_subset_eq]) 1); |
|
118 by (etac disjE 1); |
|
119 by (R0_tac[] 1); |
|
120 by (R1_tac[] 1); |
|
121 by (simp_tac |
|
122 (!simpset addsimps [measure_def,inv_image_def,less_eq,less_add_Suc1]) 1); |
|
123 |
|
124 (* Wellfoundedness of R *) |
|
125 by (simp_tac (!simpset addsimps [Unify.R_def,Unify.R1_def]) 1); |
|
126 by (REPEAT (resolve_tac [wf_inv_image,wf_lex_prod,wf_R0, |
|
127 wf_rel_prod, wf_measure] 1)); |
|
128 val tc0 = result(); |
|
129 |
|
130 |
|
131 (*--------------------------------------------------------------------------- |
|
132 * Eliminate tc0 from the recursion equations and the induction theorem. |
|
133 *---------------------------------------------------------------------------*) |
|
134 val [tc,wfr] = Prim.Rules.CONJUNCTS tc0; |
|
135 val rules1 = implies_intr_hyps rules; |
|
136 val rules2 = wfr RS rules1; |
|
137 |
|
138 val [a,b,c,d,e,f,g] = Prim.Rules.CONJUNCTS rules2; |
|
139 val g' = tc RS (g RS mp); |
|
140 val rules4 = standard (Prim.Rules.LIST_CONJ[a,b,c,d,e,f,g']); |
|
141 |
|
142 val induction1 = implies_intr_hyps induction; |
|
143 val induction2 = wfr RS induction1; |
|
144 val induction3 = tc RS induction2; |
|
145 |
|
146 val induction4 = standard |
|
147 (rewrite_rule[fst_conv RS eq_reflection, snd_conv RS eq_reflection] |
|
148 (induction3 RS (read_instantiate_sg (sign_of theory) |
|
149 [("x","%p. Phi (fst p) (snd p)")] spec))); |
|
150 |
|
151 |
|
152 (*--------------------------------------------------------------------------- |
|
153 * Some theorems about transitivity of WF combinators. Only the last |
|
154 * (transR) is used, in the proof of termination. The others are generic and |
|
155 * should maybe go somewhere. |
|
156 *---------------------------------------------------------------------------*) |
|
157 goalw WF1.thy [trans_def,lex_prod_def,mem_Collect_eq RS eq_reflection] |
|
158 "trans R1 & trans R2 --> trans (R1 ** R2)"; |
|
159 by (my_strip_tac 1); |
|
160 by (res_inst_tac [("x","a")] exI 1); |
|
161 by (res_inst_tac [("x","a'a")] exI 1); |
|
162 by (res_inst_tac [("x","b")] exI 1); |
|
163 by (res_inst_tac [("x","b'a")] exI 1); |
|
164 by (REPEAT (rewrite_tac [Pair_eq RS eq_reflection] THEN my_strip_tac 1)); |
|
165 by (Simp_tac 1); |
|
166 by (REPEAT (etac disjE 1)); |
|
167 by (rtac disjI1 1); |
|
168 by (ALLGOALS (fast_tac set_cs)); |
|
169 val trans_lex_prod = result() RS mp; |
|
170 |
|
171 |
|
172 goalw WF1.thy [trans_def,rprod_def,mem_Collect_eq RS eq_reflection] |
|
173 "trans R1 & trans R2 --> trans (rprod R1 R2)"; |
|
174 by (my_strip_tac 1); |
|
175 by (res_inst_tac [("x","a")] exI 1); |
|
176 by (res_inst_tac [("x","a'a")] exI 1); |
|
177 by (res_inst_tac [("x","b")] exI 1); |
|
178 by (res_inst_tac [("x","b'a")] exI 1); |
|
179 by (REPEAT (rewrite_tac [Pair_eq RS eq_reflection] THEN my_strip_tac 1)); |
|
180 by (Simp_tac 1); |
|
181 by (fast_tac set_cs 1); |
|
182 val trans_rprod = result() RS mp; |
|
183 |
|
184 |
|
185 goalw Unify.thy [trans_def,inv_image_def,mem_Collect_eq RS eq_reflection] |
|
186 "trans r --> trans (inv_image r f)"; |
|
187 by (rewrite_tac [fst_conv RS eq_reflection, snd_conv RS eq_reflection]); |
|
188 by (fast_tac set_cs 1); |
|
189 val trans_inv_image = result() RS mp; |
|
190 |
|
191 goalw Unify.thy [R0_def, trans_def, mem_Collect_eq RS eq_reflection] |
|
192 "trans R0"; |
|
193 by (rewrite_tac [fst_conv RS eq_reflection,snd_conv RS eq_reflection, |
|
194 ssubset_def, set_eq_subset RS eq_reflection]); |
|
195 by (fast_tac set_cs 1); |
|
196 val trans_R0 = result(); |
|
197 |
|
198 goalw Unify.thy [R_def,R1_def,measure_def] "trans R"; |
|
199 by (REPEAT (resolve_tac[trans_inv_image,trans_lex_prod,conjI, trans_R0, |
|
200 trans_rprod, trans_inv_image, trans_trancl] 1)); |
|
201 val transR = result(); |
|
202 |
|
203 |
|
204 (*--------------------------------------------------------------------------- |
|
205 * The following lemma is used in the last step of the termination proof for |
|
206 * the nested call in Unify. Loosely, it says that R doesn't care so much |
|
207 * about term structure. |
|
208 *---------------------------------------------------------------------------*) |
|
209 goalw Unify.thy [R_def,lex_prod_def, inv_image_def,point_to_prod_def] |
|
210 "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : R --> \ |
|
211 \ ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : R"; |
|
212 by (Simp_tac 1); |
|
213 by (rtac conjI 1); |
|
214 by (strip_tac 1); |
|
215 by (rtac disjI1 1); |
|
216 by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \ |
|
217 \ (vars_of D Un vars_of E Un vars_of F)) = \ |
|
218 \ (vars_of A Un (vars_of B Un vars_of C) Un \ |
|
219 \ (vars_of D Un (vars_of E Un vars_of F)))" 1); |
|
220 by (my_fast_set_tac 2); |
|
221 by (Asm_simp_tac 1); |
|
222 by (strip_tac 1); |
|
223 by (rtac disjI2 1); |
|
224 by (etac conjE 1); |
|
225 by (Asm_simp_tac 1); |
|
226 by (rtac conjI 1); |
|
227 by (my_fast_set_tac 1); |
|
228 by (asm_full_simp_tac (!simpset addsimps [R1_def, measure_def, rprod_def, |
|
229 less_eq, inv_image_def,add_assoc]) 1); |
|
230 val Rassoc = result() RS mp; |
|
231 |
|
232 (*--------------------------------------------------------------------------- |
|
233 * Rewriting support. |
|
234 *---------------------------------------------------------------------------*) |
|
235 |
|
236 val termin_ss = (!simpset addsimps (srange_iff::(subst_rews@al_rews))); |
|
237 |
|
238 |
|
239 (*--------------------------------------------------------------------------- |
|
240 * This lemma proves the nested termination condition for the base cases |
|
241 * 3, 4, and 6. It's a clumsy formulation (requiring two conjuncts, each with |
|
242 * exactly the same proof) of a more general theorem. |
|
243 *---------------------------------------------------------------------------*) |
|
244 goal theory "(~(Var x <: M)) --> [(x, M)] = theta --> \ |
|
245 \ (! N1 N2. (((N1 <| theta, N2 <| theta), (Comb M N1, Comb (Var x) N2)) : R) \ |
|
246 \ & (((N1 <| theta, N2 <| theta), (Comb(Var x) N1, Comb M N2)) : R))"; |
|
247 by (my_strip_tac 1); |
|
248 by (case_tac "Var x = M" 1); |
|
249 by (hyp_subst_tac 1); |
|
250 by (case_tac "x:(vars_of N1 Un vars_of N2)" 1); |
|
251 let val case1 = |
|
252 EVERY1[R1_tac[id_subst_lemma], rtac conjI, my_fast_set_tac, |
|
253 REPEAT o (rtac exI), REPEAT o (rtac conjI THEN' rtac refl), |
|
254 simp_tac (!simpset addsimps [measure_def,inv_image_def,less_eq])]; |
|
255 in by (rtac conjI 1); |
|
256 by case1; |
|
257 by case1 |
|
258 end; |
|
259 |
|
260 let val case2 = |
|
261 EVERY1[R0_tac[id_subst_lemma], |
|
262 simp_tac (!simpset addsimps [ssubset_def,set_eq_subset]), |
|
263 fast_tac set_cs] |
|
264 in by (rtac conjI 1); |
|
265 by case2; |
|
266 by case2 |
|
267 end; |
|
268 |
|
269 let val case3 = |
|
270 EVERY1 [R0_tac[], |
|
271 cut_inst_tac [("s2","[(x, M)]"), ("v2", "x"), ("t2","N1")] Var_elim] |
|
272 THEN ALLGOALS(asm_simp_tac(termin_ss addsimps [vars_iff_occseq])) |
|
273 THEN cut_inst_tac [("s2","[(x, M)]"),("v2", "x"), ("t2","N2")] Var_elim 1 |
|
274 THEN ALLGOALS(asm_simp_tac(termin_ss addsimps [vars_iff_occseq])) |
|
275 THEN EVERY1 [simp_tac (HOL_ss addsimps [ssubset_def]), |
|
276 rtac conjI, simp_tac (HOL_ss addsimps [subset_iff]), |
|
277 my_strip_tac, etac UnE, dtac Var_intro] |
|
278 THEN dtac Var_intro 2 |
|
279 THEN ALLGOALS (asm_full_simp_tac (termin_ss addsimps [set_eq_subset])) |
|
280 THEN TRYALL (fast_tac set_cs) |
|
281 in |
|
282 by (rtac conjI 1); |
|
283 by case3; |
|
284 by case3 |
|
285 end; |
|
286 val var_elimR = result() RS mp RS mp RS spec RS spec; |
|
287 |
|
288 |
|
289 val Some{nchotomy = subst_nchotomy,...} = assoc(!datatypes,"subst"); |
|
290 |
|
291 (*--------------------------------------------------------------------------- |
|
292 * Do a case analysis on something of type 'a subst. |
|
293 *---------------------------------------------------------------------------*) |
|
294 |
|
295 fun Subst_case_tac theta = |
|
296 (cut_inst_tac theta (standard (Prim.Rules.SPEC_ALL subst_nchotomy)) 1 |
|
297 THEN etac disjE 1 |
|
298 THEN rotate_tac ~1 1 |
|
299 THEN Asm_full_simp_tac 1 |
|
300 THEN etac exE 1 |
|
301 THEN rotate_tac ~1 1 |
|
302 THEN Asm_full_simp_tac 1); |
|
303 |
|
304 |
|
305 goals_limit := 1; |
|
306 |
|
307 (*--------------------------------------------------------------------------- |
|
308 * The nested TC. Proved by recursion induction. |
|
309 *---------------------------------------------------------------------------*) |
|
310 goalw_cterm [] |
|
311 (hd(tl(tl(map (cterm_of (sign_of theory) o USyntax.mk_prop) tcs)))); |
|
312 (*--------------------------------------------------------------------------- |
|
313 * The extracted TC needs the scope of its quantifiers adjusted, so our |
|
314 * first step is to restrict the scopes of N1 and N2. |
|
315 *---------------------------------------------------------------------------*) |
|
316 by (subgoal_tac "!M1 M2 theta. \ |
|
317 \ Unify (M1, M2) = Subst theta --> \ |
|
318 \ (!N1 N2. ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R)" 1); |
|
319 by (fast_tac HOL_cs 1); |
|
320 by (rtac allI 1); |
|
321 by (rtac allI 1); |
|
322 (* Apply induction *) |
|
323 by (res_inst_tac [("xa","M1"),("x","M2")] |
|
324 (standard (induction4 RS mp RS spec RS spec)) 1); |
|
325 by (simp_tac (!simpset addsimps (rules4::(subst_rews@al_rews)) |
|
326 setloop (split_tac [expand_if])) 1); |
|
327 (* 1 *) |
|
328 by (rtac conjI 1); |
|
329 by (my_strip_tac 1); |
|
330 by (R1_tac[subst_Nil] 1); |
|
331 by (REPEAT (rtac exI 1) THEN REPEAT ((rtac conjI THEN' rtac refl) 1)); |
|
332 by (simp_tac (!simpset addsimps [measure_def,inv_image_def,less_eq]) 1); |
|
333 |
|
334 (* 3 *) |
|
335 by (rtac conjI 1); |
|
336 by (my_strip_tac 1); |
|
337 by (rtac (Prim.Rules.CONJUNCT1 var_elimR) 1); |
|
338 by (Simp_tac 1); |
|
339 by (rtac refl 1); |
|
340 |
|
341 (* 4 *) |
|
342 by (rtac conjI 1); |
|
343 by (strip_tac 1); |
|
344 by (rtac (Prim.Rules.CONJUNCT2 var_elimR) 1); |
|
345 by (assume_tac 1); |
|
346 by (rtac refl 1); |
|
347 |
|
348 (* 6 *) |
|
349 by (rtac conjI 1); |
|
350 by (rewrite_tac [symmetric (occs_Comb RS eq_reflection)]); |
|
351 by (my_strip_tac 1); |
|
352 by (rtac (Prim.Rules.CONJUNCT1 var_elimR) 1); |
|
353 by (Asm_simp_tac 1); |
|
354 by (rtac refl 1); |
|
355 |
|
356 (* 7 *) |
|
357 by (REPEAT (rtac allI 1)); |
|
358 by (rtac impI 1); |
|
359 by (etac conjE 1); |
|
360 by (rename_tac "foo bar M1 N1 M2 N2" 1); |
|
361 by (Subst_case_tac [("v","Unify(M1, M2)")]); |
|
362 by (rename_tac "foo bar M1 N1 M2 N2 theta" 1); |
|
363 |
|
364 by (Subst_case_tac [("v","Unify(N1 <| theta, N2 <| theta)")]); |
|
365 by (rename_tac "foo bar M1 N1 M2 N2 theta sigma" 1); |
|
366 by (REPEAT (rtac allI 1)); |
|
367 by (rename_tac "foo bar M1 N1 M2 N2 theta sigma P Q" 1); |
|
368 by (simp_tac (HOL_ss addsimps [subst_comp]) 1); |
|
369 by(rtac(rewrite_rule[trans_def] transR RS spec RS spec RS spec RS mp RS mp) 1); |
|
370 by (fast_tac HOL_cs 1); |
|
371 by (simp_tac (HOL_ss addsimps [symmetric (subst_Comb RS eq_reflection)]) 1); |
|
372 by (subgoal_tac "((Comb N1 P <| theta, Comb N2 Q <| theta), \ |
|
373 \ (Comb M1 (Comb N1 P), Comb M2 (Comb N2 Q))) :R" 1); |
|
374 by (asm_simp_tac HOL_ss 2); |
|
375 |
|
376 by (rtac Rassoc 1); |
|
377 by (assume_tac 1); |
|
378 val Unify_TC2 = result(); |
|
379 |
|
380 |
|
381 (*--------------------------------------------------------------------------- |
|
382 * Now for elimination of nested TC from rules and induction. This step |
|
383 * would be easier if "rewrite_rule" used context. |
|
384 *---------------------------------------------------------------------------*) |
|
385 goal theory |
|
386 "(Unify (Comb M1 N1, Comb M2 N2) = \ |
|
387 \ (case Unify (M1, M2) of Fail => Fail \ |
|
388 \ | Subst theta => \ |
|
389 \ (case if ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R \ |
|
390 \ then Unify (N1 <| theta, N2 <| theta) else @ z. True of \ |
|
391 \ Fail => Fail | Subst sigma => Subst (theta <> sigma)))) \ |
|
392 \ = \ |
|
393 \ (Unify (Comb M1 N1, Comb M2 N2) = \ |
|
394 \ (case Unify (M1, M2) \ |
|
395 \ of Fail => Fail \ |
|
396 \ | Subst theta => (case Unify (N1 <| theta, N2 <| theta) \ |
|
397 \ of Fail => Fail \ |
|
398 \ | Subst sigma => Subst (theta <> sigma))))"; |
|
399 by (cut_inst_tac [("v","Unify(M1, M2)")] |
|
400 (standard (Prim.Rules.SPEC_ALL subst_nchotomy)) 1); |
|
401 by (etac disjE 1); |
|
402 by (Asm_simp_tac 1); |
|
403 by (etac exE 1); |
|
404 by (Asm_simp_tac 1); |
|
405 by (cut_inst_tac |
|
406 [("x","list"), ("xb","N1"), ("xa","N2"),("xc","M2"), ("xd","M1")] |
|
407 (standard(Unify_TC2 RS spec RS spec RS spec RS spec RS spec)) 1); |
|
408 by (Asm_full_simp_tac 1); |
|
409 val Unify_rec_simpl = result() RS eq_reflection; |
|
410 |
|
411 val Unify_rules = rewrite_rule[Unify_rec_simpl] rules4; |
|
412 |
|
413 |
|
414 goal theory |
|
415 "(! M1 N1 M2 N2. \ |
|
416 \ (! theta. \ |
|
417 \ Unify (M1, M2) = Subst theta --> \ |
|
418 \ ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R --> \ |
|
419 \ ?Phi (N1 <| theta) (N2 <| theta)) & ?Phi M1 M2 --> \ |
|
420 \ ?Phi (Comb M1 N1) (Comb M2 N2)) \ |
|
421 \ = \ |
|
422 \ (! M1 N1 M2 N2. \ |
|
423 \ (! theta. \ |
|
424 \ Unify (M1, M2) = Subst theta --> \ |
|
425 \ ?Phi (N1 <| theta) (N2 <| theta)) & ?Phi M1 M2 --> \ |
|
426 \ ?Phi (Comb M1 N1) (Comb M2 N2))"; |
|
427 by (simp_tac (HOL_ss addsimps [Unify_TC2]) 1); |
|
428 val Unify_induction = rewrite_rule[result() RS eq_reflection] induction4; |
|
429 |
|
430 |
|
431 |
|
432 (*--------------------------------------------------------------------------- |
|
433 * Correctness. Notice that idempotence is not needed to prove that the |
|
434 * algorithm terminates and is not needed to prove the algorithm correct, |
|
435 * if you are only interested in an MGU. This is in contrast to the |
|
436 * approach of M&W, who used idempotence and MGU-ness in the termination proof. |
|
437 *---------------------------------------------------------------------------*) |
|
438 |
|
439 goal theory "!theta. Unify (P,Q) = Subst theta --> MGUnifier theta P Q"; |
|
440 by (res_inst_tac [("xa","P"),("x","Q")] |
|
441 (standard (Unify_induction RS mp RS spec RS spec)) 1); |
|
442 by (simp_tac (!simpset addsimps [Unify_rules] |
|
443 setloop (split_tac [expand_if])) 1); |
|
444 (*1*) |
|
445 by (rtac conjI 1); |
|
446 by (REPEAT (rtac allI 1)); |
|
447 by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1); |
|
448 by (my_strip_tac 1); |
|
449 by (rtac MoreGen_Nil 1); |
|
450 |
|
451 (*3*) |
|
452 by (rtac conjI 1); |
|
453 by (my_strip_tac 1); |
|
454 by (rtac (mgu_sym RS iffD1) 1); |
|
455 by (rtac MGUnifier_Var 1); |
|
456 by (Simp_tac 1); |
|
457 |
|
458 (*4*) |
|
459 by (rtac conjI 1); |
|
460 by (my_strip_tac 1); |
|
461 by (rtac MGUnifier_Var 1); |
|
462 by (assume_tac 1); |
|
463 |
|
464 (*6*) |
|
465 by (rtac conjI 1); |
|
466 by (rewrite_tac NNF_rews); |
|
467 by (my_strip_tac 1); |
|
468 by (rtac (mgu_sym RS iffD1) 1); |
|
469 by (rtac MGUnifier_Var 1); |
|
470 by (Asm_simp_tac 1); |
|
471 |
|
472 (*7*) |
|
473 by (safe_tac HOL_cs); |
|
474 by (Subst_case_tac [("v","Unify(M1, M2)")]); |
|
475 by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]); |
|
476 by (hyp_subst_tac 1); |
|
477 by (asm_full_simp_tac(HOL_ss addsimps [MGUnifier_def,Unifier_def])1); |
|
478 by (asm_simp_tac (!simpset addsimps [subst_comp]) 1); (* It's a unifier.*) |
|
479 |
|
480 by (prune_params_tac); |
|
481 by (safe_tac HOL_cs); |
|
482 by (rename_tac "M1 N1 M2 N2 theta sigma gamma" 1); |
|
483 |
|
484 by (rewrite_tac [MoreGeneral_def]); |
|
485 by (rotate_tac ~3 1); |
|
486 by (eres_inst_tac [("x","gamma")] allE 1); |
|
487 by (Asm_full_simp_tac 1); |
|
488 by (etac exE 1); |
|
489 by (rename_tac "M1 N1 M2 N2 theta sigma gamma delta" 1); |
|
490 by (eres_inst_tac [("x","delta")] allE 1); |
|
491 by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1); |
|
492 by (dtac mp 1); |
|
493 by (atac 1); |
|
494 by (etac exE 1); |
|
495 by (rename_tac "M1 N1 M2 N2 theta sigma gamma delta rho" 1); |
|
496 |
|
497 by (rtac exI 1); |
|
498 by (rtac subst_trans 1); |
|
499 by (assume_tac 1); |
|
500 |
|
501 by (rtac subst_trans 1); |
|
502 by (rtac (comp_assoc RS subst_sym) 2); |
|
503 by (rtac subst_cong 1); |
|
504 by (rtac (refl RS subst_refl) 1); |
|
505 by (assume_tac 1); |
|
506 |
|
507 by (asm_full_simp_tac (!simpset addsimps [subst_eq_iff,subst_comp]) 1); |
|
508 by (forw_inst_tac [("x","N1")] spec 1); |
|
509 by (dres_inst_tac [("x","N2")] spec 1); |
|
510 by (Asm_full_simp_tac 1); |
|
511 val Unify_gives_MGU = standard(result() RS spec RS mp); |
|
512 |
|
513 |
|
514 (*--------------------------------------------------------------------------- |
|
515 * Unify returns idempotent substitutions, when it succeeds. |
|
516 *---------------------------------------------------------------------------*) |
|
517 goal theory "!theta. Unify (P,Q) = Subst theta --> Idem theta"; |
|
518 by (res_inst_tac [("xa","P"),("x","Q")] |
|
519 (standard (Unify_induction RS mp RS spec RS spec)) 1); |
|
520 (* Blows away all base cases automatically *) |
|
521 by (simp_tac (!simpset addsimps [Unify_rules,Idem_Nil,Var_Idem] |
|
522 setloop (split_tac [expand_if])) 1); |
|
523 |
|
524 (*7*) |
|
525 by (safe_tac HOL_cs); |
|
526 by (Subst_case_tac [("v","Unify(M1, M2)")]); |
|
527 by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]); |
|
528 by (hyp_subst_tac 1); |
|
529 by prune_params_tac; |
|
530 by (rename_tac "M1 N1 M2 N2 theta sigma" 1); |
|
531 |
|
532 by (dtac Unify_gives_MGU 1); |
|
533 by (dtac Unify_gives_MGU 1); |
|
534 by (rewrite_tac [MGUnifier_def]); |
|
535 by (my_strip_tac 1); |
|
536 by (rtac Idem_comp 1); |
|
537 by (atac 1); |
|
538 by (atac 1); |
|
539 |
|
540 by (my_strip_tac 1); |
|
541 by (eres_inst_tac [("x","q")] allE 1); |
|
542 by (Asm_full_simp_tac 1); |
|
543 by (rewrite_tac [MoreGeneral_def]); |
|
544 by (my_strip_tac 1); |
|
545 by (asm_full_simp_tac(termin_ss addsimps [subst_eq_iff,subst_comp,Idem_def])1); |
|
546 val Unify_gives_Idem = result() RS spec RS mp; |
|
547 |
|
548 |
|
549 |
|
550 (*--------------------------------------------------------------------------- |
|
551 * Exercise. The given algorithm is a bit inelegant. What about the |
|
552 * following "improvement", which adds a few recursive calls in former |
|
553 * base cases? It seems that the termination relation needs another |
|
554 * case in the lexico. product. |
|
555 |
|
556 val {theory,induction,rules,tcs,typechecks} = |
|
557 Rfunc Unify.thy ?? |
|
558 `(Unify(Const m, Const n) = (if (m=n) then Subst[] else Fail)) & |
|
559 (Unify(Const m, Comb M N) = Fail) & |
|
560 (Unify(Const m, Var v) = Unify(Var v, Const m)) & |
|
561 (Unify(Var v, M) = (if (Var v <: M) then Fail else Subst[(v,M)])) & |
|
562 (Unify(Comb M N, Const x) = Fail) & |
|
563 (Unify(Comb M N, Var v) = Unify(Var v, Comb M N)) & |
|
564 (Unify(Comb M1 N1, Comb M2 N2) = |
|
565 (case Unify(M1,M2) |
|
566 of Fail => Fail |
|
567 | Subst theta => (case Unify(N1 <| theta, N2 <| theta) |
|
568 of Fail => Fail |
|
569 | Subst sigma => Subst (theta <> sigma))))`; |
|
570 |
|
571 *---------------------------------------------------------------------------*) |