author | clasohm |
Wed, 21 Jun 1995 15:47:10 +0200 | |
changeset 1151 | c820b3cc3df0 |
parent 972 | e61b058d58d2 |
child 1266 | 3ae9fe3c0f68 |
permissions | -rw-r--r-- |
968 | 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) |
|
1151 | 15 |
"<>" :: "[('a*('a uterm)) list, ('a*('a uterm)) list] => |
16 |
('a*('a uterm)) list" (infixl 56) |
|
968 | 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 |
|
1151 | 25 |
"t <| al == uterm_rec t (%x.assoc x (Var x) al) |
26 |
(%x.Const(x)) |
|
27 |
(%u v q r.Comb q r)" |
|
968 | 28 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
968
diff
changeset
|
29 |
comp_def "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)" |
968 | 30 |
|
31 |
sdom_def |
|
1151 | 32 |
"sdom(al) == alist_rec al {} |
33 |
(%x y xs g.if Var(x)=y then g Int Compl({x}) else g Un {x})" |
|
968 | 34 |
srange_def |
35 |
"srange(al) == Union({y. EX x:sdom(al).y=vars_of(Var(x) <| al)})" |
|
36 |
||
37 |
end |