src/HOL/Library/Finite_Lattice.thy
 author nipkow Tue Sep 22 14:31:22 2015 +0200 (2015-09-22) changeset 61225 1a690dce8cfc parent 60679 ade12ef2773c child 62343 24106dc44def permissions -rw-r--r--
tuned references
```     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_code)
```
```   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_code)
```
```   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_code)
```
```   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_code)
```
```   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_code)
```
```   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_code)
```
```   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   apply (rule finite_induct)
```
```   169   apply (metis finite_code)
```
```   170   apply (metis SUP_empty Sup_empty inf_bot_right)
```
```   171   apply (metis SUP_insert Sup_insert inf_sup_distrib1)
```
```   172   done
```
```   173
```
```   174 instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
```
```   175 proof
```
```   176 qed (auto simp:
```
```   177   finite_distrib_lattice_complete_sup_Inf
```
```   178   finite_distrib_lattice_complete_inf_Sup)
```
```   179
```
```   180 text \<open>The product of two finite distributive lattices
```
```   181 is already a finite distributive lattice.\<close>
```
```   182
```
```   183 instance prod ::
```
```   184   (finite_distrib_lattice_complete, finite_distrib_lattice_complete)
```
```   185   finite_distrib_lattice_complete
```
```   186   ..
```
```   187
```
```   188 text \<open>Functions with a finite domain
```
```   189 and with a finite distributive lattice as codomain
```
```   190 already form a finite distributive lattice.\<close>
```
```   191
```
```   192 instance "fun" ::
```
```   193   (finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete
```
```   194   ..
```
```   195
```
```   196
```
```   197 subsection \<open>Linear Orders\<close>
```
```   198
```
```   199 text \<open>A linear order is a distributive lattice.
```
```   200 A type class is defined
```
```   201 that extends class @{class linorder}
```
```   202 with the operators @{const inf} and @{const sup},
```
```   203 along with assumptions that define these operators
```
```   204 in terms of the ones of class @{class linorder}.
```
```   205 The resulting class is a subclass of @{class distrib_lattice}.\<close>
```
```   206
```
```   207 class linorder_lattice = linorder + inf + sup +
```
```   208   assumes inf_def: "inf x y = (if x \<le> y then x else y)"
```
```   209   assumes sup_def: "sup x y = (if x \<ge> y then x else y)"
```
```   210
```
```   211 text \<open>The definitional assumptions
```
```   212 on the operators @{const inf} and @{const sup}
```
```   213 of class @{class linorder_lattice}
```
```   214 ensure that they yield infimum and supremum
```
```   215 and that they distribute over each other.\<close>
```
```   216
```
```   217 lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x"
```
```   218   unfolding inf_def by (metis (full_types) linorder_linear)
```
```   219
```
```   220 lemma linorder_lattice_inf_le2: "inf (x::'a::linorder_lattice) y \<le> y"
```
```   221   unfolding inf_def by (metis (full_types) linorder_linear)
```
```   222
```
```   223 lemma linorder_lattice_inf_greatest:
```
```   224   "(x::'a::linorder_lattice) \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z"
```
```   225   unfolding inf_def by (metis (full_types))
```
```   226
```
```   227 lemma linorder_lattice_sup_ge1: "sup (x::'a::linorder_lattice) y \<ge> x"
```
```   228   unfolding sup_def by (metis (full_types) linorder_linear)
```
```   229
```
```   230 lemma linorder_lattice_sup_ge2: "sup (x::'a::linorder_lattice) y \<ge> y"
```
```   231   unfolding sup_def by (metis (full_types) linorder_linear)
```
```   232
```
```   233 lemma linorder_lattice_sup_least:
```
```   234   "(x::'a::linorder_lattice) \<ge> y \<Longrightarrow> x \<ge> z \<Longrightarrow> x \<ge> sup y z"
```
```   235   by (auto simp: sup_def)
```
```   236
```
```   237 lemma linorder_lattice_sup_inf_distrib1:
```
```   238   "sup (x::'a::linorder_lattice) (inf y z) = inf (sup x y) (sup x z)"
```
```   239   by (auto simp: inf_def sup_def)
```
```   240
```
```   241 instance linorder_lattice \<subseteq> distrib_lattice
```
```   242 proof
```
```   243 qed (auto simp:
```
```   244   linorder_lattice_inf_le1
```
```   245   linorder_lattice_inf_le2
```
```   246   linorder_lattice_inf_greatest
```
```   247   linorder_lattice_sup_ge1
```
```   248   linorder_lattice_sup_ge2
```
```   249   linorder_lattice_sup_least
```
```   250   linorder_lattice_sup_inf_distrib1)
```
```   251
```
```   252
```
```   253 subsection \<open>Finite Linear Orders\<close>
```
```   254
```
```   255 text \<open>A (non-empty) finite linear order is a complete linear order.\<close>
```
```   256
```
```   257 class finite_linorder_complete = linorder_lattice + finite_lattice_complete
```
```   258
```
```   259 instance finite_linorder_complete \<subseteq> complete_linorder ..
```
```   260
```
```   261 text \<open>A (non-empty) finite linear order is a complete lattice
```
```   262 whose @{const inf} and @{const sup} operators
```
```   263 distribute over @{const Sup} and @{const Inf}.\<close>
```
```   264
```
```   265 instance finite_linorder_complete \<subseteq> finite_distrib_lattice_complete ..
```
```   266
```
```   267 end
```
```   268
```