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