equal
deleted
inserted
replaced
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 |