author | haftmann |
Fri, 27 Mar 2009 10:05:11 +0100 | |
changeset 30738 | 0842e906300c |
parent 28562 | 4e74209f113e |
child 31040 | 996ae76c9eda |
permissions | -rw-r--r-- |
15737 | 1 |
(* Title: HOL/Library/Product_ord.thy |
2 |
Author: Norbert Voelker |
|
3 |
*) |
|
4 |
||
17200 | 5 |
header {* Order on product types *} |
15737 | 6 |
|
7 |
theory Product_ord |
|
30738 | 8 |
imports Main |
15737 | 9 |
begin |
10 |
||
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
11 |
instantiation "*" :: (ord, ord) ord |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
12 |
begin |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
13 |
|
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
14 |
definition |
28562 | 15 |
prod_le_def [code del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y" |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
16 |
|
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
17 |
definition |
28562 | 18 |
prod_less_def [code del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y" |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
19 |
|
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
20 |
instance .. |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
21 |
|
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
22 |
end |
15737 | 23 |
|
28562 | 24 |
lemma [code]: |
22177 | 25 |
"(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2" |
26 |
"(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2" |
|
25502 | 27 |
unfolding prod_le_def prod_less_def by simp_all |
22177 | 28 |
|
19736 | 29 |
instance * :: (order, order) order |
25502 | 30 |
by default (auto simp: prod_le_def prod_less_def intro: order_less_trans) |
15737 | 31 |
|
19736 | 32 |
instance * :: (linorder, linorder) linorder |
33 |
by default (auto simp: prod_le_def) |
|
15737 | 34 |
|
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
35 |
instantiation * :: (linorder, linorder) distrib_lattice |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
36 |
begin |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
37 |
|
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
38 |
definition |
25502 | 39 |
inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min" |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
40 |
|
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
41 |
definition |
25502 | 42 |
sup_prod_def: "(sup \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max" |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
43 |
|
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
44 |
instance |
22483 | 45 |
by intro_classes |
46 |
(auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1) |
|
47 |
||
19736 | 48 |
end |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
49 |
|
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
50 |
end |