src/HOL/Subst/Unify.ML
 author paulson Wed Nov 05 13:23:46 1997 +0100 (1997-11-05) changeset 4153 e534c4c32d54 parent 4089 96fba19bcbe2 child 4686 74a12e86b20b permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
```     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_measure]) 1);
```
```    46 (* TC *)
```
```    47 by Safe_tac;
```
```    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 (*---------------------------------------------------------------------------
```
```   128  * Eliminate tc0 from the recursion equations and the induction theorem.
```
```   129  *---------------------------------------------------------------------------*)
```
```   130 val wfr = tc0 RS conjunct1
```
```   131 and tc  = tc0 RS conjunct2;
```
```   132 val unifyRules0 = map (normalize_thm [fn th => wfr RS th, fn th => tc RS th])
```
```   133                      unify.rules;
```
```   134
```
```   135 val unifyInduct0 = [wfr,tc] MRS unify.induct;
```
```   136
```
```   137
```
```   138 (*---------------------------------------------------------------------------
```
```   139  * The nested TC. Proved by recursion induction.
```
```   140  *---------------------------------------------------------------------------*)
```
```   141 val [_,_,tc3] = unify.tcs;
```
```   142 goalw_cterm [] (cterm_of (sign_of Unify.thy) (HOLogic.mk_Trueprop tc3));
```
```   143 (*---------------------------------------------------------------------------
```
```   144  * The extracted TC needs the scope of its quantifiers adjusted, so our
```
```   145  * first step is to restrict the scopes of N1 and N2.
```
```   146  *---------------------------------------------------------------------------*)
```
```   147 by (subgoal_tac "!M1 M2 theta.  \
```
```   148  \   unify(M1, M2) = Some theta --> \
```
```   149  \   (!N1 N2. ((N1<|theta, N2<|theta), Comb M1 N1, Comb M2 N2) : unifyRel)" 1);
```
```   150 by (Blast_tac 1);
```
```   151 by (rtac allI 1);
```
```   152 by (rtac allI 1);
```
```   153 (* Apply induction *)
```
```   154 by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1);
```
```   155 by (ALLGOALS
```
```   156     (asm_simp_tac (simpset() addsimps (var_elimR::unifyRules0)
```
```   157 			    addsplits [expand_if])));
```
```   158 (*Const-Const case*)
```
```   159 by (simp_tac
```
```   160     (simpset() addsimps [unifyRel_def, lex_prod_def, measure_def,
```
```   161 			inv_image_def, less_eq]) 1);
```
```   162 (** LEVEL 7 **)
```
```   163 (*Comb-Comb case*)
```
```   164 by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
```
```   165 by (strip_tac 1);
```
```   166 by (rtac (trans_unifyRel RS transD) 1);
```
```   167 by (Blast_tac 1);
```
```   168 by (simp_tac (HOL_ss addsimps [subst_Comb RS sym]) 1);
```
```   169 by (rtac Rassoc 1);
```
```   170 by (Blast_tac 1);
```
```   171 qed_spec_mp "unify_TC";
```
```   172
```
```   173
```
```   174 (*---------------------------------------------------------------------------
```
```   175  * Now for elimination of nested TC from unify.rules and induction.
```
```   176  *---------------------------------------------------------------------------*)
```
```   177
```
```   178 (*Desired rule, copied from the theory file.  Could it be made available?*)
```
```   179 goal Unify.thy
```
```   180   "unify(Comb M1 N1, Comb M2 N2) =      \
```
```   181 \      (case unify(M1,M2)               \
```
```   182 \        of None => None                \
```
```   183 \         | Some theta => (case unify(N1 <| theta, N2 <| theta)        \
```
```   184 \                            of None => None    \
```
```   185 \                             | Some sigma => Some (theta <> sigma)))";
```
```   186 by (asm_simp_tac (simpset() addsimps (unify_TC::unifyRules0)
```
```   187 			   addsplits [split_option_case]) 1);
```
```   188 qed "unifyCombComb";
```
```   189
```
```   190
```
```   191 val unifyRules = rev (unifyCombComb :: tl (rev unifyRules0));
```
```   192
```
```   193 Addsimps unifyRules;
```
```   194
```
```   195 bind_thm ("unifyInduct",
```
```   196 	  rule_by_tactic
```
```   197 	     (ALLGOALS (full_simp_tac (simpset() addsimps [unify_TC])))
```
```   198 	     unifyInduct0);
```
```   199
```
```   200
```
```   201 (*---------------------------------------------------------------------------
```
```   202  * Correctness. Notice that idempotence is not needed to prove that the
```
```   203  * algorithm terminates and is not needed to prove the algorithm correct,
```
```   204  * if you are only interested in an MGU.  This is in contrast to the
```
```   205  * approach of M&W, who used idempotence and MGU-ness in the termination proof.
```
```   206  *---------------------------------------------------------------------------*)
```
```   207
```
```   208 goal Unify.thy "!theta. unify(M,N) = Some theta --> MGUnifier theta M N";
```
```   209 by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
```
```   210 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
```
```   211 (*Const-Const case*)
```
```   212 by (simp_tac (simpset() addsimps [MGUnifier_def,Unifier_def]) 1);
```
```   213 (*Const-Var case*)
```
```   214 by (stac mgu_sym 1);
```
```   215 by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1);
```
```   216 (*Var-M case*)
```
```   217 by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1);
```
```   218 (*Comb-Var case*)
```
```   219 by (stac mgu_sym 1);
```
```   220 by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1);
```
```   221 (** LEVEL 8 **)
```
```   222 (*Comb-Comb case*)
```
```   223 by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
```
```   224 by (strip_tac 1);
```
```   225 by (rotate_tac ~2 1);
```
```   226 by (asm_full_simp_tac
```
```   227     (simpset() addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1);
```
```   228 by (Safe_tac THEN rename_tac "theta sigma gamma" 1);
```
```   229 by (eres_inst_tac [("x","gamma")] allE 1 THEN mp_tac 1);
```
```   230 by (etac exE 1 THEN rename_tac "delta" 1);
```
```   231 by (eres_inst_tac [("x","delta")] allE 1);
```
```   232 by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1);
```
```   233 (*Proving the subgoal*)
```
```   234 by (full_simp_tac (simpset() addsimps [subst_eq_iff]) 2
```
```   235     THEN blast_tac (claset() addIs [trans,sym] delrules [impCE]) 2);
```
```   236 by (blast_tac (claset() addIs [subst_trans, subst_cong,
```
```   237 			      comp_assoc RS subst_sym]) 1);
```
```   238 qed_spec_mp "unify_gives_MGU";
```
```   239
```
```   240
```
```   241 (*---------------------------------------------------------------------------
```
```   242  * Unify returns idempotent substitutions, when it succeeds.
```
```   243  *---------------------------------------------------------------------------*)
```
```   244 goal Unify.thy "!theta. unify(M,N) = Some theta --> Idem theta";
```
```   245 by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
```
```   246 by (ALLGOALS
```
```   247     (asm_simp_tac
```
```   248        (simpset() addsimps [Var_Idem]
```
```   249 	         addsplits [expand_if,split_option_case])));
```
```   250 (*Comb-Comb case*)
```
```   251 by Safe_tac;
```
```   252 by (REPEAT (dtac spec 1 THEN mp_tac 1));
```
```   253 by (safe_tac (claset() addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU]));
```
```   254 by (rtac Idem_comp 1);
```
```   255 by (atac 1);
```
```   256 by (atac 1);
```
```   257 by (best_tac (claset() addss (simpset() addsimps
```
```   258 			     [MoreGeneral_def, subst_eq_iff, Idem_def])) 1);
```
```   259 qed_spec_mp "unify_gives_Idem";
```
```   260
```