author  haftmann 
Thu, 14 Feb 2013 14:14:55 +0100  
changeset 51115  7dbd6832a689 
parent 47961  src/HOL/Library/Product_ord.thy@e0a85be4fca0 
child 52729  412c9e0381a1 
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 

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

69 
by default (auto simp add: bot_prod_def) 
31040  70 

71 
end 

72 

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

73 
instantiation prod :: (top, top) top 
31040  74 
begin 
75 

76 
definition 

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

77 
"top = (top, top)" 
31040  78 

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

80 
by default (auto simp add: top_prod_def) 
22483  81 

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

83 

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

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

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

86 
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

87 
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

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

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

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

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

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

95 
proof (induct b rule: less_induct) 

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

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

98 
proof (rule P) 

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

100 
show "P p" 

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

102 
case True 

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

104 
then show ?thesis by simp 

105 
next 

106 
case False 

107 
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

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

111 
qed 

112 
qed 

113 
qed 

114 
qed 

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

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

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

117 

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

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

119 

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

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

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

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

123 

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

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

125 