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