equal
deleted
inserted
replaced
157 |
157 |
158 |
158 |
159 subsection {* Parallel lists *} |
159 subsection {* Parallel lists *} |
160 |
160 |
161 definition |
161 definition |
162 parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) |
162 parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) where |
163 "(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)" |
163 "(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)" |
164 |
164 |
165 lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys" |
165 lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys" |
166 unfolding parallel_def by blast |
166 unfolding parallel_def by blast |
167 |
167 |
216 |
216 |
217 |
217 |
218 subsection {* Postfix order on lists *} |
218 subsection {* Postfix order on lists *} |
219 |
219 |
220 definition |
220 definition |
221 postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) |
221 postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) where |
222 "(xs >>= ys) = (\<exists>zs. xs = zs @ ys)" |
222 "(xs >>= ys) = (\<exists>zs. xs = zs @ ys)" |
223 |
223 |
224 lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys" |
224 lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys" |
225 unfolding postfix_def by blast |
225 unfolding postfix_def by blast |
226 |
226 |