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 + UTerm + |
|
9 |
|
10 consts |
|
11 |
|
12 "=s=" :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52) |
|
13 "<|" :: "'a uterm => ('a * 'a uterm) list => 'a uterm" (infixl 55) |
|
14 "<>" :: "[('a*('a uterm)) list, ('a*('a uterm)) list] |
|
15 => ('a*('a uterm)) list" (infixl 56) |
|
16 sdom :: "('a*('a uterm)) list => 'a set" |
|
17 srange :: "('a*('a uterm)) list => 'a set" |
|
18 |
|
19 |
|
20 primrec "op <|" uterm |
|
21 subst_Var "(Var v <| s) = assoc v (Var v) s" |
|
22 subst_Const "(Const c <| s) = Const c" |
|
23 subst_Comb "(Comb M N <| s) = Comb (M <| s) (N <| s)" |
|
24 |
|
25 |
|
26 rules |
|
27 |
|
28 subst_eq_def "r =s= s == ALL t.t <| r = t <| s" |
|
29 |
|
30 comp_def "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)" |
|
31 |
|
32 sdom_def |
|
33 "sdom(al) == alist_rec al {} |
|
34 (%x y xs g. if Var(x)=y then g - {x} else g Un {x})" |
|
35 |
|
36 srange_def |
|
37 "srange(al) == Union({y. EX x:sdom(al). y=vars_of(Var(x) <| al)})" |
|
38 |
|
39 end |