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