src/HOL/Library/Product_Order.thy
author wenzelm
Mon, 04 Jan 2016 21:49:06 +0100
changeset 62053 1c8252d07e32
parent 61166 5976fe402824
child 62343 24106dc44def
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
51115
7dbd6832a689 consolidation of library theories on product orders
haftmann
parents: 50573
diff changeset
     1
(*  Title:      HOL/Library/Product_Order.thy
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
     3
*)
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
     4
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
     5
section \<open>Pointwise order on product types\<close>
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
     6
51115
7dbd6832a689 consolidation of library theories on product orders
haftmann
parents: 50573
diff changeset
     7
theory Product_Order
54776
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
     8
imports Product_plus Conditionally_Complete_Lattices
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
     9
begin
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    10
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    11
subsection \<open>Pointwise ordering\<close>
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    12
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    13
instantiation prod :: (ord, ord) ord
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    14
begin
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    15
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    16
definition
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    17
  "x \<le> y \<longleftrightarrow> fst x \<le> fst y \<and> snd x \<le> snd y"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    18
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    19
definition
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    20
  "(x::'a \<times> 'b) < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    21
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    22
instance ..
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    23
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    24
end
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    25
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    26
lemma fst_mono: "x \<le> y \<Longrightarrow> fst x \<le> fst y"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    27
  unfolding less_eq_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    28
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    29
lemma snd_mono: "x \<le> y \<Longrightarrow> snd x \<le> snd y"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    30
  unfolding less_eq_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    31
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    32
lemma Pair_mono: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> (x, y) \<le> (x', y')"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    33
  unfolding less_eq_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    34
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    35
lemma Pair_le [simp]: "(a, b) \<le> (c, d) \<longleftrightarrow> a \<le> c \<and> b \<le> d"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    36
  unfolding less_eq_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    37
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    38
instance prod :: (preorder, preorder) preorder
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    39
proof
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    40
  fix x y z :: "'a \<times> 'b"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    41
  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    42
    by (rule less_prod_def)
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    43
  show "x \<le> x"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    44
    unfolding less_eq_prod_def
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    45
    by fast
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    46
  assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    47
    unfolding less_eq_prod_def
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    48
    by (fast elim: order_trans)
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    49
qed
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    50
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    51
instance prod :: (order, order) order
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
    52
  by standard auto
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    53
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    54
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    55
subsection \<open>Binary infimum and supremum\<close>
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    56
54776
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
    57
instantiation prod :: (inf, inf) inf
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    58
begin
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    59
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
    60
definition "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    61
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    62
lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    63
  unfolding inf_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    64
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    65
lemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    66
  unfolding inf_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    67
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    68
lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    69
  unfolding inf_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    70
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
    71
instance ..
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
    72
54776
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
    73
end
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
    74
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
    75
instance prod :: (semilattice_inf, semilattice_inf) semilattice_inf
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
    76
  by standard auto
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    77
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    78
54776
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
    79
instantiation prod :: (sup, sup) sup
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    80
begin
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    81
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    82
definition
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    83
  "sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    84
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    85
lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    86
  unfolding sup_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    87
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    88
lemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    89
  unfolding sup_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    90
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    91
lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    92
  unfolding sup_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    93
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
    94
instance ..
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
    95
54776
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
    96
end
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
    97
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
    98
instance prod :: (semilattice_sup, semilattice_sup) semilattice_sup
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
    99
  by standard auto
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   100
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   101
instance prod :: (lattice, lattice) lattice ..
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   102
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   103
instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
   104
  by standard (auto simp add: sup_inf_distrib1)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   105
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   106
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   107
subsection \<open>Top and bottom elements\<close>
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   108
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   109
instantiation prod :: (top, top) top
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   110
begin
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   111
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   112
definition
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   113
  "top = (top, top)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   114
52729
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 51542
diff changeset
   115
instance ..
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 51542
diff changeset
   116
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 51542
diff changeset
   117
end
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 51542
diff changeset
   118
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   119
lemma fst_top [simp]: "fst top = top"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   120
  unfolding top_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   121
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   122
lemma snd_top [simp]: "snd top = top"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   123
  unfolding top_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   124
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   125
lemma Pair_top_top: "(top, top) = top"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   126
  unfolding top_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   127
52729
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 51542
diff changeset
   128
instance prod :: (order_top, order_top) order_top
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
   129
  by standard (auto simp add: top_prod_def)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   130
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   131
instantiation prod :: (bot, bot) bot
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   132
begin
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   133
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   134
definition
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   135
  "bot = (bot, bot)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   136
52729
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 51542
diff changeset
   137
instance ..
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 51542
diff changeset
   138
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 51542
diff changeset
   139
end
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 51542
diff changeset
   140
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   141
lemma fst_bot [simp]: "fst bot = bot"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   142
  unfolding bot_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   143
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   144
lemma snd_bot [simp]: "snd bot = bot"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   145
  unfolding bot_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   146
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   147
lemma Pair_bot_bot: "(bot, bot) = bot"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   148
  unfolding bot_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   149
52729
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 51542
diff changeset
   150
instance prod :: (order_bot, order_bot) order_bot
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
   151
  by standard (auto simp add: bot_prod_def)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   152
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   153
instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   154
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   155
instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
62053
1c8252d07e32 tuned proofs;
wenzelm
parents: 61166
diff changeset
   156
  by standard (auto simp add: prod_eqI diff_eq)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   157
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   158
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   159
subsection \<open>Complete lattice operations\<close>
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   160
54776
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
   161
instantiation prod :: (Inf, Inf) Inf
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
   162
begin
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
   163
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
   164
definition "Inf A = (INF x:A. fst x, INF x:A. snd x)"
54776
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
   165
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
   166
instance ..
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
   167
54776
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
   168
end
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
   169
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
   170
instantiation prod :: (Sup, Sup) Sup
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   171
begin
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   172
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
   173
definition "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   174
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
   175
instance ..
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
   176
54776
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
   177
end
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   178
54776
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
   179
instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
   180
    conditionally_complete_lattice
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
   181
  by standard (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
62053
1c8252d07e32 tuned proofs;
wenzelm
parents: 61166
diff changeset
   182
    INF_def SUP_def simp del: Inf_image_eq Sup_image_eq
1c8252d07e32 tuned proofs;
wenzelm
parents: 61166
diff changeset
   183
    intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
54776
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
   184
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
   185
instance prod :: (complete_lattice, complete_lattice) complete_lattice
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
   186
  by standard (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
52729
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 51542
diff changeset
   187
    INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   188
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   189
lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   190
  unfolding Sup_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   191
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   192
lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   193
  unfolding Sup_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   194
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   195
lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   196
  unfolding Inf_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   197
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   198
lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   199
  unfolding Inf_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   200
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   201
lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 56154
diff changeset
   202
  using fst_Sup [of "f ` A", symmetric] by (simp add: comp_def)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   203
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   204
lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 56154
diff changeset
   205
  using snd_Sup [of "f ` A", symmetric] by (simp add: comp_def)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   206
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   207
lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 56154
diff changeset
   208
  using fst_Inf [of "f ` A", symmetric] by (simp add: comp_def)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   209
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   210
lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 56154
diff changeset
   211
  using snd_Inf [of "f ` A", symmetric] by (simp add: comp_def)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   212
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   213
lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 56154
diff changeset
   214
  unfolding SUP_def Sup_prod_def by (simp add: comp_def)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   215
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   216
lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 56154
diff changeset
   217
  unfolding INF_def Inf_prod_def by (simp add: comp_def)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   218
50535
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   219
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   220
text \<open>Alternative formulations for set infima and suprema over the product
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   221
of two complete lattices:\<close>
50535
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   222
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 56166
diff changeset
   223
lemma INF_prod_alt_def:
56218
1c3f1f2431f9 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents: 56212
diff changeset
   224
  "INFIMUM A f = (INFIMUM A (fst o f), INFIMUM A (snd o f))"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 56154
diff changeset
   225
  unfolding INF_def Inf_prod_def by simp
50535
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   226
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 56166
diff changeset
   227
lemma SUP_prod_alt_def:
56218
1c3f1f2431f9 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents: 56212
diff changeset
   228
  "SUPREMUM A f = (SUPREMUM A (fst o f), SUPREMUM A (snd o f))"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 56154
diff changeset
   229
  unfolding SUP_def Sup_prod_def by simp
50535
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   230
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   231
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   232
subsection \<open>Complete distributive lattices\<close>
50535
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   233
50573
765c22baa1c9 new contributor
nipkow
parents: 50535
diff changeset
   234
(* Contribution: Alessandro Coglio *)
50535
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   235
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
   236
instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
61166
5976fe402824 renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents: 60679
diff changeset
   237
proof (standard, goal_cases)
60580
7e741e22d7fc tuned proofs;
wenzelm
parents: 60500
diff changeset
   238
  case 1
7e741e22d7fc tuned proofs;
wenzelm
parents: 60500
diff changeset
   239
  then show ?case
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 56166
diff changeset
   240
    by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)
50535
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   241
next
60580
7e741e22d7fc tuned proofs;
wenzelm
parents: 60500
diff changeset
   242
  case 2
7e741e22d7fc tuned proofs;
wenzelm
parents: 60500
diff changeset
   243
  then show ?case
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 56166
diff changeset
   244
    by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP comp_def)
50535
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   245
qed
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   246
51115
7dbd6832a689 consolidation of library theories on product orders
haftmann
parents: 50573
diff changeset
   247
end
50535
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   248