src/HOL/Subst/Subst.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 5184 9b8547a9496a
child 15635 8408a06590a6
permissions -rw-r--r--
import -> imports
     1 (*  Title:      Subst/Subst.thy
     2     ID:         $Id$
     3     Author:     Martin Coen, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Substitutions on uterms
     7 *)
     8 
     9 Subst = AList + UTerm +
    10 
    11 consts
    12 
    13   "=$="  ::  "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52)
    14   "<|"   ::  "'a uterm => ('a * 'a uterm) list => 'a uterm"        (infixl 55)
    15   "<>"   ::  "[('a*('a uterm)) list, ('a*('a uterm)) list] 
    16                  => ('a*('a uterm)) list"                          (infixl 56)
    17   sdom   ::  "('a*('a uterm)) list => 'a set"
    18   srange ::  "('a*('a uterm)) list => 'a set"
    19 
    20 
    21 primrec
    22   subst_Var      "(Var v <| s) = assoc v (Var v) s"
    23   subst_Const  "(Const c <| s) = Const c"
    24   subst_Comb  "(Comb M N <| s) = Comb (M <| s) (N <| s)"
    25 
    26 
    27 defs 
    28 
    29   subst_eq_def  "r =$= s == ALL t. t <| r = t <| s"
    30 
    31   comp_def    "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)"
    32 
    33   sdom_def
    34   "sdom(al) == alist_rec al {}  
    35                 (%x y xs g. if Var(x)=y then g - {x} else g Un {x})"
    36 
    37   srange_def   
    38    "srange(al) == Union({y. EX x:sdom(al). y=vars_of(Var(x) <| al)})"
    39 
    40 end