--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Subst/uterm.thy Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,58 @@
+(* Title: Substitutions/uterm.thy
+ Author: Martin Coen, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+Simple term structure for unifiation.
+Binary trees with leaves that are constants or variables.
+*)
+
+UTerm = Sexp +
+
+types uterm 1
+
+arities
+ 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"
+ 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 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"
+ (*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))"
+ (*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)))"
+
+ (*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_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))"
+
+end