author | paulson |
Wed, 05 Nov 1997 13:23:46 +0100 | |
changeset 4153 | e534c4c32d54 |
parent 4089 | 96fba19bcbe2 |
child 4686 | 74a12e86b20b |
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 *) |
|
4089 | 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 *) |
3724 | 47 |
by Safe_tac; |
4089 | 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); |
|
4089 | 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"; |
|
4089 | 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 |
|
4089 | 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 |
|
4089 | 105 |
(simpset() addsimps [unifyRel_def, lex_prod_def, |
3192 | 106 |
measure_def, inv_image_def]) 1); |
4089 | 107 |
by (simp_tac (simpset() addsimps [finite_psubset_def, finite_vars_of, |
3192 | 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 |
|
4089 | 113 |
(simpset() addsimps [finite_vars_of, unifyRel_def, finite_psubset_def, |
3192 | 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); |
|
4089 | 117 |
by (ALLGOALS (asm_simp_tac(simpset() addsimps [srange_iff, vars_iff_occseq]))); |
3192 | 118 |
by (REPEAT_FIRST (resolve_tac [conjI, disjI1, psubsetI])); |
119 |
by (ALLGOALS (asm_full_simp_tac |
|
4089 | 120 |
(simpset() addsimps [srange_iff, set_eq_subset]))); |
3192 | 121 |
by (ALLGOALS |
4089 | 122 |
(fast_tac (claset() addEs [Var_intro RS disjE] |
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 |
*---------------------------------------------------------------------------*) |
3392 | 130 |
val wfr = tc0 RS conjunct1 |
131 |
and tc = tc0 RS conjunct2; |
|
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
132 |
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
|
133 |
unify.rules; |
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
134 |
|
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
135 |
val unifyInduct0 = [wfr,tc] MRS unify.induct; |
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 |
|
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
138 |
(*--------------------------------------------------------------------------- |
3192 | 139 |
* The nested TC. Proved by recursion induction. |
140 |
*---------------------------------------------------------------------------*) |
|
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
141 |
val [_,_,tc3] = unify.tcs; |
3241 | 142 |
goalw_cterm [] (cterm_of (sign_of Unify.thy) (HOLogic.mk_Trueprop tc3)); |
3192 | 143 |
(*--------------------------------------------------------------------------- |
144 |
* The extracted TC needs the scope of its quantifiers adjusted, so our |
|
145 |
* first step is to restrict the scopes of N1 and N2. |
|
146 |
*---------------------------------------------------------------------------*) |
|
147 |
by (subgoal_tac "!M1 M2 theta. \ |
|
3299 | 148 |
\ unify(M1, M2) = Some theta --> \ |
3192 | 149 |
\ (!N1 N2. ((N1<|theta, N2<|theta), Comb M1 N1, Comb M2 N2) : unifyRel)" 1); |
150 |
by (Blast_tac 1); |
|
151 |
by (rtac allI 1); |
|
152 |
by (rtac allI 1); |
|
153 |
(* Apply induction *) |
|
3299 | 154 |
by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1); |
3192 | 155 |
by (ALLGOALS |
4089 | 156 |
(asm_simp_tac (simpset() addsimps (var_elimR::unifyRules0) |
3919 | 157 |
addsplits [expand_if]))); |
3192 | 158 |
(*Const-Const case*) |
159 |
by (simp_tac |
|
4089 | 160 |
(simpset() addsimps [unifyRel_def, lex_prod_def, measure_def, |
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
161 |
inv_image_def, less_eq]) 1); |
3192 | 162 |
(** LEVEL 7 **) |
163 |
(*Comb-Comb case*) |
|
4089 | 164 |
by (asm_simp_tac (simpset() addsplits [split_option_case]) 1); |
3334 | 165 |
by (strip_tac 1); |
3192 | 166 |
by (rtac (trans_unifyRel RS transD) 1); |
167 |
by (Blast_tac 1); |
|
168 |
by (simp_tac (HOL_ss addsimps [subst_Comb RS sym]) 1); |
|
169 |
by (rtac Rassoc 1); |
|
170 |
by (Blast_tac 1); |
|
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
171 |
qed_spec_mp "unify_TC"; |
3192 | 172 |
|
173 |
||
174 |
(*--------------------------------------------------------------------------- |
|
175 |
* Now for elimination of nested TC from unify.rules and induction. |
|
176 |
*---------------------------------------------------------------------------*) |
|
177 |
||
178 |
(*Desired rule, copied from the theory file. Could it be made available?*) |
|
179 |
goal Unify.thy |
|
180 |
"unify(Comb M1 N1, Comb M2 N2) = \ |
|
181 |
\ (case unify(M1,M2) \ |
|
3299 | 182 |
\ of None => None \ |
183 |
\ | Some theta => (case unify(N1 <| theta, N2 <| theta) \ |
|
184 |
\ of None => None \ |
|
185 |
\ | Some sigma => Some (theta <> sigma)))"; |
|
4089 | 186 |
by (asm_simp_tac (simpset() addsimps (unify_TC::unifyRules0) |
4071 | 187 |
addsplits [split_option_case]) 1); |
3192 | 188 |
qed "unifyCombComb"; |
189 |
||
190 |
||
191 |
val unifyRules = rev (unifyCombComb :: tl (rev unifyRules0)); |
|
192 |
||
193 |
Addsimps unifyRules; |
|
194 |
||
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
195 |
bind_thm ("unifyInduct", |
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
196 |
rule_by_tactic |
4089 | 197 |
(ALLGOALS (full_simp_tac (simpset() addsimps [unify_TC]))) |
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
198 |
unifyInduct0); |
3192 | 199 |
|
200 |
||
201 |
(*--------------------------------------------------------------------------- |
|
202 |
* Correctness. Notice that idempotence is not needed to prove that the |
|
203 |
* algorithm terminates and is not needed to prove the algorithm correct, |
|
204 |
* if you are only interested in an MGU. This is in contrast to the |
|
205 |
* approach of M&W, who used idempotence and MGU-ness in the termination proof. |
|
206 |
*---------------------------------------------------------------------------*) |
|
207 |
||
3299 | 208 |
goal Unify.thy "!theta. unify(M,N) = Some theta --> MGUnifier theta M N"; |
209 |
by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1); |
|
4089 | 210 |
by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); |
3192 | 211 |
(*Const-Const case*) |
4089 | 212 |
by (simp_tac (simpset() addsimps [MGUnifier_def,Unifier_def]) 1); |
3192 | 213 |
(*Const-Var case*) |
214 |
by (stac mgu_sym 1); |
|
4089 | 215 |
by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1); |
3192 | 216 |
(*Var-M case*) |
4089 | 217 |
by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1); |
3192 | 218 |
(*Comb-Var case*) |
219 |
by (stac mgu_sym 1); |
|
4089 | 220 |
by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1); |
3334 | 221 |
(** LEVEL 8 **) |
3192 | 222 |
(*Comb-Comb case*) |
4089 | 223 |
by (asm_simp_tac (simpset() addsplits [split_option_case]) 1); |
3334 | 224 |
by (strip_tac 1); |
225 |
by (rotate_tac ~2 1); |
|
226 |
by (asm_full_simp_tac |
|
4089 | 227 |
(simpset() addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1); |
4153 | 228 |
by (Safe_tac THEN rename_tac "theta sigma gamma" 1); |
3334 | 229 |
by (eres_inst_tac [("x","gamma")] allE 1 THEN mp_tac 1); |
230 |
by (etac exE 1 THEN rename_tac "delta" 1); |
|
3192 | 231 |
by (eres_inst_tac [("x","delta")] allE 1); |
232 |
by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1); |
|
233 |
(*Proving the subgoal*) |
|
4089 | 234 |
by (full_simp_tac (simpset() addsimps [subst_eq_iff]) 2 |
235 |
THEN blast_tac (claset() addIs [trans,sym] delrules [impCE]) 2); |
|
236 |
by (blast_tac (claset() addIs [subst_trans, subst_cong, |
|
3192 | 237 |
comp_assoc RS subst_sym]) 1); |
238 |
qed_spec_mp "unify_gives_MGU"; |
|
239 |
||
240 |
||
241 |
(*--------------------------------------------------------------------------- |
|
242 |
* Unify returns idempotent substitutions, when it succeeds. |
|
243 |
*---------------------------------------------------------------------------*) |
|
3299 | 244 |
goal Unify.thy "!theta. unify(M,N) = Some theta --> Idem theta"; |
245 |
by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1); |
|
3334 | 246 |
by (ALLGOALS |
247 |
(asm_simp_tac |
|
4089 | 248 |
(simpset() addsimps [Var_Idem] |
4071 | 249 |
addsplits [expand_if,split_option_case]))); |
3192 | 250 |
(*Comb-Comb case*) |
4153 | 251 |
by Safe_tac; |
3334 | 252 |
by (REPEAT (dtac spec 1 THEN mp_tac 1)); |
4089 | 253 |
by (safe_tac (claset() addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU])); |
3192 | 254 |
by (rtac Idem_comp 1); |
255 |
by (atac 1); |
|
256 |
by (atac 1); |
|
4089 | 257 |
by (best_tac (claset() addss (simpset() addsimps |
3266
89e5f4163663
Removed rprod from the WF relation; simplified proofs;
paulson
parents:
3241
diff
changeset
|
258 |
[MoreGeneral_def, subst_eq_iff, Idem_def])) 1); |
3192 | 259 |
qed_spec_mp "unify_gives_Idem"; |
260 |