src/HOL/Library/Product_Order.thy
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 63972 c98d1dd7eba1
child 67091 1393c2340eec
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
63972
c98d1dd7eba1 Library: fix name Product_plus to Product_Plus
hoelzl
parents: 63561
diff changeset
     8
imports Product_Plus
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
    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
   183
db890d9fc5c2 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents: 52729
diff changeset
   184
instance prod :: (complete_lattice, complete_lattice) complete_lattice
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
   185
  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
   186
    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
   187
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   188
lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   189
  unfolding Sup_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   190
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   191
lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   192
  unfolding Sup_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   193
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   194
lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   195
  unfolding Inf_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   196
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   197
lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   198
  unfolding Inf_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   199
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   200
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
   201
  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
   202
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   203
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
   204
  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
   205
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   206
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
   207
  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
   208
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   209
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
   210
  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
   211
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   212
lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 62053
diff changeset
   213
  unfolding Sup_prod_def by (simp add: comp_def)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   214
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   215
lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 62053
diff changeset
   216
  unfolding Inf_prod_def by (simp add: comp_def)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   217
50535
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   218
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   219
text \<open>Alternative formulations for set infima and suprema over the product
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   220
of two complete lattices:\<close>
50535
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   221
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 56166
diff changeset
   222
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
   223
  "INFIMUM A f = (INFIMUM A (fst o f), INFIMUM A (snd o f))"
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 62053
diff changeset
   224
  unfolding Inf_prod_def by simp
50535
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   225
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 56166
diff changeset
   226
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
   227
  "SUPREMUM A f = (SUPREMUM A (fst o f), SUPREMUM A (snd o f))"
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 62053
diff changeset
   228
  unfolding Sup_prod_def by simp
50535
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   229
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   230
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   231
subsection \<open>Complete distributive lattices\<close>
50535
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   232
50573
765c22baa1c9 new contributor
nipkow
parents: 50535
diff changeset
   233
(* Contribution: Alessandro Coglio *)
50535
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   234
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60580
diff changeset
   235
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
   236
proof (standard, goal_cases)
60580
7e741e22d7fc tuned proofs;
wenzelm
parents: 60500
diff changeset
   237
  case 1
7e741e22d7fc tuned proofs;
wenzelm
parents: 60500
diff changeset
   238
  then show ?case
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 56166
diff changeset
   239
    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
   240
next
60580
7e741e22d7fc tuned proofs;
wenzelm
parents: 60500
diff changeset
   241
  case 2
7e741e22d7fc tuned proofs;
wenzelm
parents: 60500
diff changeset
   242
  then show ?case
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 56166
diff changeset
   243
    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
   244
qed
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   245
63561
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   246
subsection \<open>Bekic's Theorem\<close>
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   247
text \<open>
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   248
  Simultaneous fixed points over pairs can be written in terms of separate fixed points.
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   249
  Transliterated from HOLCF.Fix by Peter Gammie
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   250
\<close>
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   251
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   252
lemma lfp_prod:
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   253
  fixes F :: "'a::complete_lattice \<times> 'b::complete_lattice \<Rightarrow> 'a \<times> 'b"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   254
  assumes "mono F"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   255
  shows "lfp F = (lfp (\<lambda>x. fst (F (x, lfp (\<lambda>y. snd (F (x, y)))))),
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   256
                 (lfp (\<lambda>y. snd (F (lfp (\<lambda>x. fst (F (x, lfp (\<lambda>y. snd (F (x, y)))))), y)))))"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   257
  (is "lfp F = (?x, ?y)")
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   258
proof(rule lfp_eqI[OF assms])
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   259
  have 1: "fst (F (?x, ?y)) = ?x"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   260
    by (rule trans [symmetric, OF lfp_unfold])
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   261
       (blast intro!: monoI monoD[OF assms(1)] fst_mono snd_mono Pair_mono lfp_mono)+
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   262
  have 2: "snd (F (?x, ?y)) = ?y"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   263
    by (rule trans [symmetric, OF lfp_unfold])
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   264
       (blast intro!: monoI monoD[OF assms(1)] fst_mono snd_mono Pair_mono lfp_mono)+
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   265
  from 1 2 show "F (?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff)
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   266
next
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   267
  fix z assume F_z: "F z = z"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   268
  obtain x y where z: "z = (x, y)" by (rule prod.exhaust)
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   269
  from F_z z have F_x: "fst (F (x, y)) = x" by simp
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   270
  from F_z z have F_y: "snd (F (x, y)) = y" by simp
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   271
  let ?y1 = "lfp (\<lambda>y. snd (F (x, y)))"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   272
  have "?y1 \<le> y" by (rule lfp_lowerbound, simp add: F_y)
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   273
  hence "fst (F (x, ?y1)) \<le> fst (F (x, y))"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   274
    by (simp add: assms fst_mono monoD)
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   275
  hence "fst (F (x, ?y1)) \<le> x" using F_x by simp
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   276
  hence 1: "?x \<le> x" by (simp add: lfp_lowerbound)
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   277
  hence "snd (F (?x, y)) \<le> snd (F (x, y))"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   278
    by (simp add: assms snd_mono monoD)
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   279
  hence "snd (F (?x, y)) \<le> y" using F_y by simp
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   280
  hence 2: "?y \<le> y" by (simp add: lfp_lowerbound)
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   281
  show "(?x, ?y) \<le> z" using z 1 2 by simp
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   282
qed
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   283
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   284
lemma gfp_prod:
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   285
  fixes F :: "'a::complete_lattice \<times> 'b::complete_lattice \<Rightarrow> 'a \<times> 'b"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   286
  assumes "mono F"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   287
  shows "gfp F = (gfp (\<lambda>x. fst (F (x, gfp (\<lambda>y. snd (F (x, y)))))),
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   288
                 (gfp (\<lambda>y. snd (F (gfp (\<lambda>x. fst (F (x, gfp (\<lambda>y. snd (F (x, y)))))), y)))))"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   289
  (is "gfp F = (?x, ?y)")
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   290
proof(rule gfp_eqI[OF assms])
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   291
  have 1: "fst (F (?x, ?y)) = ?x"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   292
    by (rule trans [symmetric, OF gfp_unfold])
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   293
       (blast intro!: monoI monoD[OF assms(1)] fst_mono snd_mono Pair_mono gfp_mono)+
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   294
  have 2: "snd (F (?x, ?y)) = ?y"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   295
    by (rule trans [symmetric, OF gfp_unfold])
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   296
       (blast intro!: monoI monoD[OF assms(1)] fst_mono snd_mono Pair_mono gfp_mono)+
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   297
  from 1 2 show "F (?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff)
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   298
next
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   299
  fix z assume F_z: "F z = z"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   300
  obtain x y where z: "z = (x, y)" by (rule prod.exhaust)
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   301
  from F_z z have F_x: "fst (F (x, y)) = x" by simp
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   302
  from F_z z have F_y: "snd (F (x, y)) = y" by simp
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   303
  let ?y1 = "gfp (\<lambda>y. snd (F (x, y)))"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   304
  have "y \<le> ?y1" by (rule gfp_upperbound, simp add: F_y)
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   305
  hence "fst (F (x, y)) \<le> fst (F (x, ?y1))"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   306
    by (simp add: assms fst_mono monoD)
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   307
  hence "x \<le> fst (F (x, ?y1))" using F_x by simp
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   308
  hence 1: "x \<le> ?x" by (simp add: gfp_upperbound)
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   309
  hence "snd (F (x, y)) \<le> snd (F (?x, y))"
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   310
    by (simp add: assms snd_mono monoD)
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   311
  hence "y \<le> snd (F (?x, y))" using F_y by simp
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   312
  hence 2: "y \<le> ?y" by (simp add: gfp_upperbound)
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   313
  show "z \<le> (?x, ?y)" using z 1 2 by simp
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   314
qed
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 62343
diff changeset
   315
51115
7dbd6832a689 consolidation of library theories on product orders
haftmann
parents: 50573
diff changeset
   316
end