author | clasohm |
Tue, 24 Oct 1995 14:59:17 +0100 | |
changeset 251 | f04b33ce250f |
parent 194 | b93cc55cb7ab |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: Substitutions/unifier.ML |
2 |
Author: Martin Coen, Cambridge University Computer Laboratory |
|
3 |
Copyright 1993 University of Cambridge |
|
4 |
||
5 |
For unifier.thy. |
|
6 |
Properties of unifiers. |
|
7 |
Cases for partial correctness of algorithm and conditions for termination. |
|
8 |
*) |
|
9 |
||
10 |
open Unifier; |
|
11 |
||
12 |
val unify_defs = |
|
13 |
[Idem_def,Unifier_def,MoreGeneral_def,MGUnifier_def,MGIUnifier_def]; |
|
14 |
||
15 |
(**** Unifiers ****) |
|
16 |
||
17 |
goalw Unifier.thy [Unifier_def] "Unifier(s,t,u) = (t <| s = u <| s)"; |
|
18 |
by (rtac refl 1); |
|
171 | 19 |
qed "Unifier_iff"; |
0 | 20 |
|
21 |
goal Unifier.thy |
|
22 |
"Unifier(s,Comb(t,u),Comb(v,w)) --> Unifier(s,t,v) & Unifier(s,u,w)"; |
|
23 |
by (simp_tac (subst_ss addsimps [Unifier_iff]) 1); |
|
171 | 24 |
val Unifier_Comb = store_thm("Unifier_Comb", result() RS mp RS conjE); |
0 | 25 |
|
26 |
goal Unifier.thy |
|
27 |
"~v : vars_of(t) --> ~v : vars_of(u) -->Unifier(s,t,u) --> \ |
|
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
28 |
\ Unifier(<v,r>#s,t,u)"; |
0 | 29 |
by (simp_tac (subst_ss addsimps [Unifier_iff,repl_invariance]) 1); |
171 | 30 |
val Cons_Unifier = store_thm("Cons_Unifier", result() RS mp RS mp RS mp); |
0 | 31 |
|
32 |
(**** Most General Unifiers ****) |
|
33 |
||
34 |
goalw Unifier.thy [MoreGeneral_def] "r >> s = (EX q. s =s= r <> q)"; |
|
35 |
by (rtac refl 1); |
|
171 | 36 |
qed "MoreGen_iff"; |
0 | 37 |
|
194
b93cc55cb7ab
small updates because datatype list is now used. In particular Nil -> []
nipkow
parents:
171
diff
changeset
|
38 |
goal Unifier.thy "[] >> s"; |
0 | 39 |
by (simp_tac (subst_ss addsimps [MoreGen_iff]) 1); |
40 |
by (fast_tac (set_cs addIs [refl RS subst_refl]) 1); |
|
171 | 41 |
qed "MoreGen_Nil"; |
0 | 42 |
|
43 |
goalw Unifier.thy unify_defs |
|
44 |
"MGUnifier(s,t,u) = (ALL r.Unifier(r,t,u) = s >> r)"; |
|
45 |
by (REPEAT (ares_tac [iffI,allI] 1 ORELSE |
|
46 |
eresolve_tac [conjE,allE,mp,exE,ssubst_subst2] 1)); |
|
47 |
by (asm_simp_tac (subst_ss addsimps [subst_comp]) 1); |
|
48 |
by (fast_tac (set_cs addIs [comp_Nil RS sym RS subst_refl]) 1); |
|
171 | 49 |
qed "MGU_iff"; |
0 | 50 |
|
51 |
val [prem] = goal Unifier.thy |
|
194
b93cc55cb7ab
small updates because datatype list is now used. In particular Nil -> []
nipkow
parents:
171
diff
changeset
|
52 |
"~ Var(v) <: t ==> MGUnifier([<v,t>],Var(v),t)"; |
0 | 53 |
by (simp_tac (subst_ss addsimps [MGU_iff,MoreGen_iff,Unifier_iff]) 1); |
54 |
by (REPEAT_SOME (step_tac set_cs)); |
|
55 |
by (etac subst 1); |
|
56 |
by (etac ssubst_subst2 2); |
|
57 |
by (rtac (Cons_trivial RS subst_sym) 1); |
|
58 |
by (simp_tac (subst_ss addsimps [prem RS Var_not_occs,Var_subst]) 1); |
|
171 | 59 |
qed "MGUnifier_Var"; |
0 | 60 |
|
61 |
(**** Most General Idempotent Unifiers ****) |
|
62 |
||
63 |
goal Unifier.thy "r <> r =s= r --> s =s= r <> q --> r <> s =s= s"; |
|
64 |
by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1); |
|
171 | 65 |
val MGIU_iff_lemma = store_thm("MGIU_iff_lemma", result() RS mp RS mp); |
0 | 66 |
|
67 |
goalw Unifier.thy unify_defs |
|
68 |
"MGIUnifier(s,t,u) = \ |
|
69 |
\ (Idem(s) & Unifier(s,t,u) & (ALL r.Unifier(r,t,u) --> s<>r=s=r))"; |
|
70 |
by (fast_tac (set_cs addEs [subst_sym,MGIU_iff_lemma]) 1); |
|
171 | 71 |
qed "MGIU_iff"; |
0 | 72 |
|
73 |
(**** Idempotence ****) |
|
74 |
||
75 |
goalw Unifier.thy unify_defs "Idem(s) = (s <> s =s= s)"; |
|
76 |
by (rtac refl 1); |
|
171 | 77 |
qed "raw_Idem_iff"; |
0 | 78 |
|
79 |
goal Unifier.thy "Idem(s) = (sdom(s) Int srange(s) = {})"; |
|
80 |
by (simp_tac (subst_ss addsimps [raw_Idem_iff,subst_eq_iff,subst_comp, |
|
81 |
invariance,dom_range_disjoint])1); |
|
171 | 82 |
qed "Idem_iff"; |
0 | 83 |
|
194
b93cc55cb7ab
small updates because datatype list is now used. In particular Nil -> []
nipkow
parents:
171
diff
changeset
|
84 |
goal Unifier.thy "Idem([])"; |
0 | 85 |
by (simp_tac (subst_ss addsimps [raw_Idem_iff,refl RS subst_refl]) 1); |
171 | 86 |
qed "Idem_Nil"; |
0 | 87 |
|
194
b93cc55cb7ab
small updates because datatype list is now used. In particular Nil -> []
nipkow
parents:
171
diff
changeset
|
88 |
goal Unifier.thy "~ (Var(v) <: t) --> Idem([<v,t>])"; |
0 | 89 |
by (simp_tac (subst_ss addsimps [Var_subst,vars_iff_occseq,Idem_iff,srange_iff] |
90 |
setloop (split_tac [expand_if])) 1); |
|
91 |
by (fast_tac set_cs 1); |
|
171 | 92 |
val Var_Idem = store_thm("Var_Idem", result() RS mp); |
0 | 93 |
|
94 |
val [prem] = goalw Unifier.thy [Idem_def] |
|
95 |
"Idem(r) ==> Unifier(s,t <| r,u <| r) --> Unifier(r <> s,t <| r,u <| r)"; |
|
96 |
by (simp_tac (subst_ss addsimps |
|
97 |
[Unifier_iff,subst_comp,prem RS comp_subst_subst]) 1); |
|
171 | 98 |
val Unifier_Idem_subst = store_thm("Unifier_Idem_subst", result() RS mp); |
0 | 99 |
|
100 |
val [prem] = goal Unifier.thy |
|
101 |
"r <> s =s= s ==> Unifier(s,t,u) --> Unifier(s,t <| r,u <| r)"; |
|
102 |
by (simp_tac (subst_ss addsimps |
|
103 |
[Unifier_iff,subst_comp,prem RS comp_subst_subst]) 1); |
|
171 | 104 |
val Unifier_comp_subst = store_thm("Unifier_comp_subst", result() RS mp); |
0 | 105 |
|
106 |
(*** The domain of a MGIU is a subset of the variables in the terms ***) |
|
107 |
(*** NB this and one for range are only needed for termination ***) |
|
108 |
||
109 |
val [prem] = goal Unifier.thy |
|
110 |
"~ vars_of(Var(x) <| r) = vars_of(Var(x) <| s) ==> ~r =s= s"; |
|
111 |
by (rtac (prem RS contrapos) 1); |
|
112 |
by (fast_tac (set_cs addEs [subst_subst2]) 1); |
|
171 | 113 |
qed "lemma_lemma"; |
0 | 114 |
|
115 |
val prems = goal Unifier.thy |
|
116 |
"x : sdom(s) --> ~x : srange(s) --> \ |
|
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
117 |
\ ~vars_of(Var(x) <| s<> <x,Var(x)>#s) = \ |
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
118 |
\ vars_of(Var(x) <| <x,Var(x)>#s)"; |
0 | 119 |
by (simp_tac (subst_ss addsimps [not_equal_iff]) 1); |
120 |
by (REPEAT (resolve_tac [impI,disjI2] 1)); |
|
121 |
by(res_inst_tac [("x","x")] exI 1); |
|
122 |
br conjI 1; |
|
123 |
by (asm_simp_tac (subst_ss addsimps [Var_elim,subst_comp,repl_invariance]) 1); |
|
124 |
by (asm_simp_tac (subst_ss addsimps [Var_subst]) 1); |
|
171 | 125 |
val MGIU_sdom_lemma = store_thm("MGIU_sdom_lemma", result() RS mp RS mp RS lemma_lemma RS notE); |
0 | 126 |
|
127 |
goal Unifier.thy "MGIUnifier(s,t,u) --> sdom(s) <= vars_of(t) Un vars_of(u)"; |
|
128 |
by (subgoal_tac "! P Q.(P | Q) = (~( ~P & ~Q))" 1); |
|
129 |
by (asm_simp_tac (subst_ss addsimps [MGIU_iff,Idem_iff,subset_iff]) 1); |
|
130 |
by (safe_tac set_cs); |
|
131 |
by (eresolve_tac ([spec] RL [impE]) 1); |
|
132 |
by (rtac Cons_Unifier 1); |
|
133 |
by (ALLGOALS (fast_tac (set_cs addIs [Cons_Unifier,MGIU_sdom_lemma]))); |
|
171 | 134 |
val MGIU_sdom = store_thm("MGIU_sdom", result() RS mp); |
0 | 135 |
|
136 |
(*** The range of a MGIU is a subset of the variables in the terms ***) |
|
137 |
||
138 |
val prems = goal HOL.thy "P = Q ==> (~P) = (~Q)"; |
|
139 |
by (simp_tac (set_ss addsimps prems) 1); |
|
171 | 140 |
qed "not_cong"; |
0 | 141 |
|
142 |
val prems = goal Unifier.thy |
|
143 |
"~w=x --> x : vars_of(Var(w) <| s) --> w : sdom(s) --> ~w : srange(s) --> \ |
|
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
144 |
\ ~vars_of(Var(w) <| s<> <x,Var(w)>#s) = \ |
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
145 |
\ vars_of(Var(w) <| <x,Var(w)>#s)"; |
0 | 146 |
by (simp_tac (subst_ss addsimps [not_equal_iff]) 1); |
147 |
by (REPEAT (resolve_tac [impI,disjI1] 1)); |
|
148 |
by(res_inst_tac [("x","w")] exI 1); |
|
149 |
by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_elim,subst_comp, |
|
150 |
vars_var_iff RS not_cong RS iffD2 RS repl_invariance]) )); |
|
151 |
by (fast_tac (set_cs addIs [Var_in_subst]) 1); |
|
171 | 152 |
val MGIU_srange_lemma = store_thm("MGIU_srange_lemma", result() RS mp RS mp RS mp RS mp RS lemma_lemma RS notE); |
0 | 153 |
|
154 |
goal Unifier.thy "MGIUnifier(s,t,u) --> srange(s) <= vars_of(t) Un vars_of(u)"; |
|
155 |
by (subgoal_tac "! P Q.(P | Q) = (~( ~P & ~Q))" 1); |
|
156 |
by (asm_simp_tac (subst_ss addsimps [MGIU_iff,srange_iff,subset_iff]) 1); |
|
157 |
by (simp_tac (subst_ss addsimps [Idem_iff]) 1); |
|
158 |
by (safe_tac set_cs); |
|
159 |
by (eresolve_tac ([spec] RL [impE]) 1); |
|
160 |
by (rtac Cons_Unifier 1); |
|
161 |
by (imp_excluded_middle_tac "w=ta" 4); |
|
162 |
by (fast_tac (set_cs addEs [MGIU_srange_lemma]) 5); |
|
163 |
by (ALLGOALS (fast_tac (set_cs addIs [Var_elim2]))); |
|
171 | 164 |
val MGIU_srange = store_thm("MGIU_srange", result() RS mp); |
0 | 165 |
|
166 |
(*************** Correctness of a simple unification algorithm ***************) |
|
167 |
(* *) |
|
168 |
(* fun unify Const(m) Const(n) = if m=n then Nil else Fail *) |
|
169 |
(* | unify Const(m) _ = Fail *) |
|
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
170 |
(* | unify Var(v) t = if Var(v)<:t then Fail else <v,t>#Nil *) |
0 | 171 |
(* | unify Comb(t,u) Const(n) = Fail *) |
172 |
(* | unify Comb(t,u) Var(v) = if Var(v) <: Comb(t,u) then Fail *) |
|
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
173 |
(* else <v,Comb(t,u>#Nil *) |
0 | 174 |
(* | unify Comb(t,u) Comb(v,w) = let s = unify t v *) |
175 |
(* in if s=Fail then Fail *) |
|
176 |
(* else unify (u<|s) (w<|s); *) |
|
177 |
||
178 |
(**** Cases for the partial correctness of the algorithm ****) |
|
179 |
||
180 |
goalw Unifier.thy unify_defs "MGIUnifier(s,t,u) = MGIUnifier(s,u,t)"; |
|
181 |
by (safe_tac (HOL_cs addSEs ([sym]@([spec] RL [mp])))); |
|
171 | 182 |
qed "Unify_comm"; |
0 | 183 |
|
194
b93cc55cb7ab
small updates because datatype list is now used. In particular Nil -> []
nipkow
parents:
171
diff
changeset
|
184 |
goal Unifier.thy "MGIUnifier([],Const(n),Const(n))"; |
0 | 185 |
by (simp_tac (subst_ss addsimps |
186 |
[MGIU_iff,MGU_iff,Unifier_iff,subst_eq_iff,Idem_Nil]) 1); |
|
171 | 187 |
qed "Unify1"; |
0 | 188 |
|
189 |
goal Unifier.thy "~m=n --> (ALL l.~Unifier(l,Const(m),Const(n)))"; |
|
190 |
by (simp_tac (subst_ss addsimps[Unifier_iff]) 1); |
|
171 | 191 |
val Unify2 = store_thm("Unify2", result() RS mp); |
0 | 192 |
|
193 |
val [prem] = goalw Unifier.thy [MGIUnifier_def] |
|
194
b93cc55cb7ab
small updates because datatype list is now used. In particular Nil -> []
nipkow
parents:
171
diff
changeset
|
194 |
"~Var(v) <: t ==> MGIUnifier([<v,t>],Var(v),t)"; |
0 | 195 |
by (fast_tac (HOL_cs addSIs [prem RS MGUnifier_Var,prem RS Var_Idem]) 1); |
171 | 196 |
qed "Unify3"; |
0 | 197 |
|
198 |
val [prem] = goal Unifier.thy "Var(v) <: t ==> (ALL l.~Unifier(l,Var(v),t))"; |
|
199 |
by (simp_tac (subst_ss addsimps |
|
200 |
[Unifier_iff,prem RS subst_mono RS occs_irrefl2]) 1); |
|
171 | 201 |
qed "Unify4"; |
0 | 202 |
|
203 |
goal Unifier.thy "ALL l.~Unifier(l,Const(m),Comb(t,u))"; |
|
204 |
by (simp_tac (subst_ss addsimps [Unifier_iff]) 1); |
|
171 | 205 |
qed "Unify5"; |
0 | 206 |
|
207 |
goal Unifier.thy |
|
208 |
"(ALL l.~Unifier(l,t,v)) --> (ALL l.~Unifier(l,Comb(t,u),Comb(v,w)))"; |
|
209 |
by (simp_tac (subst_ss addsimps [Unifier_iff]) 1); |
|
171 | 210 |
val Unify6 = store_thm("Unify6", result() RS mp); |
0 | 211 |
|
212 |
goal Unifier.thy "MGIUnifier(s,t,v) --> (ALL l.~Unifier(l,u <| s,w <| s)) --> \ |
|
213 |
\ (ALL l.~Unifier(l,Comb(t,u),Comb(v,w)))"; |
|
214 |
by (simp_tac (subst_ss addsimps [MGIU_iff]) 1); |
|
215 |
by (fast_tac (set_cs addIs [Unifier_comp_subst] addSEs [Unifier_Comb]) 1); |
|
171 | 216 |
val Unify7 = store_thm("Unify7", result() RS mp RS mp); |
0 | 217 |
|
218 |
val [p1,p2,p3] = goal Unifier.thy |
|
219 |
"[| Idem(r); Unifier(s,t <| r,u <| r); \ |
|
220 |
\ (! q.Unifier(q,t <| r,u <| r) --> s <> q =s= q) |] ==> \ |
|
221 |
\ Idem(r <> s)"; |
|
222 |
by (cut_facts_tac [p1, |
|
223 |
p2 RS (p1 RS Unifier_Idem_subst RS (p3 RS spec RS mp))] 1); |
|
224 |
by (REPEAT_SOME (etac rev_mp)); |
|
225 |
by (simp_tac (subst_ss addsimps [raw_Idem_iff,subst_eq_iff,subst_comp]) 1); |
|
171 | 226 |
qed "Unify8_lemma1"; |
0 | 227 |
|
228 |
val [p1,p2,p3,p4] = goal Unifier.thy |
|
229 |
"[| Unifier(q,t,v); Unifier(q,u,w); (! q.Unifier(q,t,v) --> r <> q =s= q); \ |
|
230 |
\ (! q.Unifier(q,u <| r,w <| r) --> s <> q =s= q) |] ==> \ |
|
231 |
\ r <> s <> q =s= q"; |
|
232 |
val pp = p1 RS (p3 RS spec RS mp); |
|
233 |
by (cut_facts_tac [pp, |
|
234 |
p2 RS (pp RS Unifier_comp_subst) RS (p4 RS spec RS mp)] 1); |
|
235 |
by (REPEAT_SOME (etac rev_mp)); |
|
236 |
by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1); |
|
171 | 237 |
qed "Unify8_lemma2"; |
0 | 238 |
|
239 |
goal Unifier.thy "MGIUnifier(r,t,v) --> MGIUnifier(s,u <| r,w <| r) --> \ |
|
240 |
\ MGIUnifier(r <> s,Comb(t,u),Comb(v,w))"; |
|
241 |
by (simp_tac (subst_ss addsimps [MGIU_iff,subst_comp,comp_assoc]) 1); |
|
242 |
by (safe_tac HOL_cs); |
|
243 |
by (REPEAT (etac rev_mp 2)); |
|
244 |
by (simp_tac (subst_ss addsimps |
|
245 |
[Unifier_iff,MGIU_iff,subst_comp,comp_assoc]) 2); |
|
246 |
by (ALLGOALS (fast_tac (set_cs addEs |
|
247 |
[Unifier_Comb,Unify8_lemma1,Unify8_lemma2]))); |
|
171 | 248 |
qed "Unify8"; |
0 | 249 |
|
250 |
||
251 |
(********************** Termination of the algorithm *************************) |
|
252 |
(* *) |
|
253 |
(*UWFD is a well-founded relation that orders the 2 recursive calls in unify *) |
|
254 |
(* NB well-foundedness of UWFD isn't proved *) |
|
255 |
||
256 |
||
257 |
goalw Unifier.thy [UWFD_def] "UWFD(t,t',Comb(t,u),Comb(t',u'))"; |
|
258 |
by (simp_tac subst_ss 1); |
|
259 |
by (fast_tac set_cs 1); |
|
171 | 260 |
qed "UnifyWFD1"; |
0 | 261 |
|
262 |
val [prem] = goal Unifier.thy |
|
263 |
"MGIUnifier(s,t,t') ==> vars_of(u <| s) Un vars_of(u' <| s) <= \ |
|
264 |
\ vars_of(Comb(t,u)) Un vars_of(Comb(t',u'))"; |
|
265 |
by (subgoal_tac "vars_of(u <| s) Un vars_of(u' <| s) <= \ |
|
266 |
\ srange(s) Un vars_of(u) Un srange(s) Un vars_of(u')" 1); |
|
267 |
by (etac subset_trans 1); |
|
268 |
by (ALLGOALS (simp_tac (subst_ss addsimps [Var_intro,subset_iff]))); |
|
269 |
by (ALLGOALS (fast_tac (set_cs addDs |
|
270 |
[Var_intro,prem RS MGIU_srange RS subsetD]))); |
|
171 | 271 |
qed "UWFD2_lemma1"; |
0 | 272 |
|
273 |
val [major,minor] = goal Unifier.thy |
|
274 |
"[| MGIUnifier(s,t,t'); ~ u <| s = u |] ==> \ |
|
275 |
\ ~ vars_of(u <| s) Un vars_of(u' <| s) = \ |
|
276 |
\ (vars_of(t) Un vars_of(u)) Un (vars_of(t') Un vars_of(u'))"; |
|
277 |
by (cut_facts_tac |
|
278 |
[major RS (MGIU_iff RS iffD1) RS conjunct1 RS (Idem_iff RS iffD1)] 1); |
|
279 |
by (rtac (minor RS subst_not_empty RS exE) 1); |
|
280 |
by (rtac (make_elim ((major RS MGIU_sdom) RS subsetD)) 1 THEN assume_tac 1); |
|
281 |
by (rtac (disjI2 RS (not_equal_iff RS iffD2)) 1); |
|
282 |
by (REPEAT (etac rev_mp 1)); |
|
283 |
by (asm_simp_tac subst_ss 1); |
|
284 |
by (fast_tac (set_cs addIs [Var_elim2]) 1); |
|
171 | 285 |
qed "UWFD2_lemma2"; |
0 | 286 |
|
287 |
val [prem] = goalw Unifier.thy [UWFD_def] |
|
288 |
"MGIUnifier(s,t,t') ==> UWFD(u <| s,u' <| s,Comb(t,u),Comb(t',u'))"; |
|
289 |
by (cut_facts_tac |
|
290 |
[prem RS UWFD2_lemma1 RS (subseteq_iff_subset_eq RS iffD1)] 1); |
|
291 |
by (imp_excluded_middle_tac "u <| s = u" 1); |
|
292 |
by (simp_tac (set_ss addsimps [occs_Comb2] ) 1); |
|
293 |
by (rtac impI 1 THEN etac subst 1 THEN assume_tac 1); |
|
294 |
by (rtac impI 1); |
|
295 |
by (rtac (conjI RS (ssubset_iff RS iffD2) RS disjI1) 1); |
|
296 |
by (asm_simp_tac (set_ss addsimps [subseteq_iff_subset_eq]) 1); |
|
297 |
by (asm_simp_tac subst_ss 1); |
|
298 |
by (fast_tac (set_cs addDs [prem RS UWFD2_lemma2]) 1); |
|
171 | 299 |
qed "UnifyWFD2"; |