TFL/examples/Subst/Unify.ML
 author nipkow Fri Feb 07 14:15:35 1997 +0100 (1997-02-07) changeset 2597 8b523426e1a4 parent 2113 21266526ac42 permissions -rw-r--r--
Modified proofs due to added triv_forall_equality.
```     1 (*---------------------------------------------------------------------------
```
```     2  * This file defines a nested unification algorithm, then proves that it
```
```     3  * terminates, then proves 2 correctness theorems: that when the algorithm
```
```     4  * succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution.
```
```     5  * Although the proofs may seem long, they are actually quite direct, in that
```
```     6  * the correctness and termination properties are not mingled as much as in
```
```     7  * previous proofs of this algorithm.
```
```     8  *
```
```     9  * Our approach for nested recursive functions is as follows:
```
```    10  *
```
```    11  *    0. Prove the wellfoundedness of the termination relation.
```
```    12  *    1. Prove the non-nested termination conditions.
```
```    13  *    2. Eliminate (0) and (1) from the recursion equations and the
```
```    14  *       induction theorem.
```
```    15  *    3. Prove the nested termination conditions by using the induction
```
```    16  *       theorem from (2) and by using the recursion equations from (2).
```
```    17  *       These are constrained by the nested termination conditions, but
```
```    18  *       things work out magically (by wellfoundedness of the termination
```
```    19  *       relation).
```
```    20  *    4. Eliminate the nested TCs from the results of (2).
```
```    21  *    5. Prove further correctness properties using the results of (4).
```
```    22  *
```
```    23  * Deeper nestings require iteration of steps (3) and (4).
```
```    24  *---------------------------------------------------------------------------*)
```
```    25
```
```    26 (* This is just a wrapper for the definition mechanism. *)
```
```    27 local fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[])));
```
```    28 in
```
```    29 fun Rfunc thy R eqs =
```
```    30    let val read = term_of o cread thy;
```
```    31     in Tfl.Rfunction thy (read R) (read eqs)
```
```    32     end
```
```    33 end;
```
```    34
```
```    35 (*---------------------------------------------------------------------------
```
```    36  * The algorithm.
```
```    37  *---------------------------------------------------------------------------*)
```
```    38 val {theory,induction,rules,tcs} =
```
```    39 Rfunc Unify.thy "R"
```
```    40   "(Unify(Const m, Const n)  = (if (m=n) then Subst[] else Fail))    & \
```
```    41 \  (Unify(Const m, Comb M N) = Fail)                                 & \
```
```    42 \  (Unify(Const m, Var v)    = Subst[(v,Const m)])                   & \
```
```    43 \  (Unify(Var v, M) = (if (Var v <: M) then Fail else Subst[(v,M)])) & \
```
```    44 \  (Unify(Comb M N, Const x) = Fail)                                 & \
```
```    45 \  (Unify(Comb M N, Var v) = (if (Var v <: Comb M N) then Fail  \
```
```    46 \                             else Subst[(v,Comb M N)]))             & \
```
```    47 \  (Unify(Comb M1 N1, Comb M2 N2) =  \
```
```    48 \     (case Unify(M1,M2) \
```
```    49 \       of Fail => Fail \
```
```    50 \        | Subst theta => (case Unify(N1 <| theta, N2 <| theta) \
```
```    51 \                           of Fail => Fail \
```
```    52 \                             | Subst sigma => Subst (theta <> sigma))))";
```
```    53
```
```    54 open Unify;
```
```    55
```
```    56 (*---------------------------------------------------------------------------
```
```    57  * A slightly augmented strip_tac.
```
```    58  *---------------------------------------------------------------------------*)
```
```    59 fun my_strip_tac i =
```
```    60    CHANGED (strip_tac i
```
```    61              THEN REPEAT ((etac exE ORELSE' etac conjE) i)
```
```    62              THEN TRY (hyp_subst_tac i));
```
```    63
```
```    64 (*---------------------------------------------------------------------------
```
```    65  * A slightly augmented fast_tac for sets. It handles the case where the
```
```    66  * top connective is "=".
```
```    67  *---------------------------------------------------------------------------*)
```
```    68 fun my_fast_set_tac i = (TRY(rtac set_ext i) THEN fast_tac set_cs i);
```
```    69
```
```    70
```
```    71 (*---------------------------------------------------------------------------
```
```    72  * Wellfoundedness of proper subset on finite sets.
```
```    73  *---------------------------------------------------------------------------*)
```
```    74 goalw Unify.thy [R0_def] "wf(R0)";
```
```    75 by (rtac ((wf_subset RS mp) RS mp) 1);
```
```    76 by (rtac wf_measure 1);
```
```    77 by(simp_tac(!simpset addsimps[measure_def,inv_image_def,symmetric less_def])1);
```
```    78 by (my_strip_tac 1);
```
```    79 by (forward_tac[ssubset_card] 1);
```
```    80 by (fast_tac set_cs 1);
```
```    81 val wf_R0 = result();
```
```    82
```
```    83
```
```    84 (*---------------------------------------------------------------------------
```
```    85  * Tactic for selecting and working on the first projection of R.
```
```    86  *---------------------------------------------------------------------------*)
```
```    87 fun R0_tac thms i =
```
```    88   (simp_tac (!simpset addsimps (thms@[R_def,lex_prod_def,
```
```    89                measure_def,inv_image_def,point_to_prod_def])) i THEN
```
```    90    REPEAT (rtac exI i) THEN
```
```    91    REPEAT ((rtac conjI THEN' rtac refl) i) THEN
```
```    92    rtac disjI1 i THEN
```
```    93    simp_tac (!simpset addsimps [R0_def,finite_vars_of]) i);
```
```    94
```
```    95
```
```    96
```
```    97 (*---------------------------------------------------------------------------
```
```    98  * Tactic for selecting and working on the second projection of R.
```
```    99  *---------------------------------------------------------------------------*)
```
```   100 fun R1_tac thms i =
```
```   101    (simp_tac (!simpset addsimps (thms@[R_def,lex_prod_def,
```
```   102                  measure_def,inv_image_def,point_to_prod_def])) i THEN
```
```   103     REPEAT (rtac exI i) THEN
```
```   104     REPEAT ((rtac conjI THEN' rtac refl) i) THEN
```
```   105     rtac disjI2 i THEN
```
```   106     asm_simp_tac (!simpset addsimps [R1_def,rprod_def]) i);
```
```   107
```
```   108
```
```   109 (*---------------------------------------------------------------------------
```
```   110  * The non-nested TC plus the wellfoundedness of R.
```
```   111  *---------------------------------------------------------------------------*)
```
```   112 Tfl.tgoalw Unify.thy [] rules;
```
```   113 by (rtac conjI 1);
```
```   114 (* TC *)
```
```   115 by (my_strip_tac 1);
```
```   116 by (cut_facts_tac [monotone_vars_of] 1);
```
```   117 by (asm_full_simp_tac(!simpset addsimps [subseteq_iff_subset_eq]) 1);
```
```   118 by (etac disjE 1);
```
```   119 by (R0_tac[] 1);
```
```   120 by (R1_tac[] 1);
```
```   121 by (simp_tac
```
```   122      (!simpset addsimps [measure_def,inv_image_def,less_eq,less_add_Suc1]) 1);
```
```   123
```
```   124 (* Wellfoundedness of R *)
```
```   125 by (simp_tac (!simpset addsimps [Unify.R_def,Unify.R1_def]) 1);
```
```   126 by (REPEAT (resolve_tac [wf_inv_image,wf_lex_prod,wf_R0,
```
```   127                          wf_rel_prod, wf_measure] 1));
```
```   128 val tc0 = result();
```
```   129
```
```   130
```
```   131 (*---------------------------------------------------------------------------
```
```   132  * Eliminate tc0 from the recursion equations and the induction theorem.
```
```   133  *---------------------------------------------------------------------------*)
```
```   134 val [tc,wfr] = Prim.Rules.CONJUNCTS tc0;
```
```   135 val rules1 = implies_intr_hyps rules;
```
```   136 val rules2 = wfr RS rules1;
```
```   137
```
```   138 val [a,b,c,d,e,f,g] = Prim.Rules.CONJUNCTS rules2;
```
```   139 val g' = tc RS (g RS mp);
```
```   140 val rules4 = standard (Prim.Rules.LIST_CONJ[a,b,c,d,e,f,g']);
```
```   141
```
```   142 val induction1 = implies_intr_hyps induction;
```
```   143 val induction2 = wfr RS induction1;
```
```   144 val induction3 = tc RS induction2;
```
```   145
```
```   146 val induction4 = standard
```
```   147  (rewrite_rule[fst_conv RS eq_reflection, snd_conv RS eq_reflection]
```
```   148    (induction3 RS (read_instantiate_sg (sign_of theory)
```
```   149       [("x","%p. Phi (fst p) (snd p)")] spec)));
```
```   150
```
```   151
```
```   152 (*---------------------------------------------------------------------------
```
```   153  * Some theorems about transitivity of WF combinators. Only the last
```
```   154  * (transR) is used, in the proof of termination. The others are generic and
```
```   155  * should maybe go somewhere.
```
```   156  *---------------------------------------------------------------------------*)
```
```   157 goalw WF1.thy [trans_def,lex_prod_def,mem_Collect_eq RS eq_reflection]
```
```   158            "trans R1 & trans R2 --> trans (R1 ** R2)";
```
```   159 by (my_strip_tac 1);
```
```   160 by (res_inst_tac [("x","a")] exI 1);
```
```   161 by (res_inst_tac [("x","a'a")] exI 1);
```
```   162 by (res_inst_tac [("x","b")] exI 1);
```
```   163 by (res_inst_tac [("x","b'a")] exI 1);
```
```   164 by (REPEAT (rewrite_tac [Pair_eq RS eq_reflection] THEN my_strip_tac 1));
```
```   165 by (Simp_tac 1);
```
```   166 by (REPEAT (etac disjE 1));
```
```   167 by (rtac disjI1 1);
```
```   168 by (ALLGOALS (fast_tac set_cs));
```
```   169 val trans_lex_prod = result() RS mp;
```
```   170
```
```   171
```
```   172 goalw WF1.thy [trans_def,rprod_def,mem_Collect_eq RS eq_reflection]
```
```   173            "trans R1 & trans R2 --> trans (rprod R1  R2)";
```
```   174 by (my_strip_tac 1);
```
```   175 by (res_inst_tac [("x","a")] exI 1);
```
```   176 by (res_inst_tac [("x","a'a")] exI 1);
```
```   177 by (res_inst_tac [("x","b")] exI 1);
```
```   178 by (res_inst_tac [("x","b'a")] exI 1);
```
```   179 by (REPEAT (rewrite_tac [Pair_eq RS eq_reflection] THEN my_strip_tac 1));
```
```   180 by (Simp_tac 1);
```
```   181 by (fast_tac set_cs 1);
```
```   182 val trans_rprod = result() RS mp;
```
```   183
```
```   184
```
```   185 goalw Unify.thy [trans_def,inv_image_def,mem_Collect_eq RS eq_reflection]
```
```   186  "trans r --> trans (inv_image r f)";
```
```   187 by (rewrite_tac [fst_conv RS eq_reflection, snd_conv RS eq_reflection]);
```
```   188 by (fast_tac set_cs 1);
```
```   189 val trans_inv_image = result() RS mp;
```
```   190
```
```   191 goalw Unify.thy [R0_def, trans_def, mem_Collect_eq RS eq_reflection]
```
```   192  "trans R0";
```
```   193 by (rewrite_tac [fst_conv RS eq_reflection,snd_conv RS eq_reflection,
```
```   194                  ssubset_def, set_eq_subset RS eq_reflection]);
```
```   195 by (fast_tac set_cs 1);
```
```   196 val trans_R0 = result();
```
```   197
```
```   198 goalw Unify.thy [R_def,R1_def,measure_def] "trans R";
```
```   199 by (REPEAT (resolve_tac[trans_inv_image,trans_lex_prod,conjI, trans_R0,
```
```   200                         trans_rprod, trans_inv_image, trans_trancl] 1));
```
```   201 val transR = result();
```
```   202
```
```   203
```
```   204 (*---------------------------------------------------------------------------
```
```   205  * The following lemma is used in the last step of the termination proof for
```
```   206  * the nested call in Unify. Loosely, it says that R doesn't care so much
```
```   207  * about term structure.
```
```   208  *---------------------------------------------------------------------------*)
```
```   209 goalw Unify.thy [R_def,lex_prod_def, inv_image_def,point_to_prod_def]
```
```   210      "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : R --> \
```
```   211     \ ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : R";
```
```   212 by (Simp_tac 1);
```
```   213 by (rtac conjI 1);
```
```   214 by (strip_tac 1);
```
```   215 by (rtac disjI1 1);
```
```   216 by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \
```
```   217                 \  (vars_of D Un vars_of E Un vars_of F)) = \
```
```   218                 \ (vars_of A Un (vars_of B Un vars_of C) Un \
```
```   219                 \  (vars_of D Un (vars_of E Un vars_of F)))" 1);
```
```   220 by (my_fast_set_tac 2);
```
```   221 by (Asm_simp_tac 1);
```
```   222 by (strip_tac 1);
```
```   223 by (rtac disjI2 1);
```
```   224 by (etac conjE 1);
```
```   225 by (Asm_simp_tac 1);
```
```   226 by (rtac conjI 1);
```
```   227 by (my_fast_set_tac 1);
```
```   228 by (asm_full_simp_tac (!simpset addsimps [R1_def, measure_def, rprod_def,
```
```   229                           less_eq, inv_image_def,add_assoc]) 1);
```
```   230 val Rassoc = result() RS mp;
```
```   231
```
```   232 (*---------------------------------------------------------------------------
```
```   233  * Rewriting support.
```
```   234  *---------------------------------------------------------------------------*)
```
```   235
```
```   236 val termin_ss = (!simpset addsimps (srange_iff::(subst_rews@al_rews)));
```
```   237
```
```   238
```
```   239 (*---------------------------------------------------------------------------
```
```   240  * This lemma proves the nested termination condition for the base cases
```
```   241  * 3, 4, and 6. It's a clumsy formulation (requiring two conjuncts, each with
```
```   242  * exactly the same proof) of a more general theorem.
```
```   243  *---------------------------------------------------------------------------*)
```
```   244 goal theory "(~(Var x <: M)) --> [(x, M)] = theta -->       \
```
```   245 \ (! N1 N2. (((N1 <| theta, N2 <| theta), (Comb M N1, Comb (Var x) N2)) : R) \
```
```   246 \       &   (((N1 <| theta, N2 <| theta), (Comb(Var x) N1, Comb M N2)) : R))";
```
```   247 by (my_strip_tac 1);
```
```   248 by (case_tac "Var x = M" 1);
```
```   249 by (hyp_subst_tac 1);
```
```   250 by (case_tac "x:(vars_of N1 Un vars_of N2)" 1);
```
```   251 let val case1 =
```
```   252    EVERY1[R1_tac[id_subst_lemma], rtac conjI, my_fast_set_tac,
```
```   253           REPEAT o (rtac exI), REPEAT o (rtac conjI THEN' rtac refl),
```
```   254           simp_tac (!simpset addsimps [measure_def,inv_image_def,less_eq])];
```
```   255 in by (rtac conjI 1);
```
```   256    by case1;
```
```   257    by case1
```
```   258 end;
```
```   259
```
```   260 let val case2 =
```
```   261    EVERY1[R0_tac[id_subst_lemma],
```
```   262           simp_tac (!simpset addsimps [ssubset_def,set_eq_subset]),
```
```   263           fast_tac set_cs]
```
```   264 in by (rtac conjI 1);
```
```   265    by case2;
```
```   266    by case2
```
```   267 end;
```
```   268
```
```   269 let val case3 =
```
```   270  EVERY1 [R0_tac[],
```
```   271         cut_inst_tac [("s2","[(x, M)]"), ("v2", "x"), ("t2","N1")] Var_elim]
```
```   272  THEN ALLGOALS(asm_simp_tac(termin_ss addsimps [vars_iff_occseq]))
```
```   273  THEN cut_inst_tac [("s2","[(x, M)]"),("v2", "x"), ("t2","N2")] Var_elim 1
```
```   274  THEN ALLGOALS(asm_simp_tac(termin_ss addsimps [vars_iff_occseq]))
```
```   275  THEN EVERY1 [simp_tac (HOL_ss addsimps [ssubset_def]),
```
```   276              rtac conjI, simp_tac (HOL_ss addsimps [subset_iff]),
```
```   277              my_strip_tac, etac UnE, dtac Var_intro]
```
```   278  THEN dtac Var_intro 2
```
```   279  THEN ALLGOALS (asm_full_simp_tac (termin_ss addsimps [set_eq_subset]))
```
```   280  THEN TRYALL (fast_tac set_cs)
```
```   281 in
```
```   282   by (rtac conjI 1);
```
```   283   by case3;
```
```   284   by case3
```
```   285 end;
```
```   286 val var_elimR = result() RS mp RS mp RS spec RS spec;
```
```   287
```
```   288
```
```   289 val Some{nchotomy = subst_nchotomy,...} = assoc(!datatypes,"subst");
```
```   290
```
```   291 (*---------------------------------------------------------------------------
```
```   292  * Do a case analysis on something of type 'a subst.
```
```   293  *---------------------------------------------------------------------------*)
```
```   294
```
```   295 fun Subst_case_tac theta =
```
```   296 (cut_inst_tac theta (standard (Prim.Rules.SPEC_ALL subst_nchotomy)) 1
```
```   297   THEN etac disjE 1
```
```   298   THEN rotate_tac ~1 1
```
```   299   THEN Asm_full_simp_tac 1
```
```   300   THEN etac exE 1
```
```   301   THEN rotate_tac ~1 1
```
```   302   THEN Asm_full_simp_tac 1);
```
```   303
```
```   304
```
```   305 goals_limit := 1;
```
```   306
```
```   307 (*---------------------------------------------------------------------------
```
```   308  * The nested TC. Proved by recursion induction.
```
```   309  *---------------------------------------------------------------------------*)
```
```   310 goalw_cterm []
```
```   311      (hd(tl(tl(map (cterm_of (sign_of theory) o USyntax.mk_prop) tcs))));
```
```   312 (*---------------------------------------------------------------------------
```
```   313  * The extracted TC needs the scope of its quantifiers adjusted, so our
```
```   314  * first step is to restrict the scopes of N1 and N2.
```
```   315  *---------------------------------------------------------------------------*)
```
```   316 by (subgoal_tac "!M1 M2 theta.  \
```
```   317  \     Unify (M1, M2) = Subst theta --> \
```
```   318  \    (!N1 N2. ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R)" 1);
```
```   319 by (fast_tac HOL_cs 1);
```
```   320 by (rtac allI 1);
```
```   321 by (rtac allI 1);
```
```   322 (* Apply induction *)
```
```   323 by (res_inst_tac [("xa","M1"),("x","M2")]
```
```   324                  (standard (induction4 RS mp RS spec RS spec)) 1);
```
```   325 by (simp_tac (!simpset addsimps (rules4::(subst_rews@al_rews))
```
```   326                        setloop (split_tac [expand_if])) 1);
```
```   327 (* 1 *)
```
```   328 by (rtac conjI 1);
```
```   329 by (my_strip_tac 1);
```
```   330 by (R1_tac[subst_Nil] 1);
```
```   331 by (REPEAT (rtac exI 1) THEN REPEAT ((rtac conjI THEN' rtac refl) 1));
```
```   332 by (simp_tac (!simpset addsimps [measure_def,inv_image_def,less_eq]) 1);
```
```   333
```
```   334 (* 3 *)
```
```   335 by (rtac conjI 1);
```
```   336 by (my_strip_tac 1);
```
```   337 by (rtac (Prim.Rules.CONJUNCT1 var_elimR) 1);
```
```   338 by (Simp_tac 1);
```
```   339 by (rtac refl 1);
```
```   340
```
```   341 (* 4 *)
```
```   342 by (rtac conjI 1);
```
```   343 by (strip_tac 1);
```
```   344 by (rtac (Prim.Rules.CONJUNCT2 var_elimR) 1);
```
```   345 by (assume_tac 1);
```
```   346 by (rtac refl 1);
```
```   347
```
```   348 (* 6 *)
```
```   349 by (rtac conjI 1);
```
```   350 by (rewrite_tac [symmetric (occs_Comb RS eq_reflection)]);
```
```   351 by (my_strip_tac 1);
```
```   352 by (rtac (Prim.Rules.CONJUNCT1 var_elimR) 1);
```
```   353 by (Asm_simp_tac 1);
```
```   354 by (rtac refl 1);
```
```   355
```
```   356 (* 7 *)
```
```   357 by (REPEAT (rtac allI 1));
```
```   358 by (rtac impI 1);
```
```   359 by (etac conjE 1);
```
```   360 by (Subst_case_tac [("v","Unify(M1, M2)")]);
```
```   361 by (rename_tac "theta" 1);
```
```   362
```
```   363 by (Subst_case_tac [("v","Unify(N1 <| theta, N2 <| theta)")]);
```
```   364 by (rename_tac "sigma" 1);
```
```   365 by (REPEAT (rtac allI 1));
```
```   366 by (rename_tac "P Q" 1);
```
```   367 by (simp_tac (HOL_ss addsimps [subst_comp]) 1);
```
```   368 by(rtac(rewrite_rule[trans_def] transR RS spec RS spec RS spec RS mp RS mp) 1);
```
```   369 by (fast_tac HOL_cs 1);
```
```   370 by (simp_tac (HOL_ss addsimps [symmetric (subst_Comb RS eq_reflection)]) 1);
```
```   371 by (subgoal_tac "((Comb N1 P <| theta, Comb N2 Q <| theta), \
```
```   372                 \ (Comb M1 (Comb N1 P), Comb M2 (Comb N2 Q))) :R" 1);
```
```   373 by (asm_simp_tac HOL_ss 2);
```
```   374
```
```   375 by (rtac Rassoc 1);
```
```   376 by (assume_tac 1);
```
```   377 val Unify_TC2 = result();
```
```   378
```
```   379
```
```   380 (*---------------------------------------------------------------------------
```
```   381  * Now for elimination of nested TC from rules and induction. This step
```
```   382  * would be easier if "rewrite_rule" used context.
```
```   383  *---------------------------------------------------------------------------*)
```
```   384 goal theory
```
```   385  "(Unify (Comb M1 N1, Comb M2 N2) =  \
```
```   386 \   (case Unify (M1, M2) of Fail => Fail \
```
```   387 \    | Subst theta => \
```
```   388 \        (case if ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R \
```
```   389 \              then Unify (N1 <| theta, N2 <| theta) else @ z. True of \
```
```   390 \        Fail => Fail | Subst sigma => Subst (theta <> sigma)))) \
```
```   391 \  = \
```
```   392 \ (Unify (Comb M1 N1, Comb M2 N2) = \
```
```   393 \   (case Unify (M1, M2)  \
```
```   394 \      of Fail => Fail \
```
```   395 \      | Subst theta => (case Unify (N1 <| theta, N2 <| theta) \
```
```   396 \                          of Fail => Fail  \
```
```   397 \                           | Subst sigma => Subst (theta <> sigma))))";
```
```   398 by (cut_inst_tac [("v","Unify(M1, M2)")]
```
```   399                  (standard (Prim.Rules.SPEC_ALL subst_nchotomy)) 1);
```
```   400 by (etac disjE 1);
```
```   401 by (Asm_simp_tac 1);
```
```   402 by (etac exE 1);
```
```   403 by (Asm_simp_tac 1);
```
```   404 by (cut_inst_tac
```
```   405      [("x","list"), ("xb","N1"), ("xa","N2"),("xc","M2"), ("xd","M1")]
```
```   406      (standard(Unify_TC2 RS spec RS spec RS spec RS spec RS spec)) 1);
```
```   407 by (Asm_full_simp_tac 1);
```
```   408 val Unify_rec_simpl = result() RS eq_reflection;
```
```   409
```
```   410 val Unify_rules = rewrite_rule[Unify_rec_simpl] rules4;
```
```   411
```
```   412
```
```   413 goal theory
```
```   414  "(! M1 N1 M2 N2.  \
```
```   415 \       (! theta.  \
```
```   416 \           Unify (M1, M2) = Subst theta -->  \
```
```   417 \           ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R -->  \
```
```   418 \           ?Phi (N1 <| theta) (N2 <| theta)) & ?Phi M1 M2 -->  \
```
```   419 \       ?Phi (Comb M1 N1) (Comb M2 N2))  \
```
```   420 \    =  \
```
```   421 \ (! M1 N1 M2 N2.  \
```
```   422 \       (! theta.  \
```
```   423 \           Unify (M1, M2) = Subst theta -->  \
```
```   424 \           ?Phi (N1 <| theta) (N2 <| theta)) & ?Phi M1 M2 -->  \
```
```   425 \       ?Phi (Comb M1 N1) (Comb M2 N2))";
```
```   426 by (simp_tac (HOL_ss addsimps [Unify_TC2]) 1);
```
```   427 val Unify_induction = rewrite_rule[result() RS eq_reflection] induction4;
```
```   428
```
```   429
```
```   430
```
```   431 (*---------------------------------------------------------------------------
```
```   432  * Correctness. Notice that idempotence is not needed to prove that the
```
```   433  * algorithm terminates and is not needed to prove the algorithm correct,
```
```   434  * if you are only interested in an MGU. This is in contrast to the
```
```   435  * approach of M&W, who used idempotence and MGU-ness in the termination proof.
```
```   436  *---------------------------------------------------------------------------*)
```
```   437
```
```   438 goal theory "!theta. Unify (P,Q) = Subst theta --> MGUnifier theta P Q";
```
```   439 by (res_inst_tac [("xa","P"),("x","Q")]
```
```   440                  (standard (Unify_induction RS mp RS spec RS spec)) 1);
```
```   441 by (simp_tac (!simpset addsimps [Unify_rules]
```
```   442                        setloop (split_tac [expand_if])) 1);
```
```   443 (*1*)
```
```   444 by (rtac conjI 1);
```
```   445 by (REPEAT (rtac allI 1));
```
```   446 by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1);
```
```   447 by (my_strip_tac 1);
```
```   448 by (rtac MoreGen_Nil 1);
```
```   449
```
```   450 (*3*)
```
```   451 by (rtac conjI 1);
```
```   452 by (my_strip_tac 1);
```
```   453 by (rtac (mgu_sym RS iffD1) 1);
```
```   454 by (rtac MGUnifier_Var 1);
```
```   455 by (Simp_tac 1);
```
```   456
```
```   457 (*4*)
```
```   458 by (rtac conjI 1);
```
```   459 by (my_strip_tac 1);
```
```   460 by (rtac MGUnifier_Var 1);
```
```   461 by (assume_tac 1);
```
```   462
```
```   463 (*6*)
```
```   464 by (rtac conjI 1);
```
```   465 by (rewrite_tac NNF_rews);
```
```   466 by (my_strip_tac 1);
```
```   467 by (rtac (mgu_sym RS iffD1) 1);
```
```   468 by (rtac MGUnifier_Var 1);
```
```   469 by (Asm_simp_tac 1);
```
```   470
```
```   471 (*7*)
```
```   472 by (safe_tac HOL_cs);
```
```   473 by (Subst_case_tac [("v","Unify(M1, M2)")]);
```
```   474 by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]);
```
```   475 by (hyp_subst_tac 1);
```
```   476 by (asm_full_simp_tac(HOL_ss addsimps [MGUnifier_def,Unifier_def])1);
```
```   477 by (asm_simp_tac (!simpset addsimps [subst_comp]) 1); (* It's a unifier.*)
```
```   478
```
```   479 by (safe_tac HOL_cs);
```
```   480 by (rename_tac "theta sigma gamma" 1);
```
```   481
```
```   482 by (rewrite_tac [MoreGeneral_def]);
```
```   483 by (rotate_tac ~3 1);
```
```   484 by (eres_inst_tac [("x","gamma")] allE 1);
```
```   485 by (Asm_full_simp_tac 1);
```
```   486 by (etac exE 1);
```
```   487 by (rename_tac "delta" 1);
```
```   488 by (eres_inst_tac [("x","delta")] allE 1);
```
```   489 by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1);
```
```   490 by (dtac mp 1);
```
```   491 by (atac 1);
```
```   492 by (etac exE 1);
```
```   493 by (rename_tac "rho" 1);
```
```   494
```
```   495 by (rtac exI 1);
```
```   496 by (rtac subst_trans 1);
```
```   497 by (assume_tac 1);
```
```   498
```
```   499 by (rtac subst_trans 1);
```
```   500 by (rtac (comp_assoc RS subst_sym) 2);
```
```   501 by (rtac subst_cong 1);
```
```   502 by (rtac (refl RS subst_refl) 1);
```
```   503 by (assume_tac 1);
```
```   504
```
```   505 by (asm_full_simp_tac (!simpset addsimps [subst_eq_iff,subst_comp]) 1);
```
```   506 by (forw_inst_tac [("x","N1")] spec 1);
```
```   507 by (dres_inst_tac [("x","N2")] spec 1);
```
```   508 by (Asm_full_simp_tac 1);
```
```   509 val Unify_gives_MGU = standard(result() RS spec RS mp);
```
```   510
```
```   511
```
```   512 (*---------------------------------------------------------------------------
```
```   513  * Unify returns idempotent substitutions, when it succeeds.
```
```   514  *---------------------------------------------------------------------------*)
```
```   515 goal theory "!theta. Unify (P,Q) = Subst theta --> Idem theta";
```
```   516 by (res_inst_tac [("xa","P"),("x","Q")]
```
```   517                  (standard (Unify_induction RS mp RS spec RS spec)) 1);
```
```   518 (* Blows away all base cases automatically *)
```
```   519 by (simp_tac (!simpset addsimps [Unify_rules,Idem_Nil,Var_Idem]
```
```   520                        setloop (split_tac [expand_if])) 1);
```
```   521
```
```   522 (*7*)
```
```   523 by (safe_tac HOL_cs);
```
```   524 by (Subst_case_tac [("v","Unify(M1, M2)")]);
```
```   525 by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]);
```
```   526 by (hyp_subst_tac 1);
```
```   527 by prune_params_tac;
```
```   528 by (rename_tac "theta sigma" 1);
```
```   529
```
```   530 by (dtac Unify_gives_MGU 1);
```
```   531 by (dtac Unify_gives_MGU 1);
```
```   532 by (rewrite_tac [MGUnifier_def]);
```
```   533 by (my_strip_tac 1);
```
```   534 by (rtac Idem_comp 1);
```
```   535 by (atac 1);
```
```   536 by (atac 1);
```
```   537
```
```   538 by (my_strip_tac 1);
```
```   539 by (eres_inst_tac [("x","q")] allE 1);
```
```   540 by (Asm_full_simp_tac 1);
```
```   541 by (rewrite_tac [MoreGeneral_def]);
```
```   542 by (my_strip_tac 1);
```
```   543 by (asm_full_simp_tac(termin_ss addsimps [subst_eq_iff,subst_comp,Idem_def])1);
```
```   544 val Unify_gives_Idem = result() RS spec RS mp;
```
```   545
```
```   546
```
```   547
```
```   548 (*---------------------------------------------------------------------------
```
```   549  * Exercise. The given algorithm is a bit inelegant. What about the
```
```   550  * following "improvement", which adds a few recursive calls in former
```
```   551  * base cases? It seems that the termination relation needs another
```
```   552  * case in the lexico. product.
```
```   553
```
```   554 val {theory,induction,rules,tcs,typechecks} =
```
```   555 Rfunc Unify.thy ??
```
```   556   `(Unify(Const m, Const n)  = (if (m=n) then Subst[] else Fail))    &
```
```   557    (Unify(Const m, Comb M N) = Fail)                                 &
```
```   558    (Unify(Const m, Var v)    = Unify(Var v, Const m))                &
```
```   559    (Unify(Var v, M) = (if (Var v <: M) then Fail else Subst[(v,M)])) &
```
```   560    (Unify(Comb M N, Const x) = Fail)                                 &
```
```   561    (Unify(Comb M N, Var v) = Unify(Var v, Comb M N))                 &
```
```   562    (Unify(Comb M1 N1, Comb M2 N2) =
```
```   563       (case Unify(M1,M2)
```
```   564         of Fail => Fail
```
```   565          | Subst theta => (case Unify(N1 <| theta, N2 <| theta)
```
```   566                             of Fail => Fail
```
```   567                              | Subst sigma => Subst (theta <> sigma))))`;
```
```   568
```
```   569  *---------------------------------------------------------------------------*)
```