author  haftmann 
Tue, 07 Oct 2008 16:07:24 +0200  
changeset 28519  095fe24b48fd 
parent 27368  9f90ac19e32b 
child 28562  4e74209f113e 
permissions  rwrr 
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 

27368  9 
imports Plain 
15737  10 
begin 
11 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

12 
instantiation "*" :: (ord, ord) ord 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

13 
begin 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

14 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

15 
definition 
25502  16 
prod_le_def [code func 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

17 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

18 
definition 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

19 
prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

20 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

21 
instance .. 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

22 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

23 
end 
15737  24 

22177  25 
lemma [code func]: 
26 
"(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2" 

27 
"(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2" 

25502  28 
unfolding prod_le_def prod_less_def by simp_all 
22177  29 

19736  30 
instance * :: (order, order) order 
25502  31 
by default (auto simp: prod_le_def prod_less_def intro: order_less_trans) 
15737  32 

19736  33 
instance * :: (linorder, linorder) linorder 
34 
by default (auto simp: prod_le_def) 

15737  35 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

36 
instantiation * :: (linorder, linorder) distrib_lattice 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

37 
begin 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

38 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

39 
definition 
25502  40 
inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

41 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

42 
definition 
25502  43 
sup_prod_def: "(sup \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

44 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

45 
instance 
22483  46 
by intro_classes 
47 
(auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1) 

48 

19736  49 
end 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

50 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

51 
end 