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