src/HOL/Subst/Unify.ML
 author nipkow Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) changeset 15140 322485b816ac parent 13630 a013a9dd370f child 15197 19e735596e51 permissions -rw-r--r--
import -> imports
1 (*  Title:      Subst/Unify
2     ID:         \$Id\$
3     Author:     Konrad Slind, Cambridge University Computer Laboratory
4     Copyright   1997  University of Cambridge
6 Unification algorithm
7 *)
9 (*---------------------------------------------------------------------------
10  * This file defines a nested unification algorithm, then proves that it
11  * terminates, then proves 2 correctness theorems: that when the algorithm
12  * succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution.
13  * Although the proofs may seem long, they are actually quite direct, in that
14  * the correctness and termination properties are not mingled as much as in
15  * previous proofs of this algorithm.
16  *
17  * Our approach for nested recursive functions is as follows:
18  *
19  *    0. Prove the wellfoundedness of the termination relation.
20  *    1. Prove the non-nested termination conditions.
21  *    2. Eliminate (0) and (1) from the recursion equations and the
22  *       induction theorem.
23  *    3. Prove the nested termination conditions by using the induction
24  *       theorem from (2) and by using the recursion equations from (2).
25  *       These are constrained by the nested termination conditions, but
26  *       things work out magically (by wellfoundedness of the termination
27  *       relation).
28  *    4. Eliminate the nested TCs from the results of (2).
29  *    5. Prove further correctness properties using the results of (4).
30  *
31  * Deeper nestings require iteration of steps (3) and (4).
32  *---------------------------------------------------------------------------*)
34 (*---------------------------------------------------------------------------
35  * The non-nested TC plus the wellfoundedness of unifyRel.
36  *---------------------------------------------------------------------------*)
37 Tfl.tgoalw Unify.thy [] unify.simps;
38 (* Wellfoundedness of unifyRel *)
39 by (simp_tac (simpset() addsimps [unifyRel_def,
40 				 wf_inv_image, wf_lex_prod, wf_finite_psubset,
41 				 wf_measure]) 1);
42 (* TC *)
43 by Safe_tac;
44 by (simp_tac (simpset() addsimps [finite_psubset_def, finite_vars_of,
45 				 lex_prod_def, measure_def, inv_image_def]) 1);
46 by (rtac (monotone_vars_of RS (subset_iff_psubset_eq RS iffD1) RS disjE) 1);
47 by (Blast_tac 1);
48 by (asm_simp_tac (simpset() addsimps [less_eq, less_add_Suc1]) 1);
49 qed "tc0";
52 (*---------------------------------------------------------------------------
53  * Termination proof.
54  *---------------------------------------------------------------------------*)
56 Goalw [unifyRel_def, measure_def] "trans unifyRel";
57 by (REPEAT (resolve_tac [trans_inv_image, trans_lex_prod,
58 			 trans_finite_psubset, trans_less_than,
59 			 trans_inv_image] 1));
60 qed "trans_unifyRel";
63 (*---------------------------------------------------------------------------
64  * The following lemma is used in the last step of the termination proof for
65  * the nested call in Unify.  Loosely, it says that unifyRel doesn't care
66  * about term structure.
67  *---------------------------------------------------------------------------*)
68 Goalw [unifyRel_def,lex_prod_def, inv_image_def]
69   "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel  ==> \
70 \  ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel";
71 by (asm_full_simp_tac (simpset() addsimps [measure_def,
72                           less_eq, inv_image_def,add_assoc]) 1);
73 by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \
74                 \  (vars_of D Un vars_of E Un vars_of F)) = \
75                 \ (vars_of A Un (vars_of B Un vars_of C) Un \
76                 \  (vars_of D Un (vars_of E Un vars_of F)))" 1);
77 by (Blast_tac 2);
78 by (Asm_simp_tac 1);
79 qed "Rassoc";
82 (*---------------------------------------------------------------------------
83  * This lemma proves the nested termination condition for the base cases
84  * 3, 4, and 6.
85  *---------------------------------------------------------------------------*)
86 Goal "~(Var x <: M) ==> \
87 \   ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel \
88 \ & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel";
89 by (case_tac "Var x = M" 1);
90 by (hyp_subst_tac 1);
91 by (Simp_tac 1);
92 by (case_tac "x: (vars_of N1 Un vars_of N2)" 1);
93 (*uterm_less case*)
94 by (asm_simp_tac
95     (simpset() addsimps [less_eq, unifyRel_def, lex_prod_def,
96 			measure_def, inv_image_def]) 1);
97 by (Blast_tac 1);
98 (*finite_psubset case*)
99 by (simp_tac
100     (simpset() addsimps [unifyRel_def, lex_prod_def,
101 			measure_def, inv_image_def]) 1);
102 by (simp_tac (simpset() addsimps [finite_psubset_def, finite_vars_of,
103 				 psubset_def, set_eq_subset]) 1);
104 by (Blast_tac 1);
105 (** LEVEL 9 **)
106 (*Final case, also finite_psubset*)
107 by (simp_tac
108     (simpset() addsimps [finite_vars_of, unifyRel_def, finite_psubset_def,
109 			lex_prod_def, measure_def, inv_image_def]) 1);
110 by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N2")] Var_elim 1);
111 by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N1")] Var_elim 3);
112 by (ALLGOALS (asm_simp_tac(simpset() addsimps [srange_iff, vars_iff_occseq])));
113 by (REPEAT_FIRST (resolve_tac [conjI, disjI1, psubsetI]));
114 by (ALLGOALS (asm_full_simp_tac
115 	      (simpset() addsimps [srange_iff, set_eq_subset])));
116 by (ALLGOALS
117     (fast_tac (claset() addEs [Var_intro RS disjE]
119 qed "var_elimR";
122 (*---------------------------------------------------------------------------
123  * Eliminate tc0 from the recursion equations and the induction theorem.
124  *---------------------------------------------------------------------------*)
125 val wfr = tc0 RS conjunct1
126 and tc  = tc0 RS conjunct2;
127 val unifyRules0 = map (rule_by_tactic (rtac wfr 1 THEN TRY(rtac tc 1)))
128                      unify.simps;
130 val unifyInduct0 = [wfr,tc] MRS unify.induct;
133 (*---------------------------------------------------------------------------
134  * The nested TC. Proved by recursion induction.
135  *---------------------------------------------------------------------------*)
136 val [_,_,tc3] = unify.tcs;
137 goalw_cterm [] (cterm_of (sign_of Unify.thy) (HOLogic.mk_Trueprop tc3));
138 (*---------------------------------------------------------------------------
139  * The extracted TC needs the scope of its quantifiers adjusted, so our
140  * first step is to restrict the scopes of N1 and N2.
141  *---------------------------------------------------------------------------*)
142 by (subgoal_tac "!M1 M2 theta.  \
143  \   unify(M1, M2) = Some theta --> \
144  \   (!N1 N2. ((N1<|theta, N2<|theta), (Comb M1 N1, Comb M2 N2)) : unifyRel)" 1);
145 by (Blast_tac 1);
146 by (rtac allI 1);
147 by (rtac allI 1);
148 (* Apply induction *)
149 by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1);
150 by (ALLGOALS
151     (asm_simp_tac (simpset() addsimps (var_elimR::unifyRules0))));
152 (*Const-Const case*)
153 by (simp_tac
154     (simpset() addsimps [unifyRel_def, lex_prod_def, measure_def,
155 			inv_image_def, less_eq]) 1);
156 (** LEVEL 7 **)
157 (*Comb-Comb case*)
158 by (asm_simp_tac (simpset() addsplits [option.split]) 1);
159 by (strip_tac 1);
160 by (rtac (trans_unifyRel RS transD) 1);
161 by (Blast_tac 1);
162 by (simp_tac (HOL_ss addsimps [subst_Comb RS sym]) 1);
163 by (rtac Rassoc 1);
164 by (Blast_tac 1);
165 qed_spec_mp "unify_TC";
168 (*---------------------------------------------------------------------------
169  * Now for elimination of nested TC from unify.simps and induction.
170  *---------------------------------------------------------------------------*)
172 (*Desired rule, copied from the theory file.  Could it be made available?*)
173 Goal "unify(Comb M1 N1, Comb M2 N2) =      \
174 \      (case unify(M1,M2)               \
175 \        of None => None                \
176 \         | Some theta => (case unify(N1 <| theta, N2 <| theta)        \
177 \                            of None => None    \
178 \                             | Some sigma => Some (theta <> sigma)))";
179 by (asm_simp_tac (simpset() addsimps (unify_TC::unifyRules0)
180 			   addsplits [option.split]) 1);
181 qed "unifyCombComb";
184 val unifyRules = rev (unifyCombComb :: tl (rev unifyRules0));
188 bind_thm ("unifyInduct",
189 	  rule_by_tactic
190 	     (ALLGOALS (full_simp_tac (simpset() addsimps [unify_TC])))
191 	     unifyInduct0);
194 (*---------------------------------------------------------------------------
195  * Correctness. Notice that idempotence is not needed to prove that the
196  * algorithm terminates and is not needed to prove the algorithm correct,
197  * if you are only interested in an MGU.  This is in contrast to the
198  * approach of M&W, who used idempotence and MGU-ness in the termination proof.
199  *---------------------------------------------------------------------------*)
201 Goal "!theta. unify(M,N) = Some theta --> MGUnifier theta M N";
202 by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
203 by (ALLGOALS Asm_simp_tac);
204 (*Const-Const case*)
205 by (simp_tac (simpset() addsimps [MGUnifier_def,Unifier_def]) 1);
206 (*Const-Var case*)
207 by (stac mgu_sym 1);
208 by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1);
209 (*Var-M case*)
210 by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1);
211 (*Comb-Var case*)
212 by (stac mgu_sym 1);
213 by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1);
214 (** LEVEL 8 **)
215 (*Comb-Comb case*)
216 by (asm_simp_tac (simpset() addsplits [option.split]) 1);
217 by (strip_tac 1);
218 by (asm_full_simp_tac
219     (simpset() addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1);
220 by (Safe_tac THEN rename_tac "theta sigma gamma" 1);
221 by (eres_inst_tac [("x","gamma")] allE 1 THEN mp_tac 1);
222 by (etac exE 1 THEN rename_tac "delta" 1);
223 by (eres_inst_tac [("x","delta")] allE 1);
224 by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1);
225 (*Proving the subgoal*)
226 by (full_simp_tac (simpset() addsimps [subst_eq_iff]) 2
227     THEN blast_tac (claset() addIs [trans,sym] delrules [impCE]) 2);
228 by (blast_tac (claset() addIs [subst_trans, subst_cong,
229 			      comp_assoc RS subst_sym]) 1);
230 qed_spec_mp "unify_gives_MGU";
233 (*---------------------------------------------------------------------------
234  * Unify returns idempotent substitutions, when it succeeds.
235  *---------------------------------------------------------------------------*)
236 Goal "!theta. unify(M,N) = Some theta --> Idem theta";
237 by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
238 by (ALLGOALS
239     (asm_simp_tac