src/HOL/Subst/Unify.thy
 author nipkow Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) changeset 15140 322485b816ac parent 12406 c9775847ed66 child 15635 8408a06590a6 permissions -rw-r--r--
import -> imports
```     1 (*  Title:      Subst/Unify
```
```     2     ID:         \$Id\$
```
```     3     Author:     Konrad Slind, Cambridge University Computer Laboratory
```
```     4     Copyright   1997  University of Cambridge
```
```     5
```
```     6 Unification algorithm
```
```     7 *)
```
```     8
```
```     9 Unify = Unifier +
```
```    10
```
```    11 consts
```
```    12
```
```    13    unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
```
```    14    unify    :: "'a uterm * 'a uterm => ('a * 'a uterm) list option"
```
```    15
```
```    16 defs
```
```    17
```
```    18   (*Termination relation for the Unify function:
```
```    19     --either the set of variables decreases
```
```    20     --or the first argument does (in fact, both do)
```
```    21   *)
```
```    22   unifyRel_def  "unifyRel == inv_image (finite_psubset <*lex*> measure uterm_size)
```
```    23                                (%(M,N). (vars_of M Un vars_of N, M))"
```
```    24
```
```    25 recdef unify "unifyRel"
```
```    26   "unify(Const m, Const n)  = (if (m=n) then Some[] else None)"
```
```    27   "unify(Const m, Comb M N) = None"
```
```    28   "unify(Const m, Var v)    = Some[(v,Const m)]"
```
```    29   "unify(Var v, M)          = (if (Var v <: M) then None else Some[(v,M)])"
```
```    30   "unify(Comb M N, Const x) = None"
```
```    31   "unify(Comb M N, Var v)   = (if (Var v <: Comb M N) then None
```
```    32                                else Some[(v,Comb M N)])"
```
```    33   "unify(Comb M1 N1, Comb M2 N2) =
```
```    34       (case unify(M1,M2)
```
```    35         of None       => None
```
```    36          | Some theta => (case unify(N1 <| theta, N2 <| theta)
```
```    37                             of None       => None
```
```    38                              | Some sigma => Some (theta <> sigma)))"
```
```    39 end
```