src/HOL/Subst/Unifier.thy

replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style

(*  Title:      Subst/Unifier.thy
    ID:         $Id$
    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"

defs

  Unifier_def      "Unifier s t u == t <| s = u <| s"
  MoreGeneral_def  "r >> s == ? q. 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"
end