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