42 |
42 |
43 recdef (permissive) unify "unifyRel" |
43 recdef (permissive) unify "unifyRel" |
44 unify_CC: "unify(Const m, Const n) = (if (m=n) then Some[] else None)" |
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" |
45 unify_CB: "unify(Const m, Comb M N) = None" |
46 unify_CV: "unify(Const m, Var v) = Some[(v,Const m)]" |
46 unify_CV: "unify(Const m, Var v) = Some[(v,Const m)]" |
47 unify_V: "unify(Var v, M) = (if (Var v <: M) then None else Some[(v,M)])" |
47 unify_V: "unify(Var v, M) = (if (Var v \<prec> M) then None else Some[(v,M)])" |
48 unify_BC: "unify(Comb M N, Const x) = None" |
48 unify_BC: "unify(Comb M N, Const x) = None" |
49 unify_BV: "unify(Comb M N, Var v) = (if (Var v <: Comb M N) then None |
49 unify_BV: "unify(Comb M N, Var v) = (if (Var v \<prec> Comb M N) then None |
50 else Some[(v,Comb M N)])" |
50 else Some[(v,Comb M N)])" |
51 unify_BB: |
51 unify_BB: |
52 "unify(Comb M1 N1, Comb M2 N2) = |
52 "unify(Comb M1 N1, Comb M2 N2) = |
53 (case unify(M1,M2) |
53 (case unify(M1,M2) |
54 of None => None |
54 of None => None |
55 | Some theta => (case unify(N1 <| theta, N2 <| theta) |
55 | Some theta => (case unify(N1 \<lhd> theta, N2 \<lhd> theta) |
56 of None => None |
56 of None => None |
57 | Some sigma => Some (theta <> sigma)))" |
57 | Some sigma => Some (theta \<lozenge> sigma)))" |
58 (hints recdef_wf: wf_unifyRel) |
58 (hints recdef_wf: wf_unifyRel) |
59 |
59 |
60 |
60 |
|
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.*} |
61 |
67 |
62 (*--------------------------------------------------------------------------- |
68 (*--------------------------------------------------------------------------- |
63 * This file defines a nested unification algorithm, then proves that it |
69 * Our approach for nested recursive functions is as follows: |
64 * terminates, then proves 2 correctness theorems: that when the algorithm |
|
65 * succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution. |
|
66 * Although the proofs may seem long, they are actually quite direct, in that |
|
67 * the correctness and termination properties are not mingled as much as in |
|
68 * previous proofs of this algorithm. |
|
69 * |
|
70 * Our approach for nested recursive functions is as follows: |
|
71 * |
70 * |
72 * 0. Prove the wellfoundedness of the termination relation. |
71 * 0. Prove the wellfoundedness of the termination relation. |
73 * 1. Prove the non-nested termination conditions. |
72 * 1. Prove the non-nested termination conditions. |
74 * 2. Eliminate (0) and (1) from the recursion equations and the |
73 * 2. Eliminate (0) and (1) from the recursion equations and the |
75 * induction theorem. |
74 * induction theorem. |
76 * 3. Prove the nested termination conditions by using the induction |
75 * 3. Prove the nested termination conditions by using the induction |
77 * theorem from (2) and by using the recursion equations from (2). |
76 * theorem from (2) and by using the recursion equations from (2). |
78 * These are constrained by the nested termination conditions, but |
77 * These are constrained by the nested termination conditions, but |
79 * things work out magically (by wellfoundedness of the termination |
78 * things work out magically (by wellfoundedness of the termination |
80 * relation). |
79 * relation). |
81 * 4. Eliminate the nested TCs from the results of (2). |
80 * 4. Eliminate the nested TCs from the results of (2). |
82 * 5. Prove further correctness properties using the results of (4). |
81 * 5. Prove further correctness properties using the results of (4). |
83 * |
82 * |
84 * Deeper nestings require iteration of steps (3) and (4). |
83 * Deeper nestings require iteration of steps (3) and (4). |
85 *---------------------------------------------------------------------------*) |
84 *---------------------------------------------------------------------------*) |
86 |
85 |
87 text{*The non-nested TC (terminiation condition). This declaration form |
86 text{*The non-nested TC (terminiation condition).*} |
88 only seems to return one subgoal outstanding from the recdef.*} |
87 recdef_tc unify_tc1: unify (1) |
89 recdef_tc unify_tc1: unify |
|
90 apply (simp add: unifyRel_def wf_lex_prod wf_finite_psubset, safe) |
88 apply (simp add: unifyRel_def wf_lex_prod wf_finite_psubset, safe) |
91 apply (simp add: finite_psubset_def finite_vars_of lex_prod_def measure_def inv_image_def) |
89 apply (simp add: finite_psubset_def finite_vars_of lex_prod_def measure_def |
|
90 inv_image_def) |
92 apply (rule monotone_vars_of [THEN subset_iff_psubset_eq [THEN iffD1]]) |
91 apply (rule monotone_vars_of [THEN subset_iff_psubset_eq [THEN iffD1]]) |
93 done |
92 done |
94 |
|
95 |
|
96 |
93 |
97 |
94 |
98 text{*Termination proof.*} |
95 text{*Termination proof.*} |
99 |
96 |
100 lemma trans_unifyRel: "trans unifyRel" |
97 lemma trans_unifyRel: "trans unifyRel" |
103 |
100 |
104 |
101 |
105 text{*The following lemma is used in the last step of the termination proof |
102 text{*The following lemma is used in the last step of the termination proof |
106 for the nested call in Unify. Loosely, it says that unifyRel doesn't care |
103 for the nested call in Unify. Loosely, it says that unifyRel doesn't care |
107 about term structure.*} |
104 about term structure.*} |
108 lemma Rassoc: |
105 lemma Rassoc: |
109 "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel ==> |
106 "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) \<in> unifyRel ==> |
110 ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel" |
107 ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) \<in> unifyRel" |
111 by (simp add: measure_def less_eq inv_image_def add_assoc Un_assoc |
108 by (simp add: measure_def less_eq inv_image_def add_assoc Un_assoc |
112 unifyRel_def lex_prod_def) |
109 unifyRel_def lex_prod_def) |
113 |
110 |
114 |
111 |
115 text{*This lemma proves the nested termination condition for the base cases |
112 text{*This lemma proves the nested termination condition for the base cases |
116 * 3, 4, and 6.*} |
113 * 3, 4, and 6.*} |
117 lemma var_elimR: |
114 lemma var_elimR: |
118 "~(Var x <: M) ==> |
115 "~(Var x \<prec> M) ==> |
119 ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel |
116 ((N1 \<lhd> [(x,M)], N2 \<lhd> [(x,M)]), (Comb M N1, Comb(Var x) N2)) \<in> unifyRel |
120 & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel" |
117 & ((N1 \<lhd> [(x,M)], N2 \<lhd> [(x,M)]), (Comb(Var x) N1, Comb M N2)) \<in> unifyRel" |
121 apply (case_tac "Var x = M", clarify, simp) |
118 apply (case_tac "Var x = M", clarify, simp) |
122 apply (case_tac "x: (vars_of N1 Un vars_of N2) ") |
119 apply (case_tac "x \<in> (vars_of N1 Un vars_of N2)") |
123 txt{*uterm_less case*} |
120 txt{*uterm_less case*} |
124 apply (simp add: less_eq unifyRel_def lex_prod_def measure_def inv_image_def) |
121 apply (simp add: less_eq unifyRel_def lex_prod_def measure_def inv_image_def) |
125 apply blast |
122 apply blast |
126 txt{*@{text finite_psubset} case*} |
123 txt{*@{text finite_psubset} case*} |
127 apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def) |
124 apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def) |
128 apply (simp add: finite_psubset_def finite_vars_of psubset_def) |
125 apply (simp add: finite_psubset_def finite_vars_of psubset_def) |
129 apply blast |
126 apply blast |
130 txt{*Final case, also {text finite_psubset}*} |
127 txt{*Final case, also @{text finite_psubset}*} |
131 apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def measure_def inv_image_def) |
128 apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def |
132 apply (cut_tac s = "[ (x,M) ]" and v = x and t = N2 in Var_elim) |
129 measure_def inv_image_def) |
133 apply (cut_tac [3] s = "[ (x,M) ]" and v = x and t = N1 in Var_elim) |
130 apply (cut_tac s = "[(x,M)]" and v = x and t = N2 in Var_elim) |
|
131 apply (cut_tac [3] s = "[(x,M)]" and v = x and t = N1 in Var_elim) |
134 apply (simp_all (no_asm_simp) add: srange_iff vars_iff_occseq) |
132 apply (simp_all (no_asm_simp) add: srange_iff vars_iff_occseq) |
135 apply (auto elim!: Var_intro [THEN disjE] simp add: srange_iff) |
133 apply (auto elim!: Var_intro [THEN disjE] simp add: srange_iff) |
136 done |
134 done |
137 |
135 |
138 |
136 |
139 text{*Eliminate tc1 from the recursion equations and the induction theorem.*} |
137 text{*Eliminate tc1 from the recursion equations and the induction theorem.*} |
140 |
138 |
141 lemmas unify_nonrec [simp] = |
139 lemmas unify_nonrec [simp] = |
142 unify_CC unify_CB unify_CV unify_V unify_BC unify_BV |
140 unify_CC unify_CB unify_CV unify_V unify_BC unify_BV |
143 |
141 |
144 lemmas unify_simps0 = unify_nonrec unify_BB [OF unify_tc1] |
142 lemmas unify_simps0 = unify_nonrec unify_BB [OF unify_tc1] |
145 |
143 |
146 lemmas unify_induct0 = unify.induct [OF unify_tc1] |
144 lemmas unify_induct0 = unify.induct [OF unify_tc1] |
147 |
145 |
148 text{*The nested TC. Proved by recursion induction.*} |
146 text{*The nested TC. The (2) requests the second one. |
149 lemma unify_tc2: |
147 Proved by recursion induction.*} |
150 "\<forall>M1 M2 N1 N2 theta. |
148 recdef_tc unify_tc2: unify (2) |
151 unify (M1, M2) = Some theta \<longrightarrow> |
|
152 ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) \<in> unifyRel" |
|
153 txt{*The extracted TC needs the scope of its quantifiers adjusted, so our |
149 txt{*The extracted TC needs the scope of its quantifiers adjusted, so our |
154 first step is to restrict the scopes of N1 and N2.*} |
150 first step is to restrict the scopes of N1 and N2.*} |
155 apply (subgoal_tac "\<forall>M1 M2 theta. unify (M1, M2) = Some theta --> |
151 apply (subgoal_tac "\<forall>M1 M2 theta. unify (M1, M2) = Some theta --> |
156 (\<forall>N1 N2.((N1<|theta, N2<|theta), (Comb M1 N1, Comb M2 N2)) : unifyRel)") |
152 (\<forall>N1 N2.((N1\<lhd>theta, N2\<lhd>theta), (Comb M1 N1, Comb M2 N2)) \<in> unifyRel)") |
157 apply blast |
153 apply blast |
158 apply (rule allI) |
154 apply (rule allI) |
159 apply (rule allI) |
155 apply (rule allI) |
160 txt{*Apply induction on this still-quantified formula*} |
156 txt{*Apply induction on this still-quantified formula*} |
161 apply (rule_tac u = M1 and v = M2 in unify_induct0) |
157 apply (rule_tac u = M1 and v = M2 in unify_induct0) |
162 apply (simp_all (no_asm_simp) add: var_elimR unify_simps0) |
158 apply (simp_all (no_asm_simp) add: var_elimR unify_simps0) |
163 txt{*Const-Const case*} |
159 txt{*Const-Const case*} |
164 apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def less_eq) |
160 apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def less_eq) |
165 txt{*Comb-Comb case*} |
161 txt{*Comb-Comb case*} |
166 apply (simp (no_asm_simp) split add: option.split) |
162 apply (simp (no_asm_simp) split add: option.split) |
167 apply (intro strip) |
163 apply (intro strip) |
168 apply (rule trans_unifyRel [THEN transD], blast) |
164 apply (rule trans_unifyRel [THEN transD], blast) |
169 apply (simp only: subst_Comb [symmetric]) |
165 apply (simp only: subst_Comb [symmetric]) |
200 who used idempotence and MGU-ness in the termination proof.*} |
196 who used idempotence and MGU-ness in the termination proof.*} |
201 |
197 |
202 theorem unify_gives_MGU [rule_format]: |
198 theorem unify_gives_MGU [rule_format]: |
203 "\<forall>theta. unify(M,N) = Some theta --> MGUnifier theta M N" |
199 "\<forall>theta. unify(M,N) = Some theta --> MGUnifier theta M N" |
204 apply (rule_tac u = M and v = N in unify_induct0) |
200 apply (rule_tac u = M and v = N in unify_induct0) |
205 apply (simp_all (no_asm_simp)) |
201 apply (simp_all (no_asm_simp)) |
206 (*Const-Const case*) |
202 txt{*Const-Const case*} |
207 apply (simp (no_asm) add: MGUnifier_def Unifier_def) |
203 apply (simp add: MGUnifier_def Unifier_def) |
208 (*Const-Var case*) |
204 txt{*Const-Var case*} |
209 apply (subst mgu_sym) |
205 apply (subst mgu_sym) |
210 apply (simp (no_asm) add: MGUnifier_Var) |
206 apply (simp add: MGUnifier_Var) |
211 (*Var-M case*) |
207 txt{*Var-M case*} |
212 apply (simp (no_asm) add: MGUnifier_Var) |
208 apply (simp add: MGUnifier_Var) |
213 (*Comb-Var case*) |
209 txt{*Comb-Var case*} |
214 apply (subst mgu_sym) |
210 apply (subst mgu_sym) |
215 apply (simp (no_asm) add: MGUnifier_Var) |
211 apply (simp add: MGUnifier_Var) |
216 (** LEVEL 8 **) |
212 txt{*Comb-Comb case*} |
217 (*Comb-Comb case*) |
213 apply (simp add: unify_tc2) |
218 apply (simp add: unify_tc2) |
|
219 apply (simp (no_asm_simp) split add: option.split) |
214 apply (simp (no_asm_simp) split add: option.split) |
220 apply (intro strip) |
215 apply (intro strip) |
221 apply (simp add: MGUnifier_def Unifier_def MoreGeneral_def) |
216 apply (simp add: MGUnifier_def Unifier_def MoreGeneral_def) |
222 apply (safe, rename_tac theta sigma gamma) |
217 apply (safe, rename_tac theta sigma gamma) |
223 apply (erule_tac x = gamma in allE, erule (1) notE impE) |
218 apply (erule_tac x = gamma in allE, erule (1) notE impE) |
224 apply (erule exE, rename_tac delta) |
219 apply (erule exE, rename_tac delta) |
225 apply (erule_tac x = delta in allE) |
220 apply (erule_tac x = delta in allE) |
226 apply (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta") |
221 apply (subgoal_tac "N1 \<lhd> theta \<lhd> delta = N2 \<lhd> theta \<lhd> delta") |
227 apply (blast intro: subst_trans intro!: subst_cong comp_assoc[THEN subst_sym]) |
222 apply (blast intro: subst_trans intro!: subst_cong comp_assoc[THEN subst_sym]) |
228 apply (simp add: subst_eq_iff) |
223 apply (simp add: subst_eq_iff) |
229 done |
224 done |
230 |
225 |
231 |
226 |
232 text{*Unify returns idempotent substitutions, when it succeeds.*} |
227 text{*Unify returns idempotent substitutions, when it succeeds.*} |
233 theorem unify_gives_Idem [rule_format]: |
228 theorem unify_gives_Idem [rule_format]: |