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 |
|
1266
|
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
|