1(*------------------------------------------------------------------------ 2 * First order unification restricted to specified "scheme" variables. 3 * 4 *----------------------------------------------------------------------*) 5 6structure Unify :> Unify = struct 7 8open HolKernel Psyntax liteLib Abbrev; 9infix 5 |->; 10 11val ERR = mk_HOL_ERR "Unify"; 12 13fun lookup x [] = raise ERR "lookup" "not found" 14 | lookup x ({redex,residue}::t) = if redex=x then residue else lookup x t; 15 16fun deref_tmenv env tm = 17 if is_var tm then lookup tm env handle HOL_ERR _ => tm 18 else tm; 19 20fun restrict_tmenv P E = 21 mapfilter (fn {redex,residue} => 22 if P redex then redex |-> deref_tmenv E redex else fail()) E; 23 24fun occ env v = 25 let fun f t = 26 exists (fn fv => (fv = v) orelse f (lookup fv env) 27 handle HOL_ERR _ => false) (free_vars t) 28 handle HOL_ERR _ => false 29 in f 30 end; 31 32fun bind env v t = if occ env v t then failwith "occurs" else 33 let 34 val new_sub = v |-> subst env t; 35 val env' = map (fn {redex,residue} => (redex |-> (subst [new_sub] residue))) env 36 in new_sub::env' end 37 38(*--------------------------------------------------------------------------- 39 The following code assumes things have been renamed. 40 ---------------------------------------------------------------------------*) 41 42fun simp_unify_terms_in_env consts tm1 tm2 env = 43 let val tm1' = deref_tmenv env tm1 44 val tm2' = deref_tmenv env tm2 45 in 46 if is_var tm1' andalso not (mem tm1' consts) 47 then if is_var tm2' andalso not (mem tm2' consts) 48 then if tm1' = tm2' then env else bind env tm1' tm2' 49 else bind env tm1' tm2' 50 else 51 if is_var tm2' andalso not (mem tm2' consts) 52 then bind env tm2' tm1' 53 else 54 case (dest_term tm1',dest_term tm2') 55 of (VAR x, VAR y) => if tm1' = tm2' then env else failwith "unify_terms" 56 | (COMB p1,COMB p2) => 57 simp_unify_terms_in_env consts (fst p1) (fst p2) 58 (simp_unify_terms_in_env consts (snd p1) (snd p2) env) 59 | (LAMB p1,LAMB p2) => 60 let fun filt v = v <> (fst p1) andalso v <> (fst p2) 61 in restrict_tmenv filt 62 (simp_unify_terms_in_env 63 (subtract consts [fst p1, fst p2]) (snd p1) (snd p2) 64 (restrict_tmenv filt env)) 65 end 66 | otherwise => if tm1' = tm2' then env else failwith "simp_unify_terms" 67 end; 68 69 70fun simp_unify_terms consts tm1 tm2 = 71 simp_unify_terms_in_env consts tm1 tm2 []; 72 73end (* struct *) 74 75 76(* 77simp_unify_terms [] ``2 <= x`` ``m <= m`` 78SATISFY_CONV ([], [arithmeticTheory.LESS_EQ_REFL]) ``?x. 2 <= x`` 79 80simp_unify_terms [] ``f(X) /\ g(Y+2)`` ``f(2+2) /\ g(2 + Y)`` 81 82simp_unify_terms [`b:'a`] `P (x:'a) (b:'a):bool` `P (a:'a) (b:'a):bool`;; 83, `!x y:'a. Q x y`, `!z:'a. R x z`]; 84fun S facts = satisfy1 (U (map (freesl o hyp) facts)) (map concl facts); 85S facts `?a b:'a. P a b /\ R a b`; 86 87 88occ [(--`x:num`--) |-> (--`1 + 1`--)] (--`z:num`--) (--`z + x`--); 89occ [(--`x:num`--) |-> (--`z + 1`--)] (--`z:num`--) (--`x + x`--); 90occ [(--`x:num`--) |-> (--`z + 1`--)] (--`z:num`--) (--`y + y`--); 91occ [(--`x:num`--) |-> (--`z + 1`--)] (--`z:num`--) (--`\z. z = 1`--); 92 93 94*) 95