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