src/HOL/Library/Finite_Lattice.thy
changeset 56796 9f84219715a7
parent 56740 5ebaa364d8ab
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/Finite_Lattice.thy	Tue Apr 29 21:54:26 2014 +0200
     1.2 +++ b/src/HOL/Library/Finite_Lattice.thy	Tue Apr 29 22:50:55 2014 +0200
     1.3 @@ -1,4 +1,6 @@
     1.4 -(* Author: Alessandro Coglio *)
     1.5 +(*  Title:      HOL/Library/Finite_Lattice.thy
     1.6 +    Author:     Alessandro Coglio
     1.7 +*)
     1.8  
     1.9  theory Finite_Lattice
    1.10  imports Product_Order
    1.11 @@ -16,29 +18,27 @@
    1.12  The resulting class is a subclass of @{class complete_lattice}. *}
    1.13  
    1.14  class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup +
    1.15 -assumes bot_def: "bot = Inf_fin UNIV"
    1.16 -assumes top_def: "top = Sup_fin UNIV"
    1.17 -assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
    1.18 -assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
    1.19 +  assumes bot_def: "bot = Inf_fin UNIV"
    1.20 +  assumes top_def: "top = Sup_fin UNIV"
    1.21 +  assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
    1.22 +  assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
    1.23  
    1.24  text {* The definitional assumptions
    1.25  on the operators @{const bot} and @{const top}
    1.26  of class @{class finite_lattice_complete}
    1.27  ensure that they yield bottom and top. *}
    1.28  
    1.29 -lemma finite_lattice_complete_bot_least:
    1.30 -"(bot::'a::finite_lattice_complete) \<le> x"
    1.31 -by (auto simp: bot_def intro: Inf_fin.coboundedI)
    1.32 +lemma finite_lattice_complete_bot_least: "(bot::'a::finite_lattice_complete) \<le> x"
    1.33 +  by (auto simp: bot_def intro: Inf_fin.coboundedI)
    1.34  
    1.35  instance finite_lattice_complete \<subseteq> order_bot
    1.36 -proof qed (auto simp: finite_lattice_complete_bot_least)
    1.37 +  by default (auto simp: finite_lattice_complete_bot_least)
    1.38  
    1.39 -lemma finite_lattice_complete_top_greatest:
    1.40 -"(top::'a::finite_lattice_complete) \<ge> x"
    1.41 -by (auto simp: top_def Sup_fin.coboundedI)
    1.42 +lemma finite_lattice_complete_top_greatest: "(top::'a::finite_lattice_complete) \<ge> x"
    1.43 +  by (auto simp: top_def Sup_fin.coboundedI)
    1.44  
    1.45  instance finite_lattice_complete \<subseteq> order_top
    1.46 -proof qed (auto simp: finite_lattice_complete_top_greatest)
    1.47 +  by default (auto simp: finite_lattice_complete_top_greatest)
    1.48  
    1.49  instance finite_lattice_complete \<subseteq> bounded_lattice ..
    1.50  
    1.51 @@ -47,19 +47,18 @@
    1.52  of class @{class finite_lattice_complete}
    1.53  ensure that they yield infimum and supremum. *}
    1.54  
    1.55 -lemma finite_lattice_complete_Inf_empty:
    1.56 -  "Inf {} = (top :: 'a::finite_lattice_complete)"
    1.57 +lemma finite_lattice_complete_Inf_empty: "Inf {} = (top :: 'a::finite_lattice_complete)"
    1.58    by (simp add: Inf_def)
    1.59  
    1.60 -lemma finite_lattice_complete_Sup_empty:
    1.61 -  "Sup {} = (bot :: 'a::finite_lattice_complete)"
    1.62 +lemma finite_lattice_complete_Sup_empty: "Sup {} = (bot :: 'a::finite_lattice_complete)"
    1.63    by (simp add: Sup_def)
    1.64  
    1.65  lemma finite_lattice_complete_Inf_insert:
    1.66    fixes A :: "'a::finite_lattice_complete set"
    1.67    shows "Inf (insert x A) = inf x (Inf A)"
    1.68  proof -
    1.69 -  interpret comp_fun_idem "inf :: 'a \<Rightarrow> _" by (fact comp_fun_idem_inf)
    1.70 +  interpret comp_fun_idem "inf :: 'a \<Rightarrow> _"
    1.71 +    by (fact comp_fun_idem_inf)
    1.72    show ?thesis by (simp add: Inf_def)
    1.73  qed
    1.74  
    1.75 @@ -67,87 +66,87 @@
    1.76    fixes A :: "'a::finite_lattice_complete set"
    1.77    shows "Sup (insert x A) = sup x (Sup A)"
    1.78  proof -
    1.79 -  interpret comp_fun_idem "sup :: 'a \<Rightarrow> _" by (fact comp_fun_idem_sup)
    1.80 +  interpret comp_fun_idem "sup :: 'a \<Rightarrow> _"
    1.81 +    by (fact comp_fun_idem_sup)
    1.82    show ?thesis by (simp add: Sup_def)
    1.83  qed
    1.84  
    1.85  lemma finite_lattice_complete_Inf_lower:
    1.86    "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x"
    1.87 -  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2)
    1.88 +  using finite [of A]
    1.89 +  by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2)
    1.90  
    1.91  lemma finite_lattice_complete_Inf_greatest:
    1.92    "\<forall>x::'a::finite_lattice_complete \<in> A. z \<le> x \<Longrightarrow> z \<le> Inf A"
    1.93 -  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_empty finite_lattice_complete_Inf_insert)
    1.94 +  using finite [of A]
    1.95 +  by (induct A) (auto simp add: finite_lattice_complete_Inf_empty finite_lattice_complete_Inf_insert)
    1.96  
    1.97  lemma finite_lattice_complete_Sup_upper:
    1.98    "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Sup A \<ge> x"
    1.99 -  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_insert intro: le_supI2)
   1.100 +  using finite [of A]
   1.101 +  by (induct A) (auto simp add: finite_lattice_complete_Sup_insert intro: le_supI2)
   1.102  
   1.103  lemma finite_lattice_complete_Sup_least:
   1.104    "\<forall>x::'a::finite_lattice_complete \<in> A. z \<ge> x \<Longrightarrow> z \<ge> Sup A"
   1.105 -  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_empty finite_lattice_complete_Sup_insert)
   1.106 +  using finite [of A]
   1.107 +  by (induct A) (auto simp add: finite_lattice_complete_Sup_empty finite_lattice_complete_Sup_insert)
   1.108  
   1.109  instance finite_lattice_complete \<subseteq> complete_lattice
   1.110  proof
   1.111  qed (auto simp:
   1.112 - finite_lattice_complete_Inf_lower
   1.113 - finite_lattice_complete_Inf_greatest
   1.114 - finite_lattice_complete_Sup_upper
   1.115 - finite_lattice_complete_Sup_least
   1.116 - finite_lattice_complete_Inf_empty
   1.117 - finite_lattice_complete_Sup_empty)
   1.118 +  finite_lattice_complete_Inf_lower
   1.119 +  finite_lattice_complete_Inf_greatest
   1.120 +  finite_lattice_complete_Sup_upper
   1.121 +  finite_lattice_complete_Sup_least
   1.122 +  finite_lattice_complete_Inf_empty
   1.123 +  finite_lattice_complete_Sup_empty)
   1.124  
   1.125  text {* The product of two finite lattices is already a finite lattice. *}
   1.126  
   1.127  lemma finite_bot_prod:
   1.128    "(bot :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
   1.129 -   Inf_fin UNIV"
   1.130 -by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV)
   1.131 +    Inf_fin UNIV"
   1.132 +  by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV)
   1.133  
   1.134  lemma finite_top_prod:
   1.135    "(top :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
   1.136 -   Sup_fin UNIV"
   1.137 -by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV)
   1.138 +    Sup_fin UNIV"
   1.139 +  by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV)
   1.140  
   1.141  lemma finite_Inf_prod:
   1.142    "Inf(A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
   1.143 -  Finite_Set.fold inf top A"
   1.144 -by (metis Inf_fold_inf finite_code)
   1.145 +    Finite_Set.fold inf top A"
   1.146 +  by (metis Inf_fold_inf finite_code)
   1.147  
   1.148  lemma finite_Sup_prod:
   1.149    "Sup (A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
   1.150 -  Finite_Set.fold sup bot A"
   1.151 -by (metis Sup_fold_sup finite_code)
   1.152 +    Finite_Set.fold sup bot A"
   1.153 +  by (metis Sup_fold_sup finite_code)
   1.154  
   1.155 -instance prod ::
   1.156 -  (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
   1.157 -proof
   1.158 -qed (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
   1.159 +instance prod :: (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
   1.160 +  by default (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
   1.161  
   1.162  text {* Functions with a finite domain and with a finite lattice as codomain
   1.163  already form a finite lattice. *}
   1.164  
   1.165 -lemma finite_bot_fun:
   1.166 -  "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV"
   1.167 -by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code)
   1.168 +lemma finite_bot_fun: "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV"
   1.169 +  by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code)
   1.170  
   1.171 -lemma finite_top_fun:
   1.172 -  "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV"
   1.173 -by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code)
   1.174 +lemma finite_top_fun: "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV"
   1.175 +  by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code)
   1.176  
   1.177  lemma finite_Inf_fun:
   1.178    "Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
   1.179 -  Finite_Set.fold inf top A"
   1.180 -by (metis Inf_fold_inf finite_code)
   1.181 +    Finite_Set.fold inf top A"
   1.182 +  by (metis Inf_fold_inf finite_code)
   1.183  
   1.184  lemma finite_Sup_fun:
   1.185    "Sup (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
   1.186 -  Finite_Set.fold sup bot A"
   1.187 -by (metis Sup_fold_sup finite_code)
   1.188 +    Finite_Set.fold sup bot A"
   1.189 +  by (metis Sup_fold_sup finite_code)
   1.190  
   1.191  instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
   1.192 -proof
   1.193 -qed (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
   1.194 +  by default (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
   1.195  
   1.196  
   1.197  subsection {* Finite Distributive Lattices *}
   1.198 @@ -161,22 +160,22 @@
   1.199  
   1.200  lemma finite_distrib_lattice_complete_sup_Inf:
   1.201    "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)"
   1.202 -  using finite by (induct A rule: finite_induct)
   1.203 -    (simp_all add: sup_inf_distrib1)
   1.204 +  using finite
   1.205 +  by (induct A rule: finite_induct) (simp_all add: sup_inf_distrib1)
   1.206  
   1.207  lemma finite_distrib_lattice_complete_inf_Sup:
   1.208    "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
   1.209 -apply (rule finite_induct)
   1.210 -apply (metis finite_code)
   1.211 -apply (metis SUP_empty Sup_empty inf_bot_right)
   1.212 -apply (metis SUP_insert Sup_insert inf_sup_distrib1)
   1.213 -done
   1.214 +  apply (rule finite_induct)
   1.215 +  apply (metis finite_code)
   1.216 +  apply (metis SUP_empty Sup_empty inf_bot_right)
   1.217 +  apply (metis SUP_insert Sup_insert inf_sup_distrib1)
   1.218 +  done
   1.219  
   1.220  instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
   1.221  proof
   1.222  qed (auto simp:
   1.223 - finite_distrib_lattice_complete_sup_Inf
   1.224 - finite_distrib_lattice_complete_inf_Sup)
   1.225 +  finite_distrib_lattice_complete_sup_Inf
   1.226 +  finite_distrib_lattice_complete_inf_Sup)
   1.227  
   1.228  text {* The product of two finite distributive lattices
   1.229  is already a finite distributive lattice. *}
   1.230 @@ -184,7 +183,7 @@
   1.231  instance prod ::
   1.232    (finite_distrib_lattice_complete, finite_distrib_lattice_complete)
   1.233    finite_distrib_lattice_complete
   1.234 -..
   1.235 +  ..
   1.236  
   1.237  text {* Functions with a finite domain
   1.238  and with a finite distributive lattice as codomain
   1.239 @@ -192,7 +191,7 @@
   1.240  
   1.241  instance "fun" ::
   1.242    (finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete
   1.243 -..
   1.244 +  ..
   1.245  
   1.246  
   1.247  subsection {* Linear Orders *}
   1.248 @@ -206,8 +205,8 @@
   1.249  The resulting class is a subclass of @{class distrib_lattice}. *}
   1.250  
   1.251  class linorder_lattice = linorder + inf + sup +
   1.252 -assumes inf_def: "inf x y = (if x \<le> y then x else y)"
   1.253 -assumes sup_def: "sup x y = (if x \<ge> y then x else y)"
   1.254 +  assumes inf_def: "inf x y = (if x \<le> y then x else y)"
   1.255 +  assumes sup_def: "sup x y = (if x \<ge> y then x else y)"
   1.256  
   1.257  text {* The definitional assumptions
   1.258  on the operators @{const inf} and @{const sup}
   1.259 @@ -216,39 +215,39 @@
   1.260  and that they distribute over each other. *}
   1.261  
   1.262  lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x"
   1.263 -unfolding inf_def by (metis (full_types) linorder_linear)
   1.264 +  unfolding inf_def by (metis (full_types) linorder_linear)
   1.265  
   1.266  lemma linorder_lattice_inf_le2: "inf (x::'a::linorder_lattice) y \<le> y"
   1.267 -unfolding inf_def by (metis (full_types) linorder_linear)
   1.268 +  unfolding inf_def by (metis (full_types) linorder_linear)
   1.269  
   1.270  lemma linorder_lattice_inf_greatest:
   1.271    "(x::'a::linorder_lattice) \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z"
   1.272 -unfolding inf_def by (metis (full_types))
   1.273 +  unfolding inf_def by (metis (full_types))
   1.274  
   1.275  lemma linorder_lattice_sup_ge1: "sup (x::'a::linorder_lattice) y \<ge> x"
   1.276 -unfolding sup_def by (metis (full_types) linorder_linear)
   1.277 +  unfolding sup_def by (metis (full_types) linorder_linear)
   1.278  
   1.279  lemma linorder_lattice_sup_ge2: "sup (x::'a::linorder_lattice) y \<ge> y"
   1.280 -unfolding sup_def by (metis (full_types) linorder_linear)
   1.281 +  unfolding sup_def by (metis (full_types) linorder_linear)
   1.282  
   1.283  lemma linorder_lattice_sup_least:
   1.284    "(x::'a::linorder_lattice) \<ge> y \<Longrightarrow> x \<ge> z \<Longrightarrow> x \<ge> sup y z"
   1.285 -by (auto simp: sup_def)
   1.286 +  by (auto simp: sup_def)
   1.287  
   1.288  lemma linorder_lattice_sup_inf_distrib1:
   1.289    "sup (x::'a::linorder_lattice) (inf y z) = inf (sup x y) (sup x z)"
   1.290 -by (auto simp: inf_def sup_def)
   1.291 - 
   1.292 +  by (auto simp: inf_def sup_def)
   1.293 +
   1.294  instance linorder_lattice \<subseteq> distrib_lattice
   1.295 -proof                                                     
   1.296 +proof
   1.297  qed (auto simp:
   1.298 - linorder_lattice_inf_le1
   1.299 - linorder_lattice_inf_le2
   1.300 - linorder_lattice_inf_greatest
   1.301 - linorder_lattice_sup_ge1
   1.302 - linorder_lattice_sup_ge2
   1.303 - linorder_lattice_sup_least
   1.304 - linorder_lattice_sup_inf_distrib1)
   1.305 +  linorder_lattice_inf_le1
   1.306 +  linorder_lattice_inf_le2
   1.307 +  linorder_lattice_inf_greatest
   1.308 +  linorder_lattice_sup_ge1
   1.309 +  linorder_lattice_sup_ge2
   1.310 +  linorder_lattice_sup_least
   1.311 +  linorder_lattice_sup_inf_distrib1)
   1.312  
   1.313  
   1.314  subsection {* Finite Linear Orders *}
   1.315 @@ -265,6 +264,5 @@
   1.316  
   1.317  instance finite_linorder_complete \<subseteq> finite_distrib_lattice_complete ..
   1.318  
   1.319 -
   1.320  end
   1.321