author | lcp |
Thu, 06 Apr 1995 11:49:42 +0200 | |
changeset 246 | 0f9230a24164 |
parent 48 | 21291189b51e |
child 249 | 492493334e0f |
permissions | -rw-r--r-- |
0 | 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 |
||
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
29 |
comp_def "al <> bl == alist_rec(al,bl,%x y xs g.<x,y <| bl>#g)" |
0 | 30 |
|
31 |
sdom_def |
|
32 |
"sdom(al) == alist_rec(al, {}, \ |
|
33 |
\ %x y xs g.if(Var(x)=y, g Int Compl({x}), g Un {x}))" |
|
34 |
srange_def |
|
35 |
"srange(al) == Union({y. EX x:sdom(al).y=vars_of(Var(x) <| al)})" |
|
36 |
||
37 |
end |