15 "list n A == {xs. length xs = n & set xs <= A}" |
15 "list n A == {xs. length xs = n & set xs <= A}" |
16 |
16 |
17 le :: "'a ord \<Rightarrow> ('a list)ord" |
17 le :: "'a ord \<Rightarrow> ('a list)ord" |
18 "le r == list_all2 (%x y. x <=_r y)" |
18 "le r == list_all2 (%x y. x <=_r y)" |
19 |
19 |
20 syntax "@lesublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool" |
20 abbreviation |
|
21 lesublist_syntax :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool" |
21 ("(_ /<=[_] _)" [50, 0, 51] 50) |
22 ("(_ /<=[_] _)" [50, 0, 51] 50) |
22 syntax "@lesssublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool" |
23 where "x <=[r] y == x <=_(le r) y" |
|
24 |
|
25 abbreviation |
|
26 lesssublist_syntax :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool" |
23 ("(_ /<[_] _)" [50, 0, 51] 50) |
27 ("(_ /<[_] _)" [50, 0, 51] 50) |
24 translations |
28 where "x <[r] y == x <_(le r) y" |
25 "x <=[r] y" == "x <=_(Listn.le r) y" |
|
26 "x <[r] y" == "x <_(Listn.le r) y" |
|
27 |
29 |
28 constdefs |
30 constdefs |
29 map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" |
31 map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" |
30 "map2 f == (%xs ys. map (split f) (zip xs ys))" |
32 "map2 f == (%xs ys. map (split f) (zip xs ys))" |
31 |
33 |
32 syntax "@plussublist" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list" |
34 abbreviation |
|
35 plussublist_syntax :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list" |
33 ("(_ /+[_] _)" [65, 0, 66] 65) |
36 ("(_ /+[_] _)" [65, 0, 66] 65) |
34 translations "x +[f] y" == "x +_(map2 f) y" |
37 where "x +[f] y == x +_(map2 f) y" |
35 |
38 |
36 consts coalesce :: "'a err list \<Rightarrow> 'a list err" |
39 consts coalesce :: "'a err list \<Rightarrow> 'a list err" |
37 primrec |
40 primrec |
38 "coalesce [] = OK[]" |
41 "coalesce [] = OK[]" |
39 "coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)" |
42 "coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)" |