author | haftmann |
Fri, 12 Jan 2007 09:58:30 +0100 | |
changeset 22061 | 547b0303f37b |
parent 19769 | c40ce2de2020 |
child 23000 | 6f158bba99e4 |
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 |
||
13 |
text{* |
|
15648 | 14 |
Substitution and Unification in Higher-Order Logic. |
15635 | 15 |
|
16 |
Implements Manna and Waldinger's formalization, with Paulson's simplifications, |
|
17 |
and some new simplifications by Slind. |
|
18 |
||
15648 | 19 |
Z Manna and R Waldinger, Deductive Synthesis of the Unification Algorithm. |
15635 | 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: |
|
15648 | 35 |
either the set of variables decreases, |
15635 | 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)]" |
|
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" |
|
94 |
by (simp add: unifyRel_def measure_def trans_inv_image trans_lex_prod |
|
95 |
trans_finite_psubset) |
|
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 ==> |
|
103 |
((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) \<in> unifyRel" |
|
19769
c40ce2de2020
Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
krauss
parents:
19623
diff
changeset
|
104 |
by (simp add: less_eq add_assoc Un_assoc |
15635 | 105 |
unifyRel_def lex_prod_def) |
106 |
||
107 |
||
15648 | 108 |
text{*This lemma proves the nested termination condition for the base cases |
15635 | 109 |
* 3, 4, and 6.*} |
110 |
lemma var_elimR: |
|
15648 | 111 |
"~(Var x \<prec> M) ==> |
112 |
((N1 \<lhd> [(x,M)], N2 \<lhd> [(x,M)]), (Comb M N1, Comb(Var x) N2)) \<in> unifyRel |
|
113 |
& ((N1 \<lhd> [(x,M)], N2 \<lhd> [(x,M)]), (Comb(Var x) N1, Comb M N2)) \<in> unifyRel" |
|
15635 | 114 |
apply (case_tac "Var x = M", clarify, simp) |
15648 | 115 |
apply (case_tac "x \<in> (vars_of N1 Un vars_of N2)") |
15635 | 116 |
txt{*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
|
117 |
apply (simp add: less_eq unifyRel_def lex_prod_def) |
15635 | 118 |
apply blast |
119 |
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
|
120 |
apply (simp add: unifyRel_def lex_prod_def) |
15635 | 121 |
apply (simp add: finite_psubset_def finite_vars_of psubset_def) |
122 |
apply blast |
|
15648 | 123 |
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
|
124 |
apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def) |
15648 | 125 |
apply (cut_tac s = "[(x,M)]" and v = x and t = N2 in Var_elim) |
126 |
apply (cut_tac [3] s = "[(x,M)]" and v = x and t = N1 in Var_elim) |
|
15635 | 127 |
apply (simp_all (no_asm_simp) add: srange_iff vars_iff_occseq) |
128 |
apply (auto elim!: Var_intro [THEN disjE] simp add: srange_iff) |
|
129 |
done |
|
130 |
||
131 |
||
132 |
text{*Eliminate tc1 from the recursion equations and the induction theorem.*} |
|
133 |
||
15648 | 134 |
lemmas unify_nonrec [simp] = |
135 |
unify_CC unify_CB unify_CV unify_V unify_BC unify_BV |
|
15635 | 136 |
|
137 |
lemmas unify_simps0 = unify_nonrec unify_BB [OF unify_tc1] |
|
138 |
||
139 |
lemmas unify_induct0 = unify.induct [OF unify_tc1] |
|
140 |
||
15648 | 141 |
text{*The nested TC. The (2) requests the second one. |
142 |
Proved by recursion induction.*} |
|
143 |
recdef_tc unify_tc2: unify (2) |
|
15635 | 144 |
txt{*The extracted TC needs the scope of its quantifiers adjusted, so our |
145 |
first step is to restrict the scopes of N1 and N2.*} |
|
15648 | 146 |
apply (subgoal_tac "\<forall>M1 M2 theta. unify (M1, M2) = Some theta --> |
147 |
(\<forall>N1 N2.((N1\<lhd>theta, N2\<lhd>theta), (Comb M1 N1, Comb M2 N2)) \<in> unifyRel)") |
|
15635 | 148 |
apply blast |
149 |
apply (rule allI) |
|
150 |
apply (rule allI) |
|
151 |
txt{*Apply induction on this still-quantified formula*} |
|
152 |
apply (rule_tac u = M1 and v = M2 in unify_induct0) |
|
15648 | 153 |
apply (simp_all (no_asm_simp) add: var_elimR unify_simps0) |
154 |
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
|
155 |
apply (simp add: unifyRel_def lex_prod_def less_eq) |
15635 | 156 |
txt{*Comb-Comb case*} |
157 |
apply (simp (no_asm_simp) split add: option.split) |
|
158 |
apply (intro strip) |
|
159 |
apply (rule trans_unifyRel [THEN transD], blast) |
|
160 |
apply (simp only: subst_Comb [symmetric]) |
|
161 |
apply (rule Rassoc, blast) |
|
162 |
done |
|
163 |
||
164 |
||
165 |
text{* Now for elimination of nested TC from unify.simps and induction.*} |
|
166 |
||
167 |
text{*Desired rule, copied from the theory file.*} |
|
168 |
lemma unifyCombComb [simp]: |
|
15648 | 169 |
"unify(Comb M1 N1, Comb M2 N2) = |
170 |
(case unify(M1,M2) |
|
171 |
of None => None |
|
172 |
| Some theta => (case unify(N1 \<lhd> theta, N2 \<lhd> theta) |
|
173 |
of None => None |
|
174 |
| Some sigma => Some (theta \<lozenge> sigma)))" |
|
15635 | 175 |
by (simp add: unify_tc2 unify_simps0 split add: option.split) |
176 |
||
177 |
text{*The ML version had this, but it can't be used: we get |
|
178 |
*** exception THM raised: transfer: not a super theory |
|
179 |
All we can do is state the desired induction rule in full and prove it.*} |
|
180 |
ML{* |
|
181 |
bind_thm ("unify_induct", |
|
182 |
rule_by_tactic |
|
183 |
(ALLGOALS (full_simp_tac (simpset() addsimps [thm"unify_tc2"]))) |
|
184 |
(thm"unify_induct0")); |
|
185 |
*} |
|
186 |
||
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 |