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