equal
deleted
inserted
replaced
223 |
223 |
224 lemma max_less_iff_conj [simp]: |
224 lemma max_less_iff_conj [simp]: |
225 "max x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<and> y \<^loc>< z" |
225 "max x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<and> y \<^loc>< z" |
226 unfolding max_def le_less using less_linear by (auto intro: less_trans) |
226 unfolding max_def le_less using less_linear by (auto intro: less_trans) |
227 |
227 |
228 lemma split_min: |
228 lemma split_min [noatp]: |
229 "P (min i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P i) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P j)" |
229 "P (min i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P i) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P j)" |
230 by (simp add: min_def) |
230 by (simp add: min_def) |
231 |
231 |
232 lemma split_max: |
232 lemma split_max [noatp]: |
233 "P (max i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P j) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P i)" |
233 "P (max i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P j) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P i)" |
234 by (simp add: max_def) |
234 by (simp add: max_def) |
235 |
235 |
236 end |
236 end |
237 |
237 |