src/HOL/Library/Product_Order.thy
author haftmann
Fri Nov 01 18:51:14 2013 +0100 (2013-11-01)
changeset 54230 b1d955791529
parent 52729 412c9e0381a1
child 54776 db890d9fc5c2
permissions -rw-r--r--
more simplification rules on unary and binary minus
haftmann@51115
     1
(*  Title:      HOL/Library/Product_Order.thy
huffman@44006
     2
    Author:     Brian Huffman
huffman@44006
     3
*)
huffman@44006
     4
haftmann@51115
     5
header {* Pointwise order on product types *}
huffman@44006
     6
haftmann@51115
     7
theory Product_Order
wenzelm@51542
     8
imports Product_plus
huffman@44006
     9
begin
huffman@44006
    10
huffman@44006
    11
subsection {* Pointwise ordering *}
huffman@44006
    12
huffman@44006
    13
instantiation prod :: (ord, ord) ord
huffman@44006
    14
begin
huffman@44006
    15
huffman@44006
    16
definition
huffman@44006
    17
  "x \<le> y \<longleftrightarrow> fst x \<le> fst y \<and> snd x \<le> snd y"
huffman@44006
    18
huffman@44006
    19
definition
huffman@44006
    20
  "(x::'a \<times> 'b) < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
huffman@44006
    21
huffman@44006
    22
instance ..
huffman@44006
    23
huffman@44006
    24
end
huffman@44006
    25
huffman@44006
    26
lemma fst_mono: "x \<le> y \<Longrightarrow> fst x \<le> fst y"
huffman@44006
    27
  unfolding less_eq_prod_def by simp
huffman@44006
    28
huffman@44006
    29
lemma snd_mono: "x \<le> y \<Longrightarrow> snd x \<le> snd y"
huffman@44006
    30
  unfolding less_eq_prod_def by simp
huffman@44006
    31
huffman@44006
    32
lemma Pair_mono: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> (x, y) \<le> (x', y')"
huffman@44006
    33
  unfolding less_eq_prod_def by simp
huffman@44006
    34
huffman@44006
    35
lemma Pair_le [simp]: "(a, b) \<le> (c, d) \<longleftrightarrow> a \<le> c \<and> b \<le> d"
huffman@44006
    36
  unfolding less_eq_prod_def by simp
huffman@44006
    37
huffman@44006
    38
instance prod :: (preorder, preorder) preorder
huffman@44006
    39
proof
huffman@44006
    40
  fix x y z :: "'a \<times> 'b"
huffman@44006
    41
  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
huffman@44006
    42
    by (rule less_prod_def)
huffman@44006
    43
  show "x \<le> x"
huffman@44006
    44
    unfolding less_eq_prod_def
huffman@44006
    45
    by fast
huffman@44006
    46
  assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
huffman@44006
    47
    unfolding less_eq_prod_def
huffman@44006
    48
    by (fast elim: order_trans)
huffman@44006
    49
qed
huffman@44006
    50
huffman@44006
    51
instance prod :: (order, order) order
huffman@44006
    52
  by default auto
huffman@44006
    53
huffman@44006
    54
huffman@44006
    55
subsection {* Binary infimum and supremum *}
huffman@44006
    56
huffman@44006
    57
instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf
huffman@44006
    58
begin
huffman@44006
    59
huffman@44006
    60
definition
huffman@44006
    61
  "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
huffman@44006
    62
huffman@44006
    63
lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)"
huffman@44006
    64
  unfolding inf_prod_def by simp
huffman@44006
    65
huffman@44006
    66
lemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)"
huffman@44006
    67
  unfolding inf_prod_def by simp
huffman@44006
    68
huffman@44006
    69
lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
huffman@44006
    70
  unfolding inf_prod_def by simp
huffman@44006
    71
huffman@44006
    72
instance
huffman@44006
    73
  by default auto
huffman@44006
    74
huffman@44006
    75
end
huffman@44006
    76
huffman@44006
    77
instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup
huffman@44006
    78
begin
huffman@44006
    79
huffman@44006
    80
definition
huffman@44006
    81
  "sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))"
huffman@44006
    82
huffman@44006
    83
lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)"
huffman@44006
    84
  unfolding sup_prod_def by simp
huffman@44006
    85
huffman@44006
    86
lemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)"
huffman@44006
    87
  unfolding sup_prod_def by simp
huffman@44006
    88
huffman@44006
    89
lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
huffman@44006
    90
  unfolding sup_prod_def by simp
huffman@44006
    91
huffman@44006
    92
instance
huffman@44006
    93
  by default auto
huffman@44006
    94
huffman@44006
    95
end
huffman@44006
    96
huffman@44006
    97
instance prod :: (lattice, lattice) lattice ..
huffman@44006
    98
huffman@44006
    99
instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
huffman@44006
   100
  by default (auto simp add: sup_inf_distrib1)
huffman@44006
   101
huffman@44006
   102
huffman@44006
   103
subsection {* Top and bottom elements *}
huffman@44006
   104
huffman@44006
   105
instantiation prod :: (top, top) top
huffman@44006
   106
begin
huffman@44006
   107
huffman@44006
   108
definition
huffman@44006
   109
  "top = (top, top)"
huffman@44006
   110
haftmann@52729
   111
instance ..
haftmann@52729
   112
haftmann@52729
   113
end
haftmann@52729
   114
huffman@44006
   115
lemma fst_top [simp]: "fst top = top"
huffman@44006
   116
  unfolding top_prod_def by simp
huffman@44006
   117
huffman@44006
   118
lemma snd_top [simp]: "snd top = top"
huffman@44006
   119
  unfolding top_prod_def by simp
huffman@44006
   120
huffman@44006
   121
lemma Pair_top_top: "(top, top) = top"
huffman@44006
   122
  unfolding top_prod_def by simp
huffman@44006
   123
haftmann@52729
   124
instance prod :: (order_top, order_top) order_top
huffman@44006
   125
  by default (auto simp add: top_prod_def)
huffman@44006
   126
huffman@44006
   127
instantiation prod :: (bot, bot) bot
huffman@44006
   128
begin
huffman@44006
   129
huffman@44006
   130
definition
huffman@44006
   131
  "bot = (bot, bot)"
huffman@44006
   132
haftmann@52729
   133
instance ..
haftmann@52729
   134
haftmann@52729
   135
end
haftmann@52729
   136
huffman@44006
   137
lemma fst_bot [simp]: "fst bot = bot"
huffman@44006
   138
  unfolding bot_prod_def by simp
huffman@44006
   139
huffman@44006
   140
lemma snd_bot [simp]: "snd bot = bot"
huffman@44006
   141
  unfolding bot_prod_def by simp
huffman@44006
   142
huffman@44006
   143
lemma Pair_bot_bot: "(bot, bot) = bot"
huffman@44006
   144
  unfolding bot_prod_def by simp
huffman@44006
   145
haftmann@52729
   146
instance prod :: (order_bot, order_bot) order_bot
huffman@44006
   147
  by default (auto simp add: bot_prod_def)
huffman@44006
   148
huffman@44006
   149
instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
huffman@44006
   150
huffman@44006
   151
instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
huffman@44006
   152
  by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
huffman@44006
   153
huffman@44006
   154
huffman@44006
   155
subsection {* Complete lattice operations *}
huffman@44006
   156
huffman@44006
   157
instantiation prod :: (complete_lattice, complete_lattice) complete_lattice
huffman@44006
   158
begin
huffman@44006
   159
huffman@44006
   160
definition
huffman@44006
   161
  "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
huffman@44006
   162
huffman@44006
   163
definition
huffman@44006
   164
  "Inf A = (INF x:A. fst x, INF x:A. snd x)"
huffman@44006
   165
huffman@44006
   166
instance
huffman@44006
   167
  by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
haftmann@52729
   168
    INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
huffman@44006
   169
huffman@44006
   170
end
huffman@44006
   171
huffman@44006
   172
lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
huffman@44006
   173
  unfolding Sup_prod_def by simp
huffman@44006
   174
huffman@44006
   175
lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"
huffman@44006
   176
  unfolding Sup_prod_def by simp
huffman@44006
   177
huffman@44006
   178
lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"
huffman@44006
   179
  unfolding Inf_prod_def by simp
huffman@44006
   180
huffman@44006
   181
lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"
huffman@44006
   182
  unfolding Inf_prod_def by simp
huffman@44006
   183
huffman@44006
   184
lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
hoelzl@44928
   185
  by (simp add: SUP_def fst_Sup image_image)
huffman@44006
   186
huffman@44006
   187
lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
hoelzl@44928
   188
  by (simp add: SUP_def snd_Sup image_image)
huffman@44006
   189
huffman@44006
   190
lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
hoelzl@44928
   191
  by (simp add: INF_def fst_Inf image_image)
huffman@44006
   192
huffman@44006
   193
lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
hoelzl@44928
   194
  by (simp add: INF_def snd_Inf image_image)
huffman@44006
   195
huffman@44006
   196
lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
hoelzl@44928
   197
  by (simp add: SUP_def Sup_prod_def image_image)
huffman@44006
   198
huffman@44006
   199
lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
hoelzl@44928
   200
  by (simp add: INF_def Inf_prod_def image_image)
huffman@44006
   201
nipkow@50535
   202
nipkow@50535
   203
text {* Alternative formulations for set infima and suprema over the product
nipkow@50535
   204
of two complete lattices: *}
nipkow@50535
   205
nipkow@50535
   206
lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))"
nipkow@50535
   207
by (auto simp: Inf_prod_def INF_def)
nipkow@50535
   208
nipkow@50535
   209
lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))"
nipkow@50535
   210
by (auto simp: Sup_prod_def SUP_def)
nipkow@50535
   211
nipkow@50535
   212
lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
nipkow@50535
   213
by (auto simp: INF_def Inf_prod_def image_compose)
nipkow@50535
   214
nipkow@50535
   215
lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
nipkow@50535
   216
by (auto simp: SUP_def Sup_prod_def image_compose)
nipkow@50535
   217
nipkow@50535
   218
lemma INF_prod_alt_def:
nipkow@50535
   219
  "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
nipkow@50535
   220
by (metis fst_INF snd_INF surjective_pairing)
nipkow@50535
   221
nipkow@50535
   222
lemma SUP_prod_alt_def:
nipkow@50535
   223
  "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))"
nipkow@50535
   224
by (metis fst_SUP snd_SUP surjective_pairing)
nipkow@50535
   225
nipkow@50535
   226
nipkow@50535
   227
subsection {* Complete distributive lattices *}
nipkow@50535
   228
nipkow@50573
   229
(* Contribution: Alessandro Coglio *)
nipkow@50535
   230
nipkow@50535
   231
instance prod ::
nipkow@50535
   232
  (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
nipkow@50535
   233
proof
nipkow@50535
   234
  case goal1 thus ?case
nipkow@50535
   235
    by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF)
nipkow@50535
   236
next
nipkow@50535
   237
  case goal2 thus ?case
nipkow@50535
   238
    by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP)
nipkow@50535
   239
qed
nipkow@50535
   240
haftmann@51115
   241
end
nipkow@50535
   242