src/HOL/Library/Finite_Lattice.thy
author haftmann
Fri Nov 01 18:51:14 2013 +0100 (2013-11-01)
changeset 54230 b1d955791529
parent 52729 412c9e0381a1
child 56740 5ebaa364d8ab
permissions -rw-r--r--
more simplification rules on unary and binary minus
nipkow@50634
     1
(* Author: Alessandro Coglio *)
nipkow@50634
     2
nipkow@50634
     3
theory Finite_Lattice
haftmann@51115
     4
imports Product_Order
nipkow@50634
     5
begin
nipkow@50634
     6
nipkow@50634
     7
text {* A non-empty finite lattice is a complete lattice.
nipkow@50634
     8
Since types are never empty in Isabelle/HOL,
nipkow@50634
     9
a type of classes @{class finite} and @{class lattice}
nipkow@50634
    10
should also have class @{class complete_lattice}.
nipkow@50634
    11
A type class is defined
nipkow@50634
    12
that extends classes @{class finite} and @{class lattice}
nipkow@50634
    13
with the operators @{const bot}, @{const top}, @{const Inf}, and @{const Sup},
nipkow@50634
    14
along with assumptions that define these operators
nipkow@50634
    15
in terms of the ones of classes @{class finite} and @{class lattice}.
haftmann@52729
    16
The resulting class is a subclass of @{class complete_lattice}. *}
nipkow@50634
    17
nipkow@50634
    18
class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup +
haftmann@52729
    19
assumes bot_def: "bot = Inf_fin UNIV"
haftmann@52729
    20
assumes top_def: "top = Sup_fin UNIV"
nipkow@50634
    21
assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
nipkow@50634
    22
assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
haftmann@52729
    23
haftmann@52729
    24
text {* The definitional assumptions
haftmann@52729
    25
on the operators @{const bot} and @{const top}
haftmann@52729
    26
of class @{class finite_lattice_complete}
haftmann@52729
    27
ensure that they yield bottom and top. *}
haftmann@52729
    28
haftmann@52729
    29
lemma finite_lattice_complete_bot_least:
haftmann@52729
    30
"(bot::'a::finite_lattice_complete) \<le> x"
haftmann@52729
    31
by (auto simp: bot_def intro: Inf_fin.coboundedI)
haftmann@52729
    32
haftmann@52729
    33
instance finite_lattice_complete \<subseteq> order_bot
haftmann@52729
    34
proof qed (auto simp: finite_lattice_complete_bot_least)
haftmann@52729
    35
haftmann@52729
    36
lemma finite_lattice_complete_top_greatest:
haftmann@52729
    37
"(top::'a::finite_lattice_complete) \<ge> x"
haftmann@52729
    38
by (auto simp: top_def Sup_fin.coboundedI)
haftmann@52729
    39
haftmann@52729
    40
instance finite_lattice_complete \<subseteq> order_top
haftmann@52729
    41
proof qed (auto simp: finite_lattice_complete_top_greatest)
nipkow@50634
    42
nipkow@50634
    43
instance finite_lattice_complete \<subseteq> bounded_lattice ..
nipkow@50634
    44
haftmann@52729
    45
text {* The definitional assumptions
haftmann@52729
    46
on the operators @{const Inf} and @{const Sup}
haftmann@52729
    47
of class @{class finite_lattice_complete}
haftmann@52729
    48
ensure that they yield infimum and supremum. *}
nipkow@50634
    49
haftmann@51489
    50
lemma finite_lattice_complete_Inf_empty:
haftmann@51489
    51
  "Inf {} = (top :: 'a::finite_lattice_complete)"
haftmann@51489
    52
  by (simp add: Inf_def)
haftmann@51489
    53
haftmann@51489
    54
lemma finite_lattice_complete_Sup_empty:
haftmann@51489
    55
  "Sup {} = (bot :: 'a::finite_lattice_complete)"
haftmann@51489
    56
  by (simp add: Sup_def)
haftmann@51489
    57
haftmann@51489
    58
lemma finite_lattice_complete_Inf_insert:
haftmann@51489
    59
  fixes A :: "'a::finite_lattice_complete set"
haftmann@51489
    60
  shows "Inf (insert x A) = inf x (Inf A)"
haftmann@51489
    61
proof -
haftmann@51489
    62
  interpret comp_fun_idem "inf :: 'a \<Rightarrow> _" by (fact comp_fun_idem_inf)
haftmann@51489
    63
  show ?thesis by (simp add: Inf_def)
haftmann@51489
    64
qed
haftmann@51489
    65
haftmann@51489
    66
lemma finite_lattice_complete_Sup_insert:
haftmann@51489
    67
  fixes A :: "'a::finite_lattice_complete set"
haftmann@51489
    68
  shows "Sup (insert x A) = sup x (Sup A)"
haftmann@51489
    69
proof -
haftmann@51489
    70
  interpret comp_fun_idem "sup :: 'a \<Rightarrow> _" by (fact comp_fun_idem_sup)
haftmann@51489
    71
  show ?thesis by (simp add: Sup_def)
haftmann@51489
    72
qed
haftmann@51489
    73
nipkow@50634
    74
lemma finite_lattice_complete_Inf_lower:
nipkow@50634
    75
  "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x"
haftmann@51489
    76
  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2)
nipkow@50634
    77
nipkow@50634
    78
lemma finite_lattice_complete_Inf_greatest:
nipkow@50634
    79
  "\<forall>x::'a::finite_lattice_complete \<in> A. z \<le> x \<Longrightarrow> z \<le> Inf A"
haftmann@51489
    80
  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_empty finite_lattice_complete_Inf_insert)
nipkow@50634
    81
nipkow@50634
    82
lemma finite_lattice_complete_Sup_upper:
nipkow@50634
    83
  "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Sup A \<ge> x"
haftmann@51489
    84
  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_insert intro: le_supI2)
nipkow@50634
    85
nipkow@50634
    86
lemma finite_lattice_complete_Sup_least:
nipkow@50634
    87
  "\<forall>x::'a::finite_lattice_complete \<in> A. z \<ge> x \<Longrightarrow> z \<ge> Sup A"
haftmann@51489
    88
  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_empty finite_lattice_complete_Sup_insert)
nipkow@50634
    89
nipkow@50634
    90
instance finite_lattice_complete \<subseteq> complete_lattice
nipkow@50634
    91
proof
nipkow@50634
    92
qed (auto simp:
nipkow@50634
    93
 finite_lattice_complete_Inf_lower
nipkow@50634
    94
 finite_lattice_complete_Inf_greatest
nipkow@50634
    95
 finite_lattice_complete_Sup_upper
haftmann@52729
    96
 finite_lattice_complete_Sup_least
haftmann@52729
    97
 finite_lattice_complete_Inf_empty
haftmann@52729
    98
 finite_lattice_complete_Sup_empty)
nipkow@50634
    99
nipkow@50634
   100
text {* The product of two finite lattices is already a finite lattice. *}
nipkow@50634
   101
haftmann@52729
   102
lemma finite_bot_prod:
haftmann@52729
   103
  "(bot :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
haftmann@52729
   104
   Inf_fin UNIV"
haftmann@52729
   105
by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV)
haftmann@52729
   106
haftmann@52729
   107
lemma finite_top_prod:
haftmann@52729
   108
  "(top :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
haftmann@52729
   109
   Sup_fin UNIV"
haftmann@52729
   110
by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV)
haftmann@52729
   111
nipkow@50634
   112
lemma finite_Inf_prod:
haftmann@52729
   113
  "Inf(A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
nipkow@50634
   114
  Finite_Set.fold inf top A"
nipkow@50634
   115
by (metis Inf_fold_inf finite_code)
nipkow@50634
   116
nipkow@50634
   117
lemma finite_Sup_prod:
haftmann@52729
   118
  "Sup (A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
nipkow@50634
   119
  Finite_Set.fold sup bot A"
nipkow@50634
   120
by (metis Sup_fold_sup finite_code)
nipkow@50634
   121
nipkow@50634
   122
instance prod ::
nipkow@50634
   123
  (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
haftmann@52729
   124
proof
haftmann@52729
   125
qed (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
nipkow@50634
   126
nipkow@50634
   127
text {* Functions with a finite domain and with a finite lattice as codomain
nipkow@50634
   128
already form a finite lattice. *}
nipkow@50634
   129
haftmann@52729
   130
lemma finite_bot_fun:
haftmann@52729
   131
  "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV"
haftmann@52729
   132
by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code)
haftmann@52729
   133
haftmann@52729
   134
lemma finite_top_fun:
haftmann@52729
   135
  "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV"
haftmann@52729
   136
by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code)
haftmann@52729
   137
nipkow@50634
   138
lemma finite_Inf_fun:
nipkow@50634
   139
  "Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
nipkow@50634
   140
  Finite_Set.fold inf top A"
nipkow@50634
   141
by (metis Inf_fold_inf finite_code)
nipkow@50634
   142
nipkow@50634
   143
lemma finite_Sup_fun:
nipkow@50634
   144
  "Sup (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
nipkow@50634
   145
  Finite_Set.fold sup bot A"
nipkow@50634
   146
by (metis Sup_fold_sup finite_code)
nipkow@50634
   147
nipkow@50634
   148
instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
haftmann@52729
   149
proof
haftmann@52729
   150
qed (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
nipkow@50634
   151
nipkow@50634
   152
nipkow@50634
   153
subsection {* Finite Distributive Lattices *}
nipkow@50634
   154
nipkow@50634
   155
text {* A finite distributive lattice is a complete lattice
nipkow@50634
   156
whose @{const inf} and @{const sup} operators
nipkow@50634
   157
distribute over @{const Sup} and @{const Inf}. *}
nipkow@50634
   158
nipkow@50634
   159
class finite_distrib_lattice_complete =
nipkow@50634
   160
  distrib_lattice + finite_lattice_complete
nipkow@50634
   161
nipkow@50634
   162
lemma finite_distrib_lattice_complete_sup_Inf:
nipkow@50634
   163
  "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)"
nipkow@50634
   164
apply (rule finite_induct)
nipkow@50634
   165
apply (metis finite_code)
nipkow@50634
   166
apply (metis INF_empty Inf_empty sup_top_right)
nipkow@50634
   167
apply (metis INF_insert Inf_insert sup_inf_distrib1)
nipkow@50634
   168
done
nipkow@50634
   169
nipkow@50634
   170
lemma finite_distrib_lattice_complete_inf_Sup:
nipkow@50634
   171
  "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
nipkow@50634
   172
apply (rule finite_induct)
nipkow@50634
   173
apply (metis finite_code)
nipkow@50634
   174
apply (metis SUP_empty Sup_empty inf_bot_right)
nipkow@50634
   175
apply (metis SUP_insert Sup_insert inf_sup_distrib1)
nipkow@50634
   176
done
nipkow@50634
   177
nipkow@50634
   178
instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
nipkow@50634
   179
proof
nipkow@50634
   180
qed (auto simp:
nipkow@50634
   181
 finite_distrib_lattice_complete_sup_Inf
nipkow@50634
   182
 finite_distrib_lattice_complete_inf_Sup)
nipkow@50634
   183
nipkow@50634
   184
text {* The product of two finite distributive lattices
nipkow@50634
   185
is already a finite distributive lattice. *}
nipkow@50634
   186
nipkow@50634
   187
instance prod ::
nipkow@50634
   188
  (finite_distrib_lattice_complete, finite_distrib_lattice_complete)
nipkow@50634
   189
  finite_distrib_lattice_complete
nipkow@50634
   190
..
nipkow@50634
   191
nipkow@50634
   192
text {* Functions with a finite domain
nipkow@50634
   193
and with a finite distributive lattice as codomain
nipkow@50634
   194
already form a finite distributive lattice. *}
nipkow@50634
   195
nipkow@50634
   196
instance "fun" ::
nipkow@50634
   197
  (finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete
nipkow@50634
   198
..
nipkow@50634
   199
nipkow@50634
   200
nipkow@50634
   201
subsection {* Linear Orders *}
nipkow@50634
   202
nipkow@50634
   203
text {* A linear order is a distributive lattice.
haftmann@52729
   204
A type class is defined
haftmann@52729
   205
that extends class @{class linorder}
haftmann@52729
   206
with the operators @{const inf} and @{const sup},
nipkow@50634
   207
along with assumptions that define these operators
nipkow@50634
   208
in terms of the ones of class @{class linorder}.
nipkow@50634
   209
The resulting class is a subclass of @{class distrib_lattice}. *}
nipkow@50634
   210
nipkow@50634
   211
class linorder_lattice = linorder + inf + sup +
nipkow@50634
   212
assumes inf_def: "inf x y = (if x \<le> y then x else y)"
nipkow@50634
   213
assumes sup_def: "sup x y = (if x \<ge> y then x else y)"
nipkow@50634
   214
nipkow@50634
   215
text {* The definitional assumptions
nipkow@50634
   216
on the operators @{const inf} and @{const sup}
nipkow@50634
   217
of class @{class linorder_lattice}
haftmann@52729
   218
ensure that they yield infimum and supremum
haftmann@52729
   219
and that they distribute over each other. *}
nipkow@50634
   220
nipkow@50634
   221
lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x"
nipkow@50634
   222
unfolding inf_def by (metis (full_types) linorder_linear)
nipkow@50634
   223
nipkow@50634
   224
lemma linorder_lattice_inf_le2: "inf (x::'a::linorder_lattice) y \<le> y"
nipkow@50634
   225
unfolding inf_def by (metis (full_types) linorder_linear)
nipkow@50634
   226
nipkow@50634
   227
lemma linorder_lattice_inf_greatest:
nipkow@50634
   228
  "(x::'a::linorder_lattice) \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z"
nipkow@50634
   229
unfolding inf_def by (metis (full_types))
nipkow@50634
   230
nipkow@50634
   231
lemma linorder_lattice_sup_ge1: "sup (x::'a::linorder_lattice) y \<ge> x"
nipkow@50634
   232
unfolding sup_def by (metis (full_types) linorder_linear)
nipkow@50634
   233
nipkow@50634
   234
lemma linorder_lattice_sup_ge2: "sup (x::'a::linorder_lattice) y \<ge> y"
nipkow@50634
   235
unfolding sup_def by (metis (full_types) linorder_linear)
nipkow@50634
   236
nipkow@50634
   237
lemma linorder_lattice_sup_least:
nipkow@50634
   238
  "(x::'a::linorder_lattice) \<ge> y \<Longrightarrow> x \<ge> z \<Longrightarrow> x \<ge> sup y z"
nipkow@50634
   239
by (auto simp: sup_def)
nipkow@50634
   240
nipkow@50634
   241
lemma linorder_lattice_sup_inf_distrib1:
nipkow@50634
   242
  "sup (x::'a::linorder_lattice) (inf y z) = inf (sup x y) (sup x z)"
nipkow@50634
   243
by (auto simp: inf_def sup_def)
nipkow@50634
   244
 
nipkow@50634
   245
instance linorder_lattice \<subseteq> distrib_lattice
nipkow@50634
   246
proof                                                     
nipkow@50634
   247
qed (auto simp:
nipkow@50634
   248
 linorder_lattice_inf_le1
nipkow@50634
   249
 linorder_lattice_inf_le2
nipkow@50634
   250
 linorder_lattice_inf_greatest
nipkow@50634
   251
 linorder_lattice_sup_ge1
nipkow@50634
   252
 linorder_lattice_sup_ge2
nipkow@50634
   253
 linorder_lattice_sup_least
nipkow@50634
   254
 linorder_lattice_sup_inf_distrib1)
nipkow@50634
   255
nipkow@50634
   256
nipkow@50634
   257
subsection {* Finite Linear Orders *}
nipkow@50634
   258
nipkow@50634
   259
text {* A (non-empty) finite linear order is a complete linear order. *}
nipkow@50634
   260
nipkow@50634
   261
class finite_linorder_complete = linorder_lattice + finite_lattice_complete
nipkow@50634
   262
nipkow@50634
   263
instance finite_linorder_complete \<subseteq> complete_linorder ..
nipkow@50634
   264
nipkow@50634
   265
text {* A (non-empty) finite linear order is a complete lattice
nipkow@50634
   266
whose @{const inf} and @{const sup} operators
nipkow@50634
   267
distribute over @{const Sup} and @{const Inf}. *}
nipkow@50634
   268
nipkow@50634
   269
instance finite_linorder_complete \<subseteq> finite_distrib_lattice_complete ..
nipkow@50634
   270
nipkow@50634
   271
nipkow@50634
   272
end
haftmann@52729
   273