TFL/examples/Subst/Unifier.thy

Subst as modified by Konrad Slind

(*  Title:      Subst/unifier.thy
    Author:     Martin Coen, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Definition of most general unifier
*)

Unifier = Subst + 

consts

  Unifier    :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
  ">>"       :: "[('a*('a uterm))list,('a*('a uterm))list] => bool" (infixr 52)
  MGUnifier  :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
  Idem       :: "('a*('a uterm))list => bool"

rules  (*Definitions*)

  Unifier_def      "Unifier s t u == t <| s = u <| s"
  MoreGeneral_def  "r >> s == ? q. s =s= r <> q"
  MGUnifier_def    "MGUnifier s t u == Unifier s t u & 
                                       (!r. Unifier r t u --> s >> r)"
  Idem_def         "Idem(s) == s <> s =s= s"
end