src/HOL/Subst/Unifier.ML
author clasohm
Wed Mar 13 11:55:25 1996 +0100 (1996-03-13 ago)
changeset 1574 5a63ab90ee8a
parent 1465 5d7a7e439cec
child 1673 d22110ddd0af
permissions -rw-r--r--
modified primrec so it can be used in MiniML/Type.thy
clasohm@1465
     1
(*  Title:      HOL/Subst/unifier.ML
clasohm@1266
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@968
     4
    Copyright   1993  University of Cambridge
clasohm@968
     5
clasohm@968
     6
For unifier.thy.
clasohm@968
     7
Properties of unifiers.
clasohm@968
     8
Cases for partial correctness of algorithm and conditions for termination.
clasohm@968
     9
*)
clasohm@968
    10
clasohm@968
    11
open Unifier;
clasohm@968
    12
clasohm@968
    13
val unify_defs =
clasohm@968
    14
    [Idem_def,Unifier_def,MoreGeneral_def,MGUnifier_def,MGIUnifier_def];
clasohm@968
    15
clasohm@968
    16
(**** Unifiers ****)
clasohm@968
    17
clasohm@968
    18
goalw Unifier.thy [Unifier_def] "Unifier s t u = (t <| s = u <| s)";
clasohm@968
    19
by (rtac refl 1);
clasohm@968
    20
qed "Unifier_iff";
clasohm@968
    21
clasohm@968
    22
goal Unifier.thy
clasohm@968
    23
    "Unifier s (Comb t u) (Comb v w) --> Unifier s t v & Unifier s u w";
clasohm@968
    24
by (simp_tac (subst_ss addsimps [Unifier_iff]) 1);
clasohm@968
    25
val Unifier_Comb  = store_thm("Unifier_Comb", result() RS mp RS conjE);
clasohm@968
    26
clasohm@968
    27
goal Unifier.thy
clasohm@968
    28
  "~v : vars_of(t) --> ~v : vars_of(u) -->Unifier s t u --> \
clasohm@972
    29
\  Unifier ((v,r)#s) t u";
clasohm@968
    30
by (simp_tac (subst_ss addsimps [Unifier_iff,repl_invariance]) 1);
clasohm@968
    31
val Cons_Unifier  = store_thm("Cons_Unifier", result() RS mp RS mp RS mp);
clasohm@968
    32
clasohm@968
    33
(**** Most General Unifiers ****)
clasohm@968
    34
clasohm@968
    35
goalw Unifier.thy [MoreGeneral_def]  "r >> s = (EX q. s =s= r <> q)";
clasohm@968
    36
by (rtac refl 1);
clasohm@968
    37
qed "MoreGen_iff";
clasohm@968
    38
clasohm@968
    39
goal Unifier.thy  "[] >> s";
clasohm@968
    40
by (simp_tac (subst_ss addsimps [MoreGen_iff]) 1);
clasohm@968
    41
by (fast_tac (set_cs addIs [refl RS subst_refl]) 1);
clasohm@968
    42
qed "MoreGen_Nil";
clasohm@968
    43
clasohm@968
    44
goalw Unifier.thy unify_defs
clasohm@968
    45
    "MGUnifier s t u = (ALL r.Unifier r t u = s >> r)";
clasohm@968
    46
by (REPEAT (ares_tac [iffI,allI] 1 ORELSE 
clasohm@968
    47
            eresolve_tac [conjE,allE,mp,exE,ssubst_subst2] 1));
clasohm@968
    48
by (asm_simp_tac (subst_ss addsimps [subst_comp]) 1);
clasohm@968
    49
by (fast_tac (set_cs addIs [comp_Nil RS sym RS subst_refl]) 1);
clasohm@968
    50
qed "MGU_iff";
clasohm@968
    51
clasohm@968
    52
val [prem] = goal Unifier.thy
clasohm@972
    53
     "~ Var(v) <: t ==> MGUnifier [(v,t)] (Var v) t";
clasohm@968
    54
by (simp_tac (subst_ss addsimps [MGU_iff,MoreGen_iff,Unifier_iff]) 1);
clasohm@968
    55
by (REPEAT_SOME (step_tac set_cs));
clasohm@968
    56
by (etac subst 1);
clasohm@968
    57
by (etac ssubst_subst2 2);
clasohm@968
    58
by (rtac (Cons_trivial RS subst_sym) 1);
clasohm@968
    59
by (simp_tac (subst_ss addsimps [prem RS Var_not_occs,Var_subst]) 1);
clasohm@968
    60
qed "MGUnifier_Var";
clasohm@968
    61
clasohm@968
    62
(**** Most General Idempotent Unifiers ****)
clasohm@968
    63
clasohm@968
    64
goal Unifier.thy "r <> r =s= r --> s =s= r <> q --> r <> s =s= s";
clasohm@968
    65
by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1);
clasohm@968
    66
val MGIU_iff_lemma  = store_thm("MGIU_iff_lemma", result() RS mp RS mp);
clasohm@968
    67
clasohm@968
    68
goalw Unifier.thy unify_defs
clasohm@968
    69
 "MGIUnifier s t u = \
clasohm@968
    70
\  (Idem(s) & Unifier s t u & (ALL r.Unifier r t u --> s<>r=s=r))";
clasohm@968
    71
by (fast_tac (set_cs addEs [subst_sym,MGIU_iff_lemma]) 1);
clasohm@968
    72
qed "MGIU_iff";
clasohm@968
    73
clasohm@968
    74
(**** Idempotence ****)
clasohm@968
    75
clasohm@968
    76
goalw Unifier.thy unify_defs "Idem(s) = (s <> s =s= s)";
clasohm@968
    77
by (rtac refl 1);
clasohm@968
    78
qed "raw_Idem_iff";
clasohm@968
    79
clasohm@968
    80
goal Unifier.thy "Idem(s) = (sdom(s) Int srange(s) = {})";
clasohm@968
    81
by (simp_tac (subst_ss addsimps [raw_Idem_iff,subst_eq_iff,subst_comp,
clasohm@968
    82
                                invariance,dom_range_disjoint])1);
clasohm@968
    83
qed "Idem_iff";
clasohm@968
    84
clasohm@968
    85
goal Unifier.thy "Idem([])";
clasohm@968
    86
by (simp_tac (subst_ss addsimps [raw_Idem_iff,refl RS subst_refl]) 1);
clasohm@968
    87
qed "Idem_Nil";
clasohm@968
    88
clasohm@972
    89
goal Unifier.thy "~ (Var(v) <: t) --> Idem([(v,t)])";
clasohm@968
    90
by (simp_tac (subst_ss addsimps [Var_subst,vars_iff_occseq,Idem_iff,srange_iff]
clasohm@968
    91
                       setloop (split_tac [expand_if])) 1);
clasohm@968
    92
by (fast_tac set_cs 1);
clasohm@968
    93
val Var_Idem  = store_thm("Var_Idem", result() RS mp);
clasohm@968
    94
clasohm@968
    95
val [prem] = goalw Unifier.thy [Idem_def]
clasohm@968
    96
     "Idem(r) ==>  Unifier s (t <| r) (u <| r) --> Unifier (r <> s) (t <| r) (u <| r)";
clasohm@968
    97
by (simp_tac (subst_ss addsimps 
clasohm@1465
    98
              [Unifier_iff,subst_comp,prem RS comp_subst_subst]) 1);
clasohm@968
    99
val Unifier_Idem_subst  = store_thm("Unifier_Idem_subst", result() RS mp);
clasohm@968
   100
clasohm@968
   101
val [prem] = goal Unifier.thy 
clasohm@968
   102
     "r <> s =s= s ==>  Unifier s t u --> Unifier s (t <| r) (u <| r)";
clasohm@968
   103
by (simp_tac (subst_ss addsimps 
clasohm@1465
   104
              [Unifier_iff,subst_comp,prem RS comp_subst_subst]) 1);
clasohm@968
   105
val Unifier_comp_subst  = store_thm("Unifier_comp_subst", result() RS mp);
clasohm@968
   106
clasohm@968
   107
(*** The domain of a MGIU is a subset of the variables in the terms ***)
clasohm@968
   108
(***      NB this and one for range are only needed for termination ***)
clasohm@968
   109
clasohm@968
   110
val [prem] = goal Unifier.thy
clasohm@968
   111
    "~ vars_of(Var(x) <| r) = vars_of(Var(x) <| s) ==> ~r =s= s";
clasohm@968
   112
by (rtac (prem RS contrapos) 1);
clasohm@968
   113
by (fast_tac (set_cs addEs [subst_subst2]) 1);
clasohm@968
   114
qed "lemma_lemma";
clasohm@968
   115
clasohm@968
   116
val prems = goal Unifier.thy 
clasohm@968
   117
    "x : sdom(s) -->  ~x : srange(s) --> \
clasohm@972
   118
\   ~vars_of(Var(x) <| s<> (x,Var(x))#s) = \
clasohm@972
   119
\      vars_of(Var(x) <| (x,Var(x))#s)";
clasohm@968
   120
by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
clasohm@968
   121
by (REPEAT (resolve_tac [impI,disjI2] 1));
clasohm@968
   122
by(res_inst_tac [("x","x")] exI 1);
clasohm@1465
   123
by (rtac conjI 1);
clasohm@968
   124
by (asm_simp_tac (subst_ss addsimps [Var_elim,subst_comp,repl_invariance]) 1);
clasohm@968
   125
by (asm_simp_tac (subst_ss addsimps [Var_subst]) 1);
clasohm@968
   126
val MGIU_sdom_lemma = store_thm("MGIU_sdom_lemma", result() RS mp RS mp RS lemma_lemma RS notE);
clasohm@968
   127
clasohm@968
   128
goal Unifier.thy "MGIUnifier s t u --> sdom(s) <= vars_of(t) Un vars_of(u)";
clasohm@968
   129
by (subgoal_tac "! P Q.(P | Q) = (~( ~P & ~Q))" 1);
clasohm@968
   130
by (asm_simp_tac (subst_ss addsimps [MGIU_iff,Idem_iff,subset_iff]) 1);
clasohm@968
   131
by (safe_tac set_cs);
clasohm@968
   132
by (eresolve_tac ([spec] RL [impE]) 1);
clasohm@968
   133
by (rtac Cons_Unifier 1);
clasohm@968
   134
by (ALLGOALS (fast_tac (set_cs addIs [Cons_Unifier,MGIU_sdom_lemma])));
clasohm@968
   135
val MGIU_sdom  = store_thm("MGIU_sdom", result() RS mp);
clasohm@968
   136
clasohm@968
   137
(*** The range of a MGIU is a subset of the variables in the terms ***)
clasohm@968
   138
clasohm@968
   139
val prems = goal HOL.thy  "P = Q ==> (~P) = (~Q)";
clasohm@1266
   140
by (simp_tac (subst_ss addsimps prems) 1);
clasohm@968
   141
qed "not_cong";
clasohm@968
   142
clasohm@968
   143
val prems = goal Unifier.thy 
clasohm@968
   144
   "~w=x --> x : vars_of(Var(w) <| s) --> w : sdom(s) --> ~w : srange(s) --> \
clasohm@972
   145
\   ~vars_of(Var(w) <| s<> (x,Var(w))#s) = \
clasohm@972
   146
\   vars_of(Var(w) <| (x,Var(w))#s)";
clasohm@968
   147
by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
clasohm@968
   148
by (REPEAT (resolve_tac [impI,disjI1] 1));
clasohm@968
   149
by(res_inst_tac [("x","w")] exI 1);
clasohm@968
   150
by (ALLGOALS (asm_simp_tac (subst_ss addsimps  [Var_elim,subst_comp,
clasohm@968
   151
                vars_var_iff RS not_cong RS iffD2 RS repl_invariance]) ));
clasohm@968
   152
by (fast_tac (set_cs addIs [Var_in_subst]) 1);
clasohm@968
   153
val MGIU_srange_lemma  = store_thm("MGIU_srange_lemma", result() RS mp RS mp RS mp RS mp RS lemma_lemma RS notE);
clasohm@968
   154
clasohm@968
   155
goal Unifier.thy "MGIUnifier s t u --> srange(s) <= vars_of(t) Un vars_of(u)";
clasohm@968
   156
by (subgoal_tac "! P Q.(P | Q) = (~( ~P & ~Q))" 1);
clasohm@968
   157
by (asm_simp_tac (subst_ss addsimps [MGIU_iff,srange_iff,subset_iff]) 1);
clasohm@968
   158
by (simp_tac (subst_ss addsimps [Idem_iff]) 1);
clasohm@968
   159
by (safe_tac set_cs);
clasohm@968
   160
by (eresolve_tac ([spec] RL [impE]) 1);
clasohm@968
   161
by (rtac Cons_Unifier 1);
clasohm@968
   162
by (imp_excluded_middle_tac "w=ta" 4);
clasohm@968
   163
by (fast_tac (set_cs addEs [MGIU_srange_lemma]) 5);
clasohm@968
   164
by (ALLGOALS (fast_tac (set_cs addIs [Var_elim2])));
clasohm@968
   165
val MGIU_srange = store_thm("MGIU_srange", result() RS mp);
clasohm@968
   166
clasohm@968
   167
(*************** Correctness of a simple unification algorithm ***************)
clasohm@968
   168
(*                                                                           *)
clasohm@968
   169
(*  fun unify Const(m) Const(n) = if m=n then Nil else Fail                  *)
clasohm@968
   170
(*    | unify Const(m) _        = Fail                                       *)
clasohm@972
   171
(*    | unify Var(v)   t        = if Var(v)<:t then Fail else (v,t)#Nil      *)
clasohm@968
   172
(*    | unify Comb(t,u) Const(n) = Fail                                      *)
clasohm@968
   173
(*    | unify Comb(t,u) Var(v)  = if Var(v) <: Comb(t,u) then Fail           *)
clasohm@972
   174
(*                                               else (v,Comb(t,u)#Nil       *)
clasohm@968
   175
(*    | unify Comb(t,u) Comb(v,w) = let s = unify t v                        *)
clasohm@968
   176
(*                                  in if s=Fail then Fail                   *)
clasohm@968
   177
(*                                               else unify (u<|s) (w<|s);   *)
clasohm@968
   178
clasohm@968
   179
(**** Cases for the partial correctness of the algorithm ****)
clasohm@968
   180
clasohm@968
   181
goalw Unifier.thy unify_defs "MGIUnifier s t u = MGIUnifier s u t";
clasohm@968
   182
by (safe_tac (HOL_cs addSEs ([sym]@([spec] RL [mp]))));
clasohm@968
   183
qed "Unify_comm";
clasohm@968
   184
clasohm@968
   185
goal Unifier.thy "MGIUnifier [] (Const n) (Const n)";
clasohm@968
   186
by (simp_tac (subst_ss addsimps
clasohm@1465
   187
              [MGIU_iff,MGU_iff,Unifier_iff,subst_eq_iff,Idem_Nil]) 1);
clasohm@968
   188
qed "Unify1";
clasohm@968
   189
clasohm@968
   190
goal Unifier.thy "~m=n --> (ALL l.~Unifier l (Const m) (Const n))";
clasohm@968
   191
by (simp_tac (subst_ss addsimps[Unifier_iff]) 1);
clasohm@968
   192
val Unify2 = store_thm("Unify2", result() RS mp);
clasohm@968
   193
clasohm@968
   194
val [prem] = goalw Unifier.thy [MGIUnifier_def] 
clasohm@972
   195
 "~Var(v) <: t ==> MGIUnifier [(v,t)] (Var v) t";
clasohm@968
   196
by (fast_tac (HOL_cs addSIs [prem RS MGUnifier_Var,prem RS Var_Idem]) 1);
clasohm@968
   197
qed "Unify3";
clasohm@968
   198
clasohm@968
   199
val [prem] = goal Unifier.thy "Var(v) <: t ==> (ALL l.~Unifier l (Var v) t)";
clasohm@968
   200
by (simp_tac (subst_ss addsimps
clasohm@1465
   201
              [Unifier_iff,prem RS subst_mono RS occs_irrefl2]) 1);
clasohm@968
   202
qed "Unify4";
clasohm@968
   203
clasohm@968
   204
goal Unifier.thy "ALL l.~Unifier l (Const m) (Comb t u)";
clasohm@968
   205
by (simp_tac (subst_ss addsimps [Unifier_iff]) 1);
clasohm@968
   206
qed "Unify5";
clasohm@968
   207
clasohm@968
   208
goal Unifier.thy
clasohm@968
   209
    "(ALL l.~Unifier l t v) --> (ALL l.~Unifier l (Comb t u) (Comb v w))";
clasohm@968
   210
by (simp_tac (subst_ss addsimps [Unifier_iff]) 1);
clasohm@968
   211
val Unify6 = store_thm("Unify6", result() RS mp);
clasohm@968
   212
clasohm@968
   213
goal Unifier.thy "MGIUnifier s t v --> (ALL l.~Unifier l (u <| s) (w <| s)) \
clasohm@968
   214
\                                --> (ALL l.~Unifier l (Comb t u) (Comb v w))";
clasohm@968
   215
by (simp_tac (subst_ss addsimps [MGIU_iff]) 1);
clasohm@968
   216
by (fast_tac (set_cs addIs [Unifier_comp_subst] addSEs [Unifier_Comb]) 1);
clasohm@968
   217
val Unify7 = store_thm("Unify7", result() RS mp RS mp);
clasohm@968
   218
clasohm@968
   219
val [p1,p2,p3] = goal Unifier.thy
clasohm@968
   220
     "[| Idem(r); Unifier s (t <| r) (u <| r); \
clasohm@968
   221
\     (! q.Unifier q (t <| r) (u <| r) --> s <> q =s= q) |] ==> \
clasohm@968
   222
\     Idem(r <> s)";
clasohm@968
   223
by (cut_facts_tac [p1,
clasohm@1465
   224
                   p2 RS (p1 RS Unifier_Idem_subst RS (p3 RS spec RS mp))] 1);
clasohm@968
   225
by (REPEAT_SOME (etac rev_mp));
clasohm@968
   226
by (simp_tac (subst_ss addsimps [raw_Idem_iff,subst_eq_iff,subst_comp]) 1);
clasohm@968
   227
qed "Unify8_lemma1";
clasohm@968
   228
clasohm@968
   229
val [p1,p2,p3,p4] = goal Unifier.thy
clasohm@968
   230
   "[| Unifier q t v; Unifier q u w; (! q.Unifier q t v --> r <> q =s= q); \
clasohm@968
   231
\      (! q.Unifier q (u <| r) (w <| r) --> s <> q =s= q) |] ==> \
clasohm@968
   232
\   r <> s <> q =s= q";
clasohm@968
   233
val pp = p1 RS (p3 RS spec RS mp);
clasohm@968
   234
by (cut_facts_tac [pp,
clasohm@1465
   235
                   p2 RS (pp RS Unifier_comp_subst) RS (p4 RS spec RS mp)] 1);
clasohm@968
   236
by (REPEAT_SOME (etac rev_mp));
clasohm@968
   237
by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1);
clasohm@968
   238
qed "Unify8_lemma2";
clasohm@968
   239
clasohm@968
   240
goal Unifier.thy  "MGIUnifier r t v -->  MGIUnifier s (u <| r) (w <| r) --> \
clasohm@968
   241
\                MGIUnifier (r <> s) (Comb t u) (Comb v w)";
clasohm@968
   242
by (simp_tac (subst_ss addsimps [MGIU_iff,subst_comp,comp_assoc]) 1);
clasohm@968
   243
by (safe_tac HOL_cs);
clasohm@968
   244
by (REPEAT (etac rev_mp 2));
clasohm@968
   245
by (simp_tac (subst_ss addsimps 
clasohm@1465
   246
              [Unifier_iff,MGIU_iff,subst_comp,comp_assoc]) 2);
clasohm@968
   247
by (ALLGOALS (fast_tac (set_cs addEs 
clasohm@1465
   248
                        [Unifier_Comb,Unify8_lemma1,Unify8_lemma2])));
clasohm@968
   249
qed "Unify8";
clasohm@968
   250
clasohm@968
   251
clasohm@968
   252
(********************** Termination of the algorithm *************************)
clasohm@968
   253
(*                                                                           *)
clasohm@968
   254
(*UWFD is a well-founded relation that orders the 2 recursive calls in unify *)
clasohm@968
   255
(*                   NB well-foundedness of UWFD isn't proved                *)
clasohm@968
   256
clasohm@968
   257
clasohm@968
   258
goalw Unifier.thy [UWFD_def]  "UWFD t t' (Comb t u) (Comb t' u')";
clasohm@968
   259
by (simp_tac subst_ss 1);
clasohm@968
   260
by (fast_tac set_cs 1);
clasohm@968
   261
qed "UnifyWFD1";
clasohm@968
   262
clasohm@968
   263
val [prem] = goal Unifier.thy 
clasohm@968
   264
     "MGIUnifier s t t' ==> vars_of(u <| s) Un vars_of(u' <| s) <= \
clasohm@968
   265
\                           vars_of (Comb t u) Un vars_of (Comb t' u')";
clasohm@968
   266
by (subgoal_tac "vars_of(u <| s) Un vars_of(u' <| s) <= \
clasohm@968
   267
\                srange(s) Un vars_of(u) Un srange(s) Un vars_of(u')" 1);
clasohm@968
   268
by (etac subset_trans 1);
clasohm@968
   269
by (ALLGOALS (simp_tac (subst_ss addsimps [Var_intro,subset_iff])));
clasohm@968
   270
by (ALLGOALS (fast_tac (set_cs addDs 
clasohm@1465
   271
                        [Var_intro,prem RS MGIU_srange RS subsetD])));
clasohm@968
   272
qed "UWFD2_lemma1";
clasohm@968
   273
clasohm@968
   274
val [major,minor] = goal Unifier.thy 
clasohm@968
   275
     "[| MGIUnifier s t t';  ~ u <| s = u |] ==> \
clasohm@968
   276
\     ~ vars_of(u <| s) Un vars_of(u' <| s) =  \
clasohm@968
   277
\         (vars_of(t) Un vars_of(u)) Un (vars_of(t') Un vars_of(u'))";
clasohm@968
   278
by (cut_facts_tac 
clasohm@968
   279
    [major RS (MGIU_iff RS iffD1) RS conjunct1 RS (Idem_iff RS iffD1)] 1);
clasohm@968
   280
by (rtac (minor RS subst_not_empty RS exE) 1);
clasohm@968
   281
by (rtac (make_elim ((major RS MGIU_sdom) RS subsetD)) 1 THEN assume_tac 1);
clasohm@968
   282
by (rtac (disjI2 RS (not_equal_iff RS iffD2)) 1);
clasohm@968
   283
by (REPEAT (etac rev_mp 1));
clasohm@968
   284
by (asm_simp_tac subst_ss 1);
clasohm@968
   285
by (fast_tac (set_cs addIs [Var_elim2]) 1);
clasohm@968
   286
qed "UWFD2_lemma2";
clasohm@968
   287
clasohm@968
   288
val [prem] = goalw Unifier.thy [UWFD_def]  
clasohm@968
   289
  "MGIUnifier s t t' ==> UWFD (u <| s) (u' <| s) (Comb t u) (Comb t' u')";
clasohm@968
   290
by (cut_facts_tac 
clasohm@968
   291
    [prem RS UWFD2_lemma1 RS (subseteq_iff_subset_eq RS iffD1)] 1);
clasohm@968
   292
by (imp_excluded_middle_tac "u <| s = u" 1);
clasohm@1266
   293
by (simp_tac (subst_ss delsimps (ssubset_iff :: utlemmas_rews)
clasohm@1266
   294
                       addsimps [occs_Comb2]) 1);
clasohm@968
   295
by (rtac impI 1 THEN etac subst 1 THEN assume_tac 1);
clasohm@968
   296
by (rtac impI 1);
clasohm@968
   297
by (rtac (conjI RS (ssubset_iff RS iffD2) RS disjI1) 1);
clasohm@1266
   298
by (asm_simp_tac (subst_ss delsimps (ssubset_iff :: utlemmas_rews) addsimps [subseteq_iff_subset_eq]) 1);
clasohm@968
   299
by (asm_simp_tac subst_ss 1);
clasohm@968
   300
by (fast_tac (set_cs addDs [prem RS UWFD2_lemma2]) 1);
clasohm@968
   301
qed "UnifyWFD2";