src/HOL/Subst/Subst.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:      Substitutions/subst.thy
     2     Author:     Martin Coen, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 
     5 Substitutions on uterms
     6 *)
     7 
     8 Subst = Setplus + AList + UTLemmas +
     9 
    10 consts
    11 
    12   "=s="  ::  "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52)
    13 
    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 rules 
    21 
    22   subst_eq_def  "r =s= s == ALL t.t <| r = t <| s"
    23 
    24   subst_def    
    25   "t <| al == uterm_rec t (%x.assoc x (Var x) al)       
    26                          (%x.Const(x))                  
    27                          (%u v q r.Comb q r)"
    28 
    29   comp_def    "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)"
    30 
    31   sdom_def
    32   "sdom(al) == alist_rec al {}  
    33                 (%x y xs g.if Var(x)=y then g Int Compl({x}) else g Un {x})"
    34   srange_def   
    35   "srange(al) == Union({y. EX x:sdom(al).y=vars_of(Var(x) <| al)})"
    36 
    37 end