src/HOL/Library/Finite_Lattice.thy
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (11 months ago)
changeset 68658 16cc1161ad7f
parent 67829 2a6ef5ba4822
child 69260 0a9688695a1b
permissions -rw-r--r--
tuned equation
     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