equal
deleted
inserted
replaced
7 |
7 |
8 theory Product_ord |
8 theory Product_ord |
9 imports Main |
9 imports Main |
10 begin |
10 begin |
11 |
11 |
12 instance "*" :: (ord, ord) ord .. |
12 instance "*" :: (ord, ord) ord |
13 |
|
14 defs (overloaded) |
|
15 prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)" |
13 prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)" |
16 prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)" |
14 prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)" .. |
17 |
|
18 |
15 |
19 lemmas prod_ord_defs = prod_less_def prod_le_def |
16 lemmas prod_ord_defs = prod_less_def prod_le_def |
|
17 |
|
18 lemma [code]: |
|
19 "(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2" |
|
20 "(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2" |
|
21 unfolding prod_ord_defs by simp_all |
20 |
22 |
21 instance * :: (order, order) order |
23 instance * :: (order, order) order |
22 by default (auto simp: prod_ord_defs intro: order_less_trans) |
24 by default (auto simp: prod_ord_defs intro: order_less_trans) |
23 |
25 |
24 instance * :: (linorder, linorder) linorder |
26 instance * :: (linorder, linorder) linorder |