src/HOL/Library/Dual_Ordered_Lattice.thy
author haftmann
Thu Mar 14 09:46:09 2019 +0100 (5 weeks ago)
changeset 69909 5382f5691a11
child 69947 77a92e8d5167
permissions -rw-r--r--
proper theory for type of dual ordered lattice in distribution
     1 (*  Title:      Dual_Ordered_Lattice.thy
     2     Authors:    Makarius; Peter Gammie; Brian Huffman; Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 section \<open>Type of dual ordered lattices\<close>
     6 
     7 theory Dual_Ordered_Lattice
     8 imports Main
     9 begin
    10 
    11 text \<open>
    12   The \<^emph>\<open>dual\<close> of an ordered structure is an isomorphic copy of the
    13   underlying type, with the \<open>\<le>\<close> relation defined as the inverse
    14   of the original one.
    15 
    16   The class of lattices is closed under formation of dual structures.
    17   This means that for any theorem of lattice theory, the dualized
    18   statement holds as well; this important fact simplifies many proofs
    19   of lattice theory.
    20 \<close>
    21 
    22 typedef 'a dual = "UNIV :: 'a set"
    23   morphisms undual dual ..
    24 
    25 setup_lifting type_definition_dual
    26 
    27 lemma dual_eqI:
    28   "x = y" if "undual x = undual y"
    29   using that by transfer assumption
    30 
    31 lemma dual_eq_iff:
    32   "x = y \<longleftrightarrow> undual x = undual y"
    33   by transfer simp
    34 
    35 lemma eq_dual_iff [iff]:
    36   "dual x = dual y \<longleftrightarrow> x = y"
    37   by transfer simp
    38 
    39 lemma undual_dual [simp]:
    40   "undual (dual x) = x"
    41   by transfer rule
    42 
    43 lemma dual_undual [simp]:
    44   "dual (undual x) = x"
    45   by transfer rule
    46 
    47 lemma undual_comp_dual [simp]:
    48   "undual \<circ> dual = id"
    49   by (simp add: fun_eq_iff)
    50 
    51 lemma dual_comp_undual [simp]:
    52   "dual \<circ> undual = id"
    53   by (simp add: fun_eq_iff)
    54 
    55 lemma inj_dual:
    56   "inj dual"
    57   by (rule injI) simp
    58 
    59 lemma inj_undual:
    60   "inj undual"
    61   by (rule injI) (rule dual_eqI)
    62 
    63 lemma surj_dual:
    64   "surj dual"
    65   by (rule surjI [of _ undual]) simp
    66 
    67 lemma surj_undual:
    68   "surj undual"
    69   by (rule surjI [of _ dual]) simp
    70 
    71 lemma bij_dual:
    72   "bij dual"
    73   using inj_dual surj_dual by (rule bijI)
    74 
    75 lemma bij_undual:
    76   "bij undual"
    77   using inj_undual surj_undual by (rule bijI)
    78 
    79 instance dual :: (finite) finite
    80 proof
    81   from finite have "finite (range dual :: 'a dual set)"
    82     by (rule finite_imageI)
    83   then show "finite (UNIV :: 'a dual set)"
    84     by (simp add: surj_dual)
    85 qed
    86 
    87 
    88 subsection \<open>Pointwise ordering\<close>
    89 
    90 instantiation dual :: (ord) ord
    91 begin
    92 
    93 lift_definition less_eq_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> bool"
    94   is "(\<ge>)" .
    95 
    96 lift_definition less_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> bool"
    97   is "(>)" .
    98 
    99 instance ..
   100 
   101 end
   102 
   103 lemma dual_less_eqI:
   104   "x \<le> y" if "undual y \<le> undual x"
   105   using that by transfer assumption
   106 
   107 lemma dual_less_eq_iff:
   108   "x \<le> y \<longleftrightarrow> undual y \<le> undual x"
   109   by transfer simp
   110 
   111 lemma less_eq_dual_iff [iff]:
   112   "dual x \<le> dual y \<longleftrightarrow> y \<le> x"
   113   by transfer simp
   114 
   115 lemma dual_lessI:
   116   "x < y" if "undual y < undual x"
   117   using that by transfer assumption
   118 
   119 lemma dual_less_iff:
   120   "x < y \<longleftrightarrow> undual y < undual x"
   121   by transfer simp
   122 
   123 lemma less_dual_iff [iff]:
   124   "dual x < dual y \<longleftrightarrow> y < x"
   125   by transfer simp
   126 
   127 instance dual :: (preorder) preorder
   128   by (standard; transfer) (auto simp add: less_le_not_le intro: order_trans)
   129 
   130 instance dual :: (order) order
   131   by (standard; transfer) simp
   132 
   133 
   134 subsection \<open>Binary infimum and supremum\<close>
   135 
   136 instantiation dual :: (sup) inf
   137 begin
   138 
   139 lift_definition inf_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> 'a dual"
   140   is sup .
   141 
   142 instance ..
   143 
   144 end
   145 
   146 lemma undual_inf_eq [simp]:
   147   "undual (inf x y) = sup (undual x) (undual y)"
   148   by (fact inf_dual.rep_eq)
   149 
   150 lemma dual_sup_eq [simp]:
   151   "dual (sup x y) = inf (dual x) (dual y)"
   152   by transfer rule
   153 
   154 instantiation dual :: (inf) sup
   155 begin
   156 
   157 lift_definition sup_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> 'a dual"
   158   is inf .
   159 
   160 instance ..
   161 
   162 end
   163 
   164 lemma undual_sup_eq [simp]:
   165   "undual (sup x y) = inf (undual x) (undual y)"
   166   by (fact sup_dual.rep_eq)
   167 
   168 lemma dual_inf_eq [simp]:
   169   "dual (inf x y) = sup (dual x) (dual y)"
   170   by transfer simp
   171 
   172 instance dual :: (semilattice_sup) semilattice_inf
   173   by (standard; transfer) simp_all
   174 
   175 instance dual :: (semilattice_inf) semilattice_sup
   176   by (standard; transfer) simp_all
   177 
   178 instance dual :: (lattice) lattice ..
   179 
   180 instance dual :: (distrib_lattice) distrib_lattice
   181   by (standard; transfer) (fact inf_sup_distrib1)
   182 
   183 
   184 subsection \<open>Top and bottom elements\<close>
   185 
   186 instantiation dual :: (top) bot
   187 begin
   188 
   189 lift_definition bot_dual :: "'a dual"
   190   is top .
   191 
   192 instance ..
   193 
   194 end
   195 
   196 lemma undual_bot_eq [simp]:
   197   "undual bot = top"
   198   by (fact bot_dual.rep_eq)
   199 
   200 lemma dual_top_eq [simp]:
   201   "dual top = bot"
   202   by transfer rule
   203 
   204 instantiation dual :: (bot) top
   205 begin
   206 
   207 lift_definition top_dual :: "'a dual"
   208   is bot .
   209 
   210 instance ..
   211 
   212 end
   213 
   214 lemma undual_top_eq [simp]:
   215   "undual top = bot"
   216   by (fact top_dual.rep_eq)
   217 
   218 lemma dual_bot_eq [simp]:
   219   "dual bot = top"
   220   by transfer rule
   221 
   222 instance dual :: (order_top) order_bot
   223   by (standard; transfer) simp
   224 
   225 instance dual :: (order_bot) order_top
   226   by (standard; transfer) simp
   227 
   228 instance dual :: (bounded_lattice_top) bounded_lattice_bot ..
   229 
   230 instance dual :: (bounded_lattice_bot) bounded_lattice_top ..
   231 
   232 instance dual :: (bounded_lattice) bounded_lattice ..
   233 
   234 
   235 subsection \<open>Complement\<close>
   236 
   237 instantiation dual :: (uminus) uminus
   238 begin
   239 
   240 lift_definition uminus_dual :: "'a dual \<Rightarrow> 'a dual"
   241   is uminus .
   242 
   243 instance ..
   244 
   245 end
   246 
   247 lemma undual_uminus_eq [simp]:
   248   "undual (- x) = - undual x"
   249   by (fact uminus_dual.rep_eq)
   250 
   251 lemma dual_uminus_eq [simp]:
   252   "dual (- x) = - dual x"
   253   by transfer rule
   254 
   255 instantiation dual :: (boolean_algebra) boolean_algebra
   256 begin
   257 
   258 lift_definition minus_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> 'a dual"
   259   is "\<lambda>x y. - (y - x)" .
   260 
   261 instance
   262   by (standard; transfer) (simp_all add: diff_eq ac_simps)
   263 
   264 end
   265 
   266 lemma undual_minus_eq [simp]:
   267   "undual (x - y) = - (undual y - undual x)"
   268   by (fact minus_dual.rep_eq)
   269 
   270 lemma dual_minus_eq [simp]:
   271   "dual (x - y) = - (dual y - dual x)"
   272   by transfer simp
   273 
   274 
   275 subsection \<open>Complete lattice operations\<close>
   276 
   277 text \<open>
   278   The class of complete lattices is closed under formation of dual
   279   structures.
   280 \<close>
   281 
   282 instantiation dual :: (Sup) Inf
   283 begin
   284 
   285 lift_definition Inf_dual :: "'a dual set \<Rightarrow> 'a dual"
   286   is Sup .
   287 
   288 instance ..
   289 
   290 end
   291 
   292 lemma undual_Inf_eq [simp]:
   293   "undual (Inf A) = Sup (undual ` A)"
   294   by (fact Inf_dual.rep_eq)
   295 
   296 lemma dual_Sup_eq [simp]:
   297   "dual (Sup A) = Inf (dual ` A)"
   298   by transfer simp
   299 
   300 instantiation dual :: (Inf) Sup
   301 begin
   302 
   303 lift_definition Sup_dual :: "'a dual set \<Rightarrow> 'a dual"
   304   is Inf .
   305 
   306 instance ..
   307 
   308 end
   309 
   310 lemma undual_Sup_eq [simp]:
   311   "undual (Sup A) = Inf (undual ` A)"
   312   by (fact Sup_dual.rep_eq)
   313 
   314 lemma dual_Inf_eq [simp]:
   315   "dual (Inf A) = Sup (dual ` A)"
   316   by transfer simp
   317 
   318 instance dual :: (complete_lattice) complete_lattice
   319   by (standard; transfer) (auto intro: Inf_lower Sup_upper Inf_greatest Sup_least)
   320 
   321 context
   322   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   323     and g :: "'a dual \<Rightarrow> 'a dual"
   324   assumes "mono f"
   325   defines "g \<equiv> dual \<circ> f \<circ> undual"
   326 begin
   327 
   328 private lemma mono_dual:
   329   "mono g"
   330 proof
   331   fix x y :: "'a dual"
   332   assume "x \<le> y"
   333   then have "undual y \<le> undual x"
   334     by (simp add: dual_less_eq_iff)
   335   with \<open>mono f\<close> have "f (undual y) \<le> f (undual x)"
   336     by (rule monoD)
   337   then have "(dual \<circ> f \<circ> undual) x \<le> (dual \<circ> f \<circ> undual) y"
   338     by simp
   339   then show "g x \<le> g y"
   340     by (simp add: g_def)
   341 qed
   342 
   343 lemma lfp_dual_gfp:
   344   "lfp f = undual (gfp g)" (is "?lhs = ?rhs")
   345 proof (rule antisym)
   346   have "dual (undual (g (gfp g))) \<le> dual (f (undual (gfp g)))"
   347     by (simp add: g_def)
   348   with mono_dual have "f (undual (gfp g)) \<le> undual (gfp g)"
   349     by (simp add: gfp_unfold [where f = g, symmetric] dual_less_eq_iff)
   350   then show "?lhs \<le> ?rhs"
   351     by (rule lfp_lowerbound)
   352   from \<open>mono f\<close> have "dual (lfp f) \<le> dual (undual (gfp g))"
   353     by (simp add: lfp_fixpoint gfp_upperbound g_def)
   354   then show "?rhs \<le> ?lhs"
   355     by (simp only: less_eq_dual_iff)
   356 qed
   357 
   358 lemma gfp_dual_lfp:
   359   "gfp f = undual (lfp g)"
   360 proof -
   361   have "mono (\<lambda>x. undual (undual x))"
   362     by (rule monoI)  (simp add: dual_less_eq_iff)
   363   moreover have "mono (\<lambda>a. dual (dual (f a)))"
   364     using \<open>mono f\<close> by (auto intro: monoI dest: monoD)
   365   moreover have "gfp f = gfp (\<lambda>x. undual (undual (dual (dual (f x)))))"
   366     by simp
   367   ultimately have "undual (undual (gfp (\<lambda>x. dual
   368     (dual (f (undual (undual x))))))) =
   369       gfp (\<lambda>x. undual (undual (dual (dual (f x)))))"
   370     by (subst gfp_rolling [where g = "\<lambda>x. undual (undual x)"]) simp_all
   371   then have "gfp f =
   372     undual
   373      (undual
   374        (gfp (\<lambda>x. dual (dual (f (undual (undual x)))))))"
   375     by simp
   376   also have "\<dots> = undual (undual (gfp (dual \<circ> g \<circ> undual)))"
   377     by (simp add: comp_def g_def)
   378   also have "\<dots> = undual (lfp g)"
   379     using mono_dual by (simp only: Dual_Ordered_Lattice.lfp_dual_gfp)
   380   finally show ?thesis .
   381 qed
   382 
   383 end
   384 
   385 
   386 text \<open>Finally\<close>
   387 
   388 lifting_update dual.lifting
   389 lifting_forget dual.lifting
   390 
   391 end