src/HOL/Subst/Unifier.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 3268 012c43174664
child 15635 8408a06590a6
permissions -rw-r--r--
import -> imports
paulson@3268
     1
(*  Title:      Subst/Unifier.thy
paulson@3268
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@968
     4
    Copyright   1993  University of Cambridge
clasohm@968
     5
paulson@3192
     6
Definition of most general unifier
clasohm@968
     7
*)
clasohm@968
     8
paulson@3192
     9
Unifier = Subst + 
clasohm@968
    10
clasohm@968
    11
consts
clasohm@968
    12
paulson@3192
    13
  Unifier   :: "[('a * 'a uterm)list, 'a uterm, 'a uterm] => bool"
paulson@3192
    14
  ">>"      :: "[('a * 'a uterm)list, ('a * 'a uterm)list] => bool" (infixr 52)
paulson@3192
    15
  MGUnifier :: "[('a * 'a uterm)list, 'a uterm, 'a uterm] => bool"
paulson@3192
    16
  Idem      :: "('a * 'a uterm)list => bool"
clasohm@968
    17
paulson@3192
    18
defs
clasohm@968
    19
clasohm@968
    20
  Unifier_def      "Unifier s t u == t <| s = u <| s"
paulson@3192
    21
  MoreGeneral_def  "r >> s == ? q. s =$= r <> q"
clasohm@1151
    22
  MGUnifier_def    "MGUnifier s t u == Unifier s t u & 
paulson@3192
    23
                                       (!r. Unifier r t u --> s >> r)"
paulson@3192
    24
  Idem_def         "Idem(s) == (s <> s) =$= s"
clasohm@968
    25
end