author | hoelzl |
Wed, 21 Nov 2012 15:47:55 +0100 | |
changeset 50148 | b8cff6a8fda2 |
parent 47961 | e0a85be4fca0 |
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 |
||
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 |
37765 | 15 |
prod_le_def: "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 |
37765 | 18 |
prod_less_def: "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]: |
47961 | 25 |
"(x1::'a::{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2" |
26 |
"(x1::'a::{ord, equal}, 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 |
|
47961 | 29 |
instance prod :: (preorder, preorder) preorder |
30 |
by default (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans) |
|
15737 | 31 |
|
47961 | 32 |
instance prod :: (order, order) order |
33 |
by default (auto simp add: prod_le_def) |
|
31040 | 34 |
|
47961 | 35 |
instance prod :: (linorder, linorder) linorder |
36 |
by default (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 |
47961 | 42 |
inf_prod_def: "(inf :: '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 |
47961 | 45 |
sup_prod_def: "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max" |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
46 |
|
47961 | 47 |
instance |
48 |
by default (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1) |
|
31040 | 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 |
||
47961 | 58 |
instance |
59 |
by default (auto simp add: bot_prod_def prod_le_def) |
|
31040 | 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 |
||
47961 | 69 |
instance |
70 |
by default (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 |
|
44063
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset
|
74 |
text {* A stronger version of the definition holds for partial orders. *} |
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset
|
75 |
|
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset
|
76 |
lemma prod_less_eq: |
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset
|
77 |
fixes x y :: "'a::order \<times> 'b::ord" |
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset
|
78 |
shows "x < y \<longleftrightarrow> fst x < fst y \<or> (fst x = fst y \<and> snd x < snd y)" |
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset
|
79 |
unfolding prod_less_def fst_conv snd_conv le_less by auto |
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset
|
80 |
|
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset
|
81 |
instance prod :: (wellorder, wellorder) wellorder |
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset
|
82 |
proof |
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset
|
83 |
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
|
84 |
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
|
85 |
show "P z" |
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset
|
86 |
proof (induct z) |
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset
|
87 |
case (Pair a b) |
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset
|
88 |
show "P (a, b)" |
47961 | 89 |
proof (induct a arbitrary: b rule: less_induct) |
90 |
case (less a\<^isub>1) note a\<^isub>1 = this |
|
91 |
show "P (a\<^isub>1, b)" |
|
92 |
proof (induct b rule: less_induct) |
|
93 |
case (less b\<^isub>1) note b\<^isub>1 = this |
|
94 |
show "P (a\<^isub>1, b\<^isub>1)" |
|
95 |
proof (rule P) |
|
96 |
fix p assume p: "p < (a\<^isub>1, b\<^isub>1)" |
|
97 |
show "P p" |
|
98 |
proof (cases "fst p < a\<^isub>1") |
|
99 |
case True |
|
100 |
then have "P (fst p, snd p)" by (rule a\<^isub>1) |
|
101 |
then show ?thesis by simp |
|
102 |
next |
|
103 |
case False |
|
104 |
with p have 1: "a\<^isub>1 = fst p" and 2: "snd p < b\<^isub>1" |
|
105 |
by (simp_all add: prod_less_eq) |
|
106 |
from 2 have "P (a\<^isub>1, snd p)" by (rule b\<^isub>1) |
|
107 |
with 1 show ?thesis by simp |
|
108 |
qed |
|
109 |
qed |
|
110 |
qed |
|
111 |
qed |
|
44063
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset
|
112 |
qed |
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset
|
113 |
qed |
4588597ba37e
Library/Product_ord: wellorder instance for products
huffman
parents:
38857
diff
changeset
|
114 |
|
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
115 |
end |