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
paulson@3268
     1
(*  Title:      Subst/Subst.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
clasohm@968
     6
Substitutions on uterms
clasohm@968
     7
*)
clasohm@968
     8
paulson@3192
     9
Subst = AList + UTerm +
clasohm@968
    10
clasohm@968
    11
consts
clasohm@968
    12
paulson@3192
    13
  "=$="  ::  "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52)
paulson@3192
    14
  "<|"   ::  "'a uterm => ('a * 'a uterm) list => 'a uterm"        (infixl 55)
paulson@3192
    15
  "<>"   ::  "[('a*('a uterm)) list, ('a*('a uterm)) list] 
paulson@3192
    16
                 => ('a*('a uterm)) list"                          (infixl 56)
clasohm@968
    17
  sdom   ::  "('a*('a uterm)) list => 'a set"
clasohm@968
    18
  srange ::  "('a*('a uterm)) list => 'a set"
clasohm@968
    19
clasohm@968
    20
berghofe@5184
    21
primrec
paulson@3192
    22
  subst_Var      "(Var v <| s) = assoc v (Var v) s"
paulson@3192
    23
  subst_Const  "(Const c <| s) = Const c"
paulson@3192
    24
  subst_Comb  "(Comb M N <| s) = Comb (M <| s) (N <| s)"
clasohm@968
    25
paulson@3192
    26
paulson@3192
    27
defs 
clasohm@968
    28
wenzelm@3842
    29
  subst_eq_def  "r =$= s == ALL t. t <| r = t <| s"
paulson@3192
    30
paulson@3192
    31
  comp_def    "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)"
clasohm@968
    32
clasohm@968
    33
  sdom_def
clasohm@1151
    34
  "sdom(al) == alist_rec al {}  
paulson@3192
    35
                (%x y xs g. if Var(x)=y then g - {x} else g Un {x})"
paulson@3192
    36
clasohm@968
    37
  srange_def   
paulson@3192
    38
   "srange(al) == Union({y. EX x:sdom(al). y=vars_of(Var(x) <| al)})"
clasohm@968
    39
clasohm@968
    40
end