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
clasohm@1476
     1
(*  Title:      Subst/unifier.thy
clasohm@1476
     2
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@968
     3
    Copyright   1993  University of Cambridge
clasohm@968
     4
clasohm@968
     5
Definition of most general idempotent unifier
clasohm@968
     6
*)
clasohm@968
     7
clasohm@968
     8
Unifier = Subst +
clasohm@968
     9
clasohm@968
    10
consts
clasohm@968
    11
clasohm@968
    12
  Idem       :: "('a*('a uterm))list=> bool"
clasohm@968
    13
  Unifier    :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
clasohm@968
    14
  ">>"       :: "[('a*('a uterm))list,('a*('a uterm))list] => bool" (infixr 52)
clasohm@968
    15
  MGUnifier  :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
clasohm@968
    16
  MGIUnifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
clasohm@1374
    17
  UWFD       :: ['a uterm,'a uterm,'a uterm,'a uterm] => bool
clasohm@968
    18
clasohm@968
    19
rules  (*Definitions*)
clasohm@968
    20
clasohm@968
    21
  Idem_def         "Idem(s) == s <> s =s= s"
clasohm@968
    22
  Unifier_def      "Unifier s t u == t <| s = u <| s"
clasohm@968
    23
  MoreGeneral_def  "r >> s == ? q.s =s= r <> q"
clasohm@1151
    24
  MGUnifier_def    "MGUnifier s t u == Unifier s t u & 
clasohm@1476
    25
                    (! r.Unifier r t u --> s >> r)"
clasohm@968
    26
  MGIUnifier_def   "MGIUnifier s t u == MGUnifier s t u & Idem(s)"
clasohm@968
    27
clasohm@968
    28
  UWFD_def
clasohm@1151
    29
  "UWFD x y x' y' == 
clasohm@1151
    30
    (vars_of(x) Un vars_of(y) < vars_of(x') Un vars_of(y')) |  
clasohm@1151
    31
    (vars_of(x) Un vars_of(y) = vars_of(x') Un vars_of(y') & x <: x')"
clasohm@968
    32
clasohm@968
    33
end