# Theory Unify

Up to index of Isabelle/HOL/Subst

theory Unify
imports Unifier
begin

    (*  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