(* ID: $Id: Unify.thy,v 1.8 2005/04/01 19:04:01 paulson Exp $ Author: Konrad Slind, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge *) header{*Unification Algorithm*} theory Unify imports Unifier begin text{* Substitution and Unification in Higher-Order Logic. Implements Manna and Waldinger's formalization, with Paulson's simplifications, and some new simplifications by Slind. Z Manna and R Waldinger, Deductive Synthesis of the Unification Algorithm. SCP 1 (1981), 5-48 L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170 *} consts unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" unify :: "'a uterm * 'a uterm => ('a * 'a uterm) list option" defs unifyRel_def: "unifyRel == inv_image (finite_psubset <*lex*> measure uterm_size) (%(M,N). (vars_of M Un vars_of N, M))" --{*Termination relation for the Unify function: either the set of variables decreases, or the first argument does (in fact, both do) *} text{* Wellfoundedness of unifyRel *} lemma wf_unifyRel [iff]: "wf unifyRel" by (simp add: unifyRel_def wf_lex_prod wf_finite_psubset) recdef (permissive) unify "unifyRel" unify_CC: "unify(Const m, Const n) = (if (m=n) then Some[] else None)" unify_CB: "unify(Const m, Comb M N) = None" unify_CV: "unify(Const m, Var v) = Some[(v,Const m)]" unify_V: "unify(Var v, M) = (if (Var v \<prec> M) then None else Some[(v,M)])" unify_BC: "unify(Comb M N, Const x) = None" unify_BV: "unify(Comb M N, Var v) = (if (Var v \<prec> Comb M N) then None else Some[(v,Comb M N)])" unify_BB: "unify(Comb M1 N1, Comb M2 N2) = (case unify(M1,M2) of None => None | Some theta => (case unify(N1 \<lhd> theta, N2 \<lhd> theta) of None => None | Some sigma => Some (theta ◊ sigma)))" (hints recdef_wf: wf_unifyRel) text{* This file defines a nested unification algorithm, then proves that it terminates, then proves 2 correctness theorems: that when the algorithm succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution. Although the proofs may seem long, they are actually quite direct, in that the correctness and termination properties are not mingled as much as in previous proofs of this algorithm.*} (*--------------------------------------------------------------------------- * Our approach for nested recursive functions is as follows: * * 0. Prove the wellfoundedness of the termination relation. * 1. Prove the non-nested termination conditions. * 2. Eliminate (0) and (1) from the recursion equations and the * induction theorem. * 3. Prove the nested termination conditions by using the induction * theorem from (2) and by using the recursion equations from (2). * These are constrained by the nested termination conditions, but * things work out magically (by wellfoundedness of the termination * relation). * 4. Eliminate the nested TCs from the results of (2). * 5. Prove further correctness properties using the results of (4). * * Deeper nestings require iteration of steps (3) and (4). *---------------------------------------------------------------------------*) text{*The non-nested TC (terminiation condition).*} recdef_tc unify_tc1: unify (1) apply (simp add: unifyRel_def wf_lex_prod wf_finite_psubset, safe) apply (simp add: finite_psubset_def finite_vars_of lex_prod_def measure_def inv_image_def) apply (rule monotone_vars_of [THEN subset_iff_psubset_eq [THEN iffD1]]) done text{*Termination proof.*} lemma trans_unifyRel: "trans unifyRel" by (simp add: unifyRel_def measure_def trans_inv_image trans_lex_prod trans_finite_psubset) text{*The following lemma is used in the last step of the termination proof for the nested call in Unify. Loosely, it says that unifyRel doesn't care about term structure.*} lemma Rassoc: "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) ∈ unifyRel ==> ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) ∈ unifyRel" by (simp add: measure_def less_eq inv_image_def add_assoc Un_assoc unifyRel_def lex_prod_def) text{*This lemma proves the nested termination condition for the base cases * 3, 4, and 6.*} lemma var_elimR: "~(Var x \<prec> M) ==> ((N1 \<lhd> [(x,M)], N2 \<lhd> [(x,M)]), (Comb M N1, Comb(Var x) N2)) ∈ unifyRel & ((N1 \<lhd> [(x,M)], N2 \<lhd> [(x,M)]), (Comb(Var x) N1, Comb M N2)) ∈ unifyRel" apply (case_tac "Var x = M", clarify, simp) apply (case_tac "x ∈ (vars_of N1 Un vars_of N2)") txt{*uterm_less case*} apply (simp add: less_eq unifyRel_def lex_prod_def measure_def inv_image_def) apply blast txt{*@{text finite_psubset} case*} apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def) apply (simp add: finite_psubset_def finite_vars_of psubset_def) apply blast txt{*Final case, also @{text finite_psubset}*} apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def measure_def inv_image_def) apply (cut_tac s = "[(x,M)]" and v = x and t = N2 in Var_elim) apply (cut_tac [3] s = "[(x,M)]" and v = x and t = N1 in Var_elim) apply (simp_all (no_asm_simp) add: srange_iff vars_iff_occseq) apply (auto elim!: Var_intro [THEN disjE] simp add: srange_iff) done text{*Eliminate tc1 from the recursion equations and the induction theorem.*} lemmas unify_nonrec [simp] = unify_CC unify_CB unify_CV unify_V unify_BC unify_BV lemmas unify_simps0 = unify_nonrec unify_BB [OF unify_tc1] lemmas unify_induct0 = unify.induct [OF unify_tc1] text{*The nested TC. The (2) requests the second one. Proved by recursion induction.*} recdef_tc unify_tc2: unify (2) txt{*The extracted TC needs the scope of its quantifiers adjusted, so our first step is to restrict the scopes of N1 and N2.*} apply (subgoal_tac "∀M1 M2 theta. unify (M1, M2) = Some theta --> (∀N1 N2.((N1\<lhd>theta, N2\<lhd>theta), (Comb M1 N1, Comb M2 N2)) ∈ unifyRel)") apply blast apply (rule allI) apply (rule allI) txt{*Apply induction on this still-quantified formula*} apply (rule_tac u = M1 and v = M2 in unify_induct0) apply (simp_all (no_asm_simp) add: var_elimR unify_simps0) txt{*Const-Const case*} apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def less_eq) txt{*Comb-Comb case*} apply (simp (no_asm_simp) split add: option.split) apply (intro strip) apply (rule trans_unifyRel [THEN transD], blast) apply (simp only: subst_Comb [symmetric]) apply (rule Rassoc, blast) done text{* Now for elimination of nested TC from unify.simps and induction.*} text{*Desired rule, copied from the theory file.*} lemma unifyCombComb [simp]: "unify(Comb M1 N1, Comb M2 N2) = (case unify(M1,M2) of None => None | Some theta => (case unify(N1 \<lhd> theta, N2 \<lhd> theta) of None => None | Some sigma => Some (theta ◊ sigma)))" by (simp add: unify_tc2 unify_simps0 split add: option.split) text{*The ML version had this, but it can't be used: we get *** exception THM raised: transfer: not a super theory All we can do is state the desired induction rule in full and prove it.*} ML{* bind_thm ("unify_induct", rule_by_tactic (ALLGOALS (full_simp_tac (simpset() addsimps [thm"unify_tc2"]))) (thm"unify_induct0")); *} text{*Correctness. Notice that idempotence is not needed to prove that the algorithm terminates and is not needed to prove the algorithm correct, if you are only interested in an MGU. This is in contrast to the approach of M&W, who used idempotence and MGU-ness in the termination proof.*} theorem unify_gives_MGU [rule_format]: "∀theta. unify(M,N) = Some theta --> MGUnifier theta M N" apply (rule_tac u = M and v = N in unify_induct0) apply (simp_all (no_asm_simp)) txt{*Const-Const case*} apply (simp add: MGUnifier_def Unifier_def) txt{*Const-Var case*} apply (subst mgu_sym) apply (simp add: MGUnifier_Var) txt{*Var-M case*} apply (simp add: MGUnifier_Var) txt{*Comb-Var case*} apply (subst mgu_sym) apply (simp add: MGUnifier_Var) txt{*Comb-Comb case*} apply (simp add: unify_tc2) apply (simp (no_asm_simp) split add: option.split) apply (intro strip) apply (simp add: MGUnifier_def Unifier_def MoreGeneral_def) apply (safe, rename_tac theta sigma gamma) apply (erule_tac x = gamma in allE, erule (1) notE impE) apply (erule exE, rename_tac delta) apply (erule_tac x = delta in allE) apply (subgoal_tac "N1 \<lhd> theta \<lhd> delta = N2 \<lhd> theta \<lhd> delta") apply (blast intro: subst_trans intro!: subst_cong comp_assoc[THEN subst_sym]) apply (simp add: subst_eq_iff) done text{*Unify returns idempotent substitutions, when it succeeds.*} theorem unify_gives_Idem [rule_format]: "∀theta. unify(M,N) = Some theta --> Idem theta" apply (rule_tac u = M and v = N in unify_induct0) apply (simp_all add: Var_Idem unify_tc2 split add: option.split) txt{*Comb-Comb case*} apply safe apply (drule spec, erule (1) notE impE)+ apply (safe dest!: unify_gives_MGU [unfolded MGUnifier_def]) apply (rule Idem_comp, assumption+) apply (force simp add: MoreGeneral_def subst_eq_iff Idem_def) done end
lemma wf_unifyRel:
wf unifyRel
lemma trans_unifyRel:
trans unifyRel
lemma Rassoc:
((X, Y), Comb A (Comb B C), Comb D (Comb E F)) ∈ unifyRel ==> ((X, Y), Comb (Comb A B) C, Comb (Comb D E) F) ∈ unifyRel
lemma var_elimR:
¬ Var x <: M ==> ((N1.0 <| [(x, M)], N2.0 <| [(x, M)]), Comb M N1.0, Comb (Var x) N2.0) ∈ unifyRel ∧ ((N1.0 <| [(x, M)], N2.0 <| [(x, M)]), Comb (Var x) N1.0, Comb M N2.0) ∈ unifyRel
lemmas unify_nonrec:
unify (Const m, Const n) = (if m = n then Some [] else None)
unify (Const m, Comb M N) = None
unify (Const m, Var v) = Some [(v, Const m)]
unify (Var v, M) = (if Var v <: M then None else Some [(v, M)])
unify (Comb M N, Const x) = None
unify (Comb M N, Var v) = (if Var v = M ∨ Var v = N ∨ Var v <: M ∨ Var v <: N then None else Some [(v, Comb M N)])
lemmas unify_nonrec:
unify (Const m, Const n) = (if m = n then Some [] else None)
unify (Const m, Comb M N) = None
unify (Const m, Var v) = Some [(v, Const m)]
unify (Var v, M) = (if Var v <: M then None else Some [(v, M)])
unify (Comb M N, Const x) = None
unify (Comb M N, Var v) = (if Var v = M ∨ Var v = N ∨ Var v <: M ∨ Var v <: N then None else Some [(v, Comb M N)])
lemmas unify_simps0:
unify (Const m, Const n) = (if m = n then Some [] else None)
unify (Const m, Comb M N) = None
unify (Const m, Var v) = Some [(v, Const m)]
unify (Var v, M) = (if Var v <: M then None else Some [(v, M)])
unify (Comb M N, Const x) = None
unify (Comb M N, Var v) = (if Var v = M ∨ Var v = N ∨ Var v <: M ∨ Var v <: N then None else Some [(v, Comb M N)])
unify (Comb M1.0 N1.0, Comb M2.0 N2.0) = (case unify (M1.0, M2.0) of None => None | Some theta => case if ((N1.0 <| theta, N2.0 <| theta), Comb M1.0 N1.0, Comb M2.0 N2.0) ∈ unifyRel then unify (N1.0 <| theta, N2.0 <| theta) else arbitrary of None => None | Some sigma => Some (theta <> sigma))
lemmas unify_simps0:
unify (Const m, Const n) = (if m = n then Some [] else None)
unify (Const m, Comb M N) = None
unify (Const m, Var v) = Some [(v, Const m)]
unify (Var v, M) = (if Var v <: M then None else Some [(v, M)])
unify (Comb M N, Const x) = None
unify (Comb M N, Var v) = (if Var v = M ∨ Var v = N ∨ Var v <: M ∨ Var v <: N then None else Some [(v, Comb M N)])
unify (Comb M1.0 N1.0, Comb M2.0 N2.0) = (case unify (M1.0, M2.0) of None => None | Some theta => case if ((N1.0 <| theta, N2.0 <| theta), Comb M1.0 N1.0, Comb M2.0 N2.0) ∈ unifyRel then unify (N1.0 <| theta, N2.0 <| theta) else arbitrary of None => None | Some sigma => Some (theta <> sigma))
lemmas unify_induct0:
[| !!m n. P (Const m) (Const n); !!m M N. P (Const m) (Comb M N); !!m v. P (Const m) (Var v); !!v M. P (Var v) M; !!M N x. P (Comb M N) (Const x); !!M N v. P (Comb M N) (Var v); !!M1 N1 M2 N2. [| ∀theta. unify (M1, M2) = Some theta --> ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) ∈ unifyRel --> P (N1 <| theta) (N2 <| theta); P M1 M2 |] ==> P (Comb M1 N1) (Comb M2 N2) |] ==> P u v
lemmas unify_induct0:
[| !!m n. P (Const m) (Const n); !!m M N. P (Const m) (Comb M N); !!m v. P (Const m) (Var v); !!v M. P (Var v) M; !!M N x. P (Comb M N) (Const x); !!M N v. P (Comb M N) (Var v); !!M1 N1 M2 N2. [| ∀theta. unify (M1, M2) = Some theta --> ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) ∈ unifyRel --> P (N1 <| theta) (N2 <| theta); P M1 M2 |] ==> P (Comb M1 N1) (Comb M2 N2) |] ==> P u v
lemma unifyCombComb:
unify (Comb M1.0 N1.0, Comb M2.0 N2.0) = (case unify (M1.0, M2.0) of None => None | Some theta => case unify (N1.0 <| theta, N2.0 <| theta) of None => None | Some sigma => Some (theta <> sigma))
theorem unify_induct:
[| !!m n. P (Const m) (Const n); !!m M N. P (Const m) (Comb M N); !!m v. P (Const m) (Var v); !!v M. P (Var v) M; !!M N x. P (Comb M N) (Const x); !!M N v. P (Comb M N) (Var v); !!M1 N1 M2 N2. [| ∀theta. unify (M1, M2) = Some theta --> P (N1 <| theta) (N2 <| theta); P M1 M2 |] ==> P (Comb M1 N1) (Comb M2 N2) |] ==> P u v
theorem unify_gives_MGU:
unify (M, N) = Some theta ==> MGUnifier theta M N
theorem unify_gives_Idem:
unify (M, N) = Some theta ==> Idem theta