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