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