equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Product_Lexorder.thy |
1 (* Title: HOL/Library/Product_Lexorder.thy |
2 Author: Norbert Voelker |
2 Author: Norbert Voelker |
3 *) |
3 *) |
4 |
4 |
5 section {* Lexicographic order on product types *} |
5 section \<open>Lexicographic order on product types\<close> |
6 |
6 |
7 theory Product_Lexorder |
7 theory Product_Lexorder |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
27 |
27 |
28 lemma less_prod_simp [simp, code]: |
28 lemma less_prod_simp [simp, code]: |
29 "(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2" |
29 "(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2" |
30 by (simp add: less_prod_def) |
30 by (simp add: less_prod_def) |
31 |
31 |
32 text {* A stronger version for partial orders. *} |
32 text \<open>A stronger version for partial orders.\<close> |
33 |
33 |
34 lemma less_prod_def': |
34 lemma less_prod_def': |
35 fixes x y :: "'a::order \<times> 'b::ord" |
35 fixes x y :: "'a::order \<times> 'b::ord" |
36 shows "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y" |
36 shows "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y" |
37 by (auto simp add: less_prod_def le_less) |
37 by (auto simp add: less_prod_def le_less) |
117 qed |
117 qed |
118 qed |
118 qed |
119 qed |
119 qed |
120 qed |
120 qed |
121 |
121 |
122 text {* Legacy lemma bindings *} |
122 text \<open>Legacy lemma bindings\<close> |
123 |
123 |
124 lemmas prod_le_def = less_eq_prod_def |
124 lemmas prod_le_def = less_eq_prod_def |
125 lemmas prod_less_def = less_prod_def |
125 lemmas prod_less_def = less_prod_def |
126 lemmas prod_less_eq = less_prod_def' |
126 lemmas prod_less_eq = less_prod_def' |
127 |
127 |