src/HOL/Subst/Unifier.thy
author clasohm
Wed Mar 13 11:55:25 1996 +0100 (1996-03-13 ago)
changeset 1574 5a63ab90ee8a
parent 1476 608483c2122a
child 3192 a75558a4ed37
permissions -rw-r--r--
modified primrec so it can be used in MiniML/Type.thy
     1 (*  Title:      Subst/unifier.thy
     2     Author:     Martin Coen, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 
     5 Definition of most general idempotent unifier
     6 *)
     7 
     8 Unifier = Subst +
     9 
    10 consts
    11 
    12   Idem       :: "('a*('a uterm))list=> bool"
    13   Unifier    :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
    14   ">>"       :: "[('a*('a uterm))list,('a*('a uterm))list] => bool" (infixr 52)
    15   MGUnifier  :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
    16   MGIUnifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
    17   UWFD       :: ['a uterm,'a uterm,'a uterm,'a uterm] => bool
    18 
    19 rules  (*Definitions*)
    20 
    21   Idem_def         "Idem(s) == s <> s =s= s"
    22   Unifier_def      "Unifier s t u == t <| s = u <| s"
    23   MoreGeneral_def  "r >> s == ? q.s =s= r <> q"
    24   MGUnifier_def    "MGUnifier s t u == Unifier s t u & 
    25                     (! r.Unifier r t u --> s >> r)"
    26   MGIUnifier_def   "MGIUnifier s t u == MGUnifier s t u & Idem(s)"
    27 
    28   UWFD_def
    29   "UWFD x y x' y' == 
    30     (vars_of(x) Un vars_of(y) < vars_of(x') Un vars_of(y')) |  
    31     (vars_of(x) Un vars_of(y) = vars_of(x') Un vars_of(y') & x <: x')"
    32 
    33 end