src/HOL/Subst/Unify.ML
 author paulson Thu May 15 12:40:01 1997 +0200 (1997-05-15) changeset 3192 a75558a4ed37 child 3209 ccb55f3121d1 permissions -rw-r--r--
New version, modified by Konrad Slind and LCP for TFL
```     1 (*  Title:      Subst/Unify
```
```     2     Author:     Konrad Slind, Cambridge University Computer Laboratory
```
```     3     Copyright   1997  University of Cambridge
```
```     4
```
```     5 Unification algorithm
```
```     6 *)
```
```     7
```
```     8 (*---------------------------------------------------------------------------
```
```     9  * This file defines a nested unification algorithm, then proves that it
```
```    10  * terminates, then proves 2 correctness theorems: that when the algorithm
```
```    11  * succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution.
```
```    12  * Although the proofs may seem long, they are actually quite direct, in that
```
```    13  * the correctness and termination properties are not mingled as much as in
```
```    14  * previous proofs of this algorithm.
```
```    15  *
```
```    16  * Our approach for nested recursive functions is as follows:
```
```    17  *
```
```    18  *    0. Prove the wellfoundedness of the termination relation.
```
```    19  *    1. Prove the non-nested termination conditions.
```
```    20  *    2. Eliminate (0) and (1) from the recursion equations and the
```
```    21  *       induction theorem.
```
```    22  *    3. Prove the nested termination conditions by using the induction
```
```    23  *       theorem from (2) and by using the recursion equations from (2).
```
```    24  *       These are constrained by the nested termination conditions, but
```
```    25  *       things work out magically (by wellfoundedness of the termination
```
```    26  *       relation).
```
```    27  *    4. Eliminate the nested TCs from the results of (2).
```
```    28  *    5. Prove further correctness properties using the results of (4).
```
```    29  *
```
```    30  * Deeper nestings require iteration of steps (3) and (4).
```
```    31  *---------------------------------------------------------------------------*)
```
```    32
```
```    33 open Unify;
```
```    34
```
```    35
```
```    36
```
```    37 (*---------------------------------------------------------------------------
```
```    38  * The non-nested TC plus the wellfoundedness of unifyRel.
```
```    39  *---------------------------------------------------------------------------*)
```
```    40 Tfl.tgoalw Unify.thy [] unify.rules;
```
```    41 (* Wellfoundedness of unifyRel *)
```
```    42 by (simp_tac (!simpset addsimps [unifyRel_def, uterm_less_def,
```
```    43 				 wf_inv_image, wf_lex_prod, wf_finite_psubset,
```
```    44 				 wf_rel_prod, wf_measure]) 1);
```
```    45 (* TC *)
```
```    46 by (Step_tac 1);
```
```    47 by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of,
```
```    48 				 lex_prod_def, measure_def,
```
```    49 				 inv_image_def]) 1);
```
```    50 by (rtac (monotone_vars_of RS (subset_iff_psubset_eq RS iffD1) RS disjE) 1);
```
```    51 by (Blast_tac 1);
```
```    52 by (asm_simp_tac (!simpset addsimps [rprod_def, less_eq, less_add_Suc1]) 1);
```
```    53 qed "tc0";
```
```    54
```
```    55
```
```    56 (*---------------------------------------------------------------------------
```
```    57  * Eliminate tc0 from the recursion equations and the induction theorem.
```
```    58  *---------------------------------------------------------------------------*)
```
```    59 val [wfr,tc] = Prim.Rules.CONJUNCTS tc0;
```
```    60 val unifyRules0 = map (normalize_thm [fn th => wfr RS th, fn th => tc RS th])
```
```    61                      unify.rules;
```
```    62
```
```    63 val unifyInduct0 = [wfr,tc] MRS unify.induct
```
```    64                   |> read_instantiate [("P","split Q")]
```
```    65                   |> rewrite_rule [split RS eq_reflection]
```
```    66                   |> standard;
```
```    67
```
```    68
```
```    69 (*---------------------------------------------------------------------------
```
```    70  * Termination proof.
```
```    71  *---------------------------------------------------------------------------*)
```
```    72
```
```    73 goalw Unify.thy [trans_def,inv_image_def]
```
```    74     "!!r. trans r ==> trans (inv_image r f)";
```
```    75 by (Simp_tac 1);
```
```    76 by (Blast_tac 1);
```
```    77 qed "trans_inv_image";
```
```    78
```
```    79 goalw Unify.thy [finite_psubset_def, trans_def] "trans finite_psubset";
```
```    80 by (simp_tac (!simpset addsimps [psubset_def]) 1);
```
```    81 by (Blast_tac 1);
```
```    82 qed "trans_finite_psubset";
```
```    83
```
```    84 goalw Unify.thy [unifyRel_def,uterm_less_def,measure_def] "trans unifyRel";
```
```    85 by (REPEAT (resolve_tac [trans_inv_image,trans_lex_prod,conjI,
```
```    86 			 trans_finite_psubset,
```
```    87 			 trans_rprod, trans_inv_image, trans_trancl] 1));
```
```    88 qed "trans_unifyRel";
```
```    89
```
```    90
```
```    91 (*---------------------------------------------------------------------------
```
```    92  * The following lemma is used in the last step of the termination proof for
```
```    93  * the nested call in Unify.  Loosely, it says that unifyRel doesn't care
```
```    94  * about term structure.
```
```    95  *---------------------------------------------------------------------------*)
```
```    96 goalw Unify.thy [unifyRel_def,lex_prod_def, inv_image_def]
```
```    97      "!!x. ((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel  ==> \
```
```    98     \      ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel";
```
```    99 by (asm_full_simp_tac (!simpset addsimps [uterm_less_def, measure_def, rprod_def,
```
```   100                           less_eq, inv_image_def,add_assoc]) 1);
```
```   101 by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \
```
```   102                 \  (vars_of D Un vars_of E Un vars_of F)) = \
```
```   103                 \ (vars_of A Un (vars_of B Un vars_of C) Un \
```
```   104                 \  (vars_of D Un (vars_of E Un vars_of F)))" 1);
```
```   105 by (Blast_tac 2);
```
```   106 by (Asm_simp_tac 1);
```
```   107 qed "Rassoc";
```
```   108
```
```   109
```
```   110 (*---------------------------------------------------------------------------
```
```   111  * This lemma proves the nested termination condition for the base cases
```
```   112  * 3, 4, and 6.
```
```   113  *---------------------------------------------------------------------------*)
```
```   114 goal Unify.thy
```
```   115  "!!x. ~(Var x <: M) ==>        \
```
```   116 \   ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel \
```
```   117 \ & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel";
```
```   118 by (case_tac "Var x = M" 1);
```
```   119 by (hyp_subst_tac 1);
```
```   120 by (Simp_tac 1);
```
```   121 by (case_tac "x: (vars_of N1 Un vars_of N2)" 1);
```
```   122 (*uterm_less case*)
```
```   123 by (asm_simp_tac
```
```   124     (!simpset addsimps [less_eq, unifyRel_def, uterm_less_def,
```
```   125 			rprod_def, lex_prod_def,
```
```   126 			measure_def, inv_image_def]) 1);
```
```   127 by (Blast_tac 1);
```
```   128 (*finite_psubset case*)
```
```   129 by (simp_tac
```
```   130     (!simpset addsimps [unifyRel_def, lex_prod_def,
```
```   131 			measure_def, inv_image_def]) 1);
```
```   132 by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of,
```
```   133 				 psubset_def, set_eq_subset]) 1);
```
```   134 by (Blast_tac 1);
```
```   135 (** LEVEL 9 **)
```
```   136 (*Final case, also finite_psubset*)
```
```   137 by (simp_tac
```
```   138     (!simpset addsimps [finite_vars_of, unifyRel_def, finite_psubset_def,
```
```   139 			lex_prod_def, measure_def, inv_image_def]) 1);
```
```   140 by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N2")] Var_elim 1);
```
```   141 by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N1")] Var_elim 3);
```
```   142 by (ALLGOALS (asm_simp_tac(!simpset addsimps [srange_iff, vars_iff_occseq])));
```
```   143 by (REPEAT_FIRST (resolve_tac [conjI, disjI1, psubsetI]));
```
```   144 by (ALLGOALS (asm_full_simp_tac
```
```   145 	      (!simpset addsimps [srange_iff, set_eq_subset])));
```
```   146 by (ALLGOALS
```
```   147     (fast_tac (!claset addEs [Var_intro RS disjE]
```
```   148 	               unsafe_addss (!simpset addsimps [srange_iff]))));
```
```   149 qed "var_elimR";
```
```   150
```
```   151
```
```   152 val Some{nchotomy = subst_nchotomy,...} = assoc(!datatypes,"subst");
```
```   153
```
```   154 (*---------------------------------------------------------------------------
```
```   155  * Do a case analysis on something of type 'a subst.
```
```   156  *---------------------------------------------------------------------------*)
```
```   157
```
```   158 fun subst_case_tac t =
```
```   159 (cut_inst_tac [("x",t)] (subst_nchotomy RS spec) 1
```
```   160   THEN etac disjE 1
```
```   161   THEN rotate_tac ~1 1
```
```   162   THEN Asm_full_simp_tac 1
```
```   163   THEN etac exE 1
```
```   164   THEN rotate_tac ~1 1
```
```   165   THEN Asm_full_simp_tac 1);
```
```   166
```
```   167
```
```   168 (*---------------------------------------------------------------------------
```
```   169  * The nested TC. Proved by recursion induction.
```
```   170  *---------------------------------------------------------------------------*)
```
```   171 val [tc1,tc2,tc3] = unify.tcs;
```
```   172 goalw_cterm [] (cterm_of (sign_of Unify.thy) (USyntax.mk_prop tc3));
```
```   173 (*---------------------------------------------------------------------------
```
```   174  * The extracted TC needs the scope of its quantifiers adjusted, so our
```
```   175  * first step is to restrict the scopes of N1 and N2.
```
```   176  *---------------------------------------------------------------------------*)
```
```   177 by (subgoal_tac "!M1 M2 theta.  \
```
```   178  \   unify(M1, M2) = Subst theta --> \
```
```   179  \   (!N1 N2. ((N1<|theta, N2<|theta), Comb M1 N1, Comb M2 N2) : unifyRel)" 1);
```
```   180 by (Blast_tac 1);
```
```   181 by (rtac allI 1);
```
```   182 by (rtac allI 1);
```
```   183 (* Apply induction *)
```
```   184 by (res_inst_tac [("v","M1"),("v1.0","M2")] unifyInduct0 1);
```
```   185 by (ALLGOALS
```
```   186     (asm_simp_tac (!simpset addsimps (var_elimR::unifyRules0)
```
```   187 			    setloop (split_tac [expand_if]))));
```
```   188 (*Const-Const case*)
```
```   189 by (simp_tac
```
```   190     (!simpset addsimps [unifyRel_def, lex_prod_def, measure_def,
```
```   191 			inv_image_def, less_eq, uterm_less_def, rprod_def]) 1);
```
```   192 (** LEVEL 7 **)
```
```   193 (*Comb-Comb case*)
```
```   194 by (subst_case_tac "unify(M1a, M2a)");
```
```   195 by (rename_tac "theta" 1);
```
```   196 by (subst_case_tac "unify(N1 <| theta, N2 <| theta)");
```
```   197 by (rename_tac "sigma" 1);
```
```   198 by (REPEAT (rtac allI 1));
```
```   199 by (rename_tac "P Q" 1);
```
```   200 by (rtac (trans_unifyRel RS transD) 1);
```
```   201 by (Blast_tac 1);
```
```   202 by (simp_tac (HOL_ss addsimps [subst_Comb RS sym]) 1);
```
```   203 by (subgoal_tac "((Comb N1 P <| theta, Comb N2 Q <| theta), \
```
```   204                 \ (Comb M1a (Comb N1 P), Comb M2a (Comb N2 Q))) :unifyRel" 1);
```
```   205 by (asm_simp_tac HOL_ss 2);
```
```   206 by (rtac Rassoc 1);
```
```   207 by (Blast_tac 1);
```
```   208 qed_spec_mp "unify_TC2";
```
```   209
```
```   210
```
```   211 (*---------------------------------------------------------------------------
```
```   212  * Now for elimination of nested TC from unify.rules and induction.
```
```   213  *---------------------------------------------------------------------------*)
```
```   214
```
```   215 (*Desired rule, copied from the theory file.  Could it be made available?*)
```
```   216 goal Unify.thy
```
```   217   "unify(Comb M1 N1, Comb M2 N2) =      \
```
```   218 \      (case unify(M1,M2)               \
```
```   219 \        of Fail => Fail                \
```
```   220 \         | Subst theta => (case unify(N1 <| theta, N2 <| theta)        \
```
```   221 \                            of Fail => Fail    \
```
```   222 \                             | Subst sigma => Subst (theta <> sigma)))";
```
```   223 by (asm_simp_tac (!simpset addsimps unifyRules0) 1);
```
```   224 by (subst_case_tac "unify(M1, M2)");
```
```   225 by (asm_simp_tac (!simpset addsimps [unify_TC2]) 1);
```
```   226 qed "unifyCombComb";
```
```   227
```
```   228
```
```   229 val unifyRules = rev (unifyCombComb :: tl (rev unifyRules0));
```
```   230
```
```   231 Addsimps unifyRules;
```
```   232
```
```   233 val prems = goal Unify.thy
```
```   234 "   [| !!m n. Q (Const m) (Const n);      \
```
```   235 \      !!m M N. Q (Const m) (Comb M N); !!m x. Q (Const m) (Var x);     \
```
```   236 \      !!x M. Q (Var x) M; !!M N x. Q (Comb M N) (Const x);     \
```
```   237 \      !!M N x. Q (Comb M N) (Var x);   \
```
```   238 \      !!M1 N1 M2 N2.   \
```
```   239 \         (! theta.     \
```
```   240 \             unify (M1, M2) = Subst theta -->  \
```
```   241 \             Q (N1 <| theta) (N2 <| theta)) & Q M1 M2   \
```
```   242 \         ==> Q (Comb M1 N1) (Comb M2 N2) |] ==> Q M1 M2";
```
```   243 by (res_inst_tac [("v","M1"),("v1.0","M2")] unifyInduct0 1);
```
```   244 by (ALLGOALS (asm_simp_tac (!simpset addsimps (unify_TC2::prems))));
```
```   245 qed "unifyInduct";
```
```   246
```
```   247
```
```   248
```
```   249 (*---------------------------------------------------------------------------
```
```   250  * Correctness. Notice that idempotence is not needed to prove that the
```
```   251  * algorithm terminates and is not needed to prove the algorithm correct,
```
```   252  * if you are only interested in an MGU.  This is in contrast to the
```
```   253  * approach of M&W, who used idempotence and MGU-ness in the termination proof.
```
```   254  *---------------------------------------------------------------------------*)
```
```   255
```
```   256 goal Unify.thy "!theta. unify(P,Q) = Subst theta --> MGUnifier theta P Q";
```
```   257 by (res_inst_tac [("M1.0","P"),("M2.0","Q")] unifyInduct 1);
```
```   258 by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
```
```   259 (*Const-Const case*)
```
```   260 by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1);
```
```   261 (*Const-Var case*)
```
```   262 by (stac mgu_sym 1);
```
```   263 by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
```
```   264 (*Var-M case*)
```
```   265 by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
```
```   266 (*Comb-Var case*)
```
```   267 by (stac mgu_sym 1);
```
```   268 by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
```
```   269 (*Comb-Comb case*)
```
```   270 by (safe_tac (!claset));
```
```   271 by (subst_case_tac "unify(M1, M2)");
```
```   272 by (subst_case_tac "unify(N1<|list, N2<|list)");
```
```   273 by (hyp_subst_tac 1);
```
```   274 by (asm_full_simp_tac (!simpset addsimps [MGUnifier_def, Unifier_def])1);
```
```   275 (** LEVEL 13 **)
```
```   276 by (safe_tac (!claset));
```
```   277 by (rename_tac "theta sigma gamma" 1);
```
```   278 by (rewrite_goals_tac [MoreGeneral_def]);
```
```   279 by (rotate_tac ~3 1);
```
```   280 by (eres_inst_tac [("x","gamma")] allE 1);
```
```   281 by (Asm_full_simp_tac 1);
```
```   282 by (etac exE 1);
```
```   283 by (rename_tac "delta" 1);
```
```   284 by (eres_inst_tac [("x","delta")] allE 1);
```
```   285 by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1);
```
```   286 (*Proving the subgoal*)
```
```   287 by (full_simp_tac (!simpset addsimps [subst_eq_iff]) 2);
```
```   288 by (blast_tac (!claset addIs [trans,sym] delrules [impCE]) 2);
```
```   289 by (blast_tac (!claset addIs [subst_trans, subst_cong,
```
```   290 			      comp_assoc RS subst_sym]) 1);
```
```   291 qed_spec_mp "unify_gives_MGU";
```
```   292
```
```   293
```
```   294 (*---------------------------------------------------------------------------
```
```   295  * Unify returns idempotent substitutions, when it succeeds.
```
```   296  *---------------------------------------------------------------------------*)
```
```   297 goal Unify.thy "!theta. unify(P,Q) = Subst theta --> Idem theta";
```
```   298 by (res_inst_tac [("M1.0","P"),("M2.0","Q")] unifyInduct 1);
```
```   299 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Var_Idem]
```
```   300 			             setloop split_tac[expand_if])));
```
```   301 (*Comb-Comb case*)
```
```   302 by (safe_tac (!claset));
```
```   303 by (subst_case_tac "unify(M1, M2)");
```
```   304 by (subst_case_tac "unify(N1 <| list, N2 <| list)");
```
```   305 by (hyp_subst_tac 1);
```
```   306 by prune_params_tac;
```
```   307 by (rename_tac "theta sigma" 1);
```
```   308 (** LEVEL 8 **)
```
```   309 by (dtac unify_gives_MGU 1);
```
```   310 by (dtac unify_gives_MGU 1);
```
```   311 by (rewrite_tac [MGUnifier_def]);
```
```   312 by (safe_tac (!claset));
```
```   313 by (rtac Idem_comp 1);
```
```   314 by (atac 1);
```
```   315 by (atac 1);
```
```   316
```
```   317 by (eres_inst_tac [("x","q")] allE 1);
```
```   318 by (asm_full_simp_tac (!simpset addsimps [MoreGeneral_def]) 1);
```
```   319 by (safe_tac (!claset));
```
```   320 by (asm_full_simp_tac
```
```   321     (!simpset addsimps [srange_iff, subst_eq_iff, Idem_def]) 1);
```
```   322 qed_spec_mp "unify_gives_Idem";
```
```   323
```