equal
deleted
inserted
replaced
38 (*defining the abstract constants*) |
38 (*defining the abstract constants*) |
39 App_def "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))" |
39 App_def "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))" |
40 |
40 |
41 (*list recursion*) |
41 (*list recursion*) |
42 Term_rec_def |
42 Term_rec_def |
43 "Term_rec M d == wfrec (trancl pred_sexp) M \ |
43 "Term_rec M d == wfrec (trancl pred_sexp) M |
44 \ (Split(%x y g. d x y (Abs_map g y)))" |
44 (Split(%x y g. d x y (Abs_map g y)))" |
45 |
45 |
46 term_rec_def |
46 term_rec_def |
47 "term_rec t d == \ |
47 "term_rec t d == |
48 \ Term_rec (Rep_term t) (%x y r. d (Inv Leaf x) (Abs_Tlist(y)) r)" |
48 Term_rec (Rep_term t) (%x y r. d (Inv Leaf x) (Abs_Tlist(y)) r)" |
49 |
49 |
50 rules |
50 rules |
51 (*faking a type definition for term...*) |
51 (*faking a type definition for term...*) |
52 Rep_term "Rep_term(n): term(range(Leaf))" |
52 Rep_term "Rep_term(n): term(range(Leaf))" |
53 Rep_term_inverse "Abs_term(Rep_term(t)) = t" |
53 Rep_term_inverse "Abs_term(Rep_term(t)) = t" |