--- a/Subst/UTerm.thy Mon Aug 22 12:00:02 1994 +0200
+++ b/Subst/UTerm.thy Wed Aug 24 18:49:29 1994 +0200
@@ -1,4 +1,4 @@
-(* Title: Substitutions/uterm.thy
+(* Title: Substitutions/UTerm.thy
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -14,45 +14,52 @@
uterm :: (term)term
consts
- UTerm :: "'a node set set => 'a node set set"
- Rep_UTerm :: "'a uterm => 'a node set"
- Abs_UTerm :: "'a node set => 'a uterm"
- VAR :: "'a node set => 'a node set"
- CONST :: "'a node set => 'a node set"
- COMB :: "['a node set, 'a node set] => 'a node set"
+ uterm :: "'a item set => 'a item set"
+ Rep_uterm :: "'a uterm => 'a item"
+ Abs_uterm :: "'a item => 'a uterm"
+ VAR :: "'a item => 'a item"
+ CONST :: "'a item => 'a item"
+ COMB :: "['a item, 'a item] => 'a item"
Var :: "'a => 'a uterm"
Const :: "'a => 'a uterm"
Comb :: "['a uterm, 'a uterm] => 'a uterm"
- UTerm_rec :: "['a node set, 'a node set => 'b, 'a node set => 'b, \
-\ ['a node set , 'a node set, 'b, 'b]=>'b] => 'b"
+ UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b, \
+\ ['a item , 'a item, 'b, 'b]=>'b] => 'b"
uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b, \
\ ['a uterm, 'a uterm,'b,'b]=>'b] => 'b"
-rules
- UTerm_def "UTerm(A) == lfp(%Z. A <+> A <+> Z <*> Z)"
- (*faking a type definition...*)
- Rep_UTerm "Rep_UTerm(xs): UTerm(range(Leaf))"
- Rep_UTerm_inverse "Abs_UTerm(Rep_UTerm(xs)) = xs"
- Abs_UTerm_inverse "M: UTerm(range(Leaf)) ==> Rep_UTerm(Abs_UTerm(M)) = M"
+defs
(*defining the concrete constructors*)
VAR_def "VAR(v) == In0(v)"
CONST_def "CONST(v) == In1(In0(v))"
COMB_def "COMB(t,u) == In1(In1(t $ u))"
+
+inductive "uterm(A)"
+ intrs
+ VAR_I "v:A ==> VAR(v) : uterm(A)"
+ CONST_I "c:A ==> CONST(c) : uterm(A)"
+ COMB_I "[| M:uterm(A); N:uterm(A) |] ==> COMB(M,N) : uterm(A)"
+
+rules
+ (*faking a type definition...*)
+ Rep_uterm "Rep_uterm(xs): uterm(range(Leaf))"
+ Rep_uterm_inverse "Abs_uterm(Rep_uterm(xs)) = xs"
+ Abs_uterm_inverse "M: uterm(range(Leaf)) ==> Rep_uterm(Abs_uterm(M)) = M"
+
+defs
(*defining the abstract constructors*)
- Var_def "Var(v) == Abs_UTerm(VAR(Leaf(v)))"
- Const_def "Const(c) == Abs_UTerm(CONST(Leaf(c)))"
- Comb_def "Comb(t,u) == Abs_UTerm(COMB(Rep_UTerm(t),Rep_UTerm(u)))"
+ Var_def "Var(v) == Abs_uterm(VAR(Leaf(v)))"
+ Const_def "Const(c) == Abs_uterm(CONST(Leaf(c)))"
+ Comb_def "Comb(t,u) == Abs_uterm(COMB(Rep_uterm(t),Rep_uterm(u)))"
(*uterm recursion*)
UTerm_rec_def
- "UTerm_rec(M,b,c,d) == wfrec(trancl(pred_Sexp), M, \
-\ %z g. Case(z, %x. b(x), \
-\ %w. Case(w, %x. c(x), \
-\ %v. Split(v, %x y. d(x,y,g(x),g(y))))))"
+ "UTerm_rec(M,b,c,d) == wfrec(trancl(pred_sexp), M, \
+\ Case(%x g.b(x), Case(%y g. c(y), Split(%x y g. d(x,y,g(x),g(y))))))"
uterm_rec_def
"uterm_rec(t,b,c,d) == \
-\ UTerm_rec(Rep_UTerm(t), %x.b(Inv(Leaf,x)), %x.c(Inv(Leaf,x)), \
-\ %x y q r.d(Abs_UTerm(x),Abs_UTerm(y),q,r))"
+\ UTerm_rec(Rep_uterm(t), %x.b(Inv(Leaf,x)), %x.c(Inv(Leaf,x)), \
+\ %x y q r.d(Abs_uterm(x),Abs_uterm(y),q,r))"
end