--- a/Subst/UTerm.ML Mon Aug 22 12:00:02 1994 +0200
+++ b/Subst/UTerm.ML Wed Aug 24 18:49:29 1994 +0200
@@ -2,56 +2,48 @@
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-For uterm.thy.
+Simple term structure for unifiation.
+Binary trees with leaves that are constants or variables.
*)
open UTerm;
+val uterm_con_defs = [VAR_def, CONST_def, COMB_def];
+
+goal UTerm.thy "uterm(A) = A <+> A <+> (uterm(A) <*> uterm(A))";
+let val rew = rewrite_rule uterm_con_defs in
+by (fast_tac (univ_cs addSIs (equalityI :: map rew uterm.intrs)
+ addEs [rew uterm.elim]) 1)
+end;
+val uterm_unfold = result();
+
(** the uterm functional **)
-goal UTerm.thy "mono(%Z. A <+> A <+> Z <*> Z)";
-by (REPEAT (ares_tac [monoI, subset_refl, usum_mono, uprod_mono] 1));
-val UTerm_fun_mono = result();
+(*This justifies using uterm in other recursive type definitions*)
+goalw UTerm.thy uterm.defs "!!A B. A<=B ==> uterm(A) <= uterm(B)";
+by (REPEAT (ares_tac (lfp_mono::basic_monos) 1));
+val uterm_mono = result();
-val UTerm_unfold = UTerm_fun_mono RS (UTerm_def RS def_lfp_Tarski);
+(** Type checking rules -- uterm creates well-founded sets **)
-(*This justifies using UTerm in other recursive type definitions*)
-val prems = goalw UTerm.thy [UTerm_def] "[| A<=B |] ==> UTerm(A) <= UTerm(B)";
-by (REPEAT (ares_tac (prems@[monoI, subset_refl, lfp_mono,
- usum_mono, uprod_mono]) 1));
-val UTerm_mono = result();
-
-(** Type checking rules -- UTerm creates well-founded sets **)
+goalw UTerm.thy (uterm_con_defs @ uterm.defs) "uterm(sexp) <= sexp";
+by (rtac lfp_lowerbound 1);
+by (fast_tac (univ_cs addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1);
+val uterm_sexp = result();
-val prems = goalw UTerm.thy [UTerm_def] "UTerm(Sexp) <= Sexp";
-by (rtac lfp_lowerbound 1);
-by (fast_tac (univ_cs addIs [Sexp_In0I,Sexp_In1I,Sexp_SconsI]) 1);
-val UTerm_Sexp = result();
-
-(* A <= Sexp ==> UTerm(A) <= Sexp *)
-val UTerm_subset_Sexp = standard
- (UTerm_mono RS (UTerm_Sexp RSN (2,subset_trans)));
+(* A <= sexp ==> uterm(A) <= sexp *)
+val uterm_subset_sexp = standard ([uterm_mono, uterm_sexp] MRS subset_trans);
(** Induction **)
-(*Induction for the set UTerm(A) *)
-val major::prems = goalw UTerm.thy [VAR_def,CONST_def,COMB_def]
- "[| M: UTerm(A); !!M.M : A ==> P(VAR(M)); !!M.M : A ==> P(CONST(M)); \
-\ !!M N. [| M: UTerm(A); N: UTerm(A); P(M); P(N) |] ==> P(COMB(M,N)) |] \
-\ ==> P(M)";
-by (rtac (major RS (UTerm_def RS def_induct)) 1);
-by (rtac UTerm_fun_mono 1);
-by (fast_tac (set_cs addIs prems addEs [usumE,uprodE]) 1);
-val UTerm_induct = result();
-
(*Induction for the type 'a uterm *)
val prems = goalw UTerm.thy [Var_def,Const_def,Comb_def]
"[| !!x.P(Var(x)); !!x.P(Const(x)); \
\ !!u v. [| P(u); P(v) |] ==> P(Comb(u,v)) |] ==> P(t)";
-by (rtac (Rep_UTerm_inverse RS subst) 1); (*types force good instantiation*)
-by (rtac (Rep_UTerm RS UTerm_induct) 1);
+by (rtac (Rep_uterm_inverse RS subst) 1); (*types force good instantiation*)
+by (rtac (Rep_uterm RS uterm.induct) 1);
by (REPEAT (ares_tac prems 1
- ORELSE eresolve_tac [rangeE, ssubst, Abs_UTerm_inverse RS subst] 1));
+ ORELSE eresolve_tac [rangeE, ssubst, Abs_uterm_inverse RS subst] 1));
val uterm_induct = result();
(*Perform induction on xs. *)
@@ -59,40 +51,22 @@
EVERY [res_inst_tac [("t",a)] uterm_induct M,
rename_last_tac a ["1"] (M+1)];
-(** Introduction rules for UTerm constructors **)
-
-(* c : A <+> A <+> UTerm(A) <*> UTerm(A) ==> c : UTerm(A) *)
-val UTermI = UTerm_unfold RS equalityD2 RS subsetD;
-
-(* Nil is a UTerm -- this also justifies the type definition*)
-val prems = goalw UTerm.thy [VAR_def] "v:A ==> VAR(v) : UTerm(A)";
-by (REPEAT (resolve_tac ([singletonI, UTermI, usum_In0I]@prems) 1));
-val VAR_I = result();
-
-val prems = goalw UTerm.thy [CONST_def] "c:A ==> CONST(c) : UTerm(A)";
-by (REPEAT (resolve_tac ([singletonI, UTermI, usum_In0I, usum_In1I]@prems) 1));
-val CONST_I = result();
-
-val prems = goalw UTerm.thy [COMB_def]
- "[| M:UTerm(A); N:UTerm(A) |] ==> COMB(M,N) : UTerm(A)";
-by (REPEAT (resolve_tac (prems@[UTermI, uprodI, usum_In1I]) 1));
-val COMB_I = result();
(*** Isomorphisms ***)
-goal UTerm.thy "inj(Rep_UTerm)";
+goal UTerm.thy "inj(Rep_uterm)";
by (rtac inj_inverseI 1);
-by (rtac Rep_UTerm_inverse 1);
-val inj_Rep_UTerm = result();
+by (rtac Rep_uterm_inverse 1);
+val inj_Rep_uterm = result();
-goal UTerm.thy "inj_onto(Abs_UTerm,UTerm(range(Leaf)))";
+goal UTerm.thy "inj_onto(Abs_uterm,uterm(range(Leaf)))";
by (rtac inj_onto_inverseI 1);
-by (etac Abs_UTerm_inverse 1);
-val inj_onto_Abs_UTerm = result();
+by (etac Abs_uterm_inverse 1);
+val inj_onto_Abs_uterm = result();
(** Distinctness of constructors **)
-goalw UTerm.thy [CONST_def,COMB_def] "~ CONST(c) = COMB(u,v)";
+goalw UTerm.thy uterm_con_defs "~ CONST(c) = COMB(u,v)";
by (rtac notI 1);
by (etac (In1_inject RS (In0_not_In1 RS notE)) 1);
val CONST_not_COMB = result();
@@ -100,14 +74,14 @@
val CONST_neq_COMB = standard (CONST_not_COMB RS notE);
val COMB_neq_CONST = sym RS CONST_neq_COMB;
-goalw UTerm.thy [COMB_def,VAR_def] "~ COMB(u,v) = VAR(x)";
+goalw UTerm.thy uterm_con_defs "~ COMB(u,v) = VAR(x)";
by (rtac In1_not_In0 1);
val COMB_not_VAR = result();
val VAR_not_COMB = standard (COMB_not_VAR RS not_sym);
val COMB_neq_VAR = standard (COMB_not_VAR RS notE);
val VAR_neq_COMB = sym RS COMB_neq_VAR;
-goalw UTerm.thy [VAR_def,CONST_def] "~ VAR(x) = CONST(c)";
+goalw UTerm.thy uterm_con_defs "~ VAR(x) = CONST(c)";
by (rtac In0_not_In1 1);
val VAR_not_CONST = result();
val CONST_not_VAR = standard (VAR_not_CONST RS not_sym);
@@ -116,24 +90,24 @@
goalw UTerm.thy [Const_def,Comb_def] "~ Const(c) = Comb(u,v)";
-by (rtac (CONST_not_COMB RS (inj_onto_Abs_UTerm RS inj_onto_contraD)) 1);
-by (REPEAT (resolve_tac [rangeI, VAR_I, CONST_I, COMB_I, Rep_UTerm] 1));
+by (rtac (CONST_not_COMB RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1);
+by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1));
val Const_not_Comb = result();
val Comb_not_Const = standard (Const_not_Comb RS not_sym);
val Const_neq_Comb = standard (Const_not_Comb RS notE);
val Comb_neq_Const = sym RS Const_neq_Comb;
goalw UTerm.thy [Comb_def,Var_def] "~ Comb(u,v) = Var(x)";
-by (rtac (COMB_not_VAR RS (inj_onto_Abs_UTerm RS inj_onto_contraD)) 1);
-by (REPEAT (resolve_tac [rangeI, VAR_I, CONST_I, COMB_I, Rep_UTerm] 1));
+by (rtac (COMB_not_VAR RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1);
+by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1));
val Comb_not_Var = result();
val Var_not_Comb = standard (Comb_not_Var RS not_sym);
val Comb_neq_Var = standard (Comb_not_Var RS notE);
val Var_neq_Comb = sym RS Comb_neq_Var;
goalw UTerm.thy [Var_def,Const_def] "~ Var(x) = Const(c)";
-by (rtac (VAR_not_CONST RS (inj_onto_Abs_UTerm RS inj_onto_contraD)) 1);
-by (REPEAT (resolve_tac [rangeI, VAR_I, CONST_I, COMB_I, Rep_UTerm] 1));
+by (rtac (VAR_not_CONST RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1);
+by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1));
val Var_not_Const = result();
val Const_not_Var = standard (Var_not_Const RS not_sym);
val Var_neq_Const = standard (Var_not_Const RS notE);
@@ -163,66 +137,66 @@
(*For reasoning about abstract uterm constructors*)
-val UTerm_cs = set_cs addIs [Rep_UTerm, VAR_I, CONST_I, COMB_I]
- addSEs [CONST_neq_COMB,COMB_neq_VAR,VAR_neq_CONST,
- COMB_neq_CONST,VAR_neq_COMB,CONST_neq_VAR,
- COMB_inject]
- addSDs [VAR_inject,CONST_inject,
- inj_onto_Abs_UTerm RS inj_ontoD,
- inj_Rep_UTerm RS injD, Leaf_inject];
+val uterm_cs = set_cs addIs uterm.intrs @ [Rep_uterm]
+ addSEs [CONST_neq_COMB,COMB_neq_VAR,VAR_neq_CONST,
+ COMB_neq_CONST,VAR_neq_COMB,CONST_neq_VAR,
+ COMB_inject]
+ addSDs [VAR_inject,CONST_inject,
+ inj_onto_Abs_uterm RS inj_ontoD,
+ inj_Rep_uterm RS injD, Leaf_inject];
goalw UTerm.thy [Var_def] "(Var(x)=Var(y)) = (x=y)";
-by (fast_tac UTerm_cs 1);
+by (fast_tac uterm_cs 1);
val Var_Var_eq = result();
val Var_inject = standard (Var_Var_eq RS iffD1);
goalw UTerm.thy [Const_def] "(Const(x)=Const(y)) = (x=y)";
-by (fast_tac UTerm_cs 1);
+by (fast_tac uterm_cs 1);
val Const_Const_eq = result();
val Const_inject = standard (Const_Const_eq RS iffD1);
goalw UTerm.thy [Comb_def] "(Comb(u,v)=Comb(x,y)) = (u=x & v=y)";
-by (fast_tac UTerm_cs 1);
+by (fast_tac uterm_cs 1);
val Comb_Comb_eq = result();
val Comb_inject = standard (Comb_Comb_eq RS iffD1 RS conjE);
-val [major] = goal UTerm.thy "VAR(M): UTerm(A) ==> M : A";
+val [major] = goal UTerm.thy "VAR(M): uterm(A) ==> M : A";
by (rtac (major RS setup_induction) 1);
-by (etac UTerm_induct 1);
-by (ALLGOALS (fast_tac UTerm_cs));
+by (etac uterm.induct 1);
+by (ALLGOALS (fast_tac uterm_cs));
val VAR_D = result();
-val [major] = goal UTerm.thy "CONST(M): UTerm(A) ==> M : A";
+val [major] = goal UTerm.thy "CONST(M): uterm(A) ==> M : A";
by (rtac (major RS setup_induction) 1);
-by (etac UTerm_induct 1);
-by (ALLGOALS (fast_tac UTerm_cs));
+by (etac uterm.induct 1);
+by (ALLGOALS (fast_tac uterm_cs));
val CONST_D = result();
val [major] = goal UTerm.thy
- "COMB(M,N): UTerm(A) ==> M: UTerm(A) & N: UTerm(A)";
+ "COMB(M,N): uterm(A) ==> M: uterm(A) & N: uterm(A)";
by (rtac (major RS setup_induction) 1);
-by (etac UTerm_induct 1);
-by (ALLGOALS (fast_tac UTerm_cs));
+by (etac uterm.induct 1);
+by (ALLGOALS (fast_tac uterm_cs));
val COMB_D = result();
(*Basic ss with constructors and their freeness*)
-val uterm_free_simps = [Const_not_Comb,Comb_not_Var,Var_not_Const,
- Comb_not_Const,Var_not_Comb,Const_not_Var,
- Var_Var_eq,Const_Const_eq,Comb_Comb_eq,
- CONST_not_COMB,COMB_not_VAR,VAR_not_CONST,
- COMB_not_CONST,VAR_not_COMB,CONST_not_VAR,
- VAR_VAR_eq,CONST_CONST_eq,COMB_COMB_eq,
- VAR_I, CONST_I, COMB_I];
+val uterm_free_simps = uterm.intrs @
+ [Const_not_Comb,Comb_not_Var,Var_not_Const,
+ Comb_not_Const,Var_not_Comb,Const_not_Var,
+ Var_Var_eq,Const_Const_eq,Comb_Comb_eq,
+ CONST_not_COMB,COMB_not_VAR,VAR_not_CONST,
+ COMB_not_CONST,VAR_not_COMB,CONST_not_VAR,
+ VAR_VAR_eq,CONST_CONST_eq,COMB_COMB_eq];
val uterm_free_ss = HOL_ss addsimps uterm_free_simps;
-goal UTerm.thy "!u. ~(t=Comb(t,u))";
+goal UTerm.thy "!u. t~=Comb(t,u)";
by (uterm_ind_tac "t" 1);
by (rtac (Var_not_Comb RS allI) 1);
by (rtac (Const_not_Comb RS allI) 1);
by (asm_simp_tac uterm_free_ss 1);
val t_not_Comb_t = result();
-goal UTerm.thy "!t. ~(u=Comb(t,u))";
+goal UTerm.thy "!t. u~=Comb(t,u)";
by (uterm_ind_tac "u" 1);
by (rtac (Var_not_Comb RS allI) 1);
by (rtac (Const_not_Comb RS allI) 1);
@@ -230,16 +204,16 @@
val u_not_Comb_u = result();
-(*** UTerm_rec -- by wf recursion on pred_Sexp ***)
+(*** UTerm_rec -- by wf recursion on pred_sexp ***)
val UTerm_rec_unfold =
- wf_pred_Sexp RS wf_trancl RS (UTerm_rec_def RS def_wfrec);
+ [UTerm_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec;
(** conversion rules **)
goalw UTerm.thy [VAR_def] "UTerm_rec(VAR(x),b,c,d) = b(x)";
by (rtac (UTerm_rec_unfold RS trans) 1);
-by (rtac Case_In0 1);
+by (simp_tac (HOL_ss addsimps [Case_In0]) 1);
val UTerm_rec_VAR = result();
goalw UTerm.thy [CONST_def] "UTerm_rec(CONST(x),b,c,d) = c(x)";
@@ -247,23 +221,25 @@
by (simp_tac (HOL_ss addsimps [Case_In0,Case_In1]) 1);
val UTerm_rec_CONST = result();
-val prems = goalw UTerm.thy [COMB_def]
- "[| M: Sexp; N: Sexp |] ==> \
-\ UTerm_rec(COMB(M,N), b, c, d) = \
-\ d(M, N, UTerm_rec(M,b,c,d), UTerm_rec(N,b,c,d))";
+goalw UTerm.thy [COMB_def]
+ "!!M N. [| M: sexp; N: sexp |] ==> \
+\ UTerm_rec(COMB(M,N), b, c, d) = \
+\ d(M, N, UTerm_rec(M,b,c,d), UTerm_rec(N,b,c,d))";
by (rtac (UTerm_rec_unfold RS trans) 1);
by (simp_tac (HOL_ss addsimps [Split,Case_In1]) 1);
-by (simp_tac (pred_Sexp_ss addsimps (In1_def::prems)) 1);
+by (asm_simp_tac (pred_sexp_ss addsimps [In1_def]) 1);
val UTerm_rec_COMB = result();
(*** uterm_rec -- by UTerm_rec ***)
-val Rep_UTerm_in_Sexp =
- Rep_UTerm RS (range_Leaf_subset_Sexp RS UTerm_subset_Sexp RS subsetD);
+val Rep_uterm_in_sexp =
+ Rep_uterm RS (range_Leaf_subset_sexp RS uterm_subset_sexp RS subsetD);
-val uterm_rec_simps = [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB,
- Abs_UTerm_inverse, Rep_UTerm_inverse, VAR_I, CONST_I, COMB_I,
- Rep_UTerm, rangeI, inj_Leaf, Inv_f_f, Rep_UTerm_in_Sexp];
+val uterm_rec_simps =
+ uterm.intrs @
+ [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB,
+ Abs_uterm_inverse, Rep_uterm_inverse,
+ Rep_uterm, rangeI, inj_Leaf, Inv_f_f, Rep_uterm_in_sexp];
val uterm_rec_ss = HOL_ss addsimps uterm_rec_simps;
goalw UTerm.thy [uterm_rec_def, Var_def] "uterm_rec(Var(x),b,c,d) = b(x)";
@@ -283,22 +259,6 @@
uterm_rec_Var, uterm_rec_Const, uterm_rec_Comb];
val uterm_ss = uterm_free_ss addsimps uterm_simps;
-(*Type checking. Useful?*)
-val major::A_subset_Sexp::prems = goal UTerm.thy
- "[| M: UTerm(A); \
-\ A<=Sexp; \
-\ !!x.x:A ==> b(x): C(VAR(x)); \
-\ !!x.x:A ==> c(x): C(CONST(x)); \
-\ !!x y q r. [| x: UTerm(A); y: UTerm(A); q: C(x); r: C(y) |] ==> \
-\ d(x,y,q,r): C(COMB(x,y)) \
-\ |] ==> UTerm_rec(M,b,c,d) : C(M)";
-val Sexp_UTermA_I = A_subset_Sexp RS UTerm_subset_Sexp RS subsetD;
-val Sexp_A_I = A_subset_Sexp RS subsetD;
-by (rtac (major RS UTerm_induct) 1);
-by (ALLGOALS
- (asm_simp_tac (uterm_ss addsimps ([Sexp_A_I,Sexp_UTermA_I] @ prems))));
-val UTerm_rec_type = result();
-
(**********)
@@ -308,13 +268,3 @@
Comb_not_Const,Var_not_Comb,Const_not_Var,
Var_Var_eq,Const_Const_eq,Comb_Comb_eq];
-(*
-val prems = goal Subst.thy
- "[| !!x.P(Var(x)); !!x.P(Const(x)); \
-\ !!u v. P(u) --> P(v) --> P(Comb(u,v)) |] ==> P(a)";
-by (uterm_ind_tac "a" 1);
-by (ALLGOALS (cut_facts_tac prems THEN' fast_tac HOL_cs));
-val uterm_induct2 = result();
-
-add_inds uterm_induct2;
-*)
--- 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