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