src/HOL/Library/Product_Lattice.thy
author nipkow
Fri, 14 Dec 2012 18:41:45 +0100
changeset 50535 2464d77527c4
parent 45007 cc86edb97c2c
child 50573 765c22baa1c9
permissions -rw-r--r--
contribution by A. Colgio
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45007
cc86edb97c2c fixed headers;
wenzelm
parents: 44928
diff changeset
     1
(*  Title:      HOL/Library/Product_Lattice.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
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
     5
header {* Lattice operations on product types *}
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
     6
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
     7
theory Product_Lattice
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
     8
imports "~~/src/HOL/Library/Product_plus"
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
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    11
subsection {* Pointwise ordering *}
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
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    52
  by default auto
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
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    55
subsection {* Binary infimum and supremum *}
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    56
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    57
instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf
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
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    60
definition
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    61
  "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    62
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    63
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
    64
  unfolding inf_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    65
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    66
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
    67
  unfolding inf_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    68
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    69
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
    70
  unfolding inf_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    71
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    72
instance
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    73
  by default auto
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    74
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    75
end
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    76
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    77
instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    78
begin
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    79
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    80
definition
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    81
  "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
    82
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    83
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
    84
  unfolding sup_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    85
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    86
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
    87
  unfolding sup_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    88
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    89
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
    90
  unfolding sup_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    91
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    92
instance
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    93
  by default auto
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    94
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    95
end
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    96
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    97
instance prod :: (lattice, lattice) lattice ..
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    98
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
    99
instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   100
  by default (auto simp add: sup_inf_distrib1)
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   101
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
subsection {* Top and bottom elements *}
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   104
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   105
instantiation prod :: (top, top) top
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   106
begin
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   107
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   108
definition
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   109
  "top = (top, top)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   110
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   111
lemma fst_top [simp]: "fst top = top"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   112
  unfolding top_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   113
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   114
lemma snd_top [simp]: "snd top = top"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   115
  unfolding top_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   116
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   117
lemma Pair_top_top: "(top, top) = top"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   118
  unfolding top_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   119
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   120
instance
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   121
  by default (auto simp add: top_prod_def)
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   122
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   123
end
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
instantiation prod :: (bot, bot) bot
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   126
begin
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   127
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   128
definition
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   129
  "bot = (bot, bot)"
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
lemma fst_bot [simp]: "fst bot = bot"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   132
  unfolding bot_prod_def by simp
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
lemma snd_bot [simp]: "snd bot = bot"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   135
  unfolding bot_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   136
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   137
lemma Pair_bot_bot: "(bot, bot) = bot"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   138
  unfolding bot_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   139
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   140
instance
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   141
  by default (auto simp add: bot_prod_def)
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   142
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   143
end
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   144
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   145
instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
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
instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   148
  by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   149
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   150
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   151
subsection {* Complete lattice operations *}
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
instantiation prod :: (complete_lattice, complete_lattice) complete_lattice
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   154
begin
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   155
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   156
definition
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   157
  "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   158
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   159
definition
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   160
  "Inf A = (INF x:A. fst x, INF x:A. snd x)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   161
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   162
instance
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   163
  by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44006
diff changeset
   164
    INF_lower SUP_upper le_INF_iff SUP_le_iff)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   165
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   166
end
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   167
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   168
lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   169
  unfolding Sup_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   170
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   171
lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   172
  unfolding Sup_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   173
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   174
lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   175
  unfolding Inf_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   176
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   177
lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   178
  unfolding Inf_prod_def by simp
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   179
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   180
lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44006
diff changeset
   181
  by (simp add: SUP_def fst_Sup image_image)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   182
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   183
lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44006
diff changeset
   184
  by (simp add: SUP_def snd_Sup image_image)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   185
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   186
lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44006
diff changeset
   187
  by (simp add: INF_def fst_Inf image_image)
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 snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44006
diff changeset
   190
  by (simp add: INF_def snd_Inf image_image)
44006
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 SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44006
diff changeset
   193
  by (simp add: SUP_def Sup_prod_def image_image)
44006
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 INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44006
diff changeset
   196
  by (simp add: INF_def Inf_prod_def image_image)
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   197
50535
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   198
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   199
text {* Alternative formulations for set infima and suprema over the product
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   200
of two complete lattices: *}
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   201
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   202
lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))"
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   203
by (auto simp: Inf_prod_def INF_def)
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   204
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   205
lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))"
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   206
by (auto simp: Sup_prod_def SUP_def)
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   207
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   208
lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   209
by (auto simp: INF_def Inf_prod_def image_compose)
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   210
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   211
lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   212
by (auto simp: SUP_def Sup_prod_def image_compose)
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   213
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   214
lemma INF_prod_alt_def:
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   215
  "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   216
by (metis fst_INF snd_INF surjective_pairing)
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   217
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   218
lemma SUP_prod_alt_def:
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   219
  "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))"
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   220
by (metis fst_SUP snd_SUP surjective_pairing)
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   221
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   222
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   223
subsection {* Complete distributive lattices *}
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   224
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   225
(* Contribution: Allesandro Coglio *)
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   226
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   227
instance prod ::
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   228
  (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   229
proof
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   230
  case goal1 thus ?case
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   231
    by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF)
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   232
next
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   233
  case goal2 thus ?case
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   234
    by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP)
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   235
qed
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   236
2464d77527c4 contribution by A. Colgio
nipkow
parents: 45007
diff changeset
   237
44006
b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy
huffman
parents:
diff changeset
   238
end