ex/Term.thy
changeset 48 21291189b51e
parent 0 7949f97df77a
child 72 30e80f028c57
equal deleted inserted replaced
47:69d815b0e1eb 48:21291189b51e
    30   Abs_Term_inverse 	"M: Term(range(Leaf)) ==> Rep_Term(Abs_Term(M)) = M"
    30   Abs_Term_inverse 	"M: Term(range(Leaf)) ==> Rep_Term(Abs_Term(M)) = M"
    31     (*defining abstraction/representation functions for term list...*)
    31     (*defining abstraction/representation functions for term list...*)
    32   Rep_TList_def	"Rep_TList == Rep_map(Rep_Term)"
    32   Rep_TList_def	"Rep_TList == Rep_map(Rep_Term)"
    33   Abs_TList_def	"Abs_TList == Abs_map(Abs_Term)"
    33   Abs_TList_def	"Abs_TList == Abs_map(Abs_Term)"
    34     (*defining the abstract constants*)
    34     (*defining the abstract constants*)
    35   App_def 	"App(a,ts) == Abs_Term(Leaf(a) . Rep_TList(ts))"
    35   App_def 	"App(a,ts) == Abs_Term(Leaf(a) $ Rep_TList(ts))"
    36      (*list recursion*)
    36      (*list recursion*)
    37   Term_rec_def	
    37   Term_rec_def	
    38    "Term_rec(M,d) == wfrec(trancl(pred_Sexp),  M, \
    38    "Term_rec(M,d) == wfrec(trancl(pred_Sexp),  M, \
    39 \            %M g. Split(M, %x y. d(x,y, Abs_map(g,y))))"
    39 \            %M g. Split(M, %x y. d(x,y, Abs_map(g,y))))"
    40 
    40