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