src/HOL/Library/Product_Lattice.thy
author Christian Sternagel
Wed Aug 29 12:23:14 2012 +0900 (2012-08-29)
changeset 49083 01081bca31b6
parent 45007 cc86edb97c2c
child 50535 2464d77527c4
permissions -rw-r--r--
dropped ord and bot instance for list prefixes (use locale interpretation instead, which allows users to decide what order to use on lists)
wenzelm@45007
     1
(*  Title:      HOL/Library/Product_Lattice.thy
huffman@44006
     2
    Author:     Brian Huffman
huffman@44006
     3
*)
huffman@44006
     4
huffman@44006
     5
header {* Lattice operations on product types *}
huffman@44006
     6
huffman@44006
     7
theory Product_Lattice
huffman@44006
     8
imports "~~/src/HOL/Library/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
huffman@44006
   111
lemma fst_top [simp]: "fst top = top"
huffman@44006
   112
  unfolding top_prod_def by simp
huffman@44006
   113
huffman@44006
   114
lemma snd_top [simp]: "snd top = top"
huffman@44006
   115
  unfolding top_prod_def by simp
huffman@44006
   116
huffman@44006
   117
lemma Pair_top_top: "(top, top) = top"
huffman@44006
   118
  unfolding top_prod_def by simp
huffman@44006
   119
huffman@44006
   120
instance
huffman@44006
   121
  by default (auto simp add: top_prod_def)
huffman@44006
   122
huffman@44006
   123
end
huffman@44006
   124
huffman@44006
   125
instantiation prod :: (bot, bot) bot
huffman@44006
   126
begin
huffman@44006
   127
huffman@44006
   128
definition
huffman@44006
   129
  "bot = (bot, bot)"
huffman@44006
   130
huffman@44006
   131
lemma fst_bot [simp]: "fst bot = bot"
huffman@44006
   132
  unfolding bot_prod_def by simp
huffman@44006
   133
huffman@44006
   134
lemma snd_bot [simp]: "snd bot = bot"
huffman@44006
   135
  unfolding bot_prod_def by simp
huffman@44006
   136
huffman@44006
   137
lemma Pair_bot_bot: "(bot, bot) = bot"
huffman@44006
   138
  unfolding bot_prod_def by simp
huffman@44006
   139
huffman@44006
   140
instance
huffman@44006
   141
  by default (auto simp add: bot_prod_def)
huffman@44006
   142
huffman@44006
   143
end
huffman@44006
   144
huffman@44006
   145
instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
huffman@44006
   146
huffman@44006
   147
instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
huffman@44006
   148
  by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
huffman@44006
   149
huffman@44006
   150
huffman@44006
   151
subsection {* Complete lattice operations *}
huffman@44006
   152
huffman@44006
   153
instantiation prod :: (complete_lattice, complete_lattice) complete_lattice
huffman@44006
   154
begin
huffman@44006
   155
huffman@44006
   156
definition
huffman@44006
   157
  "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
huffman@44006
   158
huffman@44006
   159
definition
huffman@44006
   160
  "Inf A = (INF x:A. fst x, INF x:A. snd x)"
huffman@44006
   161
huffman@44006
   162
instance
huffman@44006
   163
  by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
hoelzl@44928
   164
    INF_lower SUP_upper le_INF_iff SUP_le_iff)
huffman@44006
   165
huffman@44006
   166
end
huffman@44006
   167
huffman@44006
   168
lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
huffman@44006
   169
  unfolding Sup_prod_def by simp
huffman@44006
   170
huffman@44006
   171
lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"
huffman@44006
   172
  unfolding Sup_prod_def by simp
huffman@44006
   173
huffman@44006
   174
lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"
huffman@44006
   175
  unfolding Inf_prod_def by simp
huffman@44006
   176
huffman@44006
   177
lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"
huffman@44006
   178
  unfolding Inf_prod_def by simp
huffman@44006
   179
huffman@44006
   180
lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
hoelzl@44928
   181
  by (simp add: SUP_def fst_Sup image_image)
huffman@44006
   182
huffman@44006
   183
lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
hoelzl@44928
   184
  by (simp add: SUP_def snd_Sup image_image)
huffman@44006
   185
huffman@44006
   186
lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
hoelzl@44928
   187
  by (simp add: INF_def fst_Inf image_image)
huffman@44006
   188
huffman@44006
   189
lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
hoelzl@44928
   190
  by (simp add: INF_def snd_Inf image_image)
huffman@44006
   191
huffman@44006
   192
lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
hoelzl@44928
   193
  by (simp add: SUP_def Sup_prod_def image_image)
huffman@44006
   194
huffman@44006
   195
lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
hoelzl@44928
   196
  by (simp add: INF_def Inf_prod_def image_image)
huffman@44006
   197
huffman@44006
   198
end