author | berghofe |
Fri, 16 Jul 1999 14:06:13 +0200 | |
changeset 7020 | 75ff179df7b7 |
parent 5184 | 9b8547a9496a |
child 15635 | 8408a06590a6 |
permissions | -rw-r--r-- |
3268
012c43174664
Mostly cosmetic changes: updated headers, ID lines, etc.
paulson
parents:
3192
diff
changeset
|
1 |
(* Title: Subst/Subst.thy |
012c43174664
Mostly cosmetic changes: updated headers, ID lines, etc.
paulson
parents:
3192
diff
changeset
|
2 |
ID: $Id$ |
1476 | 3 |
Author: Martin Coen, Cambridge University Computer Laboratory |
968 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
Substitutions on uterms |
|
7 |
*) |
|
8 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
9 |
Subst = AList + UTerm + |
968 | 10 |
|
11 |
consts |
|
12 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
13 |
"=$=" :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52) |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
14 |
"<|" :: "'a uterm => ('a * 'a uterm) list => 'a uterm" (infixl 55) |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
15 |
"<>" :: "[('a*('a uterm)) list, ('a*('a uterm)) list] |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
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 |
||
5184 | 21 |
primrec |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
22 |
subst_Var "(Var v <| s) = assoc v (Var v) s" |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
23 |
subst_Const "(Const c <| s) = Const c" |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
24 |
subst_Comb "(Comb M N <| s) = Comb (M <| s) (N <| s)" |
968 | 25 |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
26 |
|
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
27 |
defs |
968 | 28 |
|
3842 | 29 |
subst_eq_def "r =$= s == ALL t. t <| r = t <| s" |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
30 |
|
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
31 |
comp_def "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)" |
968 | 32 |
|
33 |
sdom_def |
|
1151 | 34 |
"sdom(al) == alist_rec al {} |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
35 |
(%x y xs g. if Var(x)=y then g - {x} else g Un {x})" |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
36 |
|
968 | 37 |
srange_def |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
38 |
"srange(al) == Union({y. EX x:sdom(al). y=vars_of(Var(x) <| al)})" |
968 | 39 |
|
40 |
end |