30 greaterThanAtMost :: "['a::ord, 'a] => 'a set" ("(1{')_.._})") |
30 greaterThanAtMost :: "['a::ord, 'a] => 'a set" ("(1{')_.._})") |
31 "{)l..u} == {)l..} Int {..u}" |
31 "{)l..u} == {)l..} Int {..u}" |
32 |
32 |
33 atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})") |
33 atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})") |
34 "{l..u} == {l..} Int {..u}" |
34 "{l..u} == {l..} Int {..u}" |
|
35 |
|
36 syntax |
|
37 "@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3UN _<=_./ _)" 10) |
|
38 "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3UN _<_./ _)" 10) |
|
39 "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3INT _<=_./ _)" 10) |
|
40 "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3INT _<_./ _)" 10) |
|
41 |
|
42 syntax (input) |
|
43 "@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3\<Union> _\<le>_./ _)" 10) |
|
44 "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3\<Union> _<_./ _)" 10) |
|
45 "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _\<le>_./ _)" 10) |
|
46 "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _<_./ _)" 10) |
|
47 |
|
48 syntax (xsymbols) |
|
49 "@UNION_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>\<^bsub>_ \<le> _\<^esub>/ _)" 10) |
|
50 "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>\<^bsub>_ < _\<^esub>/ _)" 10) |
|
51 "@INTER_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>\<^bsub>_ \<le> _\<^esub>/ _)" 10) |
|
52 "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>\<^bsub>_ < _\<^esub>/ _)" 10) |
|
53 |
|
54 translations |
|
55 "UN i<=n. A" == "UN i:{..n}. A" |
|
56 "UN i<n. A" == "UN i:{..n(}. A" |
|
57 "INT i<=n. A" == "INT i:{..n}. A" |
|
58 "INT i<n. A" == "INT i:{..n(}. A" |
|
59 |
35 |
60 |
36 subsection {*lessThan*} |
61 subsection {*lessThan*} |
37 |
62 |
38 lemma lessThan_iff [iff]: "(i: lessThan k) = (i<k)" |
63 lemma lessThan_iff [iff]: "(i: lessThan k) = (i<k)" |
39 by (simp add: lessThan_def) |
64 by (simp add: lessThan_def) |