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 ==