96 lemma boundedE: |
96 lemma boundedE: |
97 assumes "a \<preceq> b * c" |
97 assumes "a \<preceq> b * c" |
98 obtains "a \<preceq> b" and "a \<preceq> c" |
98 obtains "a \<preceq> b" and "a \<preceq> c" |
99 using assms by (blast intro: trans cobounded1 cobounded2) |
99 using assms by (blast intro: trans cobounded1 cobounded2) |
100 |
100 |
101 lemma bounded_iff: |
101 lemma bounded_iff (* [simp] CANDIDATE *): |
102 "a \<preceq> b * c \<longleftrightarrow> a \<preceq> b \<and> a \<preceq> c" |
102 "a \<preceq> b * c \<longleftrightarrow> a \<preceq> b \<and> a \<preceq> c" |
103 by (blast intro: boundedI elim: boundedE) |
103 by (blast intro: boundedI elim: boundedE) |
104 |
104 |
105 lemma strict_boundedE: |
105 lemma strict_boundedE: |
106 assumes "a \<prec> b * c" |
106 assumes "a \<prec> b * c" |
113 |
113 |
114 lemma coboundedI2: |
114 lemma coboundedI2: |
115 "b \<preceq> c \<Longrightarrow> a * b \<preceq> c" |
115 "b \<preceq> c \<Longrightarrow> a * b \<preceq> c" |
116 by (rule trans) auto |
116 by (rule trans) auto |
117 |
117 |
|
118 lemma strict_coboundedI1: |
|
119 "a \<prec> c \<Longrightarrow> a * b \<prec> c" |
|
120 using irrefl |
|
121 by (auto intro: not_eq_order_implies_strict coboundedI1 strict_implies_order elim: strict_boundedE) |
|
122 |
|
123 lemma strict_coboundedI2: |
|
124 "b \<prec> c \<Longrightarrow> a * b \<prec> c" |
|
125 using strict_coboundedI1 [of b c a] by (simp add: commute) |
|
126 |
118 lemma mono: "a \<preceq> c \<Longrightarrow> b \<preceq> d \<Longrightarrow> a * b \<preceq> c * d" |
127 lemma mono: "a \<preceq> c \<Longrightarrow> b \<preceq> d \<Longrightarrow> a * b \<preceq> c * d" |
119 by (blast intro: boundedI coboundedI1 coboundedI2) |
128 by (blast intro: boundedI coboundedI1 coboundedI2) |
120 |
129 |
121 lemma absorb1: "a \<preceq> b \<Longrightarrow> a * b = a" |
130 lemma absorb1: "a \<preceq> b \<Longrightarrow> a * b = a" |
122 by (rule antisym) (auto simp add: refl bounded_iff) |
131 by (rule antisym) (auto simp add: bounded_iff refl) |
123 |
132 |
124 lemma absorb2: "b \<preceq> a \<Longrightarrow> a * b = b" |
133 lemma absorb2: "b \<preceq> a \<Longrightarrow> a * b = b" |
125 by (rule antisym) (auto simp add: refl bounded_iff) |
134 by (rule antisym) (auto simp add: bounded_iff refl) |
|
135 |
|
136 lemma absorb_iff1: "a \<preceq> b \<longleftrightarrow> a * b = a" |
|
137 using order_iff by auto |
|
138 |
|
139 lemma absorb_iff2: "b \<preceq> a \<longleftrightarrow> a * b = b" |
|
140 using order_iff by (auto simp add: commute) |
126 |
141 |
127 end |
142 end |
128 |
143 |
129 locale semilattice_neutr_order = semilattice_neutr + semilattice_order |
144 locale semilattice_neutr_order = semilattice_neutr + semilattice_order |
130 begin |
145 begin |