--- a/src/ZF/Resid/Redex.thy Sun Jul 09 16:01:42 2000 +0200
+++ b/src/ZF/Resid/Redex.thy Mon Jul 10 12:17:34 2000 +0200
@@ -1,4 +1,4 @@
-(* Title: Redex.thy
+(* Title: ZF/Resid/Redex.thy
ID: $Id$
Author: Ole Rasmussen
Copyright 1995 University of Cambridge
@@ -22,28 +22,29 @@
union_aux :: i=>i
regular :: i=>o
+translations
+ "a<==b" == "<a,b>:Ssub"
+ "a ~ b" == "<a,b>:Scomp"
+ "regular(a)" == "a:Sreg"
+
+
primrec (*explicit lambda is required because both arguments of "un" vary*)
"union_aux(Var(n)) =
(lam t:redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
"union_aux(Fun(u)) =
- (lam t:redexes. redexes_case(%j. 0, %y. Fun(u un y),
+ (lam t:redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y),
%b y z. 0, t))"
"union_aux(App(b,f,a)) =
(lam t:redexes.
redexes_case(%j. 0, %y. 0,
- %c z u. App(b or c, f un z, a un u), t))"
+ %c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))"
defs
union_def "u un v == union_aux(u)`v"
-translations
- "a<==b" == "<a,b>:Ssub"
- "a ~ b" == "<a,b>:Scomp"
- "regular(a)" == "a:Sreg"
-
inductive
domains "Ssub" <= "redexes*redexes"
intrs
--- a/src/ZF/Resid/Substitution.thy Sun Jul 09 16:01:42 2000 +0200
+++ b/src/ZF/Resid/Substitution.thy Mon Jul 10 12:17:34 2000 +0200
@@ -1,4 +1,4 @@
-(* Title: Substitution.thy
+(* Title: ZF/Resid/Substitution.thy
ID: $Id$
Author: Ole Rasmussen
Copyright 1995 University of Cambridge
@@ -42,10 +42,10 @@
(lam r:redexes. lam k:nat. if k<i then Var(i #- 1)
else if k=i then r else Var(i))"
"subst_aux(Fun(t)) =
- (lam r:redexes. lam k:nat. Fun(subst_rec(lift(r), t, succ(k))))"
+ (lam r:redexes. lam k:nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
"subst_aux(App(b,f,a)) =
- (lam r:redexes. lam k:nat. App(b, subst_rec(r,f,k), subst_rec(r,a,k)))"
+ (lam r:redexes. lam k:nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
end