Subst/uterm.thy

Deleted extra space in clos_mk.

(*  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