15635
|
1 |
(* ID: $Id$
|
3192
|
2 |
Author: Konrad Slind, Cambridge University Computer Laboratory
|
|
3 |
Copyright 1997 University of Cambridge
|
|
4 |
|
|
5 |
*)
|
|
6 |
|
15635
|
7 |
header{*Unification Algorithm*}
|
|
8 |
|
|
9 |
theory Unify
|
|
10 |
imports Unifier
|
|
11 |
begin
|
|
12 |
|
|
13 |
text{*
|
|
14 |
Substitution and Unification in Higher-Order Logic.
|
|
15 |
|
|
16 |
Implements Manna and Waldinger's formalization, with Paulson's simplifications,
|
|
17 |
and some new simplifications by Slind.
|
|
18 |
|
|
19 |
Z Manna and R Waldinger, Deductive Synthesis of the Unification Algorithm.
|
|
20 |
SCP 1 (1981), 5-48
|
|
21 |
|
|
22 |
L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170
|
|
23 |
*}
|
3192
|
24 |
|
|
25 |
consts
|
|
26 |
|
3267
|
27 |
unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
|
3298
|
28 |
unify :: "'a uterm * 'a uterm => ('a * 'a uterm) list option"
|
3192
|
29 |
|
|
30 |
defs
|
15635
|
31 |
unifyRel_def:
|
|
32 |
"unifyRel == inv_image (finite_psubset <*lex*> measure uterm_size)
|
|
33 |
(%(M,N). (vars_of M Un vars_of N, M))"
|
|
34 |
--{*Termination relation for the Unify function:
|
|
35 |
either the set of variables decreases,
|
|
36 |
or the first argument does (in fact, both do) *}
|
3192
|
37 |
|
15635
|
38 |
text{* Wellfoundedness of unifyRel *}
|
|
39 |
lemma wf_unifyRel [iff]: "wf unifyRel"
|
|
40 |
by (simp add: unifyRel_def wf_lex_prod wf_finite_psubset)
|
3192
|
41 |
|
15635
|
42 |
|
|
43 |
recdef (permissive) unify "unifyRel"
|
|
44 |
unify_CC: "unify(Const m, Const n) = (if (m=n) then Some[] else None)"
|
|
45 |
unify_CB: "unify(Const m, Comb M N) = None"
|
|
46 |
unify_CV: "unify(Const m, Var v) = Some[(v,Const m)]"
|
|
47 |
unify_V: "unify(Var v, M) = (if (Var v <: M) then None else Some[(v,M)])"
|
|
48 |
unify_BC: "unify(Comb M N, Const x) = None"
|
|
49 |
unify_BV: "unify(Comb M N, Var v) = (if (Var v <: Comb M N) then None
|
|
50 |
else Some[(v,Comb M N)])"
|
|
51 |
unify_BB:
|
3192
|
52 |
"unify(Comb M1 N1, Comb M2 N2) =
|
|
53 |
(case unify(M1,M2)
|
3298
|
54 |
of None => None
|
|
55 |
| Some theta => (case unify(N1 <| theta, N2 <| theta)
|
|
56 |
of None => None
|
|
57 |
| Some sigma => Some (theta <> sigma)))"
|
15635
|
58 |
(hints recdef_wf: wf_unifyRel)
|
|
59 |
|
|
60 |
|
|
61 |
|
|
62 |
(*---------------------------------------------------------------------------
|
|
63 |
* This file defines a nested unification algorithm, then proves that it
|
|
64 |
* terminates, then proves 2 correctness theorems: that when the algorithm
|
|
65 |
* succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution.
|
|
66 |
* Although the proofs may seem long, they are actually quite direct, in that
|
|
67 |
* the correctness and termination properties are not mingled as much as in
|
|
68 |
* previous proofs of this algorithm.
|
|
69 |
*
|
|
70 |
* Our approach for nested recursive functions is as follows:
|
|
71 |
*
|
|
72 |
* 0. Prove the wellfoundedness of the termination relation.
|
|
73 |
* 1. Prove the non-nested termination conditions.
|
|
74 |
* 2. Eliminate (0) and (1) from the recursion equations and the
|
|
75 |
* induction theorem.
|
|
76 |
* 3. Prove the nested termination conditions by using the induction
|
|
77 |
* theorem from (2) and by using the recursion equations from (2).
|
|
78 |
* These are constrained by the nested termination conditions, but
|
|
79 |
* things work out magically (by wellfoundedness of the termination
|
|
80 |
* relation).
|
|
81 |
* 4. Eliminate the nested TCs from the results of (2).
|
|
82 |
* 5. Prove further correctness properties using the results of (4).
|
|
83 |
*
|
|
84 |
* Deeper nestings require iteration of steps (3) and (4).
|
|
85 |
*---------------------------------------------------------------------------*)
|
|
86 |
|
|
87 |
text{*The non-nested TC (terminiation condition). This declaration form
|
|
88 |
only seems to return one subgoal outstanding from the recdef.*}
|
|
89 |
recdef_tc unify_tc1: unify
|
|
90 |
apply (simp add: unifyRel_def wf_lex_prod wf_finite_psubset, safe)
|
|
91 |
apply (simp add: finite_psubset_def finite_vars_of lex_prod_def measure_def inv_image_def)
|
|
92 |
apply (rule monotone_vars_of [THEN subset_iff_psubset_eq [THEN iffD1]])
|
|
93 |
done
|
|
94 |
|
|
95 |
|
|
96 |
|
|
97 |
|
|
98 |
text{*Termination proof.*}
|
|
99 |
|
|
100 |
lemma trans_unifyRel: "trans unifyRel"
|
|
101 |
by (simp add: unifyRel_def measure_def trans_inv_image trans_lex_prod
|
|
102 |
trans_finite_psubset)
|
|
103 |
|
|
104 |
|
|
105 |
text{*The following lemma is used in the last step of the termination proof
|
|
106 |
for the nested call in Unify. Loosely, it says that unifyRel doesn't care
|
|
107 |
about term structure.*}
|
|
108 |
lemma Rassoc:
|
|
109 |
"((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel ==>
|
|
110 |
((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel"
|
|
111 |
by (simp add: measure_def less_eq inv_image_def add_assoc Un_assoc
|
|
112 |
unifyRel_def lex_prod_def)
|
|
113 |
|
|
114 |
|
|
115 |
text{*This lemma proves the nested termination condition for the base cases
|
|
116 |
* 3, 4, and 6.*}
|
|
117 |
lemma var_elimR:
|
|
118 |
"~(Var x <: M) ==>
|
|
119 |
((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel
|
|
120 |
& ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel"
|
|
121 |
apply (case_tac "Var x = M", clarify, simp)
|
|
122 |
apply (case_tac "x: (vars_of N1 Un vars_of N2) ")
|
|
123 |
txt{*uterm_less case*}
|
|
124 |
apply (simp add: less_eq unifyRel_def lex_prod_def measure_def inv_image_def)
|
|
125 |
apply blast
|
|
126 |
txt{*@{text finite_psubset} case*}
|
|
127 |
apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def)
|
|
128 |
apply (simp add: finite_psubset_def finite_vars_of psubset_def)
|
|
129 |
apply blast
|
|
130 |
txt{*Final case, also {text finite_psubset}*}
|
|
131 |
apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def measure_def inv_image_def)
|
|
132 |
apply (cut_tac s = "[ (x,M) ]" and v = x and t = N2 in Var_elim)
|
|
133 |
apply (cut_tac [3] s = "[ (x,M) ]" and v = x and t = N1 in Var_elim)
|
|
134 |
apply (simp_all (no_asm_simp) add: srange_iff vars_iff_occseq)
|
|
135 |
apply (auto elim!: Var_intro [THEN disjE] simp add: srange_iff)
|
|
136 |
done
|
|
137 |
|
|
138 |
|
|
139 |
text{*Eliminate tc1 from the recursion equations and the induction theorem.*}
|
|
140 |
|
|
141 |
lemmas unify_nonrec [simp] =
|
|
142 |
unify_CC unify_CB unify_CV unify_V unify_BC unify_BV
|
|
143 |
|
|
144 |
lemmas unify_simps0 = unify_nonrec unify_BB [OF unify_tc1]
|
|
145 |
|
|
146 |
lemmas unify_induct0 = unify.induct [OF unify_tc1]
|
|
147 |
|
|
148 |
text{*The nested TC. Proved by recursion induction.*}
|
|
149 |
lemma unify_tc2:
|
|
150 |
"\<forall>M1 M2 N1 N2 theta.
|
|
151 |
unify (M1, M2) = Some theta \<longrightarrow>
|
|
152 |
((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) \<in> unifyRel"
|
|
153 |
txt{*The extracted TC needs the scope of its quantifiers adjusted, so our
|
|
154 |
first step is to restrict the scopes of N1 and N2.*}
|
|
155 |
apply (subgoal_tac "\<forall>M1 M2 theta. unify (M1, M2) = Some theta -->
|
|
156 |
(\<forall>N1 N2.((N1<|theta, N2<|theta), (Comb M1 N1, Comb M2 N2)) : unifyRel)")
|
|
157 |
apply blast
|
|
158 |
apply (rule allI)
|
|
159 |
apply (rule allI)
|
|
160 |
txt{*Apply induction on this still-quantified formula*}
|
|
161 |
apply (rule_tac u = M1 and v = M2 in unify_induct0)
|
|
162 |
apply (simp_all (no_asm_simp) add: var_elimR unify_simps0)
|
|
163 |
txt{*Const-Const case*}
|
|
164 |
apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def less_eq)
|
|
165 |
txt{*Comb-Comb case*}
|
|
166 |
apply (simp (no_asm_simp) split add: option.split)
|
|
167 |
apply (intro strip)
|
|
168 |
apply (rule trans_unifyRel [THEN transD], blast)
|
|
169 |
apply (simp only: subst_Comb [symmetric])
|
|
170 |
apply (rule Rassoc, blast)
|
|
171 |
done
|
|
172 |
|
|
173 |
|
|
174 |
text{* Now for elimination of nested TC from unify.simps and induction.*}
|
|
175 |
|
|
176 |
text{*Desired rule, copied from the theory file.*}
|
|
177 |
lemma unifyCombComb [simp]:
|
|
178 |
"unify(Comb M1 N1, Comb M2 N2) =
|
|
179 |
(case unify(M1,M2)
|
|
180 |
of None => None
|
|
181 |
| Some theta => (case unify(N1 <| theta, N2 <| theta)
|
|
182 |
of None => None
|
|
183 |
| Some sigma => Some (theta <> sigma)))"
|
|
184 |
by (simp add: unify_tc2 unify_simps0 split add: option.split)
|
|
185 |
|
|
186 |
text{*The ML version had this, but it can't be used: we get
|
|
187 |
*** exception THM raised: transfer: not a super theory
|
|
188 |
All we can do is state the desired induction rule in full and prove it.*}
|
|
189 |
ML{*
|
|
190 |
bind_thm ("unify_induct",
|
|
191 |
rule_by_tactic
|
|
192 |
(ALLGOALS (full_simp_tac (simpset() addsimps [thm"unify_tc2"])))
|
|
193 |
(thm"unify_induct0"));
|
|
194 |
*}
|
|
195 |
|
|
196 |
|
|
197 |
text{*Correctness. Notice that idempotence is not needed to prove that the
|
|
198 |
algorithm terminates and is not needed to prove the algorithm correct, if you
|
|
199 |
are only interested in an MGU. This is in contrast to the approach of M&W,
|
|
200 |
who used idempotence and MGU-ness in the termination proof.*}
|
|
201 |
|
|
202 |
theorem unify_gives_MGU [rule_format]:
|
|
203 |
"\<forall>theta. unify(M,N) = Some theta --> MGUnifier theta M N"
|
|
204 |
apply (rule_tac u = M and v = N in unify_induct0)
|
|
205 |
apply (simp_all (no_asm_simp))
|
|
206 |
(*Const-Const case*)
|
|
207 |
apply (simp (no_asm) add: MGUnifier_def Unifier_def)
|
|
208 |
(*Const-Var case*)
|
|
209 |
apply (subst mgu_sym)
|
|
210 |
apply (simp (no_asm) add: MGUnifier_Var)
|
|
211 |
(*Var-M case*)
|
|
212 |
apply (simp (no_asm) add: MGUnifier_Var)
|
|
213 |
(*Comb-Var case*)
|
|
214 |
apply (subst mgu_sym)
|
|
215 |
apply (simp (no_asm) add: MGUnifier_Var)
|
|
216 |
(** LEVEL 8 **)
|
|
217 |
(*Comb-Comb case*)
|
|
218 |
apply (simp add: unify_tc2)
|
|
219 |
apply (simp (no_asm_simp) split add: option.split)
|
|
220 |
apply (intro strip)
|
|
221 |
apply (simp add: MGUnifier_def Unifier_def MoreGeneral_def)
|
|
222 |
apply (safe, rename_tac theta sigma gamma)
|
|
223 |
apply (erule_tac x = gamma in allE, erule (1) notE impE)
|
|
224 |
apply (erule exE, rename_tac delta)
|
|
225 |
apply (erule_tac x = delta in allE)
|
|
226 |
apply (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta")
|
|
227 |
apply (blast intro: subst_trans intro!: subst_cong comp_assoc[THEN subst_sym])
|
|
228 |
apply (simp add: subst_eq_iff)
|
|
229 |
done
|
|
230 |
|
|
231 |
|
|
232 |
text{*Unify returns idempotent substitutions, when it succeeds.*}
|
|
233 |
theorem unify_gives_Idem [rule_format]:
|
|
234 |
"\<forall>theta. unify(M,N) = Some theta --> Idem theta"
|
|
235 |
apply (rule_tac u = M and v = N in unify_induct0)
|
|
236 |
apply (simp_all add: Var_Idem unify_tc2 split add: option.split)
|
|
237 |
txt{*Comb-Comb case*}
|
|
238 |
apply safe
|
|
239 |
apply (drule spec, erule (1) notE impE)+
|
|
240 |
apply (safe dest!: unify_gives_MGU [unfolded MGUnifier_def])
|
|
241 |
apply (rule Idem_comp, assumption+)
|
|
242 |
apply (force simp add: MoreGeneral_def subst_eq_iff Idem_def)
|
|
243 |
done
|
|
244 |
|
3192
|
245 |
end
|