54 translations |
54 translations |
55 "[x, xs]" == "x#[xs]" |
55 "[x, xs]" == "x#[xs]" |
56 "[x]" == "x#[]" |
56 "[x]" == "x#[]" |
57 "[]" == "Nil" |
57 "[]" == "Nil" |
58 |
58 |
59 "case xs of Nil => a | y#ys => b" == "list_case a (%y ys.b) xs" |
59 "case xs of Nil => a | y#ys => b" == "list_case a (%y ys. b) xs" |
60 |
60 |
61 "[x:xs . P]" == "filter (%x.P) xs" |
61 "[x:xs . P]" == "filter (%x. P) xs" |
62 |
62 |
63 defs |
63 defs |
64 (* Defining the Concrete Constructors *) |
64 (* Defining the Concrete Constructors *) |
65 NIL_def "NIL == In0(Numb(0))" |
65 NIL_def "NIL == In0(Numb(0))" |
66 CONS_def "CONS M N == In1(M $ N)" |
66 CONS_def "CONS M N == In1(M $ N)" |
80 defs |
80 defs |
81 (* Defining the Abstract Constructors *) |
81 (* Defining the Abstract Constructors *) |
82 Nil_def "Nil == Abs_list(NIL)" |
82 Nil_def "Nil == Abs_list(NIL)" |
83 Cons_def "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))" |
83 Cons_def "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))" |
84 |
84 |
85 List_case_def "List_case c d == Case (%x.c) (Split d)" |
85 List_case_def "List_case c d == Case (%x. c) (Split d)" |
86 |
86 |
87 (* list Recursion -- the trancl is Essential; see list.ML *) |
87 (* list Recursion -- the trancl is Essential; see list.ML *) |
88 |
88 |
89 List_rec_def |
89 List_rec_def |
90 "List_rec M c d == wfrec (trancl pred_sexp) |
90 "List_rec M c d == wfrec (trancl pred_sexp) |
97 (* Generalized Map Functionals *) |
97 (* Generalized Map Functionals *) |
98 |
98 |
99 Rep_map_def "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)" |
99 Rep_map_def "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)" |
100 Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)" |
100 Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)" |
101 |
101 |
102 null_def "null(xs) == list_rec xs True (%x xs r.False)" |
102 null_def "null(xs) == list_rec xs True (%x xs r. False)" |
103 hd_def "hd(xs) == list_rec xs arbitrary (%x xs r.x)" |
103 hd_def "hd(xs) == list_rec xs arbitrary (%x xs r. x)" |
104 tl_def "tl(xs) == list_rec xs arbitrary (%x xs r.xs)" |
104 tl_def "tl(xs) == list_rec xs arbitrary (%x xs r. xs)" |
105 (* a total version of tl: *) |
105 (* a total version of tl: *) |
106 ttl_def "ttl(xs) == list_rec xs [] (%x xs r.xs)" |
106 ttl_def "ttl(xs) == list_rec xs [] (%x xs r. xs)" |
107 |
107 |
108 set_def "set xs == list_rec xs {} (%x l r. insert x r)" |
108 set_def "set xs == list_rec xs {} (%x l r. insert x r)" |
109 |
109 |
110 mem_def "x mem xs == |
110 mem_def "x mem xs == |
111 list_rec xs False (%y ys r. if y=x then True else r)" |
111 list_rec xs False (%y ys r. if y=x then True else r)" |
112 map_def "map f xs == list_rec xs [] (%x l r. f(x)#r)" |
112 map_def "map f xs == list_rec xs [] (%x l r. f(x)#r)" |
113 append_def "xs@ys == list_rec xs ys (%x l r. x#r)" |
113 append_def "xs@ys == list_rec xs ys (%x l r. x#r)" |
114 filter_def "filter P xs == |
114 filter_def "filter P xs == |
115 list_rec xs [] (%x xs r. if P(x) then x#r else r)" |
115 list_rec xs [] (%x xs r. if P(x) then x#r else r)" |
116 |
116 |
117 list_case_def "list_case a f xs == list_rec xs a (%x xs r.f x xs)" |
117 list_case_def "list_case a f xs == list_rec xs a (%x xs r. f x xs)" |
118 |
118 |
119 end |
119 end |