src/HOL/Subst/Unify.ML
changeset 3192 a75558a4ed37
child 3209 ccb55f3121d1
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Subst/Unify.ML	Thu May 15 12:40:01 1997 +0200
     1.3 @@ -0,0 +1,323 @@
     1.4 +(*  Title:      Subst/Unify
     1.5 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     1.6 +    Copyright   1997  University of Cambridge
     1.7 +
     1.8 +Unification algorithm
     1.9 +*)
    1.10 +
    1.11 +(*---------------------------------------------------------------------------
    1.12 + * This file defines a nested unification algorithm, then proves that it 
    1.13 + * terminates, then proves 2 correctness theorems: that when the algorithm
    1.14 + * succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution.
    1.15 + * Although the proofs may seem long, they are actually quite direct, in that
    1.16 + * the correctness and termination properties are not mingled as much as in 
    1.17 + * previous proofs of this algorithm. 
    1.18 + *
    1.19 + * Our approach for nested recursive functions is as follows: 
    1.20 + *
    1.21 + *    0. Prove the wellfoundedness of the termination relation.
    1.22 + *    1. Prove the non-nested termination conditions.
    1.23 + *    2. Eliminate (0) and (1) from the recursion equations and the 
    1.24 + *       induction theorem.
    1.25 + *    3. Prove the nested termination conditions by using the induction 
    1.26 + *       theorem from (2) and by using the recursion equations from (2). 
    1.27 + *       These are constrained by the nested termination conditions, but 
    1.28 + *       things work out magically (by wellfoundedness of the termination 
    1.29 + *       relation).
    1.30 + *    4. Eliminate the nested TCs from the results of (2).
    1.31 + *    5. Prove further correctness properties using the results of (4).
    1.32 + *
    1.33 + * Deeper nestings require iteration of steps (3) and (4).
    1.34 + *---------------------------------------------------------------------------*)
    1.35 +
    1.36 +open Unify;
    1.37 +
    1.38 +
    1.39 +
    1.40 +(*---------------------------------------------------------------------------
    1.41 + * The non-nested TC plus the wellfoundedness of unifyRel.
    1.42 + *---------------------------------------------------------------------------*)
    1.43 +Tfl.tgoalw Unify.thy [] unify.rules;
    1.44 +(* Wellfoundedness of unifyRel *)
    1.45 +by (simp_tac (!simpset addsimps [unifyRel_def, uterm_less_def,
    1.46 +				 wf_inv_image, wf_lex_prod, wf_finite_psubset,
    1.47 +				 wf_rel_prod, wf_measure]) 1);
    1.48 +(* TC *)
    1.49 +by (Step_tac 1);
    1.50 +by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of,
    1.51 +				 lex_prod_def, measure_def,
    1.52 +				 inv_image_def]) 1);
    1.53 +by (rtac (monotone_vars_of RS (subset_iff_psubset_eq RS iffD1) RS disjE) 1);
    1.54 +by (Blast_tac 1);
    1.55 +by (asm_simp_tac (!simpset addsimps [rprod_def, less_eq, less_add_Suc1]) 1);
    1.56 +qed "tc0";
    1.57 +
    1.58 +
    1.59 +(*---------------------------------------------------------------------------
    1.60 + * Eliminate tc0 from the recursion equations and the induction theorem.
    1.61 + *---------------------------------------------------------------------------*)
    1.62 +val [wfr,tc] = Prim.Rules.CONJUNCTS tc0;
    1.63 +val unifyRules0 = map (normalize_thm [fn th => wfr RS th, fn th => tc RS th]) 
    1.64 +                     unify.rules;
    1.65 +
    1.66 +val unifyInduct0 = [wfr,tc] MRS unify.induct 
    1.67 +                  |> read_instantiate [("P","split Q")]
    1.68 +                  |> rewrite_rule [split RS eq_reflection]
    1.69 +                  |> standard;
    1.70 +
    1.71 +
    1.72 +(*---------------------------------------------------------------------------
    1.73 + * Termination proof.
    1.74 + *---------------------------------------------------------------------------*)
    1.75 +
    1.76 +goalw Unify.thy [trans_def,inv_image_def]
    1.77 +    "!!r. trans r ==> trans (inv_image r f)";
    1.78 +by (Simp_tac 1);
    1.79 +by (Blast_tac 1);
    1.80 +qed "trans_inv_image";
    1.81 +
    1.82 +goalw Unify.thy [finite_psubset_def, trans_def] "trans finite_psubset";
    1.83 +by (simp_tac (!simpset addsimps [psubset_def]) 1);
    1.84 +by (Blast_tac 1);
    1.85 +qed "trans_finite_psubset";
    1.86 +
    1.87 +goalw Unify.thy [unifyRel_def,uterm_less_def,measure_def] "trans unifyRel";
    1.88 +by (REPEAT (resolve_tac [trans_inv_image,trans_lex_prod,conjI, 
    1.89 +			 trans_finite_psubset,
    1.90 +			 trans_rprod, trans_inv_image, trans_trancl] 1));
    1.91 +qed "trans_unifyRel";
    1.92 +
    1.93 +
    1.94 +(*---------------------------------------------------------------------------
    1.95 + * The following lemma is used in the last step of the termination proof for 
    1.96 + * the nested call in Unify.  Loosely, it says that unifyRel doesn't care
    1.97 + * about term structure.
    1.98 + *---------------------------------------------------------------------------*)
    1.99 +goalw Unify.thy [unifyRel_def,lex_prod_def, inv_image_def]
   1.100 +     "!!x. ((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel  ==> \
   1.101 +    \      ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel";
   1.102 +by (asm_full_simp_tac (!simpset addsimps [uterm_less_def, measure_def, rprod_def,
   1.103 +                          less_eq, inv_image_def,add_assoc]) 1);
   1.104 +by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \
   1.105 +                \  (vars_of D Un vars_of E Un vars_of F)) = \
   1.106 +                \ (vars_of A Un (vars_of B Un vars_of C) Un \
   1.107 +                \  (vars_of D Un (vars_of E Un vars_of F)))" 1);
   1.108 +by (Blast_tac 2);
   1.109 +by (Asm_simp_tac 1);
   1.110 +qed "Rassoc";
   1.111 +
   1.112 +
   1.113 +(*---------------------------------------------------------------------------
   1.114 + * This lemma proves the nested termination condition for the base cases 
   1.115 + * 3, 4, and 6. 
   1.116 + *---------------------------------------------------------------------------*)
   1.117 +goal Unify.thy
   1.118 + "!!x. ~(Var x <: M) ==>        \
   1.119 +\   ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel \
   1.120 +\ & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel";
   1.121 +by (case_tac "Var x = M" 1);
   1.122 +by (hyp_subst_tac 1);
   1.123 +by (Simp_tac 1);
   1.124 +by (case_tac "x: (vars_of N1 Un vars_of N2)" 1);
   1.125 +(*uterm_less case*)
   1.126 +by (asm_simp_tac
   1.127 +    (!simpset addsimps [less_eq, unifyRel_def, uterm_less_def,
   1.128 +			rprod_def, lex_prod_def,
   1.129 +			measure_def, inv_image_def]) 1);
   1.130 +by (Blast_tac 1);
   1.131 +(*finite_psubset case*)
   1.132 +by (simp_tac
   1.133 +    (!simpset addsimps [unifyRel_def, lex_prod_def,
   1.134 +			measure_def, inv_image_def]) 1);
   1.135 +by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of,
   1.136 +				 psubset_def, set_eq_subset]) 1);
   1.137 +by (Blast_tac 1);
   1.138 +(** LEVEL 9 **)
   1.139 +(*Final case, also finite_psubset*)
   1.140 +by (simp_tac
   1.141 +    (!simpset addsimps [finite_vars_of, unifyRel_def, finite_psubset_def,
   1.142 +			lex_prod_def, measure_def, inv_image_def]) 1);
   1.143 +by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N2")] Var_elim 1);
   1.144 +by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N1")] Var_elim 3);
   1.145 +by (ALLGOALS (asm_simp_tac(!simpset addsimps [srange_iff, vars_iff_occseq])));
   1.146 +by (REPEAT_FIRST (resolve_tac [conjI, disjI1, psubsetI]));
   1.147 +by (ALLGOALS (asm_full_simp_tac 
   1.148 +	      (!simpset addsimps [srange_iff, set_eq_subset]))); 
   1.149 +by (ALLGOALS
   1.150 +    (fast_tac (!claset addEs [Var_intro RS disjE]
   1.151 +	               unsafe_addss (!simpset addsimps [srange_iff]))));
   1.152 +qed "var_elimR";
   1.153 +
   1.154 +
   1.155 +val Some{nchotomy = subst_nchotomy,...} = assoc(!datatypes,"subst");
   1.156 +
   1.157 +(*---------------------------------------------------------------------------
   1.158 + * Do a case analysis on something of type 'a subst. 
   1.159 + *---------------------------------------------------------------------------*)
   1.160 +
   1.161 +fun subst_case_tac t =
   1.162 +(cut_inst_tac [("x",t)] (subst_nchotomy RS spec) 1 
   1.163 +  THEN etac disjE 1 
   1.164 +  THEN rotate_tac ~1 1 
   1.165 +  THEN Asm_full_simp_tac 1 
   1.166 +  THEN etac exE 1
   1.167 +  THEN rotate_tac ~1 1 
   1.168 +  THEN Asm_full_simp_tac 1);
   1.169 +
   1.170 +
   1.171 +(*---------------------------------------------------------------------------
   1.172 + * The nested TC. Proved by recursion induction.
   1.173 + *---------------------------------------------------------------------------*)
   1.174 +val [tc1,tc2,tc3] = unify.tcs;
   1.175 +goalw_cterm [] (cterm_of (sign_of Unify.thy) (USyntax.mk_prop tc3));
   1.176 +(*---------------------------------------------------------------------------
   1.177 + * The extracted TC needs the scope of its quantifiers adjusted, so our 
   1.178 + * first step is to restrict the scopes of N1 and N2.
   1.179 + *---------------------------------------------------------------------------*)
   1.180 +by (subgoal_tac "!M1 M2 theta.  \
   1.181 + \   unify(M1, M2) = Subst theta --> \
   1.182 + \   (!N1 N2. ((N1<|theta, N2<|theta), Comb M1 N1, Comb M2 N2) : unifyRel)" 1);
   1.183 +by (Blast_tac 1);
   1.184 +by (rtac allI 1); 
   1.185 +by (rtac allI 1);
   1.186 +(* Apply induction *)
   1.187 +by (res_inst_tac [("v","M1"),("v1.0","M2")] unifyInduct0 1);
   1.188 +by (ALLGOALS 
   1.189 +    (asm_simp_tac (!simpset addsimps (var_elimR::unifyRules0)
   1.190 +			    setloop (split_tac [expand_if]))));
   1.191 +(*Const-Const case*)
   1.192 +by (simp_tac
   1.193 +    (!simpset addsimps [unifyRel_def, lex_prod_def, measure_def,
   1.194 +			inv_image_def, less_eq, uterm_less_def, rprod_def]) 1);
   1.195 +(** LEVEL 7 **)
   1.196 +(*Comb-Comb case*)
   1.197 +by (subst_case_tac "unify(M1a, M2a)");
   1.198 +by (rename_tac "theta" 1);
   1.199 +by (subst_case_tac "unify(N1 <| theta, N2 <| theta)");
   1.200 +by (rename_tac "sigma" 1);
   1.201 +by (REPEAT (rtac allI 1));
   1.202 +by (rename_tac "P Q" 1); 
   1.203 +by (rtac (trans_unifyRel RS transD) 1);
   1.204 +by (Blast_tac 1);
   1.205 +by (simp_tac (HOL_ss addsimps [subst_Comb RS sym]) 1);
   1.206 +by (subgoal_tac "((Comb N1 P <| theta, Comb N2 Q <| theta), \
   1.207 +                \ (Comb M1a (Comb N1 P), Comb M2a (Comb N2 Q))) :unifyRel" 1);
   1.208 +by (asm_simp_tac HOL_ss 2);
   1.209 +by (rtac Rassoc 1);
   1.210 +by (Blast_tac 1);
   1.211 +qed_spec_mp "unify_TC2";
   1.212 +
   1.213 +
   1.214 +(*---------------------------------------------------------------------------
   1.215 + * Now for elimination of nested TC from unify.rules and induction. 
   1.216 + *---------------------------------------------------------------------------*)
   1.217 +
   1.218 +(*Desired rule, copied from the theory file.  Could it be made available?*)
   1.219 +goal Unify.thy 
   1.220 +  "unify(Comb M1 N1, Comb M2 N2) =      \
   1.221 +\      (case unify(M1,M2)               \
   1.222 +\        of Fail => Fail                \
   1.223 +\         | Subst theta => (case unify(N1 <| theta, N2 <| theta)        \
   1.224 +\                            of Fail => Fail    \
   1.225 +\                             | Subst sigma => Subst (theta <> sigma)))";
   1.226 +by (asm_simp_tac (!simpset addsimps unifyRules0) 1);
   1.227 +by (subst_case_tac "unify(M1, M2)");
   1.228 +by (asm_simp_tac (!simpset addsimps [unify_TC2]) 1);
   1.229 +qed "unifyCombComb";
   1.230 +
   1.231 +
   1.232 +val unifyRules = rev (unifyCombComb :: tl (rev unifyRules0));
   1.233 +
   1.234 +Addsimps unifyRules;
   1.235 +
   1.236 +val prems = goal Unify.thy 
   1.237 +"   [| !!m n. Q (Const m) (Const n);      \
   1.238 +\      !!m M N. Q (Const m) (Comb M N); !!m x. Q (Const m) (Var x);     \
   1.239 +\      !!x M. Q (Var x) M; !!M N x. Q (Comb M N) (Const x);     \
   1.240 +\      !!M N x. Q (Comb M N) (Var x);   \
   1.241 +\      !!M1 N1 M2 N2.   \
   1.242 +\         (! theta.     \
   1.243 +\             unify (M1, M2) = Subst theta -->  \
   1.244 +\             Q (N1 <| theta) (N2 <| theta)) & Q M1 M2   \
   1.245 +\         ==> Q (Comb M1 N1) (Comb M2 N2) |] ==> Q M1 M2";
   1.246 +by (res_inst_tac [("v","M1"),("v1.0","M2")] unifyInduct0 1);
   1.247 +by (ALLGOALS (asm_simp_tac (!simpset addsimps (unify_TC2::prems))));
   1.248 +qed "unifyInduct";
   1.249 +
   1.250 +
   1.251 +
   1.252 +(*---------------------------------------------------------------------------
   1.253 + * Correctness. Notice that idempotence is not needed to prove that the 
   1.254 + * algorithm terminates and is not needed to prove the algorithm correct, 
   1.255 + * if you are only interested in an MGU.  This is in contrast to the
   1.256 + * approach of M&W, who used idempotence and MGU-ness in the termination proof.
   1.257 + *---------------------------------------------------------------------------*)
   1.258 +
   1.259 +goal Unify.thy "!theta. unify(P,Q) = Subst theta --> MGUnifier theta P Q";
   1.260 +by (res_inst_tac [("M1.0","P"),("M2.0","Q")] unifyInduct 1);
   1.261 +by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
   1.262 +(*Const-Const case*)
   1.263 +by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1);
   1.264 +(*Const-Var case*)
   1.265 +by (stac mgu_sym 1);
   1.266 +by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
   1.267 +(*Var-M case*)
   1.268 +by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
   1.269 +(*Comb-Var case*)
   1.270 +by (stac mgu_sym 1);
   1.271 +by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
   1.272 +(*Comb-Comb case*)
   1.273 +by (safe_tac (!claset));
   1.274 +by (subst_case_tac "unify(M1, M2)");
   1.275 +by (subst_case_tac "unify(N1<|list, N2<|list)");
   1.276 +by (hyp_subst_tac 1);
   1.277 +by (asm_full_simp_tac (!simpset addsimps [MGUnifier_def, Unifier_def])1);
   1.278 +(** LEVEL 13 **)
   1.279 +by (safe_tac (!claset));
   1.280 +by (rename_tac "theta sigma gamma" 1);
   1.281 +by (rewrite_goals_tac [MoreGeneral_def]);
   1.282 +by (rotate_tac ~3 1);
   1.283 +by (eres_inst_tac [("x","gamma")] allE 1);
   1.284 +by (Asm_full_simp_tac 1);
   1.285 +by (etac exE 1);
   1.286 +by (rename_tac "delta" 1);
   1.287 +by (eres_inst_tac [("x","delta")] allE 1);
   1.288 +by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1);
   1.289 +(*Proving the subgoal*)
   1.290 +by (full_simp_tac (!simpset addsimps [subst_eq_iff]) 2);
   1.291 +by (blast_tac (!claset addIs [trans,sym] delrules [impCE]) 2);
   1.292 +by (blast_tac (!claset addIs [subst_trans, subst_cong, 
   1.293 +			      comp_assoc RS subst_sym]) 1);
   1.294 +qed_spec_mp "unify_gives_MGU";
   1.295 +
   1.296 +
   1.297 +(*---------------------------------------------------------------------------
   1.298 + * Unify returns idempotent substitutions, when it succeeds.
   1.299 + *---------------------------------------------------------------------------*)
   1.300 +goal Unify.thy "!theta. unify(P,Q) = Subst theta --> Idem theta";
   1.301 +by (res_inst_tac [("M1.0","P"),("M2.0","Q")] unifyInduct 1);
   1.302 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [Var_Idem] 
   1.303 +			             setloop split_tac[expand_if])));
   1.304 +(*Comb-Comb case*)
   1.305 +by (safe_tac (!claset));
   1.306 +by (subst_case_tac "unify(M1, M2)");
   1.307 +by (subst_case_tac "unify(N1 <| list, N2 <| list)");
   1.308 +by (hyp_subst_tac 1);
   1.309 +by prune_params_tac;
   1.310 +by (rename_tac "theta sigma" 1);
   1.311 +(** LEVEL 8 **)
   1.312 +by (dtac unify_gives_MGU 1);
   1.313 +by (dtac unify_gives_MGU 1);
   1.314 +by (rewrite_tac [MGUnifier_def]);
   1.315 +by (safe_tac (!claset));
   1.316 +by (rtac Idem_comp 1);
   1.317 +by (atac 1);
   1.318 +by (atac 1);
   1.319 +
   1.320 +by (eres_inst_tac [("x","q")] allE 1);
   1.321 +by (asm_full_simp_tac (!simpset addsimps [MoreGeneral_def]) 1);
   1.322 +by (safe_tac (!claset));
   1.323 +by (asm_full_simp_tac
   1.324 +    (!simpset addsimps [srange_iff, subst_eq_iff, Idem_def]) 1);
   1.325 +qed_spec_mp "unify_gives_Idem";
   1.326 +