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