src/HOL/Subst/Subst.thy
author nipkow
Mon Oct 21 09:50:50 1996 +0200 (1996-10-21)
changeset 2115 9709f9188549
parent 1476 608483c2122a
child 3192 a75558a4ed37
permissions -rw-r--r--
Added trans_tac (see Provers/nat_transitive.ML)
clasohm@1476
     1
(*  Title:      Substitutions/subst.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
Substitutions on uterms
clasohm@968
     6
*)
clasohm@968
     7
clasohm@968
     8
Subst = Setplus + AList + UTLemmas +
clasohm@968
     9
clasohm@968
    10
consts
clasohm@968
    11
clasohm@968
    12
  "=s="  ::  "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52)
clasohm@968
    13
clasohm@968
    14
  "<|"   ::  "['a uterm,('a*('a uterm)) list] => 'a uterm"         (infixl 55)
clasohm@1151
    15
  "<>"   ::  "[('a*('a uterm)) list, ('a*('a uterm)) list] => 
clasohm@1151
    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
rules 
clasohm@968
    21
clasohm@968
    22
  subst_eq_def  "r =s= s == ALL t.t <| r = t <| s"
clasohm@968
    23
clasohm@968
    24
  subst_def    
clasohm@1476
    25
  "t <| al == uterm_rec t (%x.assoc x (Var x) al)       
clasohm@1476
    26
                         (%x.Const(x))                  
clasohm@1151
    27
                         (%u v q r.Comb q r)"
clasohm@968
    28
clasohm@1266
    29
  comp_def    "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)"
clasohm@968
    30
clasohm@968
    31
  sdom_def
clasohm@1151
    32
  "sdom(al) == alist_rec al {}  
clasohm@1151
    33
                (%x y xs g.if Var(x)=y then g Int Compl({x}) else g Un {x})"
clasohm@968
    34
  srange_def   
clasohm@968
    35
  "srange(al) == Union({y. EX x:sdom(al).y=vars_of(Var(x) <| al)})"
clasohm@968
    36
clasohm@968
    37
end