equal
deleted
inserted
replaced
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, 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 |
|