src/HOL/Subst/UTerm.thy
 changeset 1476 608483c2122a parent 1381 57777949b2f8 child 2903 d1d5a0acbf72
```     1.1 --- a/src/HOL/Subst/UTerm.thy	Mon Feb 05 21:27:16 1996 +0100
1.2 +++ b/src/HOL/Subst/UTerm.thy	Mon Feb 05 21:29:06 1996 +0100
1.3 @@ -1,8 +1,8 @@
1.4 -(*  Title: 	Substitutions/UTerm.thy
1.5 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
1.6 +(*  Title:      Substitutions/UTerm.thy
1.7 +    Author:     Martin Coen, Cambridge University Computer Laboratory
1.8      Copyright   1993  University of Cambridge
1.9
1.10 -Simple term structure for unifiation.
1.11 +Simple term structure for unification.
1.12  Binary trees with leaves that are constants or variables.
1.13  *)
1.14
1.15 @@ -30,32 +30,32 @@
1.16
1.17  defs
1.18       (*defining the concrete constructors*)
1.19 -  VAR_def  	"VAR(v) == In0(v)"
1.20 -  CONST_def  	"CONST(v) == In1(In0(v))"
1.21 -  COMB_def 	"COMB t u == In1(In1(t \$ u))"
1.22 +  VAR_def       "VAR(v) == In0(v)"
1.23 +  CONST_def     "CONST(v) == In1(In0(v))"
1.24 +  COMB_def      "COMB t u == In1(In1(t \$ u))"
1.25
1.26  inductive "uterm(A)"
1.27    intrs
1.28 -    VAR_I	   "v:A ==> VAR(v) : uterm(A)"
1.29 +    VAR_I          "v:A ==> VAR(v) : uterm(A)"
1.30      CONST_I  "c:A ==> CONST(c) : uterm(A)"
1.31      COMB_I   "[| M:uterm(A);  N:uterm(A) |] ==> COMB M N : uterm(A)"
1.32
1.33  rules
1.34      (*faking a type definition...*)
1.35 -  Rep_uterm 		"Rep_uterm(xs): uterm(range(Leaf))"
1.36 -  Rep_uterm_inverse 	"Abs_uterm(Rep_uterm(xs)) = xs"
1.37 -  Abs_uterm_inverse 	"M: uterm(range(Leaf)) ==> Rep_uterm(Abs_uterm(M)) = M"
1.38 +  Rep_uterm             "Rep_uterm(xs): uterm(range(Leaf))"
1.39 +  Rep_uterm_inverse     "Abs_uterm(Rep_uterm(xs)) = xs"
1.40 +  Abs_uterm_inverse     "M: uterm(range(Leaf)) ==> Rep_uterm(Abs_uterm(M)) = M"
1.41
1.42  defs
1.43       (*defining the abstract constructors*)
1.44 -  Var_def  	"Var(v) == Abs_uterm(VAR(Leaf(v)))"
1.45 -  Const_def  	"Const(c) == Abs_uterm(CONST(Leaf(c)))"
1.46 -  Comb_def 	"Comb t u == Abs_uterm (COMB (Rep_uterm t) (Rep_uterm u))"
1.47 +  Var_def       "Var(v) == Abs_uterm(VAR(Leaf(v)))"
1.48 +  Const_def     "Const(c) == Abs_uterm(CONST(Leaf(c)))"
1.49 +  Comb_def      "Comb t u == Abs_uterm (COMB (Rep_uterm t) (Rep_uterm u))"
1.50
1.51       (*uterm recursion*)
1.52 -  UTerm_rec_def
1.53 -   "UTerm_rec M b c d == wfrec (trancl pred_sexp) M
1.54 -          (Case (%x g.b(x)) (Case (%y g. c(y)) (Split (%x y g. d x y (g x) (g y)))))"
1.55 +  UTerm_rec_def
1.56 +   "UTerm_rec M b c d == wfrec (trancl pred_sexp)
1.57 +    (%g. Case (%x.b(x)) (Case (%y. c(y)) (Split (%x y. d x y (g x) (g y))))) M"
1.58
1.59    uterm_rec_def
1.60     "uterm_rec t b c d ==
```