81 primrec |
81 primrec |
82 "inter [] ys = []" |
82 "inter [] ys = []" |
83 "inter (x#xs) ys = (let xs' = inter xs ys in if member ys x then x#xs' else xs')" |
83 "inter (x#xs) ys = (let xs' = inter xs ys in if member ys x then x#xs' else xs')" |
84 |
84 |
85 code_syntax_const "insert" |
85 code_syntax_const "insert" |
86 ml ("{*insert_*} _ _") |
86 ml ("{*insert_*}") |
87 haskell ("{*insert_*} _ _") |
87 haskell ("{*insert_*}") |
88 |
88 |
89 code_syntax_const "op Un" |
89 code_syntax_const "op Un" |
90 ml ("{*foldr insert_*} _ _") |
90 ml ("{*foldr insert_*}") |
91 haskell ("{*foldr insert_*} _ _") |
91 haskell ("{*foldr insert_*}") |
92 |
92 |
93 code_syntax_const "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
93 code_syntax_const "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
94 ml ("{*(flip o foldr) remove*} _ _") |
94 ml ("{*(flip o foldr) remove*}") |
95 haskell ("{*(flip o foldr) remove*} _ _") |
95 haskell ("{*(flip o foldr) remove*}") |
96 |
96 |
97 code_syntax_const "op Int" |
97 code_syntax_const "op Int" |
98 ml ("{*inter*} _ _") |
98 ml ("{*inter*}") |
99 haskell ("{*inter*} _ _") |
99 haskell ("{*inter*}") |
100 |
100 |
101 code_syntax_const "image" |
101 code_syntax_const "image" |
102 ml ("{*\<lambda>f. foldr (insert_ o f)*} _ _ _") |
102 ml ("{*\<lambda>f. foldr (insert_ o f)*}") |
103 haskell ("{*\<lambda>f. foldr (insert_ o f)*} _ _ _") |
103 haskell ("{*\<lambda>f. foldr (insert_ o f)*}") |
104 |
104 |
105 code_syntax_const "INTER" |
105 code_syntax_const "INTER" |
106 ml ("{*\<lambda>xs f. foldr (inter o f) xs*} _ _") |
106 ml ("{*\<lambda>xs f. foldr (inter o f) xs*}") |
107 haskell ("{*\<lambda>xs f. foldr (inter o f) xs*} _ _") |
107 haskell ("{*\<lambda>xs f. foldr (inter o f) xs*}") |
108 |
108 |
109 code_syntax_const "UNION" |
109 code_syntax_const "UNION" |
110 ml ("{*\<lambda>xs f. foldr (foldr insert_ o f) xs*} _ _") |
110 ml ("{*\<lambda>xs f. foldr (foldr insert_ o f) xs*}") |
111 haskell ("{*\<lambda>xs f. foldr (foldr insert_ o f) xs*} _ _") |
111 haskell ("{*\<lambda>xs f. foldr (foldr insert_ o f) xs*}") |
112 |
112 |
113 code_primconst "Ball" |
113 code_primconst "Ball" |
114 ml {* |
114 ml {* |
115 fun `_` [] f = true |
115 fun `_` [] f = true |
116 | `_` (x::xs) f = f x andalso `_` xs f; |
116 | `_` (x::xs) f = f x andalso `_` xs f; |