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