--- a/src/HOL/Subst/Subst.thy Thu May 15 12:29:59 1997 +0200
+++ b/src/HOL/Subst/Subst.thy Thu May 15 12:40:01 1997 +0200
@@ -5,33 +5,35 @@
Substitutions on uterms
*)
-Subst = Setplus + AList + UTLemmas +
+Subst = AList + UTerm +
consts
- "=s=" :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52)
-
- "<|" :: "['a uterm,('a*('a uterm)) list] => 'a uterm" (infixl 55)
- "<>" :: "[('a*('a uterm)) list, ('a*('a uterm)) list] =>
- ('a*('a uterm)) list" (infixl 56)
+ "=$=" :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52)
+ "<|" :: "'a uterm => ('a * 'a uterm) list => 'a uterm" (infixl 55)
+ "<>" :: "[('a*('a uterm)) list, ('a*('a uterm)) list]
+ => ('a*('a uterm)) list" (infixl 56)
sdom :: "('a*('a uterm)) list => 'a set"
srange :: "('a*('a uterm)) list => 'a set"
-rules
- subst_eq_def "r =s= s == ALL t.t <| r = t <| s"
+primrec "op <|" uterm
+ subst_Var "(Var v <| s) = assoc v (Var v) s"
+ subst_Const "(Const c <| s) = Const c"
+ subst_Comb "(Comb M N <| s) = Comb (M <| s) (N <| s)"
- subst_def
- "t <| al == uterm_rec t (%x.assoc x (Var x) al)
- (%x.Const(x))
- (%u v q r.Comb q r)"
+
+defs
- comp_def "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)"
+ subst_eq_def "r =$= s == ALL t.t <| r = t <| s"
+
+ comp_def "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)"
sdom_def
"sdom(al) == alist_rec al {}
- (%x y xs g.if Var(x)=y then g Int Compl({x}) else g Un {x})"
+ (%x y xs g. if Var(x)=y then g - {x} else g Un {x})"
+
srange_def
- "srange(al) == Union({y. EX x:sdom(al).y=vars_of(Var(x) <| al)})"
+ "srange(al) == Union({y. EX x:sdom(al). y=vars_of(Var(x) <| al)})"
end