13 |
13 |
14 type_synonym 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool" |
14 type_synonym 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool" |
15 type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
15 type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
16 type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop" |
16 type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop" |
17 |
17 |
18 consts |
18 definition lesub :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
19 "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
19 where "lesub x r y \<longleftrightarrow> r x y" |
20 "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
20 |
21 "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" |
21 definition lesssub :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
22 (*<*) |
22 where "lesssub x r y \<longleftrightarrow> lesub x r y \<and> x \<noteq> y" |
|
23 |
|
24 definition plussub :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" |
|
25 where "plussub x f y = f x y" |
|
26 |
23 notation (ASCII) |
27 notation (ASCII) |
24 "lesub" ("(_ /<='__ _)" [50, 1000, 51] 50) and |
28 "lesub" ("(_ /<='__ _)" [50, 1000, 51] 50) and |
25 "lesssub" ("(_ /<'__ _)" [50, 1000, 51] 50) and |
29 "lesssub" ("(_ /<'__ _)" [50, 1000, 51] 50) and |
26 "plussub" ("(_ /+'__ _)" [65, 1000, 66] 65) |
30 "plussub" ("(_ /+'__ _)" [65, 1000, 66] 65) |
27 (*>*) |
31 |
28 notation |
32 notation |
29 "lesub" ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and |
33 "lesub" ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and |
30 "lesssub" ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and |
34 "lesssub" ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and |
31 "plussub" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65) |
35 "plussub" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65) |
32 (*<*) |
36 |
33 (* allow \<sub> instead of \<bsub>..\<esub> *) |
37 (* allow \<sub> instead of \<bsub>..\<esub> *) |
34 |
|
35 abbreviation (input) |
38 abbreviation (input) |
36 lesub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50) |
39 lesub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50) |
37 where "x \<sqsubseteq>\<^sub>r y == x \<sqsubseteq>\<^bsub>r\<^esub> y" |
40 where "x \<sqsubseteq>\<^sub>r y == x \<sqsubseteq>\<^bsub>r\<^esub> y" |
38 |
41 |
39 abbreviation (input) |
42 abbreviation (input) |
41 where "x \<sqsubset>\<^sub>r y == x \<sqsubset>\<^bsub>r\<^esub> y" |
44 where "x \<sqsubset>\<^sub>r y == x \<sqsubset>\<^bsub>r\<^esub> y" |
42 |
45 |
43 abbreviation (input) |
46 abbreviation (input) |
44 plussub1 :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65) |
47 plussub1 :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65) |
45 where "x \<squnion>\<^sub>f y == x \<squnion>\<^bsub>f\<^esub> y" |
48 where "x \<squnion>\<^sub>f y == x \<squnion>\<^bsub>f\<^esub> y" |
46 (*>*) |
|
47 |
|
48 defs |
|
49 lesub_def: "x \<sqsubseteq>\<^sub>r y \<equiv> r x y" |
|
50 lesssub_def: "x \<sqsubset>\<^sub>r y \<equiv> x \<sqsubseteq>\<^sub>r y \<and> x \<noteq> y" |
|
51 plussub_def: "x \<squnion>\<^sub>f y \<equiv> f x y" |
|
52 |
49 |
53 definition ord :: "('a \<times> 'a) set \<Rightarrow> 'a ord" where |
50 definition ord :: "('a \<times> 'a) set \<Rightarrow> 'a ord" where |
54 "ord r \<equiv> \<lambda>x y. (x,y) \<in> r" |
51 "ord r \<equiv> \<lambda>x y. (x,y) \<in> r" |
55 |
52 |
56 definition order :: "'a ord \<Rightarrow> bool" where |
53 definition order :: "'a ord \<Rightarrow> bool" where |