author  haftmann 
Thu, 25 Jul 2013 08:57:16 +0200  
changeset 52729  412c9e0381a1 
parent 51115  7dbd6832a689 
child 53015  a1119cf551e8 
permissions  rwrr 
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

1 
(* Title: HOL/Library/Product_Lexorder.thy 
15737  2 
Author: Norbert Voelker 
3 
*) 

4 

51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

5 
header {* Lexicographic order on product types *} 
15737  6 

51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

7 
theory Product_Lexorder 
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 
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

15 
"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 
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

18 
"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 

51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

24 
lemma less_eq_prod_simp [simp, code]: 
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

25 
"(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2" 
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

26 
by (simp add: less_eq_prod_def) 
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

27 

7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

28 
lemma less_prod_simp [simp, code]: 
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

29 
"(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2" 
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

30 
by (simp add: less_prod_def) 
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

31 

7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

32 
text {* A stronger version for partial orders. *} 
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

33 

7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

34 
lemma less_prod_def': 
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

35 
fixes x y :: "'a::order \<times> 'b::ord" 
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

36 
shows "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y" 
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

37 
by (auto simp add: less_prod_def le_less) 
22177  38 

47961  39 
instance prod :: (preorder, preorder) preorder 
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

40 
by default (auto simp: less_eq_prod_def less_prod_def less_le_not_le intro: order_trans) 
15737  41 

47961  42 
instance prod :: (order, order) order 
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

43 
by default (auto simp add: less_eq_prod_def) 
31040  44 

47961  45 
instance prod :: (linorder, linorder) linorder 
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

46 
by default (auto simp: less_eq_prod_def) 
15737  47 

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

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

49 
begin 
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 
definition 
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

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

53 

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

54 
definition 
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

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

56 

47961  57 
instance 
58 
by default (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1) 

31040  59 

60 
end 

61 

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

62 
instantiation prod :: (bot, bot) bot 
31040  63 
begin 
64 

65 
definition 

51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

66 
"bot = (bot, bot)" 
31040  67 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51115
diff
changeset

68 
instance .. 
31040  69 

70 
end 

71 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51115
diff
changeset

72 
instance prod :: (order_bot, order_bot) order_bot 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51115
diff
changeset

73 
by default (auto simp add: bot_prod_def) 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51115
diff
changeset

74 

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

75 
instantiation prod :: (top, top) top 
31040  76 
begin 
77 

78 
definition 

51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

79 
"top = (top, top)" 
31040  80 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51115
diff
changeset

81 
instance .. 
22483  82 

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

84 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51115
diff
changeset

85 
instance prod :: (order_top, order_top) order_top 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51115
diff
changeset

86 
by default (auto simp add: top_prod_def) 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51115
diff
changeset

87 

44063
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset

88 
instance prod :: (wellorder, wellorder) wellorder 
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset

89 
proof 
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset

90 
fix P :: "'a \<times> 'b \<Rightarrow> bool" and z :: "'a \<times> 'b" 
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset

91 
assume P: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x" 
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset

92 
show "P z" 
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset

93 
proof (induct z) 
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset

94 
case (Pair a b) 
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset

95 
show "P (a, b)" 
47961  96 
proof (induct a arbitrary: b rule: less_induct) 
97 
case (less a\<^isub>1) note a\<^isub>1 = this 

98 
show "P (a\<^isub>1, b)" 

99 
proof (induct b rule: less_induct) 

100 
case (less b\<^isub>1) note b\<^isub>1 = this 

101 
show "P (a\<^isub>1, b\<^isub>1)" 

102 
proof (rule P) 

103 
fix p assume p: "p < (a\<^isub>1, b\<^isub>1)" 

104 
show "P p" 

105 
proof (cases "fst p < a\<^isub>1") 

106 
case True 

107 
then have "P (fst p, snd p)" by (rule a\<^isub>1) 

108 
then show ?thesis by simp 

109 
next 

110 
case False 

111 
with p have 1: "a\<^isub>1 = fst p" and 2: "snd p < b\<^isub>1" 

51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

112 
by (simp_all add: less_prod_def') 
47961  113 
from 2 have "P (a\<^isub>1, snd p)" by (rule b\<^isub>1) 
114 
with 1 show ?thesis by simp 

115 
qed 

116 
qed 

117 
qed 

118 
qed 

44063
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset

119 
qed 
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset

120 
qed 
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset

121 

51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

122 
text {* Legacy lemma bindings *} 
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

123 

7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

124 
lemmas prod_le_def = less_eq_prod_def 
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

125 
lemmas prod_less_def = less_prod_def 
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

126 
lemmas prod_less_eq = less_prod_def' 
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

127 

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

128 
end 
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
47961
diff
changeset

129 