src/HOL/Subst/Unify.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 26806 40b411ec05aa
child 38140 05691ad74079
permissions -rw-r--r--
simplified method setup;
     1 (*  ID:         $Id$
     2     Author:     Konrad Slind, Cambridge University Computer Laboratory
     3     Copyright   1997  University of Cambridge
     4 
     5 *)
     6 
     7 header{*Unification Algorithm*}
     8 
     9 theory Unify
    10 imports Unifier
    11 begin
    12 
    13 subsection {* Substitution and Unification in Higher-Order Logic. *}
    14 
    15 text {*
    16 NB: This theory is already quite old.
    17 You might want to look at the newer Isar formalization of
    18 unification in HOL/ex/Unification.thy.
    19 
    20 Implements Manna and Waldinger's formalization, with Paulson's simplifications,
    21 and some new simplifications by Slind.
    22 
    23 Z Manna and R Waldinger, Deductive Synthesis of the Unification Algorithm.
    24 SCP 1 (1981), 5-48
    25 
    26 L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170
    27 *}
    28 
    29 definition
    30    unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" where
    31   "unifyRel = inv_image (finite_psubset <*lex*> measure uterm_size)
    32       (%(M,N). (vars_of M Un vars_of N, M))"
    33    --{*Termination relation for the Unify function:
    34          either the set of variables decreases,
    35          or the first argument does (in fact, both do) *}
    36 
    37 
    38 text{* Wellfoundedness of unifyRel *}
    39 lemma wf_unifyRel [iff]: "wf unifyRel"
    40   by (simp add: unifyRel_def wf_lex_prod wf_finite_psubset)
    41 
    42 consts unify :: "'a uterm * 'a uterm => ('a * 'a uterm) list option"
    43 recdef (permissive) unify "unifyRel"
    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"
    46  unify_CV: "unify(Const m, Var v)    = Some[(v,Const 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"
    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)])"
    51  unify_BB:
    52   "unify(Comb M1 N1, Comb M2 N2) =
    53       (case unify(M1,M2)
    54         of None       => None
    55          | Some theta => (case unify(N1 \<lhd> theta, N2 \<lhd> theta)
    56                             of None       => None
    57                              | Some sigma => Some (theta \<lozenge> sigma)))"
    58   (hints recdef_wf: wf_unifyRel)
    59 
    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.*}
    67 
    68 (*---------------------------------------------------------------------------
    69  * Our approach for nested recursive functions is as follows:
    70  *
    71  *    0. Prove the wellfoundedness of the termination relation.
    72  *    1. Prove the non-nested termination conditions.
    73  *    2. Eliminate (0) and (1) from the recursion equations and the
    74  *       induction theorem.
    75  *    3. Prove the nested termination conditions by using the induction
    76  *       theorem from (2) and by using the recursion equations from (2).
    77  *       These are constrained by the nested termination conditions, but
    78  *       things work out magically (by wellfoundedness of the termination
    79  *       relation).
    80  *    4. Eliminate the nested TCs from the results of (2).
    81  *    5. Prove further correctness properties using the results of (4).
    82  *
    83  * Deeper nestings require iteration of steps (3) and (4).
    84  *---------------------------------------------------------------------------*)
    85 
    86 text{*The non-nested TC (terminiation condition).*}
    87 recdef_tc unify_tc1: unify (1)
    88   by (auto simp: unifyRel_def finite_psubset_def finite_vars_of)
    89 
    90 
    91 text{*Termination proof.*}
    92 
    93 lemma trans_unifyRel: "trans unifyRel"
    94   by (simp add: unifyRel_def measure_def trans_inv_image trans_lex_prod
    95     trans_finite_psubset)
    96 
    97 
    98 text{*The following lemma is used in the last step of the termination proof
    99 for the nested call in Unify.  Loosely, it says that unifyRel doesn't care
   100 about term structure.*}
   101 lemma Rassoc:
   102   "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) \<in> unifyRel  ==>
   103     ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) \<in> unifyRel"
   104   by (simp add: less_eq add_assoc Un_assoc unifyRel_def lex_prod_def)
   105 
   106 
   107 text{*This lemma proves the nested termination condition for the base cases
   108  * 3, 4, and 6.*}
   109 lemma var_elimR:
   110   "~(Var x \<prec> M) ==>
   111     ((N1 \<lhd> [(x,M)], N2 \<lhd> [(x,M)]), (Comb M N1, Comb(Var x) N2)) \<in> unifyRel
   112   & ((N1 \<lhd> [(x,M)], N2 \<lhd> [(x,M)]), (Comb(Var x) N1, Comb M N2)) \<in> unifyRel"
   113 apply (case_tac "Var x = M", clarify, simp)
   114 apply (case_tac "x \<in> (vars_of N1 Un vars_of N2)")
   115 txt{*@{text uterm_less} case*}
   116 apply (simp add: less_eq unifyRel_def lex_prod_def)
   117 apply blast
   118 txt{*@{text finite_psubset} case*}
   119 apply (simp add: unifyRel_def lex_prod_def)
   120 apply (simp add: finite_psubset_def finite_vars_of psubset_eq)
   121 apply blast
   122 txt{*Final case, also @{text finite_psubset}*}
   123 apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def)
   124 apply (cut_tac s = "[(x,M)]" and v = x and t = N2 in Var_elim)
   125 apply (cut_tac [3] s = "[(x,M)]" and v = x and t = N1 in Var_elim)
   126 apply (simp_all (no_asm_simp) add: srange_iff vars_iff_occseq)
   127 apply (auto elim!: Var_intro [THEN disjE] simp add: srange_iff)
   128 done
   129 
   130 
   131 text{*Eliminate tc1 from the recursion equations and the induction theorem.*}
   132 
   133 lemmas unify_nonrec [simp] =
   134        unify_CC unify_CB unify_CV unify_V unify_BC unify_BV
   135 
   136 lemmas unify_simps0 = unify_nonrec unify_BB [OF unify_tc1]
   137 
   138 lemmas unify_induct0 = unify.induct [OF unify_tc1]
   139 
   140 text{*The nested TC. The (2) requests the second one.
   141       Proved by recursion induction.*}
   142 recdef_tc unify_tc2: unify (2)
   143 txt{*The extracted TC needs the scope of its quantifiers adjusted, so our
   144  first step is to restrict the scopes of N1 and N2.*}
   145 apply (subgoal_tac "\<forall>M1 M2 theta. unify (M1, M2) = Some theta -->
   146       (\<forall>N1 N2.((N1\<lhd>theta, N2\<lhd>theta), (Comb M1 N1, Comb M2 N2)) \<in> unifyRel)")
   147 apply blast
   148 apply (rule allI)
   149 apply (rule allI)
   150 txt{*Apply induction on this still-quantified formula*}
   151 apply (rule_tac u = M1 and v = M2 in unify_induct0)
   152       apply (simp_all (no_asm_simp) add: var_elimR unify_simps0)
   153  txt{*Const-Const case*}
   154  apply (simp add: unifyRel_def lex_prod_def less_eq)
   155 txt{*Comb-Comb case*}
   156 apply (simp (no_asm_simp) split add: option.split)
   157 apply (intro strip)
   158 apply (rule trans_unifyRel [THEN transD], blast)
   159 apply (simp only: subst_Comb [symmetric])
   160 apply (rule Rassoc, blast)
   161 done
   162 
   163 
   164 text{* Now for elimination of nested TC from unify.simps and induction.*}
   165 
   166 text{*Desired rule, copied from the theory file.*}
   167 lemma unifyCombComb [simp]:
   168     "unify(Comb M1 N1, Comb M2 N2) =
   169        (case unify(M1,M2)
   170          of None => None
   171           | Some theta => (case unify(N1 \<lhd> theta, N2 \<lhd> theta)
   172                              of None => None
   173                               | Some sigma => Some (theta \<lozenge> sigma)))"
   174 by (simp add: unify_tc2 unify_simps0 split add: option.split)
   175 
   176 lemma unify_induct:
   177   "(\<And>m n. P (Const m) (Const n)) \<Longrightarrow>
   178   (\<And>m M N. P (Const m) (Comb M N)) \<Longrightarrow>
   179   (\<And>m v. P (Const m) (Var v)) \<Longrightarrow>
   180   (\<And>v M. P (Var v) M) \<Longrightarrow>
   181   (\<And>M N x. P (Comb M N) (Const x)) \<Longrightarrow>
   182   (\<And>M N v. P (Comb M N) (Var v)) \<Longrightarrow>
   183   (\<And>M1 N1 M2 N2.
   184     \<forall>theta. unify (M1, M2) = Some theta \<longrightarrow> P (N1 \<lhd> theta) (N2 \<lhd> theta) \<Longrightarrow>
   185     P M1 M2 \<Longrightarrow> P (Comb M1 N1) (Comb M2 N2)) \<Longrightarrow>
   186   P u v"
   187 by (rule unify_induct0) (simp_all add: unify_tc2)
   188 
   189 text{*Correctness. Notice that idempotence is not needed to prove that the
   190 algorithm terminates and is not needed to prove the algorithm correct, if you
   191 are only interested in an MGU.  This is in contrast to the approach of M&W,
   192 who used idempotence and MGU-ness in the termination proof.*}
   193 
   194 theorem unify_gives_MGU [rule_format]:
   195      "\<forall>theta. unify(M,N) = Some theta --> MGUnifier theta M N"
   196 apply (rule_tac u = M and v = N in unify_induct0)
   197     apply (simp_all (no_asm_simp))
   198     txt{*Const-Const case*}
   199     apply (simp add: MGUnifier_def Unifier_def)
   200    txt{*Const-Var case*}
   201    apply (subst mgu_sym)
   202    apply (simp add: MGUnifier_Var)
   203   txt{*Var-M case*}
   204   apply (simp add: MGUnifier_Var)
   205  txt{*Comb-Var case*}
   206  apply (subst mgu_sym)
   207  apply (simp add: MGUnifier_Var)
   208 txt{*Comb-Comb case*}
   209 apply (simp add: unify_tc2)
   210 apply (simp (no_asm_simp) split add: option.split)
   211 apply (intro strip)
   212 apply (simp add: MGUnifier_def Unifier_def MoreGeneral_def)
   213 apply (safe, rename_tac theta sigma gamma)
   214 apply (erule_tac x = gamma in allE, erule (1) notE impE)
   215 apply (erule exE, rename_tac delta)
   216 apply (erule_tac x = delta in allE)
   217 apply (subgoal_tac "N1 \<lhd> theta \<lhd> delta = N2 \<lhd> theta \<lhd> delta")
   218  apply (blast intro: subst_trans intro!: subst_cong comp_assoc[THEN subst_sym])
   219 apply (simp add: subst_eq_iff)
   220 done
   221 
   222 
   223 text{*Unify returns idempotent substitutions, when it succeeds.*}
   224 theorem unify_gives_Idem [rule_format]:
   225      "\<forall>theta. unify(M,N) = Some theta --> Idem theta"
   226 apply (rule_tac u = M and v = N in unify_induct0)
   227 apply (simp_all add: Var_Idem unify_tc2 split add: option.split)
   228 txt{*Comb-Comb case*}
   229 apply safe
   230 apply (drule spec, erule (1) notE impE)+
   231 apply (safe dest!: unify_gives_MGU [unfolded MGUnifier_def])
   232 apply (rule Idem_comp, assumption+)
   233 apply (force simp add: MoreGeneral_def subst_eq_iff Idem_def)
   234 done
   235 
   236 end