author | paulson |
Thu, 22 May 1997 15:10:59 +0200 | |
changeset 3299 | 8adf24153732 |
parent 3266 | 89e5f4163663 |
child 3334 | ec558598ee1d |
permissions | -rw-r--r-- |
3192 | 1 |
(* Title: Subst/Unify |
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
2 |
ID: $Id$ |
3192 | 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 |
open Unify; |
|
35 |
||
36 |
||
37 |
||
38 |
(*--------------------------------------------------------------------------- |
|
39 |
* The non-nested TC plus the wellfoundedness of unifyRel. |
|
40 |
*---------------------------------------------------------------------------*) |
|
41 |
Tfl.tgoalw Unify.thy [] unify.rules; |
|
42 |
(* Wellfoundedness of unifyRel *) |
|
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
43 |
by (simp_tac (!simpset addsimps [unifyRel_def, |
3192 | 44 |
wf_inv_image, wf_lex_prod, wf_finite_psubset, |
3299 | 45 |
wf_measure]) 1); |
3192 | 46 |
(* TC *) |
47 |
by (Step_tac 1); |
|
48 |
by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of, |
|
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
49 |
lex_prod_def, measure_def, inv_image_def]) 1); |
3192 | 50 |
by (rtac (monotone_vars_of RS (subset_iff_psubset_eq RS iffD1) RS disjE) 1); |
51 |
by (Blast_tac 1); |
|
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
52 |
by (asm_simp_tac (!simpset addsimps [less_eq, less_add_Suc1]) 1); |
3192 | 53 |
qed "tc0"; |
54 |
||
55 |
||
56 |
(*--------------------------------------------------------------------------- |
|
57 |
* Termination proof. |
|
58 |
*---------------------------------------------------------------------------*) |
|
59 |
||
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
60 |
goalw Unify.thy [unifyRel_def, measure_def] "trans unifyRel"; |
3241 | 61 |
by (REPEAT (resolve_tac [trans_inv_image, trans_lex_prod, |
62 |
trans_finite_psubset, trans_less_than, |
|
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
63 |
trans_inv_image] 1)); |
3192 | 64 |
qed "trans_unifyRel"; |
65 |
||
66 |
||
67 |
(*--------------------------------------------------------------------------- |
|
68 |
* The following lemma is used in the last step of the termination proof for |
|
69 |
* the nested call in Unify. Loosely, it says that unifyRel doesn't care |
|
70 |
* about term structure. |
|
71 |
*---------------------------------------------------------------------------*) |
|
72 |
goalw Unify.thy [unifyRel_def,lex_prod_def, inv_image_def] |
|
73 |
"!!x. ((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel ==> \ |
|
74 |
\ ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel"; |
|
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
75 |
by (asm_full_simp_tac (!simpset addsimps [measure_def, |
3192 | 76 |
less_eq, inv_image_def,add_assoc]) 1); |
77 |
by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \ |
|
78 |
\ (vars_of D Un vars_of E Un vars_of F)) = \ |
|
79 |
\ (vars_of A Un (vars_of B Un vars_of C) Un \ |
|
80 |
\ (vars_of D Un (vars_of E Un vars_of F)))" 1); |
|
81 |
by (Blast_tac 2); |
|
82 |
by (Asm_simp_tac 1); |
|
83 |
qed "Rassoc"; |
|
84 |
||
85 |
||
86 |
(*--------------------------------------------------------------------------- |
|
87 |
* This lemma proves the nested termination condition for the base cases |
|
88 |
* 3, 4, and 6. |
|
89 |
*---------------------------------------------------------------------------*) |
|
90 |
goal Unify.thy |
|
91 |
"!!x. ~(Var x <: M) ==> \ |
|
92 |
\ ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel \ |
|
93 |
\ & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel"; |
|
94 |
by (case_tac "Var x = M" 1); |
|
95 |
by (hyp_subst_tac 1); |
|
96 |
by (Simp_tac 1); |
|
97 |
by (case_tac "x: (vars_of N1 Un vars_of N2)" 1); |
|
98 |
(*uterm_less case*) |
|
99 |
by (asm_simp_tac |
|
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
100 |
(!simpset addsimps [less_eq, unifyRel_def, lex_prod_def, |
3192 | 101 |
measure_def, inv_image_def]) 1); |
102 |
by (Blast_tac 1); |
|
103 |
(*finite_psubset case*) |
|
104 |
by (simp_tac |
|
105 |
(!simpset addsimps [unifyRel_def, lex_prod_def, |
|
106 |
measure_def, inv_image_def]) 1); |
|
107 |
by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of, |
|
108 |
psubset_def, set_eq_subset]) 1); |
|
109 |
by (Blast_tac 1); |
|
110 |
(** LEVEL 9 **) |
|
111 |
(*Final case, also finite_psubset*) |
|
112 |
by (simp_tac |
|
113 |
(!simpset addsimps [finite_vars_of, unifyRel_def, finite_psubset_def, |
|
114 |
lex_prod_def, measure_def, inv_image_def]) 1); |
|
115 |
by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N2")] Var_elim 1); |
|
116 |
by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N1")] Var_elim 3); |
|
117 |
by (ALLGOALS (asm_simp_tac(!simpset addsimps [srange_iff, vars_iff_occseq]))); |
|
118 |
by (REPEAT_FIRST (resolve_tac [conjI, disjI1, psubsetI])); |
|
119 |
by (ALLGOALS (asm_full_simp_tac |
|
120 |
(!simpset addsimps [srange_iff, set_eq_subset]))); |
|
121 |
by (ALLGOALS |
|
122 |
(fast_tac (!claset addEs [Var_intro RS disjE] |
|
3209 | 123 |
addss (!simpset addsimps [srange_iff])))); |
3192 | 124 |
qed "var_elimR"; |
125 |
||
126 |
||
127 |
(*--------------------------------------------------------------------------- |
|
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
128 |
* Eliminate tc0 from the recursion equations and the induction theorem. |
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
129 |
*---------------------------------------------------------------------------*) |
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
130 |
val [wfr,tc] = Prim.Rules.CONJUNCTS tc0; |
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
131 |
val unifyRules0 = map (normalize_thm [fn th => wfr RS th, fn th => tc RS th]) |
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
132 |
unify.rules; |
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
133 |
|
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
134 |
val unifyInduct0 = [wfr,tc] MRS unify.induct; |
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
135 |
|
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
136 |
|
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
137 |
(*--------------------------------------------------------------------------- |
3192 | 138 |
* The nested TC. Proved by recursion induction. |
139 |
*---------------------------------------------------------------------------*) |
|
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
140 |
val [_,_,tc3] = unify.tcs; |
3241 | 141 |
goalw_cterm [] (cterm_of (sign_of Unify.thy) (HOLogic.mk_Trueprop tc3)); |
3192 | 142 |
(*--------------------------------------------------------------------------- |
143 |
* The extracted TC needs the scope of its quantifiers adjusted, so our |
|
144 |
* first step is to restrict the scopes of N1 and N2. |
|
145 |
*---------------------------------------------------------------------------*) |
|
146 |
by (subgoal_tac "!M1 M2 theta. \ |
|
3299 | 147 |
\ unify(M1, M2) = Some theta --> \ |
3192 | 148 |
\ (!N1 N2. ((N1<|theta, N2<|theta), Comb M1 N1, Comb M2 N2) : unifyRel)" 1); |
149 |
by (Blast_tac 1); |
|
150 |
by (rtac allI 1); |
|
151 |
by (rtac allI 1); |
|
152 |
(* Apply induction *) |
|
3299 | 153 |
by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1); |
3192 | 154 |
by (ALLGOALS |
155 |
(asm_simp_tac (!simpset addsimps (var_elimR::unifyRules0) |
|
156 |
setloop (split_tac [expand_if])))); |
|
157 |
(*Const-Const case*) |
|
158 |
by (simp_tac |
|
159 |
(!simpset addsimps [unifyRel_def, lex_prod_def, measure_def, |
|
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
160 |
inv_image_def, less_eq]) 1); |
3192 | 161 |
(** LEVEL 7 **) |
162 |
(*Comb-Comb case*) |
|
3299 | 163 |
by (option_case_tac "unify(M1a, M2a)" 1); |
3192 | 164 |
by (rename_tac "theta" 1); |
3299 | 165 |
by (option_case_tac "unify(N1 <| theta, N2 <| theta)" 1); |
3192 | 166 |
by (rename_tac "sigma" 1); |
167 |
by (REPEAT (rtac allI 1)); |
|
168 |
by (rename_tac "P Q" 1); |
|
169 |
by (rtac (trans_unifyRel RS transD) 1); |
|
170 |
by (Blast_tac 1); |
|
171 |
by (simp_tac (HOL_ss addsimps [subst_Comb RS sym]) 1); |
|
172 |
by (subgoal_tac "((Comb N1 P <| theta, Comb N2 Q <| theta), \ |
|
173 |
\ (Comb M1a (Comb N1 P), Comb M2a (Comb N2 Q))) :unifyRel" 1); |
|
174 |
by (asm_simp_tac HOL_ss 2); |
|
175 |
by (rtac Rassoc 1); |
|
176 |
by (Blast_tac 1); |
|
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
177 |
qed_spec_mp "unify_TC"; |
3192 | 178 |
|
179 |
||
180 |
(*--------------------------------------------------------------------------- |
|
181 |
* Now for elimination of nested TC from unify.rules and induction. |
|
182 |
*---------------------------------------------------------------------------*) |
|
183 |
||
184 |
(*Desired rule, copied from the theory file. Could it be made available?*) |
|
185 |
goal Unify.thy |
|
186 |
"unify(Comb M1 N1, Comb M2 N2) = \ |
|
187 |
\ (case unify(M1,M2) \ |
|
3299 | 188 |
\ of None => None \ |
189 |
\ | Some theta => (case unify(N1 <| theta, N2 <| theta) \ |
|
190 |
\ of None => None \ |
|
191 |
\ | Some sigma => Some (theta <> sigma)))"; |
|
3192 | 192 |
by (asm_simp_tac (!simpset addsimps unifyRules0) 1); |
3299 | 193 |
by (option_case_tac "unify(M1, M2)" 1); |
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
194 |
by (asm_simp_tac (!simpset addsimps [unify_TC]) 1); |
3192 | 195 |
qed "unifyCombComb"; |
196 |
||
197 |
||
198 |
val unifyRules = rev (unifyCombComb :: tl (rev unifyRules0)); |
|
199 |
||
200 |
Addsimps unifyRules; |
|
201 |
||
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
202 |
bind_thm ("unifyInduct", |
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
203 |
rule_by_tactic |
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
204 |
(ALLGOALS (full_simp_tac (!simpset addsimps [unify_TC]))) |
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
205 |
unifyInduct0); |
3192 | 206 |
|
207 |
||
208 |
(*--------------------------------------------------------------------------- |
|
209 |
* Correctness. Notice that idempotence is not needed to prove that the |
|
210 |
* algorithm terminates and is not needed to prove the algorithm correct, |
|
211 |
* if you are only interested in an MGU. This is in contrast to the |
|
212 |
* approach of M&W, who used idempotence and MGU-ness in the termination proof. |
|
213 |
*---------------------------------------------------------------------------*) |
|
214 |
||
3299 | 215 |
goal Unify.thy "!theta. unify(M,N) = Some theta --> MGUnifier theta M N"; |
216 |
by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1); |
|
3192 | 217 |
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]))); |
218 |
(*Const-Const case*) |
|
219 |
by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1); |
|
220 |
(*Const-Var case*) |
|
221 |
by (stac mgu_sym 1); |
|
222 |
by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1); |
|
223 |
(*Var-M case*) |
|
224 |
by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1); |
|
225 |
(*Comb-Var case*) |
|
226 |
by (stac mgu_sym 1); |
|
227 |
by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1); |
|
228 |
(*Comb-Comb case*) |
|
229 |
by (safe_tac (!claset)); |
|
3299 | 230 |
by (option_case_tac "unify(M1, M2)" 1); |
231 |
by (option_case_tac "unify(N1 <| a, N2 <| a)" 1); |
|
3192 | 232 |
by (hyp_subst_tac 1); |
233 |
by (asm_full_simp_tac (!simpset addsimps [MGUnifier_def, Unifier_def])1); |
|
234 |
(** LEVEL 13 **) |
|
235 |
by (safe_tac (!claset)); |
|
236 |
by (rename_tac "theta sigma gamma" 1); |
|
237 |
by (rewrite_goals_tac [MoreGeneral_def]); |
|
238 |
by (rotate_tac ~3 1); |
|
239 |
by (eres_inst_tac [("x","gamma")] allE 1); |
|
240 |
by (Asm_full_simp_tac 1); |
|
241 |
by (etac exE 1); |
|
242 |
by (rename_tac "delta" 1); |
|
243 |
by (eres_inst_tac [("x","delta")] allE 1); |
|
244 |
by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1); |
|
245 |
(*Proving the subgoal*) |
|
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
246 |
by (full_simp_tac (!simpset addsimps [subst_eq_iff]) 2 |
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
247 |
THEN blast_tac (!claset addIs [trans,sym] delrules [impCE]) 2); |
3192 | 248 |
by (blast_tac (!claset addIs [subst_trans, subst_cong, |
249 |
comp_assoc RS subst_sym]) 1); |
|
250 |
qed_spec_mp "unify_gives_MGU"; |
|
251 |
||
252 |
||
253 |
(*--------------------------------------------------------------------------- |
|
254 |
* Unify returns idempotent substitutions, when it succeeds. |
|
255 |
*---------------------------------------------------------------------------*) |
|
3299 | 256 |
goal Unify.thy "!theta. unify(M,N) = Some theta --> Idem theta"; |
257 |
by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1); |
|
3192 | 258 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Var_Idem] |
259 |
setloop split_tac[expand_if]))); |
|
260 |
(*Comb-Comb case*) |
|
261 |
by (safe_tac (!claset)); |
|
3299 | 262 |
by (option_case_tac "unify(M1, M2)" 1); |
263 |
by (option_case_tac "unify(N1 <| a, N2 <| a)" 1); |
|
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
264 |
by (safe_tac (!claset addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU])); |
3192 | 265 |
by (rtac Idem_comp 1); |
266 |
by (atac 1); |
|
267 |
by (atac 1); |
|
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
268 |
by (best_tac (!claset addss (!simpset addsimps |
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
269 |
[MoreGeneral_def, subst_eq_iff, Idem_def])) 1); |
3192 | 270 |
qed_spec_mp "unify_gives_Idem"; |
271 |