author  haftmann 
Thu, 01 Jul 2010 16:54:44 +0200  
changeset 37678  0040bafffdef 
parent 31040  996ae76c9eda 
child 37765  26bdfb7b680b 
permissions  rwrr 
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 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
31040
diff
changeset

11 
instantiation prod :: (ord, ord) ord 
25571
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 
31040  15 
prod_le_def [code del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> 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 
31040  18 
prod_less_def [code del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> 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]: 
31040  25 
"(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2" 
26 
"(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2" 

25502  27 
unfolding prod_le_def prod_less_def by simp_all 
22177  28 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
31040
diff
changeset

29 
instance prod :: (preorder, preorder) preorder proof 
31040  30 
qed (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans) 
15737  31 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
31040
diff
changeset

32 
instance prod :: (order, order) order proof 
31040  33 
qed (auto simp add: prod_le_def) 
34 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
31040
diff
changeset

35 
instance prod :: (linorder, linorder) linorder proof 
31040  36 
qed (auto simp: prod_le_def) 
15737  37 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
31040
diff
changeset

38 
instantiation prod :: (linorder, linorder) distrib_lattice 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

39 
begin 
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 
inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min" 
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 
definition 
25502  45 
sup_prod_def: "(sup \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

46 

31040  47 
instance proof 
48 
qed (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1) 

49 

50 
end 

51 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
31040
diff
changeset

52 
instantiation prod :: (bot, bot) bot 
31040  53 
begin 
54 

55 
definition 

56 
bot_prod_def: "bot = (bot, bot)" 

57 

58 
instance proof 

59 
qed (auto simp add: bot_prod_def prod_le_def) 

60 

61 
end 

62 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
31040
diff
changeset

63 
instantiation prod :: (top, top) top 
31040  64 
begin 
65 

66 
definition 

67 
top_prod_def: "top = (top, top)" 

68 

69 
instance proof 

70 
qed (auto simp add: top_prod_def prod_le_def) 

22483  71 

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

73 

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

74 
end 