15737
|
1 |
(* Title: HOL/Library/Product_ord.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Norbert Voelker
|
|
4 |
*)
|
|
5 |
|
17200
|
6 |
header {* Order on product types *}
|
15737
|
7 |
|
|
8 |
theory Product_ord
|
|
9 |
imports Main
|
|
10 |
begin
|
|
11 |
|
21458
|
12 |
instance "*" :: (ord, ord) ord
|
22177
|
13 |
prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x \<le> snd y)"
|
|
14 |
prod_less_def: "(x < y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x < snd y)" ..
|
15737
|
15 |
|
22845
|
16 |
lemmas prod_ord_defs [code func del] = prod_less_def prod_le_def
|
15737
|
17 |
|
22177
|
18 |
lemma [code func]:
|
|
19 |
"(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
|
|
20 |
"(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
|
|
21 |
unfolding prod_ord_defs by simp_all
|
|
22 |
|
21458
|
23 |
lemma [code]:
|
|
24 |
"(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
|
|
25 |
"(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
|
|
26 |
unfolding prod_ord_defs by simp_all
|
|
27 |
|
19736
|
28 |
instance * :: (order, order) order
|
|
29 |
by default (auto simp: prod_ord_defs intro: order_less_trans)
|
15737
|
30 |
|
19736
|
31 |
instance * :: (linorder, linorder) linorder
|
|
32 |
by default (auto simp: prod_le_def)
|
15737
|
33 |
|
22483
|
34 |
instance * :: (linorder, linorder) distrib_lattice
|
|
35 |
inf_prod_def: "inf \<equiv> min"
|
|
36 |
sup_prod_def: "sup \<equiv> max"
|
|
37 |
by intro_classes
|
|
38 |
(auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
|
|
39 |
|
19736
|
40 |
end
|